6 |
6 |
7 theory Boolean_Algebra |
7 theory Boolean_Algebra |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 locale boolean = |
11 locale boolean_algebra = |
12 fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) |
12 fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) |
13 and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) |
13 and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) |
14 and compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80) |
14 and compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80) |
15 and zero :: "'a" ("\<zero>") |
15 and zero :: "'a" ("\<zero>") |
16 and one :: "'a" ("\<one>") |
16 and one :: "'a" ("\<one>") |
36 lemmas disj_left_commute = disj.left_commute |
36 lemmas disj_left_commute = disj.left_commute |
37 |
37 |
38 lemmas conj_ac = conj.assoc conj.commute conj.left_commute |
38 lemmas conj_ac = conj.assoc conj.commute conj.left_commute |
39 lemmas disj_ac = disj.assoc disj.commute disj.left_commute |
39 lemmas disj_ac = disj.assoc disj.commute disj.left_commute |
40 |
40 |
41 lemma dual: "boolean disj conj compl one zero" |
41 lemma dual: "boolean_algebra disj conj compl one zero" |
42 apply (rule boolean.intro) |
42 apply (rule boolean_algebra.intro) |
43 apply (rule disj_assoc) |
43 apply (rule disj_assoc) |
44 apply (rule conj_assoc) |
44 apply (rule conj_assoc) |
45 apply (rule disj_commute) |
45 apply (rule disj_commute) |
46 apply (rule conj_commute) |
46 apply (rule conj_commute) |
47 apply (rule disj_conj_distrib) |
47 apply (rule disj_conj_distrib) |
141 |
141 |
142 |
142 |
143 subsection \<open>Disjunction\<close> |
143 subsection \<open>Disjunction\<close> |
144 |
144 |
145 lemma disj_absorb [simp]: "x \<squnion> x = x" |
145 lemma disj_absorb [simp]: "x \<squnion> x = x" |
146 by (rule boolean.conj_absorb [OF dual]) |
146 by (rule boolean_algebra.conj_absorb [OF dual]) |
147 |
147 |
148 lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>" |
148 lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>" |
149 by (rule boolean.conj_zero_right [OF dual]) |
149 by (rule boolean_algebra.conj_zero_right [OF dual]) |
150 |
150 |
151 lemma compl_zero [simp]: "\<sim> \<zero> = \<one>" |
151 lemma compl_zero [simp]: "\<sim> \<zero> = \<one>" |
152 by (rule boolean.compl_one [OF dual]) |
152 by (rule boolean_algebra.compl_one [OF dual]) |
153 |
153 |
154 lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x" |
154 lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x" |
155 by (rule boolean.conj_one_left [OF dual]) |
155 by (rule boolean_algebra.conj_one_left [OF dual]) |
156 |
156 |
157 lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>" |
157 lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>" |
158 by (rule boolean.conj_zero_left [OF dual]) |
158 by (rule boolean_algebra.conj_zero_left [OF dual]) |
159 |
159 |
160 lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>" |
160 lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>" |
161 by (rule boolean.conj_cancel_left [OF dual]) |
161 by (rule boolean_algebra.conj_cancel_left [OF dual]) |
162 |
162 |
163 lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
163 lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
164 by (rule boolean.conj_left_absorb [OF dual]) |
164 by (rule boolean_algebra.conj_left_absorb [OF dual]) |
165 |
165 |
166 lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
166 lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
167 by (rule boolean.conj_disj_distrib2 [OF dual]) |
167 by (rule boolean_algebra.conj_disj_distrib2 [OF dual]) |
168 |
168 |
169 lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2 |
169 lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2 |
170 |
170 |
171 |
171 |
172 subsection \<open>De Morgan's Laws\<close> |
172 subsection \<open>De Morgan's Laws\<close> |
187 finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>" |
187 finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>" |
188 by (simp only: disj_cancel_right disj_one_right conj_one_right) |
188 by (simp only: disj_cancel_right disj_one_right conj_one_right) |
189 qed |
189 qed |
190 |
190 |
191 lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y" |
191 lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y" |
192 by (rule boolean.de_Morgan_conj [OF dual]) |
192 by (rule boolean_algebra.de_Morgan_conj [OF dual]) |
193 |
193 |
194 end |
194 end |
195 |
195 |
196 |
196 |
197 subsection \<open>Symmetric Difference\<close> |
197 subsection \<open>Symmetric Difference\<close> |
198 |
198 |
199 locale boolean_xor = boolean + |
199 locale boolean_algebra_xor = boolean_algebra + |
200 fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<oplus>" 65) |
200 fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<oplus>" 65) |
201 assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)" |
201 assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)" |
202 begin |
202 begin |
203 |
203 |
204 sublocale xor: abel_semigroup xor |
204 sublocale xor: abel_semigroup xor |