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

changeset 97:f2b579106770

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
power set using sup on Def
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Jun 2019 19:41:53 +0900
parents f239ffc27fd0
children 1ff0ddc991ac
files ordinal-definable.agda ordinal.agda
diffstat 2 files changed, 39 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Sat Jun 08 22:17:40 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 09 19:41:53 2019 +0900
@@ -248,19 +248,23 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
+csuc :  {n : Level} →  OD {suc n} → OD {suc n}
+csuc x = ord→od ( osuc ( od→ord x ))
+
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
-Def :  {n : Level} →  OD {suc n} → OD {suc n}
-Def {n} A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  → def A x }
+
+ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
+ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
+
+Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
+Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 -- Constructible Set on α
-L : {n : Level} →  Ordinal {suc n} → OD {suc n}
-L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
-L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L ( record { lv = lx ; ord = ox } ))
-L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
-    record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) }
-
-csuc :  {n : Level} →  OD {suc n} → OD {suc n}
-csuc x = ord→od ( osuc ( od→ord x ))
+L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
+L {n}  record { lv = Zero ; ord = (Φ .0) } = od∅
+L {n}  record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 
+L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
+    record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) }
 
 -- L∋ord : {n : Level} → (x :  Ordinal {suc n} ) → L (osuc x) ∋ ord→od x
 -- L∋ord {n} record { lv = Zero ; ord = (Φ .0) } = {!!}
@@ -276,8 +280,9 @@
 supP : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n}
 supP A = sup-o ( ord-of A )
 
-L→P : {n : Level} → (A : OD {suc n} ) → L (supP A) ∋ Def A 
-L→P {n} A = {!!}
+L→P : {n : Level} → (A x : OD {suc n} ) → L {n}  (supP A) ∋ ZFSubset A x
+L→P {n} A x with sup-o< (ord-of A) {{!!}}
+... | lt = {!!}
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
@@ -303,7 +308,7 @@
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
     Power : OD {suc n} → OD {suc n}
-    Power A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  → def A x }
+    Power A = Def A
     ZFSet = OD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
@@ -320,7 +325,7 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union-u = union-u
+       ;   union-u = λ _ z _ → csuc z
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
@@ -341,14 +346,25 @@
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
-         --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  →  def X x }
+         --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
+         --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = P∋t (od→ord x) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x )
+         power→ A t P∋t {x} t∋x = proj1 lemma-s where
+              lemma-t : ZFSubset A {!!} ∋ csuc t
+              lemma-t = record { proj1 = {!!} ; proj2 = {!!} }
+              lemma-s : ZFSubset A {!!} ∋ x
+              lemma-s = {!!} -- transitive {!!} t∋x
+              lemma : od→ord (ZFSubset A (ord→od (od→ord (csuc t))) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
+              lemma = sup-o< {suc n} (  λ x → od→ord ( ZFSubset A (ord→od x ))) 
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A z _ = {!!}
-         union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
-         union-u X z U>z = ord→od ( osuc ( od→ord z ) )
-         union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
+         power← A t t→A  = {!!} where
+              lemma-eq :  ZFSubset A t == t
+              eq→ lemma-eq {z} w = proj2 w 
+              eq← lemma-eq {z} w = record { proj2 = w  ;
+                 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+              lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
+              lemma = sup-o< {suc n} (  λ x → od→ord ( ZFSubset A (ord→od x ))) 
+         union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
          union-lemma-u {X} {z} U>z = lemma <-osuc where
              lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
              lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl refl
@@ -360,8 +376,8 @@
              lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
              lemma refl lt = lt
          union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 
-         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
-         union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (union-u X z X∋z)} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
+         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z )
+         union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
--- a/ordinal.agda	Sat Jun 08 22:17:40 2019 +0900
+++ b/ordinal.agda	Sun Jun 09 19:41:53 2019 +0900
@@ -289,3 +289,4 @@
 TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv
 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
+