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

comparison src/OD.agda @ 1286:619e68271cf8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 May 2023 19:06:25 +0900
parents 302cfb533201
children d9f3774ddb00
comparison
equal deleted inserted replaced
1285:302cfb533201 1286:619e68271cf8
258 _,_ : HOD → HOD → HOD 258 _,_ : HOD → HOD → HOD
259 x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x) (& y) ; <odmax = lemma } where 259 x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x) (& y) ; <odmax = lemma } where
260 lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y) 260 lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y)
261 lemma {t} (case1 refl) = omax-x _ _ 261 lemma {t} (case1 refl) = omax-x _ _
262 lemma {t} (case2 refl) = omax-y _ _ 262 lemma {t} (case2 refl) = omax-y _ _
263
264 -- {x y : HOD} → & (x , y) ≡ omax (& x) (& y)
263 265
264 pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y) 266 pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y)
265 pair<y {x} {y} y∋x = ⊆→o≤ lemma where 267 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
266 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z 268 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
267 lemma (case1 refl) = y∋x 269 lemma (case1 refl) = y∋x
458 -- This means that many of OD may not be HODs because of the & mapping divergence. 460 -- This means that many of OD may not be HODs because of the & mapping divergence.
459 -- We should have some axioms to prevent this such as & x o< next (odmax x). 461 -- We should have some axioms to prevent this such as & x o< next (odmax x).
460 -- 462 --
461 -- Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho< 463 -- Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
462 464
465 infinite-od : OD
466 infinite-od = record { def = λ x → infinite-d x }
467
468 postulate
469 infinite-odmax : Ordinal
470 infinite-odmax< : {z : Ordinal } → def infinite-od z → z o< infinite-odmax
471
463 infinite : HOD 472 infinite : HOD
464 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 473 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = infinite-odmax ; <odmax = infinite-odmax< }
465 u : (y : Ordinal ) → HOD 474
466 u y = Union (* y , (* y , * y)) 475 -- where
467 -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z 476 -- u : (y : Ordinal ) → HOD
468 lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y)) 477 -- u y = Union (* y , (* y , * y))
469 lemma8 = ho< 478 -- -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
470 --- (x,y) < next (omax x y) < next (osuc y) = next y 479 -- lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
471 lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y) 480 -- lemma8 = ho<
472 lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< ) 481 -- --- (x,y) < next (omax x y) < next (osuc y) = next y
473 lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y)) 482 -- lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
474 lemma81 {y} = nexto=n (subst (λ k → & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) 483 -- lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
475 lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y)) 484 -- lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
476 lemma9 = lemmaa (c<→o< (case1 refl)) 485 -- lemma81 {y} = nexto=n (subst (λ k → & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
477 lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y)) 486 -- lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
478 lemma71 = next< lemma81 lemma9 487 -- lemma9 = lemmaa (c<→o< (case1 refl))
479 lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y)))) 488 -- lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
480 lemma1 = ho< 489 -- lemma71 = ? -- next< lemma81 lemma9
481 --- main recursion 490 -- lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
482 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 491 -- lemma1 = ho<
483 lemma {o∅} iφ = x<nx 492 -- --- main recursion
484 lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1)) 493 -- lemma : {y : Ordinal} → infinite-d y → y o< next o∅
494 -- lemma {o∅} iφ = x<nx
495 -- lemma (isuc {y} x) = ? -- next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
485 496
486 empty : (x : HOD ) → ¬ (od∅ ∋ x) 497 empty : (x : HOD ) → ¬ (od∅ ∋ x)
487 empty x = ¬x<0 498 empty x = ¬x<0
488 499
489 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) 500 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y )