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