--- 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