diff -r 8e5428ff35af -r bbe5d3ef2052 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Nov 22 18:26:54 2020 +0000
+++ b/src/HOL/Library/Word.thy	Thu Nov 26 18:09:02 2020 +0000
@@ -841,23 +841,15 @@
   show \<open>a div 1 = a\<close>
     for a :: \<open>'a word\<close>
     by transfer simp
+  have \<section>: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n"
+    by (metis le_less take_bit_eq_mod take_bit_nonnegative)
+  have less_power: "\<And>n i p. (i::int) mod numeral p ^ n < numeral p ^ n"
+    by simp
   show \<open>a mod b div b = 0\<close>
     for a b :: \<open>'a word\<close>
     apply transfer
-    apply (simp add: take_bit_eq_mod)
-    apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>])
-      apply simp_all
-     apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power)
-    using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp
-  proof -
-    fix aa :: int and ba :: int
-    have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n"
-      by (metis le_less take_bit_eq_mod take_bit_nonnegative)
-    have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
-      by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power)
-    then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
-      using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound)
-  qed
+    apply (simp add: take_bit_eq_mod mod_eq_0_iff_dvd dvd_def)
+    by (metis (no_types, hide_lams) "\<section>" Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign le_less_trans mult_eq_0_iff take_bit_eq_mod take_bit_nonnegative zdiv_eq_0_iff zmod_le_nonneg_dividend)
   show \<open>(1 + a) div 2 = a div 2\<close>
     if \<open>even a\<close>
     for a :: \<open>'a word\<close>
@@ -1655,10 +1647,7 @@
 
 lemma signed_ordering: \<open>ordering word_sle word_sless\<close>
   apply (standard; transfer)
-  apply simp_all
-  using signed_take_bit_decr_length_iff apply force
-  using signed_take_bit_decr_length_iff apply force
-  done
+  using signed_take_bit_decr_length_iff by force+
 
 lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
   by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
@@ -1930,11 +1919,15 @@
 lemma signed_drop_bit_signed_drop_bit [simp]:
   \<open>signed_drop_bit m (signed_drop_bit n w) = signed_drop_bit (m + n) w\<close>
   for w :: \<open>'a::len word\<close>
