Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 548:5ad7a31df4f4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 28 Apr 2022 10:29:47 +0900 |
| parents | 379bd9b4610c |
| children | f007e044b2c6 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 24 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Apr 27 23:21:21 2022 +0900 +++ b/src/zorn.agda Thu Apr 28 10:29:47 2022 +0900 @@ -200,7 +200,7 @@ f-total : IsTotalOrderSet chain f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) - is-max : {a b : Ordinal } → (ca : odef chain a ) → a o< z → (ba : odef A b) + is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< z → (ba : odef A b) → Prev< A chain ba f ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ) → * a < * b → odef chain b @@ -277,7 +277,7 @@ z03 f mf zc = z14 where chain = ZChain.chain zc sp1 = sp0 f mf zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → a o< & A → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) → Prev< A chain ab f ∨ (supO (& chain) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b ) → * a < * b → odef chain b @@ -287,7 +287,7 @@ z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) s<A (SUP.A∋maximal sp1) (case2 refl ) z13 where + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) z11 (SUP.A∋maximal sp1) (case2 refl ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc )) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) @@ -315,13 +315,14 @@ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc c = & (SUP.sup sp1) - premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain A sa f mf supO y ) - → {a b : Ordinal} (ca : odef (ZChain.chain zc0) a) → (ab : odef A b) → a o< y - → Prev< A (ZChain.chain zc0) ab f ∨ (supO (& (ZChain.chain zc0)) - (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) - (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b) - → * a < * b → odef (ZChain.chain zc0) b - premax {x} {y} y<x f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca a<y ab P a<b -- ca ab y P a<b + + 3cases : {x y : Ordinal} → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) + → (ax : odef A x )→ (ay : odef A y ) + → (zc0 : ZChain A ay f mf supO x ) + → Prev< A (ZChain.chain zc0) ax f + ∨ (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ x) + ∨ ( ( z : Ordinal) → odef (ZChain.chain zc0) z → ¬ ( * z < * x )) + 3cases {x} {y} f mf ax ay zc0 = {!!} -- Union of ZFChain UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) → ( (z : Ordinal) → z o< B → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → HOD @@ -331,32 +332,28 @@ ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → { y : Ordinal } → (ya : odef A y) → ZChain A ya f mf supO x ind f mf x prev {y} ay with Oprev-p x - ... | yes op with ODC.∋-p O A (* (Oprev.oprev op)) - ... | yes apx = zc4 where -- we have previous ordinal and A ∋ op + ... | yes op = zc4 where px = Oprev.oprev op - apx0 = subst (λ k → odef A k ) &iso apx zc0 : ZChain A ay f mf supO (Oprev.oprev op) zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay - zc1 : {y : Ordinal } → (ay : odef A y ) → ZChain A ay f mf supO (Oprev.oprev op) - zc1 {y} ay = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay - ay0 : odef A (& (* y)) - ay0 = (subst (λ k → odef A k ) (sym &iso) ay ) - Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x) - Afx {x} ax = (subst (λ k → odef A k ) (sym &iso) (proj2 (mf x (subst (λ k → odef A k ) &iso ax)))) - -- x is in the previous chain, use the same - -- x has some y which y < x ∧ f y ≡ x - -- x has no y which y < x zc4 : ZChain A ay f mf supO x - zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ay f ) + zc4 with ODC.∋-p O A (* x) + ... | no noax = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } where -- no extention + ... | yes ax with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ay f ) ... | case1 pr = zc7 where -- we have previous < + ay0 : odef A (& (* y)) + ay0 = (subst (λ k → odef A k ) (sym &iso) ay ) + Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x) + Afx {x} ax = (subst (λ k → odef A k ) (sym &iso) (proj2 (mf x (subst (λ k → odef A k ) &iso ax)))) chain = ZChain.chain zc0 zc7 : ZChain A ay f mf supO x - zc7 with ODC.∋-p O (ZChain.chain zc0) (* ( f x ) ) + zc7 with ODC.∋-p O (ZChain.chain zc0) (* ( f y ) ) ... | yes pr = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 - ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = {!!} -- ZChain.chain∋x zc0 + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = z22 ; is-max = {!!} } where -- no extention - z22 : {a : Ordinal} → x o< osuc a → ¬ odef (ZChain.chain zc0) a - z22 {a} x<oa = {!!} + z22 : odef (ZChain.chain zc0) y -- y ≡ f pr , chain ∋ f y ≡ f (f pr) + z22 = {!!} zc20 : {P : Ordinal → Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a) → {a : Ordinal} → (za : odef (ZChain.chain zc0) a ) → (a<x : a o< x) → P a zc20 {P} prev {a} za a<x with trio< a px