Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 878:1ec8c0cfc892
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 Sep 2022 10:52:57 +0900 |
| parents | eaa863c4ebe8 |
| children | 6222efcf3b04 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 45 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Sep 20 10:06:23 2022 +0900 +++ b/src/zorn.agda Sat Sep 24 10:52:57 2022 +0900 @@ -261,6 +261,12 @@ ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z +-- +-- f (f ( ... (sup y))) f (f ( ... (sup z1))) +-- / | / | +-- / | / | +-- sup y < sup z1 < sup z2 +-- o< o< -- data UChain is total chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) @@ -351,12 +357,6 @@ ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy ) ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) --- --- f (f ( ... (sup y))) f (f ( ... (sup z1))) --- / | / | --- / | / | --- sup y < sup z1 < sup z2 --- o< o< record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where @@ -372,11 +372,13 @@ sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) + csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) + + supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y - supf-max : {x : Ordinal } → supf x o≤ supf z supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y - x≤supfx : {x : Ordinal } → x o≤ supf x - csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) + x≤supfx : z o≤ supf z + chain∋init : odef chain y chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ f-next : {a : Ordinal} → odef chain a → odef chain (f a) @@ -522,6 +524,23 @@ sp1 : {z : Ordinal } → z o≤ x → SUP A (UnionCF A f mf ay (ZChain.supf zc) z) sp1 {z} z≤x = ZChain.sup zc z≤x + record MinSUP ( A B : HOD ) (z : Ordinal) : Set (Level.suc n) where + field + sup : HOD + asm : A ∋ sup + x<sup : {x : HOD} → B ∋ x → (& x) o< z → (x ≡ sup ) ∨ (x < sup ) + minsup : {x sup1 : HOD} → B ∋ x → (& x) o< z → (x ≡ sup1 ) ∨ (x < sup1 ) → sup ≤ sup1 + + msupP : {B : HOD} → MinSUP A B (& A) + msupP {B} = tf (& A) where + ind : (x : Ordinal) → ((y : Ordinal) → y o< x → MinSUP A B y) → MinSUP A B x + ind x prev = ? + tf : (z : Ordinal) → MinSUP A B z + tf z = TransFinite {λ x → MinSUP A B x } ind z + + M→S : {B : HOD} {z : Ordinal } → (& B) o< z → MinSUP A B z → SUP A B + M→S {B} lt ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = ? } + -- -- Second TransFinite Pass for maximality -- @@ -892,23 +911,23 @@ ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ? } ... | tri> ¬a ¬b px<z = record { tsup = ? ; tsup=sup = ? } - -- csupf1 : {b : Ordinal } → supf1 b o< z → odef (UnionCF A f mf ay supf1 z) (supf1 b) - -- csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z - -- record { fcy<sup = ZChain.fcy<sup zc (o<→≤ sb<z) ; order = order ; supu=u = ZChain.supf-idem zc } - -- (init (subst (λ k → odef A k) (sym (ZChain.supf-idem zc) asb)) (ZChain.supf-idem zc)) ⟫ where - -- b<z : b o< z - -- b<z = supf-inject0 (ZChain.supf-mono zc ( ordtrans<-≤ sb<z x≤supfx )) - -- asb : odef A (supf b) - -- asb = supf∈A (o<→≤ b<z) - -- supb : SUP A (UnionCF A f mf ay supf (supf b)) - -- supb = ZChain.sup zc (o<→≤ sb<z) - -- supb-is-b : supf (supf b) ≡ & (SUP.sup supb) - -- supb-is-b = ZChain.supf-is-sup zc (o<→≤ sb<z) - -- order : {s z1 : Ordinal} → supf s o< supf (supf b) → - -- FClosure A f (supf s) z1 → (z1 ≡ supf (supf b)) ∨ (z1 << supf (supf b)) - -- order {s} {z1} ss<ssb fs with SUP.x<sup supb ? - -- ... | case1 eq = ? - -- ... | case2 lt = ? + csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) + csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z + record { fcy<sup = ? ; order = order ; supu=u = ? } + (init ? ? ) ⟫ where + b<x : b o< x + b<x = ZChain.supf-inject zc ? + asb : odef A (supf1 b) + asb = ? -- ZChain.supf∈A zc ? -- (o<→≤ b<x) + supb : SUP A (UnionCF A f mf ay supf1 (supf1 b)) + supb = ? -- ZChain.sup zc (o<→≤ sb<z) + supb-is-b : supf1 (supf1 b) ≡ & (SUP.sup supb) + supb-is-b = ? -- ZChain.supf-is-sup zc ? -- (o<→≤ sb<z) + order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b)) + order {s} {z1} ss<ssb fs with SUP.x<sup supb ? + ... | case1 eq = ? + ... | case2 lt = ? ... | case2 px<spfx = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where