Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 300:e70980bd80c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
-- the set of finite partial functions from ω to 2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jun 2020 15:12:43 +0900
parents ef93c56ad311
children b012a915bbb5
comparison
equal deleted inserted replaced
296:42f89e5efb00 300:e70980bd80c7
206 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) 206 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
207 207
208 ZFSubset : (A x : OD ) → OD 208 ZFSubset : (A x : OD ) → OD
209 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set 209 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set
210 210
211 Def : (A : OD ) → OD 211 OPwr : (A : OD ) → OD
212 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) 212 OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) )
213 213
214 -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n 214 -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n
215 -- _⊆_ A B {x} = A ∋ x → B ∋ x 215 -- _⊆_ A B {x} = A ∋ x → B ∋ x
216 216
217 record _⊆_ ( A B : OD ) : Set (suc n) where 217 record _⊆_ ( A B : OD ) : Set (suc n) where
266 Union : OD → OD 266 Union : OD → OD
267 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 267 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
268 _∈_ : ( A B : ZFSet ) → Set n 268 _∈_ : ( A B : ZFSet ) → Set n
269 A ∈ B = B ∋ A 269 A ∈ B = B ∋ A
270 Power : OD → OD 270 Power : OD → OD
271 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 271 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
272 -- ｛_｝ : ZFSet → ZFSet 272 -- ｛_｝ : ZFSet → ZFSet
273 -- ｛ x ｝ = ( x , x ) -- it works but we don't use 273 -- ｛ x ｝ = ( x , x ) -- it works but we don't use
274 274
275 data infinite-d : ( x : Ordinal ) → Set n where 275 data infinite-d : ( x : Ordinal ) → Set n where
276 iφ : infinite-d o∅ 276 iφ : infinite-d o∅
367 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; 367 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ;
368 eq← = λ {x} x<a∩b → proj2 x<a∩b } 368 eq← = λ {x} x<a∩b → proj2 x<a∩b }
369 -- 369 --
370 -- Transitive Set case 370 -- Transitive Set case
371 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t 371 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t
372 -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t 372 -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t
373 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 373 -- OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
374 -- 374 --
375 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t 375 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
376 ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t} 376 ord-power← a t t→A = def-subst {_} {_} {OPwr (Ord a)} {od→ord t}
377 lemma refl (lemma1 lemma-eq )where 377 lemma refl (lemma1 lemma-eq )where
378 lemma-eq : ZFSubset (Ord a) t == t 378 lemma-eq : ZFSubset (Ord a) t == t
379 eq→ lemma-eq {z} w = proj2 w 379 eq→ lemma-eq {z} w = proj2 w
380 eq← lemma-eq {z} w = record { proj2 = w ; 380 eq← lemma-eq {z} w = record { proj2 = w ;
381 proj1 = def-subst {_} {_} {(Ord a)} {z} 381 proj1 = def-subst {_} {_} {(Ord a)} {z}
385 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 385 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
386 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x)) 386 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x))
387 lemma = sup-o< 387 lemma = sup-o<
388 388
389 -- 389 --
390 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first 390 -- Every set in OD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
391 -- then replace of all elements of the Power set by A ∩ y 391 -- then replace of all elements of the Power set by A ∩ y
392 -- 392 --
393 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) 393 -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y )
394 394
395 -- we have oly double negation form because of the replacement axiom 395 -- we have oly double negation form because of the replacement axiom
396 -- 396 --
397 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) 397 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
398 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where 398 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
399 a = od→ord A 399 a = od→ord A
400 lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) 400 lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y)))
401 lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t 401 lemma2 = replacement→ (OPwr (Ord (od→ord A))) t P∋t
402 lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) 402 lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x)
403 lemma3 y eq not = not (proj1 (eq→ eq t∋x)) 403 lemma3 y eq not = not (proj1 (eq→ eq t∋x))
404 lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) 404 lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y)))
405 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 )) 405 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 ))
406 lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → ¬ ¬ (def A (od→ord x)) 406 lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → ¬ ¬ (def A (od→ord x))
409 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t 409 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
410 power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 410 power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where
411 a = od→ord A 411 a = od→ord A
412 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x 412 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
413 lemma0 {x} t∋x = c<→o< (t→A t∋x) 413 lemma0 {x} t∋x = c<→o< (t→A t∋x)
414 lemma3 : Def (Ord a) ∋ t 414 lemma3 : OPwr (Ord a) ∋ t
415 lemma3 = ord-power← a t lemma0 415 lemma3 = ord-power← a t lemma0
416 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t 416 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t
417 lemma4 = let open ≡-Reasoning in begin 417 lemma4 = let open ≡-Reasoning in begin
418 A ∩ ord→od (od→ord t) 418 A ∩ ord→od (od→ord t)
419 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ 419 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
422 t 422 t
423 ∎ 423 ∎
424 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) 424 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x))
425 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) 425 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x)))
426 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) 426 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} )
427 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 427 lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
428 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 428 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
429 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 429 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
430 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 430 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
431 431
432 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 432 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))