--- a/src/HOL/Bit_Operations.thy Sun Oct 10 18:16:57 2021 +0000
+++ b/src/HOL/Bit_Operations.thy Mon Oct 11 06:32:09 2021 +0000
@@ -1412,6 +1412,14 @@
\<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
by (simp only: numeral_eq_Suc push_bit_Suc_minus_numeral)
+lemma take_bit_Suc_1:
+ \<open>take_bit (Suc n) (- 1) = 2 ^ Suc n - 1\<close>
+ by (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
+
+lemma take_bit_numeral_1 [simp]:
+ \<open>take_bit (numeral k) (- 1) = 2 ^ numeral k - 1\<close>
+ by (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
+
end