# HG changeset patch
# User haftmann
# Date 1599322876 0
# Node ID 5a6d8675bf4b72550e73a2b545205ee01d53a561
# Parent  bb88e31220af1301c9d05c1a79b01b5025133390
generalized signed_take_bit

diff -r bb88e31220af -r 5a6d8675bf4b src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Sat Sep 05 08:32:34 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Sat Sep 05 16:21:16 2020 +0000
@@ -552,6 +552,10 @@
 end
 
 
+lemma mask_half_int:
+  \<open>mask n div 2 = (mask (n - 1) :: int)\<close>
+  by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps)
+
 lemma mask_nonnegative_int [simp]:
   \<open>mask n \<ge> (0::int)\<close>
   by (simp add: mask_eq_exp_minus_1)
@@ -896,43 +900,55 @@
     (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def)  
 
 
-subsection \<open>Taking bit with sign propagation\<close>
+subsection \<open>Taking bits with sign propagation\<close>
 
-definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
+context ring_bit_operations
+begin
 
-lemma signed_take_bit_unfold:
-  \<open>signed_take_bit n k = take_bit n k OR (of_bool (bit k n) * NOT (mask n))\<close>
-  by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask)
+definition signed_take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>signed_take_bit n a = take_bit n a OR (of_bool (bit a n) * NOT (mask n))\<close>
 
-lemma signed_take_bit_eq:
-  \<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close>
+lemma signed_take_bit_eq_if_positive:
+  \<open>signed_take_bit n a = take_bit n a\<close> if \<open>\<not> bit a n\<close>
   using that by (simp add: signed_take_bit_def)
 
-lemma signed_take_bit_eq_or:
-  \<open>signed_take_bit n k = take_bit n k OR NOT (mask n)\<close> if \<open>bit k n\<close>
-  using that by (simp add: signed_take_bit_def concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask)
+lemma signed_take_bit_eq_if_negative:
+  \<open>signed_take_bit n a = take_bit n a OR NOT (mask n)\<close> if \<open>bit a n\<close>
+  using that by (simp add: signed_take_bit_def)
+
+lemma even_signed_take_bit_iff:
+  \<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
+  by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
+
+lemma bit_signed_take_bit_iff:
+  \<open>bit (signed_take_bit m a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit a (min m n)\<close>
+  by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le)
+    (use exp_eq_0_imp_not_bit in blast)
 
 lemma signed_take_bit_0 [simp]:
-  \<open>signed_take_bit 0 k = - (k mod 2)\<close>
+  \<open>signed_take_bit 0 a = - (a mod 2)\<close>
   by (simp add: signed_take_bit_def odd_iff_mod_2_eq_one)
 
-lemma mask_half_int:
-  \<open>mask n div 2 = (mask (n - 1) :: int)\<close>
-  by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps)
-
 lemma signed_take_bit_Suc:
-  \<open>signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)\<close>
-  by (unfold signed_take_bit_def or_int_rec [of \<open>take_bit (Suc n) k\<close>])
-    (simp add: bit_Suc concat_bit_Suc even_or_iff even_mask_iff odd_iff_mod_2_eq_one not_int_div_2 mask_half_int)
-
-lemma signed_take_bit_rec:
-  \<open>signed_take_bit n k = (if n = 0 then - (k mod 2) else k mod 2 + 2 * signed_take_bit (n - 1) (k div 2))\<close>
-  by (cases n) (simp_all add: signed_take_bit_Suc)
-
-lemma bit_signed_take_bit_iff:
-  \<open>bit (signed_take_bit m k) n = bit k (min m n)\<close>
-  by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def)
+  \<open>signed_take_bit (Suc n) a = a mod 2 + 2 * signed_take_bit n (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  show \<open>bit (signed_take_bit (Suc n) a) m \<longleftrightarrow>
+    bit (a mod 2 + 2 * signed_take_bit n (a div 2)) m\<close>
+  proof (cases m)
+    case 0
+    then show ?thesis
+      by (simp add: even_signed_take_bit_iff)
+  next
+    case (Suc m)
+    with * have \<open>2 ^ m \<noteq> 0\<close>
+      by (metis mult_not_zero power_Suc)
+    with Suc show ?thesis
+      by (simp add: bit_signed_take_bit_iff mod2_eq_if bit_double_iff even_bit_succ_iff
+        ac_simps flip: bit_Suc)
+  qed
+qed
 
 lemma signed_take_bit_of_0 [simp]:
   \<open>signed_take_bit n 0 = 0\<close>
@@ -940,36 +956,56 @@
 
 lemma signed_take_bit_of_minus_1 [simp]:
   \<open>signed_take_bit n (- 1) = - 1\<close>
-  by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask)
+  by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
 