-  apply (cases \<open>LENGTH('a)\<close>)
-   apply simp_all
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps)
-  done
+proof (cases \<open>LENGTH('a)\<close>)
+  case 0
+  then show ?thesis
+    using len_not_eq_0 by blast
+next
+  case (Suc n)
+  then show ?thesis
+    by (force simp add: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI)
+qed
 
 lemma signed_drop_bit_0 [simp]:
   \<open>signed_drop_bit 0 w = w\<close>
@@ -1942,11 +1935,13 @@
 
 lemma sint_signed_drop_bit_eq:
   \<open>sint (signed_drop_bit n w) = drop_bit n (sint w)\<close>
-  apply (cases \<open>LENGTH('a)\<close>; cases n)
-     apply simp_all
-  apply (rule bit_eqI)
-  apply (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
-  done
+proof (cases \<open>LENGTH('a) = 0 \<or> n=0\<close>)
+  case False
+  then show ?thesis
+    apply simp
+    apply (rule bit_eqI)
+    by (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
+qed auto
 
 lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
   is \<open>\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)\<close>
@@ -1972,9 +1967,8 @@
     (drop_bit (n mod LENGTH('a)) (take_bit LENGTH('a) k))
     (take_bit (n mod LENGTH('a)) k)\<close>
   subgoal for n k l
-    apply (simp add: concat_bit_def nat_le_iff less_imp_le
+    by (simp add: concat_bit_def nat_le_iff less_imp_le
       take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>n mod LENGTH('a::len)\<close>])
-    done
   done
 
 lift_definition word_rotl :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close>
@@ -1982,9 +1976,8 @@
     (drop_bit (LENGTH('a) - n mod LENGTH('a)) (take_bit LENGTH('a) k))
     (take_bit (LENGTH('a) - n mod LENGTH('a)) k)\<close>
   subgoal for n k l
-    apply (simp add: concat_bit_def nat_le_iff less_imp_le
+    by (simp add: concat_bit_def nat_le_iff less_imp_le
       take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>LENGTH('a) - n mod LENGTH('a::len)\<close>])
-    done
   done
 
 lift_definition word_roti :: \<open>int \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word\<close>
@@ -1992,9 +1985,8 @@
     (drop_bit (nat (r mod int LENGTH('a))) (take_bit LENGTH('a) k))
     (take_bit (nat (r mod int LENGTH('a))) k)\<close>
   subgoal for r k l
-    apply (simp add: concat_bit_def nat_le_iff less_imp_le
+    by (simp add: concat_bit_def nat_le_iff less_imp_le
       take_bit_tightened [of \<open>LENGTH('a)\<close> k l \<open>nat (r mod int LENGTH('a::len))\<close>])
-    done
   done
 
 lemma word_rotl_eq_word_rotr [code]:
@@ -2102,9 +2094,7 @@
     (uint (take_bit (n mod LENGTH('a)) w))\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
-  apply (simp add: concat_bit_def take_bit_drop_bit push_bit_take_bit min_def)
-  using mod_less_divisor not_less apply blast
-  done
+  by (simp add: min.absorb2 take_bit_concat_bit_eq)
 
 lemma [code]:
   \<open>Word.the_int (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a))
@@ -2253,10 +2243,7 @@
 lemma sint_numeral:
   "sint (numeral b :: 'a::len word) =
     (numeral b + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)"
-  apply (transfer fixing: b)
-  using int_word_sint [of \<open>numeral b\<close>]
-  apply simp
-  done
+  by (metis int_word_sint word_numeral_alt)
 
 lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0"
   by (fact of_int_0)
@@ -2492,15 +2479,13 @@
 lemma drop_bit_eq_zero_iff_not_bit_last:
   \<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close>
   for w :: "'a::len word"
-    apply (cases \<open>LENGTH('a)\<close>)
-    apply simp_all
-    apply (simp add: bit_iff_odd_drop_bit)
+proof (cases \<open>LENGTH('a)\<close>)
+  case (Suc n)
+  then show ?thesis
     apply transfer
     apply (simp add: take_bit_drop_bit)
-    apply (auto simp add: drop_bit_eq_div take_bit_eq_mod min_def)
-    apply (auto elim!: evenE)
-    apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral)
-    done
+    by (simp add: bit_iff_odd_drop_bit drop_bit_take_bit min.absorb2 odd_iff_mod_2_eq_one)
+qed auto
 
 
 subsection \<open>Word Arithmetic\<close>
@@ -2569,10 +2554,14 @@
     and "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)"
     and "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0"
     and "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1"
-         apply transfer apply (simp add: signed_take_bit_add)
-        apply transfer apply (simp add: signed_take_bit_diff)
-       apply transfer apply (simp add: signed_take_bit_mult)
-      apply transfer apply (simp add: signed_take_bit_minus)
+  subgoal
+    by transfer (simp add: signed_take_bit_add)
+  subgoal
+    by transfer (simp add: signed_take_bit_diff)
+  subgoal
+    by transfer (simp add: signed_take_bit_mult)
+  subgoal
+    by transfer (simp add: signed_take_bit_minus)
      apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_succ)
     apply (metis of_int_sint scast_id sint_sbintrunc' wi_hom_pred)
    apply (simp_all add: sint_uint)
@@ -2701,13 +2690,8 @@
 
 lemma udvd_unfold_int:
   \<open>a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. uint b = n * uint a)\<close>
-  apply (auto elim!: dvdE simp add: udvd_iff_dvd)
-   apply (simp only: uint_nat)
-   apply auto
-  using of_nat_0_le_iff apply blast
-  apply (simp only: unat_eq_nat_uint)
-  apply (simp add: nat_mult_distrib)
-  done
+  unfolding udvd_iff_dvd_int
+  by (metis dvd_div_mult_self dvd_triv_right uint_div_distrib uint_ge_0)
 
 lemma unat_minus_one:
   \<open>unat (w - 1) = unat w - 1\<close> if \<open>w \<noteq> 0\<close>
@@ -2777,15 +2761,11 @@
 qed
 
 lemma mod_add_if_z:
-  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+  "\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
     (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   for x y z :: int
-  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 (metis add.commute add_less_cancel_left add_mono_thms_linordered_field(5) diff_add_cancel diff_ge_0_iff_ge mod_pos_pos_trivial order_refl)
-  done
+  apply (simp add: not_less)
+  by (metis (no_types) add_strict_mono diff_ge_0_iff_ge diff_less_eq minus_mod_self2 mod_pos_pos_trivial)
 
 lemma uint_plus_if':
   "uint (a + b) =
@@ -2795,16 +2775,10 @@
   using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
 
 lemma mod_sub_if_z:
-  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+  "\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
     (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
   for x y z :: int
-  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_less)
-  done
+  using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp add: not_le)
 
 lemma uint_sub_if':
   "uint (a - b) =
@@ -2819,10 +2793,7 @@
 lemma word_of_int_inverse:
   "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> uint a = r"
   for a :: "'a::len word"
-  apply transfer
-  apply (drule sym)
-  apply (simp add: take_bit_int_eq_self)
-  done
+  by transfer (simp add: take_bit_int_eq_self)
 
 lemma uint_split:
   "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
@@ -3017,51 +2988,36 @@
 lemma udvd_incr':
   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
     uint q = ua + n' * uint K \<Longrightarrow> p + K \<le> q"
-  apply (unfold word_less_alt word_le_def)
-  apply (drule (2) udvd_incr_lem)
-  apply (erule uint_add_le [THEN order_trans])
-  done
+  unfolding word_less_alt word_le_def
+  by (metis (full_types) order_trans udvd_incr_lem uint_add_le)
 
 lemma udvd_decr':
-  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
-    uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K"
-  apply (unfold word_less_alt word_le_def)
-  apply (drule (2) udvd_incr_lem)
-  apply (drule le_diff_eq [THEN iffD2])
-  apply (erule order_trans)
-  apply (rule uint_sub_ge)
-  done
+  assumes "p < q" "uint p = ua + n * uint K" "uint q = ua + n' * uint K"
+    shows "uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K"
+proof -
+  have "\<And>w wa. uint (w::'a word) \<le> uint wa + uint (w - wa)"
+    by (metis (no_types) add_diff_cancel_left' diff_add_cancel uint_add_le)
+  moreover have "uint K + uint p \<le> uint q"
+    using assms by (metis (no_types) add_diff_cancel_left' diff_add_cancel udvd_incr_lem word_less_def)
+  ultimately show ?thesis
+    by (meson add_le_cancel_left order_trans word_less_eq_iff_unsigned)
+qed
 
 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
 
 lemma udvd_minus_le': "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy \<le> k - z"
-  apply (unfold udvd_unfold_int)
-  apply clarify
-  apply (erule (2) udvd_decr0)
-  done
+  unfolding udvd_unfold_int
+  by (meson udvd_decr0)
 
 lemma udvd_incr2_K:
   "p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow>
     0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
-  supply [[simproc del: linordered_ring_less_cancel_factor]]
-  apply (unfold udvd_unfold_int)
-  apply clarify
+  unfolding udvd_unfold_int
   apply (simp add: uint_arith_simps split: if_split_asm)
-   prefer 2
-  using uint_lt2p [of s] apply simp
-  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
+  apply (metis (no_types, hide_lams) le_add_diff_inverse le_less_trans udvd_incr_lem)
+  using uint_lt2p [of s] by simp
 
 
 subsection \<open>Arithmetic type class instantiations\<close>
@@ -3079,10 +3035,7 @@
 lemma iszero_word_no [simp]:
   "iszero (numeral bin :: 'a::len word) =
     iszero (take_bit LENGTH('a) (numeral bin :: int))"
-  apply (simp add: iszero_def)
-  apply transfer
-  apply simp
-  done
+  by (metis iszero_def uint_0_iff uint_bintrunc)
 
 text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close>
 
@@ -3093,10 +3046,7 @@
 subsection \<open>Word and nat\<close>
 
 lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ LENGTH('a)"
-  apply (rule allI)
-  apply (rule exI [of _ \<open>unat w\<close> for w :: \<open>'a word\<close>])
-  apply simp
-  done
+  by (metis of_nat_unat ucast_id unsigned_less)
 
 lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ LENGTH('a))"
   for w :: "'a::len word"
@@ -3174,36 +3124,24 @@
 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"
-  apply (auto simp: unat_word_ariths)
-  apply (drule sym)
-  apply (metis unat_of_nat unsigned_less)
-  done
+  by (metis mod_less unat_word_ariths(1) unsigned_less)
 
 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"
-  apply (auto simp: unat_word_ariths)
-  apply (drule sym)
-  apply (metis unat_of_nat unsigned_less)
-  done
+  by (metis mod_less unat_word_ariths(2) unsigned_less)
 
 lemma unat_plus_if':
   \<open>unat (a + b) =
     (if unat a + unat b < 2 ^ LENGTH('a)
     then unat a + unat b
     else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
-  apply (auto simp: unat_word_ariths not_less)
-  apply (subst (asm) le_iff_add)
-  apply auto
-  apply (simp flip: take_bit_eq_mod add: take_bit_nat_eq_self_iff)
-  apply (metis add.commute add_less_cancel_right le_less_trans less_imp_le unsigned_less)
-  done
+  apply (auto simp: unat_word_ariths not_less le_iff_add)
+  by (metis add.commute add_less_cancel_right add_strict_mono mod_less unsigned_less)
 
 lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
   for a b x :: "'a::len word"
-  apply (erule order_trans)
-  apply (erule olen_add_eqv [THEN iffD1])
-  done
+  using word_le_plus_either by blast
 
 lemmas un_ui_le =
   trans [OF word_le_nat_alt [symmetric] word_le_def]
@@ -3213,21 +3151,20 @@
     (if unat y \<le> unat x
      then unat x - unat y
      else unat x + 2 ^ size x - unat y)"
-  supply nat_uint_eq [simp del]
-  apply (unfold word_size)
-  apply (simp add: un_ui_le)
-  apply (auto simp add: unat_eq_nat_uint uint_sub_if')
-   apply (rule nat_diff_distrib)
-    prefer 3
-    apply (simp add: algebra_simps)
-    apply (rule nat_diff_distrib [THEN trans])
-      prefer 3
-      apply (subst nat_add_distrib)
-        prefer 3
-        apply (simp add: nat_power_eq)
-       apply auto
-  apply uint_arith
-  done
+proof -
+  { assume xy: "\<not> uint y \<le> uint x"
+    have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)"
+      by simp
+    also have "... = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
+      by (simp add: nat_diff_distrib')
+    also have "... = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
+      by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less)
+    finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
+  }
+  then show ?thesis
+  unfolding word_size
+  by (metis nat_diff_distrib' uint_sub_if' un_ui_le unat_eq_nat_uint unsigned_greater_eq)
+qed
 
 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
 
@@ -3261,10 +3198,7 @@
 lemma of_nat_inverse:
   \<open>word_of_nat r = a \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> unat a = r\<close>
   for a :: \<open>'a::len word\<close>
-  apply (drule sym)
-  apply transfer
-  apply (simp add: take_bit_int_eq_self)
-  done
+  by (metis mod_if unat_of_nat)
 
 lemma word_unat_eq_iff:
   \<open>v = w \<longleftrightarrow> unat v = unat w\<close>
@@ -3323,55 +3257,34 @@
 lemmas unat_plus_simple =
   trans [OF no_olen_add_nat unat_add_lem]
 
-lemma word_div_mult: "0 < y \<Longrightarrow> unat x * unat y < 2 ^ LENGTH('a) \<Longrightarrow> x * y div y = x"
+lemma word_div_mult: "\<lbrakk>0 < y; unat x * unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x * y div y = x"
   for x y :: "'a::len word"
-  apply unat_arith
-  apply clarsimp
-  apply (subst unat_mult_lem [THEN iffD1])
-   apply auto
-  done
+  by (simp add: unat_eq_zero unat_mult_lem word_arith_nat_div)
 
 lemma div_lt': "i \<le> k div x \<Longrightarrow> unat i * unat x < 2 ^ LENGTH('a)"
   for i k x :: "'a::len word"
-  apply unat_arith
-  apply clarsimp
-  apply (drule mult_le_mono1)
-  apply (erule order_le_less_trans)
-  apply (metis add_lessD1 div_mult_mod_eq unsigned_less)
-  done
+  by unat_arith (meson le_less_trans less_mult_imp_div_less not_le unsigned_less)
 
 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
 
-lemma div_lt_mult: "i < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
+lemma div_lt_mult: "\<lbrakk>i < k div x; 0 < x\<rbrakk> \<Longrightarrow> i * x < k"
   for i k x :: "'a::len word"
-  apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
-  apply (simp add: unat_arith_simps)
-  apply (drule (1) mult_less_mono1)
-  apply (erule order_less_le_trans)
-  apply auto
-  done
-
-lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k"
+  by (metis div_le_mono div_lt'' not_le unat_div word_div_mult word_less_iff_unsigned)
+
+lemma div_le_mult: "\<lbrakk>i \<le> k div x; 0 < x\<rbrakk> \<Longrightarrow> i * x \<le> k"
   for i k x :: "'a::len word"
-  apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
-  apply (simp add: unat_arith_simps)
-  apply (drule mult_le_mono1)
-  apply (erule order_trans)
-  apply auto
-  done
+  by (metis div_lt' less_mult_imp_div_less not_less unat_arith_simps(2) unat_div unat_mult_lem)
 
 lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ LENGTH('a)"
   for i k x :: "'a::len word"
-  apply (unfold uint_nat)
-  apply (drule div_lt')
-  apply (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
-  done
+  unfolding uint_nat
+  by (metis div_lt' int_ops(7) of_nat_unat uint_mult_lem unat_mult_lem)
 
 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
 
 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"
-  by (metis add_diff_cancel_left' add_diff_eq uint_add_lem uint_plus_simple)
+  by (metis add.commute diff_add_cancel no_olen_add)
   
 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
 
@@ -3420,13 +3333,8 @@
 subsection \<open>Cardinality, finiteness of set of words\<close>
 
 lemma inj_on_word_of_int: \<open>inj_on (word_of_int :: int \<Rightarrow> 'a word) {0..<2 ^ LENGTH('a::len)}\<close>
-  apply (rule inj_onI)
-  apply transfer
-  apply (simp add: take_bit_eq_mod)
-  done
-
-lemma inj_uint: \<open>inj uint\<close>
-  by (fact inj_unsigned)
+  unfolding inj_on_def
+  by (metis atLeastLessThan_iff word_of_int_inverse)
 
 lemma range_uint: \<open>range (uint :: 'a word \<Rightarrow> int) = {0..<2 ^ LENGTH('a::len)}\<close>
   apply transfer
@@ -3648,9 +3556,7 @@
   by simp
 
 lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
-  apply (cases \<open>n < LENGTH('a)\<close>; transfer)
-  apply auto
-  done
+  by (cases \<open>n < LENGTH('a)\<close>; transfer; force)
 
 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
   by (induct n) (simp_all add: wi_hom_syms)
@@ -3693,19 +3599,13 @@
 
 lemma uint_shiftr1: "uint (shiftr1 w) = uint w div 2"
   using drop_bit_eq_div [of 1 \<open>uint w\<close>, symmetric]
-  apply simp
-  apply transfer
-  apply (simp add: drop_bit_take_bit min_def)
-  done
+  by transfer (simp add: drop_bit_take_bit min_def)
 
 lemma bit_sshiftr1_iff [bit_simps]:
   \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
-  apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc)
-  using le_less_Suc_eq apply fastforce
-  using le_less_Suc_eq apply fastforce
-  done
+  by (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def le_Suc_eq simp flip: bit_Suc)
 
 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
   by (fact uint_shiftr1)
@@ -3718,7 +3618,6 @@
   \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
-  apply (simp add: bit_take_bit_iff flip: bit_Suc)
     apply (subst disjunctive_add)
    apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff simp flip: bit_Suc)
   done
@@ -3727,9 +3626,7 @@
 subsubsection \<open>shift functions in terms of lists of bools\<close>
 
 lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_shiftl1_iff bit_word_reverse_iff bit_shiftr1_iff Suc_diff_Suc)
-  done
+  by (intro bit_word_eqI) (auto simp add: bit_shiftl1_iff bit_word_reverse_iff bit_shiftr1_iff Suc_diff_Suc)
 
 \<comment> \<open>note -- the following results use \<open>'a::len word < number_ring\<close>\<close>
 
@@ -3758,42 +3655,33 @@
     (word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
   by transfer simp
 
-lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
-  apply (induct ys arbitrary: n)
-   apply simp_all
-  apply (case_tac n)
-   apply simp_all
-  done
-
-lemma align_lem_or [rule_format] :
-  "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
-    drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
-    map2 (|) x y = take m x @ drop m y"
-  apply (induct y)
-   apply force
-  apply clarsimp
-  apply (case_tac x)
-   apply force
-  apply (case_tac m)
-   apply auto
-  apply (drule_tac t="length xs" for xs in sym)
-  apply (auto simp: zip_replicate o_def)
-  done
-
-lemma align_lem_and [rule_format] :
-  "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
-    drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
-    map2 (\<and>) x y = replicate (n + m) False"
-  apply (induct y)
-   apply force
-  apply clarsimp
-  apply (case_tac x)
-   apply force
-  apply (case_tac m)
-  apply auto
-  apply (drule_tac t="length xs" for xs in sym)
-  apply (auto simp: zip_replicate o_def map_replicate_const)
-  done
+lemma False_map2_or: "\<lbrakk>set xs \<subseteq> {False}; length ys = length xs\<rbrakk> \<Longrightarrow> map2 (\<or>) xs ys = ys"
+  by (induction xs arbitrary: ys) (auto simp: length_Suc_conv)
+
+lemma align_lem_or:
+  assumes "length xs = n + m" "length ys = n + m" 
+    and "drop m xs = replicate n False" "take m ys = replicate m False"
+  shows "map2 (\<or>) xs ys = take m xs @ drop m ys"
+  using assms
+proof (induction xs arbitrary: ys m)
+  case (Cons a xs)
+  then show ?case
+    by (cases m) (auto simp: length_Suc_conv False_map2_or)
+qed auto
+
+lemma False_map2_and: "\<lbrakk>set xs \<subseteq> {False}; length ys = length xs\<rbrakk> \<Longrightarrow> map2 (\<and>) xs ys = xs"
+  by (induction xs arbitrary: ys) (auto simp: length_Suc_conv)
+
+lemma align_lem_and:
+  assumes "length xs = n + m" "length ys = n + m" 
+    and "drop m xs = replicate n False" "take m ys = replicate m False"
+  shows "map2 (\<and>) xs ys = replicate (n + m) False"
+  using assms
+proof (induction xs arbitrary: ys m)
+  case (Cons a xs)
+  then show ?case
+    by (cases m) (auto simp: length_Suc_conv set_replicate_conv_if False_map2_and)
+qed auto
 
 
 subsubsection \<open>Mask\<close>
@@ -3843,10 +3731,7 @@
   by transfer simp
 
 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
-  apply (simp flip: take_bit_eq_mask)
-  apply transfer
-  apply (auto simp add: min_def)
-  using antisym_conv take_bit_int_eq_self_iff by fastforce
+  by (metis take_bit_eq_mask take_bit_int_less_exp unsigned_take_bit_eq)
 
 lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
   apply (auto simp flip: take_bit_eq_mask)
@@ -3864,14 +3749,10 @@
   for w :: "'a::len word"
   by transfer simp
 
-lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
-  for x :: "'a::len word"
-  apply (cases \<open>n < LENGTH('a)\<close>)
-   apply (simp_all add: not_less flip: take_bit_eq_mask exp_eq_zero_iff)
-  apply transfer
-  apply (simp add: min_def)
-  apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit)
-  done
+lemma less_mask_eq:
+  fixes x :: "'a::len word"
+  assumes "x < 2 ^ n" shows "x AND mask n = x"
+  by (metis (no_types) assms lt2p_lem mask_eq_iff not_less word_2p_lem word_size)
 
 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
 
@@ -3899,40 +3780,14 @@
   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
-             apply (auto simp flip: take_bit_eq_mask)
-             apply transfer
-             apply (simp add: take_bit_eq_mod mod_simps)
-            apply transfer
-            apply (simp add: take_bit_eq_mod mod_simps)
-           apply transfer
-           apply (simp add: take_bit_eq_mod mod_simps)
-          apply transfer
-          apply (simp add: take_bit_eq_mod mod_simps)
-         apply transfer
-         apply (simp add: take_bit_eq_mod mod_simps)
-        apply transfer
-        apply (simp add: take_bit_eq_mod mod_simps)
-       apply transfer
-       apply (simp add: take_bit_eq_mod mod_simps)
-      apply transfer
-      apply (simp add: take_bit_eq_mod mod_simps)
-     apply transfer
-     apply (simp add: take_bit_eq_mod mod_simps)
-    apply transfer
-    apply (simp add: take_bit_eq_mod mod_simps)
-   apply transfer
-   apply (simp add: take_bit_eq_mod mod_simps)
-  apply transfer
-  apply (simp add: take_bit_eq_mod mod_simps)
-  done
+  unfolding take_bit_eq_mask [symmetric]
+  by (transfer; simp add: take_bit_eq_mod mod_simps)+
 
 lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
   for x :: \<open>'a::len word\<close>
   using word_of_int_Ex [where x=x]
-  apply (auto simp flip: take_bit_eq_mask)
-  apply transfer
-  apply (simp add: take_bit_eq_mod mod_simps)
-  done
+  unfolding take_bit_eq_mask [symmetric]
+  by (transfer; simp add: take_bit_eq_mod mod_simps)+
 
 lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)"
   by transfer (simp add: take_bit_minus_one_eq_mask)
@@ -3949,7 +3804,7 @@
   \<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
     \<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
   for w :: \<open>'a::len word\<close>
-  by (auto simp add: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff exp_eq_zero_iff not_less not_le ac_simps
+  by (auto simp add: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff not_less not_le ac_simps
     dest: bit_imp_le_length)
 
 definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
@@ -3967,10 +3822,7 @@
   unfolding slice_def by auto
 
 lemma ucast_slice1: "ucast w = slice1 (size w) w"
-  apply (simp add: slice1_def)
-  apply transfer
-  apply simp
-  done
+  unfolding slice1_def by (simp add: size_word.rep_eq)
 
 lemma ucast_slice: "ucast w = slice 0 w"
   by (simp add: slice_def slice1_def)
@@ -3987,20 +3839,16 @@
   from that have **: \<open>LENGTH('b) = n + k - LENGTH('a)\<close>
     by simp
   show \<open>bit (slice1 n (word_reverse w :: 'b word) :: 'a word) m \<longleftrightarrow> bit (word_reverse (slice1 k w :: 'a word)) m\<close>
-    apply (simp add: bit_slice1_iff bit_word_reverse_iff)
+    unfolding bit_slice1_iff bit_word_reverse_iff
     using * **
-    apply (cases \<open>n \<le> LENGTH('a)\<close>; cases \<open>k \<le> LENGTH('a)\<close>)
-       apply auto
-    done
+    by (cases \<open>n \<le> LENGTH('a)\<close>; cases \<open>k \<le> LENGTH('a)\<close>) auto
 qed
 
 lemma rev_slice:
   "n + k + LENGTH('a::len) = LENGTH('b::len) \<Longrightarrow>
     slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
-  apply (unfold slice_def word_size)
-  apply (rule rev_slice1)
-  apply arith
-  done
+  unfolding slice_def word_size
+  by (simp add: rev_slice1)
 
 
 subsubsection \<open>Revcast\<close>
@@ -4020,14 +3868,7 @@
 lemma revcast_rev_ucast [OF refl refl refl]:
   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
     rc = word_reverse uc"
-  apply auto
-  apply (rule bit_word_eqI)
-  apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
-   apply (simp_all add: bit_revcast_iff bit_word_reverse_iff bit_ucast_iff not_le
-     bit_imp_le_length)
-  using bit_imp_le_length apply fastforce
-  using bit_imp_le_length apply fastforce
-  done
+  by (metis rev_slice1 revcast_slice1 ucast_slice1 word_size)
 
 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
   using revcast_rev_ucast [of "word_reverse w"] by simp
@@ -4058,58 +3899,60 @@
 lemma word_cat_id: "word_cat a b = b"
   by transfer (simp add: take_bit_concat_bit_eq)
 
-lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_word_cat_iff not_less word_size word_split_def bit_ucast_iff bit_drop_bit_eq)
-  done
+lemma word_cat_split_alt: "\<lbrakk>size w \<le> size u + size v; word_split w = (u,v)\<rbrakk> \<Longrightarrow> word_cat u v = w"
+  unfolding word_split_def
+  by (rule bit_word_eqI) (auto simp add: bit_word_cat_iff not_less word_size bit_ucast_iff bit_drop_bit_eq)
 
 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
 
 
 subsubsection \<open>Split and slice\<close>
 
-lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w"
-  apply (auto simp add: word_split_def word_size)
-   apply (rule bit_word_eqI)
-   apply (simp add: bit_slice_iff bit_ucast_iff bit_drop_bit_eq)
-   apply (cases \<open>LENGTH('c) \<ge> LENGTH('b)\<close>)
-    apply (auto simp add: ac_simps dest: bit_imp_le_length)
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_slice_iff bit_ucast_iff dest: bit_imp_le_length)
-  done
+lemma split_slices:
+  assumes "word_split w = (u, v)"
+  shows "u = slice (size v) w \<and> v = slice 0 w"
+  unfolding word_size
+proof (intro conjI)
+  have \<section>: "\<And>n. \<lbrakk>ucast (drop_bit LENGTH('b) w) = u; LENGTH('c) < LENGTH('b)\<rbrakk> \<Longrightarrow> \<not> bit u n"
+    by (metis bit_take_bit_iff bit_word_of_int_iff diff_is_0_eq' drop_bit_take_bit less_imp_le less_nat_zero_code of_int_uint unsigned_drop_bit_eq)
+  show "u = slice LENGTH('b) w"
+  proof (rule bit_word_eqI)
+    show "bit u n = bit ((slice LENGTH('b) w)::'a word) n" if "n < LENGTH('a)" for n
+      using assms bit_imp_le_length
+      unfolding word_split_def bit_slice_iff
+      by (fastforce simp add: \<section> ac_simps word_size bit_ucast_iff bit_drop_bit_eq)
+  qed
+  show "v = slice 0 w"
+    by (metis Pair_inject assms ucast_slice word_split_bin')
+qed
+
 
 lemma slice_cat1 [OF refl]:
-  "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
-  done
+  "\<lbrakk>wc = word_cat a b; size a + size b \<le> size wc\<rbrakk> \<Longrightarrow> slice (size b) wc = a"
+  by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
 
 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
 
 lemma cat_slices:
-  "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
-    size a + size b >= size c \<Longrightarrow> word_cat a b = c"
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
-  done
+  "\<lbrakk>a = slice n c; b = slice 0 c; n = size b; size c \<le> size a + size b\<rbrakk> \<Longrightarrow> word_cat a b = c"
+  by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
 
 lemma word_split_cat_alt:
-  "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)"
-  apply (auto simp add: word_split_def word_size)
-   apply (rule bit_eqI)
-   apply (auto simp add: bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff dest: bit_imp_le_length)
-  apply (rule bit_eqI)
-   apply (auto simp add: bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff dest: bit_imp_le_length)
-  done
+  assumes "w = word_cat u v" and size: "size u + size v \<le> size w"
+  shows "word_split w = (u,v)"
+proof -
+  have "ucast ((drop_bit LENGTH('c) (word_cat u v))::'a word) = u" "ucast ((word_cat u v)::'a word) = v"
+    using assms
+    by (auto simp add: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI)
+  then show ?thesis
+    by (simp add: assms(1) word_split_bin')
+qed
 
 lemma horner_sum_uint_exp_Cons_eq:
   \<open>horner_sum uint (2 ^ LENGTH('a)) (w # ws) =
     concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)\<close>
   for ws :: \<open>'a::len word list\<close>
-  apply (simp add: concat_bit_eq push_bit_eq_mult)
-  apply transfer
-  apply simp
-  done
+  by (simp add: bintr_uint concat_bit_eq push_bit_eq_mult)
 
 lemma bit_horner_sum_uint_exp_iff:
   \<open>bit (horner_sum uint (2 ^ LENGTH('a)) ws) n \<longleftrightarrow>
@@ -4129,27 +3972,25 @@
 
 subsection \<open>Rotation\<close>
 
-lemma word_rotr_word_rotr_eq:
-  \<open>word_rotr m (word_rotr n w) = word_rotr (m + n) w\<close>
+lemma word_rotr_word_rotr_eq: \<open>word_rotr m (word_rotr n w) = word_rotr (m + n) w\<close>
   by (rule bit_word_eqI) (simp add: bit_word_rotr_iff ac_simps mod_add_right_eq)
 
-lemma word_rot_rl [simp]:
-  \<open>word_rotl k (word_rotr k v) = v\<close>
-  apply (rule bit_word_eqI)
-  apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
-  apply (auto dest: bit_imp_le_length)
-   apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
-  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
-  done
-
-lemma word_rot_lr [simp]:
-  \<open>word_rotr k (word_rotl k v) = v\<close>
-  apply (rule bit_word_eqI)
-  apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
-  apply (auto dest: bit_imp_le_length)
-   apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
-  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
-  done
+lemma word_rot_lem: "\<lbrakk>l + k = d + k mod l; n < l\<rbrakk> \<Longrightarrow> ((d + n) mod l) = n" for l::nat
+  by (metis (no_types, lifting) add.commute add.right_neutral add_diff_cancel_left' mod_if mod_mult_div_eq mod_mult_self2 mod_self)
+ 
+lemma word_rot_rl [simp]: \<open>word_rotl k (word_rotr k v) = v\<close>
+proof (rule bit_word_eqI)
+  show "bit (word_rotl k (word_rotr k v)) n = bit v n" if "n < LENGTH('a)" for n
+    using that
+    by (auto simp: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split)
+qed
+
+lemma word_rot_lr [simp]: \<open>word_rotr k (word_rotl k v) = v\<close>
+proof (rule bit_word_eqI)
+  show "bit (word_rotr k (word_rotl k v)) n = bit v n" if "n < LENGTH('a)" for n
+    using that
+    by (auto simp add: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split)
+qed
 
 lemma word_rot_gal:
   \<open>word_rotr n v = w \<longleftrightarrow> word_rotl n w = v\<close>
@@ -4173,10 +4014,7 @@
     using zmod_zminus1_eq_if [of \<open>1 + (int m + int n mod int LENGTH('a))\<close> \<open>int LENGTH('a)\<close>]
     apply simp_all
      apply (auto simp add: algebra_simps)
-     apply (simp add: minus_equation_iff [of \<open>int m\<close>])
-     apply (drule sym [of _ \<open>int m\<close>])
-    apply simp
-    apply (metis add.commute add_minus_cancel diff_minus_eq_add len_gt_0 less_imp_of_nat_less less_nat_zero_code mod_mult_self3 of_nat_gt_0 zmod_minus1)
+    apply (metis (mono_tags, hide_lams) Abs_fnat_hom_add mod_Suc mod_mult_self2_is_0 of_nat_Suc of_nat_mod semiring_char_0_class.of_nat_neq_0)
     apply (metis (no_types, hide_lams) Abs_fnat_hom_add less_not_refl mod_Suc of_nat_Suc of_nat_gt_0 of_nat_mod)
     done
   then have \<open>int ((m + n) mod LENGTH('a)) =
@@ -4220,23 +4058,7 @@
   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
-         apply (rule bit_word_eqI)
-         apply (auto simp add: bit_word_rotl_iff bit_not_iff algebra_simps exp_eq_zero_iff not_le)
-        apply (rule bit_word_eqI)
-        apply (auto simp add: bit_word_rotr_iff bit_not_iff algebra_simps exp_eq_zero_iff not_le)
-       apply (rule bit_word_eqI)
-       apply (auto simp add: bit_word_rotl_iff bit_and_iff algebra_simps exp_eq_zero_iff not_le)
-      apply (rule bit_word_eqI)
-      apply (auto simp add: bit_word_rotr_iff bit_and_iff algebra_simps exp_eq_zero_iff not_le)
-     apply (rule bit_word_eqI)
-     apply (auto simp add: bit_word_rotl_iff bit_or_iff algebra_simps exp_eq_zero_iff not_le)
-    apply (rule bit_word_eqI)
-    apply (auto simp add: bit_word_rotr_iff bit_or_iff algebra_simps exp_eq_zero_iff not_le)
-   apply (rule bit_word_eqI)
-   apply (auto simp add: bit_word_rotl_iff bit_xor_iff algebra_simps exp_eq_zero_iff not_le)
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_word_rotr_iff bit_xor_iff algebra_simps exp_eq_zero_iff not_le)
-  done
+  by (rule bit_word_eqI, auto simp add: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+
 
 end
 
@@ -4315,10 +4137,7 @@
     (if uint x + uint y < 2^size x
      then uint x + uint y
      else uint x + uint y - 2^size x)"
-  apply (simp only: word_arith_wis word_size uint_word_of_int_eq)
-  apply (auto simp add: not_less take_bit_int_eq_self_iff)
-  apply (metis not_less take_bit_eq_mod uint_plus_if' uint_word_ariths(1))
-  done
+  by (simp add: take_bit_eq_mod word_size uint_word_of_int_eq uint_plus_if')
 
 lemma unat_plus_if_size:
   "unat (x + y) =
@@ -4326,11 +4145,7 @@
      then unat x + unat y
      else unat x + unat y - 2^size x)"
   for x y :: "'a::len word"
-  apply (subst word_arith_nat_defs)
-  apply (subst unat_of_nat)
-  apply (auto simp add: not_less word_size)
-  apply (metis not_le unat_plus_if' unat_word_ariths(1))
-  done
+  by (simp add: size_word.rep_eq unat_arith_simps)
 
 lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
   for w :: "'a::len word"
@@ -4345,35 +4160,18 @@
     (if uint y \<le> uint x
      then uint x - uint y
      else uint x - uint y + 2^size x)"
-  apply (simp only: word_arith_wis word_size uint_word_of_int_eq)
-  apply (auto simp add: take_bit_int_eq_self_iff not_le)
-  apply (metis not_less uint_sub_if' uint_word_arith_bintrs(2))
-  done
+  by (simp add: size_word.rep_eq uint_sub_if')
 
 lemma unat_sub:
   \<open>unat (a - b) = unat a - unat b\<close>
   if \<open>b \<le> a\<close>
-proof -
-  from that have \<open>unat b \<le> unat a\<close>
-    by transfer simp
-  with that show ?thesis
-    apply transfer
-    apply simp
-    apply (subst take_bit_diff [symmetric])
-    apply (subst nat_take_bit_eq)
-     apply (simp add: nat_le_eq_zle)
-    apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less)
-    done
-qed
+  by (meson that unat_sub_if_size word_le_nat_alt)
 
 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
 
 lemma word_of_int_minus: "word_of_int (2^LENGTH('a) - i) = (word_of_int (-i)::'a::len word)"
-  apply transfer
-  apply (subst take_bit_diff [symmetric])
-  apply (simp add: take_bit_minus)
-  done
+  by simp
 
 lemma word_of_int_inj:
   \<open>(word_of_int x :: 'a::len word) = word_of_int y \<longleftrightarrow> x = y\<close>
@@ -4409,7 +4207,7 @@
   shows "(x - y) mod b = z' mod b'"
   using assms [symmetric] by (auto intro: mod_diff_cong)
 
-lemma word_induct_less:
+lemma word_induct_less [case_names zero less]:
   \<open>P m\<close> if zero: \<open>P 0\<close> and less: \<open>\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)\<close>
   for m :: \<open>'a::len word\<close>
 proof -
@@ -4435,12 +4233,7 @@
       then have **: \<open>n < (1 + word_of_nat q :: 'a word) \<longleftrightarrow> n \<le> (word_of_nat q :: 'a word)\<close> for n
         by (metis (no_types, lifting) add.commute inc_le le_less_trans not_less of_nat_Suc)
       have \<open>P (word_of_nat q)\<close>
-        apply (rule Suc.IH)
-        apply (rule Suc.prems)
-         apply (erule less_trans)
-         apply (rule *)
-        apply assumption
-        done
+        by (simp add: "**" Suc.IH Suc.prems)
       with * have \<open>P (1 + word_of_nat q)\<close>
         by (rule Suc.prems)
       then show ?thesis
@@ -4455,13 +4248,9 @@
   for P :: "'a::len word \<Rightarrow> bool"
   by (rule word_induct_less)
 
-lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
+lemma word_induct2 [case_names zero suc, induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
   for P :: "'b::len word \<Rightarrow> bool"
-  apply (rule word_induct_less)
-   apply simp_all
-  apply (case_tac "1 + na = 0")
-   apply auto
-  done
+by (induction rule: word_induct_less; force)
 
 
 subsection \<open>Recursion combinator for words\<close>
@@ -4469,90 +4258,68 @@
 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
   where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
 
-lemma word_rec_0: "word_rec z s 0 = z"
+lemma word_rec_0 [simp]: "word_rec z s 0 = z"
   by (simp add: word_rec_def)
 
-lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
+lemma word_rec_Suc [simp]: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
   for n :: "'a::len word"
-  apply (auto simp add: word_rec_def unat_word_ariths)
-  apply (metis (mono_tags, lifting) Abs_fnat_hom_add add_diff_cancel_left' o_def of_nat_1 old.nat.simps(7) plus_1_eq_Suc unatSuc unat_word_ariths(1) unsigned_1 word_arith_nat_add)
-  done
+  by (simp add: unatSuc word_rec_def)
 
 lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
-  apply (rule subst[where t="n" and s="1 + (n - 1)"])
-   apply simp
-  apply (subst word_rec_Suc)
-   apply simp
-  apply simp
-  done
+  by (metis add.commute diff_add_cancel word_rec_Suc)
 
 lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
-  by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
+  by (induct n) (simp_all add: word_rec_Suc)
 
 lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> (+) 1) n"
-  by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
+  by (induct n) (simp_all add: word_rec_Suc)
+
+
 
 lemma word_rec_twice:
   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> (+) (n - m)) m"
-  apply (erule rev_mp)
-  apply (rule_tac x=z in spec)
-  apply (rule_tac x=f in spec)
-  apply (induct n)
-   apply (simp add: word_rec_0)
-  apply clarsimp
-  apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
-   apply simp
-  apply (case_tac "1 + (n - m) = 0")
-   apply (simp add: word_rec_0)
-   apply (rule_tac f = "word_rec a b" for a b in arg_cong)
-   apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
-    apply simp
-   apply (simp (no_asm_use))
-  apply (simp add: word_rec_Suc word_rec_in2)
-  apply (erule impE)
-   apply uint_arith
-  apply (drule_tac x="x \<circ> (+) 1" in spec)
-  apply (drule_tac x="x 0 xa" in spec)
-  apply simp
-  apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst)
-   apply (clarsimp simp add: fun_eq_iff)
-   apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
-    apply simp
-   apply (rule refl)
-  apply (rule refl)
-  done
+proof (induction n arbitrary: z f)
+  case zero
+  then show ?case
+    by (metis diff_0_right word_le_0_iff word_rec_0)
+next
+  case (suc n z f)
+  show ?case
+  proof (cases "1 + (n - m) = 0")
+    case True
+    then show ?thesis
+      by (simp add: add_diff_eq)
+  next
+    case False
+    then have eq: "1 + n - m = 1 + (n - m)"
+      by simp
+    with False have "m \<le> n"
+      by (metis "suc.prems" add.commute dual_order.antisym eq_iff_diff_eq_0 inc_le leI)
+    with False "suc.hyps" show ?thesis
+      using suc.IH [of "f 0 z" "f \<circ> (+) 1"] 
+      by (simp add: word_rec_in2 eq add.assoc o_def)
+  qed
+qed
 
 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
-  by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
-
-lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
-  apply (erule rev_mp)
-  apply (induct n)
-   apply (auto simp add: word_rec_0 word_rec_Suc)
-   apply (drule spec, erule mp)
-   apply uint_arith
-  apply (drule_tac x=n in spec, erule impE)
-   apply uint_arith
-  apply simp
-  done
+  by (induct n) auto
+
+lemma word_rec_id_eq: "(\<And>m. m < n \<Longrightarrow> f m = id) \<Longrightarrow> word_rec z f n = z"
+  by (induction n) (auto simp add: unatSuc unat_arith_simps(2))
 
 lemma word_rec_max:
-  "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
-  apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
-   apply simp
-  apply simp
-  apply (rule word_rec_id_eq)
-  apply clarsimp
-  apply (drule spec, rule mp, erule mp)
-   apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
-    prefer 2
-    apply assumption
-   apply simp
-  apply (erule contrapos_pn)
-  apply simp
-  apply (drule arg_cong[where f="\<lambda>x. x - n"])
-  apply simp
-  done
+  assumes "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id"
+  shows "word_rec z f (- 1) = word_rec z f n"
+proof -
+  have \<section>: "\<And>m. \<lbrakk>m < - 1 - n\<rbrakk> \<Longrightarrow> (f \<circ> (+) n) m = id"
+    using assms
+    by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge)
+  have "word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)"
+    by (meson word_n1_ge word_rec_twice)
+  also have "... = word_rec z f n"
+    by (metis (no_types, lifting) \<section> diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq)
+  finally show ?thesis .
+qed
 
 
 subsection \<open>More\<close>