Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 205:61ff37d51230
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 31 Jul 2019 17:17:24 +0900 |
parents | d4802eb159ff |
children | 684d70f1f26b |
comparison
equal
deleted
inserted
replaced
204:d4802eb159ff | 205:61ff37d51230 |
---|---|
101 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) | 101 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) |
102 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) | 102 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) |
103 | 103 |
104 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y | 104 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y |
105 otrans x<a y<x = ordtrans y<x x<a | 105 otrans x<a y<x = ordtrans y<x x<a |
106 | |
107 def→o< : {n : Level } {X : OD {suc n}} → {x : Ordinal {suc n}} → def X x → x o< od→ord X | |
108 def→o< {n} {X} {x} lt = o<-subst {suc n} {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {suc n} {X} {x} lt (sym oiso) (sym diso) )) diso diso | |
106 | 109 |
107 ∅3 : {n : Level} → { x : Ordinal {suc n}} → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n} | 110 ∅3 : {n : Level} → { x : Ordinal {suc n}} → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n} |
108 ∅3 {n} {x} = TransFinite {n} c2 c3 x where | 111 ∅3 {n} {x} = TransFinite {n} c2 c3 x where |
109 c0 : Nat → Ordinal {suc n} → Set (suc n) | 112 c0 : Nat → Ordinal {suc n} → Set (suc n) |
110 c0 lx x = (∀(y : Ordinal {suc n}) → ¬ (y o< x)) → x ≡ o∅ {suc n} | 113 c0 lx x = (∀(y : Ordinal {suc n}) → ¬ (y o< x)) → x ≡ o∅ {suc n} |
559 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where | 562 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where |
560 field | 563 field |
561 a-choice : OD {suc n} | 564 a-choice : OD {suc n} |
562 is-in : X ∋ a-choice | 565 is-in : X ∋ a-choice |
563 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X | 566 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X |
564 choice-func' X ∋-p not = {!!} where | 567 choice-func' X ∋-p not = lemma0 |
565 lemma-ord : ( lx : Nat ) (ox : OrdinalD lx ) → {ly : Nat} → {oy : OrdinalD ly } | 568 where |
566 → ordinal ly oy o< ordinal lx ox → choiced X ∨ ( ¬ ( def X (ordinal ly oy) )) | 569 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) |
567 lemma-ord lx (OSuc lx ox) y<x with ∋-p X (ord→od (ordinal lx (OSuc lx ox))) | 570 <-not {X} ox = ( y : Ordinal {suc n}) → y o< ox → ¬ (X ∋ (ord→od y)) |
568 lemma-ord lx (OSuc lx ox) y<x | yes p = case1 ( record { a-choice = (ord→od (ordinal lx (OSuc lx ox))) ; is-in = p } ) | 571 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox ∨ choiced X |
569 lemma-ord lx (OSuc lx ox) y<x | no ¬p with osuc-≡< y<x | 572 lemma-ord ox = TransFinite {n} {suc (suc n)} {λ ox → <-not {X} ox ∨ choiced X } caseΦ caseOSuc ox where |
570 lemma-ord lx (OSuc lx ox) y<x | no ¬p | case1 refl = {!!} | 573 caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → <-not {X} x ∨ choiced X) → |
571 lemma-ord lx (OSuc lx ox) y<x | no ¬p | case2 t = lemma-ord lx ox t | 574 <-not {X} (record { lv = lx ; ord = Φ lx }) ∨ choiced X |
572 lemma-ord (Suc lx) (Φ (Suc lx)) (case1 x) = {!!} | 575 caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) )) |
576 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) | |
577 caseΦ lx prev | no ¬p = {!!} | |
578 caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) ∨ choiced X) → | |
579 <-not {X} (record { lv = lx ; ord = OSuc lx x }) ∨ choiced X | |
580 caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } ) | |
581 caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }) | |
582 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where | |
583 lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X (od→ord (ord→od y)) → ⊥ | |
584 lemma y lt with trio< y (ordinal lx x ) | |
585 lemma y lt | tri< a ¬b ¬c = not_found y a | |
586 lemma y lt | tri≈ ¬a refl ¬c = ¬p | |
587 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt | |
588 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl ) | |
589 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 ) | |
590 caseOSuc lx x (case2 found) | no ¬p = case2 found | |
591 lemma0 : choiced X | |
592 lemma0 with lemma-ord (od→ord X ) | |
593 lemma0 | case1 not_found = ⊥-elim ( not ( record { | |
594 eq→ = λ {x} lt → ⊥-elim (not_found x (def→o< lt) (def-subst {suc n} {_} {_} {X} {_} lt refl (sym diso ))) ; | |
595 eq← = λ lt → ⊥-elim (¬x<0 lt) } ) ) | |
596 lemma0 | case2 found = found | |
597 |