-lemma signed_take_bit_signed_take_bit [simp]:
-  \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close>
-  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
+lemma signed_take_bit_Suc_1 [simp]:
+  \<open>signed_take_bit (Suc n) 1 = 1\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_rec:
+  \<open>signed_take_bit n a = (if n = 0 then - (a mod 2) else a mod 2 + 2 * signed_take_bit (n - 1) (a div 2))\<close>
+  by (cases n) (simp_all add: signed_take_bit_Suc)
 
 lemma signed_take_bit_eq_iff_take_bit_eq:
-  \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close>
-proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>)
-  case True
-  moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close>
-    for k :: int
-    by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask)
-  ultimately show ?thesis
-    by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq)
-next
-  case False
-  then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close>
-    by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
+  \<open>signed_take_bit n a = signed_take_bit n b \<longleftrightarrow> take_bit (Suc n) a = take_bit (Suc n) b\<close>
+proof -
+  have \<open>bit (signed_take_bit n a) = bit (signed_take_bit n b) \<longleftrightarrow> bit (take_bit (Suc n) a) = bit (take_bit (Suc n) b)\<close>
+    by (simp add: fun_eq_iff bit_signed_take_bit_iff bit_take_bit_iff not_le less_Suc_eq_le min_def)
+      (use exp_eq_0_imp_not_bit in fastforce)
   then show ?thesis
-    by simp
+    by (simp add: bit_eq_iff fun_eq_iff)
 qed
 
