src/HOL/Library/Boolean_Algebra.thy
 changeset 60855 6449ae4b85f9 parent 60500 903bb1495239 child 61605 1bf7b186542e
1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Thu Aug 06 14:28:59 2015 +0200
1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Aug 06 14:29:05 2015 +0200
1.3 @@ -26,11 +26,11 @@
1.4    assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
1.5  begin
1.7 -sublocale conj!: abel_semigroup conj proof
1.8 -qed (fact conj_assoc conj_commute)+
1.9 +sublocale conj!: abel_semigroup conj
1.10 +  by standard (fact conj_assoc conj_commute)+
1.12 -sublocale disj!: abel_semigroup disj proof
1.13 -qed (fact disj_assoc disj_commute)+
1.14 +sublocale disj!: abel_semigroup disj
1.15 +  by standard (fact disj_assoc disj_commute)+
1.17  lemmas conj_left_commute = conj.left_commute
1.19 @@ -53,6 +53,7 @@
1.20  apply (rule conj_cancel_right)
1.21  done
1.23 +
1.24  subsection \<open>Complement\<close>
1.26  lemma complement_unique:
1.27 @@ -81,6 +82,7 @@
1.28  lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
1.29  by (rule inj_eq [OF inj_on_inverseI], rule double_compl)
1.31 +
1.32  subsection \<open>Conjunction\<close>
1.34  lemma conj_absorb [simp]: "x \<sqinter> x = x"
1.35 @@ -118,12 +120,13 @@
1.36  by (simp only: conj_assoc [symmetric] conj_absorb)
1.38  lemma conj_disj_distrib2:
1.39 -  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
1.40 +  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
1.41  by (simp only: conj_commute conj_disj_distrib)
1.43  lemmas conj_disj_distribs =
1.44     conj_disj_distrib conj_disj_distrib2
1.46 +
1.47  subsection \<open>Disjunction\<close>
1.49  lemma disj_absorb [simp]: "x \<squnion> x = x"
1.50 @@ -154,6 +157,7 @@
1.51  lemmas disj_conj_distribs =
1.52     disj_conj_distrib disj_conj_distrib2
1.54 +
1.55  subsection \<open>De Morgan's Laws\<close>
1.57  lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
1.58 @@ -178,14 +182,16 @@
1.60  end
1.62 +
1.63  subsection \<open>Symmetric Difference\<close>
1.65  locale boolean_xor = boolean +
1.66 -  fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
1.67 +  fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<oplus>" 65)
1.68    assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
1.69  begin
1.71 -sublocale xor!: abel_semigroup xor proof
1.72 +sublocale xor!: abel_semigroup xor
1.73 +proof
1.74    fix x y z :: 'a
1.75    let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
1.76              (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
1.77 @@ -262,8 +268,7 @@
1.78          conj_disj_distribs conj_ac disj_ac)
1.79  qed
1.81 -lemma conj_xor_distrib2:
1.82 -  "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
1.83 +lemma conj_xor_distrib2: "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
1.84  proof -
1.85    have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
1.86      by (rule conj_xor_distrib)
1.87 @@ -271,8 +276,7 @@
1.88      by (simp only: conj_commute)
1.89  qed
1.91 -lemmas conj_xor_distribs =
1.92 -   conj_xor_distrib conj_xor_distrib2
1.93 +lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2
1.95  end