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

comparison OD.agda @ 209:e59e682ad120

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
∀-imply-or
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2019 10:22:16 +0900
parents 64ef1db53c49
children 2c7d45734e3b
comparison
equal deleted inserted replaced
208:64ef1db53c49 209:e59e682ad120
561 561
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∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
567 choice-func' X ∋-p not = have_to_find 567 choice-func' X p∨¬p not = have_to_find
568 where 568 where
569 ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n)) 569 ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
570 ψ ox = ( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x ) ∨ choiced X 570 ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X
571 lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox 571 lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
572 lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where 572 lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where
573 ∋-p' : (A x : OD {suc n} ) → Dec ( A ∋ x )
574 ∋-p' A x with p∨¬p ( A ∋ x )
575 ∋-p' A x | case1 t = yes t
576 ∋-p' A x | case2 t = no t
577 ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
578 → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B
579 ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x)
580 ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
581 ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
582 lemma : ¬ ((x : Ordinal {suc n}) → A x) → B
583 lemma not with p∨¬p B
584 lemma not | case1 b = b
585 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
573 caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) 586 caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
574 caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) )) 587 caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
575 caseΦ lx prev | yes p = {!!} -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) 588 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
576 caseΦ lx prev | no ¬p = {!!} 589 caseΦ lx prev | no ¬p = lemma where
590 lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
591 lemma1 x with trio< x (ordinal lx (Φ lx))
592 lemma1 x | tri< a ¬b ¬c with prev x a
593 lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 {!!}
594 lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
595 lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
596 lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
597 lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
598 lemma = ∀-imply-or lemma1
577 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) ) 599 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
578 caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } ) 600 caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
579 caseOSuc lx x prev | yes p = {!!} -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }) 601 caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
580 caseOSuc lx x prev | no ¬p = {!!} 602 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
603 lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
604 lemma y lt with trio< y (ordinal lx x )
605 lemma y lt | tri< a ¬b ¬c = not_found y a
606 lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
607 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
608 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
609 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
610 caseOSuc lx x (case2 found) | no ¬p = case2 found
581 have_to_find : choiced X 611 have_to_find : choiced X
582 have_to_find with lemma-ord (od→ord X ) 612 have_to_find with lemma-ord (od→ord X )
583 have_to_find | t = dont-or ( t (od→ord X) {!!} ) {!!} 613 have_to_find | t = dont-or t {!!}
584 614