# HG changeset patch
# User haftmann
# Date 1635259439 0
# Node ID 3c587b7c3d5cc693018dddc88096fdca5591079f
# Parent  a0ab0dc28d3c19029fa8b7c89ed4a71df8dcc2a5
more generic bit/word lemmas for distribution

diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Bit_Operations.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -542,10 +542,6 @@
   \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
   by (simp add: bit_1_iff)
 
-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 [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit m n\<close>
 proof (cases \<open>(2::'a) ^ n = 0\<close>)
@@ -831,7 +827,7 @@
   "push_bit n 0 = 0"
   by (simp add: push_bit_eq_mult)
 
-lemma push_bit_of_1:
+lemma push_bit_of_1 [simp]:
   "push_bit n 1 = 2 ^ n"
   by (simp add: push_bit_eq_mult)
 
@@ -1129,7 +1125,7 @@
   \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
   by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)
 
-lemma take_bit_mask [simp]:
+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)
 
@@ -1152,7 +1148,7 @@
 lemma bit_iff_and_push_bit_not_eq_0:
   \<open>bit a n \<longleftrightarrow> a AND push_bit n 1 \<noteq> 0\<close>
   apply (cases \<open>2 ^ n = 0\<close>)
-  apply (simp_all add: push_bit_of_1 bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit)
+  apply (simp_all add: bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit)
   apply (simp_all add: bit_exp_iff)
   done
 
@@ -1160,7 +1156,7 @@
 
 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_def push_bit_of_1 bit_or_iff bit_exp_iff)
+  by (auto simp add: set_bit_def 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>
@@ -1246,6 +1242,10 @@
   \<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)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -1379,7 +1379,7 @@
   \<open>mask n = take_bit n (- 1)\<close>
   by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)
 
-lemma take_bit_minus_one_eq_mask:
+lemma take_bit_minus_one_eq_mask [simp]:
   \<open>take_bit n (- 1) = mask n\<close>
   by (simp add: mask_eq_take_bit_minus_one)
 
@@ -1387,7 +1387,7 @@
   \<open>- (2 ^ n) = NOT (mask n)\<close>
   by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1)
 
-lemma push_bit_minus_one_eq_not_mask:
+lemma push_bit_minus_one_eq_not_mask [simp]:
   \<open>push_bit n (- 1) = NOT (mask n)\<close>
   by (simp add: push_bit_eq_mult minus_exp_eq_not_mask)
 
@@ -1412,13 +1412,30 @@
   \<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
   by (simp only: numeral_eq_Suc push_bit_Suc_minus_numeral)
 
-lemma take_bit_Suc_1:
+lemma take_bit_Suc_minus_1_eq:
   \<open>take_bit (Suc n) (- 1) = 2 ^ Suc n - 1\<close>
