author wenzelm Thu, 06 Aug 2015 14:29:05 +0200 changeset 60855 6449ae4b85f9 parent 60854 8f45dd297357 child 60856 eb21ae05ec43
tuned;
```--- a/src/HOL/Library/Boolean_Algebra.thy	Thu Aug 06 14:28:59 2015 +0200
+++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Aug 06 14:29:05 2015 +0200
@@ -26,11 +26,11 @@
assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
begin

-sublocale conj!: abel_semigroup conj proof
-qed (fact conj_assoc conj_commute)+
+sublocale conj!: abel_semigroup conj
+  by standard (fact conj_assoc conj_commute)+

-sublocale disj!: abel_semigroup disj proof
-qed (fact disj_assoc disj_commute)+
+sublocale disj!: abel_semigroup disj
+  by standard (fact disj_assoc disj_commute)+

lemmas conj_left_commute = conj.left_commute

@@ -53,6 +53,7 @@
apply (rule conj_cancel_right)
done

+
subsection \<open>Complement\<close>

lemma complement_unique:
@@ -81,6 +82,7 @@
lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
by (rule inj_eq [OF inj_on_inverseI], rule double_compl)

+
subsection \<open>Conjunction\<close>

lemma conj_absorb [simp]: "x \<sqinter> x = x"
@@ -118,12 +120,13 @@
by (simp only: conj_assoc [symmetric] conj_absorb)

lemma conj_disj_distrib2:
-  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
+  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
by (simp only: conj_commute conj_disj_distrib)

lemmas conj_disj_distribs =
conj_disj_distrib conj_disj_distrib2

+
subsection \<open>Disjunction\<close>

lemma disj_absorb [simp]: "x \<squnion> x = x"
@@ -154,6 +157,7 @@
lemmas disj_conj_distribs =
disj_conj_distrib disj_conj_distrib2

+
subsection \<open>De Morgan's Laws\<close>

lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
@@ -178,14 +182,16 @@

end

+
subsection \<open>Symmetric Difference\<close>

locale boolean_xor = boolean +
-  fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
+  fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<oplus>" 65)
assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
begin

-sublocale xor!: abel_semigroup xor proof
+sublocale xor!: abel_semigroup xor
+proof
fix x y z :: 'a
let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
(\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
@@ -262,8 +268,7 @@
conj_disj_distribs conj_ac disj_ac)
qed

-lemma conj_xor_distrib2:
-  "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
+lemma conj_xor_distrib2: "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
proof -
have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
by (rule conj_xor_distrib)
@@ -271,8 +276,7 @@
by (simp only: conj_commute)
qed

-lemmas conj_xor_distribs =
-   conj_xor_distrib conj_xor_distrib2
+lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2

end
```