src/HOL/Library/Boolean_Algebra.thy
changeset 29996 c09f348ca88a
parent 29629 5111ce425e7a
child 30663 0b6aff7451b2
equal deleted inserted replaced
29995:62efbd0ef132 29996:c09f348ca88a
   221 by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
   221 by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
   222 
   222 
   223 lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
   223 lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
   224 by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
   224 by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
   225 
   225 
   226 lemma xor_compl_left: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
   226 lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
   227 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   227 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   228 apply (simp only: conj_disj_distribs)
   228 apply (simp only: conj_disj_distribs)
   229 apply (simp only: conj_cancel_right conj_cancel_left)
   229 apply (simp only: conj_cancel_right conj_cancel_left)
   230 apply (simp only: disj_zero_left disj_zero_right)
   230 apply (simp only: disj_zero_left disj_zero_right)
   231 apply (simp only: disj_ac conj_ac)
   231 apply (simp only: disj_ac conj_ac)
   232 done
   232 done
   233 
   233 
   234 lemma xor_compl_right: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
   234 lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
   235 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   235 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   236 apply (simp only: conj_disj_distribs)
   236 apply (simp only: conj_disj_distribs)
   237 apply (simp only: conj_cancel_right conj_cancel_left)
   237 apply (simp only: conj_cancel_right conj_cancel_left)
   238 apply (simp only: disj_zero_left disj_zero_right)
   238 apply (simp only: disj_zero_left disj_zero_right)
   239 apply (simp only: disj_ac conj_ac)
   239 apply (simp only: disj_ac conj_ac)
   240 done
   240 done
   241 
   241 
   242 lemma xor_cancel_right [simp]: "x \<oplus> \<sim> x = \<one>"
   242 lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>"
   243 by (simp only: xor_compl_right xor_self compl_zero)
   243 by (simp only: xor_compl_right xor_self compl_zero)
   244 
   244 
   245 lemma xor_cancel_left [simp]: "\<sim> x \<oplus> x = \<one>"
   245 lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>"
   246 by (subst xor_commute) (rule xor_cancel_right)
   246 by (simp only: xor_compl_left xor_self compl_zero)
   247 
   247 
   248 lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   248 lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   249 proof -
   249 proof -
   250   have "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
   250   have "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
   251         (y \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z)"
   251         (y \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z)"