diff --git a/lib/Word_Lib/Ancient_Numeral.thy b/lib/Word_Lib/Ancient_Numeral.thy
deleted file mode 100644
index 88d054072..000000000
--- a/lib/Word_Lib/Ancient_Numeral.thy
+++ /dev/null
@@ -1,237 +0,0 @@
-(*
- * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
- *
- * SPDX-License-Identifier: BSD-2-Clause
- *)
-
-theory Ancient_Numeral
-  imports Main Reversed_Bit_Lists Legacy_Aliases
-begin
-
-definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int"  (infixl "BIT" 90)
-  where "k BIT b = (if b then 1 else 0) + k + k"
-
-lemma Bit_B0: "k BIT False = k + k"
-   by (simp add: Bit_def)
-
-lemma Bit_B1: "k BIT True = k + k + 1"
-   by (simp add: Bit_def)
-
-lemma Bit_B0_2t: "k BIT False = 2 * k"
-  by (rule trans, rule Bit_B0) simp
-
-lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
-  by (rule trans, rule Bit_B1) simp
-
-lemma uminus_Bit_eq:
-  "- k BIT b = (- k - of_bool b) BIT b"
-  by (cases b) (simp_all add: Bit_def)
-
-lemma power_BIT: "2 ^ Suc n - 1 = (2 ^ n - 1) BIT True"
-  by (simp add: Bit_B1)
-
-lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w"
-  by (simp add: Bit_def)
-
-lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
-  by (simp add: Bit_def)
-
-lemma even_BIT [simp]: "even (x BIT b) \<longleftrightarrow> \<not> b"
-  by (simp add: Bit_def)
-
-lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b"
-  by simp
-
-lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
-  by (auto simp: Bit_def) arith+
-
-lemma BIT_bin_simps [simp]:
-  "numeral k BIT False = numeral (Num.Bit0 k)"
-  "numeral k BIT True = numeral (Num.Bit1 k)"
-  "(- numeral k) BIT False = - numeral (Num.Bit0 k)"
-  "(- numeral k) BIT True = - numeral (Num.BitM k)"
-  by (simp_all only: Bit_B0 Bit_B1 numeral.simps numeral_BitM)
-
-lemma BIT_special_simps [simp]:
-  shows "0 BIT False = 0"
-    and "0 BIT True = 1"
-    and "1 BIT False = 2"
-    and "1 BIT True = 3"
-    and "(- 1) BIT False = - 2"
-    and "(- 1) BIT True = - 1"
-  by (simp_all add: Bit_def)
-
-lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b"
-  by (auto simp: Bit_def) arith
-
-lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b"
-  by (auto simp: Bit_def) arith
-
-lemma expand_BIT:
-  "numeral (Num.Bit0 w) = numeral w BIT False"
-  "numeral (Num.Bit1 w) = numeral w BIT True"
-  "- numeral (Num.Bit0 w) = (- numeral w) BIT False"
-  "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True"
-  by (simp_all add: BitM_inc_eq add_One)
-
-lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
-  by (auto simp: Bit_def)
-
-lemma le_Bits: "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)"
-  by (auto simp: Bit_def)
-
-lemma pred_BIT_simps [simp]:
-  "x BIT False - 1 = (x - 1) BIT True"
-  "x BIT True - 1 = x BIT False"
-  by (simp_all add: Bit_B0_2t Bit_B1_2t)
-
-lemma succ_BIT_simps [simp]:
-  "x BIT False + 1 = x BIT True"
-  "x BIT True + 1 = (x + 1) BIT False"
-  by (simp_all add: Bit_B0_2t Bit_B1_2t)
-
-lemma add_BIT_simps [simp]:
-  "x BIT False + y BIT False = (x + y) BIT False"
-  "x BIT False + y BIT True = (x + y) BIT True"
-  "x BIT True + y BIT False = (x + y) BIT True"
-  "x BIT True + y BIT True = (x + y + 1) BIT False"
-  by (simp_all add: Bit_B0_2t Bit_B1_2t)
-
-lemma mult_BIT_simps [simp]:
-  "x BIT False * y = (x * y) BIT False"
-  "x * y BIT False = (x * y) BIT False"
-  "x BIT True * y = (x * y) BIT False + y"
-  by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
-
-lemma B_mod_2': "X = 2 \<Longrightarrow> (w BIT True) mod X = 1 \<and> (w BIT False) mod X = 0"
-  by (simp add: Bit_B0 Bit_B1)
-
-lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
-  by (metis bin_rl_simp)
-
-lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
-by (metis bin_ex_rl)
-
-lemma bin_abs_lem: "bin = (w BIT b) \<Longrightarrow> bin \<noteq> -1 \<longrightarrow> bin \<noteq> 0 \<longrightarrow> nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
-  apply clarsimp
-  apply (unfold Bit_def)
-  apply (cases b)
-   apply (clarsimp, arith)
-  apply (clarsimp, arith)
-  done
-
-lemma bin_induct:
-  assumes PPls: "P 0"
-    and PMin: "P (- 1)"
-    and PBit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)"
-  shows "P bin"
-  apply (rule_tac P=P and a=bin and f1="nat \<circ> abs" in wf_measure [THEN wf_induct])
-  apply (simp add: measure_def inv_image_def)
-  apply (case_tac x rule: bin_exhaust)
-  apply (frule bin_abs_lem)
-  apply (auto simp add : PPls PMin PBit)
-  done
-
-lemma Bit_div2: "(w BIT b) div 2 = w"
-  by (fact bin_rest_BIT)
-
-lemma twice_conv_BIT: "2 * x = x BIT False"
-  by (simp add: Bit_def)
-
-lemma BIT_lt0 [simp]: "x BIT b < 0 \<longleftrightarrow> x < 0"
-by(cases b)(auto simp add: Bit_def)
-
-lemma BIT_ge0 [simp]: "x BIT b \<ge> 0 \<longleftrightarrow> x \<ge> 0"
-by(cases b)(auto simp add: Bit_def)
-
-lemma bin_to_bl_aux_Bit_minus_simp [simp]:
-  "0 < n \<Longrightarrow> bin_to_bl_aux n (w BIT b) bl = bin_to_bl_aux (n - 1) w (b # bl)"
-  by (cases n) auto
-
-lemma bl_to_bin_BIT:
-  "bl_to_bin bs BIT b = bl_to_bin (bs @ [b])"
-  by (simp add: bl_to_bin_append Bit_def)
-
-lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \<longleftrightarrow> b"
-  by simp
-
-lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
-  by (simp add: bit_Suc)
-
-lemma bin_nth_minus [simp]: "0 < n \<Longrightarrow> bin_nth (w BIT b) n = bin_nth w (n - 1)"
-  by (cases n) (simp_all add: bit_Suc)
-
-lemma bin_sign_simps [simp]:
-  "bin_sign (w BIT b) = bin_sign w"
-  by (simp add: bin_sign_def Bit_def)
-
-lemma bin_nth_Bit: "bin_nth (w BIT b) n \<longleftrightarrow> n = 0 \<and> b \<or> (\<exists>m. n = Suc m \<and> bin_nth w m)"
-  by (cases n) auto
-
-lemmas sbintrunc_Suc_BIT [simp] =
-  signed_take_bit_Suc [where a="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
-
-lemmas sbintrunc_0_BIT_B0 [simp] =
-  signed_take_bit_0 [where a="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-  for w
-
-lemmas sbintrunc_0_BIT_B1 [simp] =
-  signed_take_bit_0 [where a="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
-  for w
-
-lemma sbintrunc_Suc_minus_Is:
-  \<open>0 < n \<Longrightarrow>
-  sbintrunc (n - 1) w = y \<Longrightarrow>
-  sbintrunc n (w BIT b) = y BIT b\<close>
-  by (cases n) (simp_all add: Bit_def signed_take_bit_Suc)
-
-lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
-  by (auto simp add: Bit_def concat_bit_Suc)
-
-context
-  includes bit_operations_syntax
-begin
-
-lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
-  by (simp add: not_int_def Bit_def)
-
-lemma int_and_Bits [simp]: "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
-  using and_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
-
-lemma int_or_Bits [simp]: "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
-  using or_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
-
-lemma int_xor_Bits [simp]: "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
-  using xor_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
-
-end
-
-lemma mod_BIT:
-  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" for bit
-proof -
-  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
-    by (simp add: mod_mult_mult1)
-  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
-    by (simp add: ac_simps pos_zmod_mult_2)
-  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
-    by (simp only: mod_simps)
-  finally show ?thesis
-    by (auto simp add: Bit_def)
-qed
-
-lemma minus_BIT_0: fixes x y :: int shows "x BIT b - y BIT False = (x - y) BIT b"
-by(simp add: Bit_def)
-
-lemma int_lsb_BIT [simp]: fixes x :: int shows
-  "lsb (x BIT b) \<longleftrightarrow> b"
-by(simp add: lsb_int_def)
-
-lemma int_shiftr_BIT [simp]: fixes x :: int
-  shows int_shiftr0: "drop_bit 0 x = x"
-  and int_shiftr_Suc: "drop_bit (Suc n) (x BIT b) = drop_bit n x"
-  by (simp_all add: drop_bit_Suc)
-
-lemma msb_BIT [simp]: "msb (x BIT b) = msb x"
-by(simp add: msb_int_def)
-
-end
\ No newline at end of file
diff --git a/lib/Word_Lib/Bit_Comprehension.thy b/lib/Word_Lib/Bit_Comprehension.thy
index 647828efd..8dbed8d01 100644
--- a/lib/Word_Lib/Bit_Comprehension.thy
+++ b/lib/Word_Lib/Bit_Comprehension.thy
@@ -22,46 +22,6 @@ lemma set_bits_False_eq [simp]:
 
 end
 
-instantiation int :: bit_comprehension
-begin
-
-definition
-  \<open>set_bits f = (
-      if \<exists>n. \<forall>m\<ge>n. f m = f n then
-      let n = LEAST n. \<forall>m\<ge>n. f m = f n
-      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<Suc n]))
-     else 0 :: int)\<close>
-
-instance proof
-  fix k :: int
-  from int_bit_bound [of k]
-  obtain 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>
-    by blast
-  then have ***: \<open>\<exists>n. \<forall>n'\<ge>n. bit k n' \<longleftrightarrow> bit k n\<close>
-    by meson
-  have l: \<open>(LEAST q. \<forall>m\<ge>q. bit k m \<longleftrightarrow> bit k q) = n\<close>
-    apply (rule Least_equality)
-    using * apply blast
-    apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq)
-    done
-  show \<open>set_bits (bit k) = k\<close>
-    apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l)
-    apply simp
-    apply (rule bit_eqI)
-    apply (simp add: bit_signed_take_bit_iff min_def)
-    apply (auto simp add: not_le bit_take_bit_iff dest: *)
-    done
-qed
-
-end
-
-lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)"
-  by (simp add: set_bits_int_def)
-
-lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
-  by (simp add: set_bits_int_def)
-
 instantiation word :: (len) bit_comprehension
 begin
 
