# HG changeset patch
# User wenzelm
# Date 1594924503 -7200
# Node ID 438adb97d82c29cf706134d92174a7085b16c07b
# Parent  b8bcdb88465173c46498420fb7265047c5a386e1# Parent  d4de7e4754d2ad5e8403aa0313b86d8d6e7f5ae6
merged

diff -r d4de7e4754d2 -r 438adb97d82c NEWS
--- a/NEWS	Thu Jul 16 20:34:21 2020 +0200
+++ b/NEWS	Thu Jul 16 20:35:03 2020 +0200
@@ -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.
diff -r d4de7e4754d2 -r 438adb97d82c src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Thu Jul 16 20:34:21 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Thu Jul 16 20:35:03 2020 +0200
@@ -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)
   
diff -r d4de7e4754d2 -r 438adb97d82c src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jul 16 20:34:21 2020 +0200
+++ b/src/HOL/Word/Word.thy	Thu Jul 16 20:35:03 2020 +0200
@@ -64,25 +64,6 @@
 definition unat :: "'a::len word \<Rightarrow> nat"
   where "unat w = nat (uint w)"
 
-definition uints :: "nat \<Rightarrow> int set"
-  \<comment> \<open>the sets of integers representing the words\<close>
-  where "uints n = range (bintrunc n)"
-
-definition sints :: "nat \<Rightarrow> int set"
-  where "sints n = range (sbintrunc (n - 1))"
-
-lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
-  by (simp add: uints_def range_bintrunc)
-
-lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
-  by (simp add: sints_def range_sbintrunc)
-
-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)"
@@ -182,6 +163,33 @@
 lemmas uint_lt = uint_bounded (* FIXME duplicate *)
 lemmas uint_mod_same = uint_idem (* FIXME duplicate *)
 
+definition uints :: "nat \<Rightarrow> int set"
+  \<comment> \<open>the sets of integers representing the words\<close>
+  where "uints n = range (bintrunc n)"
+
+definition sints :: "nat \<Rightarrow> int set"
+  where "sints n = range (sbintrunc (n - 1))"
+
+lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
+  by (simp add: uints_def range_bintrunc)
+
+lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
+  by (simp add: sints_def range_sbintrunc)
+
+definition unats :: "nat \<Rightarrow> nat set"
+  where "unats n = {i. i < 2 ^ n}"
+
+\<comment> \<open>naturals\<close>
+lemma uints_unats: "uints n = int ` unats n"
+  apply (unfold unats_def uints_num)
+  apply safe
+    apply (rule_tac image_eqI)
+     apply (erule_tac nat_0_le [symmetric])
+  by auto
+
+lemma unats_uints: "unats n = nat ` uints n"
+  by (auto simp: uints_unats image_iff)
+
 lemma td_ext_uint:
   "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
     (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
@@ -1486,17 +1494,6 @@
   for x :: "'a::len word"
   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
-\<comment> \<open>naturals\<close>
-lemma uints_unats: "uints n = int ` unats n"
-  apply (unfold unats_def uints_num)
-  apply safe
-    apply (rule_tac image_eqI)
-     apply (erule_tac nat_0_le [symmetric])
-  by auto
-
-lemma unats_uints: "unats n = nat ` uints n"
-  by (auto simp: uints_unats image_iff)
-
 lemmas bintr_num =
   word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
 lemmas sbintr_num =