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

comparison OD.agda @ 197:b114cf5b9130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
transfinite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2019 18:27:22 +0900
parents a3211dcb4d83
children 8589660ee388
comparison
equal deleted inserted replaced
196:a3211dcb4d83 197:b114cf5b9130
511 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) 511 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
512 ε-induction-ord Zero (Φ 0) (case1 ()) 512 ε-induction-ord Zero (Φ 0) (case1 ())
513 ε-induction-ord Zero (Φ 0) (case2 ()) 513 ε-induction-ord Zero (Φ 0) (case2 ())
514 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = 514 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x =
515 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where 515 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
516 lemma : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } 516 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
517 lemma y lt with osuc-≡< y<x 517 lemma z lt with osuc-≡< y<x
518 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso 518 lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso
519 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 519 lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1
520 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = 520 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =
521 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where 521 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where
522 -- 522 --
523 -- if lv of z if less than x Ok 523 -- if lv of z if less than x Ok
524 -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma 524 -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma
561 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where 561 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
562 field 562 field
563 a-choice : OD {suc n} 563 a-choice : OD {suc n}
564 is-in : X ∋ a-choice 564 is-in : X ∋ a-choice
565 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X 565 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X
566 choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X))) <-osuc 566 choice-func' X ∋-p not = lemma-ord (od→ord X) lemma-init
567 where 567 where
568 lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } 568 <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
569 → (ly < lx) ∨ (oy d< ox ) → choiced X 569 <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y))
570 lemma-ord Zero (Φ 0) (case1 ()) 570 lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y)
571 lemma-ord Zero (Φ 0) (case2 ()) 571 lemma-init y lt lt2 with osuc-≡< lt
572 lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox }) 572 lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl )
573 lemma-ord lx (OSuc lx ox) lt | yes p = record { a-choice = ord→od record { lv = lx ; ord = OSuc lx ox } ; is-in = p } 573 lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl )
574 lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!} 574 lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X
575 lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}) 575 lemma-ord ox = TransFinite {suc n} {suc (suc n)} {λ ox → <-not {X} ox → choiced X } caseΦ caseOSuc ox where
576 lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = record { a-choice = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)} ; is-in = p } 576 caseΦ : (lx : Nat) → <-not {X} (record { lv = lx ; ord = Φ lx }) → choiced X
577 lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!} 577 caseΦ Zero n = ⊥-elim ( not {!!} )
578 caseΦ (Suc lx) n = caseΦ lx ( λ y lt → {!!} )
579 caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) → choiced X) →
580 <-not {X} (record { lv = lx ; ord = OSuc lx x }) → choiced X
581 caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
582 caseOSuc lx x prev | yes p = λ _ → record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }
583 caseOSuc lx x prev | no ¬p = λ px → prev ( λ y lt → {!!} )
584