Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 206:684d70f1f26b
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 31 Jul 2019 17:48:08 +0900 |
parents | 61ff37d51230 |
children | 3e4eb4da1453 |
comparison
equal
deleted
inserted
replaced
205:61ff37d51230 | 206:684d70f1f26b |
---|---|
562 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 |
563 field | 563 field |
564 a-choice : OD {suc n} | 564 a-choice : OD {suc n} |
565 is-in : X ∋ a-choice | 565 is-in : X ∋ a-choice |
566 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 |
567 choice-func' X ∋-p not = lemma0 | 567 choice-func' X ∋-p not = have_to_find |
568 where | 568 where |
569 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) | 569 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) |
570 <-not {X} ox = ( y : Ordinal {suc n}) → y o< ox → ¬ (X ∋ (ord→od y)) | 570 <-not {X} ox = ( y : Ordinal {suc n}) → y o< ox → ¬ (X ∋ (ord→od y)) |
571 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox ∨ choiced X | 571 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox ∨ choiced X |
572 lemma-ord ox = TransFinite {n} {suc (suc n)} {λ ox → <-not {X} ox ∨ choiced X } caseΦ caseOSuc ox where | 572 lemma-ord ox = TransFinite {n} {suc (suc n)} {λ ox → <-not {X} ox ∨ choiced X } caseΦ caseOSuc ox where |
573 caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → <-not {X} x ∨ choiced X) → | 573 caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → <-not {X} x ∨ choiced X) → |
574 <-not {X} (record { lv = lx ; ord = Φ lx }) ∨ choiced X | 574 <-not {X} (record { lv = lx ; ord = Φ lx }) ∨ choiced X |
575 caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) )) | 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 } ) | 576 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) |
577 caseΦ lx prev | no ¬p = {!!} | 577 caseΦ lx prev | no ¬p = lemma (ordinal lx (Φ lx)) <-osuc where |
578 lemma : (x : Ordinal {suc n}) → x o< osuc (ordinal lx (Φ lx)) | |
579 → ((y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< Φ lx) → def X (od→ord (ord→od y)) → ⊥) ∨ choiced X | |
580 lemma x lt with osuc-≡< lt | |
581 lemma x lt | case1 refl = case1 ? | |
582 lemma x lt | case2 lt1 with prev x lt1 | |
583 lemma x lt | case2 lt1 | case1 lt2 = case1 {!!} | |
584 lemma x lt | case2 lt1 | case2 found = case2 found | |
578 caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) ∨ choiced X) → | 585 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 | 586 <-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 } ) | 587 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 }) | 588 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 | 589 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where |
586 lemma y lt | tri≈ ¬a refl ¬c = ¬p | 593 lemma y lt | tri≈ ¬a refl ¬c = ¬p |
587 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt | 594 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt |
588 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl ) | 595 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 ) | 596 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 ) |
590 caseOSuc lx x (case2 found) | no ¬p = case2 found | 597 caseOSuc lx x (case2 found) | no ¬p = case2 found |
591 lemma0 : choiced X | 598 have_to_find : choiced X |
592 lemma0 with lemma-ord (od→ord X ) | 599 have_to_find with lemma-ord (od→ord X ) |
593 lemma0 | case1 not_found = ⊥-elim ( not ( record { | 600 have_to_find | 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 ))) ; | 601 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) } ) ) | 602 eq← = λ lt → ⊥-elim (¬x<0 lt) } ) ) |
596 lemma0 | case2 found = found | 603 have_to_find | case2 found = found |
597 | 604 |