# HG changeset patch
# User haftmann
# Date 1645126935 0
# Node ID 4cc719621825ff87e140a529bbf63346e30cae6b
# Parent  ccc3a72210e619353641abd48d577893cd3a0121
more lemmas for distribution

diff -r ccc3a72210e6 -r 4cc719621825 src/HOL/Bit_Operations.thy
--- 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"])