Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 601:8b2a4af84e25
sup done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Jun 2022 11:08:15 +0900 |
| parents | 71a1ed72cd21 |
| children | 0ef3ef93c5c3 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 26 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jun 14 06:17:24 2022 +0900 +++ b/src/zorn.agda Tue Jun 14 11:08:15 2022 +0900 @@ -241,7 +241,6 @@ record FSup ( A : HOD ) ( f : Ordinal → Ordinal ) (p c : Ordinal) ( x : Ordinal ) : Set n where field sup : (z : Ordinal) → FClosure A f p z → * z < * x - min : ( x1 : Ordinal) → ((z : Ordinal) → FClosure A f p z → * z < * x1 ) → ( x ≡ x1 ) ∨ ( * x < * x1 ) chain∋x : odef (* c) x chain∋p : odef (* c) p @@ -262,6 +261,7 @@ is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc z → (ab : odef A b) → HasPrev A chain ab f ∨ IsSup A chain ab → * a < * b → odef chain b + chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b) → IsSup A s ab → odef chain b fc∨sup : {c : Ordinal } → ( ca : odef chain c ) → Fc∨sup A (chain⊆A chain∋x) f (& chain) c @@ -423,7 +423,7 @@ zc4 with ODC.∋-p O A (* x) ... | no noax = -- ¬ A ∋ p, just skip record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 - ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!} ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = ZChain.fc∨sup zc0 } where -- no extention zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab → @@ -442,10 +442,11 @@ ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr)) zc9 : ZChain A y f x zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 -- no extention + ; chain∋sup = {!!} ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = ZChain.fc∨sup zc0 } ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax ) ... | case1 is-sup = -- x is a sup of zc0 - record { chain = schain ; chain⊆A = s⊆A ; f-total = scmp ; f-next = scnext + record { chain = schain ; chain⊆A = s⊆A ; f-total = scmp ; f-next = scnext ; chain∋sup = {!!} ; initial = scinit ; f-immediate = simm ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = s-fc∨sup} where sup0 : SUP A (ZChain.chain zc0) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where @@ -549,7 +550,7 @@ ... | case1 y=b = subst (λ k → odef chain k ) y=b ( ZChain.chain∋x zc0 ) ... | case2 y<b = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b ... | case2 ¬x=sup = -- x is not f y' nor sup of former ZChain from y - record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!} ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = ZChain.fc∨sup zc0 } where -- no extention z18 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → @@ -562,12 +563,12 @@ ... | case2 b=sup = ⊥-elim ( ¬x=sup record { x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) ... | no ¬ox with trio< x y - ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} + ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!} ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b y<x = UnionZ where UnionZ : ZChain A y f x - UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next + UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next ; chain∋sup = {!!} ; initial = u-initial ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } where --- limit ordinal case record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x field @@ -599,7 +600,25 @@ um01 : odef (chain zb) i um01 with FC ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb ) - ... | Fsup {p} {i} p<i pFC sup = ? + ... | Fsup {p} {i} p<i pFC sup = cb∋i where + ca∋i : odef (chain za) i + ca∋i = subst (λ k → odef k i) *iso (FSup.chain∋x sup) + i-asup : (z : Ordinal) → FClosure A f p z → * z < * i + i-asup = FSup.sup sup + um06 : odef (chain za) p + um06 = subst (λ k → odef k p ) *iso ( FSup.chain∋p sup ) + -- FClosure A f p is a subset of chain zb + um07 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2 + um07 i2 (init ap ) = previ p p<i um06 + um07 i (fsuc j fc) = f-next zb ( um07 j fc ) + um08 : odef (chain zb) p + um08 = previ p p<i um06 + cl : HOD + cl = record { od = record { def = λ x → FClosure A f p x } ; odmax = & A ; <odmax = λ lt → cla lt } where + cla : {i2 : Ordinal} → FClosure A f p i2 → i2 o< & A + cla {i2} cl = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (A∋fc p f mf cl) ) ) + cb∋i : odef (chain zb) i + cb∋i = ZChain.chain∋sup zb cl (λ {i2} lt → um07 i2 lt) (chain⊆A za zai) record { x<sup = λ {i2} cl → case2 (i-asup i2 cl) } ... | Fc {p} {i} p<i pFC FC with (FChain.fc∨sup FC) ... | fc = um02 i fc where um02 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2