src/HOL/Bit_Operations.thy

 class semiring_bits = semiring_parity + semiring_modulo_trivial +
   assumes bit_induct [case_names stable rec]:
     \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
      \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
         \<Longrightarrow> P a\<close>
-  assumes half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
+  assumes bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+    and half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
     and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close>
-    and even_mod_exp_div_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
   fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
   assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
 begin
 
 text \<open>

   next
     case (odd n)
     with rec [of n True] show ?case
       by simp
   qed
-  show \<open>even (q mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (q div 2 ^ n)\<close> for q m n :: nat
-  proof (cases \<open>m \<le> n\<close>)
-    case True
-    moreover define r where \<open>r = n - m\<close>
-    ultimately have \<open>n = m + r\<close>
-      by simp
-    with True show ?thesis
-      by (simp add: power_add div_mult2_eq)
-  next
-    case False
-    moreover define r where \<open>r = m - Suc n\<close>
-    ultimately have \<open>m = n + Suc r\<close>
-      by simp
-    moreover have \<open>even (q mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (q div 2 ^ n)\<close>
-      by (simp only: power_add) (simp add: mod_mult2_eq dvd_mod_iff)
-    ultimately show ?thesis
-      by simp
-  qed
 qed (auto simp add: div_mult2_eq bit_nat_def)
 
 end
 
 lemma possible_bit_nat [simp]:

       by (simp add: ac_simps)
   next
     case (odd k)
     with rec [of k True] show ?case
       by (simp add: ac_simps)
-  qed
-  show \<open>even (k mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (k div 2 ^ n)\<close> for k :: int and m n :: nat
-  proof (cases \<open>m \<le> n\<close>)
-    case True
-    moreover define r where \<open>r = n - m\<close>
-    ultimately have \<open>n = m + r\<close>
-      by simp
-    with True show ?thesis
-      by (simp add: power_add zdiv_zmult2_eq)
-  next
-    case False
-    moreover define r where \<open>r = m - Suc n\<close>
-    ultimately have \<open>m = n + Suc r\<close>
-      by simp
-    moreover have \<open>even (k mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (k div 2 ^ n)\<close>
-      by (simp only: power_add) (simp add: zmod_zmult2_eq dvd_mod_iff)
-    ultimately show ?thesis
-      by simp
   qed
 qed (auto simp add: zdiv_zmult2_eq bit_int_def)
 
 end
 

 
 lemma push_bit_numeral [simp]:
   \<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
   by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
 
-lemma take_bit_0 [simp]:
-  "take_bit 0 a = 0"
-  by (simp add: take_bit_eq_mod)
-
-lemma bit_take_bit_iff [bit_simps]:
-  \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
-  by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_div_exp_iff not_le)
-
-lemma take_bit_Suc:
-  \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
-proof (rule bit_eqI)
-  fix m
-  assume \<open>possible_bit TYPE('a) m\<close>
-  then show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
-    apply (cases a rule: parity_cases; cases m)
-       apply (simp_all add: bit_simps even_bit_succ_iff mult.commute [of _ 2] add.commute [of _ 1] flip: bit_Suc)
-     apply (simp_all add: bit_0)
-    done
-qed
-
-lemma take_bit_rec:
-  \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + a mod 2)\<close>
-  by (cases n) (simp_all add: take_bit_Suc)
-
-lemma take_bit_Suc_0 [simp]:
-  \<open>take_bit (Suc 0) a = a mod 2\<close>
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_of_0 [simp]:
-  \<open>take_bit n 0 = 0\<close>
-  by (rule bit_eqI) (simp add: bit_simps)
-
-lemma take_bit_of_1 [simp]:
-  \<open>take_bit n 1 = of_bool (n > 0)\<close>
-  by (cases n) (simp_all add: take_bit_Suc)
-
 lemma bit_drop_bit_eq [bit_simps]:
   \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
   by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
-
-lemma drop_bit_of_0 [simp]:
-  \<open>drop_bit n 0 = 0\<close>
-  by (rule bit_eqI) (simp add: bit_simps)
-
-lemma drop_bit_of_1 [simp]:
-  \<open>drop_bit n 1 = of_bool (n = 0)\<close>
-  by (rule bit_eqI) (simp add: bit_simps ac_simps)
-
-lemma drop_bit_0 [simp]:
-  \<open>drop_bit 0 = id\<close>
-  by (simp add: fun_eq_iff drop_bit_eq_div)
-
-lemma drop_bit_Suc:
-  \<open>drop_bit (Suc n) a = drop_bit n (a div 2)\<close>
-  using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
-
-lemma drop_bit_rec:
-  \<open>drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))\<close>
-  by (cases n) (simp_all add: drop_bit_Suc)
-
-lemma drop_bit_half:
-  \<open>drop_bit n (a div 2) = drop_bit n a div 2\<close>
-  by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)
-
-lemma drop_bit_of_bool [simp]:
-  \<open>drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)\<close>
-  by (cases n) simp_all
-
-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]:
-  \<open>take_bit m (take_bit n a) = take_bit (min m n) a\<close>
-  by (rule bit_eqI) (simp add: bit_simps)
-
-lemma drop_bit_drop_bit [simp]:
-  \<open>drop_bit m (drop_bit n a) = drop_bit (m + n) a\<close>
-  by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)
-
-lemma push_bit_take_bit:
-  \<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
-
-lemma take_bit_push_bit:
-  \<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
-
-lemma take_bit_drop_bit:
-  \<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
-
-lemma drop_bit_take_bit:
-  \<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
-
-lemma even_push_bit_iff [simp]:
-  \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
-  by (simp add: push_bit_eq_mult) auto
-
-lemma stable_imp_drop_bit_eq:
-  \<open>drop_bit n a = a\<close>
-  if \<open>a div 2 = a\<close>
-  by (induction n) (simp_all add: that drop_bit_Suc)
-
-lemma stable_imp_take_bit_eq:
-  \<open>take_bit n a = (if even a then 0 else mask n)\<close>
-    if \<open>a div 2 = a\<close>
-  by (rule bit_eqI) (use that in \<open>simp add: bit_simps stable_imp_bit_iff_odd\<close>)
-
-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
-
-lemma take_bit_tightened:
-  \<open>take_bit m a = take_bit m b\<close> if \<open>take_bit n a = take_bit n b\<close> and \<open>m \<le> n\<close>
-proof -
-  from that have \<open>take_bit m (take_bit n a) = take_bit m (take_bit n b)\<close>
-    by simp
-  then have \<open>take_bit (min m n) a = take_bit (min m n) b\<close>
-    by simp
-  with that show ?thesis
-    by (simp add: min_def)
-qed
-
-lemma take_bit_eq_self_iff_drop_bit_eq_0:
-  \<open>take_bit n a = a \<longleftrightarrow> drop_bit n a = 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-proof
-  assume ?P
-  show ?Q
-  proof (rule bit_eqI)
-    fix m
-    from \<open>?P\<close> have \<open>a = take_bit n a\<close> ..
-    also have \<open>\<not> bit (take_bit n a) (n + m)\<close>
-      unfolding bit_simps
-      by (simp add: bit_simps)
-    finally show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
-      by (simp add: bit_simps)
-  qed
-next
-  assume ?Q
-  show ?P
-  proof (rule bit_eqI)
-    fix m
-    from \<open>?Q\<close> have \<open>\<not> bit (drop_bit n a) (m - n)\<close>
-      by simp
-    then have \<open> \<not> bit a (n + (m - n))\<close>
-      by (simp add: bit_simps)
-    then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close>
-      by (cases \<open>m < n\<close>) (auto simp add: bit_simps)
-  qed
-qed
-
-lemma drop_bit_exp_eq:
-  \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma take_bit_and [simp]:
-  \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma take_bit_or [simp]:
-  \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma take_bit_xor [simp]:
-  \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma push_bit_and [simp]:
-  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma push_bit_or [simp]:
-  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma push_bit_xor [simp]:
-  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma drop_bit_and [simp]:
-  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma drop_bit_or [simp]:
-  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma drop_bit_xor [simp]:
-  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma take_bit_of_mask [simp]:
-  \<open>take_bit m (mask n) = mask (min m n)\<close>
-  by (rule bit_eqI) (simp add: bit_simps)
-
-lemma take_bit_eq_mask:
-  \<open>take_bit n a = a AND mask n\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma or_eq_0_iff:
-  \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
-  by (auto simp add: bit_eq_iff bit_or_iff)
-
-lemma bit_iff_and_drop_bit_eq_1:
-  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
-  by (simp add: bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)
-
-lemma bit_iff_and_push_bit_not_eq_0:
-  \<open>bit a n \<longleftrightarrow> a AND push_bit n 1 \<noteq> 0\<close>
-  by (cases \<open>possible_bit TYPE('a) n\<close>) (simp_all add: bit_eq_iff bit_simps impossible_bit)
-
-lemma bit_set_bit_iff [bit_simps]:
-  \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
-  by (auto simp add: set_bit_eq_or bit_or_iff bit_exp_iff)
-
-lemma even_set_bit_iff:
-  \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
-  using bit_set_bit_iff [of m a 0] by (auto simp add: bit_0)
-
-lemma bit_unset_bit_iff [bit_simps]:
-  \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
-  by (auto simp add: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit)
-
-lemma even_unset_bit_iff:
-  \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
-  using bit_unset_bit_iff [of m a 0] by (auto simp add: bit_0)
-
-lemma bit_flip_bit_iff [bit_simps]:
-  \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> possible_bit TYPE('a) n\<close>
-  by (auto simp add: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)
-
-lemma even_flip_bit_iff:
-  \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
-  using bit_flip_bit_iff [of m a 0] by (auto simp: possible_bit_def  bit_0)
-
-lemma and_exp_eq_0_iff_not_bit:
-  \<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-  using bit_imp_possible_bit[of a n]
-  by (auto simp add: bit_eq_iff bit_simps)
-
-lemma bit_sum_mult_2_cases:
-  assumes a: \<open>\<forall>j. \<not> bit a (Suc j)\<close>
-  shows \<open>bit (a + 2 * b) n = (if n = 0 then odd a else bit (2 * b) n)\<close>
-proof -
-  from a have \<open>n = 0\<close> if \<open>bit a n\<close> for n using that
-    by (cases n) simp_all
-  then have \<open>a = 0 \<or> a = 1\<close>
-    by (auto simp add: bit_eq_iff bit_1_iff)
-  then show ?thesis
-    by (cases n) (auto simp add: bit_0 bit_double_iff even_bit_succ_iff)
-qed
-
-lemma set_bit_0 [simp]:
-  \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
-
-lemma set_bit_Suc:
-  \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
-    elim: possible_bit_less_imp)
-
-lemma unset_bit_0 [simp]:
-  \<open>unset_bit 0 a = 2 * (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_simps simp flip: bit_Suc)
-
-lemma unset_bit_Suc:
-  \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
-
-lemma flip_bit_0 [simp]:
-  \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
-
-lemma flip_bit_Suc:
-  \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
-    elim: possible_bit_less_imp)
-
-lemma flip_bit_eq_if:
-  \<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close>
-  by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)
-
-lemma take_bit_set_bit_eq:
-  \<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close>
-  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff)
-
-lemma take_bit_unset_bit_eq:
-  \<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close>
-  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff)
-
-lemma take_bit_flip_bit_eq:
-  \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
-  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)
-
-lemma bit_1_0 [simp]:
-  \<open>bit 1 0\<close>
-  by (simp add: bit_0)
-
-lemma not_bit_1_Suc [simp]:
-  \<open>\<not> bit 1 (Suc n)\<close>
-  by (simp add: bit_Suc)
-
-lemma push_bit_Suc_numeral [simp]:
-  \<open>push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\<close>
-  by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
-
-lemma mask_eq_0_iff [simp]:
-  \<open>mask n = 0 \<longleftrightarrow> n = 0\<close>
-  by (cases n) (simp_all add: mask_Suc_double or_eq_0_iff)
-
-lemma bit_horner_sum_bit_iff [bit_simps]:
-  \<open>bit (horner_sum of_bool 2 bs) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < length bs \<and> bs ! n\<close>
-proof (induction bs arbitrary: n)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  show ?case
-  proof (cases n)
-    case 0
-    then show ?thesis
-      by (simp add: bit_0)
-  next
-    case (Suc m)
-    with bit_rec [of _ n] Cons.prems Cons.IH [of m]
-    show ?thesis
-      by (simp add: bit_simps)
-        (auto simp add: possible_bit_less_imp bit_simps simp flip: bit_Suc)
-  qed
-qed
-
-lemma horner_sum_bit_eq_take_bit:
-  \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
-
-lemma take_bit_horner_sum_bit_eq:
-  \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
-
-lemma take_bit_sum:
-  \<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
-  by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
 
 lemma disjunctive_xor_eq_or:
   \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
   using that by (auto simp add: bit_eq_iff bit_simps)
 

 qed
 
 lemma disjunctive_add_eq_xor:
   \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
   using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