-  by (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
-
-lemma take_bit_numeral_1 [simp]:
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma take_bit_numeral_minus_1_eq:
   \<open>take_bit (numeral k) (- 1) = 2 ^ numeral k - 1\<close>
-  by (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma push_bit_mask_eq:
+  \<open>push_bit m (mask n) = mask (n + m) AND NOT (mask m)\<close>
+  apply (rule bit_eqI)
+  apply (auto simp add: bit_simps not_less possible_bit_def)
+  apply (drule sym [of 0])
+  apply (simp only:)
+  using exp_not_zero_imp_exp_diff_not_zero apply (blast dest: exp_not_zero_imp_exp_diff_not_zero)
+  done
+
+lemma slice_eq_mask:
+  \<open>push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma push_bit_numeral_minus_1 [simp]:
+  \<open>push_bit (numeral n) (- 1) = - (2 ^ numeral n)\<close>
+  by (simp add: push_bit_eq_mult)
 
 end
 
@@ -2041,6 +2058,293 @@
   for k :: int
   by (simp add: bit_simps)
 
+lemma take_bit_incr_eq:
+  \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
+  for k :: int
+proof -
+  from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
+    by (simp add: take_bit_eq_mod)
+  moreover have \<open>k mod 2 ^ n < 2 ^ n\<close>
+    by simp
+  ultimately have *: \<open>k mod 2 ^ n + 1 < 2 ^ n\<close>
+    by linarith
+  have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
+    by (simp add: mod_simps)
+  also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
+    using * by (simp add: zmod_trivial_iff)
+  finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_decr_eq:
+  \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
+  for k :: int
+proof -
+  from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
+    by (simp add: take_bit_eq_mod)
+  moreover have \<open>k mod 2 ^ n \<ge> 0\<close> \<open>k mod 2 ^ n < 2 ^ n\<close>
+    by simp_all
+  ultimately have *: \<open>k mod 2 ^ n > 0\<close>
+    by linarith
+  have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
+    by (simp add: mod_simps)
+  also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
+    by (simp add: zmod_trivial_iff)
+      (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
+  finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_greater_eq:
+  \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
+proof -
+  have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
+  proof (cases \<open>k > - (2 ^ n)\<close>)
+    case False
+    then have \<open>k + 2 ^ n \<le> 0\<close>
+      by simp
+    also note take_bit_nonnegative
+    finally show ?thesis .
+  next
+    case True
+    with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
+      by simp_all
+    then show ?thesis
+      by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
+  qed
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_less_eq:
+  \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
+  using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_int_less_eq_self_iff:
+  \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for k :: int
+proof
+  assume ?P
+  show ?Q
+  proof (rule ccontr)
+    assume \<open>\<not> 0 \<le> k\<close>
+    then have \<open>k < 0\<close>
+      by simp
+    with \<open>?P\<close>
+    have \<open>take_bit n k < 0\<close>
+      by (rule le_less_trans)
+    then show False
+      by simp
+  qed
+next
+  assume ?Q
+  then show ?P
+    by (simp add: take_bit_eq_mod zmod_le_nonneg_dividend)
+qed
+
+lemma take_bit_int_less_self_iff:
+  \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+  for k :: int
+  by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
+    intro: order_trans [of 0 \<open>2 ^ n\<close> k])
+
+lemma take_bit_int_greater_self_iff:
+  \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
+  for k :: int
+  using take_bit_int_less_eq_self_iff [of n k] by auto
+
+lemma take_bit_int_greater_eq_self_iff:
+  \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+  for k :: int
+  by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
+    dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
+
+lemma not_exp_less_eq_0_int [simp]:
+  \<open>\<not> 2 ^ n \<le> (0::int)\<close>
+  by (simp add: power_le_zero_eq)
+
+lemma half_nonnegative_int_iff [simp]:
+  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+proof (cases \<open>k \<ge> 0\<close>)
+  case True
+  then show ?thesis
+    by (auto simp add: divide_int_def sgn_1_pos)
+next
+  case False
+  then show ?thesis
+    by (auto simp add: divide_int_def not_le elim!: evenE)
+qed
+
+lemma half_negative_int_iff [simp]:
+  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
+lemma int_bit_bound:
+  fixes k :: int
+  obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+    and \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close>
+proof -
+  obtain q where *: \<open>\<And>m. q \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k q\<close>
+  proof (cases \<open>k \<ge> 0\<close>)
+    case True
+    moreover from power_gt_expt [of 2 \<open>nat k\<close>]
+    have \<open>nat k < 2 ^ nat k\<close>
+      by simp
+    then have \<open>int (nat k) < int (2 ^ nat k)\<close>
+      by (simp only: of_nat_less_iff)
+    ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
+      by simp
+    show thesis
+    proof (rule that [of \<open>nat k\<close>])
+      fix m
+      assume \<open>nat k \<le> m\<close>
+      then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
+        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
+    qed
+  next
+    case False
+    moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
+    have \<open>nat (- k) < 2 ^ nat (- k)\<close>
+      by simp
+    then have \<open>int (nat (- k)) < int (2 ^ nat (- k))\<close>
+      by (simp only: of_nat_less_iff)
+    ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
+      by (subst div_pos_neg_trivial) simp_all
+    then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
+      by simp
+    show thesis
+    proof (rule that [of \<open>nat (- k)\<close>])
+      fix m
+      assume \<open>nat (- k) \<le> m\<close>
+      then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
+        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
+    qed
+  qed
+  show thesis
+  proof (cases \<open>\<forall>m. bit k m \<longleftrightarrow> bit k q\<close>)
+    case True
+    then have \<open>bit k 0 \<longleftrightarrow> bit k q\<close>
+      by blast
+    with True that [of 0] show thesis
+      by simp
+  next
+    case False
+    then obtain r where **: \<open>bit k r \<noteq> bit k q\<close>
+      by blast
+    have \<open>r < q\<close>
+      by (rule ccontr) (use * [of r] ** in simp)
+    define N where \<open>N = {n. n < q \<and> bit k n \<noteq> bit k q}\<close>
+    moreover have \<open>finite N\<close> \<open>r \<in> N\<close>
+      using ** N_def \<open>r < q\<close> by auto
+    moreover define n where \<open>n = Suc (Max N)\<close>
+    ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+      apply auto
+         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
+        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
+        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
+      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
+      done
+    have \<open>bit k (Max N) \<noteq> bit k n\<close>
+      by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
+    show thesis apply (rule that [of n])
+      using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
+      using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
+  qed
+qed
+
+lemma take_bit_tightened_less_eq_int:
+  \<open>take_bit m k \<le> take_bit n k\<close> if \<open>m \<le> n\<close> for k :: int
+proof -
+  have \<open>take_bit m (take_bit n k) \<le> take_bit n k\<close>
+    by (simp only: take_bit_int_less_eq_self_iff take_bit_nonnegative)
+  with that show ?thesis
+    by simp
+qed
+
+context ring_bit_operations
+begin
+
+lemma even_of_int_iff:
+  \<open>even (of_int k) \<longleftrightarrow> even k\<close>
+  by (induction k rule: int_bit_induct) simp_all
+
+lemma bit_of_int_iff [bit_simps]:
+  \<open>bit (of_int k) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit k n\<close>
+proof (cases \<open>possible_bit TYPE('a) n\<close>)
+  case False
+  then show ?thesis
+    by (simp add: impossible_bit)
+next
+  case True
+  then have \<open>bit (of_int k) n \<longleftrightarrow> bit k n\<close>
+  proof (induction k arbitrary: n rule: int_bit_induct)
+    case zero
+    then show ?case
+      by simp
+  next
+    case minus
+    then show ?case
+      by simp
+  next
+    case (even k)
+    then show ?case
+      using bit_double_iff [of \<open>of_int k\<close> n] Bit_Operations.bit_double_iff [of k n]
+      by (cases n) (auto simp add: ac_simps possible_bit_def dest: mult_not_zero)
+  next
+    case (odd k)
+    then show ?case
+      using bit_double_iff [of \<open>of_int k\<close> n]
+      by (cases n) (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Bit_Operations.bit_Suc possible_bit_def dest: mult_not_zero)
+  qed
+  with True show ?thesis
+    by simp
+qed
+
+lemma push_bit_of_int:
+  \<open>push_bit n (of_int k) = of_int (push_bit n k)\<close>
+  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
+
+lemma of_int_push_bit:
+  \<open>of_int (push_bit n k) = push_bit n (of_int k)\<close>
+  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
+
+lemma take_bit_of_int:
+  \<open>take_bit n (of_int k) = of_int (take_bit n k)\<close>
+  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_int_iff)
+
+lemma of_int_take_bit:
+  \<open>of_int (take_bit n k) = take_bit n (of_int k)\<close>
+  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_int_iff)
+
+lemma of_int_not_eq:
+  \<open>of_int (NOT k) = NOT (of_int k)\<close>
+  by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff)
+
+lemma of_int_not_numeral:
+  \<open>of_int (NOT (numeral k)) = NOT (numeral k)\<close>
+  by (simp add: local.of_int_not_eq)
+
+lemma of_int_and_eq:
+  \<open>of_int (k AND l) = of_int k AND of_int l\<close>
+  by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma of_int_or_eq:
+  \<open>of_int (k OR l) = of_int k OR of_int l\<close>
+  by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma of_int_xor_eq:
+  \<open>of_int (k XOR l) = of_int k XOR of_int l\<close>
+  by (rule bit_eqI) (simp add: bit_of_int_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+lemma of_int_mask_eq:
+  \<open>of_int (mask n) = mask n\<close>
+  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_int_or_eq)
+
+end
+
 
 subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
@@ -2139,24 +2443,15 @@
 
 lemma and_nat_rec:
   \<open>m AND n = of_bool (odd m \<and> odd n) + 2 * ((m div 2) AND (n div 2))\<close> for m n :: nat
-  apply (simp add: and_nat_def and_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
-  apply (subst nat_add_distrib)
-    apply auto
-  done
+  by (simp add: and_nat_def and_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
 
 lemma or_nat_rec:
   \<open>m OR n = of_bool (odd m \<or> odd n) + 2 * ((m div 2) OR (n div 2))\<close> for m n :: nat
-  apply (simp add: or_nat_def or_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
-  apply (subst nat_add_distrib)
-    apply auto
-  done
+  by (simp add: or_nat_def or_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
 
 lemma xor_nat_rec:
   \<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * ((m div 2) XOR (n div 2))\<close> for m n :: nat
-  apply (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
-  apply (subst nat_add_distrib)
-    apply auto
-  done
+  by (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
 
 lemma Suc_0_and_eq [simp]:
   \<open>Suc 0 AND n = n mod 2\<close>
@@ -2202,6 +2497,92 @@
   \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m n :: nat
   by (simp_all add: unset_bit_Suc)
 
+lemma push_bit_of_Suc_0 [simp]:
+  \<open>push_bit n (Suc 0) = 2 ^ n\<close>
+  using push_bit_of_1 [where ?'a = nat] by simp
+
+lemma take_bit_of_Suc_0 [simp]:
+  \<open>take_bit n (Suc 0) = of_bool (0 < n)\<close>
+  using take_bit_of_1 [where ?'a = nat] by simp
+
+lemma drop_bit_of_Suc_0 [simp]:
+  \<open>drop_bit n (Suc 0) = of_bool (n = 0)\<close>
+  using drop_bit_of_1 [where ?'a = nat] by simp
+
+lemma Suc_mask_eq_exp:
+  \<open>Suc (mask n) = 2 ^ n\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma less_eq_mask:
+  \<open>n \<le> mask n\<close>
+  by (simp add: mask_eq_exp_minus_1 le_diff_conv2)
+    (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0)
+
+lemma less_mask:
+  \<open>n < mask n\<close> if \<open>Suc 0 < n\<close>
+proof -
+  define m where \<open>m = n - 2\<close>
+  with that have *: \<open>n = m + 2\<close>
+    by simp
+  have \<open>Suc (Suc (Suc m)) < 4 * 2 ^ m\<close>
+    by (induction m) simp_all
+  then have \<open>Suc (m + 2) < Suc (mask (m + 2))\<close>
+    by (simp add: Suc_mask_eq_exp)
+  then have \<open>m + 2 < mask (m + 2)\<close>
+    by (simp add: less_le)
+  with * show ?thesis
+    by simp
+qed
+
+lemma mask_nat_less_exp [simp]:
+  \<open>(mask n :: nat) < 2 ^ n\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma mask_nat_positive_iff [simp]:
+  \<open>(0::nat) < mask n \<longleftrightarrow> 0 < n\<close>
+proof (cases \<open>n = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have \<open>0 < n\<close>
+    by simp
+  then have \<open>(0::nat) < mask n\<close>
+    using less_eq_mask [of n] by (rule order_less_le_trans)
+  with \<open>0 < n\<close> show ?thesis
+    by simp
+qed
+
+lemma take_bit_tightened_less_eq_nat:
+  \<open>take_bit m q \<le> take_bit n q\<close> if \<open>m \<le> n\<close> for q :: nat
+proof -
+  have \<open>take_bit m (take_bit n q) \<le> take_bit n q\<close>
+    by (rule take_bit_nat_less_eq_self)
+  with that 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)
+
 context semiring_bit_operations
 begin
 
@@ -2223,6 +2604,31 @@
 
 end
 
+context semiring_bit_operations
+begin
+
+lemma of_nat_and_eq:
+  \<open>of_nat (m AND n) = of_nat m AND of_nat n\<close>
+  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma of_nat_or_eq:
+  \<open>of_nat (m OR n) = of_nat m OR of_nat n\<close>
+  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma of_nat_xor_eq:
+  \<open>of_nat (m XOR n) = of_nat m XOR of_nat n\<close>
+  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+lemma of_nat_mask_eq:
+  \<open>of_nat (mask n) = mask n\<close>
+  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)
+
+end
+
+lemma nat_mask_eq:
+  \<open>nat (mask n) = mask n\<close>
+  by (simp add: nat_eq_iff of_nat_mask_eq)
+
 
 subsection \<open>Common algebraic structure\<close>
 
@@ -2238,10 +2644,6 @@
   \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
   using take_bit_of_exp [of n 1] by simp
 
-lemma take_bit_of_mask:
-  \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
-  by (simp add: take_bit_eq_mod mask_mod_exp)
-
 lemma push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)
@@ -2274,11 +2676,11 @@
   \<open>take_bit (Suc n) 1 = 1\<close>
   by (simp add: take_bit_Suc)
 
-lemma take_bit_Suc_bit0 [simp]:
+lemma take_bit_Suc_bit0:
   \<open>take_bit (Suc n) (numeral (Num.Bit0 k)) = take_bit n (numeral k) * 2\<close>
   by (simp add: take_bit_Suc numeral_Bit0_div_2)
 
-lemma take_bit_Suc_bit1 [simp]:
+lemma take_bit_Suc_bit1:
   \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
   by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
 
@@ -2286,11 +2688,11 @@
   \<open>take_bit (numeral l) 1 = 1\<close>
   by (simp add: take_bit_rec [of \<open>numeral l\<close> 1])
 
-lemma take_bit_numeral_bit0 [simp]:
+lemma take_bit_numeral_bit0:
   \<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
   by (simp add: take_bit_rec numeral_Bit0_div_2)
 
-lemma take_bit_numeral_bit1 [simp]:
+lemma take_bit_numeral_bit1:
   \<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)
 
@@ -2354,21 +2756,21 @@
   \<open>drop_bit (numeral l) (- numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (- numeral (Num.inc k) :: int)\<close>
   by (simp add: numeral_eq_Suc numeral_Bit1_div_2)
 
-lemma take_bit_Suc_minus_bit0 [simp]:
+lemma take_bit_Suc_minus_bit0:
   \<open>take_bit (Suc n) (- numeral (Num.Bit0 k)) = take_bit n (- numeral k) * (2 :: int)\<close>
   by (simp add: take_bit_Suc numeral_Bit0_div_2)
 
-lemma take_bit_Suc_minus_bit1 [simp]:
+lemma take_bit_Suc_minus_bit1:
   \<open>take_bit (Suc n) (- numeral (Num.Bit1 k)) = take_bit n (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
   by (simp add: take_bit_Suc numeral_Bit1_div_2 add_One)
 
-lemma take_bit_numeral_minus_bit0 [simp]:
+lemma take_bit_numeral_minus_bit0:
   \<open>take_bit (numeral l) (- numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (- numeral k) * (2 :: int)\<close>
-  by (simp add: numeral_eq_Suc numeral_Bit0_div_2)
-
-lemma take_bit_numeral_minus_bit1 [simp]:
+  by (simp add: numeral_eq_Suc numeral_Bit0_div_2 take_bit_Suc_minus_bit0)
+
+lemma take_bit_numeral_minus_bit1:
   \<open>take_bit (numeral l) (- numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
-  by (simp add: numeral_eq_Suc numeral_Bit1_div_2)
+  by (simp add: numeral_eq_Suc numeral_Bit1_div_2 take_bit_Suc_minus_bit1)
 
 
 subsection \<open>Symbolic computations on numeral expressions\<close>
@@ -2569,6 +2971,14 @@
   \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
   by (simp_all add: bit_minus_iff bit_not_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq)
 
+lemma bit_minus_numeral_Bit0_Suc_iff [simp]:
+  \<open>bit (- numeral (num.Bit0 w) :: int) (Suc n) \<longleftrightarrow> bit (- numeral w :: int) n\<close>
+  by (simp add: bit_Suc)
+
+lemma bit_minus_numeral_Bit1_Suc_iff [simp]:
+  \<open>bit (- numeral (num.Bit1 w) :: int) (Suc n) \<longleftrightarrow> \<not> bit (numeral w :: int) n\<close>
+  by (simp add: bit_Suc add_One flip: bit_not_int_iff)
+
 lemma and_not_numerals:
   \<open>1 AND NOT 1 = (0 :: int)\<close>
   \<open>1 AND NOT (numeral (Num.Bit0 n)) = (1 :: int)\<close>
@@ -2684,6 +3094,91 @@
   \<open>k XOR - numeral n = NOT (k XOR (neg_numeral_class.sub n num.One))\<close> for k :: int
   by (simp_all add: minus_numeral_eq_not_sub_one)
 
+definition take_bit_num :: \<open>nat \<Rightarrow> num \<Rightarrow> num option\<close>
+  where \<open>take_bit_num n m =
+    (if take_bit n (numeral m ::nat) = 0 then None else Some (num_of_nat (take_bit n (numeral m ::nat))))\<close>
+
+lemma take_bit_num_simps [code]:
+  \<open>take_bit_num 0 m = None\<close>
+  \<open>take_bit_num (Suc n) Num.One =
+    Some Num.One\<close>
+  \<open>take_bit_num (Suc n) (Num.Bit0 m) =
+    (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))\<close>
+  \<open>take_bit_num (Suc n) (Num.Bit1 m) =
+    Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q)\<close>
+  by (auto simp add: take_bit_num_def ac_simps mult_2 num_of_nat_double
+    take_bit_Suc_bit0 take_bit_Suc_bit1)
+
+lemma take_bit_num_numeral_simps:
+  \<open>take_bit_num (numeral n) Num.One =
+    Some Num.One\<close>
+  \<open>take_bit_num (numeral n) (Num.Bit0 m) =
+    (case take_bit_num (pred_numeral n) m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))\<close>
+  \<open>take_bit_num (numeral n) (Num.Bit1 m) =
+    Some (case take_bit_num (pred_numeral n) m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q)\<close>
+  by (auto simp add: take_bit_num_def ac_simps mult_2 num_of_nat_double
+    take_bit_numeral_bit0 take_bit_numeral_bit1)
+
+context semiring_bit_operations
+begin
+
+lemma take_bit_num_eq_None_imp:
+  \<open>take_bit m (numeral n) = 0\<close> if \<open>take_bit_num m n = None\<close>
+proof -
+  from that have \<open>take_bit m (numeral n :: nat) = 0\<close>
+    by (simp add: take_bit_num_def split: if_splits)
+  then have \<open>of_nat (take_bit m (numeral n)) = of_nat 0\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_take_bit)
+qed
+    
+lemma take_bit_num_eq_Some_imp:
+  \<open>take_bit m (numeral n) = numeral q\<close> if \<open>take_bit_num m n = Some q\<close>
+proof -
+  from that have \<open>take_bit m (numeral n :: nat) = numeral q\<close>
+    by (auto simp add: take_bit_num_def Num.numeral_num_of_nat_unfold split: if_splits)
+  then have \<open>of_nat (take_bit m (numeral n)) = of_nat (numeral q)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_take_bit)
+qed
+
+lemma take_bit_numeral_numeral:
+  \<open>take_bit (numeral m) (numeral n) =
+    (case take_bit_num (numeral m) n of None \<Rightarrow> 0 | Some q \<Rightarrow> numeral q)\<close>
+  by (auto split: option.split dest: take_bit_num_eq_None_imp take_bit_num_eq_Some_imp)
+
+end
+
+lemma take_bit_numeral_minus_numeral_int:
+  \<open>take_bit (numeral m) (- numeral n :: int) =
+    (case take_bit_num (numeral m) n of None \<Rightarrow> 0 | Some q \<Rightarrow> take_bit (numeral m) (2 ^ numeral m - numeral q))\<close> (is \<open>?lhs = ?rhs\<close>)
+proof (cases \<open>take_bit_num (numeral m) n\<close>)
+  case None
+  then show ?thesis
+    by (auto dest: take_bit_num_eq_None_imp [where ?'a = int] simp add: take_bit_eq_0_iff)
+next
+  case (Some q)
+  then have q: \<open>take_bit (numeral m) (numeral n :: int) = numeral q\<close>
+    by (auto dest: take_bit_num_eq_Some_imp)
+  let ?T = \<open>take_bit (numeral m) :: int \<Rightarrow> int\<close>
+  have *: \<open>?T (2 ^ numeral m) = ?T (?T 0)\<close>
+    by (simp add: take_bit_eq_0_iff)
+  have \<open>?lhs = ?T (0 - numeral n)\<close>
+    by simp
+  also have \<open>\<dots> = ?T (?T (?T 0) - ?T (?T (numeral n)))\<close>
+    by (simp only: take_bit_diff)
+  also have \<open>\<dots> = ?T (2 ^ numeral m - ?T (numeral n))\<close>
+    by (simp only: take_bit_diff flip: *)
+  also have \<open>\<dots> = ?rhs\<close>
+    by (simp add: q Some)
+  finally show ?thesis .
+qed
+
+declare take_bit_num_simps [simp] take_bit_num_numeral_simps [simp] take_bit_numeral_numeral [simp]
+  take_bit_numeral_minus_numeral_int [simp]
+
 
 subsection \<open>More properties\<close>
 
@@ -2705,7 +3200,7 @@
   moreover have \<open>take_bit n (take_bit n (k + 1) - 1) = take_bit n k\<close>
     by (simp add: take_bit_eq_mod mod_simps)
   ultimately show ?P
-    by (simp add: take_bit_minus_one_eq_mask)
+    by simp
 qed
 
 lemma take_bit_eq_mask_iff_exp_dvd:
@@ -2713,367 +3208,6 @@
   for k :: int
   by (simp add: take_bit_eq_mask_iff flip: take_bit_eq_0_iff)
 
-context ring_bit_operations
-begin
-
-lemma even_of_int_iff:
-  \<open>even (of_int k) \<longleftrightarrow> even k\<close>
-  by (induction k rule: int_bit_induct) simp_all
-
-lemma bit_of_int_iff [bit_simps]:
-  \<open>bit (of_int k) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit k n\<close>
-proof (cases \<open>possible_bit TYPE('a) n\<close>)
-  case False
-  then show ?thesis
-    by (simp add: impossible_bit)
-next
-  case True
-  then have \<open>bit (of_int k) n \<longleftrightarrow> bit k n\<close>
-  proof (induction k arbitrary: n rule: int_bit_induct)
-    case zero
-    then show ?case
-      by simp
-  next
-    case minus
-    then show ?case
-      by simp
-  next
-    case (even k)
-    then show ?case
-      using bit_double_iff [of \<open>of_int k\<close> n] Bit_Operations.bit_double_iff [of k n]
-      by (cases n) (auto simp add: ac_simps possible_bit_def dest: mult_not_zero)
-  next
-    case (odd k)
-    then show ?case
-      using bit_double_iff [of \<open>of_int k\<close> n]
-      by (cases n) (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Bit_Operations.bit_Suc possible_bit_def dest: mult_not_zero)
-  qed
-  with True show ?thesis
-    by simp
-qed
-
-lemma push_bit_of_int:
-  \<open>push_bit n (of_int k) = of_int (push_bit n k)\<close>
-  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
-
-lemma of_int_push_bit:
-  \<open>of_int (push_bit n k) = push_bit n (of_int k)\<close>
-  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
-
-lemma take_bit_of_int:
-  \<open>take_bit n (of_int k) = of_int (take_bit n k)\<close>
-  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_int_iff)
-
-lemma of_int_take_bit:
-  \<open>of_int (take_bit n k) = take_bit n (of_int k)\<close>
-  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_int_iff)
-
-lemma of_int_not_eq:
-  \<open>of_int (NOT k) = NOT (of_int k)\<close>
-  by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff)
-
-lemma of_int_not_numeral:
-  \<open>of_int (NOT (numeral k)) = NOT (numeral k)\<close>
-  by (simp add: local.of_int_not_eq)
-
-lemma of_int_and_eq:
-  \<open>of_int (k AND l) = of_int k AND of_int l\<close>
-  by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff)
-
-lemma of_int_or_eq:
-  \<open>of_int (k OR l) = of_int k OR of_int l\<close>
-  by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff)
-
-lemma of_int_xor_eq:
-  \<open>of_int (k XOR l) = of_int k XOR of_int l\<close>
-  by (rule bit_eqI) (simp add: bit_of_int_iff bit_xor_iff Bit_Operations.bit_xor_iff)
-
-lemma of_int_mask_eq:
-  \<open>of_int (mask n) = mask n\<close>
-  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_int_or_eq)
-
-end
-
-lemma take_bit_incr_eq:
-  \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
-  for k :: int
-proof -
-  from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
-    by (simp add: take_bit_eq_mod)
-  moreover have \<open>k mod 2 ^ n < 2 ^ n\<close>
-    by simp
-  ultimately have *: \<open>k mod 2 ^ n + 1 < 2 ^ n\<close>
-    by linarith
-  have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
-    by (simp add: mod_simps)
-  also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
-    using * by (simp add: zmod_trivial_iff)
-  finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
-  then show ?thesis
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_decr_eq:
-  \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
-  for k :: int
-proof -
-  from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
-    by (simp add: take_bit_eq_mod)
-  moreover have \<open>k mod 2 ^ n \<ge> 0\<close> \<open>k mod 2 ^ n < 2 ^ n\<close>
-    by simp_all
-  ultimately have *: \<open>k mod 2 ^ n > 0\<close>
-    by linarith
-  have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
-    by (simp add: mod_simps)
-  also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
-    by (simp add: zmod_trivial_iff)
-      (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
-  finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
-  then show ?thesis
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_int_greater_eq:
-  \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
-proof -
-  have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
-  proof (cases \<open>k > - (2 ^ n)\<close>)
-    case False
-    then have \<open>k + 2 ^ n \<le> 0\<close>
-      by simp
-    also note take_bit_nonnegative
-    finally show ?thesis .
-  next
-    case True
-    with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
-      by simp_all
-    then show ?thesis
-      by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
-  qed
-  then show ?thesis
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_int_less_eq:
-  \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
-  using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_int_less_eq_self_iff:
-  \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-  for k :: int
-proof
-  assume ?P
-  show ?Q
-  proof (rule ccontr)
-    assume \<open>\<not> 0 \<le> k\<close>
-    then have \<open>k < 0\<close>
-      by simp
-    with \<open>?P\<close>
-    have \<open>take_bit n k < 0\<close>
-      by (rule le_less_trans)
-    then show False
-      by simp
-  qed
-next
-  assume ?Q
-  then show ?P
-    by (simp add: take_bit_eq_mod zmod_le_nonneg_dividend)
-qed
-
-lemma take_bit_int_less_self_iff:
-  \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
-  for k :: int
-  by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
-    intro: order_trans [of 0 \<open>2 ^ n\<close> k])
-
-lemma take_bit_int_greater_self_iff:
-  \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
-  for k :: int
-  using take_bit_int_less_eq_self_iff [of n k] by auto
-
-lemma take_bit_int_greater_eq_self_iff:
-  \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
-  for k :: int
-  by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
-    dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
-
-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)
-
-lemma not_exp_less_eq_0_int [simp]:
-  \<open>\<not> 2 ^ n \<le> (0::int)\<close>
-  by (simp add: power_le_zero_eq)
-
-lemma half_nonnegative_int_iff [simp]:
-  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-proof (cases \<open>k \<ge> 0\<close>)
-  case True
-  then show ?thesis
-    by (auto simp add: divide_int_def sgn_1_pos)
-next
-  case False
-  then show ?thesis
-    by (auto simp add: divide_int_def not_le elim!: evenE)
-qed
-
-lemma half_negative_int_iff [simp]:
-  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
-lemma push_bit_of_Suc_0 [simp]:
-  "push_bit n (Suc 0) = 2 ^ n"
-  using push_bit_of_1 [where ?'a = nat] by simp
-
-lemma take_bit_of_Suc_0 [simp]:
-  "take_bit n (Suc 0) = of_bool (0 < n)"
-  using take_bit_of_1 [where ?'a = nat] by simp
-
-lemma drop_bit_of_Suc_0 [simp]:
-  "drop_bit n (Suc 0) = of_bool (n = 0)"
-  using drop_bit_of_1 [where ?'a = nat] by simp
-
-lemma int_bit_bound:
-  fixes k :: int
-  obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
-    and \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close>
-proof -
-  obtain q where *: \<open>\<And>m. q \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k q\<close>
-  proof (cases \<open>k \<ge> 0\<close>)
-    case True
-    moreover from power_gt_expt [of 2 \<open>nat k\<close>]
-    have \<open>nat k < 2 ^ nat k\<close>
-      by simp
-    then have \<open>int (nat k) < int (2 ^ nat k)\<close>
-      by (simp only: of_nat_less_iff)
-    ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
-      by simp
-    show thesis
-    proof (rule that [of \<open>nat k\<close>])
-      fix m
-      assume \<open>nat k \<le> m\<close>
-      then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
-        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
-    qed
-  next
-    case False
-    moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
-    have \<open>nat (- k) < 2 ^ nat (- k)\<close>
-      by simp
-    then have \<open>int (nat (- k)) < int (2 ^ nat (- k))\<close>
-      by (simp only: of_nat_less_iff)
-    ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
-      by (subst div_pos_neg_trivial) simp_all
-    then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
-      by simp
-    show thesis
-    proof (rule that [of \<open>nat (- k)\<close>])
-      fix m
-      assume \<open>nat (- k) \<le> m\<close>
-      then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
-        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
-    qed
-  qed
-  show thesis
-  proof (cases \<open>\<forall>m. bit k m \<longleftrightarrow> bit k q\<close>)
-    case True
-    then have \<open>bit k 0 \<longleftrightarrow> bit k q\<close>
-      by blast
-    with True that [of 0] show thesis
-      by simp
-  next
-    case False
-    then obtain r where **: \<open>bit k r \<noteq> bit k q\<close>
-      by blast
-    have \<open>r < q\<close>
-      by (rule ccontr) (use * [of r] ** in simp)
-    define N where \<open>N = {n. n < q \<and> bit k n \<noteq> bit k q}\<close>
-    moreover have \<open>finite N\<close> \<open>r \<in> N\<close>
-      using ** N_def \<open>r < q\<close> by auto
-    moreover define n where \<open>n = Suc (Max N)\<close>
-    ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
-      apply auto
-         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
-        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
-        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
-      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
-      done
-    have \<open>bit k (Max N) \<noteq> bit k n\<close>
-      by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
-    show thesis apply (rule that [of n])
-      using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
-      using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
-  qed
-qed
-
-context semiring_bit_operations
-begin
-
-lemma of_nat_and_eq:
-  \<open>of_nat (m AND n) = of_nat m AND of_nat n\<close>
-  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff)
-
-lemma of_nat_or_eq:
-  \<open>of_nat (m OR n) = of_nat m OR of_nat n\<close>
-  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff)
-
-lemma of_nat_xor_eq:
-  \<open>of_nat (m XOR n) = of_nat m XOR of_nat n\<close>
-  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff)
-
-end
-
-context ring_bit_operations
-begin
-
-lemma of_nat_mask_eq:
-  \<open>of_nat (mask n) = mask n\<close>
-  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)
-
-end
-
-lemma Suc_mask_eq_exp:
-  \<open>Suc (mask n) = 2 ^ n\<close>
-  by (simp add: mask_eq_exp_minus_1)
-
-lemma less_eq_mask:
-  \<open>n \<le> mask n\<close>
-  by (simp add: mask_eq_exp_minus_1 le_diff_conv2)
-    (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0)
-
-lemma less_mask:
-  \<open>n < mask n\<close> if \<open>Suc 0 < n\<close>
-proof -
-  define m where \<open>m = n - 2\<close>
-  with that have *: \<open>n = m + 2\<close>
-    by simp
-  have \<open>Suc (Suc (Suc m)) < 4 * 2 ^ m\<close>
-    by (induction m) simp_all
-  then have \<open>Suc (m + 2) < Suc (mask (m + 2))\<close>
-    by (simp add: Suc_mask_eq_exp)
-  then have \<open>m + 2 < mask (m + 2)\<close>
-    by (simp add: less_le)
-  with * show ?thesis
-    by simp
-qed
-
 
 subsection \<open>Bit concatenation\<close>
 
@@ -3203,7 +3337,7 @@
 
 lemma signed_take_bit_of_minus_1 [simp]:
   \<open>signed_take_bit n (- 1) = - 1\<close>
-  by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask mask_eq_exp_minus_1 possible_bit_def)
+  by (simp add: signed_take_bit_def mask_eq_exp_minus_1 possible_bit_def)
 
 lemma signed_take_bit_Suc_1 [simp]:
   \<open>signed_take_bit (Suc n) 1 = 1\<close>
@@ -3246,7 +3380,7 @@
 
 lemma signed_take_bit_eq_concat_bit:
   \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
-  by (simp add: concat_bit_def signed_take_bit_def push_bit_minus_one_eq_not_mask)
+  by (simp add: concat_bit_def signed_take_bit_def)
 
 lemma signed_take_bit_add:
   \<open>signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\<close>
@@ -3449,7 +3583,8 @@
        simp flip: push_bit_minus_one_eq_not_mask)
   show ?thesis
     by (rule bit_eqI)
