--- a/NEWS Wed Jul 15 20:06:45 2020 +0200
+++ b/NEWS Thu Jul 16 04:52:25 2020 +0000
@@ -75,8 +75,8 @@
into its components "drop_bit" and "take_bit". INCOMPATIBILITY.
* Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
-"bintrunc", "sbintrunc", "bin_cat" and "max_word" are now mere
-input abbreviations. Minor INCOMPATIBILITY.
+"bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now
+mere input abbreviations. Minor INCOMPATIBILITY.
* Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
Minor INCOMPATIBILITY.
--- a/src/HOL/Word/Bits_Int.thy Wed Jul 15 20:06:45 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy Thu Jul 16 04:52:25 2020 +0000
@@ -246,6 +246,9 @@
abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>sbintrunc \<equiv> signed_take_bit\<close>
+abbreviation (input) norm_sint :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>norm_sint n \<equiv> signed_take_bit (n - 1)\<close>
+
lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n"
by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift)
--- a/src/HOL/Word/Word.thy Wed Jul 15 20:06:45 2020 +0200
+++ b/src/HOL/Word/Word.thy Thu Jul 16 04:52:25 2020 +0000
@@ -80,9 +80,6 @@
definition unats :: "nat \<Rightarrow> nat set"
where "unats n = {i. i < 2 ^ n}"
-definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int"
- where "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
-
definition scast :: "'a::len word \<Rightarrow> 'b::len word"
\<comment> \<open>cast a word to a different length\<close>
where "scast w = word_of_int (sint w)"