src/HOL/Parity.thy

 
 lemma drop_bit_of_bool [simp]:
   "drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)"
   by (cases n) simp_all
 
-lemma take_bit_eq_0_imp_dvd:
-  "take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a"
-  by (simp add: take_bit_eq_mod mod_0_imp_dvd)
-
 lemma even_take_bit_eq [simp]:
   \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
   by (simp add: take_bit_rec [of n a])
 
 lemma take_bit_take_bit [simp]:

   assume \<open>2 ^ m \<noteq> 0\<close>
   with that show \<open>bit (take_bit n a) m \<longleftrightarrow> bit (if even a then 0 else 2 ^ n - 1) m\<close>
     by (simp add: bit_take_bit_iff bit_mask_iff stable_imp_bit_iff_odd)
 qed
 
+lemma exp_dvdE:
+  assumes \<open>2 ^ n dvd a\<close>
+  obtains b where \<open>a = push_bit n b\<close>
+proof -
+  from assms obtain b where \<open>a = 2 ^ n * b\<close> ..
+  then have \<open>a = push_bit n b\<close>
+    by (simp add: push_bit_eq_mult ac_simps)
+  with that show thesis .
+qed
+
+lemma take_bit_eq_0_iff:
+  \<open>take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?P
+  then show ?Q
+	  by (simp add: take_bit_eq_mod mod_0_imp_dvd)
+next
+  assume ?Q
+  then obtain b where \<open>a = push_bit n b\<close>
+    by (rule exp_dvdE)
+  then show ?P
+    by (simp add: take_bit_push_bit)
+qed
+
 end
 
 instantiation nat :: semiring_bit_shifts
 begin
 

   by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
 
 lemma take_bit_add:
   "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
   by (simp add: take_bit_eq_mod mod_simps)
-
-lemma take_bit_eq_0_iff:
-  "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a"
-  by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd)
 
 lemma take_bit_of_1_eq_0_iff [simp]:
   "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
   by (simp add: take_bit_eq_mod)