# HG changeset patch
# User haftmann
# Date 1573456577 0
# Node ID 038727567817a16541e03c343372e2f398be03c7
# Parent  a197532693a5d003be7e3bdb2f1b98a46737130b
tuned order between theories

diff -r a197532693a5 -r 038727567817 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Sat Nov 09 15:39:21 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Mon Nov 11 07:16:17 2019 +0000
@@ -5,7 +5,7 @@
 
 theory Bit_Lists
   imports
-    Bit_Operations
+    Word
 begin
 
 subsection \<open>Fragments of algebraic bit representations\<close>
diff -r a197532693a5 -r 038727567817 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Sat Nov 09 15:39:21 2019 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Mon Nov 11 07:16:17 2019 +0000
@@ -6,7 +6,7 @@
 theory Bit_Operations
   imports
     "HOL-Library.Boolean_Algebra"
-    Word
+    Main
 begin
 
 subsection \<open>Bit operations in suitable algebraic structures\<close>
@@ -741,50 +741,4 @@
   apply simp
   done
 
-
-subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
-
-instantiation word :: (len) ring_bit_operations
-begin
-
-lift_definition not_word :: "'a word \<Rightarrow> 'a word"
-  is not
-  by (simp add: take_bit_not_iff)
-
-lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "and"
-  by simp
-
-lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is or
-  by simp
-
-lift_definition xor_word ::  "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is xor
-  by simp
-
-instance proof
-  interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
-  proof
-    show "a AND (b OR c) = a AND b OR a AND c"
-      for a b c :: "'a word"
-      by transfer (simp add: bit.conj_disj_distrib)
-    show "a OR b AND c = (a OR b) AND (a OR c)"
-      for a b c :: "'a word"
-      by transfer (simp add: bit.disj_conj_distrib)
-  qed (transfer; simp add: ac_simps)+
-  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
-    by (fact bit_word.boolean_algebra_axioms)
-  show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
-  proof (rule ext)+
-    fix a b :: "'a word"
-    have "a XOR b = a AND NOT b OR NOT a AND b"
-      by transfer (simp add: bit.xor_def)
-    then show "bit_word.xor a b = a XOR b"
-      by (simp add: bit_word.xor_def)
-  qed
-qed
-
 end
-
-end
diff -r a197532693a5 -r 038727567817 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sat Nov 09 15:39:21 2019 +0000
+++ b/src/HOL/ex/Word.thy	Mon Nov 11 07:16:17 2019 +0000
@@ -7,6 +7,7 @@
   imports
     Main
     "HOL-Library.Type_Length"
+    "HOL-ex.Bit_Operations"
 begin
 
 subsection \<open>Preliminaries\<close>
@@ -562,8 +563,6 @@
   qed
 qed
 
-subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
-
 instance word :: (len) semiring_bits
 proof
   show \<open>of_bool (odd a) + 2 * (a div 2) = a\<close>
@@ -601,9 +600,6 @@
   qed
 qed
 
-
-subsubsection \<open>Instance \<^typ>\<open>'a word\<close>\<close>
-
 instantiation word :: (len) semiring_bit_shifts
 begin
 
@@ -649,4 +645,47 @@
 
 end
 
+instantiation word :: (len) ring_bit_operations
+begin
+
+lift_definition not_word :: "'a word \<Rightarrow> 'a word"
+  is not
+  by (simp add: take_bit_not_iff)
+
+lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "and"
+  by simp
+
+lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is or
+  by simp
+
+lift_definition xor_word ::  "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is xor
+  by simp
+
+instance proof
+  interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
+  proof
+    show "a AND (b OR c) = a AND b OR a AND c"
+      for a b c :: "'a word"
+      by transfer (simp add: bit.conj_disj_distrib)
+    show "a OR b AND c = (a OR b) AND (a OR c)"
+      for a b c :: "'a word"
+      by transfer (simp add: bit.disj_conj_distrib)
+  qed (transfer; simp add: ac_simps)+
+  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
+    by (fact bit_word.boolean_algebra_axioms)
+  show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
+  proof (rule ext)+
+    fix a b :: "'a word"
+    have "a XOR b = a AND NOT b OR NOT a AND b"
+      by transfer (simp add: bit.xor_def)
+    then show "bit_word.xor a b = a XOR b"
+      by (simp add: bit_word.xor_def)
+  qed
+qed
+
 end
+
+end