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