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

changeset 270:fc3d4bc1dc5e

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 Mon, 07 Oct 2019 01:28:11 +0900
parents 30e419a2be24
children 2169d948159b
files filter.agda
diffstat 1 files changed, 54 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/filter.agda	Sun Oct 06 16:42:42 2019 +0900
+++ b/filter.agda	Mon Oct 07 01:28:11 2019 +0900
@@ -28,6 +28,9 @@
 _∪_ : ( A B : OD  ) → OD
 A ∪ B = record { def = λ x → def A x ∨ def B x } 
 
+_＼_ : ( A B : OD  ) → OD
+A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
+
 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
@@ -37,7 +40,7 @@
         lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
         lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
         lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
-        lemma3 not = double-neg-eilm (FExists _ lemma4 not) 
+        lemma3 not = double-neg-eilm (FExists _ lemma4 not)   -- choice
     lemma2 :  {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
        (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
@@ -73,35 +76,67 @@
     lemma2 {x} lt | _ | case1 cp = case1 cp 
     lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } )
 
+record IsBooleanAlgebra ( L : Set n)
+       ( b1 : L )
+       ( b0 : L )
+       ( -_ : L → L  )
+       ( _+_ : L → L → L )
+       ( _*_ : L → L → L ) : Set (suc n) where
+   field
+       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
+       *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
+       +-sym : {a b : L } → a + b ≡ b + a
+       -sym : {a b : L } → a * b  ≡ b * a
+       -aab : {a b : L } → a + ( a * b ) ≡ a
+       *-aab : {a b : L } → a * ( a + b ) ≡ a
+       -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
+       *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
+       a+0 : {a : L } → a + b0 ≡ a
+       a*1 : {a : L } → a * b1 ≡ a
+       a+-a1 : {a : L } → a + ( - a ) ≡ b1
+       a*-a0 : {a : L } → a * ( - a ) ≡ b0
+
+record BooleanAlgebra ( L : Set n) : Set (suc n) where
+   field
+       b1 : L
+       b0 : L
+       -_ : L → L 
+       _++_ : L → L → L
+       _**_ : L → L → L
+       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
+       
+
 record Filter  ( L : OD  ) : Set (suc n) where
    field
-       F1 : { p q : OD } → L ∋ p →  ({ x : OD} → _⊆_ p q {x} ) → L ∋ q
-       F2 : { p q : OD } → L ∋ p →  L ∋ q  → L ∋ (p ∩ q)
+       filter : OD
+       proper : ¬ ( filter ∋ od∅ )
+       inL : { x : OD} → _⊆_ filter L {x}
+       filter1 : { p q : OD } → ( {x : OD} → _⊆_ q L {x} ) → filter ∋ p →  ({ x : OD} → _⊆_ p q {x} ) → filter ∋ q
+       filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
 open Filter
 
-proper-filter : {L : OD} → Filter L → Set n
-proper-filter {L} P = ¬ ( L ∋ od∅ )
+L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
+L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!}
 
-prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
-prime-filter {L} P {p} {q} =  L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q )
+prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
+prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
 
-ultra-filter :  {L : OD} → Filter L → {p : OD } → Set n 
-ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
+ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set n 
+ultra-filter {L} P {p} = L ∋ p →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
 
 
-filter-lemma1 :  {L : OD} → (P : Filter L)  → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
-filter-lemma1 {L} P {p} {q} u lt with u p | u q
-filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x
-filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x
-filter-lemma1 {L} P {p} {q} u lt | case2 x | case1 y = case2 y
-filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim (lemma (record { proj1 = x ; proj2 = y })) where
-    lemma :  ¬ ( ¬ ( L ∋ p ) ) ∧ ( ¬ ( L ∋ q )) 
-    lemma = {!!}
+filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
+filter-lemma1 {L} P {p} {q} u lt = {!!}
+
+filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p} 
+filter-lemma2 {L} P prime p with prime {!!}
+... | t = {!!}
 
 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
 generated-filter {L} P p = record {
-     F1 = {!!} ; F2 = {!!}
+     filter = {!!}  ; inL = {!!} ; 
+     filter1 = {!!} ; filter2 = {!!}
    }
 
 record Dense  (P : OD ) : Set (suc n) where
@@ -122,5 +157,5 @@
    open  ordinal.C-Ordinal-with-choice 
 
    Hω2 : Filter (Power (Power infinite))
-   Hω2 = record { F1 = {!!} ; F2 = {!!} }
+   Hω2 = {!!}