+
+lemma take_bit_0 [simp]:
+  "take_bit 0 a = 0"
+  by (simp add: take_bit_eq_mod)
+
+lemma bit_take_bit_iff [bit_simps]:
+  \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
+proof -
+  have \<open>push_bit m (drop_bit m a) AND take_bit m a = 0\<close> (is \<open>?lhs = _\<close>)
+  proof (rule bit_eqI)
+    fix n
+    show \<open>bit ?lhs n \<longleftrightarrow> bit 0 n\<close>
+    proof (cases \<open>m \<le> n\<close>)
+      case False
+      then show ?thesis
+        by (simp add: bit_simps)
+    next
+      case True
+      moreover define q where \<open>q = n - m\<close>
+      ultimately have \<open>n = m + q\<close> by simp
+      moreover have \<open>\<not> bit (take_bit m a) (m + q)\<close>
+        by (simp add: take_bit_eq_mod bit_iff_odd flip: div_exp_eq)
+      ultimately show ?thesis
+        by (simp add: bit_simps)
+    qed
+  qed
+  then have \<open>push_bit m (drop_bit m a) XOR take_bit m a = push_bit m (drop_bit m a) + take_bit m a\<close>
+    by (simp add: disjunctive_add_eq_xor)
+  also have \<open>\<dots> = a\<close>
+    by (simp add: bits_ident)
+  finally have \<open>bit (push_bit m (drop_bit m a) XOR take_bit m a) n \<longleftrightarrow> bit a n\<close>
+    by simp
+  also have \<open>\<dots> \<longleftrightarrow> (m \<le> n \<or> n < m) \<and> bit a n\<close>
+    by auto
+  also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
+    by auto
+  also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
+    by (auto simp add: bit_simps bit_imp_possible_bit)
+  finally show ?thesis
+    by (auto simp add: bit_simps)
+qed
+
+lemma take_bit_Suc:
+  \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
+proof (rule bit_eqI)
+  fix m
+  assume \<open>possible_bit TYPE('a) m\<close>
+  then show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
+    apply (cases a rule: parity_cases; cases m)
+       apply (simp_all add: bit_simps even_bit_succ_iff mult.commute [of _ 2] add.commute [of _ 1] flip: bit_Suc)
+     apply (simp_all add: bit_0)
+    done
+qed
+
+lemma take_bit_rec:
+  \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + a mod 2)\<close>
+  by (cases n) (simp_all add: take_bit_Suc)
+
+lemma take_bit_Suc_0 [simp]:
+  \<open>take_bit (Suc 0) a = a mod 2\<close>
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_of_0 [simp]:
+  \<open>take_bit n 0 = 0\<close>
+  by (rule bit_eqI) (simp add: bit_simps)
+
+lemma take_bit_of_1 [simp]:
+  \<open>take_bit n 1 = of_bool (n > 0)\<close>
+  by (cases n) (simp_all add: take_bit_Suc)
+
+lemma drop_bit_of_0 [simp]:
+  \<open>drop_bit n 0 = 0\<close>
+  by (rule bit_eqI) (simp add: bit_simps)
+
+lemma drop_bit_of_1 [simp]:
+  \<open>drop_bit n 1 = of_bool (n = 0)\<close>
+  by (rule bit_eqI) (simp add: bit_simps ac_simps)
+
+lemma drop_bit_0 [simp]:
+  \<open>drop_bit 0 = id\<close>
+  by (simp add: fun_eq_iff drop_bit_eq_div)
+
+lemma drop_bit_Suc:
+  \<open>drop_bit (Suc n) a = drop_bit n (a div 2)\<close>
+  using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_rec:
+  \<open>drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))\<close>
+  by (cases n) (simp_all add: drop_bit_Suc)
+
+lemma drop_bit_half:
+  \<open>drop_bit n (a div 2) = drop_bit n a div 2\<close>
+  by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)
+
+lemma drop_bit_of_bool [simp]:
+  \<open>drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)\<close>
+  by (cases n) simp_all
+
+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]:
+  \<open>take_bit m (take_bit n a) = take_bit (min m n) a\<close>
+  by (rule bit_eqI) (simp add: bit_simps)
+
+lemma drop_bit_drop_bit [simp]:
+  \<open>drop_bit m (drop_bit n a) = drop_bit (m + n) a\<close>
+  by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)
+
+lemma push_bit_take_bit:
+  \<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma take_bit_push_bit:
+  \<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma take_bit_drop_bit:
+  \<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma drop_bit_take_bit:
+  \<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma even_push_bit_iff [simp]:
+  \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
+  by (simp add: push_bit_eq_mult) auto
+
+lemma stable_imp_drop_bit_eq:
+  \<open>drop_bit n a = a\<close>
+  if \<open>a div 2 = a\<close>
+  by (induction n) (simp_all add: that drop_bit_Suc)
+
+lemma stable_imp_take_bit_eq:
+  \<open>take_bit n a = (if even a then 0 else mask n)\<close>
+    if \<open>a div 2 = a\<close>
+  by (rule bit_eqI) (use that in \<open>simp add: bit_simps stable_imp_bit_iff_odd\<close>)
+
+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
+
+lemma take_bit_tightened:
+  \<open>take_bit m a = take_bit m b\<close> if \<open>take_bit n a = take_bit n b\<close> and \<open>m \<le> n\<close>
+proof -
+  from that have \<open>take_bit m (take_bit n a) = take_bit m (take_bit n b)\<close>
+    by simp
+  then have \<open>take_bit (min m n) a = take_bit (min m n) b\<close>
+    by simp
+  with that show ?thesis
+    by (simp add: min_def)
+qed
+
+lemma take_bit_eq_self_iff_drop_bit_eq_0:
+  \<open>take_bit n a = a \<longleftrightarrow> drop_bit n a = 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?P
+  show ?Q
+  proof (rule bit_eqI)
+    fix m
+    from \<open>?P\<close> have \<open>a = take_bit n a\<close> ..
+    also have \<open>\<not> bit (take_bit n a) (n + m)\<close>
+      unfolding bit_simps
+      by (simp add: bit_simps)
+    finally show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
+      by (simp add: bit_simps)
+  qed
+next
+  assume ?Q
+  show ?P
+  proof (rule bit_eqI)
+    fix m
+    from \<open>?Q\<close> have \<open>\<not> bit (drop_bit n a) (m - n)\<close>
+      by simp
+    then have \<open> \<not> bit a (n + (m - n))\<close>
+      by (simp add: bit_simps)
+    then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close>
+      by (cases \<open>m < n\<close>) (auto simp add: bit_simps)
+  qed
+qed
+
+lemma drop_bit_exp_eq:
+  \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma take_bit_and [simp]:
+  \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma take_bit_or [simp]:
+  \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma take_bit_xor [simp]:
+  \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma push_bit_and [simp]:
+  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma push_bit_or [simp]:
+  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma push_bit_xor [simp]:
+  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma drop_bit_and [simp]:
+  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma drop_bit_or [simp]:
+  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma drop_bit_xor [simp]:
+  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma take_bit_of_mask [simp]:
+  \<open>take_bit m (mask n) = mask (min m n)\<close>
+  by (rule bit_eqI) (simp add: bit_simps)
+
+lemma take_bit_eq_mask:
+  \<open>take_bit n a = a AND mask n\<close>
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma or_eq_0_iff:
+  \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
+  by (auto simp add: bit_eq_iff bit_or_iff)
+
+lemma bit_iff_and_drop_bit_eq_1:
+  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
+  by (simp add: bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)
+
+lemma bit_iff_and_push_bit_not_eq_0:
+  \<open>bit a n \<longleftrightarrow> a AND push_bit n 1 \<noteq> 0\<close>
+  by (cases \<open>possible_bit TYPE('a) n\<close>) (simp_all add: bit_eq_iff bit_simps impossible_bit)
+
+lemma bit_set_bit_iff [bit_simps]:
+  \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
+  by (auto simp add: set_bit_eq_or bit_or_iff bit_exp_iff)
+
+lemma even_set_bit_iff:
+  \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
+  using bit_set_bit_iff [of m a 0] by (auto simp add: bit_0)
+
+lemma bit_unset_bit_iff [bit_simps]:
+  \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
+  by (auto simp add: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit)
+
+lemma even_unset_bit_iff:
+  \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
+  using bit_unset_bit_iff [of m a 0] by (auto simp add: bit_0)
+
+lemma bit_flip_bit_iff [bit_simps]:
+  \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> possible_bit TYPE('a) n\<close>
+  by (auto simp add: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)
+
+lemma even_flip_bit_iff:
+  \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
+  using bit_flip_bit_iff [of m a 0] by (auto simp: possible_bit_def  bit_0)
+
+lemma and_exp_eq_0_iff_not_bit:
+  \<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  using bit_imp_possible_bit[of a n]
+  by (auto simp add: bit_eq_iff bit_simps)
+
+lemma bit_sum_mult_2_cases:
+  assumes a: \<open>\<forall>j. \<not> bit a (Suc j)\<close>
+  shows \<open>bit (a + 2 * b) n = (if n = 0 then odd a else bit (2 * b) n)\<close>
+proof -
+  from a have \<open>n = 0\<close> if \<open>bit a n\<close> for n using that
+    by (cases n) simp_all
+  then have \<open>a = 0 \<or> a = 1\<close>
+    by (auto simp add: bit_eq_iff bit_1_iff)
+  then show ?thesis
+    by (cases n) (auto simp add: bit_0 bit_double_iff even_bit_succ_iff)
+qed
+
+lemma set_bit_0 [simp]:
+  \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
+  by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
+
+lemma set_bit_Suc:
+  \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
+  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
+    elim: possible_bit_less_imp)
+
+lemma unset_bit_0 [simp]:
+  \<open>unset_bit 0 a = 2 * (a div 2)\<close>
+  by (auto simp add: bit_eq_iff bit_simps simp flip: bit_Suc)
+
+lemma unset_bit_Suc:
+  \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
+  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
+
+lemma flip_bit_0 [simp]:
+  \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
+  by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
+
+lemma flip_bit_Suc:
+  \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
+  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
+    elim: possible_bit_less_imp)
+
+lemma flip_bit_eq_if:
+  \<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close>
+  by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)
+
+lemma take_bit_set_bit_eq:
+  \<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close>
+  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff)
+
+lemma take_bit_unset_bit_eq:
+  \<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close>
+  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff)
+
+lemma take_bit_flip_bit_eq:
+  \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
+  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)
+
+lemma bit_1_0 [simp]:
+  \<open>bit 1 0\<close>
+  by (simp add: bit_0)
+
+lemma not_bit_1_Suc [simp]:
+  \<open>\<not> bit 1 (Suc n)\<close>
+  by (simp add: bit_Suc)
+
+lemma push_bit_Suc_numeral [simp]:
+  \<open>push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\<close>
+  by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
+
+lemma mask_eq_0_iff [simp]:
+  \<open>mask n = 0 \<longleftrightarrow> n = 0\<close>
+  by (cases n) (simp_all add: mask_Suc_double or_eq_0_iff)
+
+lemma bit_horner_sum_bit_iff [bit_simps]:
+  \<open>bit (horner_sum of_bool 2 bs) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < length bs \<and> bs ! n\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  show ?case
+  proof (cases n)
+    case 0
+    then show ?thesis
+      by (simp add: bit_0)
+  next
+    case (Suc m)
+    with bit_rec [of _ n] Cons.prems Cons.IH [of m]
+    show ?thesis
+      by (simp add: bit_simps)
+        (auto simp add: possible_bit_less_imp bit_simps simp flip: bit_Suc)
+  qed
+qed
+
+lemma horner_sum_bit_eq_take_bit:
+  \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma take_bit_horner_sum_bit_eq:
+  \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
+
+lemma take_bit_sum:
+  \<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
+  by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
 
 lemma set_bit_eq:
   \<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
 proof -
   have \<open>a AND of_bool (\<not> bit a n) * 2 ^ n = 0\<close>

 
 lemma disjunctive_add [no_atp]:
   \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
   by (rule disjunctive_add_eq_or) (use that in \<open>simp add: bit_eq_iff bit_simps\<close>)
 
+lemma even_mod_exp_div_exp_iff [no_atp]:
+  \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
+  by (auto simp add: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod)
+
 end
 
 context ring_bit_operations
 begin