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 = |
12 fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) |
12 fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) |
13 fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) |
13 and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) |
14 fixes compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80) |
14 and compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80) |
15 fixes zero :: "'a" ("\<zero>") |
15 and zero :: "'a" ("\<zero>") |
16 fixes one :: "'a" ("\<one>") |
16 and one :: "'a" ("\<one>") |
17 assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
17 assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
18 assumes disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
18 and disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
19 assumes conj_commute: "x \<sqinter> y = y \<sqinter> x" |
19 and conj_commute: "x \<sqinter> y = y \<sqinter> x" |
20 assumes disj_commute: "x \<squnion> y = y \<squnion> x" |
20 and disj_commute: "x \<squnion> y = y \<squnion> x" |
21 assumes conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
21 and conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
22 assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
22 and disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
23 assumes conj_one_right [simp]: "x \<sqinter> \<one> = x" |
23 and conj_one_right [simp]: "x \<sqinter> \<one> = x" |
24 assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x" |
24 and disj_zero_right [simp]: "x \<squnion> \<zero> = x" |
25 assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>" |
25 and conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>" |
26 assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>" |
26 and disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>" |
27 begin |
27 begin |
28 |
28 |
29 sublocale conj: abel_semigroup conj |
29 sublocale conj: abel_semigroup conj |
30 by standard (fact conj_assoc conj_commute)+ |
30 by standard (fact conj_assoc conj_commute)+ |
31 |
31 |
32 sublocale disj: abel_semigroup disj |
32 sublocale disj: abel_semigroup disj |
33 by standard (fact disj_assoc disj_commute)+ |
33 by standard (fact disj_assoc disj_commute)+ |
34 |
34 |
35 lemmas conj_left_commute = conj.left_commute |
35 lemmas conj_left_commute = conj.left_commute |
36 |
|
37 lemmas disj_left_commute = disj.left_commute |
36 lemmas disj_left_commute = disj.left_commute |
38 |
37 |
39 lemmas conj_ac = conj.assoc conj.commute conj.left_commute |
38 lemmas conj_ac = conj.assoc conj.commute conj.left_commute |
40 lemmas disj_ac = disj.assoc disj.commute disj.left_commute |
39 lemmas disj_ac = disj.assoc disj.commute disj.left_commute |
41 |
40 |
42 lemma dual: "boolean disj conj compl one zero" |
41 lemma dual: "boolean disj conj compl one zero" |
43 apply (rule boolean.intro) |
42 apply (rule boolean.intro) |
44 apply (rule disj_assoc) |
43 apply (rule disj_assoc) |
45 apply (rule conj_assoc) |
44 apply (rule conj_assoc) |
46 apply (rule disj_commute) |
45 apply (rule disj_commute) |
47 apply (rule conj_commute) |
46 apply (rule conj_commute) |
48 apply (rule disj_conj_distrib) |
47 apply (rule disj_conj_distrib) |
49 apply (rule conj_disj_distrib) |
48 apply (rule conj_disj_distrib) |
50 apply (rule disj_zero_right) |
49 apply (rule disj_zero_right) |
51 apply (rule conj_one_right) |
50 apply (rule conj_one_right) |
52 apply (rule disj_cancel_right) |
51 apply (rule disj_cancel_right) |
53 apply (rule conj_cancel_right) |
52 apply (rule conj_cancel_right) |
54 done |
53 done |
55 |
54 |
56 |
55 |
57 subsection \<open>Complement\<close> |
56 subsection \<open>Complement\<close> |
61 assumes 2: "a \<squnion> x = \<one>" |
60 assumes 2: "a \<squnion> x = \<one>" |
62 assumes 3: "a \<sqinter> y = \<zero>" |
61 assumes 3: "a \<sqinter> y = \<zero>" |
63 assumes 4: "a \<squnion> y = \<one>" |
62 assumes 4: "a \<squnion> y = \<one>" |
64 shows "x = y" |
63 shows "x = y" |
65 proof - |
64 proof - |
66 have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)" |
65 from 1 3 have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)" |
67 using 1 3 by simp |
66 by simp |
68 then have "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)" |
67 then have "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)" |
69 using conj_commute by simp |
68 by (simp add: conj_commute) |
70 then have "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)" |
69 then have "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)" |
71 using conj_disj_distrib by simp |
70 by (simp add: conj_disj_distrib) |
72 then have "x \<sqinter> \<one> = y \<sqinter> \<one>" |
71 with 2 4 have "x \<sqinter> \<one> = y \<sqinter> \<one>" |
73 using 2 4 by simp |
72 by simp |
74 then show "x = y" |
73 then show "x = y" |
75 using conj_one_right by simp |
74 by simp |
76 qed |
75 qed |
77 |
76 |
78 lemma compl_unique: "x \<sqinter> y = \<zero> \<Longrightarrow> x \<squnion> y = \<one> \<Longrightarrow> \<sim> x = y" |
77 lemma compl_unique: "x \<sqinter> y = \<zero> \<Longrightarrow> x \<squnion> y = \<one> \<Longrightarrow> \<sim> x = y" |
79 by (rule complement_unique [OF conj_cancel_right disj_cancel_right]) |
78 by (rule complement_unique [OF conj_cancel_right disj_cancel_right]) |
80 |
79 |
81 lemma double_compl [simp]: "\<sim> (\<sim> x) = x" |
80 lemma double_compl [simp]: "\<sim> (\<sim> x) = x" |
82 proof (rule compl_unique) |
81 proof (rule compl_unique) |
83 from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>" |
82 show "\<sim> x \<sqinter> x = \<zero>" |
84 by (simp only: conj_commute) |
83 by (simp only: conj_cancel_right conj_commute) |
85 from disj_cancel_right show "\<sim> x \<squnion> x = \<one>" |
84 show "\<sim> x \<squnion> x = \<one>" |
86 by (simp only: disj_commute) |
85 by (simp only: disj_cancel_right disj_commute) |
87 qed |
86 qed |
88 |
87 |
89 lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y" |
88 lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y" |
90 by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl) |
89 by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl) |
91 |
90 |
93 subsection \<open>Conjunction\<close> |
92 subsection \<open>Conjunction\<close> |
94 |
93 |
95 lemma conj_absorb [simp]: "x \<sqinter> x = x" |
94 lemma conj_absorb [simp]: "x \<sqinter> x = x" |
96 proof - |
95 proof - |
97 have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" |
96 have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" |
98 using disj_zero_right by simp |
97 by simp |
99 also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" |
98 also have "\<dots> = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" |
100 using conj_cancel_right by simp |
99 by simp |
101 also have "... = x \<sqinter> (x \<squnion> \<sim> x)" |
100 also have "\<dots> = x \<sqinter> (x \<squnion> \<sim> x)" |
102 using conj_disj_distrib by (simp only:) |
101 by (simp only: conj_disj_distrib) |
103 also have "... = x \<sqinter> \<one>" |
102 also have "\<dots> = x \<sqinter> \<one>" |
104 using disj_cancel_right by simp |
103 by simp |
105 also have "... = x" |
104 also have "\<dots> = x" |
106 using conj_one_right by simp |
105 by simp |
107 finally show ?thesis . |
106 finally show ?thesis . |
108 qed |
107 qed |
109 |
108 |
110 lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>" |
109 lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>" |
111 proof - |
110 proof - |
112 have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" |
111 from conj_cancel_right have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" |
113 using conj_cancel_right by simp |
112 by simp |
114 also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" |
113 also from conj_assoc have "\<dots> = (x \<sqinter> x) \<sqinter> \<sim> x" |
115 using conj_assoc by (simp only:) |
114 by (simp only:) |
116 also have "... = x \<sqinter> \<sim> x" |
115 also from conj_absorb have "\<dots> = x \<sqinter> \<sim> x" |
117 using conj_absorb by simp |
116 by simp |
118 also have "... = \<zero>" |
117 also have "\<dots> = \<zero>" |
119 using conj_cancel_right by simp |
118 by simp |
120 finally show ?thesis . |
119 finally show ?thesis . |
121 qed |
120 qed |
122 |
121 |
123 lemma compl_one [simp]: "\<sim> \<one> = \<zero>" |
122 lemma compl_one [simp]: "\<sim> \<one> = \<zero>" |
124 by (rule compl_unique [OF conj_zero_right disj_zero_right]) |
123 by (rule compl_unique [OF conj_zero_right disj_zero_right]) |
174 |
173 |
175 lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y" |
174 lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y" |
176 proof (rule compl_unique) |
175 proof (rule compl_unique) |
177 have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)" |
176 have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)" |
178 by (rule conj_disj_distrib) |
177 by (rule conj_disj_distrib) |
179 also have "... = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))" |
178 also have "\<dots> = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))" |
180 by (simp only: conj_ac) |
179 by (simp only: conj_ac) |
181 finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>" |
180 finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>" |
182 by (simp only: conj_cancel_right conj_zero_right disj_zero_right) |
181 by (simp only: conj_cancel_right conj_zero_right disj_zero_right) |
183 next |
182 next |
184 have "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = (x \<squnion> (\<sim> x \<squnion> \<sim> y)) \<sqinter> (y \<squnion> (\<sim> x \<squnion> \<sim> y))" |
183 have "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = (x \<squnion> (\<sim> x \<squnion> \<sim> y)) \<sqinter> (y \<squnion> (\<sim> x \<squnion> \<sim> y))" |
185 by (rule disj_conj_distrib2) |
184 by (rule disj_conj_distrib2) |
186 also have "... = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))" |
185 also have "\<dots> = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))" |
187 by (simp only: disj_ac) |
186 by (simp only: disj_ac) |
188 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>" |
189 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) |
190 qed |
189 qed |
191 |
190 |
203 begin |
202 begin |
204 |
203 |
205 sublocale xor: abel_semigroup xor |
204 sublocale xor: abel_semigroup xor |
206 proof |
205 proof |
207 fix x y z :: 'a |
206 fix x y z :: 'a |
208 let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion> |
207 let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)" |
209 (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)" |
208 have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) = ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)" |
210 have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) = |
|
211 ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)" |
|
212 by (simp only: conj_cancel_right conj_zero_right) |
209 by (simp only: conj_cancel_right conj_zero_right) |
213 then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
210 then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
214 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) |
211 by (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) |
215 apply (simp only: conj_disj_distribs conj_ac disj_ac) |
212 (simp only: conj_disj_distribs conj_ac disj_ac) |
216 done |
|
217 show "x \<oplus> y = y \<oplus> x" |
213 show "x \<oplus> y = y \<oplus> x" |
218 by (simp only: xor_def conj_commute disj_commute) |
214 by (simp only: xor_def conj_commute disj_commute) |
219 qed |
215 qed |
220 |
216 |
221 lemmas xor_assoc = xor.assoc |
217 lemmas xor_assoc = xor.assoc |