bit on numerals

--- a/src/HOL/Divides.thy	Thu Apr 16 08:09:29 2020 +0200
+++ b/src/HOL/Divides.thy	Thu Apr 16 08:09:29 2020 +0200
@@ -1130,6 +1130,14 @@
   \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
   by (cases m) simp_all
 
+lemma bit_numeral_Bit0_Suc_iff [simp]:
+  \<open>bit (numeral (Num.Bit0 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
+  by (simp add: bit_Suc)
+
+lemma bit_numeral_Bit1_Suc_iff [simp]:
+  \<open>bit (numeral (Num.Bit1 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
+  by (simp add: bit_Suc)
+
 lemma div_positive_int:
   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
   using that div_positive [of l k] by blast

--- a/src/HOL/Parity.thy	Thu Apr 16 08:09:29 2020 +0200
+++ b/src/HOL/Parity.thy	Thu Apr 16 08:09:29 2020 +0200
@@ -938,6 +938,10 @@
   \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
   by (simp add: bit_def even_mask_div_iff not_le)
 
+lemma bit_Numeral1_iff [simp]:
+  \<open>bit (numeral Num.One) n \<longleftrightarrow> n = 0\<close>
+  by (simp add: bit_rec)
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]: