--- a/NEWS Tue Apr 16 19:50:19 2019 +0000
+++ b/NEWS Tue Apr 16 19:50:20 2019 +0000
@@ -287,6 +287,7 @@
* Session HOL-Word:
* New theory More_Word as comprehensive entrance point.
+ * Merged type class bitss into type class bits.
INCOMPATIBILITY.
--- a/src/HOL/Word/Bits.thy Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Bits.thy Tue Apr 16 19:50:20 2019 +0000
@@ -25,12 +25,10 @@
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)
-class bitss = bits +
- fixes msb :: "'a \<Rightarrow> bool"
-
end
--- a/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:20 2019 +0000
@@ -746,7 +746,7 @@
bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
by (simp add: numeral_eq_Suc)
-instantiation int :: bitss
+instantiation int :: bits
begin
definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
--- a/src/HOL/Word/Word.thy Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Word.thy Tue Apr 16 19:50:20 2019 +0000
@@ -62,7 +62,7 @@
definition sint :: "'a::len word \<Rightarrow> int"
\<comment> \<open>treats the most-significant-bit as a sign bit\<close>
- where sint_uint: "sint w = sbintrunc (len_of TYPE('a) - 1) (uint w)"
+ where sint_uint: "sint w = sbintrunc (LENGTH('a) - 1) (uint w)"
definition unat :: "'a::len0 word \<Rightarrow> nat"
where "unat w = nat (uint w)"
@@ -377,10 +377,12 @@
definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
-definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE('a)) f)"
+definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
+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)"
@@ -396,6 +398,10 @@
end
+lemma word_msb_def:
+ "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
+ by (simp add: msb_word_def sint_uint)
+
lemma [code]:
shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))"
and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
@@ -403,15 +409,6 @@
and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def)
-instantiation word :: (len) bitss
-begin
-
-definition word_msb_def: "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
-
-instance ..
-
-end
-
definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
where "setBit w n = set_bit w n True"