diff --git a/thys/Word_Lib/More_Divides.thy b/thys/Word_Lib/More_Divides.thy
--- a/thys/Word_Lib/More_Divides.thy
+++ b/thys/Word_Lib/More_Divides.thy
@@ -1,54 +1,55 @@
 (*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section "More Lemmas on Division"
 
 theory More_Divides
 imports Main
 begin
 
 lemma div_mult_le:
-  "(a::nat) div b * b \<le> a"
+  \<open>a div b * b \<le> a\<close> for a b :: nat
   by (fact div_times_less_eq_dividend)
 
 lemma diff_mod_le:
-  "\<lbrakk> (a::nat) < d; b dvd d \<rbrakk> \<Longrightarrow> a - a mod b \<le> d - b"
+  \<open>a - a mod b \<le> d - b\<close> if \<open>a < d\<close> \<open>b dvd d\<close> for a b d :: nat
+  using that
   apply(subst minus_mod_eq_mult_div)
   apply(clarsimp simp: dvd_def)
   apply(case_tac "b = 0")
    apply simp
   apply(subgoal_tac "a div b \<le> k - 1")
    prefer 2
    apply(subgoal_tac "a div b < k")
     apply(simp add: less_Suc_eq_le [symmetric])
    apply(subgoal_tac "b * (a div b) < b * ((b * k) div b)")
     apply clarsimp
    apply(subst div_mult_self1_is_m)
     apply arith
    apply(rule le_less_trans)
     apply simp
     apply(subst mult.commute)
     apply(rule div_mult_le)
    apply assumption
   apply clarsimp
   apply(subgoal_tac "b * (a div b) \<le> b * (k - 1)")
    apply(erule le_trans)
    apply(simp add: diff_mult_distrib2)
   apply simp
   done
 
 lemma int_div_same_is_1 [simp]:
-  "0 < a \<Longrightarrow> ((a :: int) div b = a) = (b = 1)"
-  by (metis div_by_1 abs_ge_zero abs_of_pos int_div_less_self neq_iff
+  \<open>a div b = a \<longleftrightarrow> b = 1\<close> if \<open>0 < a\<close> for a b :: int
+  using that by (metis div_by_1 abs_ge_zero abs_of_pos int_div_less_self neq_iff
             nonneg1_imp_zdiv_pos_iff zabs_less_one_iff)
 
+lemma int_div_minus_is_minus1 [simp]:
+  \<open>a div b = - a \<longleftrightarrow> b = - 1\<close> if \<open>0 > a\<close> for a b :: int
+  using that by (metis div_minus_right equation_minus_iff int_div_same_is_1 neg_0_less_iff_less)
+
 declare div_eq_dividend_iff [simp]
 
-lemma int_div_minus_is_minus1 [simp]:
-    "a < 0 \<Longrightarrow> ((a :: int) div b = -a) = (b = -1)"
-  by (metis div_minus_right equation_minus_iff int_div_same_is_1 neg_0_less_iff_less)
-
 end
diff --git a/thys/Word_Lib/Word_Lemmas_32.thy b/thys/Word_Lib/Word_Lemmas_32.thy
--- a/thys/Word_Lib/Word_Lemmas_32.thy
+++ b/thys/Word_Lib/Word_Lemmas_32.thy
@@ -1,312 +1,305 @@
 (*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section "Lemmas for Word Length 32"
 
 theory Word_Lemmas_32
 imports
   Word_Lemmas
   Word_Setup_32
 begin
 
 lemma ucast_8_32_inj:
   "inj (ucast ::  8 word \<Rightarrow> 32 word)"
   by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)
 
 lemma upto_2_helper:
   "{0..<2 :: 32 word} = {0, 1}"
   by (safe; simp) unat_arith
 
 lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def]
 lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def]
 lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def]
 
 lemma word_bits_len_of:
   "len_of TYPE (32) = word_bits"
   by (simp add: word_bits_conv)
 
 lemmas unat_power_lower32' = unat_power_lower[where 'a=32]
 lemmas unat_power_lower32 [simp] = unat_power_lower32'[unfolded word_bits_len_of]
 
 lemmas word32_less_sub_le' = word_less_sub_le[where 'a = 32]
 lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def]
 
 lemma word_bits_size:
   "size (w::word32) = word_bits"
   by (simp add: word_bits_def word_size)
 
 lemmas word32_power_less_1' = word_power_less_1[where 'a = 32]
 lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def]
 
 lemma of_nat32_0:
   "\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
   by (erule of_nat_0, simp add: word_bits_def)
 
 lemma unat_mask_2_less_4:
   "unat (p && mask 2 :: word32) < 4"
   apply (rule unat_less_helper)
   apply (rule order_le_less_trans, rule word_and_le1)
   apply (simp add: mask_eq)
   done
 
 lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32]
 lemmas unat_of_nat32 = unat_of_nat32'[unfolded word_bits_len_of]
 
 lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def]
 
 lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 32, unfolded word_bits_len_of]]
 
 lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def]
 
 lemma n_less_word_bits:
   "(n < word_bits) = (n < 32)"
   by (simp add: word_bits_def)
 
 lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def]
 
 lemma lt_word_bits_lt_pow:
   "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
   by (simp add: word_bits_conv)
 
 lemma unat_less_word_bits:
   fixes y :: word32
   shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
   unfolding word_bits_def
   by (rule order_less_trans [OF _ unat_lt2p])
 
 lemmas unat_mask_word32' = unat_mask[where 'a=32]
 lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def]
 
 lemma unat_less_2p_word_bits:
   "unat (x :: 32 word) < 2 ^ word_bits"
   apply (simp only: word_bits_def)
   apply (rule unat_lt2p)
   done
 
 lemma Suc_unat_mask_div:
   "Suc (unat (mask sz div word_size::word32)) = 2 ^ (min sz word_bits - 2)"
   apply (case_tac "sz < word_bits")
    apply (case_tac "2\<le>sz")
     apply (clarsimp simp: word_size_def word_bits_def min_def mask_eq)
     apply (drule (2) Suc_div_unat_helper
            [where 'a=32 and sz=sz and us=2, simplified, symmetric])
    apply (simp add: not_le word_size_def word_bits_def)
    apply (case_tac sz, simp add: unat_word_ariths)
    apply (case_tac nat, simp add: unat_word_ariths
                                   unat_mask_word32 min_def word_bits_def)
    apply simp
   apply (simp add: unat_word_ariths
                    unat_mask_word32 min_def word_bits_def word_size_def)
   done
 
 lemmas word32_minus_one_le' = word_minus_one_le[where 'a=32]
 lemmas word32_minus_one_le = word32_minus_one_le'[simplified]
 
 lemma ucast_not_helper:
   fixes a::word8
   assumes a: "a \<noteq> 0xFF"
   shows "ucast a \<noteq> (0xFF::word32)"
 proof
   assume "ucast a = (0xFF::word32)"
   also
   have "(0xFF::word32) = ucast (0xFF::word8)" by simp
   finally
   show False using a
     apply -
     apply (drule up_ucast_inj, simp)
     apply simp
     done
 qed
 
 lemma less_4_cases:
   "(x::word32) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
   apply clarsimp
   apply (drule word_less_cases, erule disjE, simp, simp)+
   done
 
 lemma unat_ucast_8_32:
   fixes x :: "word8"
   shows "unat (ucast x :: word32) = unat x"
   by transfer simp
 
 lemma if_then_1_else_0:
   "((if P then 1 else 0) = (0 :: word32)) = (\<not> P)"
   by simp
 
 lemma if_then_0_else_1:
   "((if P then 0 else 1) = (0 :: word32)) = (P)"
   by simp
 
 lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
 
 lemma ucast_le_ucast_8_32:
   "(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: word8))"
   by (simp add: ucast_le_ucast)
 
 lemma in_16_range:
   "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word32)) ` S"
   "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word32. r + x * 16) ` S"
   by (clarsimp simp: image_def elim!: bexI[rotated])+
 
 lemma eq_2_32_0:
   "(2 ^ 32 :: word32) = 0"
   by simp
 
 lemma x_less_2_0_1:
   fixes x :: word32 shows
   "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
   by (rule x_less_2_0_1') auto
 
 lemmas mask_32_max_word  = max_word_mask [symmetric, where 'a=32, simplified]
 
 lemma of_nat32_n_less_equal_power_2:
  "n < 32 \<Longrightarrow> ((of_nat n)::32 word) < 2 ^ n"
   by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)
 
 lemma word_rsplit_0:
   "word_rsplit (0 :: word32) = [0, 0, 0, 0 :: word8]"
   by (simp add: word_rsplit_def bin_rsplit_def)
 
 lemma unat_ucast_10_32 :
   fixes x :: "10 word"
   shows "unat (ucast x :: word32) = unat x"
   by transfer simp
 
 lemma bool_mask [simp]:
   fixes x :: word32
   shows "(0 < x && 1) = (x && 1 = 1)"
   by (rule bool_mask') auto
 
 lemma word32_bounds:
   "- (2 ^ (size (x :: word32) - 1)) = (-2147483648 :: int)"
   "((2 ^ (size (x :: word32) - 1)) - 1) = (2147483647 :: int)"
   "- (2 ^ (size (y :: 32 signed word) - 1)) = (-2147483648 :: int)"
   "((2 ^ (size (y :: 32 signed word) - 1)) - 1) = (2147483647 :: int)"
   by (simp_all add: word_size)
 
 lemma word_ge_min:"sint (x::32 word) \<ge> -2147483648"
   by (metis sint_ge word32_bounds(1) word_size)
 
 lemmas signed_arith_ineq_checks_to_eq_word32'
     = signed_arith_ineq_checks_to_eq[where 'a=32]
       signed_arith_ineq_checks_to_eq[where 'a="32 signed"]
 
 lemmas signed_arith_ineq_checks_to_eq_word32
     = signed_arith_ineq_checks_to_eq_word32' [unfolded word32_bounds]
 
 lemmas signed_mult_eq_checks32_to_64'
     = signed_mult_eq_checks_double_size[where 'a=32 and 'b=64]
       signed_mult_eq_checks_double_size[where 'a="32 signed" and 'b=64]
 
 lemmas signed_mult_eq_checks32_to_64 = signed_mult_eq_checks32_to_64'[simplified]
 
 lemmas sdiv_word32_max' = sdiv_word_max [where 'a=32] sdiv_word_max [where 'a="32 signed"]
 lemmas sdiv_word32_max = sdiv_word32_max'[simplified word_size, simplified]
 
 lemmas sdiv_word32_min' = sdiv_word_min [where 'a=32] sdiv_word_min [where 'a="32 signed"]
 lemmas sdiv_word32_min = sdiv_word32_min' [simplified word_size, simplified]
 
 lemmas sint32_of_int_eq' = sint_of_int_eq [where 'a=32]
 lemmas sint32_of_int_eq = sint32_of_int_eq' [simplified]
 
 lemma ucast_of_nats [simp]:
   "(ucast (of_nat x :: word32) :: sword32) = (of_nat x)"
   "(ucast (of_nat x :: word32) :: sword16) = (of_nat x)"
   "(ucast (of_nat x :: word32) :: sword8) = (of_nat x)"
   "(ucast (of_nat x :: word16) :: sword16) = (of_nat x)"
   "(ucast (of_nat x :: word16) :: sword8) = (of_nat x)"
   "(ucast (of_nat x :: word8) :: sword8) = (of_nat x)"
-       apply (simp_all add: of_nat_take_bit)
-       apply (transfer, simp)
-      apply (transfer, simp)
-     apply (transfer, simp)
-    apply (transfer, simp)
-   apply (transfer, simp)
-  apply (transfer, simp)
-  done
+  by (simp_all add: of_nat_take_bit take_bit_word_eq_self)
 
 lemmas signed_shift_guard_simpler_32'
     = power_strict_increasing_iff[where b="2 :: nat" and y=31]
 lemmas signed_shift_guard_simpler_32 = signed_shift_guard_simpler_32'[simplified]
 
 lemma word32_31_less:
   "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)"
   "31 < len_of TYPE (32)" "31 > (0 :: nat)"
   by auto
 
 lemmas signed_shift_guard_to_word_32
     = signed_shift_guard_to_word[OF word32_31_less(1-2)]
     signed_shift_guard_to_word[OF word32_31_less(3-4)]
 
 lemma le_step_down_word_3:
   fixes x :: "32 word"
   shows "\<lbrakk>x \<le>  y; x \<noteq> y; y < 2 ^ 32 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1"
   by (rule le_step_down_word_2, assumption+)
 
 lemma shiftr_1:
   "(x::word32) >> 1 = 0 \<Longrightarrow> x < 2"
   by word_bitwise clarsimp
 
 lemma has_zero_byte:
   "~~ (((((v::word32) && 0x7f7f7f7f) + 0x7f7f7f7f) || v) || 0x7f7f7f7f) \<noteq> 0
     \<Longrightarrow> v && 0xff000000 = 0 \<or> v && 0xff0000 = 0 \<or> v && 0xff00 = 0 \<or> v && 0xff = 0"
   apply clarsimp
   apply word_bitwise
   by metis
 
 lemma mask_step_down_32:
   \<open>\<exists>x. mask x = b\<close> if \<open>b && 1 = 1\<close>
     and \<open>\<exists>x. x < 32 \<and> mask x = b >> 1\<close> for b :: \<open>32word\<close>
 proof -
   from \<open>b && 1 = 1\<close> have \<open>odd b\<close>
     by (auto simp add: mod_2_eq_odd and_one_eq)
   then have \<open>b mod 2 = 1\<close>
     using odd_iff_mod_2_eq_one by blast
   from \<open>\<exists>x. x < 32 \<and> mask x = b >> 1\<close> obtain x where \<open>x < 32\<close> \<open>mask x = b >> 1\<close> by blast
   then have \<open>mask x = b div 2\<close>
     using shiftr1_is_div_2 [of b] by simp
   with \<open>b mod 2 = 1\<close> have \<open>2 * mask x + 1 = 2 * (b div 2) + b mod 2\<close>
     by (simp only:) 
   also have \<open>\<dots> = b\<close>
     by (simp add: mult_div_mod_eq)
   finally have \<open>2 * mask x + 1 = b\<close> .
   moreover have \<open>mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\<close>
     by (simp add: mask_Suc_rec)
   ultimately show ?thesis
     by auto
 qed
 
 lemma unat_of_int_32:
   "\<lbrakk>i \<ge> 0; i \<le>2 ^ 31\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword32)) = nat i"
   unfolding unat_eq_nat_uint
   apply (subst eq_nat_nat_iff)
     apply (auto simp add: take_bit_int_eq_self)
   done
 
 lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified]
 
 (* Helper for packing then unpacking a 64-bit variable. *)
 lemma cast_chunk_assemble_id_64[simp]:
   "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x"
   by (simp add:cast_chunk_assemble_id)
 
 (* Another variant of packing and unpacking a 64-bit variable. *)
 lemma cast_chunk_assemble_id_64'[simp]:
   "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x"
   by (simp add:cast_chunk_scast_assemble_id)
 
 (* Specialisations of down_cast_same for adding to local simpsets. *)
 lemma cast_down_u64: "(scast::64 word \<Rightarrow> 32 word) = (ucast::64 word \<Rightarrow> 32 word)"
   apply (subst down_cast_same[symmetric])
    apply (simp add:is_down)+
   done
 
 lemma cast_down_s64: "(scast::64 sword \<Rightarrow> 32 word) = (ucast::64 sword \<Rightarrow> 32 word)"
   apply (subst down_cast_same[symmetric])
    apply (simp add:is_down)+
   done
 
 end
diff --git a/thys/Word_Lib/Word_Lemmas_64.thy b/thys/Word_Lib/Word_Lemmas_64.thy
--- a/thys/Word_Lib/Word_Lemmas_64.thy
+++ b/thys/Word_Lib/Word_Lemmas_64.thy
@@ -1,301 +1,294 @@
 (*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section "Lemmas for Word Length 64"
 
 theory Word_Lemmas_64
 imports
   Word_Lemmas
   Word_Setup_64
 begin
 
 lemma ucast_8_64_inj:
   "inj (ucast ::  8 word \<Rightarrow> 64 word)"
   by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)
 
 lemma upto_2_helper:
   "{0..<2 :: 64 word} = {0, 1}"
   by (safe; simp) unat_arith
 
 lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def]
 lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def]
 lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def]
 
 lemma word_bits_len_of:
   "len_of TYPE (64) = word_bits"
   by (simp add: word_bits_conv)
 
 lemmas unat_power_lower64' = unat_power_lower[where 'a=64]
 lemmas unat_power_lower64 [simp] = unat_power_lower64'[unfolded word_bits_len_of]
 
 lemmas word64_less_sub_le' = word_less_sub_le[where 'a = 64]
 lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def]
 
 lemma word_bits_size:
   "size (w::word64) = word_bits"
   by (simp add: word_bits_def word_size)
 
 lemmas word64_power_less_1' = word_power_less_1[where 'a = 64]
 lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def]
 
 lemma of_nat64_0:
   "\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
   by (erule of_nat_0, simp add: word_bits_def)
 
 lemma unat_mask_2_less_4:
   "unat (p && mask 2 :: word64) < 4"
   apply (rule unat_less_helper)
   apply (rule order_le_less_trans, rule word_and_le1)
   apply (simp add: mask_eq)
   done
 
 lemmas unat_of_nat64' = unat_of_nat_eq[where 'a=64]
 lemmas unat_of_nat64 = unat_of_nat64'[unfolded word_bits_len_of]
 
 lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def]
 
 lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 64, unfolded word_bits_len_of]]
 
 lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def]
 
 lemma n_less_word_bits:
   "(n < word_bits) = (n < 64)"
   by (simp add: word_bits_def)
 
 lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, folded word_bits_def]
 
 lemma lt_word_bits_lt_pow:
   "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
   by (simp add: word_bits_conv)
 
 lemma unat_less_word_bits:
   fixes y :: word64
   shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
   unfolding word_bits_def
   by (rule order_less_trans [OF _ unat_lt2p])
 
 lemmas unat_mask_word64' = unat_mask[where 'a=64]
 lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
 
 lemma unat_less_2p_word_bits:
   "unat (x :: 64 word) < 2 ^ word_bits"
   apply (simp only: word_bits_def)
   apply (rule unat_lt2p)
   done
 
 lemma Suc_unat_mask_div:
   "Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)"
   apply (case_tac "sz < word_bits")
    apply (case_tac "3\<le>sz")
     apply (clarsimp simp: word_size_def word_bits_def min_def mask_eq)
     apply (drule (2) Suc_div_unat_helper
            [where 'a=64 and sz=sz and us=3, simplified, symmetric])
    apply (simp add: not_le word_size_def word_bits_def)
    apply (case_tac sz, simp add: unat_word_ariths)
    apply (case_tac nat, simp add: unat_word_ariths
                                   unat_mask_word64 min_def word_bits_def)
    apply (case_tac nata, simp add: unat_word_ariths unat_mask_word64 word_bits_def)
    apply simp
   apply (simp add: unat_word_ariths
                    unat_mask_word64 min_def word_bits_def word_size_def)
   done
 
 lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64]
 lemmas word64_minus_one_le = word64_minus_one_le'[simplified]
 
 lemma ucast_not_helper:
   fixes a::word8
   assumes a: "a \<noteq> 0xFF"
   shows "ucast a \<noteq> (0xFF::word64)"
 proof
   assume "ucast a = (0xFF::word64)"
   also
   have "(0xFF::word64) = ucast (0xFF::word8)" by simp
   finally
   show False using a
     apply -
     apply (drule up_ucast_inj, simp)
     apply simp
     done
 qed
 
 lemma less_4_cases:
   "(x::word64) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
   apply clarsimp
   apply (drule word_less_cases, erule disjE, simp, simp)+
   done
 
 lemma if_then_1_else_0:
   "((if P then 1 else 0) = (0 :: word64)) = (\<not> P)"
   by simp
 
 lemma if_then_0_else_1:
   "((if P then 0 else 1) = (0 :: word64)) = (P)"
   by simp
 
 lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
 
 lemma ucast_le_ucast_8_64:
   "(ucast x \<le> (ucast y :: word64)) = (x \<le> (y :: word8))"
   by (simp add: ucast_le_ucast)
 
 lemma in_16_range:
   "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word64)) ` S"
   "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word64. r + x * 16) ` S"
   by (clarsimp simp: image_def elim!: bexI[rotated])+
 
 lemma eq_2_64_0:
   "(2 ^ 64 :: word64) = 0"
   by simp
 
 lemma x_less_2_0_1:
   fixes x :: word64 shows
   "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
   by (rule x_less_2_0_1') auto
 
 lemmas mask_64_max_word  = max_word_mask [symmetric, where 'a=64, simplified]
 
 lemma of_nat64_n_less_equal_power_2:
  "n < 64 \<Longrightarrow> ((of_nat n)::64 word) < 2 ^ n"
   by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)
 
 lemma word_rsplit_0:
   "word_rsplit (0 :: word64) = [0, 0, 0, 0, 0, 0, 0, 0 :: word8]"
   by (simp add: word_rsplit_def bin_rsplit_def)
 
 lemma unat_ucast_10_64 :
   fixes x :: "10 word"
   shows "unat (ucast x :: word64) = unat x"
   by transfer simp
 
 lemma bool_mask [simp]:
   fixes x :: word64
   shows "(0 < x && 1) = (x && 1 = 1)"
   by (rule bool_mask') auto
 
 lemma word64_bounds:
   "- (2 ^ (size (x :: word64) - 1)) = (-9223372036854775808 :: int)"
   "((2 ^ (size (x :: word64) - 1)) - 1) = (9223372036854775807 :: int)"
   "- (2 ^ (size (y :: 64 signed word) - 1)) = (-9223372036854775808 :: int)"
   "((2 ^ (size (y :: 64 signed word) - 1)) - 1) = (9223372036854775807 :: int)"
   by (simp_all add: word_size)
 
 lemma word_ge_min:"sint (x::64 word) \<ge> -9223372036854775808"
   by (metis sint_ge word64_bounds(1) word_size)
 
 lemmas signed_arith_ineq_checks_to_eq_word64'
     = signed_arith_ineq_checks_to_eq[where 'a=64]
       signed_arith_ineq_checks_to_eq[where 'a="64 signed"]
 
 lemmas signed_arith_ineq_checks_to_eq_word64
     = signed_arith_ineq_checks_to_eq_word64' [unfolded word64_bounds]
 
 lemmas signed_mult_eq_checks64_to_64'
     = signed_mult_eq_checks_double_size[where 'a=64 and 'b=64]
       signed_mult_eq_checks_double_size[where 'a="64 signed" and 'b=64]
 
 lemmas signed_mult_eq_checks64_to_64 = signed_mult_eq_checks64_to_64'[simplified]
 
 lemmas sdiv_word64_max' = sdiv_word_max [where 'a=64] sdiv_word_max [where 'a="64 signed"]
 lemmas sdiv_word64_max = sdiv_word64_max'[simplified word_size, simplified]
 
 lemmas sdiv_word64_min' = sdiv_word_min [where 'a=64] sdiv_word_min [where 'a="64 signed"]
 lemmas sdiv_word64_min = sdiv_word64_min' [simplified word_size, simplified]
 
 lemmas sint64_of_int_eq' = sint_of_int_eq [where 'a=64]
 lemmas sint64_of_int_eq = sint64_of_int_eq' [simplified]
 
 lemma ucast_of_nats [simp]:
   "(ucast (of_nat x :: word64) :: sword64) = (of_nat x)"
   "(ucast (of_nat x :: word64) :: sword16) = (of_nat x)"
   "(ucast (of_nat x :: word64) :: sword8) = (of_nat x)"
   "(ucast (of_nat x :: word16) :: sword16) = (of_nat x)"
   "(ucast (of_nat x :: word16) :: sword8) = (of_nat x)"
   "(ucast (of_nat x :: word8) :: sword8) = (of_nat x)"
-       apply (simp_all add: of_nat_take_bit)
-       apply (transfer, simp)
-      apply (transfer, simp)
-     apply (transfer, simp)
-    apply (transfer, simp)
-   apply (transfer, simp)
-  apply (transfer, simp)
-  done
+  by (simp_all add: of_nat_take_bit take_bit_word_eq_self)
 
 lemmas signed_shift_guard_simpler_64'
     = power_strict_increasing_iff[where b="2 :: nat" and y=31]
 lemmas signed_shift_guard_simpler_64 = signed_shift_guard_simpler_64'[simplified]
 
 lemma word64_31_less:
   "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)"
   "31 < len_of TYPE (64)" "31 > (0 :: nat)"
   by auto
 
 lemmas signed_shift_guard_to_word_64
     = signed_shift_guard_to_word[OF word64_31_less(1-2)]
     signed_shift_guard_to_word[OF word64_31_less(3-4)]
 
 lemma le_step_down_word_3:
   fixes x :: "64 word"
   shows "\<lbrakk>x \<le>  y; x \<noteq> y; y < 2 ^ 64 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1"
   by (rule le_step_down_word_2, assumption+)
 
 lemma shiftr_1:
   "(x::word64) >> 1 = 0 \<Longrightarrow> x < 2"
   by word_bitwise clarsimp
 
 lemma mask_step_down_64:
   \<open>\<exists>x. mask x = b\<close> if \<open>b && 1 = 1\<close>
     and \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> for b :: \<open>64word\<close>
 proof -
   from \<open>b && 1 = 1\<close> have \<open>odd b\<close>
     by (auto simp add: mod_2_eq_odd and_one_eq)
   then have \<open>b mod 2 = 1\<close>
     using odd_iff_mod_2_eq_one by blast
   from \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> obtain x where \<open>x < 64\<close> \<open>mask x = b >> 1\<close> by blast
   then have \<open>mask x = b div 2\<close>
     using shiftr1_is_div_2 [of b] by simp
   with \<open>b mod 2 = 1\<close> have \<open>2 * mask x + 1 = 2 * (b div 2) + b mod 2\<close>
     by (simp only:) 
   also have \<open>\<dots> = b\<close>
     by (simp add: mult_div_mod_eq)
   finally have \<open>2 * mask x + 1 = b\<close> .
   moreover have \<open>mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\<close>
     by (simp add: mask_Suc_rec)
   ultimately show ?thesis
     by auto
 qed
 
 lemma unat_of_int_64:
   "\<lbrakk>i \<ge> 0; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i"
   unfolding unat_eq_nat_uint
   apply (subst eq_nat_nat_iff)
   apply (simp_all add: take_bit_int_eq_self)
   done
 
 lemmas word_ctz_not_minus_1_64 = word_ctz_not_minus_1[where 'a=64, simplified]
 
 (* Helper for packing then unpacking a 64-bit variable. *)
 lemma cast_chunk_assemble_id_64[simp]:
   "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x"
   by (simp add:cast_chunk_assemble_id)
 
 (* Another variant of packing and unpacking a 64-bit variable. *)
 lemma cast_chunk_assemble_id_64'[simp]:
   "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x"
   by (simp add:cast_chunk_scast_assemble_id)
 
 (* Specialisations of down_cast_same for adding to local simpsets. *)
 lemma cast_down_u64: "(scast::64 word \<Rightarrow> 32 word) = (ucast::64 word \<Rightarrow> 32 word)"
   apply (subst down_cast_same[symmetric])
    apply (simp add:is_down)+
   done
 
 lemma cast_down_s64: "(scast::64 sword \<Rightarrow> 32 word) = (ucast::64 sword \<Rightarrow> 32 word)"
   apply (subst down_cast_same[symmetric])
    apply (simp add:is_down)+
   done
 
 end
diff --git a/thys/Word_Lib/Word_Lib.thy b/thys/Word_Lib/Word_Lib.thy
--- a/thys/Word_Lib/Word_Lib.thy
+++ b/thys/Word_Lib/Word_Lib.thy
@@ -1,716 +1,731 @@
 (*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section "Additional Word Operations"
 
 theory Word_Lib
 imports
   "HOL-Word.Misc_set_bit" Word_Syntax
 begin
 
 definition
   ptr_add :: "'a :: len word \<Rightarrow> nat \<Rightarrow> 'a word" where
   "ptr_add ptr n \<equiv> ptr + of_nat n"
 
 definition
   complement :: "'a :: len word \<Rightarrow> 'a word"  where
  "complement x \<equiv> ~~ x"
 
 definition
   alignUp :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" where
  "alignUp x n \<equiv> x + 2 ^ n - 1 && complement (2 ^ n - 1)"
 
 (* standard notation for blocks of 2^n-1 words, usually aligned;
    abbreviation so it simplifies directly *)
 abbreviation mask_range :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word set" where
   "mask_range p n \<equiv> {p .. p + mask n}"
 
 (* Haskellish names/syntax *)
 notation (input)
   test_bit ("testBit")
 
 definition
   w2byte :: "'a :: len word \<Rightarrow> 8 word" where
   "w2byte \<equiv> ucast"
 
 
 (*
  * Signed division: when the result of a division is negative,
  * we will round towards zero instead of towards minus infinity.
  *)
 class signed_div =
   fixes sdiv :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "sdiv" 70)
   fixes smod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "smod" 70)
 
 instantiation int :: signed_div
 begin
 definition "(a :: int) sdiv b \<equiv> sgn (a * b) * (abs a div abs b)"
 definition "(a :: int) smod b \<equiv> a - (a sdiv b) * b"
 instance ..
 end
 
 instantiation word :: (len) signed_div
 begin
 definition "(a :: ('a::len) word) sdiv b = word_of_int (sint a sdiv sint b)"
 definition "(a :: ('a::len) word) smod b = word_of_int (sint a smod sint b)"
 instance ..
 end
 
 (* Tests *)
 lemma
   "( 4 :: word32) sdiv  4 =  1"
   "(-4 :: word32) sdiv  4 = -1"
   "(-3 :: word32) sdiv  4 =  0"
   "( 3 :: word32) sdiv -4 =  0"
   "(-3 :: word32) sdiv -4 =  0"
   "(-5 :: word32) sdiv -4 =  1"
   "( 5 :: word32) sdiv -4 = -1"
   by (simp_all add: sdiv_word_def sdiv_int_def)
 
 lemma
   "( 4 :: word32) smod  4 =   0"
   "( 3 :: word32) smod  4 =   3"
   "(-3 :: word32) smod  4 =  -3"
   "( 3 :: word32) smod -4 =   3"
   "(-3 :: word32) smod -4 =  -3"
   "(-5 :: word32) smod -4 =  -1"
   "( 5 :: word32) smod -4 =   1"
   by (simp_all add: smod_word_def smod_int_def sdiv_int_def)
 
 
 (* Count leading zeros  *)
 definition
   word_clz :: "'a::len word \<Rightarrow> nat"
 where
   "word_clz w \<equiv> length (takeWhile Not (to_bl w))"
 
 (* Count trailing zeros  *)
 definition
   word_ctz :: "'a::len word \<Rightarrow> nat"
 where
   "word_ctz w \<equiv> length (takeWhile Not (rev (to_bl w)))"
 
 definition
   word_log2 :: "'a::len word \<Rightarrow> nat"
 where
   "word_log2 (w::'a::len word) \<equiv> size w - 1 - word_clz w"
 
 
 (* Bit population count. Equivalent of __builtin_popcount. *)
 definition
   pop_count :: "('a::len) word \<Rightarrow> nat"
 where
   "pop_count w \<equiv> length (filter id (to_bl w))"
 
 
 (* Sign extension from bit n *)
 
 definition
   sign_extend :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 'a word"
 where
   "sign_extend n w \<equiv> if w !! n then w || ~~ (mask n) else w && mask n"
 
+lemma sign_extend_eq_signed_take_bit:
+  \<open>sign_extend = signed_take_bit\<close>
+proof (rule ext)+
+  fix n and w :: \<open>'a::len word\<close>
+  show \<open>sign_extend n w = signed_take_bit n w\<close>
+  proof (rule bit_word_eqI)
+    fix q
+    assume \<open>q < LENGTH('a)\<close>
+    then show \<open>bit (sign_extend n w) q \<longleftrightarrow> bit (signed_take_bit n w) q\<close>
+      by (auto simp add: test_bit_eq_bit bit_signed_take_bit_iff
+        sign_extend_def bit_and_iff bit_or_iff bit_not_iff bit_mask_iff not_less
+        exp_eq_0_imp_not_bit not_le min_def)
+  qed
+qed
+
 definition
   sign_extended :: "nat \<Rightarrow> 'a::len word \<Rightarrow> bool"
 where
   "sign_extended n w \<equiv> \<forall>i. n < i \<longrightarrow> i < size w \<longrightarrow> w !! i = w !! n"
 
 
 lemma ptr_add_0 [simp]:
   "ptr_add ref 0 = ref "
   unfolding ptr_add_def by simp
 
 lemma shiftl_power:
   "(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y"
   apply (induct x)
    apply simp
   apply (simp add: shiftl1_2t)
   done
 
 lemmas of_bl_reasoning = to_bl_use_of_bl of_bl_append
 
 lemma uint_of_bl_is_bl_to_bin_drop:
   "length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> uint (of_bl l :: 'a::len word) = bl_to_bin l"
   apply transfer
   apply (simp add: take_bit_eq_mod)
   apply (rule Divides.mod_less)
    apply (rule bl_to_bin_ge0)
   using bl_to_bin_lt2p_drop apply (rule order.strict_trans2)
   apply simp
   done
 
 corollary uint_of_bl_is_bl_to_bin:
   "length l\<le>LENGTH('a) \<Longrightarrow> uint ((of_bl::bool list\<Rightarrow> ('a :: len) word) l) = bl_to_bin l"
   apply(rule uint_of_bl_is_bl_to_bin_drop)
   using le_trans length_dropWhile_le by blast
 
 lemma bin_to_bl_or:
   "bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)"
   using bl_or_aux_bin[where n=n and v=a and w=b and bs="[]" and cs="[]"]
   by simp
 
 lemma word_ops_nth [simp]:
   shows
   word_or_nth:  "(x || y) !! n = (x !! n \<or> y !! n)" and
   word_and_nth: "(x && y) !! n = (x !! n \<and> y !! n)" and
   word_xor_nth: "(x xor y) !! n = (x !! n \<noteq> y !! n)"
   by ((cases "n < size x",
       auto dest: test_bit_size simp: word_ops_nth_size word_size)[1])+
 
 (* simp del to avoid warning on the simp add in iff *)
 declare test_bit_1 [simp del, iff]
 
 (* test: *)
 lemma "1 < (1024::32 word) \<and> 1 \<le> (1024::32 word)" by simp
 
 lemma and_not_mask:
   "w AND NOT (mask n) = (w >> n) << n"
   for w :: \<open>'a::len word\<close>
   apply (rule word_eqI)
   apply (simp add : word_ops_nth_size word_size)
   apply (simp add : nth_shiftr nth_shiftl)
   by auto
 
 lemma and_mask:
   "w AND mask n = (w << (size w - n)) >> (size w - n)"
   for w :: \<open>'a::len word\<close>
   apply (rule word_eqI)
   apply (simp add : word_ops_nth_size word_size)
   apply (simp add : nth_shiftr nth_shiftl)
   by auto
 
 lemma AND_twice [simp]:
   "(w && m) && m = w && m"
   by (simp add: word_eqI)
 
 lemma word_combine_masks:
   "w && m = z \<Longrightarrow> w && m' = z' \<Longrightarrow> w && (m || m') = (z || z')"
   by (auto simp: word_eq_iff)
 
 lemma nth_w2p_same:
   "(2^n :: 'a :: len word) !! n = (n < LENGTH('a))"
   by (simp add : nth_w2p)
 
 lemma p2_gt_0:
   "(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))"
   apply (simp add : word_gt_0)
   apply safe
    apply (erule swap)
    apply (rule word_eqI)
    apply (simp add : nth_w2p)
   apply (drule word_eqD)
   apply simp
   apply (erule notE)
   apply (erule nth_w2p_same [THEN iffD2])
   done
 
 lemmas uint_2p_alt = uint_2p [unfolded p2_gt_0]
 
 lemma shiftr_div_2n_w: "n < size w \<Longrightarrow> w >> n = w div (2^n :: 'a :: len word)"
   apply (unfold word_div_def)
   apply (simp add : uint_2p_alt word_size)
   apply (rule word_uint.Rep_inverse' [THEN sym])
   apply (rule shiftr_div_2n)
   done
 
 lemmas less_def = less_eq [symmetric]
 lemmas le_def = not_less [symmetric, where ?'a = nat]
 
 lemmas p2_eq_0 [simp] = trans [OF eq_commute
   iffD2 [OF Not_eq_iff p2_gt_0, folded le_def, unfolded word_gt_0 not_not]]
 
 lemma neg_mask_is_div':
   "n < size w \<Longrightarrow> w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))"
   for w :: \<open>'a::len word\<close>
   by (simp add : and_not_mask shiftr_div_2n_w shiftl_t2n word_size)
 
 lemma neg_mask_is_div:
   "w AND NOT (mask n) = (w div 2^n) * 2^n"
   for w :: \<open>'a::len word\<close>
   apply (cases "n < size w")
    apply (erule neg_mask_is_div')
   apply (simp add: word_size)
   apply (frule p2_gt_0 [THEN Not_eq_iff [THEN iffD2], THEN iffD2])
   apply (simp add: word_gt_0  del: p2_eq_0)
   apply (rule word_eqI)
   apply (simp add: word_ops_nth_size word_size)
   done
 
 lemma and_mask_arith':
   "0 < n \<Longrightarrow> w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
   for w :: \<open>'a::len word\<close>
   by (simp add: and_mask shiftr_div_2n_w shiftl_t2n word_size mult.commute)
 
 lemmas p2len = iffD2 [OF p2_eq_0 order_refl]
 
 lemma and_mask_arith:
   "w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
   for w :: \<open>'a::len word\<close>
   apply (cases "0 < n")
    apply (auto elim!: and_mask_arith')
   apply (simp add: word_size)
   done
 
 lemma mask_2pm1: "mask n = 2 ^ n - (1 :: 'a::len word)"
   by (fact mask_eq_decr_exp)
 
 lemma add_mask_fold:
   "x + 2 ^ n - 1 = x + mask n"
   for x :: \<open>'a::len word\<close>
   by (simp add: mask_eq_decr_exp)
 
 lemma word_and_mask_le_2pm1: "w && mask n \<le> 2 ^ n - 1"
   by (simp add: mask_2pm1[symmetric] word_and_le1)
 
 lemma is_aligned_AND_less_0:
   "u && mask n = 0 \<Longrightarrow> v < 2^n \<Longrightarrow> u && v = 0"
   apply (drule less_mask_eq)
   apply (simp add: mask_2pm1)
   apply (rule word_eqI)
   apply (clarsimp simp add: word_size)
   apply (drule_tac x=na in word_eqD)
   apply (drule_tac x=na in word_eqD)
   apply simp
   done
 
 lemma le_shiftr1:
   "u <= v \<Longrightarrow> shiftr1 u <= shiftr1 v"
   apply (unfold word_le_def shiftr1_eq word_ubin.eq_norm)
   apply (unfold bin_rest_trunc_i
                 trans [OF bintrunc_bintrunc_l word_ubin.norm_Rep,
                           unfolded word_ubin.norm_Rep,
                        OF order_refl [THEN le_SucI]])
   apply (case_tac "uint u" rule: bin_exhaust)
   apply (rename_tac bs bit)
   apply (case_tac "uint v" rule: bin_exhaust)
   apply (rename_tac bs' bit')
   apply (case_tac "bit")
    apply (case_tac "bit'", auto simp: less_eq_int_code)[1]
   apply (case_tac bit')
     apply (simp add: less_eq_int_code)
   apply (simp add: less_eq_int_code)
   done
 
 lemma le_shiftr:
   "u \<le> v \<Longrightarrow> u >> (n :: nat) \<le> (v :: 'a :: len word) >> n"
   apply (unfold shiftr_def)
   apply (induct_tac "n")
    apply auto
   apply (erule le_shiftr1)
   done
 
 lemma shiftr_mask_le:
   "n <= m \<Longrightarrow> mask n >> m = (0 :: 'a::len word)"
   apply (rule word_eqI)
   apply (simp add: word_size nth_shiftr)
   done
 
 lemmas shiftr_mask = order_refl [THEN shiftr_mask_le, simp]
 
 lemma word_leI:
   "(\<And>n.  \<lbrakk>n < size (u::'a::len word); u !! n \<rbrakk> \<Longrightarrow> (v::'a::len word) !! n) \<Longrightarrow> u <= v"
   apply (rule xtr4)
    apply (rule word_and_le2)
   apply (rule word_eqI)
   apply (simp add: word_ao_nth)
   apply safe
     apply assumption
    apply (erule_tac [2] asm_rl)
   apply (unfold word_size)
   by auto
 
 lemma le_mask_iff:
   "(w \<le> mask n) = (w >> n = 0)"
   for w :: \<open>'a::len word\<close>
   apply safe
    apply (rule word_le_0_iff [THEN iffD1])
    apply (rule xtr3)
     apply (erule_tac [2] le_shiftr)
    apply simp
   apply (rule word_leI)
   apply (rename_tac n')
   apply (drule_tac x = "n' - n" in word_eqD)
   apply (simp add : nth_shiftr word_size)
   apply (case_tac "n <= n'")
   by auto
 
 lemma and_mask_eq_iff_shiftr_0:
   "(w AND mask n = w) = (w >> n = 0)"
   for w :: \<open>'a::len word\<close>
   apply (unfold test_bit_eq_iff [THEN sym])
   apply (rule iffI)
    apply (rule ext)
    apply (rule_tac [2] ext)
    apply (auto simp add : word_ao_nth nth_shiftr)
     apply (drule arg_cong)
     apply (drule iffD2)
      apply assumption
     apply (simp add : word_ao_nth)
    prefer 2
    apply (simp add : word_size test_bit_bin)
   apply (drule_tac f = "%u. u !! (x - n)" in arg_cong)
   apply (simp add : nth_shiftr)
   apply (case_tac "n <= x")
    apply auto
   done
 
 lemmas and_mask_eq_iff_le_mask = trans
   [OF and_mask_eq_iff_shiftr_0 le_mask_iff [THEN sym]]
 
 lemma mask_shiftl_decompose:
   "mask m << n = mask (m + n) && ~~ (mask n)"
   by (auto intro!: word_eqI simp: and_not_mask nth_shiftl nth_shiftr word_size)
 
 lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n"
   apply (rule word_eqI)
   apply (auto simp add: test_bit_set_gen nth_shiftl word_size
               simp del: word_set_bit_0 shiftl_1)
   done
 
 lemmas one_bit_pow = trans [OF one_bit_shiftl shiftl_1]
 
 lemmas bin_sc_minus_simps =
   bin_sc_simps (2,3,4) [THEN [2] trans, OF bin_sc_minus [THEN sym]]
 
 lemma NOT_eq:
   "NOT (x :: 'a :: len word) = - x - 1"
   apply (cut_tac x = "x" in word_add_not)
   apply (drule add.commute [THEN trans])
   apply (drule eq_diff_eq [THEN iffD2])
   by simp
 
 lemma NOT_mask: "NOT (mask n :: 'a::len word) = - (2 ^ n)"
   by (simp add : NOT_eq mask_2pm1)
 
 lemma le_m1_iff_lt: "(x > (0 :: 'a :: len word)) = ((y \<le> x - 1) = (y < x))"
   by uint_arith
 
 lemmas gt0_iff_gem1 = iffD1 [OF iffD1 [OF iff_left_commute le_m1_iff_lt] order_refl]
 
 lemmas power_2_ge_iff = trans [OF gt0_iff_gem1 [THEN sym] p2_gt_0]
 
 lemma le_mask_iff_lt_2n:
   "n < len_of TYPE ('a) = (((w :: 'a :: len word) \<le> mask n) = (w < 2 ^ n))"
   unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt])
 
 lemmas mask_lt_2pn =
   le_mask_iff_lt_2n [THEN iffD1, THEN iffD1, OF _ order_refl]
 
 lemma bang_eq:
   fixes x :: "'a::len word"
   shows "(x = y) = (\<forall>n. x !! n = y !! n)"
   by (subst test_bit_eq_iff[symmetric]) fastforce
 
 lemma word_unat_power:
   "(2 :: 'a :: len word) ^ n = of_nat (2 ^ n)"
   by simp
 
 lemma of_nat_mono_maybe:
   assumes xlt: "x < 2 ^ len_of TYPE ('a)"
   shows   "y < x \<Longrightarrow> of_nat y < (of_nat x :: 'a :: len word)"
   apply (subst word_less_nat_alt)
   apply (subst unat_of_nat)+
   apply (subst mod_less)
    apply (erule order_less_trans [OF _ xlt])
   apply (subst mod_less [OF xlt])
   apply assumption
   done
 
 lemma shiftl_over_and_dist:
   fixes a::"'a::len word"
   shows "(a AND b) << c = (a << c) AND (b << c)"
   apply(rule word_eqI)
   apply(simp add: word_ao_nth nth_shiftl, safe)
   done
 
 lemma shiftr_over_and_dist:
   fixes a::"'a::len word"
   shows "a AND b >> c = (a >> c) AND (b >> c)"
   apply(rule word_eqI)
   apply(simp add:nth_shiftr word_ao_nth)
   done
 
 lemma sshiftr_over_and_dist:
   fixes a::"'a::len word"
   shows "a AND b >>> c = (a >>> c) AND (b >>> c)"
   apply(rule word_eqI)
   apply(simp add:nth_sshiftr word_ao_nth word_size)
   done
 
 lemma shiftl_over_or_dist:
   fixes a::"'a::len word"
   shows "a OR b << c = (a << c) OR (b << c)"
   apply(rule word_eqI)
   apply(simp add:nth_shiftl word_ao_nth, safe)
   done
 
 lemma shiftr_over_or_dist:
   fixes a::"'a::len word"
   shows "a OR b >> c = (a >> c) OR (b >> c)"
   apply(rule word_eqI)
   apply(simp add:nth_shiftr word_ao_nth)
   done
 
 lemma sshiftr_over_or_dist:
   fixes a::"'a::len word"
   shows "a OR b >>> c = (a >>> c) OR (b >>> c)"
   apply(rule word_eqI)
   apply(simp add:nth_sshiftr word_ao_nth word_size)
   done
 
 lemmas shift_over_ao_dists =
   shiftl_over_or_dist shiftr_over_or_dist
   sshiftr_over_or_dist shiftl_over_and_dist
   shiftr_over_and_dist sshiftr_over_and_dist
 
 lemma shiftl_shiftl:
   fixes a::"'a::len word"
   shows "a << b << c = a << (b + c)"
   apply(rule word_eqI)
   apply(auto simp:word_size nth_shiftl add.commute add.left_commute)
   done
 
 lemma shiftr_shiftr:
   fixes a::"'a::len word"
   shows "a >> b >> c = a >> (b + c)"
   apply(rule word_eqI)
   apply(simp add:word_size nth_shiftr add.left_commute add.commute)
   done
 
 lemma shiftl_shiftr1:
   fixes a::"'a::len word"
   shows "c \<le> b \<Longrightarrow> a << b >> c = a AND (mask (size a - b)) << (b - c)"
   apply(rule word_eqI)
   apply(auto simp:nth_shiftr nth_shiftl word_size word_ao_nth)
   done
 
 lemma shiftl_shiftr2:
   fixes a::"'a::len word"
   shows "b < c \<Longrightarrow> a << b >> c = (a >> (c - b)) AND (mask (size a - c))"
   apply(rule word_eqI)
   apply(auto simp:nth_shiftr nth_shiftl word_size word_ao_nth)
   done
 
 lemma shiftr_shiftl1:
   fixes a::"'a::len word"
   shows "c \<le> b \<Longrightarrow> a >> b << c = (a >> (b - c)) AND (NOT (mask c))"
   apply(rule word_eqI)
   apply(auto simp:nth_shiftr nth_shiftl word_size word_ops_nth_size)
   done
 
 lemma shiftr_shiftl2:
   fixes a::"'a::len word"
   shows "b < c \<Longrightarrow> a >> b << c = (a << (c - b)) AND (NOT (mask c))"
   apply(rule word_eqI)
   apply(auto simp:nth_shiftr nth_shiftl word_size word_ops_nth_size)
   done
 
 lemmas multi_shift_simps =
   shiftl_shiftl shiftr_shiftr
   shiftl_shiftr1 shiftl_shiftr2
   shiftr_shiftl1 shiftr_shiftl2
 
 lemma word_and_max_word:
   fixes a::"'a::len word"
   shows "x = max_word \<Longrightarrow> a AND x = a"
   by simp
 
 lemma word_and_full_mask_simp:
   \<open>x && Bit_Operations.mask LENGTH('a) = x\<close> for x :: \<open>'a::len word\<close>
 proof (rule bit_eqI)
   fix n
   assume \<open>2 ^ n \<noteq> (0 :: 'a word)\<close>
   then have \<open>n < LENGTH('a)\<close>
     by simp
   then show \<open>bit (x && Bit_Operations.mask LENGTH('a)) n \<longleftrightarrow> bit x n\<close>
     by (simp add: bit_and_iff bit_mask_iff)
 qed
 	
 lemma word8_and_max_simp:
   \<open>x && 0xFF = x\<close> for x :: \<open>8 word\<close>
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 	
 lemma word16_and_max_simp:
   \<open>x && 0xFFFF = x\<close> for x :: \<open>16 word\<close>
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 	
 lemma word32_and_max_simp:
   \<open>x && 0xFFFFFFFF = x\<close> for x :: \<open>32 word\<close>
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 	
 lemma word64_and_max_simp:
   \<open>x && 0xFFFFFFFFFFFFFFFF = x\<close> for x :: \<open>64 word\<close>
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 	
 lemmas word_and_max_simps =
   word8_and_max_simp
   word16_and_max_simp
   word32_and_max_simp
   word64_and_max_simp
 
 lemma word_and_1_bl:
   fixes x::"'a::len word"
   shows "(x AND 1) = of_bl [x !! 0]"
   by (simp add: mod_2_eq_odd test_bit_word_eq and_one_eq)
 
 lemma word_1_and_bl:
   fixes x::"'a::len word"
   shows "(1 AND x) = of_bl [x !! 0]"
   by (simp add: mod_2_eq_odd test_bit_word_eq one_and_eq)
 
 lemma scast_scast_id [simp]:
   "scast (scast x :: ('a::len) signed word) = (x :: 'a word)"
   "scast (scast y :: ('a::len) word) = (y :: 'a signed word)"
   by (auto simp: is_up scast_up_scast_id)
 
 lemma scast_ucast_id [simp]:
     "scast (ucast (x :: 'a::len word) :: 'a signed word) = x"
   by (metis down_cast_same is_down len_signed order_refl scast_scast_id(1))
 
 lemma ucast_scast_id [simp]:
     "ucast (scast (x :: 'a::len signed word) :: 'a word) = x"
   by (metis scast_scast_id(2) scast_ucast_id)
 
 lemma scast_of_nat [simp]:
     "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)"
   by transfer simp
 
 lemma ucast_of_nat:
   "is_down (ucast :: 'a :: len word \<Rightarrow> 'b :: len word)
     \<Longrightarrow> ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)"
   by transfer simp
 
 (* shortcut for some specific lengths *)
 lemma word_fixed_sint_1[simp]:
   "sint (1::8 word) = 1"
   "sint (1::16 word) = 1"
   "sint (1::32 word) = 1"
   "sint (1::64 word) = 1"
   by (auto simp: sint_word_ariths)
 
 lemma word_sint_1 [simp]:
   "sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)"
   by (cases \<open>LENGTH('a)\<close>)
     (simp_all add: not_le sint_uint le_Suc_eq sbintrunc_minus_simps)
 
 lemma scast_1':
   "(scast (1::'a::len word) :: 'b::len word) =
    (word_of_int (sbintrunc (LENGTH('a::len) - Suc 0) (1::int)))"
   by transfer simp
 
 lemma scast_1:
   "(scast (1::'a::len word) :: 'b::len word) = (if LENGTH('a) = 1 then -1 else 1)"
   by (fact signed_1)
 
 lemma scast_eq_scast_id [simp]:
   "((scast (a :: 'a::len signed word) :: 'a word) = scast b) = (a = b)"
   by (metis ucast_scast_id)
 
 lemma ucast_eq_ucast_id [simp]:
   "((ucast (a :: 'a::len word) :: 'a signed word) = ucast b) = (a = b)"
   by (metis scast_ucast_id)
 
 lemma scast_ucast_norm [simp]:
   "(ucast (a :: 'a::len word) = (b :: 'a signed word)) = (a = scast b)"
   "((b :: 'a signed word) = ucast (a :: 'a::len word)) = (a = scast b)"
   by (metis scast_ucast_id ucast_scast_id)+
 
 lemma of_bl_drop:
   "of_bl (drop n xs) = (of_bl xs && mask (length xs - n))"
   apply (clarsimp simp: bang_eq test_bit_of_bl rev_nth cong: rev_conj_cong)
   apply (safe; simp add: word_size to_bl_nth)
   done
 
 lemma of_int_uint:
   "of_int (uint x) = x"
   by (fact word_of_int_uint)
 
 lemma shiftr_mask2:
   "n \<le> LENGTH('a) \<Longrightarrow> (mask n >> m :: ('a :: len) word) = mask (n - m)"
   apply (rule word_eqI)
   apply (simp add: nth_shiftr word_size)
   apply arith
   done
 
 corollary word_plus_and_or_coroll:
   "x && y = 0 \<Longrightarrow> x + y = x || y"
   using word_plus_and_or[where x=x and y=y]
   by simp
 
 corollary word_plus_and_or_coroll2:
   "(x && w) + (x && ~~ w) = x"
   apply (subst word_plus_and_or_coroll)
    apply (rule word_eqI, simp add: word_size word_ops_nth_size)
   apply (rule word_eqI, simp add: word_size word_ops_nth_size)
   apply blast
   done
 
 lemma less_le_mult_nat':
   "w * c < b * c ==> 0 \<le> c ==> Suc w * c \<le> b * (c::nat)"
   apply (rule mult_right_mono)
    apply (rule Suc_leI)
    apply (erule (1) mult_right_less_imp_less)
   apply assumption
   done
 
 lemmas less_le_mult_nat = less_le_mult_nat'[simplified distrib_right, simplified]
 
 (* FIXME: these should eventually be moved to HOL/Word. *)
 lemmas extra_sle_sless_unfolds [simp] =
     word_sle_eq[where a=0 and b=1]
     word_sle_eq[where a=0 and b="numeral n"]
     word_sle_eq[where a=1 and b=0]
     word_sle_eq[where a=1 and b="numeral n"]
     word_sle_eq[where a="numeral n" and b=0]
     word_sle_eq[where a="numeral n" and b=1]
     word_sless_alt[where a=0 and b=1]
     word_sless_alt[where a=0 and b="numeral n"]
     word_sless_alt[where a=1 and b=0]
     word_sless_alt[where a=1 and b="numeral n"]
     word_sless_alt[where a="numeral n" and b=0]
     word_sless_alt[where a="numeral n" and b=1]
   for n
 
 
 lemma to_bl_1:
   "to_bl (1::'a::len word) = replicate (LENGTH('a) - 1) False @ [True]"
   by (rule nth_equalityI) (auto simp add: to_bl_unfold nth_append rev_nth bit_1_iff not_less not_le)
 
 lemma list_of_false:
   "True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False"
   by (induct xs, simp_all)
 
 lemma eq_zero_set_bl:
   "(w = 0) = (True \<notin> set (to_bl w))"
   using list_of_false word_bl.Rep_inject by fastforce
 
 lemma diff_diff_less:
   "(i < m - (m - (n :: nat))) = (i < m \<and> i < n)"
   by auto
 
 lemma pop_count_0[simp]:
   "pop_count 0 = 0"
   by (clarsimp simp:pop_count_def)
 
 lemma pop_count_1[simp]:
   "pop_count 1 = 1"
   by (clarsimp simp:pop_count_def to_bl_1)
 
 lemma pop_count_0_imp_0:
   "(pop_count w = 0) = (w = 0)"
   apply (rule iffI)
    apply (clarsimp simp:pop_count_def)
    apply (subst (asm) filter_empty_conv)
    apply (clarsimp simp:eq_zero_set_bl)
    apply fast
   apply simp
   done
 
 end