diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/Library/Boolean_Algebra.thy --- a/src/HOL/Library/Boolean_Algebra.thy Wed Jan 27 14:03:08 2010 +0100 +++ b/src/HOL/Library/Boolean_Algebra.thy Thu Jan 28 11:48:43 2010 +0100 @@ -24,15 +24,22 @@ assumes disj_zero_right [simp]: "x \ \ = x" assumes conj_cancel_right [simp]: "x \ \ x = \" assumes disj_cancel_right [simp]: "x \ \ x = \" + +sublocale boolean < conj!: abel_semigroup conj proof +qed (fact conj_assoc conj_commute)+ + +sublocale boolean < disj!: abel_semigroup disj proof +qed (fact disj_assoc disj_commute)+ + +context boolean begin -lemmas disj_ac = - disj_assoc disj_commute - mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute] +lemmas conj_left_commute = conj.left_commute -lemmas conj_ac = - conj_assoc conj_commute - mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute] +lemmas disj_left_commute = disj.left_commute + +lemmas conj_ac = conj.assoc conj.commute conj.left_commute +lemmas disj_ac = disj.assoc disj.commute disj.left_commute lemma dual: "boolean disj conj compl one zero" apply (rule boolean.intro) @@ -178,18 +185,9 @@ locale boolean_xor = boolean + fixes xor :: "'a => 'a => 'a" (infixr "\" 65) assumes xor_def: "x \ y = (x \ \ y) \ (\ x \ y)" -begin -lemma xor_def2: - "x \ y = (x \ y) \ (\ x \ \ y)" -by (simp only: xor_def conj_disj_distribs - disj_ac conj_ac conj_cancel_right disj_zero_left) - -lemma xor_commute: "x \ y = y \ x" -by (simp only: xor_def conj_commute disj_commute) - -lemma xor_assoc: "(x \ y) \ z = x \ (y \ z)" -proof - +sublocale boolean_xor < xor!: abel_semigroup xor proof + fix x y z :: 'a let ?t = "(x \ y \ z) \ (x \ \ y \ \ z) \ (\ x \ y \ \ z) \ (\ x \ \ y \ z)" have "?t \ (z \ x \ \ x) \ (z \ y \ \ y) = @@ -199,11 +197,23 @@ apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) apply (simp only: conj_disj_distribs conj_ac disj_ac) done + show "x \ y = y \ x" + by (simp only: xor_def conj_commute disj_commute) qed -lemmas xor_ac = - xor_assoc xor_commute - mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute] +context boolean_xor +begin + +lemmas xor_assoc = xor.assoc +lemmas xor_commute = xor.commute +lemmas xor_left_commute = xor.left_commute + +lemmas xor_ac = xor.assoc xor.commute xor.left_commute + +lemma xor_def2: + "x \ y = (x \ y) \ (\ x \ \ y)" +by (simp only: xor_def conj_disj_distribs + disj_ac conj_ac conj_cancel_right disj_zero_left) lemma xor_zero_right [simp]: "x \ \ = x" by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)