yet another alias
authorhaftmann
Thu, 16 Jul 2020 04:52:25 +0000
changeset 72272 587d4681240c
parent 72271 7b112eedc859
child 72273 b8bcdb884651
yet another alias
NEWS
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Word.thy
--- 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)"