@@ -77,174 +37,51 @@ lemma bit_set_bits_word_iff [bit_simps]:
   \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close>
   by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)
 
-lemma set_bits_K_False [simp]:
+lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. bit i n)"
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma set_bits_K_False:
   \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
-  by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
+  by (fact set_bits_False_eq)
 
-lemma set_bits_int_unfold':
-  \<open>set_bits f =
-    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-      in horner_sum of_bool 2 (map f [0..<n])
-     else if \<exists>n. \<forall>n'\<ge>n. f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. f n'
-      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True]))
-     else 0 :: int)\<close>
-proof (cases \<open>\<exists>n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close>)
-  case True
-  then obtain q where q: \<open>\<forall>m\<ge>q. f m \<longleftrightarrow> f q\<close>
-    by blast
-  define n where \<open>n = (LEAST n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n)\<close>
-  have \<open>\<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close>
-    unfolding n_def
-    using q by (rule LeastI [of _ q])
-  then have n: \<open>\<And>m. n \<le> m \<Longrightarrow> f m \<longleftrightarrow> f n\<close>
-    by blast
-  from n_def have n_eq: \<open>(LEAST q. \<forall>m\<ge>q. f m \<longleftrightarrow> f n) = n\<close>
-    by (smt (verit, best) Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.antisym wellorder_Least_lemma(1))
-  show ?thesis
-  proof (cases \<open>f n\<close>)
-    case False
-    with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. \<not> f n'\<close>
-      by blast
-    have **: \<open>(LEAST n. \<forall>n'\<ge>n. \<not> f n') = n\<close>
-      using False n_eq by simp
-    from * False show ?thesis
-    apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc)
-    apply (auto simp add: take_bit_horner_sum_bit_eq
-      bit_horner_sum_bit_iff take_map
-      signed_take_bit_def set_bits_int_def
-      horner_sum_bit_eq_take_bit simp del: upt.upt_Suc)
-    done
-  next
-    case True
-    with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. f n'\<close>
-      by blast
-    have ***: \<open>\<not> (\<exists>n. \<forall>n'\<ge>n. \<not> f n')\<close>
-      apply (rule ccontr)
-      using * nat_le_linear by auto
-    have **: \<open>(LEAST n. \<forall>n'\<ge>n. f n') = n\<close>
-      using True n_eq by simp
-    from * *** True show ?thesis
-    apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc)
-    apply (auto simp add: take_bit_horner_sum_bit_eq
-      bit_horner_sum_bit_iff take_map
-      signed_take_bit_def set_bits_int_def
-      horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc)
-    done
-  qed
-next
-  case False
-  then show ?thesis
-    by (auto simp add: set_bits_int_def)
-qed
-
-inductive wf_set_bits_int :: "(nat \<Rightarrow> bool) \<Rightarrow> bool"
-  for f :: "nat \<Rightarrow> bool"
-where
-  zeros: "\<forall>n' \<ge> n. \<not> f n' \<Longrightarrow> wf_set_bits_int f"
-| ones: "\<forall>n' \<ge> n. f n' \<Longrightarrow> wf_set_bits_int f"
-
-lemma wf_set_bits_int_simps: "wf_set_bits_int f \<longleftrightarrow> (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))"
-by(auto simp add: wf_set_bits_int.simps)
-
-lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\<lambda>_. b)"
-by(cases b)(auto intro: wf_set_bits_int.intros)
-
-lemma wf_set_bits_int_fun_upd [simp]:
-  "wf_set_bits_int (f(n := b)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  then obtain n'
-    where "(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')"
-    by(auto simp add: wf_set_bits_int_simps)
-  hence "(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')" by auto
-  thus ?rhs by(auto simp only: wf_set_bits_int_simps)
-next
-  assume ?rhs
-  then obtain n' where "(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')" (is "?wf f n'")
-    by(auto simp add: wf_set_bits_int_simps)
-  hence "?wf (f(n := b)) (max (Suc n) n')" by auto
-  thus ?lhs by(auto simp only: wf_set_bits_int_simps)
-qed
-
-lemma wf_set_bits_int_Suc [simp]:
-  "wf_set_bits_int (\<lambda>n. f (Suc n)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
-by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D)
+lemma word_test_bit_set_bits: "bit (BITS n. f n :: 'a :: len word) n \<longleftrightarrow> n < LENGTH('a) \<and> f n"
+  by (fact bit_set_bits_word_iff)
 
 context
