haftmann@29629: (* Title: HOL/Library/Boolean_Algebra.thy haftmann@29629: Author: Brian Huffman kleing@24332: *) kleing@24332: kleing@24332: header {* Boolean Algebras *} kleing@24332: kleing@24332: theory Boolean_Algebra haftmann@27368: imports Plain kleing@24332: begin kleing@24332: kleing@24332: locale boolean = huffman@24357: fixes conj :: "'a \ 'a \ 'a" (infixr "\" 70) huffman@24357: fixes disj :: "'a \ 'a \ 'a" (infixr "\" 65) huffman@24357: fixes compl :: "'a \ 'a" ("\ _" [81] 80) kleing@24332: fixes zero :: "'a" ("\") kleing@24332: fixes one :: "'a" ("\") kleing@24332: assumes conj_assoc: "(x \ y) \ z = x \ (y \ z)" kleing@24332: assumes disj_assoc: "(x \ y) \ z = x \ (y \ z)" kleing@24332: assumes conj_commute: "x \ y = y \ x" kleing@24332: assumes disj_commute: "x \ y = y \ x" kleing@24332: assumes conj_disj_distrib: "x \ (y \ z) = (x \ y) \ (x \ z)" kleing@24332: assumes disj_conj_distrib: "x \ (y \ z) = (x \ y) \ (x \ z)" huffman@24357: assumes conj_one_right [simp]: "x \ \ = x" huffman@24357: assumes disj_zero_right [simp]: "x \ \ = x" huffman@24357: assumes conj_cancel_right [simp]: "x \ \ x = \" huffman@24357: assumes disj_cancel_right [simp]: "x \ \ x = \" kleing@24332: begin kleing@24332: kleing@24332: lemmas disj_ac = kleing@24332: disj_assoc disj_commute ballarin@25283: mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute] kleing@24332: kleing@24332: lemmas conj_ac = kleing@24332: conj_assoc conj_commute ballarin@25283: mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute] kleing@24332: kleing@24332: lemma dual: "boolean disj conj compl one zero" kleing@24332: apply (rule boolean.intro) kleing@24332: apply (rule disj_assoc) kleing@24332: apply (rule conj_assoc) kleing@24332: apply (rule disj_commute) kleing@24332: apply (rule conj_commute) kleing@24332: apply (rule disj_conj_distrib) kleing@24332: apply (rule conj_disj_distrib) kleing@24332: apply (rule disj_zero_right) kleing@24332: apply (rule conj_one_right) kleing@24332: apply (rule disj_cancel_right) kleing@24332: apply (rule conj_cancel_right) kleing@24332: done kleing@24332: huffman@24357: subsection {* Complement *} kleing@24332: kleing@24332: lemma complement_unique: kleing@24332: assumes 1: "a \ x = \" kleing@24332: assumes 2: "a \ x = \" kleing@24332: assumes 3: "a \ y = \" kleing@24332: assumes 4: "a \ y = \" kleing@24332: shows "x = y" kleing@24332: proof - kleing@24332: have "(a \ x) \ (x \ y) = (a \ y) \ (x \ y)" using 1 3 by simp kleing@24332: hence "(x \ a) \ (x \ y) = (y \ a) \ (y \ x)" using conj_commute by simp kleing@24332: hence "x \ (a \ y) = y \ (a \ x)" using conj_disj_distrib by simp kleing@24332: hence "x \ \ = y \ \" using 2 4 by simp kleing@24332: thus "x = y" using conj_one_right by simp kleing@24332: qed kleing@24332: huffman@24357: lemma compl_unique: "\x \ y = \; x \ y = \\ \ \ x = y" kleing@24332: by (rule complement_unique [OF conj_cancel_right disj_cancel_right]) kleing@24332: kleing@24332: lemma double_compl [simp]: "\ (\ x) = x" kleing@24332: proof (rule compl_unique) huffman@24357: from conj_cancel_right show "\ x \ x = \" by (simp only: conj_commute) huffman@24357: from disj_cancel_right show "\ x \ x = \" by (simp only: disj_commute) kleing@24332: qed kleing@24332: kleing@24332: lemma compl_eq_compl_iff [simp]: "(\ x = \ y) = (x = y)" kleing@24332: by (rule inj_eq [OF inj_on_inverseI], rule double_compl) kleing@24332: huffman@24357: subsection {* Conjunction *} kleing@24332: huffman@24393: lemma conj_absorb [simp]: "x \ x = x" kleing@24332: proof - kleing@24332: have "x \ x = (x \ x) \ \" using disj_zero_right by simp kleing@24332: also have "... = (x \ x) \ (x \ \ x)" using conj_cancel_right by simp huffman@24357: also have "... = x \ (x \ \ x)" using conj_disj_distrib by (simp only:) kleing@24332: also have "... = x \ \" using disj_cancel_right by simp kleing@24332: also have "... = x" using conj_one_right by simp kleing@24332: finally show ?thesis . kleing@24332: qed kleing@24332: kleing@24332: lemma conj_zero_right [simp]: "x \ \ = \" kleing@24332: proof - kleing@24332: have "x \ \ = x \ (x \ \ x)" using conj_cancel_right by simp huffman@24393: also have "... = (x \ x) \ \ x" using conj_assoc by (simp only:) kleing@24332: also have "... = x \ \ x" using conj_absorb by simp kleing@24332: also have "... = \" using conj_cancel_right by simp kleing@24332: finally show ?thesis . kleing@24332: qed kleing@24332: kleing@24332: lemma compl_one [simp]: "\ \ = \" kleing@24332: by (rule compl_unique [OF conj_zero_right disj_zero_right]) kleing@24332: kleing@24332: lemma conj_zero_left [simp]: "\ \ x = \" kleing@24332: by (subst conj_commute) (rule conj_zero_right) kleing@24332: kleing@24332: lemma conj_one_left [simp]: "\ \ x = x" kleing@24332: by (subst conj_commute) (rule conj_one_right) kleing@24332: kleing@24332: lemma conj_cancel_left [simp]: "\ x \ x = \" kleing@24332: by (subst conj_commute) (rule conj_cancel_right) kleing@24332: kleing@24332: lemma conj_left_absorb [simp]: "x \ (x \ y) = x \ y" huffman@24357: by (simp only: conj_assoc [symmetric] conj_absorb) kleing@24332: kleing@24332: lemma conj_disj_distrib2: kleing@24332: "(y \ z) \ x = (y \ x) \ (z \ x)" huffman@24357: by (simp only: conj_commute conj_disj_distrib) kleing@24332: kleing@24332: lemmas conj_disj_distribs = kleing@24332: conj_disj_distrib conj_disj_distrib2 kleing@24332: huffman@24357: subsection {* Disjunction *} kleing@24332: kleing@24332: lemma disj_absorb [simp]: "x \ x = x" kleing@24332: by (rule boolean.conj_absorb [OF dual]) kleing@24332: kleing@24332: lemma disj_one_right [simp]: "x \ \ = \" kleing@24332: by (rule boolean.conj_zero_right [OF dual]) kleing@24332: kleing@24332: lemma compl_zero [simp]: "\ \ = \" kleing@24332: by (rule boolean.compl_one [OF dual]) kleing@24332: kleing@24332: lemma disj_zero_left [simp]: "\ \ x = x" kleing@24332: by (rule boolean.conj_one_left [OF dual]) kleing@24332: kleing@24332: lemma disj_one_left [simp]: "\ \ x = \" kleing@24332: by (rule boolean.conj_zero_left [OF dual]) kleing@24332: kleing@24332: lemma disj_cancel_left [simp]: "\ x \ x = \" kleing@24332: by (rule boolean.conj_cancel_left [OF dual]) kleing@24332: kleing@24332: lemma disj_left_absorb [simp]: "x \ (x \ y) = x \ y" kleing@24332: by (rule boolean.conj_left_absorb [OF dual]) kleing@24332: kleing@24332: lemma disj_conj_distrib2: kleing@24332: "(y \ z) \ x = (y \ x) \ (z \ x)" kleing@24332: by (rule boolean.conj_disj_distrib2 [OF dual]) kleing@24332: kleing@24332: lemmas disj_conj_distribs = kleing@24332: disj_conj_distrib disj_conj_distrib2 kleing@24332: huffman@24357: subsection {* De Morgan's Laws *} kleing@24332: kleing@24332: lemma de_Morgan_conj [simp]: "\ (x \ y) = \ x \ \ y" kleing@24332: proof (rule compl_unique) kleing@24332: have "(x \ y) \ (\ x \ \ y) = ((x \ y) \ \ x) \ ((x \ y) \ \ y)" kleing@24332: by (rule conj_disj_distrib) kleing@24332: also have "... = (y \ (x \ \ x)) \ (x \ (y \ \ y))" huffman@24357: by (simp only: conj_ac) kleing@24332: finally show "(x \ y) \ (\ x \ \ y) = \" huffman@24357: by (simp only: conj_cancel_right conj_zero_right disj_zero_right) kleing@24332: next kleing@24332: have "(x \ y) \ (\ x \ \ y) = (x \ (\ x \ \ y)) \ (y \ (\ x \ \ y))" kleing@24332: by (rule disj_conj_distrib2) kleing@24332: also have "... = (\ y \ (x \ \ x)) \ (\ x \ (y \ \ y))" huffman@24357: by (simp only: disj_ac) kleing@24332: finally show "(x \ y) \ (\ x \ \ y) = \" huffman@24357: by (simp only: disj_cancel_right disj_one_right conj_one_right) kleing@24332: qed kleing@24332: kleing@24332: lemma de_Morgan_disj [simp]: "\ (x \ y) = \ x \ \ y" kleing@24332: by (rule boolean.de_Morgan_conj [OF dual]) kleing@24332: kleing@24332: end kleing@24332: huffman@24357: subsection {* Symmetric Difference *} kleing@24332: kleing@24332: locale boolean_xor = boolean + kleing@24332: fixes xor :: "'a => 'a => 'a" (infixr "\" 65) kleing@24332: assumes xor_def: "x \ y = (x \ \ y) \ (\ x \ y)" kleing@24332: begin kleing@24332: kleing@24332: lemma xor_def2: kleing@24332: "x \ y = (x \ y) \ (\ x \ \ y)" huffman@24357: by (simp only: xor_def conj_disj_distribs huffman@24357: disj_ac conj_ac conj_cancel_right disj_zero_left) kleing@24332: kleing@24332: lemma xor_commute: "x \ y = y \ x" huffman@24357: by (simp only: xor_def conj_commute disj_commute) kleing@24332: kleing@24332: lemma xor_assoc: "(x \ y) \ z = x \ (y \ z)" kleing@24332: proof - kleing@24332: let ?t = "(x \ y \ z) \ (x \ \ y \ \ z) \ kleing@24332: (\ x \ y \ \ z) \ (\ x \ \ y \ z)" kleing@24332: have "?t \ (z \ x \ \ x) \ (z \ y \ \ y) = kleing@24332: ?t \ (x \ y \ \ y) \ (x \ z \ \ z)" huffman@24357: by (simp only: conj_cancel_right conj_zero_right) kleing@24332: thus "(x \ y) \ z = x \ (y \ z)" huffman@24357: apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) huffman@24357: apply (simp only: conj_disj_distribs conj_ac disj_ac) kleing@24332: done kleing@24332: qed kleing@24332: kleing@24332: lemmas xor_ac = kleing@24332: xor_assoc xor_commute ballarin@25283: mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute] kleing@24332: kleing@24332: lemma xor_zero_right [simp]: "x \ \ = x" huffman@24357: by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right) kleing@24332: kleing@24332: lemma xor_zero_left [simp]: "\ \ x = x" kleing@24332: by (subst xor_commute) (rule xor_zero_right) kleing@24332: kleing@24332: lemma xor_one_right [simp]: "x \ \ = \ x" huffman@24357: by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left) kleing@24332: kleing@24332: lemma xor_one_left [simp]: "\ \ x = \ x" kleing@24332: by (subst xor_commute) (rule xor_one_right) kleing@24332: kleing@24332: lemma xor_self [simp]: "x \ x = \" huffman@24357: by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right) kleing@24332: kleing@24332: lemma xor_left_self [simp]: "x \ (x \ y) = y" huffman@24357: by (simp only: xor_assoc [symmetric] xor_self xor_zero_left) kleing@24332: huffman@29996: lemma xor_compl_left [simp]: "\ x \ y = \ (x \ y)" huffman@24357: apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) huffman@24357: apply (simp only: conj_disj_distribs) huffman@24357: apply (simp only: conj_cancel_right conj_cancel_left) huffman@24357: apply (simp only: disj_zero_left disj_zero_right) huffman@24357: apply (simp only: disj_ac conj_ac) kleing@24332: done kleing@24332: huffman@29996: lemma xor_compl_right [simp]: "x \ \ y = \ (x \ y)" huffman@24357: apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) huffman@24357: apply (simp only: conj_disj_distribs) huffman@24357: apply (simp only: conj_cancel_right conj_cancel_left) huffman@24357: apply (simp only: disj_zero_left disj_zero_right) huffman@24357: apply (simp only: disj_ac conj_ac) kleing@24332: done kleing@24332: huffman@29996: lemma xor_cancel_right: "x \ \ x = \" huffman@24357: by (simp only: xor_compl_right xor_self compl_zero) kleing@24332: huffman@29996: lemma xor_cancel_left: "\ x \ x = \" huffman@29996: by (simp only: xor_compl_left xor_self compl_zero) kleing@24332: kleing@24332: lemma conj_xor_distrib: "x \ (y \ z) = (x \ y) \ (x \ z)" kleing@24332: proof - kleing@24332: have "(x \ y \ \ z) \ (x \ \ y \ z) = kleing@24332: (y \ x \ \ x) \ (z \ x \ \ x) \ (x \ y \ \ z) \ (x \ \ y \ z)" huffman@24357: by (simp only: conj_cancel_right conj_zero_right disj_zero_left) kleing@24332: thus "x \ (y \ z) = (x \ y) \ (x \ z)" huffman@24357: by (simp (no_asm_use) only: kleing@24332: xor_def de_Morgan_disj de_Morgan_conj double_compl kleing@24332: conj_disj_distribs conj_ac disj_ac) kleing@24332: qed kleing@24332: kleing@24332: lemma conj_xor_distrib2: kleing@24332: "(y \ z) \ x = (y \ x) \ (z \ x)" kleing@24332: proof - kleing@24332: have "x \ (y \ z) = (x \ y) \ (x \ z)" kleing@24332: by (rule conj_xor_distrib) kleing@24332: thus "(y \ z) \ x = (y \ x) \ (z \ x)" huffman@24357: by (simp only: conj_commute) kleing@24332: qed kleing@24332: kleing@24332: lemmas conj_xor_distribs = kleing@24332: conj_xor_distrib conj_xor_distrib2 kleing@24332: kleing@24332: end kleing@24332: kleing@24332: end