--- a/src/HOL/Bit_Operations.thy Thu Feb 17 19:42:15 2022 +0000
+++ b/src/HOL/Bit_Operations.thy Thu Feb 17 19:42:15 2022 +0000
@@ -2645,6 +2645,10 @@
unique_euclidean_semiring_with_nat + semiring_bit_operations
begin
+lemma possible_bit [simp]:
+ \<open>possible_bit TYPE('a) n\<close>
+ by (simp add: possible_bit_def)
+
lemma take_bit_of_exp [simp]:
\<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
by (simp add: take_bit_eq_mod exp_mod_exp)
@@ -2716,6 +2720,10 @@
by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
qed
+lemma drop_bit_mask_eq:
+ \<open>drop_bit m (mask n) = mask (n - m)\<close>
+ by (rule bit_eqI) (auto simp add: bit_simps possible_bit_def)
+
lemma drop_bit_of_nat:
"drop_bit n (of_nat m) = of_nat (drop_bit n m)"
by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div [of m "2 ^ n"])