+lemma signed_take_bit_signed_take_bit [simp]:
+  \<open>signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a\<close>
+proof (rule bit_eqI)
+  fix q
+  show \<open>bit (signed_take_bit m (signed_take_bit n a)) q \<longleftrightarrow>
+    bit (signed_take_bit (min m n) a) q\<close>
+    by (simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
+      (use le_Suc_ex exp_add_not_zero_imp in blast)
+qed
+
+lemma signed_take_bit_take_bit:
+  \<open>signed_take_bit m (take_bit n a) = (if n \<le> m then take_bit n else signed_take_bit m) a\<close>
+  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
+
 lemma take_bit_signed_take_bit:
-  \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close>
+  \<open>take_bit m (signed_take_bit n a) = take_bit m a\<close> if \<open>m \<le> Suc n\<close>
   using that by (rule le_SucE; intro bit_eqI)
    (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
 
+end
+
+text \<open>Modulus centered around 0\<close>
+
+lemma signed_take_bit_eq_concat_bit:
+  \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
+  by (simp add: concat_bit_def signed_take_bit_def push_bit_minus_one_eq_not_mask)
+
 lemma signed_take_bit_add:
   \<open>signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\<close>
+  for k l :: int
 proof -
   have \<open>take_bit (Suc n)
      (take_bit (Suc n) (signed_take_bit n k) +
@@ -982,6 +1018,7 @@
 
 lemma signed_take_bit_diff:
   \<open>signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)\<close>
+  for k l :: int
 proof -
   have \<open>take_bit (Suc n)
      (take_bit (Suc n) (signed_take_bit n k) -
@@ -994,6 +1031,7 @@
 
 lemma signed_take_bit_minus:
   \<open>signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)\<close>
+  for k :: int
 proof -
   have \<open>take_bit (Suc n)
      (- take_bit (Suc n) (signed_take_bit n k)) =
@@ -1005,6 +1043,7 @@
 
 lemma signed_take_bit_mult:
   \<open>signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)\<close>
+  for k l :: int
 proof -
   have \<open>take_bit (Suc n)
      (take_bit (Suc n) (signed_take_bit n k) *
@@ -1015,10 +1054,9 @@
     by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult)
 qed
 
-text \<open>Modulus centered around 0\<close>
-
 lemma signed_take_bit_eq_take_bit_minus:
   \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close>
+  for k :: int
 proof (cases \<open>bit k n\<close>)
   case True
   have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
@@ -1029,13 +1067,13 @@
     by (simp flip: minus_exp_eq_not_mask)
 next
   case False
-  then show ?thesis
-    by (simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
-      (auto intro: bit_eqI simp add: less_Suc_eq)
+  show ?thesis
+    by (rule bit_eqI) (simp add: False bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq)
 qed
 
 lemma signed_take_bit_eq_take_bit_shift:
   \<open>signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
+  for k :: int
 proof -
   have *: \<open>take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\<close>
     by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff)
@@ -1055,87 +1093,80 @@
     by (rule disjunctive_add)
       (auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff)
   finally show ?thesis
-    using * **
-    by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
-      (simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps)
+    using * ** by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
 qed
 
-lemma signed_take_bit_take_bit:
-  \<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close>
-  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
-
 lemma signed_take_bit_nonnegative_iff [simp]:
   \<open>0 \<le> signed_take_bit n k \<longleftrightarrow> \<not> bit k n\<close>
+  for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
 lemma signed_take_bit_negative_iff [simp]:
   \<open>signed_take_bit n k < 0 \<longleftrightarrow> bit k n\<close>
+  for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
 lemma signed_take_bit_greater_eq:
   \<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
+  for k :: int
   using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
 lemma signed_take_bit_less_eq:
   \<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close>
+  for k :: int
   using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
 lemma signed_take_bit_eq_self:
   \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
+  for k :: int
   using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self)
 
-lemma signed_take_bit_Suc_1 [simp]:
-  \<open>signed_take_bit (Suc n) 1 = 1\<close>
-  by (simp add: signed_take_bit_Suc)
-
 lemma signed_take_bit_Suc_bit0 [simp]:
-  \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * 2\<close>
+  \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_Suc_bit1 [simp]:
-  \<open>signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + 1\<close>
+  \<open>signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_Suc_minus_bit0 [simp]:
-  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * 2\<close>
+  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_Suc_minus_bit1 [simp]:
-  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + 1\<close>
+  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_numeral_bit0 [simp]:
-  \<open>signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2\<close>
+  \<open>signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_numeral_bit1 [simp]:
-  \<open>signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
+  \<open>signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_numeral_minus_bit0 [simp]:
-  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * 2\<close>
+  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_numeral_minus_bit1 [simp]:
-  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + 1\<close>
+  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_code [code]:
-  \<open>signed_take_bit n k =
-  (let l = take_bit (Suc n) k
-   in if bit l n then l - (push_bit n 2) else l)\<close>
+  \<open>signed_take_bit n a =
+  (let l = take_bit (Suc n) a
+   in if bit l n then l + push_bit (Suc n) (- 1) else l)\<close>
 proof -
-  have *: \<open>take_bit (Suc n) k - 2 * 2 ^ n = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
-    apply (subst disjunctive_add [symmetric])
-    apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff bit_take_bit_iff)
-    apply (simp flip: minus_exp_eq_not_mask)
-    done
+  have *: \<open>take_bit (Suc n) a + push_bit n (- 2) =
+    take_bit (Suc n) a OR NOT (mask (Suc n))\<close>
+    by (auto simp add: bit_take_bit_iff bit_push_bit_iff bit_not_iff bit_mask_iff disjunctive_add
+       simp flip: push_bit_minus_one_eq_not_mask)
   show ?thesis
     by (rule bit_eqI)
-     (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le
-       bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_take_bit_iff bit_not_iff)
+      (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
 qed
 
 
@@ -1358,9 +1389,9 @@
 
       \<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
 
-      \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]}
+      \<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
 
-      \<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
+      \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]}
 
       \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 \<close>
diff -r bb88e31220af -r 5a6d8675bf4b src/HOL/Word/Ancient_Numeral.thy
--- a/src/HOL/Word/Ancient_Numeral.thy	Sat Sep 05 08:32:34 2020 +0000
+++ b/src/HOL/Word/Ancient_Numeral.thy	Sat Sep 05 16:21:16 2020 +0000
@@ -163,14 +163,14 @@
   by (cases n) auto
 
 lemmas sbintrunc_Suc_BIT [simp] =
-  signed_take_bit_Suc [where k="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
+  signed_take_bit_Suc [where a="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
 
 lemmas sbintrunc_0_BIT_B0 [simp] =
-  signed_take_bit_0 [where k="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   for w
 
 lemmas sbintrunc_0_BIT_B1 [simp] =
-  signed_take_bit_0 [where k="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
   for w
 
 lemma sbintrunc_Suc_minus_Is:
diff -r bb88e31220af -r 5a6d8675bf4b src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Sat Sep 05 08:32:34 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Sat Sep 05 16:21:16 2020 +0000
@@ -227,19 +227,19 @@
   by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2)
 
 lemmas sbintrunc_Suc_Pls =
-  signed_take_bit_Suc [where k="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_Suc [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Suc_Min =
-  signed_take_bit_Suc [where k="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_Suc [where a="-1::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min
   sbintrunc_Suc_numeral
 
 lemmas sbintrunc_Pls =
-  signed_take_bit_0 [where k="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Min =
-  signed_take_bit_0 [where k="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="-1::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_0_simps =
   sbintrunc_Pls sbintrunc_Min
diff -r bb88e31220af -r 5a6d8675bf4b src/HOL/Word/Conversions.thy
--- a/src/HOL/Word/Conversions.thy	Sat Sep 05 08:32:34 2020 +0000
+++ b/src/HOL/Word/Conversions.thy	Sat Sep 05 16:21:16 2020 +0000
@@ -214,8 +214,8 @@
 
 lemma signed_1 [simp]:
   \<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\<close>
-  by (transfer fixing: uminus)
-    (simp_all add: signed_take_bit_eq not_le Suc_lessI)
+  by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>)
+    (simp_all add: sbintrunc_minus_simps)
 
 lemma signed_minus_1 [simp]:
   \<open>signed (- 1 :: 'b::len word) = - 1\<close>
@@ -242,7 +242,8 @@
 lemma bit_signed_iff:
   \<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
   for w :: \<open>'b::len word\<close>
-  by (transfer fixing: bit) (auto simp add: bit_of_int_iff bit_signed_take_bit_iff min_def)
+  by (transfer fixing: bit)
+    (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
 
 lemma signed_push_bit_eq:
   \<open>signed (push_bit n w) = take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w))
@@ -274,7 +275,7 @@
   \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
   for w :: \<open>'b::len word\<close>
   by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
-    (auto simp add: signed_take_bit_take_bit take_bit_signed_take_bit take_bit_of_int min_def)
+    (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
 
 lemma signed_not_eq:
   \<open>signed (NOT w) = take_bit LENGTH('b) (NOT (signed w)) OR of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))\<close>
@@ -447,21 +448,34 @@
 lemma sint_not_eq:
   \<open>sint (NOT w) = signed_take_bit LENGTH('a) (NOT (sint w))\<close>
   for w :: \<open>'a::len word\<close>
-  by (simp add: signed_not_eq signed_take_bit_unfold)
+  by (simp add: signed_not_eq signed_take_bit_def)
 
 lemma sint_push_bit_eq:
   \<open>signed (push_bit n w) = signed_take_bit (LENGTH('a) - Suc 0) (push_bit n (signed w))\<close>
   for w :: \<open>'a::len word\<close>
-  by (transfer fixing: n; cases \<open>LENGTH('a)\<close>)
-     (auto simp add: signed_take_bit_def bit_concat_bit_iff bit_push_bit_iff bit_take_bit_iff bit_or_iff le_diff_conv2,
-        auto simp add: take_bit_push_bit not_less concat_bit_eq_iff take_bit_concat_bit_eq le_diff_conv2)
+  apply (transfer fixing: n; cases \<open>LENGTH('a)\<close>)
+   apply simp_all
+  apply (rule bit_eqI)
+  apply (simp add: bit_of_int_iff bit_signed_take_bit_iff bit_push_bit_iff min_def not_le le_diff_conv2)
+  apply auto
+           apply (metis le_add_diff_inverse mult_zero_left power_add)
+          apply (metis (no_types, lifting) diff_le_self le_add_diff_inverse mult_zero_left power_add)
+  using diff_diff_cancel apply fastforce
+  using diff_diff_cancel apply fastforce
+  apply (metis add_diff_cancel_right' diff_commute diff_le_self le_antisym less_imp_add_positive)
+      apply (metis le_add_diff_inverse mult_zero_left power_add)
+          apply (metis (no_types, lifting) diff_le_self le_add_diff_inverse mult_zero_left power_add)
+    apply (metis add.commute le_Suc_ex mult_zero_right power_add)
+   apply (metis le_add_diff_inverse mult_zero_left mult_zero_right power_add)
+  apply (metis le_add_diff_inverse mult_zero_right power_add)
+  done
 
 lemma sint_greater_eq:
   \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
 proof (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>)
   case True
   then show ?thesis
-    by transfer (simp add: signed_take_bit_eq_or minus_exp_eq_not_mask or_greater_eq ac_simps)
+    by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps)
 next
   have *: \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> (0::int)\<close>
     by simp
@@ -473,7 +487,7 @@
 lemma sint_less:
   \<open>sint w < 2 ^ (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
   by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
-    (simp_all add: signed_take_bit_eq signed_take_bit_unfold take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
+    (simp_all add: signed_take_bit_eq signed_take_bit_def take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
 
 context semiring_1
 begin
diff -r bb88e31220af -r 5a6d8675bf4b src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Sep 05 08:32:34 2020 +0000
+++ b/src/HOL/Word/Word.thy	Sat Sep 05 16:21:16 2020 +0000
@@ -1281,7 +1281,7 @@
 lemma sshiftr_eq:
   \<open>w >>> n = (sshiftr1 ^^ n) w\<close>
 proof -
-  have *: \<open>(\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n =
+  have *: \<open>(\<lambda>k::int. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n =
     take_bit LENGTH('a) \<circ> drop_bit (Suc n) \<circ> signed_take_bit (LENGTH('a) - Suc 0)\<close>
     for n
     apply (induction n)
@@ -1804,7 +1804,7 @@
   unfolding bintr_num by (erule subst, simp)
 
 lemma num_of_sbintr':
-  "signed_take_bit (LENGTH('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
+  "signed_take_bit (LENGTH('a::len) - 1) (numeral a :: int) = (numeral b) \<Longrightarrow>
     numeral a = (numeral b :: 'a word)"
   unfolding sbintr_num by (erule subst, simp)
 
@@ -3404,7 +3404,8 @@
 
 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
   apply transfer
-  apply (auto simp add: bit_eq_iff bit_signed_take_bit_iff bit_drop_bit_eq min_def simp flip: drop_bit_eq_div)
+  apply (rule bit_eqI)
+  apply (simp add: bit_signed_take_bit_iff bit_drop_bit_eq min_def flip: drop_bit_eq_div)
   done
 
 lemma bit_bshiftr1_iff: