1(* Title: HOL/Library/Boolean_Algebra.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Boolean Algebras\<close> 6 7theory Boolean_Algebra 8 imports Main 9begin 10 11locale boolean_algebra = conj: abel_semigroup "(\<^bold>\<sqinter>)" + disj: abel_semigroup "(\<^bold>\<squnion>)" 12 for conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^bold>\<sqinter>" 70) 13 and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^bold>\<squnion>" 65) + 14 fixes compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80) 15 and zero :: "'a" ("\<zero>") 16 and one :: "'a" ("\<one>") 17 assumes conj_disj_distrib: "x \<^bold>\<sqinter> (y \<^bold>\<squnion> z) = (x \<^bold>\<sqinter> y) \<^bold>\<squnion> (x \<^bold>\<sqinter> z)" 18 and disj_conj_distrib: "x \<^bold>\<squnion> (y \<^bold>\<sqinter> z) = (x \<^bold>\<squnion> y) \<^bold>\<sqinter> (x \<^bold>\<squnion> z)" 19 and conj_one_right: "x \<^bold>\<sqinter> \<one> = x" 20 and disj_zero_right: "x \<^bold>\<squnion> \<zero> = x" 21 and conj_cancel_right [simp]: "x \<^bold>\<sqinter> \<sim> x = \<zero>" 22 and disj_cancel_right [simp]: "x \<^bold>\<squnion> \<sim> x = \<one>" 23begin 24 25sublocale conj: semilattice_neutr "(\<^bold>\<sqinter>)" "\<one>" 26proof 27 show "x \<^bold>\<sqinter> \<one> = x" for x 28 by (fact conj_one_right) 29 show "x \<^bold>\<sqinter> x = x" for x 30 proof - 31 have "x \<^bold>\<sqinter> x = (x \<^bold>\<sqinter> x) \<^bold>\<squnion> \<zero>" 32 by (simp add: disj_zero_right) 33 also have "\<dots> = (x \<^bold>\<sqinter> x) \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> x)" 34 by simp 35 also have "\<dots> = x \<^bold>\<sqinter> (x \<^bold>\<squnion> \<sim> x)" 36 by (simp only: conj_disj_distrib) 37 also have "\<dots> = x \<^bold>\<sqinter> \<one>" 38 by simp 39 also have "\<dots> = x" 40 by (simp add: conj_one_right) 41 finally show ?thesis . 42 qed 43qed 44 45sublocale disj: semilattice_neutr "(\<^bold>\<squnion>)" "\<zero>" 46proof 47 show "x \<^bold>\<squnion> \<zero> = x" for x 48 by (fact disj_zero_right) 49 show "x \<^bold>\<squnion> x = x" for x 50 proof - 51 have "x \<^bold>\<squnion> x = (x \<^bold>\<squnion> x) \<^bold>\<sqinter> \<one>" 52 by simp 53 also have "\<dots> = (x \<^bold>\<squnion> x) \<^bold>\<sqinter> (x \<^bold>\<squnion> \<sim> x)" 54 by simp 55 also have "\<dots> = x \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> x)" 56 by (simp only: disj_conj_distrib) 57 also have "\<dots> = x \<^bold>\<squnion> \<zero>" 58 by simp 59 also have "\<dots> = x" 60 by (simp add: disj_zero_right) 61 finally show ?thesis . 62 qed 63qed 64 65 66subsection \<open>Complement\<close> 67 68lemma complement_unique: 69 assumes 1: "a \<^bold>\<sqinter> x = \<zero>" 70 assumes 2: "a \<^bold>\<squnion> x = \<one>" 71 assumes 3: "a \<^bold>\<sqinter> y = \<zero>" 72 assumes 4: "a \<^bold>\<squnion> y = \<one>" 73 shows "x = y" 74proof - 75 from 1 3 have "(a \<^bold>\<sqinter> x) \<^bold>\<squnion> (x \<^bold>\<sqinter> y) = (a \<^bold>\<sqinter> y) \<^bold>\<squnion> (x \<^bold>\<sqinter> y)" 76 by simp 77 then have "(x \<^bold>\<sqinter> a) \<^bold>\<squnion> (x \<^bold>\<sqinter> y) = (y \<^bold>\<sqinter> a) \<^bold>\<squnion> (y \<^bold>\<sqinter> x)" 78 by (simp add: ac_simps) 79 then have "x \<^bold>\<sqinter> (a \<^bold>\<squnion> y) = y \<^bold>\<sqinter> (a \<^bold>\<squnion> x)" 80 by (simp add: conj_disj_distrib) 81 with 2 4 have "x \<^bold>\<sqinter> \<one> = y \<^bold>\<sqinter> \<one>" 82 by simp 83 then show "x = y" 84 by simp 85qed 86 87lemma compl_unique: "x \<^bold>\<sqinter> y = \<zero> \<Longrightarrow> x \<^bold>\<squnion> y = \<one> \<Longrightarrow> \<sim> x = y" 88 by (rule complement_unique [OF conj_cancel_right disj_cancel_right]) 89 90lemma double_compl [simp]: "\<sim> (\<sim> x) = x" 91proof (rule compl_unique) 92 show "\<sim> x \<^bold>\<sqinter> x = \<zero>" 93 by (simp only: conj_cancel_right conj.commute) 94 show "\<sim> x \<^bold>\<squnion> x = \<one>" 95 by (simp only: disj_cancel_right disj.commute) 96qed 97 98lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y" 99 by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl) 100 101 102subsection \<open>Conjunction\<close> 103 104lemma conj_zero_right [simp]: "x \<^bold>\<sqinter> \<zero> = \<zero>" 105 using conj.left_idem conj_cancel_right by fastforce 106 107lemma compl_one [simp]: "\<sim> \<one> = \<zero>" 108 by (rule compl_unique [OF conj_zero_right disj_zero_right]) 109 110lemma conj_zero_left [simp]: "\<zero> \<^bold>\<sqinter> x = \<zero>" 111 by (subst conj.commute) (rule conj_zero_right) 112 113lemma conj_cancel_left [simp]: "\<sim> x \<^bold>\<sqinter> x = \<zero>" 114 by (subst conj.commute) (rule conj_cancel_right) 115 116lemma conj_disj_distrib2: "(y \<^bold>\<squnion> z) \<^bold>\<sqinter> x = (y \<^bold>\<sqinter> x) \<^bold>\<squnion> (z \<^bold>\<sqinter> x)" 117 by (simp only: conj.commute conj_disj_distrib) 118 119lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2 120 121lemma conj_assoc: "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> (y \<^bold>\<sqinter> z)" 122 by (fact ac_simps) 123 124lemma conj_commute: "x \<^bold>\<sqinter> y = y \<^bold>\<sqinter> x" 125 by (fact ac_simps) 126 127lemmas conj_left_commute = conj.left_commute 128lemmas conj_ac = conj.assoc conj.commute conj.left_commute 129 130lemma conj_one_left: "\<one> \<^bold>\<sqinter> x = x" 131 by (fact conj.left_neutral) 132 133lemma conj_left_absorb: "x \<^bold>\<sqinter> (x \<^bold>\<sqinter> y) = x \<^bold>\<sqinter> y" 134 by (fact conj.left_idem) 135 136lemma conj_absorb: "x \<^bold>\<sqinter> x = x" 137 by (fact conj.idem) 138 139 140subsection \<open>Disjunction\<close> 141 142interpretation dual: boolean_algebra "(\<^bold>\<squnion>)" "(\<^bold>\<sqinter>)" compl \<one> \<zero> 143 apply standard 144 apply (rule disj_conj_distrib) 145 apply (rule conj_disj_distrib) 146 apply simp_all 147 done 148 149lemma compl_zero [simp]: "\<sim> \<zero> = \<one>" 150 by (fact dual.compl_one) 151 152lemma disj_one_right [simp]: "x \<^bold>\<squnion> \<one> = \<one>" 153 by (fact dual.conj_zero_right) 154 155lemma disj_one_left [simp]: "\<one> \<^bold>\<squnion> x = \<one>" 156 by (fact dual.conj_zero_left) 157 158lemma disj_cancel_left [simp]: "\<sim> x \<^bold>\<squnion> x = \<one>" 159 by (rule dual.conj_cancel_left) 160 161lemma disj_conj_distrib2: "(y \<^bold>\<sqinter> z) \<^bold>\<squnion> x = (y \<^bold>\<squnion> x) \<^bold>\<sqinter> (z \<^bold>\<squnion> x)" 162 by (rule dual.conj_disj_distrib2) 163 164lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2 165 166lemma disj_assoc: "(x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> (y \<^bold>\<squnion> z)" 167 by (fact ac_simps) 168 169lemma disj_commute: "x \<^bold>\<squnion> y = y \<^bold>\<squnion> x" 170 by (fact ac_simps) 171 172lemmas disj_left_commute = disj.left_commute 173 174lemmas disj_ac = disj.assoc disj.commute disj.left_commute 175 176lemma disj_zero_left: "\<zero> \<^bold>\<squnion> x = x" 177 by (fact disj.left_neutral) 178 179lemma disj_left_absorb: "x \<^bold>\<squnion> (x \<^bold>\<squnion> y) = x \<^bold>\<squnion> y" 180 by (fact disj.left_idem) 181 182lemma disj_absorb: "x \<^bold>\<squnion> x = x" 183 by (fact disj.idem) 184 185 186subsection \<open>De Morgan's Laws\<close> 187 188lemma de_Morgan_conj [simp]: "\<sim> (x \<^bold>\<sqinter> y) = \<sim> x \<^bold>\<squnion> \<sim> y" 189proof (rule compl_unique) 190 have "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> (\<sim> x \<^bold>\<squnion> \<sim> y) = ((x \<^bold>\<sqinter> y) \<^bold>\<sqinter> \<sim> x) \<^bold>\<squnion> ((x \<^bold>\<sqinter> y) \<^bold>\<sqinter> \<sim> y)" 191 by (rule conj_disj_distrib) 192 also have "\<dots> = (y \<^bold>\<sqinter> (x \<^bold>\<sqinter> \<sim> x)) \<^bold>\<squnion> (x \<^bold>\<sqinter> (y \<^bold>\<sqinter> \<sim> y))" 193 by (simp only: conj_ac) 194 finally show "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> (\<sim> x \<^bold>\<squnion> \<sim> y) = \<zero>" 195 by (simp only: conj_cancel_right conj_zero_right disj_zero_right) 196next 197 have "(x \<^bold>\<sqinter> y) \<^bold>\<squnion> (\<sim> x \<^bold>\<squnion> \<sim> y) = (x \<^bold>\<squnion> (\<sim> x \<^bold>\<squnion> \<sim> y)) \<^bold>\<sqinter> (y \<^bold>\<squnion> (\<sim> x \<^bold>\<squnion> \<sim> y))" 198 by (rule disj_conj_distrib2) 199 also have "\<dots> = (\<sim> y \<^bold>\<squnion> (x \<^bold>\<squnion> \<sim> x)) \<^bold>\<sqinter> (\<sim> x \<^bold>\<squnion> (y \<^bold>\<squnion> \<sim> y))" 200 by (simp only: disj_ac) 201 finally show "(x \<^bold>\<sqinter> y) \<^bold>\<squnion> (\<sim> x \<^bold>\<squnion> \<sim> y) = \<one>" 202 by (simp only: disj_cancel_right disj_one_right conj_one_right) 203qed 204 205lemma de_Morgan_disj [simp]: "\<sim> (x \<^bold>\<squnion> y) = \<sim> x \<^bold>\<sqinter> \<sim> y" 206 using dual.boolean_algebra_axioms by (rule boolean_algebra.de_Morgan_conj) 207 208 209subsection \<open>Symmetric Difference\<close> 210 211definition xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<oplus>" 65) 212 where "x \<oplus> y = (x \<^bold>\<sqinter> \<sim> y) \<^bold>\<squnion> (\<sim> x \<^bold>\<sqinter> y)" 213 214sublocale xor: comm_monoid xor \<zero> 215proof 216 fix x y z :: 'a 217 let ?t = "(x \<^bold>\<sqinter> y \<^bold>\<sqinter> z) \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (\<sim> x \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (\<sim> x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> z)" 218 have "?t \<^bold>\<squnion> (z \<^bold>\<sqinter> x \<^bold>\<sqinter> \<sim> x) \<^bold>\<squnion> (z \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> y) = ?t \<^bold>\<squnion> (x \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> y) \<^bold>\<squnion> (x \<^bold>\<sqinter> z \<^bold>\<sqinter> \<sim> z)" 219 by (simp only: conj_cancel_right conj_zero_right) 220 then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 221 by (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) 222 (simp only: conj_disj_distribs conj_ac disj_ac) 223 show "x \<oplus> y = y \<oplus> x" 224 by (simp only: xor_def conj_commute disj_commute) 225 show "x \<oplus> \<zero> = x" 226 by (simp add: xor_def) 227qed 228 229lemmas xor_assoc = xor.assoc 230lemmas xor_commute = xor.commute 231lemmas xor_left_commute = xor.left_commute 232 233lemmas xor_ac = xor.assoc xor.commute xor.left_commute 234 235lemma xor_def2: "x \<oplus> y = (x \<^bold>\<squnion> y) \<^bold>\<sqinter> (\<sim> x \<^bold>\<squnion> \<sim> y)" 236 using conj.commute conj_disj_distrib2 disj.commute xor_def by auto 237 238lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x" 239 by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right) 240 241lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x" 242 by (subst xor_commute) (rule xor_zero_right) 243 244lemma xor_one_right [simp]: "x \<oplus> \<one> = \<sim> x" 245 by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left) 246 247lemma xor_one_left [simp]: "\<one> \<oplus> x = \<sim> x" 248 by (subst xor_commute) (rule xor_one_right) 249 250lemma xor_self [simp]: "x \<oplus> x = \<zero>" 251 by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right) 252 253lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y" 254 by (simp only: xor_assoc [symmetric] xor_self xor_zero_left) 255 256lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)" 257 by (metis xor_assoc xor_one_left) 258 259lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)" 260 using xor_commute xor_compl_left by auto 261 262lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>" 263 by (simp only: xor_compl_right xor_self compl_zero) 264 265lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>" 266 by (simp only: xor_compl_left xor_self compl_zero) 267 268lemma conj_xor_distrib: "x \<^bold>\<sqinter> (y \<oplus> z) = (x \<^bold>\<sqinter> y) \<oplus> (x \<^bold>\<sqinter> z)" 269proof - 270 have *: "(x \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> z) = 271 (y \<^bold>\<sqinter> x \<^bold>\<sqinter> \<sim> x) \<^bold>\<squnion> (z \<^bold>\<sqinter> x \<^bold>\<sqinter> \<sim> x) \<^bold>\<squnion> (x \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> z)" 272 by (simp only: conj_cancel_right conj_zero_right disj_zero_left) 273 then show "x \<^bold>\<sqinter> (y \<oplus> z) = (x \<^bold>\<sqinter> y) \<oplus> (x \<^bold>\<sqinter> z)" 274 by (simp (no_asm_use) only: 275 xor_def de_Morgan_disj de_Morgan_conj double_compl 276 conj_disj_distribs conj_ac disj_ac) 277qed 278 279lemma conj_xor_distrib2: "(y \<oplus> z) \<^bold>\<sqinter> x = (y \<^bold>\<sqinter> x) \<oplus> (z \<^bold>\<sqinter> x)" 280 by (simp add: conj.commute conj_xor_distrib) 281 282lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2 283 284end 285 286end 287