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

changeset 739:f92c675c3ef0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 19 Jul 2022 18:35:38 +0900
parents ffd3bb1a43fe
children 11f46927e3f7
files src/zorn.agda
diffstat 1 files changed, 9 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 19 17:57:26 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 18:35:38 2022 +0900
@@ -265,6 +265,7 @@
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u
+      csupz    : FClosure A f (supf u) z 
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
 
       -- u>0      : o∅ o< u    -- ¬ ch-init
@@ -274,7 +275,6 @@
       -- au       : odef A u
       -- ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
       -- asup     : (x : Ordinal) → odef A (supf x)
-      -- csupz    : FClosure A f (supf u) z 
 
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
@@ -493,7 +493,7 @@
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = {!!}   -- b = px case
+                 ... | tri≈ ¬a b=px ¬c = ? -- b = px case
         ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x  }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -503,8 +503,10 @@
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x ? o≤-refl m04 where
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u ? ab is-sup)   -- ZChain on x
+                 m06 : ChainP A f mf ay (ZChain.supf zc) b b
+                 m06 = record { fcy<sup = ? ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = ? }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup ? (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
+                 m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -646,16 +648,6 @@
                ; initial = pinit ; chain∋init = pcy  ; sup=u = ? 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
-          chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
-          chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = zc11 ; uchain = UChain.uchain (proj2 za)  }  ⟫ where
-              zc11 : (UChain.u (proj2 za) o< x) ∨ (UChain.u (proj2 za) ≡ o∅)
-              zc11 with UChain.u<x (proj2 za)
-              ... | case1 z<x = case1 (ordtrans z<x px<x )
-              ... | case2 z=0 = case2 z=0
-
-          chain-≡ : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) 
-             → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) 
-          chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 
           chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
           chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
@@ -678,7 +670,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  supf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
-                     ; initial = pinit ; chain∋init  = pcy } 
+                     ; initial = pinit ; chain∋init  = pcy ; sup=u = ? } 
           ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
      ... | no lim = zc5 where
 
@@ -727,7 +719,7 @@
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; sup=u = ?}
 
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal
@@ -745,8 +737,8 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  
-              ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?) 
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = ?
+              ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z