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