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

changeset 865:b095c84310df

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 Sat, 10 Sep 2022 18:20:24 +0900
parents 06f692bf7a97
children 8a49ab1dcbd0
files src/zorn.agda
diffstat 1 files changed, 29 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Sep 10 02:35:23 2022 +0900
+++ b/src/zorn.agda	Sat Sep 10 18:20:24 2022 +0900
@@ -351,6 +351,14 @@
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
+record Zsupf ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+        {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      s : Ordinal
+      s=z : odef A z → s ≡ z
+      as : odef A s
+      sup : SUP A (UnionCF A f mf ay (λ _ → s) z)
+
 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
    field
@@ -360,12 +368,12 @@
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
    field
-      supf-max : {x : Ordinal } → z o≤ x  → supf z ≡ supf x
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
       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) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
+      supf-max : {x : Ordinal } → z o< x  → supf (osuc z) ≡ supf x
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
 
    chain∋init : odef chain y
@@ -741,13 +749,13 @@
           supfx {z} x≤z with trio< z px
           ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
           ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
-          ... | tri> ¬a ¬b c = ZChain.supf-max zc (o<→≤ c)
+          ... | tri> ¬a ¬b c = ? --  ZChain.supf-max zc (o<→≤ c)
 
           supf∈A : {b : Ordinal} → b o≤ x → odef A (supf0 b)
           supf∈A {b} b≤z with trio< b px
           ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a ))
           ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b ))
-          ... | tri> ¬a ¬b c = subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) (proj1 ( ZChain.csupf zc o≤-refl))
+          ... | tri> ¬a ¬b c = ? -- subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) ? -- (proj1 ( ZChain.csupf zc o≤-refl))
 
           supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b 
           supf-mono = ZChain.supf-mono zc
@@ -755,9 +763,9 @@
           supf-max : {z : Ordinal} → x o≤ z → supf0 x ≡ supf0 z
           supf-max {z} z≤x = trans ( sym zc02) zc01 where
               zc02 : supf0 px ≡ supf0 x
-              zc02 = ZChain.supf-max zc (o<→≤ (pxo<x op))
+              zc02 = ? -- ZChain.supf-max zc (o<→≤ (pxo<x op))
               zc01 : supf0 px ≡ supf0 z
-              zc01 = ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x)
+              zc01 = ? -- ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x)
           zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
           zc04 {b} b≤x with trio< b px 
           ... | tri< a ¬b ¬c = case1 (o<→≤ a)
@@ -774,7 +782,7 @@
           --           supf0 px ≡ supf0 x 
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-          no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max
+          no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = ?
               ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf }  where
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
@@ -842,22 +850,27 @@
                  sup {z} z≤x with trio< z px 
                  ... | tri< a ¬b ¬c = record { tsup = ZChain.sup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-sup zc (o<→≤ a) }
                  ... | tri≈ ¬a b ¬c = record { tsup = ZChain.sup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-sup zc (o≤-refl0 b) }
-                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 } ; tsup=sup = zc33  } where
-                     zc32 = ZChain.sup zc o≤-refl 
+                 ... | tri> ¬a ¬b px<z = zc35 where
                      zc30 : z ≡ x
                      zc30 with osuc-≡< z≤x
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
-                     zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt) 
+                     zc32 = ZChain.sup zc o≤-refl 
+                     zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
+                     zc34 ne {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt) 
                      ... | case1 lt = SUP.x<sup zc32 lt 
-                     ... | case2 P = ?
-                     --  FClosure A f px z
-                     -- where
-                     --    zc35 : odef (UnionCF A f mf ay supf0 x) (& w)
-                     --     zc35 = 
+                     ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
+                     zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
+                     zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  } 
+                     zc35 : STMP z≤x
+                     zc35 with trio< (supf0 px) px
+                     ... | tri< a ¬b ¬c = zc36 ¬b
+                     ... | tri> ¬a ¬b c = zc36 ¬b
+                     ... | tri≈ ¬a b ¬c = record { tsup = zc37 ; tsup=sup = ?  } where
+                          zc37 : SUP A (UnionCF A f mf ay supf0 z)
+                          zc37 = record { sup = ? ; as = ? ; x<sup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
@@ -880,7 +893,7 @@
                                 ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } ) 
                  csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b)
                  csupf {b} b≤x with zc04 b≤x 
-                 ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) (ZChain.supf-max zc zc05 ) ( ZChain.csupf zc o≤-refl ) where
+                 ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) ? ( ZChain.csupf zc o≤-refl ) where
                      zc05 : px o≤ b
                      zc05 = subst (λ k → px o≤ k) (sym b=x) (o<→≤ (pxo<x op) )
                  ... | case1 b≤px = ZChain.csupf zc b≤px