# HG changeset patch
# User haftmann
# Date 1555783341 0
# Node ID 2082287357e694e8c7a098820a0fe5dca8fb23a1
# Parent  18e94864fd0f22bdb9bef5a8c017a43522489853
avoid separate type class for mere definitional extension

diff -r 18e94864fd0f -r 2082287357e6 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Sat Apr 20 18:02:20 2019 +0000
+++ b/src/HOL/Library/Boolean_Algebra.thy	Sat Apr 20 18:02:21 2019 +0000
@@ -191,15 +191,11 @@
 lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
   by (rule boolean_algebra.de_Morgan_conj [OF dual])
 
-end
-
 
 subsection \<open>Symmetric Difference\<close>
 
-locale boolean_algebra_xor = boolean_algebra +
-  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
+definition xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<oplus>" 65)
+  where "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
 
 sublocale xor: abel_semigroup xor
 proof
diff -r 18e94864fd0f -r 2082287357e6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Apr 20 18:02:20 2019 +0000
+++ b/src/HOL/Word/Word.thy	Sat Apr 20 18:02:21 2019 +0000
@@ -4202,34 +4202,28 @@
 lemma word_or_not [simp]: "x OR NOT x = max_word"
   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
-lemma word_boolean_algebra: "boolean_algebra (AND) (OR) bitNOT 0 max_word"
-  apply (rule boolean_algebra.intro)
-           apply (rule word_bw_assocs)
-          apply (rule word_bw_assocs)
-         apply (rule word_bw_comms)
-        apply (rule word_bw_comms)
-       apply (rule word_ao_dist2)
-      apply (rule word_oa_dist2)
-     apply (rule word_and_max)
-    apply (rule word_log_esimps)
-   apply (rule word_and_not)
-  apply (rule word_or_not)
-  done
-
-interpretation word_bool_alg: boolean_algebra "(AND)" "(OR)" bitNOT 0 max_word
-  by (rule word_boolean_algebra)
+global_interpretation word_bool_alg: boolean_algebra
+  where conj = "(AND)" and disj = "(OR)" and compl = bitNOT
+    and zero = 0 and one = max_word
+  rewrites "word_bool_alg.xor = (XOR)"
+proof -
+  interpret boolean_algebra
+    where conj = "(AND)" and disj = "(OR)" and compl = bitNOT
+      and zero = 0 and one = max_word
+    apply standard
+             apply (simp_all add: word_bw_assocs word_bw_comms word_bw_lcs)
+     apply (fact word_ao_dist2)
+    apply (fact word_oa_dist2)
+    done
+  show "boolean_algebra (AND) (OR) bitNOT 0 max_word" ..
+  show "xor = (XOR)"
+    by (auto simp add: fun_eq_iff word_eq_iff xor_def word_ops_nth_size word_size)
+qed
 
 lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
   for x y :: "'a::len0 word"
   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
-interpretation word_bool_alg: boolean_algebra_xor "(AND)" "(OR)" bitNOT 0 max_word "(XOR)"
-  apply (rule boolean_algebra_xor.intro)
-   apply (rule word_boolean_algebra)
-  apply (rule boolean_algebra_xor_axioms.intro)
-  apply (rule word_xor_and_or)
-  done
-
 lemma shiftr_x_0 [iff]: "x >> 0 = x"
   for x :: "'a::len0 word"
   by (simp add: shiftr_bl)