diff -r d488d643e677 -r 5193570b739a src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy	Thu Sep 17 09:57:30 2020 +0000
@@ -1106,23 +1106,45 @@
   for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
-lemma signed_take_bit_greater_eq:
+lemma signed_take_bit_int_eq_self_iff:
+  \<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
+  for k :: int
+  by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_less_eq_self_iff:
+  \<open>signed_take_bit n k \<le> k \<longleftrightarrow> - (2 ^ n) \<le> k\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_eq_self_iff algebra_simps)
+    linarith
+
+lemma signed_take_bit_int_less_self_iff:
+  \<open>signed_take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_self_iff:
+  \<open>k < signed_take_bit n k \<longleftrightarrow> k < - (2 ^ n)\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_self_iff algebra_simps)
+    linarith
+
+lemma signed_take_bit_int_greater_eq_self_iff:
+  \<open>k \<le> signed_take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_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:
+lemma signed_take_bit_int_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_bit0 [simp]:
   \<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)