src/HOL/Parity.thy

   by (simp add: bit_iff_odd 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)
+
+lemma exp_add_not_zero_imp:
+  \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+  have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+  proof (rule notI)
+    assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+    then have \<open>2 ^ (m + n) = 0\<close>
+      by (rule disjE) (simp_all add: power_add)
+    with that show False ..
+  qed
+  then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+    by simp_all
+qed
 
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
   "P n" if zero: "P 0"

       by (simp add: algebra_simps)
     finally show ?case
       using odd by simp
   qed
 qed
+
+context semiring_bits
+begin
+
+lemma even_of_nat_iff:
+  \<open>even (of_nat n) \<longleftrightarrow> even n\<close>
+  by (induction n rule: nat_bit_induct) simp_all
+
+lemma bit_of_nat_iff:
+  \<open>bit (of_nat m) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit m n\<close>
+proof (cases \<open>(2::'a) ^ n = 0\<close>)
+  case True
+  then show ?thesis
+    by (simp add: exp_eq_0_imp_not_bit)
+next
+  case False
+  then have \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
+  proof (induction m arbitrary: n rule: nat_bit_induct)
+    case zero
+    then show ?case
+      by simp
+  next
+    case (even m)
+    then show ?case
+      by (cases n)
+        (auto simp add: bit_double_iff Parity.bit_double_iff dest: mult_not_zero)
+  next
+    case (odd m)
+    then show ?case
+      by (cases n)
+         (auto simp add: bit_double_iff even_bit_succ_iff Parity.bit_Suc dest: mult_not_zero)
+  qed
+  with False show ?thesis
+    by simp
+qed
+
+end
 
 instantiation int :: semiring_bits
 begin
 
 definition bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>

 instance
   by standard (simp_all add: push_bit_nat_def drop_bit_nat_def take_bit_nat_def)
 
 end
 
+context semiring_bit_shifts
+begin
+
+lemma push_bit_of_nat:
+  \<open>push_bit n (of_nat m) = of_nat (push_bit n m)\<close>
+  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma of_nat_push_bit:
+  \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
+  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma take_bit_of_nat:
+  \<open>take_bit n (of_nat m) = of_nat (take_bit n m)\<close>
+  by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_nat_iff)
+
+lemma of_nat_take_bit:
+  \<open>of_nat (take_bit n m) = take_bit n (of_nat m)\<close>
+  by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_nat_iff)
+
+end
+
 instantiation int :: semiring_bit_shifts
 begin
 
 definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>push_bit_int n k = k * 2 ^ n\<close>

 
 lemma push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)
 
-lemma push_bit_of_nat:
-  "push_bit n (of_nat m) = of_nat (push_bit n m)"
-  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_of_1_eq_0_iff [simp]:

   by (simp add: take_bit_rec numeral_Bit0_div_2)
 
 lemma take_bit_numeral_bit1 [simp]:
   \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
   by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
-
-lemma take_bit_of_nat:
-  "take_bit n (of_nat m) = of_nat (take_bit n m)"
-  by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
 
 lemma drop_bit_Suc_bit0 [simp]:
   \<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
   by (simp add: drop_bit_Suc numeral_Bit0_div_2)
 

     by (simp add: of_nat_div)
   finally show ?thesis
     by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
 qed
 
-lemma of_nat_push_bit:
-  \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
-  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
-
 lemma of_nat_drop_bit:
   \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
   by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
 
-lemma of_nat_take_bit:
-  \<open>of_nat (take_bit m n) = take_bit m (of_nat n)\<close>
-  by (simp add: take_bit_eq_mod semiring_bit_shifts_class.take_bit_eq_mod of_nat_mod)
-
 lemma bit_push_bit_iff_of_nat_iff:
   \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
   by (auto simp add: bit_push_bit_iff)
 
 end
 
 instance nat :: unique_euclidean_semiring_with_bit_shifts ..
 
 instance int :: unique_euclidean_semiring_with_bit_shifts ..
 
-lemma bit_nat_iff [simp]:
-  \<open>bit (nat k) n \<longleftrightarrow> k > 0 \<and> bit k n\<close>
-proof (cases \<open>k > 0\<close>)
+lemma bit_nat_iff:
+  \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
+proof (cases \<open>k \<ge> 0\<close>)
   case True
   moreover define m where \<open>m = nat k\<close>
   ultimately have \<open>k = int m\<close>
     by simp
   then show ?thesis

 next
   case False
   then show ?thesis
     by simp
 qed
+
+lemma push_bit_nat_eq:
+  \<open>push_bit n (nat k) = nat (push_bit n k)\<close>
+  by (cases \<open>k \<ge> 0\<close>) (simp_all add: push_bit_eq_mult nat_mult_distrib not_le mult_nonneg_nonpos2)
+
+lemma drop_bit_nat_eq:
+  \<open>drop_bit n (nat k) = nat (drop_bit n k)\<close>
+  apply (cases \<open>k \<ge> 0\<close>)
+   apply (simp_all add: drop_bit_eq_div nat_div_distrib nat_power_eq not_le)
+  apply (simp add: divide_int_def)
+  done
+
+lemma take_bit_nat_eq:
+  \<open>take_bit n (nat k) = nat (take_bit n k)\<close> if \<open>k \<ge> 0\<close>
+  using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
 
 lemma nat_take_bit_eq:
   \<open>nat (take_bit n k) = take_bit n (nat k)\<close>
   if \<open>k \<ge> 0\<close>
   using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)