diff -r 7b112eedc859 -r 587d4681240c src/HOL/Word/Bits_Int.thy
--- 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)