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