--- 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)