# HG changeset patch
# User haftmann
# Date 1587017369 -7200
# Node ID 02c50bba930442f391c007f0ad8a31573a01640a
# Parent  3d1f72d25fc33855dbedc84c1c3cf6e9597f4c00
bit on numerals

diff -r 3d1f72d25fc3 -r 02c50bba9304 src/HOL/Divides.thy
--- 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
diff -r 3d1f72d25fc3 -r 02c50bba9304 src/HOL/Parity.thy
--- 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]: