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

changeset 267:e469de3ae7cc

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, 30 Sep 2019 20:59:45 +0900
parents 0d7d6e4da36f
children 7b4a66710cdd
files filter.agda
diffstat 1 files changed, 17 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/filter.agda	Mon Sep 30 17:07:40 2019 +0900
+++ b/filter.agda	Mon Sep 30 20:59:45 2019 +0900
@@ -22,36 +22,39 @@
 open _∨_
 open Bool
 
+_∩_ : ( A B : OD  ) → OD
+A ∩ B = record { def = λ x → def A x ∧ def B x } 
+
+_∪_ : ( A B : OD  ) → OD
+A ∪ B = Union (A , B)    
+
 record Filter  ( L : OD  ) : Set (suc n) where
    field
-       F1 : { p q : Ordinal } → def L p →  p o< osuc q  → def L q
-       F2 : { p q : Ordinal } → def L p →  def L q  → def L (minα p q)
+       F1 : { p q : OD } → L ∋ p →  ({ x : OD} → _⊆_ p q {x} ) → L ∋ q
+       F2 : { p q : OD } → L ∋ p →  L ∋ q  → L ∋ (p ∩ q)
 
 open Filter
 
 proper-filter : {L : OD} → Filter L → Set n
-proper-filter {L} P = ¬ ( def L o∅ )
+proper-filter {L} P = ¬ ( L ∋ od∅ )
 
-prime-filter : {L : OD} → Filter L → {p q : Ordinal } → Set n
-prime-filter {L} P {p} {q} =  def L ( maxα p q) → ( def L p ) ∨ ( def L q )
+prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
+prime-filter {L} P {p} {q} =  L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q )
 
-ultra-filter :  {L : OD} → Filter L → {p : Ordinal } → Set n 
-ultra-filter {L} P {p} = ( def L p ) ∨ ( ¬ ( def L p ))
+ultra-filter :  {L : OD} → Filter L → {p : OD } → Set n 
+ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
 
 postulate
-   dist-ord : {p q r : Ordinal } → minα p ( maxα q r ) ≡ maxα  ( minα p q ) ( minα p r )
+   dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 
-filter-lemma1 :  {L : OD} → (P : Filter L)  → {p q : Ordinal } → ( (p : Ordinal ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
+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 with trio< p q
-filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y | tri< a ¬b ¬c =  ⊥-elim ( y lt )
-filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y | tri≈ ¬a refl ¬c = ⊥-elim ( y lt )
-filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y | tri> ¬a ¬b c = ⊥-elim ( x lt )
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim ( y ? )
 
-generated-filter : {L : OD} → Filter L → (p : Ordinal ) → Filter ( record { def = λ x → def L x ∨ (x ≡ p) } )
+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 = {!!}
    }