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

comparison OD.agda @ 207:3e4eb4da1453

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try again ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2019 00:13:07 +0900
parents 684d70f1f26b
children 64ef1db53c49
comparison
equal deleted inserted replaced
206:684d70f1f26b 207:3e4eb4da1453
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 = have_to_find 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 ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
570 <-not {X} ox = ( y : Ordinal {suc n}) → y o< ox → ¬ (X ∋ (ord→od y)) 570 ψ ox = ( x : Ordinal {suc n}) → x o< ox → ¬ (def X x ) ∨ choiced X
571 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox ∨ choiced X 571 lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
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)} {ψ} 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 {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
574 <-not {X} (record { lv = lx ; ord = Φ lx }) ∨ choiced X
575 caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) )) 574 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 } ) 575 caseΦ lx prev | yes p = ? -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
577 caseΦ lx prev | no ¬p = lemma (ordinal lx (Φ lx)) <-osuc where 576 caseΦ lx prev | no ¬p = ?
578 lemma : (x : Ordinal {suc n}) → x o< osuc (ordinal lx (Φ lx)) 577 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
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
585 caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) ∨ choiced X) →
586 <-not {X} (record { lv = lx ; ord = OSuc lx x }) ∨ choiced X
587 caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } ) 578 caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
588 caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }) 579 caseOSuc lx x prev | yes p = ? -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
589 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where 580 caseOSuc lx x prev | no ¬p = ?
590 lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X (od→ord (ord→od y)) → ⊥
591 lemma y lt with trio< y (ordinal lx x )
592 lemma y lt | tri< a ¬b ¬c = not_found y a
593 lemma y lt | tri≈ ¬a refl ¬c = ¬p
594 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
595 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
596 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
597 caseOSuc lx x (case2 found) | no ¬p = case2 found
598 have_to_find : choiced X 581 have_to_find : choiced X
599 have_to_find with lemma-ord (od→ord X ) 582 have_to_find with lemma-ord (od→ord X )
600 have_to_find | case1 not_found = ⊥-elim ( not ( record { 583 have_to_find | t = ?
601 eq→ = λ {x} lt → ⊥-elim (not_found x (def→o< lt) (def-subst {suc n} {_} {_} {X} {_} lt refl (sym diso ))) ; 584
602 eq← = λ lt → ⊥-elim (¬x<0 lt) } ) )
603 have_to_find | case2 found = found
604