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

changeset 443:3681cac8d6a8

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 Wed, 09 Mar 2022 17:42:22 +0900
parents 3fbcd11c2a35
children 8c43e804581e
files src/OD.agda src/filter.agda src/generic-filter.agda
diffstat 3 files changed, 21 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/OD.agda	Fri Mar 04 19:04:08 2022 +0900
+++ b/src/OD.agda	Wed Mar 09 17:42:22 2022 +0900
@@ -96,9 +96,9 @@
   * : Ordinal  → HOD  
   c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
   ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
-  *iso   :  {x : HOD }      → * ( & x ) ≡ x
+  *iso   :  {x : HOD }      → * ( & x ) ≡ x            -- should be (* ( & x )) == x
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
-  ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
+  ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y   -- should be  & x ≡ & y
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 -- possible order restriction
@@ -217,6 +217,9 @@
 ∅6 : { x : HOD  }  → ¬ ( x ∋ x )    --  no Russel paradox
 ∅6  {x} x∋x = o<¬≡ refl ( c<→o<  {x} {x} x∋x )
 
+∅7 : {x : HOD} → o∅ o< & x → ¬ ( od x == od od∅ )
+∅7 {x} lt eq = ¬x<0 (subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) lt )
+
 odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y  → (odef A y → odef B y)  → odef A x → odef B x
 odef-iso refl t = t
 
--- a/src/filter.agda	Fri Mar 04 19:04:08 2022 +0900
+++ b/src/filter.agda	Wed Mar 09 17:42:22 2022 +0900
@@ -120,6 +120,16 @@
         lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
         lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
 
+-----
+--
+--  if Filter not contains L, there is a ultra filter
+--
+-- filter-lemma3 :  {L : HOD} → (P : Filter L)  → ¬ ( filter P ∋ L ) → ultra-filter P
+-- filter-lemma3 {L} P ¬f∋L = record {
+--          proper = {!!}
+--        ; ultra = {!!}
+--    } where
+
 record Dense  (P : HOD ) : Set (suc n) where
    field
        dense : HOD
--- a/src/generic-filter.agda	Fri Mar 04 19:04:08 2022 +0900
+++ b/src/generic-filter.agda	Wed Mar 09 17:42:22 2022 +0900
@@ -92,11 +92,13 @@
 ... | yes _ = B P C i x lt
 ... | no _  with is-o∅ ( & (BR.b (B P C i x lt) ∩ A i P C ) )
 ... | no ne =  record { b = BR.b (B P C i x lt ) ∩ A i P C  ; b>0 = ¬≡o∅< ne } 
-... | yes y = record { b = BR.b (B P C i x lt) ＼ (ODC.minimal O _ (b02 (b01 ? y ))) ; b>0 = {!!} } where
+... | yes y = record { b = BR.b (B P C i x lt) ＼ (ODC.minimal O b03 (b02 (b01 (BR.b>0 (B P C i x lt)) y ))) ; b>0 = {!!} } where
+    b03 : HOD 
+    b03 = BR.b (B P C i x lt) ＼ A i P C
     b02 : {x : HOD} → o∅ o< & x → ¬ ( x =h= od∅ )
-    b02 = {!!}
-    b01 : {an bn : HOD} → o∅ o< & bn  →  &( an ∩ bn ) ≡ o∅  → o∅ o< &( bn ＼ an )
-    b01 = {!!}
+    b02 = ∅7
+    b01 : {an bn : HOD} → o∅ o< & bn  →  &( bn ∩ an ) ≡ o∅  → o∅ o< &( bn ＼ an )
+    b01 {an} {bn} 0<b ba=0 = {!!}
        
 
 B⊆ : (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : HOD) →  (lt : o∅ o< & x) → BR.b (B P C (Suc i) x lt) ⊆  BR.b (B P C (Suc i) x lt)