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

changeset 228:49736efc822b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try transfinite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2019 20:42:48 +0900
parents a4cdfc84f65f
children 5e36744b8dce
files OD.agda cardinal.agda
diffstat 2 files changed, 10 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Sun Aug 11 18:37:33 2019 +0900
+++ b/OD.agda	Sun Aug 11 20:42:48 2019 +0900
@@ -483,3 +483,4 @@
 Select = ZF.Select OD→ZF
 Replace = ZF.Replace OD→ZF
 isZF = ZF.isZF  OD→ZF
+TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
--- a/cardinal.agda	Sun Aug 11 18:37:33 2019 +0900
+++ b/cardinal.agda	Sun Aug 11 20:42:48 2019 +0900
@@ -51,30 +51,10 @@
 -- contra position of sup-o<
 --
 
-record Sup ( ψ : Ordinal  →  Ordinal )  : Set n where
-   field
-        sup-x  : Ordinal 
-        sup-lb : {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ sup-x )
-
-sup-o> : ( ψ : Ordinal  →  Ordinal )  → Sup ψ
-sup-o> ψ = record {
-        sup-x = od→ord ( minimul (Ord (osuc (sup-o ψ))) lemma )
-      ; sup-lb = λ {z} z<sψ → lemma1 z<sψ
-   } where
-       lemma0 : {x : Ordinal} → o∅ o< osuc x
-       lemma0 {x} with trio< o∅ (osuc x)
-       lemma0 {x} | tri< a ¬b ¬c = a
-       lemma0 {x} | tri≈ ¬a refl ¬c = ⊥-elim (¬x<0 <-osuc )
-       lemma0 {x} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
-       lemma : ¬ (Ord (osuc (sup-o ψ)) == od∅)
-       lemma record { eq→ = eq→ ; eq← = eq← } = ¬x<0 {o∅} ( eq→  lemma0 )
-       lemma1 :  {z : Ordinal} → z o< sup-o ψ → z o< osuc (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma)))
-       lemma1 {z} lt with trio< z (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma)))
-       lemma1 {z} lt | tri< a ¬b ¬c = ordtrans a <-osuc
-       lemma1 {z} lt | tri≈ ¬a refl ¬c = <-osuc
-       lemma1 {z} lt | tri> ¬a ¬b c = ⊥-elim (o<> c lemma2 ) where
-           lemma2 :  z o< ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma))
-           lemma2 = ordtrans sup-o< ( o<-subst (x∋minimul (Ord (osuc (sup-o ψ))) lemma ) ? ?)
+postulate
+  -- contra-position of mimimulity of supermum required in Cardinal
+  sup-x  : ( Ordinal  → Ordinal ) →  Ordinal 
+  sup-lb : { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
 
 ------------
 --
@@ -107,8 +87,12 @@
     cardinal-p x with p∨¬p ( Onto (Ord x) X ) 
     cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
+    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc (sup-o (λ x₁ → proj1 (cardinal-p x₁)))) → Onto (Ord y) X)) →
+                    Lift (suc n) (x o< (osuc  (sup-o (λ x₁ → proj1 (cardinal-p x₁)))) → Onto (Ord x) X)
+    lemma1 = {!!}
     onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X
-    onto = {!!}
+    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc (sup-o (λ x → proj1 (cardinal-p x))) → Onto (Ord x) X ) } lemma1 (sup-o (λ x → proj1 (cardinal-p x))) 
+    ... | lift t = t <-osuc  where
     cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X
     cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
        (sup-o<  {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where