Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 269:30e419a2be24
disjunction and conjunction
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 06 Oct 2019 16:42:42 +0900 |
parents | 7b4a66710cdd |
children | fc3d4bc1dc5e |
comparison
equal
deleted
inserted
replaced
268:7b4a66710cdd | 269:30e419a2be24 |
---|---|
24 | 24 |
25 _∩_ : ( A B : OD ) → OD | 25 _∩_ : ( A B : OD ) → OD |
26 A ∩ B = record { def = λ x → def A x ∧ def B x } | 26 A ∩ B = record { def = λ x → def A x ∧ def B x } |
27 | 27 |
28 _∪_ : ( A B : OD ) → OD | 28 _∪_ : ( A B : OD ) → OD |
29 A ∪ B = Union (A , B) | 29 A ∪ B = record { def = λ x → def A x ∨ def B x } |
30 | |
31 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) | |
32 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
33 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x | |
34 lemma1 {x} lt = lemma3 lt where | |
35 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) | |
36 lemma4 {y} z with proj1 z | |
37 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) | |
38 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) | |
39 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x | |
40 lemma3 not = double-neg-eilm (FExists _ lemma4 not) | |
41 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x | |
42 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A | |
43 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) | |
44 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B | |
45 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) | |
46 | |
47 ∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) | |
48 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
49 lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x | |
50 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } | |
51 lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x | |
52 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = | |
53 record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } | |
54 | |
55 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) | |
56 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
57 lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x | |
58 lemma1 {x} lt with proj2 lt | |
59 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) | |
60 lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } ) | |
61 lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x | |
62 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } | |
63 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } | |
64 | |
65 dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) | |
66 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
67 lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x | |
68 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } | |
69 lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) } | |
70 lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x | |
71 lemma2 {x} lt with proj1 lt | proj2 lt | |
72 lemma2 {x} lt | case1 cp | _ = case1 cp | |
73 lemma2 {x} lt | _ | case1 cp = case1 cp | |
74 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } ) | |
30 | 75 |
31 record Filter ( L : OD ) : Set (suc n) where | 76 record Filter ( L : OD ) : Set (suc n) where |
32 field | 77 field |
33 F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ q p {x} ) → L ∋ q | 78 F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ p q {x} ) → L ∋ q |
34 F2 : { p q : OD } → L ∋ p → L ∋ q → L ∋ (p ∩ q) | 79 F2 : { p q : OD } → L ∋ p → L ∋ q → L ∋ (p ∩ q) |
35 | 80 |
36 open Filter | 81 open Filter |
37 | 82 |
38 proper-filter : {L : OD} → Filter L → Set n | 83 proper-filter : {L : OD} → Filter L → Set n |
42 prime-filter {L} P {p} {q} = L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q ) | 87 prime-filter {L} P {p} {q} = L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q ) |
43 | 88 |
44 ultra-filter : {L : OD} → Filter L → {p : OD } → Set n | 89 ultra-filter : {L : OD} → Filter L → {p : OD } → Set n |
45 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p )) | 90 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p )) |
46 | 91 |
47 postulate | |
48 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) | |
49 | 92 |
50 filter-lemma1 : {L : OD} → (P : Filter L) → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} | 93 filter-lemma1 : {L : OD} → (P : Filter L) → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} |
51 filter-lemma1 {L} P {p} {q} u lt with u p | u q | 94 filter-lemma1 {L} P {p} {q} u lt with u p | u q |
52 filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x | 95 filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x |
53 filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x | 96 filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x |
59 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) | 102 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) |
60 generated-filter {L} P p = record { | 103 generated-filter {L} P p = record { |
61 F1 = {!!} ; F2 = {!!} | 104 F1 = {!!} ; F2 = {!!} |
62 } | 105 } |
63 | 106 |
107 record Dense (P : OD ) : Set (suc n) where | |
108 field | |
109 dense : OD | |
110 incl : { x : OD} → _⊆_ dense P {x} | |
111 dense-f : OD → OD | |
112 dense-p : { p x : OD} → P ∋ p → _⊆_ p (dense-f p) {x} | |
113 | |
64 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) | 114 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) |
65 | 115 |
66 infinite = ZF.infinite OD→ZF | 116 infinite = ZF.infinite OD→ZF |
67 | 117 |
68 Hω2 : Filter (Power (Power infinite)) | 118 module in-countable-ordinal {n : Level} where |
69 Hω2 = record { F1 = {!!} ; F2 = {!!} } | |
70 | 119 |
120 import ordinal | |
121 | |
122 open ordinal.C-Ordinal-with-choice | |
123 | |
124 Hω2 : Filter (Power (Power infinite)) | |
125 Hω2 = record { F1 = {!!} ; F2 = {!!} } | |
126 |