Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/BAlgebra.agda @ 1240:fbe072447243
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Mar 2023 13:02:09 +0900 |
parents | 0727cf865ebd |
children | 5f1572d1f19a |
rev | line source |
---|---|
431 | 1 open import Level |
2 open import Ordinals | |
1124 | 3 module BAlgebra {n : Level } (O : Ordinals {n}) where |
431 | 4 |
5 open import zf | |
6 open import logic | |
7 import OrdUtil | |
8 import OD | |
9 import ODUtil | |
10 import ODC | |
11 | |
12 open import Relation.Nullary | |
13 open import Relation.Binary | |
14 open import Data.Empty | |
15 open import Relation.Binary | |
16 open import Relation.Binary.Core | |
17 open import Relation.Binary.PropositionalEquality | |
18 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ ) | |
19 | |
20 open inOrdinal O | |
21 open Ordinals.Ordinals O | |
22 open Ordinals.IsOrdinals isOrdinal | |
23 open Ordinals.IsNext isNext | |
24 open OrdUtil O | |
25 open ODUtil O | |
26 | |
27 open OD O | |
28 open OD.OD | |
29 open ODAxiom odAxiom | |
30 open HOD | |
31 | |
32 open _∧_ | |
33 open _∨_ | |
34 open Bool | |
35 | |
1123 | 36 L\L=0 : { L : HOD } → L \ L ≡ od∅ |
37 L\L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← = lem1 } ) where | |
38 lem0 : {x : Ordinal} → odef (L \ L) x → odef od∅ x | |
39 lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx) | |
40 lem1 : {x : Ordinal} → odef od∅ x → odef (L \ L) x | |
41 lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | |
42 | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
43 L\Lx=x : { L x : HOD } → x ⊆ L → L \ ( L \ x ) ≡ x |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
44 L\Lx=x {L} {x} x⊆L = ==→o≡ ( record { eq→ = lem03 ; eq← = lem04 } ) where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
45 lem03 : {z : Ordinal} → odef (L \ (L \ x)) z → odef x z |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
46 lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O x (* z) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
47 ... | yes y = subst (λ k → odef x k ) &iso y |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
48 ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ ) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
49 lem04 : {z : Ordinal} → odef x z → odef (L \ (L \ x)) z |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
50 lem04 {z} xz with ODC.∋-p O L (* z) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
51 ... | yes y = ⟪ subst (λ k → odef L k ) &iso y , ( λ p → proj2 p xz ) ⟫ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
52 ... | no n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) )) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
53 |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
54 L\0=L : { L : HOD } → L \ od∅ ≡ L |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
55 L\0=L {L} = ==→o≡ ( record { eq→ = lem05 ; eq← = lem06 } ) where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
56 lem05 : {x : Ordinal} → odef (L \ od∅) x → odef L x |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
57 lem05 {x} ⟪ Lx , _ ⟫ = Lx |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
58 lem06 : {x : Ordinal} → odef L x → odef (L \ od∅) x |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
59 lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt) ⟫ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
60 |
1182 | 61 ∨L\X : { L X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L \ X) x |
62 ∨L\X {L} {X} {x} Lx with ODC.∋-p O X (* x) | |
63 ... | yes y = case1 ( subst (λ k → odef X k ) &iso y ) | |
64 ... | no n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫ | |
65 | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
66 |
451 | 67 [a-b]∩b=0 : { A B : HOD } → (A \ B) ∩ B ≡ od∅ |
68 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | |
69 ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } | |
70 | |
480 | 71 U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U |
1096 | 72 U-F=∅→F⊆U {F} {U} not = gt02 where |
480 | 73 gt02 : { x : Ordinal } → odef F x → odef U x |
74 gt02 {x} fx with ODC.∋-p O U (* x) | |
75 ... | yes y = subst (λ k → odef U k ) &iso y | |
76 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) | |
77 | |
431 | 78 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) |
79 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
80 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x | |
1096 | 81 lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo ) |
82 ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin | |
83 * owner ≡⟨ cong (*) (sym a=o) ⟩ | |
84 * (& A) ≡⟨ *iso ⟩ | |
85 A ∎ ) ox ) where open ≡-Reasoning | |
86 ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) *iso ) ox) | |
431 | 87 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x |
88 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A | |
89 ⟪ case1 refl , d→∋ A A∋x ⟫ ) | |
90 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B | |
91 ⟪ case2 refl , d→∋ B B∋x ⟫ ) | |
92 | |
93 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) | |
94 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
95 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x | |
96 lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫ | |
97 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x | |
98 lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫ | |
99 | |
100 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) | |
101 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
102 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x | |
103 lemma1 {x} lt with proj2 lt | |
104 lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ | |
105 lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ | |
106 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x | |
107 lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ | |
108 lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ | |
109 | |
110 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) | |
111 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | |
112 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x | |
113 lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫ | |
114 lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫ | |
115 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x | |
116 lemma2 {x} lt with proj1 lt | proj2 lt | |
117 lemma2 {x} lt | case1 cp | _ = case1 cp | |
118 lemma2 {x} lt | _ | case1 cp = case1 cp | |
119 lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ | |
120 | |
121 record IsBooleanAlgebra ( L : Set n) | |
122 ( b1 : L ) | |
123 ( b0 : L ) | |
124 ( -_ : L → L ) | |
125 ( _+_ : L → L → L ) | |
126 ( _x_ : L → L → L ) : Set (suc n) where | |
127 field | |
128 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c | |
129 x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c | |
130 +-sym : {a b : L } → a + b ≡ b + a | |
131 -sym : {a b : L } → a x b ≡ b x a | |
132 +-aab : {a b : L } → a + ( a x b ) ≡ a | |
133 x-aab : {a b : L } → a x ( a + b ) ≡ a | |
134 +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c ) | |
135 x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c ) | |
136 a+0 : {a : L } → a + b0 ≡ a | |
137 ax1 : {a : L } → a x b1 ≡ a | |
138 a+-a1 : {a : L } → a + ( - a ) ≡ b1 | |
139 ax-a0 : {a : L } → a x ( - a ) ≡ b0 | |
140 | |
141 record BooleanAlgebra ( L : Set n) : Set (suc n) where | |
142 field | |
143 b1 : L | |
144 b0 : L | |
145 -_ : L → L | |
146 _+_ : L → L → L | |
147 _x_ : L → L → L | |
148 isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_ | |
149 |