Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 197:b114cf5b9130
transfinite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Jul 2019 18:27:22 +0900 |
| parents | a3211dcb4d83 |
| children | 8589660ee388 |
| files | OD.agda |
| diffstat | 1 files changed, 22 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Mon Jul 29 11:58:10 2019 +0900 +++ b/OD.agda Mon Jul 29 18:27:22 2019 +0900 @@ -513,10 +513,10 @@ ε-induction-ord Zero (Φ 0) (case2 ()) ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where - lemma : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } - lemma y lt with osuc-≡< y<x - lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso - lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 + lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox } + lemma z lt with osuc-≡< y<x + lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso + lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where -- @@ -563,15 +563,22 @@ a-choice : OD {suc n} is-in : X ∋ a-choice choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X - choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X))) <-osuc + choice-func' X ∋-p not = lemma-ord (od→ord X) lemma-init where - lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } - → (ly < lx) ∨ (oy d< ox ) → choiced X - lemma-ord Zero (Φ 0) (case1 ()) - lemma-ord Zero (Φ 0) (case2 ()) - lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox }) - lemma-ord lx (OSuc lx ox) lt | yes p = record { a-choice = ord→od record { lv = lx ; ord = OSuc lx ox } ; is-in = p } - lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!} - lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}) - lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = record { a-choice = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)} ; is-in = p } - lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!} + <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n) + <-not {X} ox = ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) + lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y) + lemma-init y lt lt2 with osuc-≡< lt + lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl ) + lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl ) + lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X + lemma-ord ox = TransFinite {suc n} {suc (suc n)} {λ ox → <-not {X} ox → choiced X } caseΦ caseOSuc ox where + caseΦ : (lx : Nat) → <-not {X} (record { lv = lx ; ord = Φ lx }) → choiced X + caseΦ Zero n = ⊥-elim ( not {!!} ) + caseΦ (Suc lx) n = caseΦ lx ( λ y lt → {!!} ) + caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) → choiced X) → + <-not {X} (record { lv = lx ; ord = OSuc lx x }) → choiced X + caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } ) + caseOSuc lx x prev | yes p = λ _ → record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p } + caseOSuc lx x prev | no ¬p = λ px → prev ( λ y lt → {!!} ) +