-      (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
+      (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff
+        bit_mask_iff bit_or_iff simp del: push_bit_minus_one_eq_not_mask)
 qed
 
 
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -16,6 +16,14 @@
   by a corresponding \<open>export_code\<close> command.
 \<close>
 
+lemma take_bit_num_code [code]: \<comment> \<open>TODO: move\<close>
+  \<open>take_bit_num n m = (case (n, m)
+   of (0, _) \<Rightarrow> None
+    | (Suc n, Num.One) \<Rightarrow> Some Num.One
+    | (Suc n, Num.Bit0 m) \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))
+    | (Suc n, Num.Bit1 m) \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
+  by (cases n; cases m) simp_all
+
 export_code _ checking SML OCaml? Haskell? Scala
 
 end
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Euclidean_Division.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -2110,6 +2110,30 @@
 instance int :: unique_euclidean_ring_with_nat
   by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
 
+lemma zdiv_zmult2_eq:
+  \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+  case True
+  with that show ?thesis
+    using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+  case False
+  with that show ?thesis
+    using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
+lemma zmod_zmult2_eq:
+  \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+  case True
+  with that show ?thesis
+    using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+  case False
+  with that show ?thesis
+    using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
 
 subsection \<open>Code generation\<close>
 
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -113,4 +113,17 @@
 end
 \<close>
 
+
+subsection \<open>One candidate which needs special treatment\<close>
+
+lemma take_bit_num_code [code]:
+  \<open>take_bit_num n Num.One =
+    (case n of 0 \<Rightarrow> None | Suc n \<Rightarrow> Some Num.One)\<close>
+  \<open>take_bit_num n (Num.Bit0 m) =
+    (case n of 0 \<Rightarrow> None | Suc n \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q)))\<close>
+  \<open>take_bit_num n (Num.Bit1 m) =
+    (case n of 0 \<Rightarrow> None | Suc n \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
+    apply (cases n; simp)+
+  done
+
 end
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Library/Signed_Division.thy
--- a/src/HOL/Library/Signed_Division.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Library/Signed_Division.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -141,4 +141,28 @@
     "\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"
   by (clarsimp simp: smod_int_alt_def zsgn_def)
 
+lemma minus_sdiv_eq [simp]:
+  \<open>- k sdiv l = - (k sdiv l)\<close> for k l :: int
+  by (simp add: signed_divide_int_def)
+
+lemma sdiv_minus_eq [simp]:
+  \<open>k sdiv - l = - (k sdiv l)\<close> for k l :: int
+  by (simp add: signed_divide_int_def)
+
+lemma sdiv_int_numeral_numeral [simp]:
+  \<open>numeral m sdiv numeral n = numeral m div (numeral n :: int)\<close>
+  by (simp add: signed_divide_int_def)
+
+lemma minus_smod_eq [simp]:
+  \<open>- k smod l = - (k smod l)\<close> for k l :: int
+  by (simp add: smod_int_alt_def)
+
+lemma smod_minus_eq [simp]:
+  \<open>k smod - l = k smod l\<close> for k l :: int
+  by (simp add: smod_int_alt_def)
+
+lemma smod_int_numeral_numeral [simp]:
+  \<open>numeral m smod numeral n = numeral m mod (numeral n :: int)\<close>
+  by (simp add: smod_int_alt_def) 
+
 end
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Library/Word.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -876,7 +876,8 @@
     by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
   show \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close>
     for m n :: nat
-    by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)
+    by transfer
+      (simp flip: drop_bit_eq_div mask_eq_exp_minus_1 add: bit_simps even_drop_bit_iff_not_bit not_less)
   show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n - m))\<close>
     for a :: \<open>'a word\<close> and m n :: nat
   proof transfer
