# HG changeset patch
# User haftmann
# Date 1555925635 0
# Node ID bdc835d934b78d991eaca13a5c4166cf0d5cc4f2
# Parent  ff9efdc84289bc682df25f3007354bbf7731a214
no need to maintain two separate type classes

diff -r ff9efdc84289 -r bdc835d934b7 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Mon Apr 22 06:28:17 2019 +0000
+++ b/src/HOL/Word/Bits.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -2,17 +2,24 @@
     Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
 *)
 
-section \<open>Syntactic classes for bitwise operations\<close>
+section \<open>Syntactic type classes for bit operations\<close>
 
 theory Bits
   imports Main
 begin
 
-class bit =
+class bit_operations =
   fixes bitNOT :: "'a \<Rightarrow> 'a"  ("NOT _" [70] 71)
     and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
     and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
     and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
+    and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
+    and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
+  fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
+    and lsb :: "'a \<Rightarrow> bool"
+    and msb :: "'a \<Rightarrow> bool"
+    and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
+    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
 
 text \<open>
   We want the bitwise operations to bind slightly weaker
@@ -20,13 +27,4 @@
   bind slightly stronger than \<open>*\<close>.
 \<close>
 
-class bits = bit +
-  fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
-    and lsb :: "'a \<Rightarrow> bool"
-    and msb :: "'a \<Rightarrow> bool"
-    and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
-    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
-    and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
-    and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
-
 end
diff -r ff9efdc84289 -r bdc835d934b7 src/HOL/Word/Bits_Bit.thy
--- a/src/HOL/Word/Bits_Bit.thy	Mon Apr 22 06:28:17 2019 +0000
+++ b/src/HOL/Word/Bits_Bit.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -8,7 +8,7 @@
   imports Bits "HOL-Library.Bit"
 begin
 
-instantiation bit :: bit
+instantiation bit :: bit_operations
 begin
 
 primrec bitNOT_bit
diff -r ff9efdc84289 -r bdc835d934b7 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Mon Apr 22 06:28:17 2019 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -1185,9 +1185,86 @@
 
 subsection \<open>Logical operations\<close>
 
-text "bit-wise logical operations on the int type"
-
-instantiation int :: bit
+primrec bin_sc :: "nat \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> int"
+  where
+    Z: "bin_sc 0 b w = bin_rest w BIT b"
+  | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
+
+lemma bin_nth_sc [simp]: "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
+  by (induct n arbitrary: w) auto
+
+lemma bin_sc_sc_same [simp]: "bin_sc n c (bin_sc n b w) = bin_sc n c w"
+  by (induct n arbitrary: w) auto
+
+lemma bin_sc_sc_diff: "m \<noteq> n \<Longrightarrow> bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
+  apply (induct n arbitrary: w m)
+   apply (case_tac [!] m)
+     apply auto
+  done
+
+lemma bin_nth_sc_gen: "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
+  by (induct n arbitrary: w m) (case_tac [!] m, auto)
+
+lemma bin_sc_nth [simp]: "bin_sc n (bin_nth w n) w = w"
+  by (induct n arbitrary: w) auto
+
+lemma bin_sign_sc [simp]: "bin_sign (bin_sc n b w) = bin_sign w"
+  by (induct n arbitrary: w) auto
+
+lemma bin_sc_bintr [simp]: "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
+  apply (induct n arbitrary: w m)
+   apply (case_tac [!] w rule: bin_exhaust)
+   apply (case_tac [!] m, auto)
+  done
+
+lemma bin_clr_le: "bin_sc n False w \<le> w"
+  apply (induct n arbitrary: w)
+   apply (case_tac [!] w rule: bin_exhaust)
+   apply (auto simp: le_Bits)
+  done
+
+lemma bin_set_ge: "bin_sc n True w \<ge> w"
+  apply (induct n arbitrary: w)
+   apply (case_tac [!] w rule: bin_exhaust)
+   apply (auto simp: le_Bits)
+  done
+
+lemma bintr_bin_clr_le: "bintrunc n (bin_sc m False w) \<le> bintrunc n w"
+  apply (induct n arbitrary: w m)
+   apply simp
+  apply (case_tac w rule: bin_exhaust)
+  apply (case_tac m)
+   apply (auto simp: le_Bits)
+  done
+
+lemma bintr_bin_set_ge: "bintrunc n (bin_sc m True w) \<ge> bintrunc n w"
+  apply (induct n arbitrary: w m)
+   apply simp
+  apply (case_tac w rule: bin_exhaust)
+  apply (case_tac m)
+   apply (auto simp: le_Bits)
+  done
+
+lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
+  by (induct n) auto
+
+lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
+  by (induct n) auto
+
+lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
+
+lemma bin_sc_minus: "0 < n \<Longrightarrow> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
+  by auto
+
+lemmas bin_sc_Suc_minus =
+  trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
+
+lemma bin_sc_numeral [simp]:
+  "bin_sc (numeral k) b w =
+    bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
+  by (simp add: numeral_eq_Suc)
+
+instantiation int :: bit_operations
 begin
 
 definition int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)"
@@ -1207,10 +1284,33 @@
 
 definition int_xor_def: "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
 
+definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
+
+definition "lsb i = i !! 0" for i :: int
+
+definition "set_bit i n b = bin_sc n b i"
+
+definition
+  "set_bits f =
+    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+      in bl_to_bin (rev (map f [0..<n]))
+     else if \<exists>n. \<forall>n'\<ge>n. f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. f n'
+      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+     else 0 :: int)"
+
+definition "shiftl x n = x * 2 ^ n" for x :: int
+
+definition "shiftr x n = x div 2 ^ n" for x :: int
+
+definition "msb x \<longleftrightarrow> x < 0" for x :: int
+
 instance ..
 
 end
 
+
 subsubsection \<open>Basic simplification rules\<close>
 
 lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
@@ -1871,113 +1971,7 @@
 
 subsection \<open>Setting and clearing bits\<close>
 
-primrec bin_sc :: "nat \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> int"
-  where
-    Z: "bin_sc 0 b w = bin_rest w BIT b"
-  | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
-
-lemma bin_nth_sc [simp]: "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
-  by (induct n arbitrary: w) auto
-
-lemma bin_sc_sc_same [simp]: "bin_sc n c (bin_sc n b w) = bin_sc n c w"
-  by (induct n arbitrary: w) auto
-
-lemma bin_sc_sc_diff: "m \<noteq> n \<Longrightarrow> bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
-  apply (induct n arbitrary: w m)
-   apply (case_tac [!] m)
-     apply auto
-  done
-
-lemma bin_nth_sc_gen: "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
-  by (induct n arbitrary: w m) (case_tac [!] m, auto)
-
-lemma bin_sc_nth [simp]: "bin_sc n (bin_nth w n) w = w"
-  by (induct n arbitrary: w) auto
-
-lemma bin_sign_sc [simp]: "bin_sign (bin_sc n b w) = bin_sign w"
-  by (induct n arbitrary: w) auto
-
-lemma bin_sc_bintr [simp]: "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
-  apply (induct n arbitrary: w m)
-   apply (case_tac [!] w rule: bin_exhaust)
-   apply (case_tac [!] m, auto)
-  done
-
-lemma bin_clr_le: "bin_sc n False w \<le> w"
-  apply (induct n arbitrary: w)
-   apply (case_tac [!] w rule: bin_exhaust)
-   apply (auto simp: le_Bits)
-  done
-
-lemma bin_set_ge: "bin_sc n True w \<ge> w"
-  apply (induct n arbitrary: w)
-   apply (case_tac [!] w rule: bin_exhaust)
-   apply (auto simp: le_Bits)
-  done
-
-lemma bintr_bin_clr_le: "bintrunc n (bin_sc m False w) \<le> bintrunc n w"
-  apply (induct n arbitrary: w m)
-   apply simp
-  apply (case_tac w rule: bin_exhaust)
-  apply (case_tac m)
-   apply (auto simp: le_Bits)
-  done
-
-lemma bintr_bin_set_ge: "bintrunc n (bin_sc m True w) \<ge> bintrunc n w"
-  apply (induct n arbitrary: w m)
-   apply simp
-  apply (case_tac w rule: bin_exhaust)
-  apply (case_tac m)
-   apply (auto simp: le_Bits)
-  done
-
-lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
-  by (induct n) auto
-
-lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
-  by (induct n) auto
-
-lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
-
-lemma bin_sc_minus: "0 < n \<Longrightarrow> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
-  by auto
-
-lemmas bin_sc_Suc_minus =
-  trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
-
-lemma bin_sc_numeral [simp]:
-  "bin_sc (numeral k) b w =
-    bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
-  by (simp add: numeral_eq_Suc)
-
-instantiation int :: bits
-begin
-
-definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
-
-definition "lsb i = i !! 0" for i :: int
-
-definition "set_bit i n b = bin_sc n b i"
-
-definition
-  "set_bits f =
-    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-      in bl_to_bin (rev (map f [0..<n]))
-     else if \<exists>n. \<forall>n'\<ge>n. f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. f n'
-      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
-     else 0 :: int)"
-
-definition "shiftl x n = x * 2 ^ n" for x :: int
-
-definition "shiftr x n = x div 2 ^ n" for x :: int
-
-definition "msb x \<longleftrightarrow> x < 0" for x :: int
-
-instance ..
-
-end
+
 
 lemma int_lsb_BIT [simp]: fixes x :: int shows
   "lsb (x BIT b) \<longleftrightarrow> b"
diff -r ff9efdc84289 -r bdc835d934b7 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Apr 22 06:28:17 2019 +0000
+++ b/src/HOL/Word/Word.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -358,7 +358,14 @@
 
 subsection \<open>Bit-wise operations\<close>
 
-instantiation word :: (len0) bits
+definition shiftl1 :: "'a::len0 word \<Rightarrow> 'a word"
+  where "shiftl1 w = word_of_int (uint w BIT False)"
+
+definition shiftr1 :: "'a::len0 word \<Rightarrow> 'a word"
+  \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
+  where "shiftr1 w = word_of_int (bin_rest (uint w))"
+
+instantiation word :: (len0) bit_operations
 begin
 
 lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT
@@ -383,13 +390,6 @@
 
 definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
 
-definition shiftl1 :: "'a word \<Rightarrow> 'a word"
-  where "shiftl1 w = word_of_int (uint w BIT False)"
-
-definition shiftr1 :: "'a word \<Rightarrow> 'a word"
-  \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
-  where "shiftr1 w = word_of_int (bin_rest (uint w))"
-
 definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
 
 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w"