tuned;
authorwenzelm
Thu Aug 06 14:29:05 2015 +0200 (2015-08-06)
changeset 608556449ae4b85f9
parent 60854 8f45dd297357
child 60856 eb21ae05ec43
tuned;
src/HOL/Library/Boolean_Algebra.thy
     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.6  
     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.11  
    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.16  
    1.17  lemmas conj_left_commute = conj.left_commute
    1.18  
    1.19 @@ -53,6 +53,7 @@
    1.20  apply (rule conj_cancel_right)
    1.21  done
    1.22  
    1.23 +
    1.24  subsection \<open>Complement\<close>
    1.25  
    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.30  
    1.31 +
    1.32  subsection \<open>Conjunction\<close>
    1.33  
    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.37  
    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.42  
    1.43  lemmas conj_disj_distribs =
    1.44     conj_disj_distrib conj_disj_distrib2
    1.45  
    1.46 +
    1.47  subsection \<open>Disjunction\<close>
    1.48  
    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.53  
    1.54 +
    1.55  subsection \<open>De Morgan's Laws\<close>
    1.56  
    1.57  lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
    1.58 @@ -178,14 +182,16 @@
    1.59  
    1.60  end
    1.61  
    1.62 +
    1.63  subsection \<open>Symmetric Difference\<close>
    1.64  
    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.70  
    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.80  
    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.90  
    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.94  
    1.95  end
    1.96