src/HOL/Library/Boolean_Algebra.thy
 changeset 29996 c09f348ca88a parent 29629 5111ce425e7a child 30663 0b6aff7451b2
equal 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)"`