# HG changeset patch # User Shinji KONO # 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) } )