src/HOL/Library/Boolean_Algebra.thy
changeset 34973 ae634fad947e
parent 30663 0b6aff7451b2
child 54868 bab6cade3cc5
equal deleted inserted replaced
34972:cc1d4c3ca9db 34973:ae634fad947e
    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"