@@ -1109,6 +1110,10 @@
 context semiring_bit_operations
 begin
 
+lemma unsigned_minus_1_eq_mask:
+  \<open>unsigned (- 1 :: 'b::len word) = mask LENGTH('b)\<close>
+  by (transfer fixing: mask) (simp add: nat_mask_eq of_nat_mask_eq)
+
 lemma unsigned_push_bit_eq:
   \<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close>
   for w :: \<open>'b::len word\<close>
@@ -1251,7 +1256,7 @@
 lemma signed_not_eq:
   \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
   for w :: \<open>'b::len word\<close>
-  by (simp add: bit_eq_iff bit_simps possible_bit_min possible_bit_less_imp min_less_iff_disj)
+  by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj)
     (auto simp: min_def)
 
 lemma signed_and_eq:
@@ -1359,7 +1364,7 @@
 lemma signed_ucast_eq:
   \<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\<close>
   for w :: \<open>'b::len word\<close>
-  by (simp add: bit_eq_iff bit_simps possible_bit_min min_less_iff_disj)
+  by (simp add: bit_eq_iff bit_simps min_less_iff_disj)
 
 lemma signed_scast_eq:
   \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
@@ -1536,6 +1541,58 @@
 
 subsection \<open>Arithmetic operations\<close>
 
+lemma div_word_self:
+  \<open>w div w = 1\<close> if \<open>w \<noteq> 0\<close> for w :: \<open>'a::len word\<close>
+  using that by transfer simp
+
+lemma mod_word_self [simp]:
+  \<open>w mod w = 0\<close> for w :: \<open>'a::len word\<close>
+  apply (cases \<open>w = 0\<close>)
+  apply auto
+  using div_mult_mod_eq [of w w] by (simp add: div_word_self)
+
+lemma div_word_less:
+  \<open>w div v = 0\<close> if \<open>w < v\<close> for w v :: \<open>'a::len word\<close>
+  using that by transfer simp
+
+lemma mod_word_less:
+  \<open>w mod v = w\<close> if \<open>w < v\<close> for w v :: \<open>'a::len word\<close>
+  using div_mult_mod_eq [of w v] using that by (simp add: div_word_less)
+
+lemma div_word_one [simp]:
+  \<open>1 div w = of_bool (w = 1)\<close> for w :: \<open>'a::len word\<close>
+proof transfer
+  fix k :: int
+  show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) 1 div take_bit LENGTH('a) k) =
+         take_bit LENGTH('a) (of_bool (take_bit LENGTH('a) k = take_bit LENGTH('a) 1))\<close>
+  proof (cases \<open>take_bit LENGTH('a) k > 1\<close>)
+    case False
+    with take_bit_nonnegative [of \<open>LENGTH('a)\<close> k]
+    have \<open>take_bit LENGTH('a) k = 0 \<or> take_bit LENGTH('a) k = 1\<close>
+      by linarith
+    then show ?thesis
+      by auto
+  next
+    case True
+    then show ?thesis
+      by simp
+  qed
+qed
+
+lemma mod_word_one [simp]:
+  \<open>1 mod w = 1 - w * of_bool (w = 1)\<close> for w :: \<open>'a::len word\<close>
+  using div_mult_mod_eq [of 1 w] by simp
+
+lemma div_word_by_minus_1_eq [simp]:
+  \<open>w div - 1 = of_bool (w = - 1)\<close> for w :: \<open>'a::len word\<close>
+  by (auto intro: div_word_less simp add: div_word_self word_order.not_eq_extremum)
+
+lemma mod_word_by_minus_1_eq [simp]:
+  \<open>w mod - 1 = w * of_bool (w < - 1)\<close> for w :: \<open>'a::len word\<close>
+  apply (cases \<open>w = - 1\<close>)
+   apply (auto simp add: word_order.not_eq_extremum)
+  using div_mult_mod_eq [of w \<open>- 1\<close>] by simp
+
 text \<open>Legacy theorems:\<close>
 
 lemma word_add_def [code]:
@@ -1664,7 +1721,7 @@
   by (fact word_coorder.extremum)
 
 lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
-  by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 )
+  by transfer (simp add: mask_eq_exp_minus_1)
 
 lemma word_n1_ge [simp]: "y \<le> -1"
   for y :: "'a::len word"
@@ -2217,6 +2274,11 @@
   for w :: "'a::len word"
   unfolding word_size by (rule order_trans [OF _ sint_ge])
 
+lemma word_unat_eq_iff:
+  \<open>v = w \<longleftrightarrow> unat v = unat w\<close>
+  for v w :: \<open>'a::len word\<close>
+  by (fact word_eq_iff_unsigned)
+
 
 subsection \<open>Testing bits\<close>
 
@@ -2415,9 +2477,123 @@
     by (simp add: bit_iff_odd_drop_bit drop_bit_take_bit odd_iff_mod_2_eq_one)
 qed auto
 
+lemma unat_div:
+  \<open>unat (x div y) = unat x div unat y\<close>
+  by (fact unat_div_distrib)
+
+lemma unat_mod:
+  \<open>unat (x mod y) = unat x mod unat y\<close>
+  by (fact unat_mod_distrib)
+
 
 subsection \<open>Word Arithmetic\<close>
 
+lemmas less_eq_word_numeral_numeral [simp] =
+  word_le_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_word_numeral_numeral [simp] =
+  word_less_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_eq_word_minus_numeral_numeral [simp] =
+  word_le_def [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_word_minus_numeral_numeral [simp] =
+  word_less_def [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_eq_word_numeral_minus_numeral [simp] =
+  word_le_def [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_word_numeral_minus_numeral [simp] =
+  word_less_def [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_eq_word_minus_numeral_minus_numeral [simp] =
+  word_le_def [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_word_minus_numeral_minus_numeral [simp] =
+  word_less_def [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_word_numeral_minus_1 [simp] =
+  word_less_def [of \<open>numeral a\<close> \<open>- 1\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas less_word_minus_numeral_minus_1 [simp] =
+  word_less_def [of \<open>- numeral a\<close> \<open>- 1\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+
+lemmas sless_eq_word_numeral_numeral [simp] =
+  word_sle_eq [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_word_numeral_numeral [simp] =
+  word_sless_alt [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_eq_word_minus_numeral_numeral [simp] =
+  word_sle_eq [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_word_minus_numeral_numeral [simp] =
+  word_sless_alt [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_eq_word_numeral_minus_numeral [simp] =
+  word_sle_eq [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_word_numeral_minus_numeral [simp] =
+  word_sless_alt [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_eq_word_minus_numeral_minus_numeral [simp] =
+  word_sle_eq [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+lemmas sless_word_minus_numeral_minus_numeral [simp] =
+  word_sless_alt [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
+  for a b
+
+lemmas div_word_numeral_numeral [simp] =
+  word_div_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas div_word_minus_numeral_numeral [simp] =
+  word_div_def [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas div_word_numeral_minus_numeral [simp] =
+  word_div_def [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas div_word_minus_numeral_minus_numeral [simp] =
+  word_div_def [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas div_word_minus_1_numeral [simp] =
+  word_div_def [of \<open>- 1\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas div_word_minus_1_minus_numeral [simp] =
+  word_div_def [of \<open>- 1\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+
+lemmas mod_word_numeral_numeral [simp] =
+  word_mod_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas mod_word_minus_numeral_numeral [simp] =
+  word_mod_def [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas mod_word_numeral_minus_numeral [simp] =
+  word_mod_def [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas mod_word_minus_numeral_minus_numeral [simp] =
+  word_mod_def [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas mod_word_minus_1_numeral [simp] =
+  word_mod_def [of \<open>- 1\<close> \<open>numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+lemmas mod_word_minus_1_minus_numeral [simp] =
+  word_mod_def [of \<open>- 1\<close> \<open>- numeral b\<close>, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1]
+  for a b
+
+lemma signed_drop_bit_of_1 [simp]:
+  \<open>signed_drop_bit n (1 :: 'a::len word) = of_bool (LENGTH('a) = 1 \<or> n = 0)\<close>
+  apply (transfer fixing: n)
+  apply (cases \<open>LENGTH('a)\<close>)
+   apply (auto simp add: take_bit_signed_take_bit)
+  apply (auto simp add: take_bit_drop_bit gr0_conv_Suc simp flip: take_bit_eq_self_iff_drop_bit_eq_0)
+  done
+
+lemma take_bit_word_beyond_length_eq:
+  \<open>take_bit n w = w\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  using that by transfer simp
+
 lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b
 lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b
 lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b
@@ -2434,6 +2610,52 @@
 lemmas unat_eq_0 = unat_0_iff
 lemmas unat_eq_zero = unat_0_iff
 
+lemma mask_1: "mask 1 = 1"
+  by simp
+
+lemma mask_Suc_0: "mask (Suc 0) = 1"
+  by simp
+
+lemma bin_last_bintrunc: "odd (take_bit l n) \<longleftrightarrow> l > 0 \<and> odd n"
+  by simp
+
+lemma push_bit_word_beyond [simp]:
+  \<open>push_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  using that by (transfer fixing: n) (simp add: take_bit_push_bit)
+
+lemma drop_bit_word_beyond [simp]:
+  \<open>drop_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  using that by (transfer fixing: n) (simp add: drop_bit_take_bit)
+
+lemma signed_drop_bit_beyond:
+  \<open>signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)\<close>
+  if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that)
+
+lemma take_bit_numeral_minus_numeral_word [simp]:
+  \<open>take_bit (numeral m) (- numeral n :: 'a::len word) =
+    (case take_bit_num (numeral m) n of None \<Rightarrow> 0 | Some q \<Rightarrow> take_bit (numeral m) (2 ^ numeral m - numeral q))\<close> (is \<open>?lhs = ?rhs\<close>)
+proof (cases \<open>LENGTH('a) \<le> numeral m\<close>)
+  case True
+  then have *: \<open>(take_bit (numeral m) :: 'a word \<Rightarrow> 'a word) = id\<close>
+    by (simp add: fun_eq_iff take_bit_word_eq_self)
+  have **: \<open>2 ^ numeral m = (0 :: 'a word)\<close>
+    using True by (simp flip: exp_eq_zero_iff)
+  show ?thesis
+    by (auto simp only: * ** split: option.split
+      dest!: take_bit_num_eq_None_imp [where ?'a = \<open>'a word\<close>] take_bit_num_eq_Some_imp [where ?'a = \<open>'a word\<close>])
+      simp_all
+next
+  case False
+  then show ?thesis
+    by (transfer fixing: m n) simp
+qed
+
+lemma of_nat_inverse:
+  \<open>word_of_nat r = a \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> unat a = r\<close>
+  for a :: \<open>'a::len word\<close>
+  by (metis id_apply of_nat_eq_id take_bit_nat_eq_self_iff unsigned_of_nat)
+
 
 subsection \<open>Transferring goals from words to ints\<close>
 
@@ -2715,14 +2937,54 @@
   for a b :: "'a::len word"
   using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
 
-
-subsection \<open>Definition of \<open>uint_arith\<close>\<close>
-
 lemma word_of_int_inverse:
   "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> uint a = r"
   for a :: "'a::len word"
   by transfer (simp add: take_bit_int_eq_self)
 
+lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
+  for x :: "'a::len word"
+  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
+
+lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
+  for x :: "'a::len word"
+  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
+
+lemma un_ui_le:
+  \<open>unat a \<le> unat b \<longleftrightarrow> uint a \<le> uint b\<close>
+  by transfer (simp add: nat_le_iff) 
+
+lemma unat_plus_if':
+  \<open>unat (a + b) =
+    (if unat a + unat b < 2 ^ LENGTH('a)
+    then unat a + unat b
+    else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
+  apply (auto simp add: not_less le_iff_add)
+   apply (metis (mono_tags, lifting) of_nat_add of_nat_unat take_bit_nat_eq_self_iff unsigned_less unsigned_of_nat unsigned_word_eqI)
+  apply (smt (verit, ccfv_SIG) dbl_simps(3) dbl_simps(5) numerals(1) of_nat_0_le_iff of_nat_add of_nat_eq_iff of_nat_numeral of_nat_power of_nat_unat uint_plus_if' unsigned_1)
+  done
+
+lemma unat_sub_if_size:
+  "unat (x - y) =
+    (if unat y \<le> unat x
+     then unat x - unat y
+     else unat x + 2 ^ size x - unat y)"
+proof -
+  { assume xy: "\<not> uint y \<le> uint x"
+    have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)"
+      by simp
+    also have "... = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
+      by (simp add: nat_diff_distrib')
+    also have "... = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
+      by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less)
+    finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
+  }
+  then show ?thesis
+    by (simp add: word_size) (metis nat_diff_distrib' uint_sub_if' un_ui_le unat_eq_nat_uint unsigned_greater_eq)
+qed
+
+lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
+
 lemma uint_split:
   "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
   for x :: "'a::len word"
@@ -2733,6 +2995,20 @@
   for x :: "'a::len word"
   by (auto simp add: unsigned_of_int take_bit_int_eq_self)
 
+
+subsection \<open>Some proof tool support\<close>
+
+\<comment> \<open>use this to stop, eg. \<open>2 ^ LENGTH(32)\<close> being simplified\<close>
+lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
+  by auto
+
+lemmas unat_splits = unat_split unat_split_asm
+
+lemmas unat_arith_simps =
+  word_le_nat_alt word_less_nat_alt
+  word_unat_eq_iff
+  unat_sub_if' unat_plus_if' unat_div unat_mod
+
 lemmas uint_splits = uint_split uint_split_asm
 
 lemmas uint_arith_simps =
@@ -2740,14 +3016,45 @@
   word_uint_eq_iff
   uint_sub_if' uint_plus_if'
 
-\<comment> \<open>use this to stop, eg. \<open>2 ^ LENGTH(32)\<close> being simplified\<close>
-lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
-  by auto
+\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
+ML \<open>
+val unat_arith_simpset =
+  @{context} (* TODO: completely explicitly determined simpset *)
+  |> fold Simplifier.add_simp @{thms unat_arith_simps}
+  |> fold Splitter.add_split @{thms if_split_asm}
+  |> fold Simplifier.add_cong @{thms power_False_cong}
+  |> simpset_of
+
+fun unat_arith_tacs ctxt =
+  let
+    fun arith_tac' n t =
+      Arith_Data.arith_tac ctxt n t
+        handle Cooper.COOPER _ => Seq.empty;
+  in
+    [ clarify_tac ctxt 1,
+      full_simp_tac (put_simpset unat_arith_simpset ctxt) 1,
+      ALLGOALS (full_simp_tac
+        (put_simpset HOL_ss ctxt
+          |> fold Splitter.add_split @{thms unat_splits}
+          |> fold Simplifier.add_cong @{thms power_False_cong})),
+      rewrite_goals_tac ctxt @{thms word_size},
+      ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
+                         REPEAT (eresolve_tac ctxt [conjE] n) THEN
+                         REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)),
+      TRYALL arith_tac' ]
+  end
+
+fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
+\<close>
+
+method_setup unat_arith =
+  \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
+  "solving word arithmetic via natural numbers and arith"
 
 \<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close>
 ML \<open>
 val uint_arith_simpset =
-  @{context}
+  @{context} (* TODO: completely explicitly determined simpset *)
   |> fold Simplifier.add_simp @{thms uint_arith_simps}
   |> fold Splitter.add_split @{thms if_split_asm}
   |> fold Simplifier.add_cong @{thms power_False_cong}
@@ -2786,13 +3093,13 @@
 
 lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x"
   for x y :: "'a::len word"
-  unfolding word_size by uint_arith
+  by (auto simp add: word_size word_le_def uint_add_lem uint_sub_lem)
 
 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
 
 lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x"
   for x y :: "'a::len word"
-  by uint_arith
+  by (auto simp add: word_size word_le_def uint_add_lem uint_sub_lem)
 
 lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ LENGTH('a)"
   for x y :: "'a::len word"
@@ -2809,19 +3116,20 @@
 
 lemma word_less_sub1: "x \<noteq> 0 \<Longrightarrow> 1 < x \<longleftrightarrow> 0 < x - 1"
   for x :: "'a::len word"
-  by uint_arith
+  by transfer (simp add: take_bit_decr_eq) 
 
 lemma word_le_sub1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> x \<longleftrightarrow> 0 \<le> x - 1"
   for x :: "'a::len word"
-  by uint_arith
+  by transfer (simp add: int_one_le_iff_zero_less less_le)
 
 lemma sub_wrap_lt: "x < x - z \<longleftrightarrow> x < z"
   for x z :: "'a::len word"
-  by uint_arith
-
+  by (simp add: word_less_def uint_sub_lem)
+   (meson linorder_not_le uint_minus_simple_iff uint_sub_lem word_less_iff_unsigned)
+  
 lemma sub_wrap: "x \<le> x - z \<longleftrightarrow> z = 0 \<or> x < z"
   for x z :: "'a::len word"
-  by uint_arith
+  by (simp add: le_less sub_wrap_lt ac_simps)
 
 lemma plus_minus_not_NULL_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> x + c \<noteq> 0"
   for x ab c :: "'a::len word"
@@ -3059,123 +3367,18 @@
   for x y :: "'a::len word"
   by (metis mod_less unat_word_ariths(2) unsigned_less)
 
-lemma unat_plus_if':
-  \<open>unat (a + b) =
-    (if unat a + unat b < 2 ^ LENGTH('a)
-    then unat a + unat b
-    else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
-  apply (auto simp: unat_word_ariths not_less le_iff_add)
-  by (metis add.commute add_less_cancel_right add_strict_mono mod_less unsigned_less)
-
 lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
   for a b x :: "'a::len word"
   using word_le_plus_either by blast
 
-lemmas un_ui_le =
-  trans [OF word_le_nat_alt [symmetric] word_le_def]
-
-lemma unat_sub_if_size:
-  "unat (x - y) =
-    (if unat y \<le> unat x
-     then unat x - unat y
-     else unat x + 2 ^ size x - unat y)"
-proof -
-  { assume xy: "\<not> uint y \<le> uint x"
-    have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)"
-      by simp
-    also have "... = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
-      by (simp add: nat_diff_distrib')
-    also have "... = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
-      by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less)
-    finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
-  }
-  then show ?thesis
-  unfolding word_size
-  by (metis nat_diff_distrib' uint_sub_if' un_ui_le unat_eq_nat_uint unsigned_greater_eq)
-qed
-
-lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
-
 lemma uint_div:
   \<open>uint (x div y) = uint x div uint y\<close>
   by (fact uint_div_distrib)
 
-lemma unat_div:
-  \<open>unat (x div y) = unat x div unat y\<close>
-  by (fact unat_div_distrib)
-
 lemma uint_mod:
   \<open>uint (x mod y) = uint x mod uint y\<close>
   by (fact uint_mod_distrib)
   
-lemma unat_mod:
-  \<open>unat (x mod y) = unat x mod unat y\<close>
-  by (fact unat_mod_distrib)
-
-
-text \<open>Definition of \<open>unat_arith\<close> tactic\<close>
-
-lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
-  for x :: "'a::len word"
-  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
-
-lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
-  for x :: "'a::len word"
-  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
-
-lemma of_nat_inverse:
-  \<open>word_of_nat r = a \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> unat a = r\<close>
-  for a :: \<open>'a::len word\<close>
-  by (metis mod_if unat_of_nat)
-
-lemma word_unat_eq_iff:
-  \<open>v = w \<longleftrightarrow> unat v = unat w\<close>
-  for v w :: \<open>'a::len word\<close>
-  by (fact word_eq_iff_unsigned)
-
-lemmas unat_splits = unat_split unat_split_asm
-
-lemmas unat_arith_simps =
-  word_le_nat_alt word_less_nat_alt
-  word_unat_eq_iff
-  unat_sub_if' unat_plus_if' unat_div unat_mod
-
-\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
-ML \<open>
-val unat_arith_simpset =
-  @{context} (* TODO: completely explicitly determined simpset *)
-  |> fold Simplifier.del_simp @{thms unsigned_of_nat unsigned_of_int}
-  |> fold Simplifier.add_simp @{thms unat_arith_simps}
-  |> fold Splitter.add_split @{thms if_split_asm}
-  |> fold Simplifier.add_cong @{thms power_False_cong}
-  |> simpset_of
-
-fun unat_arith_tacs ctxt =
-  let
-    fun arith_tac' n t =
-      Arith_Data.arith_tac ctxt n t
-        handle Cooper.COOPER _ => Seq.empty;
-  in
-    [ clarify_tac ctxt 1,
-      full_simp_tac (put_simpset unat_arith_simpset ctxt) 1,
-      ALLGOALS (full_simp_tac
-        (put_simpset HOL_ss ctxt
-          |> fold Splitter.add_split @{thms unat_splits}
-          |> fold Simplifier.add_cong @{thms power_False_cong})),
-      rewrite_goals_tac ctxt @{thms word_size},
-      ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
-                         REPEAT (eresolve_tac ctxt [conjE] n) THEN
-                         REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)),
-      TRYALL arith_tac' ]
-  end
-
-fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
-\<close>
-
-method_setup unat_arith =
-  \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
-  "solving word arithmetic via natural numbers and arith"
-
 lemma no_plus_overflow_unat_size: "x \<le> x + y \<longleftrightarrow> unat x + unat y < 2 ^ size x"
   for x y :: "'a::len word"
   unfolding word_size by unat_arith
@@ -3641,7 +3844,7 @@
 end
 
 lemma mask_bin: "mask n = word_of_int (take_bit n (- 1))"
-  by transfer (simp add: take_bit_minus_one_eq_mask) 
+  by transfer simp 
 
 lemma and_mask_bintr: "w AND mask n = word_of_int (take_bit n (uint w))"
   by transfer (simp add: ac_simps take_bit_eq_mask)
@@ -3723,7 +3926,7 @@
   by (transfer; simp add: take_bit_eq_mod mod_simps)+
 
 lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)"
-  by transfer (simp add: take_bit_minus_one_eq_mask)
+  by transfer simp
 
 
 subsubsection \<open>Slices\<close>
@@ -4266,36 +4469,10 @@
   finally show ?thesis .
 qed
 
-
-subsection \<open>More\<close>
-
-lemma mask_1: "mask 1 = 1"
-  by simp
-
-lemma mask_Suc_0: "mask (Suc 0) = 1"
-  by simp
-
-lemma bin_last_bintrunc: "odd (take_bit l n) \<longleftrightarrow> l > 0 \<and> odd n"
-  by simp
-
-
-lemma push_bit_word_beyond [simp]:
-  \<open>push_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
-  using that by (transfer fixing: n) (simp add: take_bit_push_bit)
-
-lemma drop_bit_word_beyond [simp]:
-  \<open>drop_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
-  using that by (transfer fixing: n) (simp add: drop_bit_take_bit)
-
-lemma signed_drop_bit_beyond:
-  \<open>signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)\<close>
-  if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
-  by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that)
-
 end
 
 
-subsection \<open>SMT support\<close>
+subsection \<open>Tool support\<close>
 
 ML_file \<open>Tools/smt_word.ML\<close>
 
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Num.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -1490,4 +1490,41 @@
 
 lemmas [code_post] = Num.inc.simps
 
+
+subsection \<open>More on auxiliary conversion\<close>
+
+context semiring_1
+begin
+
+lemma numeral_num_of_nat_unfold:
+  \<open>numeral (num_of_nat n) = (if n = 0 then 1 else of_nat n)\<close>
+  by (induction n) (simp_all add: numeral_inc ac_simps)
+
+lemma num_of_nat_numeral_eq [simp]:
+  \<open>num_of_nat (numeral q) = q\<close>
+proof (induction q)
+  case One
+  then show ?case
+    by simp
+next
+  case (Bit0 q)
+  then show ?case
+    apply (simp only: Num.numeral_Bit0 Num.numeral_add)
+    apply (subst num_of_nat_double)
+     apply simp_all
+    done
+next
+  case (Bit1 q)
+  then show ?case
+    apply (simp only: Num.numeral_Bit1 Num.numeral_add)
+    apply (subst num_of_nat_plus_distrib)
+      apply simp
+     apply simp
+    apply (subst num_of_nat_double)
+     apply simp_all
+    done
+qed
+
 end
+
+end
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Parity.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -241,16 +241,6 @@
   qed
 qed
 
-lemma even_of_nat [simp]:
-  "even (of_nat a) \<longleftrightarrow> even a"
-proof -
-  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
-    by simp
-  also have "\<dots> \<longleftrightarrow> even a"
-    by (simp only: of_nat_dvd_iff)
-  finally show ?thesis .
-qed
-
 lemma even_succ_div_two [simp]:
   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
@@ -427,6 +417,10 @@
 context semiring_parity
 begin
 
+lemma even_of_nat_iff [simp]:
+  "even (of_nat n) \<longleftrightarrow> even n"
+  by (induction n) simp_all
+
 lemma even_sum_iff:
   \<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close>
 using that proof (induction A)
@@ -639,31 +633,7 @@
   by simp
 
 lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
-  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
-
-lemma zdiv_zmult2_eq:
-  \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
-proof (cases \<open>b \<ge> 0\<close>)
-  case True
-  with that show ?thesis
-    using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
-next
-  case False
-  with that show ?thesis
-    using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
-qed
-
-lemma zmod_zmult2_eq:
-  \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
-proof (cases \<open>b \<ge> 0\<close>)
-  case True
-  with that show ?thesis
-    using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
-next
-  case False
-  with that show ?thesis
-    using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
-qed
+  by (simp add: even_of_nat_iff [of "nat k", where ?'a = int, symmetric])
 
 context
   assumes "SORT_CONSTRAINT('a::division_ring)"
@@ -702,4 +672,6 @@
 code_identifier
   code_module Parity \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
+lemmas even_of_nat = even_of_nat_iff
+
 end
diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Transcendental.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -4148,9 +4148,9 @@
 lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>i. odd i \<and> x = of_int i * (pi/2))"
 proof -
   have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"
-    by (metis even_of_nat of_int_of_nat_eq)
+    by (metis even_of_nat_iff of_int_of_nat_eq)
   have 2: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> - (real n * pi) = real_of_int i * pi"
-    by (metis even_minus even_of_nat mult.commute mult_minus_right of_int_minus of_int_of_nat_eq)
+    by (metis even_minus even_of_nat_iff mult.commute mult_minus_right of_int_minus of_int_of_nat_eq)
   have 3: "\<lbrakk>odd i;  \<forall>n. even n \<or> real_of_int i \<noteq> - (real n)\<rbrakk>
          \<Longrightarrow> \<exists>n. odd n \<and> real_of_int i = real n" for i
     by (cases i rule: int_cases2) auto
@@ -4167,7 +4167,7 @@
   proof cases
     case plus
     then show ?rhs
-      by (metis even_of_nat of_int_of_nat_eq)
+      by (metis even_of_nat_iff of_int_of_nat_eq)
   next
     case minus
     then show ?thesis