# HG changeset patch
# User haftmann
# Date 1593895524 0
# Node ID 4a013c92a0914c2d9d6ad465219f3873dc0bc47c
# Parent  c7ac6d4f3914c75a2ac82337c7e2dbc3808d67e9
factored out auxiliary theory

diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/SPARK/Examples/RIPEMD-160/F.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -26,7 +26,7 @@
 proof -
   from H8 have "nat j <= 15" by simp
   with assms show ?thesis
-    by (simp add: f_def bwsimps int_word_uint int_mod_eq')
+    by (simp add: f_def bwsimps int_word_uint)
 qed
 
 spark_vc function_f_7
@@ -34,7 +34,7 @@
   from H7 have "16 <= nat j" by simp
   moreover from H8 have "nat j <= 31" by simp
   ultimately show ?thesis using assms
-    by (simp add: f_def bwsimps int_word_uint int_mod_eq')
+    by (simp add: f_def bwsimps int_word_uint)
 qed
 
 spark_vc function_f_8
@@ -42,7 +42,7 @@
   from H7 have "32 <= nat j" by simp
   moreover from H8 have "nat j <= 47" by simp
   ultimately show ?thesis using assms
-    by (simp add: f_def bwsimps int_word_uint int_mod_eq')
+    by (simp add: f_def bwsimps int_word_uint)
 qed
 
 spark_vc function_f_9
@@ -50,7 +50,7 @@
   from H7 have "48 <= nat j" by simp
   moreover from H8 have   "nat j <= 63" by simp
   ultimately show ?thesis using assms
-    by (simp add: f_def bwsimps int_word_uint int_mod_eq')
+    by (simp add: f_def bwsimps int_word_uint)
 qed
 
 spark_vc function_f_10
@@ -58,7 +58,7 @@
   from H2 have "nat j <= 79" by simp
   moreover from H12 have "64 <= nat j" by simp
   ultimately show ?thesis using assms
-    by (simp add: f_def bwsimps int_word_uint int_mod_eq')
+    by (simp add: f_def bwsimps int_word_uint)
 qed
 
 spark_end
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -56,7 +56,7 @@
   shows"uint(word_of_int x::word32) = x"
   unfolding int_word_uint
   using assms
-  by (simp add:int_mod_eq')
+  by simp
 
 lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i"
   unfolding steps_def
@@ -186,11 +186,11 @@
     (is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
   proof -
     have "a mod ?MM = a" using \<open>0 <= a\<close> \<open>a <= ?M\<close>
-      by (simp add: int_mod_eq')
+      by simp
     have "?X mod ?MM = ?X" using \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>
-      by (simp add: int_mod_eq')
+      by simp
     have "e mod ?MM = e" using \<open>0 <= e\<close> \<open>e <= ?M\<close>
-      by (simp add: int_mod_eq')
+      by simp
     have "(?MM::int) = 2 ^ LENGTH(32)" by simp
     show ?thesis
       unfolding
@@ -226,11 +226,11 @@
     (is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
   proof -
     have "a' mod ?MM = a'" using \<open>0 <= a'\<close> \<open>a' <= ?M\<close>
-      by (simp add: int_mod_eq')
+      by simp
     have "?X mod ?MM = ?X" using \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>
-      by (simp add: int_mod_eq')
+      by simp
     have "e' mod ?MM = e'" using \<open>0 <= e'\<close> \<open>e' <= ?M\<close>
-      by (simp add: int_mod_eq')
+      by simp
     have "(?MM::int) = 2 ^ LENGTH(32)" by simp
     have nat_transfer: "79 - nat j = nat (79 - j)"
       using nat_diff_distrib \<open>0 <= j\<close>  \<open>j <= 79\<close>
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/Bit_Lists.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Lists.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -0,0 +1,137 @@
+(*  Title:      HOL/Word/Bit_Lists.thy
+    Author:     Jeremy Dawson, NICTA
+*)
+
+section \<open>Bit values as reversed lists of bools\<close>
+
+theory Bit_Lists
+  imports Bits_Int
+begin
+
+subsection \<open>Implicit augmentation of list prefixes\<close>
+
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+    Z: "takefill fill 0 xs = []"
+  | Suc: "takefill fill (Suc n) xs =
+      (case xs of
+        [] \<Rightarrow> fill # takefill fill n xs
+      | y # ys \<Rightarrow> y # takefill fill n ys)"
+
+lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
+  apply (induct n arbitrary: m l)
+   apply clarsimp
+  apply clarsimp
+  apply (case_tac m)
+   apply (simp split: list.split)
+  apply (simp split: list.split)
+  done
+
+lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
+  by (induct n arbitrary: l) (auto split: list.split)
+
+lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
+  by (simp add: takefill_alt replicate_add [symmetric])
+
+lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+  by (induct m arbitrary: l n) (auto split: list.split)
+
+lemma length_takefill [simp]: "length (takefill fill n l) = n"
+  by (simp add: takefill_alt)
+
+lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
+  by (induct k arbitrary: w n) (auto split: list.split)
+
+lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
+  by (induct k arbitrary: w) (auto split: list.split)
+
+lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+  by (auto simp: le_iff_add takefill_le')
+
+lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
+  by (auto simp: le_iff_add take_takefill')
+
+lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
+  by (induct xs) auto
+
+lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
+  by (induct xs arbitrary: l) auto
+
+lemmas takefill_same [simp] = takefill_same' [OF refl]
+
+lemma tf_rev:
+  "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
+    rev (takefill y m (rev (takefill x k (rev bl))))"
+  apply (rule nth_equalityI)
+   apply (auto simp add: nth_takefill rev_nth)
+  apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
+  apply arith
+  done
+
+lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
+  by auto
+
+lemmas takefill_Suc_cases =
+  list.cases [THEN takefill.Suc [THEN trans]]
+
+lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
+lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
+
+lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
+  takefill_minus [symmetric, THEN trans]]
+
+lemma takefill_numeral_Nil [simp]:
+  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
+  by (simp add: numeral_eq_Suc)
+
+lemma takefill_numeral_Cons [simp]:
+  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
+  by (simp add: numeral_eq_Suc)
+
+
+subsection \<open>Range projection\<close>
+
+definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
+  where "bl_of_nth n f = map f (rev [0..<n])"
+
+lemma bl_of_nth_simps [simp, code]:
+  "bl_of_nth 0 f = []"
+  "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+  by (simp_all add: bl_of_nth_def)
+
+lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
+  by (simp add: bl_of_nth_def)
+
+lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
+  by (simp add: bl_of_nth_def rev_map)
+
+lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
+  by (simp add: bl_of_nth_def)
+
+lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
+  apply (induct n arbitrary: xs)
+   apply clarsimp
+  apply clarsimp
+  apply (rule trans [OF _ hd_Cons_tl])
+   apply (frule Suc_le_lessD)
+   apply (simp add: rev_nth trans [OF drop_Suc drop_tl, symmetric])
+   apply (subst hd_drop_conv_nth)
+    apply force
+   apply simp_all
+  apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
+  apply simp
+  done
+
+lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
+  by (simp add: bl_of_nth_nth_le)
+
+lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
+  apply (rule nth_equalityI)
+   apply simp
+  apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
+  done
+
+lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
+  by (simp add: takefill_bintrunc)
+
+end
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -9,9 +9,16 @@
 section \<open>Bitwise Operations on integers\<close>
 
 theory Bits_Int
-  imports Misc_Auxiliary Bits
+  imports Bits
 begin
 
+subsection \<open>Generic auxiliary\<close>
+
+lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
+  for a n :: int
+  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
+
+
 subsection \<open>Implicit bit representation of \<^typ>\<open>int\<close>\<close>
 
 abbreviation (input) bin_last :: "int \<Rightarrow> bool"
@@ -256,6 +263,10 @@
     by (auto elim!: evenE oddE simp add: mult_mod_right ac_simps)
 qed
 
+lemma sbintrunc_eq_take_bit:
+  \<open>sbintrunc n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
+  by (simp add: sbintrunc_mod2p take_bit_eq_mod)
+
 lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
   by (simp add: bintrunc_mod2p bin_sign_def)
 
@@ -464,47 +475,59 @@
   by (rule ext) (rule bintrunc_mod2p)
 
 lemma range_bintrunc: "range (bintrunc n) = {i. 0 \<le> i \<and> i < 2 ^ n}"
-  apply (unfold no_bintr_alt1)
-  apply (auto simp add: image_iff)
-  apply (rule exI)
-  apply (rule sym)
-  using int_mod_lem [symmetric, of "2 ^ n"]
-  apply auto
-  done
+  by (auto simp add: take_bit_eq_mod image_iff) (metis mod_pos_pos_trivial)
 
 lemma no_sbintr_alt2: "sbintrunc n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
   by (rule ext) (simp add : sbintrunc_mod2p)
 
 lemma range_sbintrunc: "range (sbintrunc n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}"
-  apply (unfold no_sbintr_alt2)
-  apply (auto simp add: image_iff eq_diff_eq)
-
-  apply (rule exI)
-  apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
-  done
-
-lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
-  for a :: int
-  using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"]
-  by simp
-
-lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
-  for a :: int
-  by (rule sb_inc_lem) simp
-
-lemma sbintrunc_inc: "x < - (2^n) \<Longrightarrow> x + 2^(Suc n) \<le> sbintrunc n x"
-  unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
-
-lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
-  for a :: int
-  using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
-
-lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
-  for a :: int
-  by (rule sb_dec_lem) simp
-
-lemma sbintrunc_dec: "x \<ge> (2 ^ n) \<Longrightarrow> x - 2 ^ (Suc n) >= sbintrunc n x"
-  unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
+proof -
+  have \<open>surj (\<lambda>k::int. k + 2 ^ n)\<close>
+    by (rule surjI [of _ \<open>(\<lambda>k. k - 2 ^ n)\<close>]) simp
+  moreover have \<open>sbintrunc n = ((\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n))\<close>
+    by (simp add: sbintrunc_eq_take_bit fun_eq_iff)
+  ultimately show ?thesis
+    apply (simp only: fun.set_map range_bintrunc)
+    apply (auto simp add: image_iff)
+    apply presburger
+    done
+qed
+
+lemma take_bit_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_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 sbintrunc_inc:
+  \<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
+  using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
+  by (simp add: sbintrunc_eq_take_bit)
+
+lemma sbintrunc_dec:
+  \<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
+  using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
+  by (simp add: sbintrunc_eq_take_bit)
 
 lemma bintr_ge0: "0 \<le> bintrunc n w"
   by (simp add: bintrunc_mod2p)
@@ -513,8 +536,8 @@
   by (simp add: bintrunc_mod2p)
 
 lemma bintr_Min: "bintrunc n (- 1) = 2 ^ n - 1"
-  by (simp add: bintrunc_mod2p m1mod2k)
-
+  by (simp add: stable_imp_take_bit_eq)
+  
 lemma sbintr_ge: "- (2 ^ n) \<le> sbintrunc n w"
   by (simp add: sbintrunc_mod2p)
 
@@ -540,7 +563,7 @@
   by (auto simp add: take_bit_Suc)
 
 lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
-  by (induct n arbitrary: bin) auto
+  by simp
 
 lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
   by (induct n arbitrary: bin) (simp_all add: take_bit_Suc)
@@ -609,8 +632,12 @@
 proof -
   have \<open>0 \<le> x\<close> if \<open>0 \<le> x * 2 ^ n + y mod 2 ^ n\<close>
   proof -
-    from that have \<open>x \<noteq> - 1\<close>
-      using int_mod_le' [of \<open>y mod 2 ^ n\<close> \<open>2 ^ n\<close>] by auto
+    have \<open>y mod 2 ^ n < 2 ^ n\<close>
+      using pos_mod_bound [of \<open>2 ^ n\<close> y] by simp
+    then have \<open>\<not> y mod 2 ^ n \<ge> 2 ^ n\<close>
+      by (simp add: less_le)
+    with that have \<open>x \<noteq> - 1\<close>
+      by auto
     have *: \<open>- 1 \<le> (- (y mod 2 ^ n)) div 2 ^ n\<close>
       by (simp add: zdiv_zminus1_eq_if)
     from that have \<open>- (y mod 2 ^ n) \<le> x * 2 ^ n\<close>
@@ -1858,11 +1885,14 @@
 
 lemma nth_bin_to_bl_aux:
   "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
-    (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
+    (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
   apply (induction bl arbitrary: w)
    apply simp_all
-   apply (metis add.right_neutral bin_nth_bl bin_to_bl_def diff_Suc_less less_Suc_eq_0_disj less_imp_Suc_add list.size(3) nth_rev_alt size_bin_to_bl_aux)
-  apply (metis One_nat_def Suc_pred add_diff_cancel_left' add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def cancel_comm_monoid_add_class.diff_cancel diff_Suc_Suc diff_is_0_eq diff_zero le_add_diff_inverse le_eq_less_or_eq less_Suc_eq_0_disj less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append order_refl size_bin_to_bl_aux)
+   apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
+   apply (metis One_nat_def Suc_pred add_diff_cancel_left'
+     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
+     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
+     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
   done
 
 lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
@@ -2030,19 +2060,10 @@
   "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
   using bin_split_take by simp
 
-lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
-  apply (rule nth_equalityI)
-   apply simp
-  apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
-  done
-
-lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
-  by (simp add: takefill_bintrunc)
-
 lemma bl_bin_bl_rep_drop:
   "bin_to_bl n (bl_to_bin bl) =
     replicate (n - length bl) False @ drop (length bl - n) bl"
-  by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
+  by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
 
 lemma bl_to_bin_aux_cat:
   "bl_to_bin_aux bs (bin_cat w nv v) =
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/Misc_Arithmetic.thy
--- a/src/HOL/Word/Misc_Arithmetic.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Misc_Arithmetic.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -3,9 +3,49 @@
 section \<open>Miscellaneous lemmas, mostly for arithmetic\<close>
 
 theory Misc_Arithmetic
-  imports Misc_Auxiliary
+  imports Main Bits_Int
 begin
 
+lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
+  for b n :: int
+  apply safe
+    apply (erule (1) mod_pos_pos_trivial)
+   apply (erule_tac [!] subst)
+   apply auto
+  done
+
+lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
+  for b n :: int
+  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
+
+lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+  for b n :: int
+  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
+
+lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+  for n d :: int
+  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
+
+lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
+  by (rule zmod_minus1) simp
+
+lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+  for a :: int
+  using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"]
+  by simp
+
+lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+  for a :: int
+  by (rule sb_inc_lem) simp
+
+lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+  for a :: int
+  using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
+
+lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+  for a :: int
+  by (rule sb_dec_lem) simp
+
 lemma one_mod_exp_eq_one [simp]:
   "1 mod (2 * 2 ^ n) = (1::int)"
   using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/Misc_Auxiliary.thy
--- a/src/HOL/Word/Misc_Auxiliary.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Misc_Auxiliary.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -8,42 +8,6 @@
   imports Main
 begin
 
-subsection \<open>Arithmetic lemmas\<close>
-
-lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
-  for b n :: int
-  apply safe
-    apply (erule (1) mod_pos_pos_trivial)
-   apply (erule_tac [!] subst)
-   apply auto
-  done
-
-lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
-  for a n :: int
-  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
-
-lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
-  for b n :: int
-  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
-
-lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
-  for b n :: int
-  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
-
-lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
-  for n d :: int
-  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
-
-lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
-  by (rule zmod_minus1) simp
-
-lemma sub_inc_One: "Num.sub (Num.inc n) num.One = numeral n"
-  by (metis add_diff_cancel add_neg_numeral_special(3) add_uminus_conv_diff numeral_inc)
-  
-lemma inc_BitM: "Num.inc (Num.BitM n) = num.Bit0 n"
-  by (simp add: BitM_plus_one[symmetric] add_One)
-
-
 subsection \<open>Lemmas on list operations\<close>
 
 lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
@@ -58,122 +22,4 @@
 lemma hd_butlast: "length xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
   by (cases xs) auto
 
-
-subsection \<open>Implicit augmentation of list prefixes\<close>
-
-primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-    Z: "takefill fill 0 xs = []"
-  | Suc: "takefill fill (Suc n) xs =
-      (case xs of
-        [] \<Rightarrow> fill # takefill fill n xs
-      | y # ys \<Rightarrow> y # takefill fill n ys)"
-
-lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
-  apply (induct n arbitrary: m l)
-   apply clarsimp
-  apply clarsimp
-  apply (case_tac m)
-   apply (simp split: list.split)
-  apply (simp split: list.split)
-  done
-
-lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
-  by (induct n arbitrary: l) (auto split: list.split)
-
-lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
-  by (simp add: takefill_alt replicate_add [symmetric])
-
-lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
-  by (induct m arbitrary: l n) (auto split: list.split)
-
-lemma length_takefill [simp]: "length (takefill fill n l) = n"
-  by (simp add: takefill_alt)
-
-lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
-  by (induct k arbitrary: w n) (auto split: list.split)
-
-lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
-  by (induct k arbitrary: w) (auto split: list.split)
-
-lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
-  by (auto simp: le_iff_add takefill_le')
-
-lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
-  by (auto simp: le_iff_add take_takefill')
-
-lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
-  by (induct xs) auto
-
-lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
-  by (induct xs arbitrary: l) auto
-
-lemmas takefill_same [simp] = takefill_same' [OF refl]
-
-lemma tf_rev:
-  "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
-    rev (takefill y m (rev (takefill x k (rev bl))))"
-  apply (rule nth_equalityI)
-   apply (auto simp add: nth_takefill nth_rev)
-  apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
-  apply arith
-  done
-
-lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
-  by auto
-
-lemmas takefill_Suc_cases =
-  list.cases [THEN takefill.Suc [THEN trans]]
-
-lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
-lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
-
-lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
-  takefill_minus [symmetric, THEN trans]]
-
-lemma takefill_numeral_Nil [simp]:
-  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
-  by (simp add: numeral_eq_Suc)
-
-lemma takefill_numeral_Cons [simp]:
-  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
-  by (simp add: numeral_eq_Suc)
-
-
-subsection \<open>Auxiliary: Range projection\<close>
-
-definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
-  where "bl_of_nth n f = map f (rev [0..<n])"
-
-lemma bl_of_nth_simps [simp, code]:
-  "bl_of_nth 0 f = []"
-  "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
-  by (simp_all add: bl_of_nth_def)
-
-lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
-  by (simp add: bl_of_nth_def)
-
-lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
-  by (simp add: bl_of_nth_def rev_map)
-
-lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
-  by (simp add: bl_of_nth_def)
-
-lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
-  apply (induct n arbitrary: xs)
-   apply clarsimp
-  apply clarsimp
-  apply (rule trans [OF _ hd_Cons_tl])
-   apply (frule Suc_le_lessD)
-   apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
-   apply (subst hd_drop_conv_nth)
-    apply force
-   apply simp_all
-  apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
-  apply simp
-  done
-
-lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
-  by (simp add: bl_of_nth_nth_le)
-
 end
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/More_Word.thy
--- a/src/HOL/Word/More_Word.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/More_Word.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -7,6 +7,8 @@
 imports
   Word
   Ancient_Numeral
+  Misc_Auxiliary
+  Misc_Arithmetic
 begin
 
 end
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Word.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -11,8 +11,8 @@
   "HOL-Library.Bit_Operations"
   Bits_Int
   Bit_Comprehension
+  Bit_Lists
   Misc_Typedef
-  Misc_Arithmetic
 begin
 
 subsection \<open>Type definition\<close>
@@ -1290,7 +1290,7 @@
 
 lemma lt2p_lem: "LENGTH('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
   for w :: "'a::len word"
-  by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
+  by (metis bintr_lt2p bintr_uint)
 
 lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
   by (fact uint_ge_0 [THEN leD, THEN antisym_conv1])
@@ -1953,7 +1953,7 @@
   unfolding word_le_def by auto
 
 lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
-  by (simp only: word_le_def word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
+  by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p)
 
 lemma word_n1_ge [simp]: "y \<le> -1"
   for y :: "'a::len word"
@@ -2056,28 +2056,34 @@
   "(uint x + uint y < 2 ^ LENGTH('a)) =
     (uint (x + y) = uint x + uint y)"
   for x y :: "'a::len word"
-  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
+  by (metis add.right_neutral add_mono_thms_linordered_semiring(1) mod_pos_pos_trivial of_nat_0_le_iff uint_lt2p uint_nat uint_word_ariths(1))
 
 lemma uint_mult_lem:
   "(uint x * uint y < 2 ^ LENGTH('a)) =
     (uint (x * y) = uint x * uint y)"
   for x y :: "'a::len word"
-  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
+  by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3))
 
 lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
-  by (auto simp: uint_word_ariths intro!: trans [OF _ int_mod_lem])
+  by (metis (mono_tags, hide_lams) diff_ge_0_iff_ge mod_pos_pos_trivial of_nat_0_le_iff take_bit_eq_mod uint_nat uint_sub_lt2p word_sub_wi word_ubin.eq_norm)  find_theorems uint \<open>- _\<close>
 
 lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
-  unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
+  unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend) 
 
 lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
-  unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
-
+  unfolding uint_word_ariths by (simp add: int_mod_ge)
+  
 lemma mod_add_if_z:
   "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
     (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   for x y z :: int
-  by (auto intro: int_mod_eq)
+  apply (auto simp add: not_less)
+  apply (rule antisym)
+  apply (metis diff_ge_0_iff_ge minus_mod_self2 zmod_le_nonneg_dividend)
+   apply (simp only: flip: minus_mod_self2 [of \<open>x + y\<close> z])
+  apply (rule int_mod_ge)
+   apply simp_all
+  done
 
 lemma uint_plus_if':
   "uint (a + b) =
@@ -2090,7 +2096,13 @@
   "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
     (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
   for x y z :: int
-  by (auto intro: int_mod_eq)
+  apply (auto simp add: not_le)
+  apply (rule antisym)
+   apply (simp only: flip: mod_add_self2 [of \<open>x - y\<close> z])
+   apply (rule zmod_le_nonneg_dividend)
+   apply simp
+  apply (metis add.commute add.right_neutral add_le_cancel_left diff_ge_0_iff_ge int_mod_ge le_less le_less_trans mod_add_self1 not_le not_less)
+  done
 
 lemma uint_sub_if':
   "uint (a - b) =
@@ -2301,10 +2313,7 @@
 lemma udvd_incr_lem:
   "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
     uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq"
-  apply clarsimp
-  apply (drule less_le_mult)
-   apply safe
-  done
+  by auto (metis int_distrib(1) linorder_not_less mult.left_neutral mult_right_mono uint_nonnegative zless_imp_add1_zle)
 
 lemma udvd_incr':
   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
@@ -2344,11 +2353,16 @@
    prefer 2
    apply (insert uint_range' [of s])[1]
    apply arith
-  apply (drule add.commute [THEN xtr1])
-  apply (simp add: diff_less_eq [symmetric])
-  apply (drule less_le_mult)
-   apply arith
+  apply (drule add.commute [THEN xtrans(1)])
+  apply (simp flip: diff_less_eq)
+  apply (subst (asm) mult_less_cancel_right)
   apply simp
+  apply (simp add: diff_eq_eq not_less)
+  apply (subst (asm) (3) zless_iff_Suc_zadd)
+  apply auto
+    apply (auto simp add: algebra_simps)
+  apply (drule less_le_trans [of _ \<open>2 ^ LENGTH('a)\<close>]) apply assumption
+  apply (simp add: mult_less_0_iff)
   done
 
 \<comment> \<open>links with \<open>rbl\<close> operations\<close>
@@ -2527,15 +2541,27 @@
 lemma unat_add_lem:
   "unat x + unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
   for x y :: "'a::len word"
-  by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
+  apply (auto simp: unat_word_ariths)
+  apply (metis unat_lt2p word_unat.eq_norm)
+  done
 
 lemma unat_mult_lem:
   "unat x * unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
   for x y :: "'a::len word"
-  by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
-
-lemmas unat_plus_if' =
-  trans [OF unat_word_ariths(1) mod_nat_add, simplified]
+  apply (auto simp: unat_word_ariths)
+  apply (metis unat_lt2p word_unat.eq_norm)
+  done
+
+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)
+  apply (subst (asm) le_iff_add)
+  apply auto
+  apply (metis add_less_cancel_left add_less_cancel_right le_less_trans less_imp_le mod_less unat_lt2p)
+  done
 
 lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
   for a b x :: "'a::len word"
@@ -2568,30 +2594,22 @@
 
 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
 
-lemma unat_div: "unat (x div y) = unat x div unat y"
-  for x y :: " 'a::len word"
-  apply (simp add : unat_word_ariths)
-  apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
-  apply (rule div_le_dividend)
-  done
-
+lemma uint_div:
+  \<open>uint (x div y) = uint x div uint y\<close>
+  by (metis div_le_dividend le_less_trans mod_less uint_nat unat_lt2p unat_word_ariths(6) zdiv_int)
+
+lemma unat_div:
+  \<open>unat (x div y) = unat x div unat y\<close>
+  by (simp add: unat_def uint_div add: nat_div_distrib)
+
+lemma uint_mod:
+  \<open>uint (x mod y) = uint x mod uint y\<close>
+  by (metis (no_types, lifting) le_less_trans mod_by_0 mod_le_divisor mod_less neq0_conv uint_nat unat_lt2p unat_word_ariths(7) zmod_int)
+  
 lemma unat_mod: "unat (x mod y) = unat x mod unat y"
   for x y :: "'a::len word"
-  apply (clarsimp simp add : unat_word_ariths)
-  apply (cases "unat y")
-   prefer 2
-   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
-   apply (rule mod_le_divisor)
-   apply auto
-  done
-
-lemma uint_div: "uint (x div y) = uint x div uint y"
-  for x y :: "'a::len word"
-  by (simp add: uint_nat unat_div zdiv_int)
-
-lemma uint_mod: "uint (x mod y) = uint x mod uint y"
-  for x y :: "'a::len word"
-  by (simp add: uint_nat unat_mod zmod_int)
+  by (simp add: unat_def uint_mod add: nat_mod_distrib)
+
 
 text \<open>Definition of \<open>unat_arith\<close> tactic\<close>
 
@@ -2671,7 +2689,7 @@
   apply clarsimp
   apply (drule mult_le_mono1)
   apply (erule order_le_less_trans)
-  apply (rule xtr7 [OF unat_lt2p div_mult_le])
+  apply (metis add_lessD1 div_mult_mod_eq unat_lt2p)
   done
 
 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
@@ -2682,7 +2700,7 @@
   apply (simp add: unat_arith_simps)
   apply (drule (1) mult_less_mono1)
   apply (erule order_less_le_trans)
-  apply (rule div_mult_le)
+  apply auto
   done
 
 lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k"
@@ -2691,7 +2709,7 @@
   apply (simp add: unat_arith_simps)
   apply (drule mult_le_mono1)
   apply (erule order_trans)
-  apply (rule div_mult_le)
+  apply auto
   done
 
 lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ LENGTH('a)"
@@ -2705,12 +2723,8 @@
 
 lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ LENGTH('a)"
   for x y z :: "'a::len word"
-  apply (rule exI)
-  apply (rule conjI)
-   apply (rule zadd_diff_inverse)
-  apply uint_arith
-  done
-
+  by (metis add_diff_cancel_left' add_diff_eq uint_add_lem uint_plus_simple)
+  
 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
 
 lemmas plus_minus_no_overflow =
@@ -2727,32 +2741,20 @@
 
 lemmas thd = times_div_less_eq_dividend
 
-lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
+lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend
 
 lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n"
   for n b :: "'a::len word"
-  apply (unfold word_less_nat_alt word_arith_nat_defs)
-  apply (cut_tac y="unat b" in gt_or_eq_0)
-  apply (erule disjE)
-   apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse)
-  apply simp
-  done
+  by (fact div_mult_mod_eq)
 
 lemma word_div_mult_le: "a div b * b \<le> a"
   for a b :: "'a::len word"
-  apply (unfold word_le_nat_alt word_arith_nat_defs)
-  apply (cut_tac y="unat b" in gt_or_eq_0)
-  apply (erule disjE)
-   apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
-  apply simp
-  done
+  by (metis div_le_mult mult_not_zero order.not_eq_order_implies_strict order_refl word_zero_le)
 
 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < n"
   for m n :: "'a::len word"
-  apply (simp only: word_less_nat_alt word_arith_nat_defs)
-  apply (auto simp: uno_simps)
-  done
-
+  by (simp add: unat_arith_simps)
+  
 lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
   by (induct n) (simp_all add: wi_hom_mult [symmetric])
 
@@ -3039,9 +3041,9 @@
   for x y :: "'a::len word"
   by (auto simp: word_le_def uint_or intro: le_int_or)
 
-lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
-lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
-lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
+lemmas le_word_or1 = xtrans(3) [OF word_bw_comms (2) le_word_or2]
+lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2]
+lemmas word_and_le2 = xtrans(3) [OF word_ao_absorbs (8) [symmetric] le_word_or2]
 
 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
   unfolding to_bl_def word_log_defs bl_not_bin
@@ -3129,12 +3131,7 @@
   unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint)
 
 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
-  apply (unfold test_bit_bl)
-  apply clarsimp
-  apply (rule trans)
-   apply (rule nth_rev_alt)
-   apply (auto simp add: word_size)
-  done
+  by (simp add: word_size rev_nth test_bit_bl)
 
 lemma map_bit_interval_eq:
   \<open>map (bit w) [0..<n] = takefill False n (rev (to_bl w))\<close> for w :: \<open>'a::len word\<close>
@@ -3325,7 +3322,7 @@
 
 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
   for x :: "'a::len word"
-  apply (rule xtr3)
+  apply (rule xtrans(3))
    apply (rule_tac [2] y = "x" in le_word_or2)
   apply (rule word_eqI)
   apply (auto simp add: word_ao_nth nth_w2p word_size)
@@ -3433,7 +3430,7 @@
   by (simp add: shiftl1_def)
 
 lemma shiftl1_def_u: "shiftl1 w = word_of_int (2 * uint w)"
-  by (simp only: shiftl1_def) (* FIXME: duplicate *)
+  by (fact shiftl1_def)
 
 lemma shiftl1_def_s: "shiftl1 w = word_of_int (2 * sint w)"
   by (simp add: shiftl1_def wi_hom_syms)
@@ -3555,10 +3552,7 @@
   apply (unfold shiftr1_def)
   apply (rule word_uint.Abs_inverse)
   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
-  apply (rule xtr7)
-   prefer 2
-   apply (rule zdiv_le_dividend)
-    apply auto
+  apply (metis uint_lt2p uint_shiftr1)
   done
 
 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
@@ -3599,8 +3593,9 @@
 
 subsubsection \<open>shift functions in terms of lists of bools\<close>
 
-lemmas bshiftr1_numeral [simp] =
-  bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
+lemma bshiftr1_numeral [simp]:
+  \<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close>
+  by (simp add: bshiftr1_def)
 
 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
@@ -3742,7 +3737,9 @@
   finally show ?thesis .
 qed
 
-lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
+lemma shiftl_numeral [simp]:
+  \<open>numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)\<close>
+  by (fact shiftl_word_eq)
 
 lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
   by (simp add: shiftl_bl word_rep_drop word_size)
@@ -3778,19 +3775,23 @@
     word_of_int (bin_rest (sbintrunc (LENGTH('a) - 1) (numeral w)))"
   unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm)
 
-lemma shiftr_no [simp]:
-  (* FIXME: neg_numeral *)
-  "(numeral w::'a::len word) >> n = word_of_int
-    ((bin_rest ^^ n) (bintrunc (LENGTH('a)) (numeral w)))"
-  by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
-
-lemma sshiftr_no [simp]:
-  (* FIXME: neg_numeral *)
-  "(numeral w::'a::len word) >>> n = word_of_int
-    ((bin_rest ^^ n) (sbintrunc (LENGTH('a) - 1) (numeral w)))"
+text \<open>TODO: rules for \<^term>\<open>- (numeral n)\<close>\<close>
+
+lemma drop_bit_word_numeral [simp]:
+  \<open>drop_bit (numeral n) (numeral k) =
+    (word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
+lemma shiftr_numeral [simp]:
+  \<open>(numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)\<close>
+  by (fact shiftr_word_eq)
+
+lemma sshiftr_numeral [simp]:
+  \<open>(numeral k >>> numeral n :: 'a::len word) =
+    word_of_int (drop_bit (numeral n) (sbintrunc (LENGTH('a) - 1) (numeral k)))\<close>
   apply (rule word_eqI)
-  apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
-   apply (subgoal_tac "na + n = LENGTH('a) - Suc 0", simp, simp)+
+  apply (cases \<open>LENGTH('a)\<close>)
+   apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr nth_sbintr not_le not_less less_Suc_eq_le ac_simps)
   done
 
 lemma shiftr1_bl_of:
@@ -3938,24 +3939,18 @@
    apply simp
   apply (clarsimp simp add: to_bl_nth word_size)
   apply (simp add: word_size word_ops_nth_size)
-  apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
+  apply (auto simp add: word_size test_bit_bl nth_append rev_nth)
   done
 
 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
   by (simp only: and_mask_bintr bintrunc_mod2p)
 
 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
-  apply (simp add: and_mask_bintr word_ubin.eq_norm)
-  apply (simp add: bintrunc_mod2p)
-  apply (rule xtr8)
-   prefer 2
-   apply (rule pos_mod_bound)
-   apply auto
-  done
+  by (simp add: and_mask_bintr uint.abs_eq min_def not_le lt2p_lem bintr_lt2p)
 
 lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
   for b n :: int
-  by (simp add: int_mod_lem eq_sym_conv)
+  by auto (metis pos_mod_conj)+
 
 lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
   apply (simp add: and_mask_bintr)
@@ -3991,12 +3986,11 @@
 
 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
   for x :: "'a::len word"
-  apply (unfold word_less_alt word_numeral_alt)
-  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm
-      simp del: word_of_int_numeral)
-  apply (drule xtr8 [rotated])
-   apply (rule int_mod_le)
-   apply simp_all
+  apply (simp add: and_mask_bintr)
+  apply transfer
+  apply (simp add: ac_simps)
+  apply (auto simp add: min_def)
+  apply (metis bintrunc_bintrunc_ge mod_pos_pos_trivial mult.commute mult.left_neutral mult_zero_left not_le of_bool_def take_bit_eq_mod take_bit_nonnegative)
   done
 
 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
@@ -4521,8 +4515,6 @@
 
 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
 
-lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
-
 lemma nth_rcat_lem:
   "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
     rev (concat (map to_bl wl)) ! n =
@@ -4530,9 +4522,8 @@
   apply (induct wl)
    apply clarsimp
   apply (clarsimp simp add : nth_append size_rcat_lem)
-  apply (simp (no_asm_use) only:  mult_Suc [symmetric]
-         td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
-  apply clarsimp
+  apply (simp flip: mult_Suc minus_div_mult_eq_mod add: less_Suc_eq_le not_less)
+  apply (metis (no_types, lifting) diff_is_0_eq div_le_mono len_not_eq_0 less_Suc_eq less_mult_imp_div_less nonzero_mult_div_cancel_right not_le nth_Cons_0)
   done
 
 lemma test_bit_rcat:
@@ -4540,9 +4531,8 @@
     (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
   for wl :: "'a::len word list"
   apply (unfold word_rcat_bl word_size)
-  apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
-  apply safe
-   apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
+  apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size)
+  apply (metis div_le_mono len_gt_0 len_not_eq_0 less_mult_imp_div_less mod_less_divisor nonzero_mult_div_cancel_right not_le nth_rcat_lem test_bit_bl word_size)
   done
 
 lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
@@ -4558,8 +4548,10 @@
   for w :: \<open>'a::len word\<close>
   apply (rule trans)
    apply (rule test_bit_cong)
-   apply (rule nth_rev_alt)
+   apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, simplified rev_rev_ident])
+  apply simp
    apply (rule that(1))
+  apply simp
   apply (rule test_bit_rsplit)
     apply (rule refl)
   apply (rule asm_rl)
@@ -4589,13 +4581,13 @@
 lemma length_word_rsplit_even_size:
   "n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
     length (word_rsplit w :: 'a word list) = m"
-  by (auto simp: length_word_rsplit_exp_size given_quot_alt)
+  by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
 
 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
 
 \<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
 lemmas tdle = times_div_less_eq_dividend
-lemmas dtle = xtr4 [OF tdle mult.commute]
+lemmas dtle = xtrans(4) [OF tdle mult.commute]
 
 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
   apply (rule word_eqI)
@@ -4604,16 +4596,14 @@
     apply (simp_all add: word_size
       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
    apply safe
-   apply (erule xtr7, rule dtle)+
+   apply (erule xtrans(7), rule dtle)+
   done
 
 lemma size_word_rsplit_rcat_size:
   "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a)
     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
   for ws :: "'a::len word list" and frcw :: "'b::len word"
-  apply (clarsimp simp: word_size length_word_rsplit_exp_size')
-  apply (fast intro: given_quot_alt)
-  done
+  by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
 
 lemma msrevs:
   "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
@@ -4636,12 +4626,11 @@
   apply (rule trans)
    apply (rule test_bit_rcat [OF refl refl])
   apply (simp add: word_size)
-  apply (subst nth_rev)
+  apply (subst rev_nth)
    apply arith
-  apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
+  apply (simp add: le0 [THEN [2] xtrans(7), THEN diff_Suc_less])
   apply safe
   apply (simp add: diff_mult_distrib)
-  apply (rule mpl_lem)
    apply (cases "size ws")
     apply simp_all
   done
@@ -5234,7 +5223,8 @@
   for x y :: "'a::len word"
   apply (subst word_arith_nat_defs)
   apply (subst unat_of_nat)
-  apply (simp add:  mod_nat_add word_size)
+  apply (auto simp add: not_less word_size)
+  apply (metis not_le unat_plus_if' unat_word_ariths(1))
   done
 
 lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
@@ -5347,10 +5337,8 @@
 
 lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
   for n :: "'a::len word"
-  apply (simp add: word_rec_def unat_word_ariths)
-  apply (subst nat_mod_eq')
-   apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
-  apply simp
+  apply (auto simp add: word_rec_def unat_word_ariths)
+  apply (metis (mono_tags, lifting) old.nat.simps(7) unatSuc word_unat.Rep_inverse word_unat.eq_norm word_unat.td_th)
   done
 
 lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
diff -r c7ac6d4f3914 -r 4a013c92a091 src/HOL/Word/Word_Examples.thy
--- a/src/HOL/Word/Word_Examples.thy	Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Word_Examples.thy	Sat Jul 04 20:45:24 2020 +0000
@@ -81,7 +81,8 @@
 lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
 
 text "this is not exactly fast, but bearable"
-lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
+lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
+  by (simp add: numeral_eq_Suc)
 
 text "this works only for replicate n True"
 lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"