-  fixes f
-  assumes wff: "wf_set_bits_int f"
+  includes bit_operations_syntax
+  fixes f :: \<open>nat \<Rightarrow> bool\<close>
 begin
 
-lemma int_set_bits_unfold_BIT:
-  "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \<circ> Suc)"
-using wff proof cases
-  case (zeros n)
-  show ?thesis
-  proof(cases "\<forall>n. \<not> f n")
-    case True
-    hence "f = (\<lambda>_. False)" by auto
-    thus ?thesis using True by(simp add: o_def)
-  next
-    case False
-    then obtain n' where "f n'" by blast
-    with zeros have "(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')"
-      by(auto intro: Least_Suc)
-    also have "(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))" by(auto dest: Suc_le_D)
-    also from zeros have "\<forall>n'\<ge>n. \<not> f (Suc n')" by auto
-    ultimately show ?thesis using zeros
-      apply (simp (no_asm_simp) add: set_bits_int_unfold' exI
-        del: upt.upt_Suc flip: map_map split del: if_split)
-      apply (simp only: map_Suc_upt upt_conv_Cons)
-      apply simp
-      done
-  qed
-next
-  case (ones n)
-  show ?thesis
-  proof(cases "\<forall>n. f n")
-    case True
-    hence "f = (\<lambda>_. True)" by auto
-    thus ?thesis using True by(simp add: o_def)
-  next
-    case False
-    then obtain n' where "\<not> f n'" by blast
-    with ones have "(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')"
-      by(auto intro: Least_Suc)
-    also have "(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))" by(auto dest: Suc_le_D)
-    also from ones have "\<forall>n'\<ge>n. f (Suc n')" by auto
-    moreover from ones have "(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False"
-      by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm)
-    moreover hence "(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False"
-      by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D)
-    ultimately show ?thesis using ones
-      apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split)
-      apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc
-        not_le simp del: map_map)
-      done
-  qed
-qed
+definition set_bits_aux :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a::len word\<close>
+  where \<open>set_bits_aux n w = push_bit n w OR take_bit n (set_bits f)\<close>
 
-lemma bin_last_set_bits [simp]:
-  "odd (set_bits f :: int) = f 0"
-  by (subst int_set_bits_unfold_BIT) simp_all
+lemma bit_set_bit_aux [bit_simps]:
+  \<open>bit (set_bits_aux n w) m \<longleftrightarrow> m < LENGTH('a) \<and>
+    (if m < n then f m else bit w (m - n))\<close> for w :: \<open>'a::len word\<close>
+  by (auto simp add: bit_simps set_bits_aux_def)
 
-lemma bin_rest_set_bits [simp]:
-  "set_bits f div (2 :: int) = set_bits (f \<circ> Suc)"
-  by (subst int_set_bits_unfold_BIT) simp_all
+corollary set_bits_conv_set_bits_aux:
+  \<open>set_bits f = (set_bits_aux LENGTH('a) 0 :: 'a :: len word)\<close>
+  by (rule bit_word_eqI) (simp add: bit_simps)
 
-lemma bin_nth_set_bits [simp]:
-  "bit (set_bits f :: int) m \<longleftrightarrow> f m"
-using wff proof (induction m arbitrary: f)
-  case 0
-  then show ?case
-    by (simp add: Bit_Comprehension.bin_last_set_bits)
-next
-  case Suc
-  from Suc.IH [of "f \<circ> Suc"] Suc.prems show ?case
-    by (simp add: Bit_Comprehension.bin_rest_set_bits comp_def bit_Suc)
-qed
+lemma set_bits_aux_0 [simp]:
+  \<open>set_bits_aux 0 w = w\<close>
+  by (simp add: set_bits_aux_def)
+
+lemma set_bits_aux_Suc [simp]:
+  \<open>set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\<close>
+  by (rule bit_word_eqI) (auto simp add: bit_simps le_less_Suc_eq mult.commute [of _ 2])
+
+lemma set_bits_aux_simps [code]:
+  \<open>set_bits_aux 0 w = w\<close>
+  \<open>set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\<close>
+  by simp_all
+
+lemma set_bits_aux_rec:
+  \<open>set_bits_aux n w =
+  (if n = 0 then w
+   else let n' = n - 1 in set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))\<close>
+  by (cases n) simp_all
 
 end
 
diff --git a/lib/Word_Lib/Bit_Comprehension_Int.thy b/lib/Word_Lib/Bit_Comprehension_Int.thy
new file mode 100644
index 000000000..b09d16594
--- /dev/null
+++ b/lib/Word_Lib/Bit_Comprehension_Int.thy
@@ -0,0 +1,225 @@
+(*
+ * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+section \<open>Comprehension syntax for \<open>int\<close>\<close>
+
+theory Bit_Comprehension_Int
+  imports
+    Bit_Comprehension
+begin
+
+instantiation int :: bit_comprehension
+begin
+
+definition
+  \<open>set_bits f = (
+      if \<exists>n. \<forall>m\<ge>n. f m = f n then
+      let n = LEAST n. \<forall>m\<ge>n. f m = f n
+      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<Suc n]))
+     else 0 :: int)\<close>
+
+instance proof
+  fix k :: int
+  from int_bit_bound [of k]
+  obtain 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>
+    by blast
+  then have ***: \<open>\<exists>n. \<forall>n'\<ge>n. bit k n' \<longleftrightarrow> bit k n\<close>
+    by meson
+  have l: \<open>(LEAST q. \<forall>m\<ge>q. bit k m \<longleftrightarrow> bit k q) = n\<close>
+    apply (rule Least_equality)
+    using * apply blast
+    apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq)
+    done
+  show \<open>set_bits (bit k) = k\<close>
+    apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l)
+    apply simp
+    apply (rule bit_eqI)
+    apply (simp add: bit_signed_take_bit_iff min_def)
+    apply (auto simp add: not_le bit_take_bit_iff dest: *)
+    done
+qed
+
+end
+
+lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)"
+  by (simp add: set_bits_int_def)
+
+lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
+  by (simp add: set_bits_int_def)
+
+lemma set_bits_code [code]:
+  "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\<lambda>_. set_bits :: _ \<Rightarrow> int)"
+  by simp
+
+lemma set_bits_int_unfold':
+  \<open>set_bits f =
+    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+      in horner_sum of_bool 2 (map f [0..<n])
+     else if \<exists>n. \<forall>n'\<ge>n. f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. f n'
+      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True]))
+     else 0 :: int)\<close>
+proof (cases \<open>\<exists>n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close>)
+  case True
+  then obtain q where q: \<open>\<forall>m\<ge>q. f m \<longleftrightarrow> f q\<close>
+    by blast
+  define n where \<open>n = (LEAST n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n)\<close>
+  have \<open>\<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close>
+    unfolding n_def
+    using q by (rule LeastI [of _ q])
+  then have n: \<open>\<And>m. n \<le> m \<Longrightarrow> f m \<longleftrightarrow> f n\<close>
+    by blast
+  from n_def have n_eq: \<open>(LEAST q. \<forall>m\<ge>q. f m \<longleftrightarrow> f n) = n\<close>
+    by (smt (verit, best) Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.antisym wellorder_Least_lemma(1))
+  show ?thesis
+  proof (cases \<open>f n\<close>)
+    case False
+    with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. \<not> f n'\<close>
+      by blast
+    have **: \<open>(LEAST n. \<forall>n'\<ge>n. \<not> f n') = n\<close>
+      using False n_eq by simp
+    from * False show ?thesis
+    apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc)
+    apply (auto simp add: take_bit_horner_sum_bit_eq
+      bit_horner_sum_bit_iff take_map
+      signed_take_bit_def set_bits_int_def
+      horner_sum_bit_eq_take_bit simp del: upt.upt_Suc)
+    done
+  next
+    case True
+    with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. f n'\<close>
+      by blast
+    have ***: \<open>\<not> (\<exists>n. \<forall>n'\<ge>n. \<not> f n')\<close>
+      apply (rule ccontr)
+      using * nat_le_linear by auto
+    have **: \<open>(LEAST n. \<forall>n'\<ge>n. f n') = n\<close>
+      using True n_eq by simp
+    from * *** True show ?thesis
+    apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc)
+    apply (auto simp add: take_bit_horner_sum_bit_eq
+      bit_horner_sum_bit_iff take_map
+      signed_take_bit_def set_bits_int_def
+      horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc)
+    done
+  qed
+next
+  case False
+  then show ?thesis
+    by (auto simp add: set_bits_int_def)
+qed
+
+inductive wf_set_bits_int :: "(nat \<Rightarrow> bool) \<Rightarrow> bool"
+  for f :: "nat \<Rightarrow> bool"
+where
+  zeros: "\<forall>n' \<ge> n. \<not> f n' \<Longrightarrow> wf_set_bits_int f"
+| ones: "\<forall>n' \<ge> n. f n' \<Longrightarrow> wf_set_bits_int f"
+
+lemma wf_set_bits_int_simps: "wf_set_bits_int f \<longleftrightarrow> (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))"
+by(auto simp add: wf_set_bits_int.simps)
+
+lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\<lambda>_. b)"
+by(cases b)(auto intro: wf_set_bits_int.intros)
+
+lemma wf_set_bits_int_fun_upd [simp]:
+  "wf_set_bits_int (f(n := b)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  then obtain n'
+    where "(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')"
+    by(auto simp add: wf_set_bits_int_simps)
+  hence "(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')" by auto
+  thus ?rhs by(auto simp only: wf_set_bits_int_simps)
+next
+  assume ?rhs
+  then obtain n' where "(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')" (is "?wf f n'")
+    by(auto simp add: wf_set_bits_int_simps)
+  hence "?wf (f(n := b)) (max (Suc n) n')" by auto
+  thus ?lhs by(auto simp only: wf_set_bits_int_simps)
+qed
+
+lemma wf_set_bits_int_Suc [simp]:
+  "wf_set_bits_int (\<lambda>n. f (Suc n)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
+by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D)
+
+context
+  fixes f
+  assumes wff: "wf_set_bits_int f"
+begin
+
+lemma int_set_bits_unfold_BIT:
+  "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \<circ> Suc)"
+using wff proof cases
+  case (zeros n)
+  show ?thesis
+  proof(cases "\<forall>n. \<not> f n")
+    case True
+    hence "f = (\<lambda>_. False)" by auto
+    thus ?thesis using True by(simp add: o_def)
+  next
+    case False
+    then obtain n' where "f n'" by blast
+    with zeros have "(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')"
+      by(auto intro: Least_Suc)
+    also have "(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))" by(auto dest: Suc_le_D)
+    also from zeros have "\<forall>n'\<ge>n. \<not> f (Suc n')" by auto
+    ultimately show ?thesis using zeros
+      apply (simp (no_asm_simp) add: set_bits_int_unfold' exI
+        del: upt.upt_Suc flip: map_map split del: if_split)
+      apply (simp only: map_Suc_upt upt_conv_Cons)
+      apply simp
+      done
+  qed
+next
+  case (ones n)
+  show ?thesis
+  proof(cases "\<forall>n. f n")
+    case True
+    hence "f = (\<lambda>_. True)" by auto
+    thus ?thesis using True by(simp add: o_def)
+  next
+    case False
+    then obtain n' where "\<not> f n'" by blast
+    with ones have "(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')"
+      by(auto intro: Least_Suc)
+    also have "(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))" by(auto dest: Suc_le_D)
+    also from ones have "\<forall>n'\<ge>n. f (Suc n')" by auto
+    moreover from ones have "(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False"
+      by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm)
+    moreover hence "(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False"
+      by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D)
+    ultimately show ?thesis using ones
+      apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split)
+      apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc
+        not_le simp del: map_map)
+      done
+  qed
+qed
+
+lemma bin_last_set_bits [simp]:
+  "odd (set_bits f :: int) = f 0"
+  by (subst int_set_bits_unfold_BIT) simp_all
+
+lemma bin_rest_set_bits [simp]:
+  "set_bits f div (2 :: int) = set_bits (f \<circ> Suc)"
+  by (subst int_set_bits_unfold_BIT) simp_all
+
+lemma bin_nth_set_bits [simp]:
+  "bit (set_bits f :: int) m \<longleftrightarrow> f m"
+using wff proof (induction m arbitrary: f)
+  case 0
+  then show ?case
+    by (simp add: Bit_Comprehension_Int.bin_last_set_bits bit_0)
+next
+  case Suc
+  from Suc.IH [of "f \<circ> Suc"] Suc.prems show ?case
+    by (simp add: Bit_Comprehension_Int.bin_rest_set_bits comp_def bit_Suc)
+qed
+
+end
+
+end
diff --git a/lib/Word_Lib/Bits_Int.thy b/lib/Word_Lib/Bits_Int.thy
index c81c48e02..2587cfbf7 100644
--- a/lib/Word_Lib/Bits_Int.thy
+++ b/lib/Word_Lib/Bits_Int.thy
@@ -812,10 +812,7 @@ lemma bin_sc_sc_diff: "m \<noteq> n \<Longrightarrow> bin_sc m c (bin_sc n b w)
   done
 
 lemma bin_nth_sc_gen: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (bin_sc n b w) m = (if m = n then b else (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w m)"
-  apply (induct n arbitrary: w m)
-   apply (case_tac m; simp add: bit_Suc)
-  apply (case_tac m; simp add: bit_Suc)
-  done
+  by (simp add: bit_simps)
 
 lemma bin_sc_eq:
   \<open>bin_sc n False = unset_bit n\<close>
@@ -1339,33 +1336,22 @@ lemma int_shiftr_numeral_Suc0 [simp]:
 
 lemma bin_nth_minus_p2:
   assumes sign: "bin_sign x = 0"
-  and y: "y = push_bit n 1"
-  and m: "m < n"
-  and x: "x < y"
+    and y: "y = push_bit n 1"
+    and m: "m < n"
+    and x: "x < y"
   shows "bit (x - y) m = bit x m"
 proof -
-  from sign y x have \<open>x \<ge> 0\<close> and \<open>y = 2 ^ n\<close> and \<open>x < 2 ^ n\<close>
-    by (simp_all add: bin_sign_def push_bit_eq_mult split: if_splits)
-  from \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>m < n\<close> have \<open>bit x m \<longleftrightarrow> bit (x - 2 ^ n) m\<close>
-  proof (induction m arbitrary: x n)
-    case 0
-    then show ?case
-      by simp
-  next
-    case (Suc m)
-    moreover define q where \<open>q = n - 1\<close>
-    ultimately have n: \<open>n = Suc q\<close>
-      by simp
-    have \<open>(x - 2 ^ Suc q) div 2 = x div 2 - 2 ^ q\<close>
-      by simp
-    moreover from Suc.IH [of \<open>x div 2\<close> q] Suc.prems
-    have \<open>bit (x div 2) m \<longleftrightarrow> bit (x div 2 - 2 ^ q) m\<close>
-      by (simp add: n)
-    ultimately show ?case
-      by (simp add: bit_Suc n)
-  qed
-  with \<open>y = 2 ^ n\<close> show ?thesis
+  from \<open>bin_sign x = 0\<close> have \<open>x \<ge> 0\<close>
+    by (simp add: sign_Pls_ge_0)
+  moreover from x y have \<open>x < 2 ^ n\<close>
     by simp
+  ultimately have \<open>q < n\<close> if \<open>bit x q\<close> for q
+    using that by (metis bit_take_bit_iff take_bit_int_eq_self)
+  then have \<open>bit (x + NOT (mask n)) m = bit x m\<close>
+    using \<open>m < n\<close> by (simp add: disjunctive_add bit_simps)
+  also have \<open>x + NOT (mask n) = x - y\<close>
+    using y by (simp flip: minus_exp_eq_not_mask)
+  finally show ?thesis .
 qed
 
 lemma bin_clr_conv_NAND:
@@ -1430,7 +1416,7 @@ lemma clearBit_no:
 
 lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
   for b n :: int
-  by auto (metis pos_mod_conj)+
+  using pos_mod_sign [of n b] pos_mod_bound [of n b] by (safe, auto)
 
 lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
     a = take_bit (LENGTH('a) - n) a \<and> b = take_bit (LENGTH('a)) b"
diff --git a/lib/Word_Lib/Generic_set_bit.thy b/lib/Word_Lib/Generic_set_bit.thy
index f3641eb8c..743b32d22 100644
--- a/lib/Word_Lib/Generic_set_bit.thy
+++ b/lib/Word_Lib/Generic_set_bit.thy
@@ -38,6 +38,18 @@ instance
 
 end
 
+context
+  includes bit_operations_syntax
+begin
+
+lemma fixes i :: int
+  shows int_set_bit_True_conv_OR [code]: "Generic_set_bit.set_bit i n True = i OR push_bit n 1"
+  and int_set_bit_False_conv_NAND [code]: "Generic_set_bit.set_bit i n False = i AND NOT (push_bit n 1)"
+  and int_set_bit_conv_ops: "Generic_set_bit.set_bit i n b = (if b then i OR (push_bit n 1) else i AND NOT (push_bit n 1))"
+  by (simp_all add: bit_eq_iff) (auto simp add: bit_simps)
+
+end
+
 instantiation word :: (len) set_bit
 begin
 
@@ -121,4 +133,20 @@ lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n"
 lemma one_bit_pow: "set_bit 0 n True = (2 :: 'a :: len word) ^ n"
   by (simp add: one_bit_shiftl shiftl_def)
 
+instantiation integer :: set_bit
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition set_bit_integer :: \<open>integer \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> integer\<close> is set_bit .
+
+instance
+  by (standard; transfer) (simp add: bit_simps)
+
+end
+
+end
+
 end
diff --git a/lib/Word_Lib/Guide.thy b/lib/Word_Lib/Guide.thy
index ab5220883..f87ee74e7 100644
--- a/lib/Word_Lib/Guide.thy
+++ b/lib/Word_Lib/Guide.thy
@@ -6,7 +6,7 @@
 
 (*<*)
 theory Guide
-  imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64 Ancient_Numeral
+  imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64
 begin
 
 context semiring_bit_operations
@@ -364,8 +364,13 @@ text \<open>
   \<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension\<close>]
 
     Comprehension syntax for bit values over predicates
-    \<^typ>\<open>nat \<Rightarrow> bool\<close>.  For \<^typ>\<open>'a::len word\<close>, straightforward
-    alternatives exist; difficult to handle for \<^typ>\<open>int\<close>.
+    \<^typ>\<open>nat \<Rightarrow> bool\<close>, for \<^typ>\<open>'a::len word\<close>; straightforward
+    alternatives exist.
+
+  \<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>]
+
+    Comprehension syntax for bit values over predicates
+    \<^typ>\<open>nat \<Rightarrow> bool\<close>, for \<^typ>\<open>int\<close>; inherently non-computational.
 
   \<^descr>[\<^theory>\<open>Word_Lib.Reversed_Bit_Lists\<close>]
 
@@ -388,9 +393,16 @@ text \<open>
 section \<open>Changelog\<close>
 
 text \<open>
+  \<^descr>[Changes since AFP 2022] ~
+
+    \<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> has been removed from session.
+
+    \<^item> Bit comprehension syntax for \<^typ>\<open>int\<close> moved to separate theory
+      \<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>.
+
   \<^descr>[Changes since AFP 2021] ~
 
-    \<^item> Theory \<^theory>\<open>Word_Lib.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>
+    \<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>
       any longer.
 
     \<^item> Infix syntax for \<^term>\<open>(AND)\<close>, \<^term>\<open>(OR)\<close>, \<^term>\<open>(XOR)\<close> organized in
diff --git a/lib/Word_Lib/Least_significant_bit.thy b/lib/Word_Lib/Least_significant_bit.thy
index 587b0318c..b1cfda83c 100644
--- a/lib/Word_Lib/Least_significant_bit.thy
+++ b/lib/Word_Lib/Least_significant_bit.thy
@@ -25,7 +25,7 @@ definition lsb_int :: \<open>int \<Rightarrow> bool\<close>
   where \<open>lsb i = bit i 0\<close> for i :: int
 
 instance
-  by standard (simp add: fun_eq_iff lsb_int_def)
+  by standard (simp add: fun_eq_iff lsb_int_def bit_0)
 
 end
 
@@ -42,7 +42,7 @@ lemma int_lsb_numeral [simp]:
   "lsb (numeral (num.Bit1 w) :: int) = True"
   "lsb (- numeral (num.Bit0 w) :: int) = False"
   "lsb (- numeral (num.Bit1 w) :: int) = True"
-  by (simp_all add: lsb_int_def)
+  by (simp_all add: lsb_int_def bit_0)
 
 instantiation word :: (len) lsb
 begin
@@ -64,7 +64,7 @@ lemma lsb_word_eq:
 
 lemma word_lsb_alt: "lsb w = bit w 0"
   for w :: "'a::len word"
-  by (simp add: lsb_word_eq)
+  by (simp add: lsb_word_eq bit_0)
 
 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
   unfolding word_lsb_def by simp
@@ -91,4 +91,20 @@ lemma word_lsb_nat:"lsb w = (unat w mod 2 = 1)"
   apply (simp add: even_nat_iff)
   done
 
+instantiation integer :: lsb
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition lsb_integer :: \<open>integer \<Rightarrow> bool\<close> is lsb .
+
+instance
+  by (standard; transfer) (fact lsb_odd)
+
+end
+
+end
+
 end
diff --git a/lib/Word_Lib/Many_More.thy b/lib/Word_Lib/Many_More.thy
index c255278ca..2dbea777a 100644
--- a/lib/Word_Lib/Many_More.thy
+++ b/lib/Word_Lib/Many_More.thy
@@ -683,4 +683,7 @@ lemma plus_minus_one_rewrite:
 lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)"
   by (metis One_nat_def len_gt_0 lessI numeral_2_eq_2 one_less_power)
 
+lemma bin_rest_code: "i div 2 = drop_bit 1 i" for i :: int
+  by (simp add: drop_bit_eq_div)
+
 end
diff --git a/lib/Word_Lib/More_Word.thy b/lib/Word_Lib/More_Word.thy
index 4623d21af..c2dc1e7a9 100644
--- a/lib/Word_Lib/More_Word.thy
+++ b/lib/Word_Lib/More_Word.thy
@@ -13,19 +13,6 @@ theory More_Word
     More_Divides
 begin
 
-context unique_euclidean_semiring_with_bit_operations \<comment>\<open>TODO: move\<close>
-begin
-
-lemma possible_bit [simp]:
-  \<open>possible_bit TYPE('a) n\<close>
-  by (simp add: possible_bit_def)
-
-lemma drop_bit_mask_eq:
-  \<open>drop_bit m (mask n) = mask (n - m)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps possible_bit_def)
-
-end
-
 context
   includes bit_operations_syntax
 begin
@@ -59,10 +46,6 @@ proof -
              prefer 10
              apply (subst signed_take_bit_int_eq_self)
                apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
-       apply (smt (z3) take_bit_nonnegative)
-      apply (smt (z3) take_bit_int_less_exp)
-     apply (smt (z3) take_bit_nonnegative)
-    apply (smt (z3) take_bit_int_less_exp)
     done
   then show ?thesis
     apply (simp only: One_nat_def word_size drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
@@ -2178,10 +2161,10 @@ lemma odd_word_imp_even_next:"odd (unat (x::('a::len) word)) \<Longrightarrow> x
   done
 
 lemma overflow_imp_lsb:"(x::('a::len) word) + 1 = 0 \<Longrightarrow> bit x 0"
-  using even_plus_one_iff [of x] by simp
+  using even_plus_one_iff [of x] by (simp add: bit_0)
 
 lemma odd_iff_lsb:"odd (unat (x::('a::len) word)) = bit x 0"
-  by transfer (simp add: even_nat_iff)
+  by transfer (simp add: even_nat_iff bit_0)
 
 lemma of_nat_neq_iff_word:
       "x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a) \<Longrightarrow>
@@ -2196,7 +2179,7 @@ lemma of_nat_neq_iff_word:
   done
 
 lemma lsb_this_or_next: "\<not> (bit ((x::('a::len) word) + 1) 0) \<Longrightarrow> bit x 0"
-  by simp
+  by (simp add: bit_0)
 
 lemma mask_or_not_mask:
   "x AND mask n OR x AND NOT (mask n) = x"
@@ -2275,8 +2258,8 @@ lemma word_ops_nth:
 lemma word_power_nonzero:
   "\<lbrakk> (x :: 'a::len word) < 2 ^ (LENGTH('a) - n); n < LENGTH('a); x \<noteq> 0 \<rbrakk>
   \<Longrightarrow> x * 2 ^ n \<noteq> 0"
-  by (metis gr_implies_not0 mult_eq_0_iff nat_mult_power_less_eq numeral_2_eq_2
-    p2_gt_0 unat_eq_zero unat_less_power unat_mult_lem unat_power_lower word_gt_a_gt_0 zero_less_Suc)
+  by (metis Word.word_div_mult bits_div_0 len_gt_0 len_of_finite_2_def nat_mult_power_less_eq
+    p2_gt_0 unat_mono unat_power_lower word_gt_a_gt_0)
 
 lemma less_1_helper:
   "n \<le> m \<Longrightarrow> (n - 1 :: int) < m"
diff --git a/lib/Word_Lib/More_Word_Operations.thy b/lib/Word_Lib/More_Word_Operations.thy
index cfb43dbc7..a607aadd8 100644
--- a/lib/Word_Lib/More_Word_Operations.thy
+++ b/lib/Word_Lib/More_Word_Operations.thy
@@ -722,7 +722,7 @@ definition
 
 lemma to_bool_and_1:
   "to_bool (x AND 1) \<longleftrightarrow> bit x 0"
-  by (simp add: to_bool_def and_one_eq mod_2_eq_odd)
+  by (simp add: to_bool_def word_and_1)
 
 lemma to_bool_from_bool [simp]:
   "to_bool (from_bool r) = r"
@@ -785,7 +785,7 @@ lemma from_bool_eqI:
 
 lemma from_bool_odd_eq_and:
   "from_bool (odd w) = w AND 1"
-  unfolding from_bool_def by (simp add: word_and_1)
+  unfolding from_bool_def by (simp add: word_and_1 bit_0)
 
 lemma neg_mask_in_mask_range:
   "is_aligned ptr bits \<Longrightarrow> (ptr' AND NOT(mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)"
diff --git a/lib/Word_Lib/Most_significant_bit.thy b/lib/Word_Lib/Most_significant_bit.thy
index e3f6f9d12..89f8ef967 100644
--- a/lib/Word_Lib/Most_significant_bit.thy
+++ b/lib/Word_Lib/Most_significant_bit.thy
@@ -191,4 +191,19 @@ lemma msb_big:
   apply (simp add: take_bit_eq_self_iff_drop_bit_eq_0 drop_bit_eq_zero_iff_not_bit_last)
   done
 
+instantiation integer :: msb
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition msb_integer :: \<open>integer \<Rightarrow> bool\<close> is msb .
+
+instance ..
+
+end
+
+end
+
 end
diff --git a/lib/Word_Lib/ROOT b/lib/Word_Lib/ROOT
index 0c3c2d429..5a2b12301 100644
--- a/lib/Word_Lib/ROOT
+++ b/lib/Word_Lib/ROOT
@@ -23,7 +23,6 @@ session Word_Lib (lib) = HOL +
     More_Misc
     Strict_part_mono
     Many_More
-    Ancient_Numeral
     Examples
   theories
     Guide
diff --git a/lib/Word_Lib/Reversed_Bit_Lists.thy b/lib/Word_Lib/Reversed_Bit_Lists.thy
index 2d4484cb2..ecc4725f4 100644
--- a/lib/Word_Lib/Reversed_Bit_Lists.thy
+++ b/lib/Word_Lib/Reversed_Bit_Lists.thy
@@ -498,15 +498,7 @@ lemma bin_nth_of_bl: "bit (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
   by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
 
 lemma bin_nth_bl: "n < m \<Longrightarrow> bit w n = nth (rev (bin_to_bl m w)) n"
-  apply (induct n arbitrary: m w)
-   apply clarsimp
-   apply (case_tac m, clarsimp)
-   apply (clarsimp simp: bin_to_bl_def)
-   apply (simp add: bin_to_bl_aux_alt)
-  apply (case_tac m, clarsimp)
-  apply (clarsimp simp: bin_to_bl_def)
-  apply (simp add: bin_to_bl_aux_alt bit_Suc)
-  done
+  by (metis bin_bl_bin bin_nth_of_bl nth_bintr size_bin_to_bl)
 
 lemma nth_bin_to_bl_aux:
   "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
@@ -1798,11 +1790,8 @@ lemma bl_word_roti_dt':
   apply safe
    apply (simp add: zmod_zminus1_eq_if)
    apply safe
-    apply (simp add: nat_mult_distrib)
-   apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
-                                      [THEN conjunct2, THEN order_less_imp_le]]
-                    nat_mod_distrib)
-  apply (simp add: nat_mod_distrib)
+    apply (auto simp add: nat_mult_distrib nat_mod_distrib)
+  using nat_0_le nat_minus_as_int zmod_int apply presburger
   done
 
 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
@@ -1891,12 +1880,12 @@ lemma bin_to_bl_or:
 lemma word_and_1_bl:
   fixes x::"'a::len word"
   shows "(x AND 1) = of_bl [bit x 0]"
-  by (simp add: mod_2_eq_odd and_one_eq)
+  by (simp add: word_and_1)
 
 lemma word_1_and_bl:
   fixes x::"'a::len word"
   shows "(1 AND x) = of_bl [bit x 0]"
-  by (simp add: mod_2_eq_odd one_and_eq)
+  using word_and_1_bl [of x] by (simp add: ac_simps)
 
 lemma of_bl_drop:
   "of_bl (drop n xs) = (of_bl xs AND mask (length xs - n))"
@@ -1955,7 +1944,7 @@ lemma word_lsb_last:
   \<open>lsb w \<longleftrightarrow> last (to_bl w)\<close>
   for w :: \<open>'a::len word\<close>
   using nth_to_bl [of \<open>LENGTH('a) - Suc 0\<close> w]
-  by (simp add: lsb_odd last_conv_nth)
+  by (simp add: last_conv_nth bit_0 lsb_odd)
 
 lemma is_aligned_to_bl:
   "is_aligned (w :: 'a :: len word) n = (True \<notin> set (drop (size w - n) (to_bl w)))"
diff --git a/lib/Word_Lib/Signed_Division_Word.thy b/lib/Word_Lib/Signed_Division_Word.thy
index 7aeaf4aa8..14a7ab54c 100644
--- a/lib/Word_Lib/Signed_Division_Word.thy
+++ b/lib/Word_Lib/Signed_Division_Word.thy
@@ -21,10 +21,6 @@ lift_definition signed_modulo_word :: \<open>'a::len word \<Rightarrow> 'a word
   is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - Suc 0) k smod signed_take_bit (LENGTH('a) - Suc 0) l\<close>
   by (simp flip: signed_take_bit_decr_length_iff)
 
-instance ..
-
-end
-
 lemma sdiv_word_def [code]:
   \<open>v sdiv w = word_of_int (sint v sdiv sint w)\<close>
   for v w :: \<open>'a::len word\<close>
@@ -35,10 +31,22 @@ lemma smod_word_def [code]:
   for v w :: \<open>'a::len word\<close>
   by transfer simp
 
+instance proof
+  fix v w :: \<open>'a word\<close>
+  have \<open>sint v sdiv sint w * sint w + sint v smod sint w = sint v\<close>
+    by (fact sdiv_mult_smod_eq)
+  then have \<open>word_of_int (sint v sdiv sint w * sint w + sint v smod sint w) = (word_of_int (sint v) :: 'a word)\<close>
+    by simp
+  then show \<open>v sdiv w * w + v smod w = v\<close>
+    by (simp add: sdiv_word_def smod_word_def)
+qed
+
+end
+
 lemma sdiv_smod_id:
   \<open>(a sdiv b) * b + (a smod b) = a\<close>
   for a b :: \<open>'a::len word\<close>
-  by (cases \<open>sint a < 0\<close>; cases \<open>sint b < 0\<close>) (simp_all add: signed_modulo_int_def sdiv_word_def smod_word_def)
+  by (fact sdiv_mult_smod_eq)
 
 lemma signed_div_arith:
     "sint ((a::('a::len) word) sdiv b) = signed_take_bit (LENGTH('a) - 1) (sint a sdiv sint b)"
@@ -59,7 +67,7 @@ lemma word_sdiv_div0 [simp]:
 
 lemma smod_word_zero [simp]:
   \<open>w smod 0 = w\<close> for w :: \<open>'a::len word\<close>
-  by (simp add: smod_word_def signed_modulo_int_def)
+  by transfer (simp add: take_bit_signed_take_bit)
 
 lemma word_sdiv_div1 [simp]:
     "(a :: ('a::len) word) sdiv 1 = a"
@@ -124,11 +132,7 @@ lemma minus_one_smod_word_eq [simp]:
 
 lemma smod_word_alt_def:
   "(a :: ('a::len) word) smod b = a - (a sdiv b) * b"
-  apply (cases \<open>a \<noteq> - (2 ^ (LENGTH('a) - 1)) \<or> b \<noteq> - 1\<close>)
-   apply (clarsimp simp: smod_word_def sdiv_word_def signed_modulo_int_def
-     simp flip: wi_hom_sub wi_hom_mult)
-  apply (clarsimp simp: smod_word_def signed_modulo_int_def)
-  done
+  by (simp add: minus_sdiv_mult_eq_smod)
 
 lemmas sdiv_word_numeral_numeral [simp] =
   sdiv_word_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
@@ -244,4 +248,4 @@ lemmas word_smod_numerals_lhs = smod_word_def[where v="numeral x" for x]
 lemmas word_smod_numerals = word_smod_numerals_lhs[where w="numeral y" for y]
     word_smod_numerals_lhs[where w=0] word_smod_numerals_lhs[where w=1]
 
-end
\ No newline at end of file
+end
diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy
index c2dba748b..8c4e8ffe0 100644
--- a/lib/Word_Lib/Word_Lemmas.thy
+++ b/lib/Word_Lib/Word_Lemmas.thy
@@ -622,16 +622,13 @@ lemma shiftr1_0_or_1:"(x::('a::len) word) >> 1 = 0 \<Longrightarrow> x = 0 \<or>
   done
 
 lemma shiftr1_irrelevant_lsb: "bit (x::('a::len) word) 0 \<or> x >> 1 = (x + 1) >> 1"
-  apply (cases \<open>LENGTH('a)\<close>; transfer)
-   apply (simp_all add: take_bit_drop_bit)
-  apply (simp add: drop_bit_take_bit drop_bit_Suc)
-  done
+  by (auto simp add: bit_0 shiftr_def drop_bit_Suc ac_simps elim: evenE)
 
 lemma shiftr1_0_imp_only_lsb:"((x::('a::len) word) + 1) >> 1 = 0 \<Longrightarrow> x = 0 \<or> x + 1 = 0"
   by (metis One_nat_def shiftr1_0_or_1 word_less_1 word_overflow)
 
 lemma shiftr1_irrelevant_lsb': "\<not> (bit (x::('a::len) word) 0) \<Longrightarrow> x >> 1 = (x + 1) >> 1"
-  by (metis shiftr1_irrelevant_lsb)
+  using shiftr1_irrelevant_lsb [of x] by simp
 
 (* Perhaps this one should be a simp lemma, but it seems a little dangerous. *)
 lemma cast_chunk_assemble_id:
diff --git a/lib/Word_Lib/Word_Lib_Sumo.thy b/lib/Word_Lib/Word_Lib_Sumo.thy
index a7457e8ae..942ffd14b 100644
--- a/lib/Word_Lib/Word_Lib_Sumo.thy
+++ b/lib/Word_Lib/Word_Lib_Sumo.thy
@@ -11,6 +11,7 @@ imports
   "HOL-Library.Word"
   Aligned
   Bit_Comprehension
+  Bit_Comprehension_Int
   Bit_Shifts_Infix_Syntax
   Bits_Int
   Bitwise_Signed