src/HOL/Library/Boolean_Algebra.thy
equal inserted replaced
`    22   assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"`
`    22   assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"`
`    23   assumes conj_one_right [simp]: "x \<sqinter> \<one> = x"`
`    23   assumes conj_one_right [simp]: "x \<sqinter> \<one> = x"`
`    24   assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"`
`    24   assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"`
`    25   assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"`
`    25   assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"`
`    26   assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"`
`    26   assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"`
`       `
`    27 `
`       `
`    28 sublocale boolean < conj!: abel_semigroup conj proof`
`       `
`    29 qed (fact conj_assoc conj_commute)+`
`       `
`    30 `
`       `
`    31 sublocale boolean < disj!: abel_semigroup disj proof`
`       `
`    32 qed (fact disj_assoc disj_commute)+`
`       `
`    33 `
`       `
`    34 context boolean`
`    27 begin`
`    35 begin`
`    28 `
`    36 `
`    29 lemmas disj_ac =`
`    37 lemmas conj_left_commute = conj.left_commute`
`    30   disj_assoc disj_commute`
`    38 `
`    31   mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute]`
`    39 lemmas disj_left_commute = disj.left_commute`
`    32 `
`    40 `
`    33 lemmas conj_ac =`
`    41 lemmas conj_ac = conj.assoc conj.commute conj.left_commute`
`    34   conj_assoc conj_commute`
`    42 lemmas disj_ac = disj.assoc disj.commute disj.left_commute`
`    35   mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute]`
`       `
`    36 `
`    43 `
`    37 lemma dual: "boolean disj conj compl one zero"`
`    44 lemma dual: "boolean disj conj compl one zero"`
`    38 apply (rule boolean.intro)`
`    45 apply (rule boolean.intro)`
`    39 apply (rule disj_assoc)`
`    46 apply (rule disj_assoc)`
`    40 apply (rule conj_assoc)`
`    47 apply (rule conj_assoc)`
`   176 subsection {* Symmetric Difference *}`
`   183 subsection {* Symmetric Difference *}`
`   177 `
`   184 `
`   178 locale boolean_xor = boolean +`
`   185 locale boolean_xor = boolean +`
`   179   fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)`
`   186   fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)`
`   180   assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"`
`   187   assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"`
`   181 begin`
`   188 `
`   182 `
`   189 sublocale boolean_xor < xor!: abel_semigroup xor proof`
`   183 lemma xor_def2:`
`   190   fix x y z :: 'a`
`   184   "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"`
`       `
`   185 by (simp only: xor_def conj_disj_distribs`
`       `
`   186                disj_ac conj_ac conj_cancel_right disj_zero_left)`
`       `
`   187 `
`       `
`   188 lemma xor_commute: "x \<oplus> y = y \<oplus> x"`
`       `
`   189 by (simp only: xor_def conj_commute disj_commute)`
`       `
`   190 `
`       `
`   191 lemma xor_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"`
`       `
`   192 proof -`
`       `
`   193   let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>`
`   191   let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>`
`   194             (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"`
`   192             (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"`
`   195   have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =`
`   193   have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =`
`   196         ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"`
`   194         ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"`
`   197     by (simp only: conj_cancel_right conj_zero_right)`
`   195     by (simp only: conj_cancel_right conj_zero_right)`
`   198   thus "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"`
`   196   thus "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"`
`   199     apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)`
`   197     apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)`
`   200     apply (simp only: conj_disj_distribs conj_ac disj_ac)`
`   198     apply (simp only: conj_disj_distribs conj_ac disj_ac)`
`   201     done`
`   199     done`
`   202 qed`
`   200   show "x \<oplus> y = y \<oplus> x"`
`   203 `
`   201     by (simp only: xor_def conj_commute disj_commute)`
`   204 lemmas xor_ac =`
`   202 qed`
`   205   xor_assoc xor_commute`
`   203 `
`   206   mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute]`
`   204 context boolean_xor`
`       `
`   205 begin`
`       `
`   206 `
`       `
`   207 lemmas xor_assoc = xor.assoc`
`       `
`   208 lemmas xor_commute = xor.commute`
`       `
`   209 lemmas xor_left_commute = xor.left_commute`
`       `
`   210 `
`       `
`   211 lemmas xor_ac = xor.assoc xor.commute xor.left_commute`
`       `
`   212 `
`       `
`   213 lemma xor_def2:`
`       `
`   214   "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"`
`       `
`   215 by (simp only: xor_def conj_disj_distribs`
`       `
`   216                disj_ac conj_ac conj_cancel_right disj_zero_left)`
`   207 `
`   217 `
`   208 lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"`
`   218 lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"`
`   209 by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)`
`   219 by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)`
`   210 `
`   220 `
`   211 lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x"`
`   221 lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x"`