# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1592129498 -32400
# Node ID 4340ffcfa83d2e77957090e082c011f73c6c332f
# Parent  9972bd4a0d6ffb3017ee4b5db03d3327a05cb4e9
ultra-filter P  → prime-filter P done

diff -r 9972bd4a0d6f -r 4340ffcfa83d filter.agda
--- a/filter.agda	Sun Jun 14 08:57:14 2020 +0900
+++ b/filter.agda	Sun Jun 14 19:11:38 2020 +0900
@@ -22,6 +22,8 @@
 open OD.OD
 open ODAxiom odAxiom
 
+import ODC
+
 open _∧_
 open _∨_
 open Bool
@@ -41,16 +43,60 @@
 proper-filter {L} P {p} = ¬ (filter P ∋ od∅)
 
 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 )
+prime-filter {L} P {p} {q} =  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+
+open _⊆_
+
+trans-⊆ :  { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C
+trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
+
+power→⊆ :  ( A t : OD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
+   t1 : {x : OD }  → t ∋ x → ¬ ¬ (A ∋ x)
+   t1 = zf.IsZF.power→ isZF A t PA∋t
 
-ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set (suc n )
-ultra-filter {L} P {p} = p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
+∈-filter : {L p : OD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
+∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
+
+∪-lemma1 : {L p q : OD } → (p ∪ q)  ⊆ L → p ⊆ L
+∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
+
+∪-lemma2 : {L p q : OD } → (p ∪ q)  ⊆ L → q ⊆ L
+∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
+
+q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q 
+q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
-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 lt
-... | t = {!!}
+-- is-∅ : ( x : OD ) → Dec ( x ≡ od∅  )
+-- is-∅ x with is-o∅ (od→ord x)
+-- ... | yes eq = yes {!!}
+-- ... | no ne = no {!!}
+
+record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       ultra   : {p : OD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
 
-filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p} 
+filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ultra-filter P  → prime-filter {L} P {p} {q}
+filter-lemma1 {L} P {p} {q} u lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
+... | case1 p∈P  = case1 p∈P
+... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
+    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) ==  (q ∩ (L ＼ p))
+    lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt  }
+       ;  eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
+      } where
+         lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L ＼ p)) x → def q x
+         lemma4 x lt with proj1 lt
+         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
+         lemma4 x lt | case2 qx = qx
+    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
+    lemma6 = filter2 P lt ¬p∈P
+    lemma7 : filter P ∋ (q ∩ (L ＼ p))
+    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
+    lemma8 : (q ∩ (L ＼ p)) ⊆ q
+    lemma8 = q∩q⊆q
+
+filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter P
 filter-lemma2 {L} P prime p = {!!}
 
 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )