Session Word_Lib

Theory More_Arithmetic

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Arithmetic lemmas›

theory More_Arithmetic
  imports Main "HOL-Library.Type_Length" "HOL-Library.Bit_Operations"
begin

declare iszero_0 [intro]

declare min.absorb1 [simp] min.absorb2 [simp]

lemma n_less_equal_power_2 [simp]:
  "n < 2 ^ n"
  by (fact less_exp)

lemma min_pm [simp]: "min a b + (a - b) = a"
  for a b :: nat
  by arith

lemma min_pm1 [simp]: "a - b + min a b = a"
  for a b :: nat
  by arith

lemma rev_min_pm [simp]: "min b a + (a - b) = a"
  for a b :: nat
  by arith

lemma rev_min_pm1 [simp]: "a - b + min b a = a"
  for a b :: nat
  by arith

lemma min_minus [simp]: "min m (m - k) = m - k"
  for m k :: nat
  by arith

lemma min_minus' [simp]: "min (m - k) m = m - k"
  for m k :: nat
  by arith

lemma nat_less_power_trans:
  fixes n :: nat
  assumes nv: "n < 2 ^ (m - k)"
  and     kv: "k  m"
  shows "2 ^ k * n < 2 ^ m"
proof (rule order_less_le_trans)
  show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)"
    by (rule mult_less_mono2 [OF nv zero_less_power]) simp
  show "(2::nat) ^ k * 2 ^ (m - k)  2 ^ m" using nv kv
    by (subst power_add [symmetric]) simp
qed

lemma nat_le_power_trans:
  fixes n :: nat
  shows "n  2 ^ (m - k); k  m  2 ^ k * n  2 ^ m"
  by (metis le_add_diff_inverse mult_le_mono2 semiring_normalization_rules(26))

lemma nat_add_offset_less:
  fixes x :: nat
  assumes yv: "y < 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y < 2 ^ sz"
proof (subst mn)
  from yv obtain qy where "y + qy = 2 ^ n" and "0 < qy"
    by (auto dest: less_imp_add_positive)

  have "x * 2 ^ n + y < x * 2 ^ n + 2 ^ n" by simp fact+
  also have " = (x + 1) * 2 ^ n" by simp
  also have "  2 ^ (m + n)" using xv
    by (subst power_add) (rule mult_le_mono1, simp)
  finally show "x * 2 ^ n + y < 2 ^ (m + n)" .
qed

lemma nat_power_less_diff:
  assumes lt: "(2::nat) ^ n * q < 2 ^ m"
  shows "q < 2 ^ (m - n)"
  using lt
proof (induct n arbitrary: m)
  case 0
  then show ?case by simp
next
  case (Suc n)

  have ih: "m. 2 ^ n * q < 2 ^ m  q < 2 ^ (m - n)"
    and prem: "2 ^ Suc n * q < 2 ^ m" by fact+

  show ?case
  proof (cases m)
    case 0
    then show ?thesis using Suc by simp
  next
    case (Suc m')
    then show ?thesis using prem
      by (simp add: ac_simps ih)
  qed
qed

lemma power_2_mult_step_le:
  "n'  n; 2 ^ n' * k' < 2 ^ n * k  2 ^ n' * (k' + 1)  2 ^ n * (k::nat)"
  apply (cases "n'=n", simp)
   apply (metis Suc_leI le_refl mult_Suc_right mult_le_mono semiring_normalization_rules(7))
  apply (drule (1) le_neq_trans)
  apply clarsimp
  apply (subgoal_tac "m. n = n' + m")
   prefer 2
   apply (simp add: le_Suc_ex)
  apply (clarsimp simp: power_add)
  apply (metis Suc_leI mult.assoc mult_Suc_right nat_mult_le_cancel_disj)
  done

lemma nat_mult_power_less_eq:
  "b > 0  (a * b ^ n < (b :: nat) ^ m) = (a < b ^ (m - n))"
  using mult_less_cancel2[where m = a and k = "b ^ n" and n="b ^ (m - n)"]
        mult_less_cancel2[where m="a * b ^ (n - m)" and k="b ^ m" and n=1]
  apply (simp only: power_add[symmetric] nat_minus_add_max)
  apply (simp only: power_add[symmetric] nat_minus_add_max ac_simps)
  apply (simp add: max_def split: if_split_asm)
  done

lemma diff_diff_less:
  "(i < m - (m - (n :: nat))) = (i < m  i < n)"
  by auto

lemma small_powers_of_2:
  x < 2 ^ (x - 1) if x  3 for x :: nat
proof -
  define m where m = x - 3
  with that have x = m + 3
    by simp
  moreover have m + 3 < 4 * 2 ^ m
    by (induction m) simp_all
  ultimately show ?thesis
    by simp
qed

end

Theory More_Divides

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Lemmas on division›

theory More_Divides
  imports
    "HOL-Library.Word"
begin

declare div_eq_dividend_iff [simp]

lemma int_div_same_is_1 [simp]:
  a div b = a  b = 1 if 0 < a 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]:
  a div b = - a  b = - 1 if 0 > a for a b :: int
  using that by (metis div_minus_right equation_minus_iff int_div_same_is_1 neg_0_less_iff_less)

lemma nat_div_eq_Suc_0_iff: "n div m = Suc 0  m  n  n < 2 * m"
  apply auto
  using div_greater_zero_iff apply fastforce
   apply (metis One_nat_def div_greater_zero_iff dividend_less_div_times mult.right_neutral mult_Suc mult_numeral_1 numeral_2_eq_2 zero_less_numeral)
  apply (simp add: div_nat_eqI)
  done

lemma diff_mod_le:
  a - a mod b  d - b if a < d b dvd d for a b d :: nat
  using that
  apply(subst minus_mod_eq_mult_div)
  apply(clarsimp simp: dvd_def)
  apply(cases b = 0)
   apply simp
  apply(subgoal_tac "a div b  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_times_less_eq_dividend)
   apply assumption
  apply clarsimp
  apply(subgoal_tac "b * (a div b)  b * (k - 1)")
   apply(erule le_trans)
   apply(simp add: diff_mult_distrib2)
  apply simp
  done

lemma one_mod_exp_eq_one [simp]:
  "1 mod (2 * 2 ^ n) = (1::int)"
  using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)

lemma int_mod_lem: "0 < n  0  b  b < n  b mod n = b"
  for b n :: int
  apply safe
    apply (erule (1) mod_pos_pos_trivial)
   apply (erule_tac [!] subst)
   apply auto
  done

lemma int_mod_ge': "b < 0  0 < n  b + n  b mod n"
  for b n :: int
  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)

lemma int_mod_le': "0  b - n  b mod n  b - n"
  for b n :: int
  by (metis minus_mod_self2 zmod_le_nonneg_dividend)

lemma emep1: "even n  even d  0  d  (n + 1) mod d = (n mod d) + 1"
  for n d :: int
  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)

lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
  by (rule zmod_minus1) simp

lemma sb_inc_lem: "a + 2^k < 0  a + 2^k + 2^(Suc k)  (a + 2^k) mod 2^(Suc k)"
  for a :: int
  using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"]
  by simp

lemma sb_inc_lem': "a < - (2^k)  a + 2^k + 2^(Suc k)  (a + 2^k) mod 2^(Suc k)"
  for a :: int
  by (rule sb_inc_lem) simp

lemma sb_dec_lem: "0  - (2 ^ k) + a  (a + 2 ^ k) mod (2 * 2 ^ k)  - (2 ^ k) + a"
  for a :: int
  using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp

lemma sb_dec_lem': "2 ^ k  a  (a + 2 ^ k) mod (2 * 2 ^ k)  - (2 ^ k) + a"
  for a :: int
  by (rule sb_dec_lem) simp

lemma mod_2_neq_1_eq_eq_0: "k mod 2  1  k mod 2 = 0"
  for k :: int
  by (fact not_mod_2_eq_1_eq_0)

lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
  for b :: int
  by arith

lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
  for b :: int
  by (rule pos_zmod_mult_2) simp

lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
  for b :: int
  by (simp add: p1mod22k' add.commute)

lemma pos_mod_sign2:
  0  a mod 2 for a :: int
  by simp

lemma pos_mod_bound2:
  a mod 2 < 2 for a :: int
  by simp

lemma nmod2: "n mod 2 = 0  n mod 2 = 1"
  for n :: int
  by arith

lemma eme1p:
  "even n  even d  0  d  (1 + n) mod d = 1 + n mod d" for n d :: int
  using emep1 [of n d] by (simp add: ac_simps)

lemma m1mod22k:
  - 1 mod (2 * 2 ^ n) = 2 * 2 ^ n - (1::int)
  by (simp add: zmod_minus1)

lemma z1pdiv2: "(2 * b + 1) div 2 = b"
  for b :: int
  by arith

lemma zdiv_le_dividend:
  0  a  0 < b  a div b  a for a b :: int
  by (metis div_by_1 int_one_le_iff_zero_less zdiv_mono2 zero_less_one)

lemma axxmod2: "(1 + x + x) mod 2 = 1  (0 + x + x) mod 2 = 0"
  for x :: int
  by arith

lemma axxdiv2: "(1 + x + x) div 2 = x  (0 + x + x) div 2 = x"
  for x :: int
  by arith

lemmas rdmods =
  mod_minus_eq [symmetric]
  mod_diff_left_eq [symmetric]
  mod_diff_right_eq [symmetric]
  mod_add_left_eq [symmetric]
  mod_add_right_eq [symmetric]
  mod_mult_right_eq [symmetric]
  mod_mult_left_eq [symmetric]

lemma mod_plus_right: "(a + x) mod m = (b + x) mod m  a mod m = b mod m"
  for a b m x :: nat
  by (induct x) (simp_all add: mod_Suc, arith)

lemma nat_minus_mod: "(n - n mod m) mod m = 0"
  for m n :: nat
  by (induct n) (simp_all add: mod_Suc)

lemmas nat_minus_mod_plus_right =
  trans [OF nat_minus_mod mod_0 [symmetric],
    THEN mod_plus_right [THEN iffD2], simplified]

lemmas push_mods' = mod_add_eq
  mod_mult_eq mod_diff_eq
  mod_minus_eq

lemmas push_mods = push_mods' [THEN eq_reflection]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]

lemma nat_mod_eq: "b < n  a mod n = b mod n  a mod n = b"
  for a b n :: nat
  by (induct a) auto

lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]

lemma nat_mod_lem: "0 < n  b < n  b mod n = b"
  for b n :: nat
  apply safe
   apply (erule nat_mod_eq')
  apply (erule subst)
  apply (erule mod_less_divisor)
  done

lemma mod_nat_add: "x < z  y < z  (x + y) mod z = (if x + y < z then x + y else x + y - z)"
  for x y z :: nat
  apply (rule nat_mod_eq)
   apply auto
  apply (rule trans)
   apply (rule le_mod_geq)
   apply simp
  apply (rule nat_mod_eq')
  apply arith
  done

lemma mod_nat_sub: "x < z  (x - y) mod z = x - y"
  for x y :: nat
  by (rule nat_mod_eq') arith

lemma int_mod_eq: "0  b  b < n  a mod n = b mod n  a mod n = b"
  for a b n :: int
  by (metis mod_pos_pos_trivial)

lemma zmde:
  b * (a div b) = a - a mod b for a b :: 'a::{group_add,semiring_modulo}
  using mult_div_mod_eq [of b a] by (simp add: eq_diff_eq)

(* already have this for naturals, div_mult_self1/2, but not for ints *)
lemma zdiv_mult_self: "m  0  (a + m * n) div m = a div m + n"
  for a m n :: int
  by simp

lemma mod_power_lem: "a > 1  a ^ n mod a ^ m = (if m  n then 0 else a ^ n)"
  for a :: int
  by (simp add: mod_eq_0_iff_dvd le_imp_power_dvd)

lemma nonneg_mod_div: "0  a  0  b  0  (a mod b)  0  a div b"
  for a b :: int
  by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])

lemma mod_exp_less_eq_exp:
  a mod 2 ^ n < 2 ^ n for a :: int
  by (rule pos_mod_bound) simp

lemma div_mult_le:
  a div b * b  a for a b :: nat
  by (fact div_times_less_eq_dividend)

lemma power_sub:
  fixes a :: nat
  assumes lt: "n  m"
  and     av: "0 < a"
  shows "a ^ (m - n) = a ^ m div a ^ n"
proof (subst nat_mult_eq_cancel1 [symmetric])
  show "(0::nat) < a ^ n" using av by simp
next
  from lt obtain q where mv: "n + q = m"
    by (auto simp: le_iff_add)

  have "a ^ n * (a ^ m div a ^ n) = a ^ m"
  proof (subst mult.commute)
    have "a ^ m = (a ^ m div a ^ n) * a ^ n + a ^ m mod a ^ n"
      by (rule  div_mult_mod_eq [symmetric])

    moreover have "a ^ m mod a ^ n = 0"
      by (subst mod_eq_0_iff_dvd, subst dvd_def, rule exI [where x = "a ^ q"],
      (subst power_add [symmetric] mv)+, rule refl)

    ultimately show "(a ^ m div a ^ n) * a ^ n = a ^ m" by simp
  qed

  then show "a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n)" using lt
    by (simp add: power_add [symmetric])
qed

lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
  apply (cut_tac m = q and n = c in mod_less_divisor)
  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
  apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
  apply (simp add: add_mult_distrib2)
  done

lemma less_two_pow_divD:
  " (x :: nat) < 2 ^ n div 2 ^ m 
     n  m  (x < 2 ^ (n - m))"
  apply (rule context_conjI)
   apply (rule ccontr)
   apply (simp add: power_strict_increasing)
  apply (simp add: power_sub)
  done

lemma less_two_pow_divI:
  " (x :: nat) < 2 ^ (n - m); m  n   x < 2 ^ n div 2 ^ m"
  by (simp add: power_sub)

lemmas m2pths = pos_mod_sign mod_exp_less_eq_exp

lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)

lemmas int_mod_le = zmod_le_nonneg_dividend (* FIXME: delete *)

lemma power_mod_div:
  fixes x :: "nat"
  shows "x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)" (is "?LHS = ?RHS")
proof (cases "n  m")
  case True
  then have "?LHS = 0"
    apply -
    apply (rule div_less)
    apply (rule order_less_le_trans [OF mod_less_divisor]; simp)
    done
  also have " = ?RHS" using True
    by simp
  finally show ?thesis .
next
  case False
  then have lt: "m < n" by simp
  then obtain q where nv: "n = m + q" and "0 < q"
    by (auto dest: less_imp_Suc_add)

  then have "x mod 2 ^ n = 2 ^ m * (x div 2 ^ m mod 2 ^ q) + x mod 2 ^ m"
    by (simp add: power_add mod_mult2_eq)

  then have "?LHS = x div 2 ^ m mod 2 ^ q"
    by (simp add: div_add1_eq)

  also have " = ?RHS" using nv
    by simp

  finally show ?thesis .
qed

lemma mod_mod_power:
  fixes k :: nat
  shows "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ (min m n)"
proof (cases "m  n")
  case True

  then have "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ m"
    apply -
    apply (subst mod_less [where n = "2 ^ n"])
    apply (rule order_less_le_trans [OF mod_less_divisor])
    apply simp+
    done
  also have " = k mod  2 ^ (min m n)" using True by simp
  finally show ?thesis .
next
  case False
  then have "n < m" by simp
  then obtain d where md: "m = n + d"
    by (auto dest: less_imp_add_positive)
  then have "k mod 2 ^ m = 2 ^ n * (k div 2 ^ n mod 2 ^ d) + k mod 2 ^ n"
    by (simp add: mod_mult2_eq power_add)
  then have "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ n"
    by (simp add: mod_add_left_eq)
  then show ?thesis using False
    by simp
qed

lemma mod_div_equality_div_eq:
  "a div b * b = (a - (a mod b) :: int)"
  by (simp add: field_simps)

lemma zmod_helper:
  "n mod m = k  ((n :: int) + a) mod m = (k + a) mod m"
  by (metis add.commute mod_add_right_eq)

lemma int_div_sub_1:
  " m  1   (n - (1 :: int)) div m = (if m dvd n then (n div m) - 1 else n div m)"
  apply (subgoal_tac "m = 0  (n - (1 :: int)) div m = (if m dvd n then (n div m) - 1 else n div m)")
   apply fastforce
  apply (subst mult_cancel_right[symmetric])
  apply (simp only: left_diff_distrib split: if_split)
  apply (simp only: mod_div_equality_div_eq)
  apply (clarsimp simp: field_simps)
  apply (clarsimp simp: dvd_eq_mod_eq_0)
  apply (cases "m = 1")
   apply simp
  apply (subst mod_diff_eq[symmetric], simp add: zmod_minus1)
  apply clarsimp
  apply (subst diff_add_cancel[where b=1, symmetric])
  apply (subst mod_add_eq[symmetric])
  apply (simp add: field_simps)
  apply (rule mod_pos_pos_trivial)
   apply (subst add_0_right[where a=0, symmetric])
   apply (rule add_mono)
    apply simp
   apply simp
  apply (cases "(n - 1) mod m = m - 1")
   apply (drule zmod_helper[where a=1])
   apply simp
  apply (subgoal_tac "1 + (n - 1) mod m  m")
   apply simp
  apply (subst field_simps, rule zless_imp_add1_zle)
  apply simp
  done

lemma power_minus_is_div:
  "b  a  (2 :: nat) ^ (a - b) = 2 ^ a div 2 ^ b"
  apply (induct a arbitrary: b)
   apply simp
  apply (erule le_SucE)
   apply (clarsimp simp:Suc_diff_le le_iff_add power_add)
  apply simp
  done

lemma two_pow_div_gt_le:
  "v < 2 ^ n div (2 ^ m :: nat)  m  n"
  by (clarsimp dest!: less_two_pow_divD)

lemma td_gal_lt:
  0 < c  a < b * c  a div c < b
  for a b c :: nat
  apply (auto dest: less_mult_imp_div_less)
  apply (metis div_le_mono div_mult_self_is_m leD leI)
  done

lemma td_gal:
  0 < c  b * c  a   b  a div c
  for a b c :: nat
  by (meson not_le td_gal_lt)

end

Theory More_Word

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Lemmas on words›

theory More_Word
  imports
    "HOL-Library.Word"
    More_Arithmetic
    More_Divides
begin

lemma unat_power_lower [simp]:
  "unat ((2::'a::len word) ^ n) = 2 ^ n" if "n < LENGTH('a::len)"
  using that by transfer simp

lemma unat_p2: "n < LENGTH('a :: len)  unat (2 ^ n :: 'a word) = 2 ^ n"
  by (fact unat_power_lower)

lemma word_div_lt_eq_0:
  "x < y  x div y = 0" for x :: "'a :: len word"
  by transfer simp

lemma word_div_eq_1_iff: "n div m = 1  n  m  unat n < 2 * unat (m :: 'a :: len word)"
  apply (simp only: word_arith_nat_defs word_le_nat_alt word_of_nat_eq_iff flip: nat_div_eq_Suc_0_iff)
  apply (simp flip: unat_div unsigned_take_bit_eq)
  done

lemma shiftl_power:
  "(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y"
  apply (induct x)
   apply simp
  apply (simp add: shiftl1_2t)
  done

lemma AND_twice [simp]:
  "(w AND m) AND m = w AND m"
  by (fact and.right_idem)

lemma word_combine_masks:
  "w AND m = z  w AND m' = z'  w AND (m OR m') = (z OR z')"
  for w m m' z z' :: 'a::len word›
  by (simp add: bit.conj_disj_distrib)

lemma p2_gt_0:
  "(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))"
  by (simp add : word_gt_0 not_le)

lemma uint_2p_alt:
  n < LENGTH('a::len)  uint ((2::'a::len word) ^ n) = 2 ^ n
  using p2_gt_0 [of n, where ?'a = 'a] by (simp add: uint_2p)

lemma p2_eq_0:
  (2::'a::len word) ^ n = 0  LENGTH('a::len)  n
  by (fact exp_eq_zero_iff)

lemma p2len:
  (2 :: 'a word) ^ LENGTH('a::len) = 0
  by simp

lemma neg_mask_is_div:
  "w AND NOT (mask n) = (w div 2^n) * 2^n"
  for w :: 'a::len word›
  by (rule bit_word_eqI)
    (auto simp add: bit_simps simp flip: push_bit_eq_mult drop_bit_eq_div)

lemma neg_mask_is_div':
  "n < size w  w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))"
  for w :: 'a::len word›
  by (rule neg_mask_is_div)

lemma and_mask_arith:
  "w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
  for w :: 'a::len word›
  by (rule bit_word_eqI)
    (auto simp add: bit_simps word_size simp flip: push_bit_eq_mult drop_bit_eq_div)

lemma and_mask_arith':
  "0 < n  w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
  for w :: 'a::len word›
  by (rule and_mask_arith)

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 :: 'a::len word›
  by (simp add: mask_eq_decr_exp)

lemma word_and_mask_le_2pm1: "w AND mask n  2 ^ n - 1"
  for w :: 'a::len word›
  by (simp add: mask_2pm1[symmetric] word_and_le1)

lemma is_aligned_AND_less_0:
  "u AND mask n = 0  v < 2^n  u AND v = 0"
  for u v :: 'a::len word›
  apply (drule less_mask_eq)
  apply (simp flip: take_bit_eq_mask)
  apply (simp add: bit_eq_iff)
  apply (auto simp add: bit_simps)
  done

lemma le_shiftr1:
  ‹shiftr1 u  shiftr1 v if u  v
using that proof transfer
  fix k l :: int
  assume ‹take_bit LENGTH('a) k  take_bit LENGTH('a) l
  then have ‹take_bit LENGTH('a) (drop_bit 1 (take_bit LENGTH('a) k))
     take_bit LENGTH('a) (drop_bit 1 (take_bit LENGTH('a) l))
    apply (simp add: take_bit_drop_bit min_def)
    apply (simp add: drop_bit_eq_div)
    done
  then show ‹take_bit LENGTH('a) (take_bit LENGTH('a) k div 2)
     take_bit LENGTH('a) (take_bit LENGTH('a) l div 2)
    by (simp add: drop_bit_eq_div)
qed

lemma and_mask_eq_iff_le_mask:
  w AND mask n = w  w  mask n
  for w :: 'a::len word›
  apply (simp flip: take_bit_eq_mask)
  apply (cases n  LENGTH('a); transfer)
   apply (simp_all add: not_le min_def)
   apply (simp_all add: mask_eq_exp_minus_1)
  apply auto
   apply (metis take_bit_int_less_exp)
  apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit)
  done

lemma less_eq_mask_iff_take_bit_eq_self:
  w  mask n  take_bit n w = w
  for w :: 'a::len word›
  by (simp add: and_mask_eq_iff_le_mask take_bit_eq_mask)

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  x - 1) = (y < x))"
  by uint_arith

lemma gt0_iff_gem1:
  0 < x  x - 1 < x
  for x :: 'a::len word›
  by (metis add.right_neutral diff_add_cancel less_irrefl measure_unat unat_arith_simps(2) word_neq_0_conv word_sub_less_iff)

lemma power_2_ge_iff:
  2 ^ n - (1 :: 'a::len word) < 2 ^ n  n < LENGTH('a)
  using gt0_iff_gem1 p2_gt_0 by blast

lemma le_mask_iff_lt_2n:
  "n < len_of TYPE ('a) = (((w :: 'a :: len word)  mask n) = (w < 2 ^ n))"
  unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt])

lemma mask_lt_2pn:
  n < LENGTH('a)  mask n < (2 :: 'a::len word) ^ n
  by (simp add: mask_eq_exp_minus_1 power_2_ge_iff)

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  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 word_and_max_word:
  fixes a::"'a::len word"
  shows "x = max_word  a AND x = a"
  by simp

lemma word_and_full_mask_simp:
  x AND mask LENGTH('a) = x for x :: 'a::len word›
proof (rule bit_eqI)
  fix n
  assume 2 ^ n  (0 :: 'a word)
  then have n < LENGTH('a)
    by simp
  then show ‹bit (x AND Bit_Operations.mask LENGTH('a)) n  bit x n
    by (simp add: bit_and_iff bit_mask_iff)
qed

lemma of_int_uint:
  "of_int (uint x) = x"
  by (fact word_of_int_uint)

corollary word_plus_and_or_coroll:
  "x AND y = 0  x + y = x OR y"
  for x y :: 'a::len word›
  using word_plus_and_or[where x=x and y=y]
  by simp

corollary word_plus_and_or_coroll2:
  "(x AND w) + (x AND NOT w) = x"
  for x w :: 'a::len word›
  apply (subst disjunctive_add)
   apply (simp add: bit_simps)
  apply (simp flip: bit.conj_disj_distrib)
  done

lemma nat_mask_eq:
  ‹nat (mask n) = mask n
  by (simp add: nat_eq_iff of_nat_mask_eq)

lemma unat_mask_eq:
  ‹unat (mask n :: 'a::len word) = mask (min LENGTH('a) n)
  by transfer (simp add: nat_mask_eq)

lemma word_plus_mono_left:
  fixes x :: "'a :: len word"
  shows "y  z; x  x + z  y + x  z + x"
  by unat_arith

lemma less_Suc_unat_less_bound:
  "n < Suc (unat (x :: 'a :: len word))  n < 2 ^ LENGTH('a)"
  by (auto elim!: order_less_le_trans intro: Suc_leI)

lemma up_ucast_inj:
  " ucast x = (ucast y::'b::len word); LENGTH('a)  len_of TYPE ('b)   x = (y::'a::len word)"
  by transfer (simp add: min_def split: if_splits)

lemmas ucast_up_inj = up_ucast_inj

lemma up_ucast_inj_eq:
  "LENGTH('a)  len_of TYPE ('b)  (ucast x = (ucast y::'b::len word)) = (x = (y::'a::len word))"
  by (fastforce dest: up_ucast_inj)

lemma no_plus_overflow_neg:
  "(x :: 'a :: len word) < -y  x  x + y"
  by (metis diff_minus_eq_add less_imp_le sub_wrap_lt)

lemma ucast_ucast_eq:
  " ucast x = (ucast (ucast y::'a word)::'c::len word); LENGTH('a)  LENGTH('b);
     LENGTH('b)  LENGTH('c)  
   x = ucast y" for x :: "'a::len word" and y :: "'b::len word"
  apply transfer
  apply (cases LENGTH('c) = LENGTH('a))
   apply (auto simp add: min_def)
  done

lemma ucast_0_I:
  "x = 0  ucast x = 0"
  by simp

lemma word_add_offset_less:
  fixes x :: "'a :: len word"
  assumes yv: "y < 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mnv: "sz < LENGTH('a :: len)"
  and    xv': "x < 2 ^ (LENGTH('a :: len) - n)"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y < 2 ^ sz"
proof (subst mn)
  from mnv mn have nv: "n < LENGTH('a)" and mv: "m < LENGTH('a)"  by auto

  have uy: "unat y < 2 ^ n"
    by (rule order_less_le_trans [OF unat_mono [OF yv] order_eq_refl],
        rule unat_power_lower[OF nv])

  have ux: "unat x < 2 ^ m"
    by (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl],
        rule unat_power_lower[OF mv])

  then show "x * 2 ^ n + y < 2 ^ (m + n)" using ux uy nv mnv xv'
    apply (subst word_less_nat_alt)
    apply (subst unat_word_ariths)+
    apply (subst mod_less)
     apply simp
     apply (subst mult.commute)
     apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]])
     apply (rule order_less_le_trans [OF unat_mono [OF xv']])
     apply (cases "n = 0"; simp)
    apply (subst unat_power_lower[OF nv])
    apply (subst mod_less)
     apply (erule order_less_le_trans [OF nat_add_offset_less], assumption)
      apply (rule mn)
     apply simp
    apply (simp add: mn mnv)
    apply (erule nat_add_offset_less; simp)
    done
qed

lemma word_less_power_trans:
  fixes n :: "'a :: len word"
  assumes nv: "n < 2 ^ (m - k)"
  and     kv: "k  m"
  and     mv: "m < len_of TYPE ('a)"
  shows "2 ^ k * n < 2 ^ m"
  using nv kv mv
  apply -
  apply (subst word_less_nat_alt)
  apply (subst unat_word_ariths)
  apply (subst mod_less)
   apply simp
   apply (rule nat_less_power_trans)
    apply (erule order_less_trans [OF unat_mono])
    apply simp
   apply simp
  apply simp
  apply (rule nat_less_power_trans)
   apply (subst unat_power_lower[where 'a = 'a, symmetric])
    apply simp
   apply (erule unat_mono)
  apply simp
  done

lemma  word_less_power_trans2:
  fixes n :: "'a::len word"
  shows "n < 2 ^ (m - k); k  m; m < LENGTH('a)  n * 2 ^ k < 2 ^ m"
  by (subst field_simps, rule word_less_power_trans)

lemma Suc_unat_diff_1:
  fixes x :: "'a :: len word"
  assumes lt: "1  x"
  shows "Suc (unat (x - 1)) = unat x"
proof -
  have "0 < unat x"
    by (rule order_less_le_trans [where y = 1], simp, subst unat_1 [symmetric],
        rule iffD1 [OF word_le_nat_alt lt])

  then show ?thesis
    by ((subst unat_sub [OF lt])+, simp only:  unat_1)
qed

lemma word_eq_unatI:
  v = w if ‹unat v = unat w
  using that by transfer (simp add: nat_eq_iff)

lemma word_div_sub:
  fixes x :: "'a :: len word"
  assumes yx: "y  x"
  and     y0: "0 < y"
  shows "(x - y) div y = x div y - 1"
  apply (rule word_eq_unatI)
  apply (subst unat_div)
  apply (subst unat_sub [OF yx])
  apply (subst unat_sub)
   apply (subst word_le_nat_alt)
   apply (subst unat_div)
   apply (subst le_div_geq)
     apply (rule order_le_less_trans [OF _ unat_mono [OF y0]])
     apply simp
    apply (subst word_le_nat_alt [symmetric], rule yx)
   apply simp
  apply (subst unat_div)
  apply (subst le_div_geq [OF _ iffD1 [OF word_le_nat_alt yx]])
   apply (rule order_le_less_trans [OF _ unat_mono [OF y0]])
   apply simp
  apply simp
  done

lemma word_mult_less_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i < j"
  and    knz: "0 < k"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "i * k < j * k"
proof -
  from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)"
    by (auto intro: order_less_subst2 simp: word_less_nat_alt elim: mult_less_mono1)

  then show ?thesis using ujk knz ij
    by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem])
qed

lemma word_mult_less_dest:
  fixes i :: "'a :: len word"
  assumes ij: "i * k < j * k"
  and    uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "i < j"
  using uik ujk ij
  by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem] elim: mult_less_mono1)

lemma word_mult_less_cancel:
  fixes k :: "'a :: len word"
  assumes knz: "0 < k"
  and    uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows "(i * k < j * k) = (i < j)"
  by (rule iffI [OF word_mult_less_dest [OF _ uik ujk] word_mult_less_mono1 [OF _ knz ujk]])

lemma Suc_div_unat_helper:
  assumes szv: "sz < LENGTH('a :: len)"
  and   usszv: "us  sz"
  shows "2 ^ (sz - us) = Suc (unat (((2::'a :: len word) ^ sz - 1) div 2 ^ us))"
proof -
  note usv = order_le_less_trans [OF usszv szv]

  from usszv obtain q where qv: "sz = us + q" by (auto simp: le_iff_add)

  have "Suc (unat (((2:: 'a word) ^ sz - 1) div 2 ^ us)) =
    (2 ^ us + unat ((2:: 'a word) ^ sz - 1)) div 2 ^ us"
    apply (subst unat_div unat_power_lower[OF usv])+
    apply (subst div_add_self1, simp+)
    done

  also have " = ((2 ^ us - 1) + 2 ^ sz) div 2 ^ us" using szv
    by (simp add: unat_minus_one)

  also have " = 2 ^ q + ((2 ^ us - 1) div 2 ^ us)"
    apply (subst qv)
    apply (subst power_add)
    apply (subst div_mult_self2; simp)
    done

  also have " = 2 ^ (sz - us)" using qv by simp

  finally show ?thesis ..
qed

lemma enum_word_nth_eq:
  (Enum.enum :: 'a::len word list) ! n = word_of_nat n
    if n < 2 ^ LENGTH('a)
    for n
  using that by (simp add: enum_word_def)

lemma length_enum_word_eq:
  ‹length (Enum.enum :: 'a::len word list) = 2 ^ LENGTH('a)
  by (simp add: enum_word_def)

lemma unat_lt2p [iff]:
  ‹unat x < 2 ^ LENGTH('a) for x :: 'a::len word›
  by transfer simp

lemma of_nat_unat [simp]:
  "of_nat  unat = id"
  by (rule ext, simp)

lemma Suc_unat_minus_one [simp]:
  "x  0  Suc (unat (x - 1)) = unat x"
  by (metis Suc_diff_1 unat_gt_0 unat_minus_one)

lemma word_add_le_dest:
  fixes i :: "'a :: len word"
  assumes le: "i + k  j + k"
  and    uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i  j"
  using uik ujk le
  by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem] elim: add_le_mono1)

lemma word_add_le_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i  j"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i + k  j + k"
proof -
  from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)"
    by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: add_le_mono1)

  then show ?thesis using ujk ij
    by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem])
qed

lemma word_add_le_mono2:
  fixes i :: "'a :: len word"
  shows "i  j; unat j + unat k < 2 ^ LENGTH('a)  k + i  k + j"
  by (subst field_simps, subst field_simps, erule (1) word_add_le_mono1)

lemma word_add_le_iff:
  fixes i :: "'a :: len word"
  assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i + k  j + k) = (i  j)"
proof
  assume "i  j"
  show "i + k  j + k" by (rule word_add_le_mono1) fact+
next
  assume "i + k  j + k"
  show "i  j" by (rule word_add_le_dest) fact+
qed

lemma word_add_less_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i < j"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i + k < j + k"
proof -
  from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)"
    by (auto elim: order_le_less_subst2 simp: word_less_nat_alt elim: add_less_mono1)

  then show ?thesis using ujk ij
    by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem])
qed

lemma word_add_less_dest:
  fixes i :: "'a :: len word"
  assumes le: "i + k < j + k"
  and    uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i < j"
  using uik ujk le
  by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem] elim: add_less_mono1)

lemma word_add_less_iff:
  fixes i :: "'a :: len word"
  assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i + k < j + k) = (i < j)"
proof
  assume "i < j"
  show "i + k < j + k" by (rule word_add_less_mono1) fact+
next
  assume "i + k < j + k"
  show "i < j" by (rule word_add_less_dest) fact+
qed

lemma word_mult_less_iff:
  fixes i :: "'a :: len word"
  assumes knz: "0 < k"
  and     uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i * k < j * k) = (i < j)"
  using assms by (rule word_mult_less_cancel)

lemma word_le_imp_diff_le:
  fixes n :: "'a::len word"
  shows "k  n; n  m  n - k  m"
  by (auto simp: unat_sub word_le_nat_alt)

lemma word_less_imp_diff_less:
  fixes n :: "'a::len word"
  shows "k  n; n < m  n - k < m"
  by (clarsimp simp: unat_sub word_less_nat_alt
             intro!: less_imp_diff_less)

lemma word_mult_le_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i  j"
  and    knz: "0 < k"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "i * k  j * k"
proof -
  from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)"
    by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: mult_le_mono1)

  then show ?thesis using ujk knz ij
    by (auto simp: word_le_nat_alt iffD1 [OF unat_mult_lem])
qed

lemma word_mult_le_iff:
  fixes i :: "'a :: len word"
  assumes knz: "0 < k"
  and     uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i * k  j * k) = (i  j)"
proof
  assume "i  j"
  show "i * k  j * k" by (rule word_mult_le_mono1) fact+
next
  assume p: "i * k  j * k"

  have "0 < unat k" using knz by (simp add: word_less_nat_alt)
  then show "i  j" using p
    by (clarsimp simp: word_le_nat_alt iffD1 [OF unat_mult_lem uik]
      iffD1 [OF unat_mult_lem ujk])
qed

lemma word_diff_less:
  fixes n :: "'a :: len word"
  shows "0 < n; 0 < m; n  m  m - n < m"
  apply (subst word_less_nat_alt)
  apply (subst unat_sub)
   apply assumption
  apply (rule diff_less)
   apply (simp_all add: word_less_nat_alt)
  done

lemma word_add_increasing:
  fixes x :: "'a :: len word"
  shows " p + w  x; p  p + w   p  x"
  by unat_arith

lemma word_random:
  fixes x :: "'a :: len word"
  shows " p  p + x'; x  x'   p  p + x"
  by unat_arith

lemma word_sub_mono:
  " a  c; d  b; a - b  a; c - d  c 
     (a - b)  (c - d :: 'a :: len word)"
  by unat_arith

lemma power_not_zero:
  "n < LENGTH('a::len)  (2 :: 'a word) ^ n  0"
  by (metis p2_gt_0 word_neq_0_conv)

lemma word_gt_a_gt_0:
  "a < n  (0 :: 'a::len word) < n"
  apply (case_tac "n = 0")
   apply clarsimp
  apply (clarsimp simp: word_neq_0_conv)
  done

lemma word_power_less_1 [simp]:
  "sz < LENGTH('a::len)  (2::'a word) ^ sz - 1 < 2 ^ sz"
  apply (simp add: word_less_nat_alt)
  apply (subst unat_minus_one)
  apply simp_all
  done

lemma word_sub_1_le:
  "x  0  x - 1  (x :: ('a :: len) word)"
  apply (subst no_ulen_sub)
  apply simp
  apply (cases "uint x = 0")
   apply (simp add: uint_0_iff)
  apply (insert uint_ge_0[where x=x])
  apply arith
  done

lemma push_bit_word_eq_nonzero:
  ‹push_bit n w  0 if w < 2 ^ m m + n < LENGTH('a) w  0
    for w :: 'a::len word›
  using that
  apply (simp only: word_neq_0_conv word_less_nat_alt
                    mod_0 unat_word_ariths
                    unat_power_lower word_le_nat_alt)
  apply (metis add_diff_cancel_right' gr0I gr_implies_not0 less_or_eq_imp_le min_def push_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_push_bit take_bit_take_bit unsigned_push_bit_eq)
  done

lemma unat_less_power:
  fixes k :: "'a::len word"
  assumes szv: "sz < LENGTH('a)"
  and     kv:  "k < 2 ^ sz"
  shows   "unat k < 2 ^ sz"
  using szv unat_mono [OF kv] by simp

lemma unat_mult_power_lem:
  assumes kv: "k < 2 ^ (LENGTH('a::len) - sz)"
  shows "unat (2 ^ sz * of_nat k :: (('a::len) word)) = 2 ^ sz * k"
proof (cases sz < LENGTH('a))
  case True
  with assms show ?thesis
    by (simp add: unat_word_ariths take_bit_eq_mod mod_simps)
      (simp add: take_bit_nat_eq_self_iff nat_less_power_trans flip: take_bit_eq_mod)
next
  case False
  with assms show ?thesis
    by simp
qed

lemma word_plus_mcs_4:
  "v + x  w + x; x  v + x  v  (w::'a::len word)"
  by uint_arith

lemma word_plus_mcs_3:
  "v  w; x  w + x  v + x  w + (x::'a::len word)"
  by unat_arith

lemma word_le_minus_one_leq:
  "x < y  x  y - 1" for x :: "'a :: len word"
  by transfer (metis le_less_trans less_irrefl take_bit_decr_eq take_bit_nonnegative zle_diff1_eq)

lemma word_less_sub_le[simp]:
  fixes x :: "'a :: len word"
  assumes nv: "n < LENGTH('a)"
  shows "(x  2 ^ n - 1) = (x < 2 ^ n)"
  using le_less_trans word_le_minus_one_leq nv power_2_ge_iff by blast

lemma unat_of_nat_len:
  "x < 2 ^ LENGTH('a)  unat (of_nat x :: 'a::len word) = x"
  by (simp add: take_bit_nat_eq_self_iff)

lemma unat_of_nat_eq:
  "x < 2 ^ LENGTH('a)  unat (of_nat x ::'a::len word) = x"
  by (rule unat_of_nat_len)

lemma unat_eq_of_nat:
  "n < 2 ^ LENGTH('a)  (unat (x :: 'a::len word) = n) = (x = of_nat n)"
  by transfer
    (auto simp add: take_bit_of_nat nat_eq_iff take_bit_nat_eq_self_iff intro: sym)

lemma alignUp_div_helper:
  fixes a :: "'a::len word"
  assumes kv: "k < 2 ^ (LENGTH('a) - n)"
  and     xk: "x = 2 ^ n * of_nat k"
  and    le: "a  x"
  and    sz: "n < LENGTH('a)"
  and   anz: "a mod 2 ^ n  0"
  shows "a div 2 ^ n < of_nat k"
proof -
  have kn: "unat (of_nat k :: 'a word) * unat ((2::'a word) ^ n) < 2 ^ LENGTH('a)"
    using xk kv sz
    apply (subst unat_of_nat_eq)
     apply (erule order_less_le_trans)
     apply simp
    apply (subst unat_power_lower, simp)
    apply (subst mult.commute)
    apply (rule nat_less_power_trans)
     apply simp
    apply simp
    done

  have "unat a div 2 ^ n * 2 ^ n  unat a"
  proof -
    have "unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n"
      by (simp add: div_mult_mod_eq)
    also have "  unat a div 2 ^ n * 2 ^ n" using sz anz
      by (simp add: unat_arith_simps)
    finally show ?thesis ..
  qed

  then have "a div 2 ^ n * 2 ^ n < a" using sz anz
    apply (subst word_less_nat_alt)
    apply (subst unat_word_ariths)
    apply (subst unat_div)
    apply simp
    apply (rule order_le_less_trans [OF mod_less_eq_dividend])
    apply (erule order_le_neq_trans [OF div_mult_le])
    done

  also from xk le have "  of_nat k * 2 ^ n" by (simp add: field_simps)
  finally show ?thesis using sz kv
    apply -
    apply (erule word_mult_less_dest [OF _ _ kn])
    apply (simp add: unat_div)
    apply (rule order_le_less_trans [OF div_mult_le])
    apply (rule unat_lt2p)
    done
qed

lemma mask_out_sub_mask:
  "(x AND NOT (mask n)) = x - (x AND (mask n))"
  for x :: 'a::len word›
  by (simp add: field_simps word_plus_and_or_coroll2)

lemma subtract_mask:
  "p - (p AND mask n) = (p AND NOT (mask n))"
  "p - (p AND NOT (mask n)) = (p AND mask n)"
  for p :: 'a::len word›
  by (simp add: field_simps word_plus_and_or_coroll2)+

lemma take_bit_word_eq_self_iff:
  ‹take_bit n w = w  n  LENGTH('a)  w < 2 ^ n
  for w :: 'a::len word›
  using take_bit_int_eq_self_iff [of n ‹take_bit LENGTH('a) (uint w)]
  by (transfer fixing: n) auto

lemma word_power_increasing:
  assumes x: "2 ^ x < (2 ^ y::'a::len word)" "x < LENGTH('a::len)" "y < LENGTH('a::len)"
  shows "x < y" using x
  using assms by transfer simp

lemma mask_twice:
  "(x AND mask n) AND mask m = x AND mask (min m n)"
  for x :: 'a::len word›
  by (simp flip: take_bit_eq_mask)

lemma plus_one_helper[elim!]:
  "x < n + (1 :: 'a :: len word)  x  n"
  apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
  apply (case_tac "1 + n = 0")
   apply simp_all
  apply (subst(asm) unatSuc, assumption)
  apply arith
  done

lemma plus_one_helper2:
  " x  n; n + 1  0   x < n + (1 :: 'a :: len word)"
  by (simp add: word_less_nat_alt word_le_nat_alt field_simps
                unatSuc)

lemma less_x_plus_1:
  fixes x :: "'a :: len word" shows
  "x  max_word  (y < (x + 1)) = (y < x  y = x)"
  apply (rule iffI)
   apply (rule disjCI)
   apply (drule plus_one_helper)
   apply simp
  apply (subgoal_tac "x < x + 1")
   apply (erule disjE, simp_all)
  apply (rule plus_one_helper2 [OF order_refl])
  apply (rule notI, drule max_word_wrap)
  apply simp
  done

lemma word_Suc_leq:
  fixes k::"'a::len word" shows "k  max_word  x < k + 1  x  k"
  using less_x_plus_1 word_le_less_eq by auto

lemma word_Suc_le:
   fixes k::"'a::len word" shows "x  max_word  x + 1  k  x < k"
  by (meson not_less word_Suc_leq)

lemma word_lessThan_Suc_atMost:
  {..< k + 1} = {..k} if k  - 1 for k :: 'a::len word›
  using that by (simp add: lessThan_def atMost_def word_Suc_leq)

lemma word_atLeastLessThan_Suc_atLeastAtMost:
  {l ..< u + 1} = {l..u} if u  - 1 for l :: 'a::len word›
  using that by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)

lemma word_atLeastAtMost_Suc_greaterThanAtMost:
  {m<..u} = {m + 1..u} if m  - 1 for m :: 'a::len word›
  using that by (simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)

lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
  fixes l::"'a::len word"
  assumes "m  max_word" and "l  m" and "m  u"
  shows "{l..m}  {m+1..u} = {l..u}"
  proof -
  from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m}  {m<..u}" by blast
  with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost)
  qed

lemma max_word_less_eq_iff [simp]:
  - 1  w  w = - 1 for w :: 'a::len word›
  by (fact word_order.extremum_unique)

lemma word_or_zero:
  "(a OR b = 0) = (a = 0  b = 0)"
  for a b :: 'a::len word›
  by (fact or_eq_0_iff)

lemma word_2p_mult_inc:
  assumes x: "2 * 2 ^ n < (2::'a::len word) * 2 ^ m"
  assumes suc_n: "Suc n < LENGTH('a::len)"
  shows "2^n < (2::'a::len word)^m"
  by (smt suc_n le_less_trans lessI nat_less_le nat_mult_less_cancel_disj p2_gt_0
          power_Suc power_Suc unat_power_lower word_less_nat_alt x)

lemma power_overflow:
  "n  LENGTH('a)  2 ^ n = (0 :: 'a::len word)"
  by simp

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 word_sint_1:
  "sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)"
  by (fact signed_1)

lemma ucast_of_nat:
  "is_down (ucast :: 'a :: len word  'b :: len word)
     ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)"
  by transfer simp

lemma scast_1':
  "(scast (1::'a::len word) :: 'b::len word) =
   (word_of_int (signed_take_bit (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 unat_minus_one_word:
  "unat (-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1"
  apply (simp only: flip: mask_eq_exp_minus_1)
  apply transfer
  apply (simp add: take_bit_minus_one_eq_mask nat_mask_eq)
  done

lemmas word_diff_ls'' = word_diff_ls [where xa=x and x=x for x]
lemmas word_diff_ls' = word_diff_ls'' [simplified]

lemmas word_l_diffs' = word_l_diffs [where xa=x and x=x for x]
lemmas word_l_diffs = word_l_diffs' [simplified]

lemma two_power_increasing:
  " n  m; m < LENGTH('a)   (2 :: 'a :: len word) ^ n  2 ^ m"
  by (simp add: word_le_nat_alt)

lemma word_leq_le_minus_one:
  " x  y; x  0   x - 1 < (y :: 'a :: len word)"
  apply (simp add: word_less_nat_alt word_le_nat_alt)
  apply (subst unat_minus_one)
   apply assumption
  apply (cases "unat x")
   apply (simp add: unat_eq_zero)
  apply arith
  done

lemma neg_mask_combine:
  "NOT(mask a) AND NOT(mask b) = NOT(mask (max a b) :: 'a::len word)"
  by (rule bit_word_eqI) (auto simp add: bit_simps)

lemma neg_mask_twice:
  "x AND NOT(mask n) AND NOT(mask m) = x AND NOT(mask (max n m))"
  for x :: 'a::len word›
  by (rule bit_word_eqI) (auto simp add: bit_simps)

lemma multiple_mask_trivia:
  "n  m  (x AND NOT(mask n)) + (x AND mask n AND NOT(mask m)) = x AND NOT(mask m)"
  for x :: 'a::len word›
  apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2)
  apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice
                   max_absorb2)
  done

lemma word_of_nat_less:
  " n < unat x   of_nat n < x"
  apply (simp add: word_less_nat_alt)
  apply (erule order_le_less_trans[rotated])
  apply (simp add: take_bit_eq_mod)
  done

lemma unat_mask:
  "unat (mask n :: 'a :: len word) = 2 ^ (min n (LENGTH('a))) - 1"
  apply (subst min.commute)
  apply (simp add: mask_eq_decr_exp not_less min_def  split: if_split_asm)
  apply (intro conjI impI)
   apply (simp add: unat_sub_if_size)
   apply (simp add: power_overflow word_size)
  apply (simp add: unat_sub_if_size)
  done

lemma mask_over_length:
  "LENGTH('a)  n  mask n = (-1::'a::len word)"
  by (simp add: mask_eq_decr_exp)

lemma Suc_2p_unat_mask:
  "n < LENGTH('a)  Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)"
  by (simp add: unat_mask)

lemma sint_of_nat_ge_zero:
  "x < 2 ^ (LENGTH('a) - 1)  sint (of_nat x :: 'a :: len word)  0"
  by (simp add: bit_iff_odd)

lemma int_eq_sint:
  "x < 2 ^ (LENGTH('a) - 1)  sint (of_nat x :: 'a :: len word) = int x"
  apply transfer
  apply (rule signed_take_bit_int_eq_self)
   apply simp_all
  apply (metis negative_zle numeral_power_eq_of_nat_cancel_iff)
  done

lemma sint_of_nat_le:
  " b < 2 ^ (LENGTH('a) - 1); a  b 
    sint (of_nat a :: 'a :: len word)  sint (of_nat b :: 'a :: len word)"
  apply (cases LENGTH('a))
  apply simp_all
  apply transfer
  apply (subst signed_take_bit_eq_if_positive)
   apply (simp add: bit_simps)
  apply (metis bit_take_bit_iff nat_less_le order_less_le_trans take_bit_nat_eq_self_iff)
  apply (subst signed_take_bit_eq_if_positive)
    apply (simp add: bit_simps)
  apply (metis bit_take_bit_iff nat_less_le take_bit_nat_eq_self_iff)
    apply (simp flip: of_nat_take_bit add: take_bit_nat_eq_self)
  done

lemma word_le_not_less:
  "((b::'a::len word)  a) = (¬(a < b))"
  by fastforce

lemma less_is_non_zero_p1:
  fixes a :: "'a :: len word"
  shows "a < k  a + 1  0"
  apply (erule contrapos_pn)
  apply (drule max_word_wrap)
  apply (simp add: not_less)
  done

lemma unat_add_lem':
  "(unat x + unat y < 2 ^ LENGTH('a)) 
    (unat (x + y :: 'a :: len word) = unat x + unat y)"
  by (subst unat_add_lem[symmetric], assumption)

lemma word_less_two_pow_divI:
  " (x :: 'a::len word) < 2 ^ (n - m); m  n; n < LENGTH('a)   x < 2 ^ n div 2 ^ m"
  apply (simp add: word_less_nat_alt)
  apply (subst unat_word_ariths)
  apply (subst mod_less)
   apply (rule order_le_less_trans [OF div_le_dividend])
   apply (rule unat_lt2p)
  apply (simp add: power_sub)
  done

lemma word_less_two_pow_divD:
  " (x :: 'a::len word) < 2 ^ n div 2 ^ m 
      n  m  (x < 2 ^ (n - m))"
  apply (cases "n < LENGTH('a)")
   apply (cases "m < LENGTH('a)")
    apply (simp add: word_less_nat_alt)
    apply (subst(asm) unat_word_ariths)
    apply (subst(asm) mod_less)
     apply (rule order_le_less_trans [OF div_le_dividend])
     apply (rule unat_lt2p)
    apply (clarsimp dest!: less_two_pow_divD)
   apply (simp add: power_overflow)
   apply (simp add: word_div_def)
  apply (simp add: power_overflow word_div_def)
  done

lemma of_nat_less_two_pow_div_set:
  " n < LENGTH('a)  
   {x. x < (2 ^ n div 2 ^ m :: 'a::len word)}
      = of_nat ` {k. k < 2 ^ n div 2 ^ m}"
  apply (simp add: image_def)
  apply (safe dest!: word_less_two_pow_divD less_two_pow_divD
             intro!: word_less_two_pow_divI)
   apply (rule_tac x="unat x" in exI)
   apply (simp add: power_sub[symmetric])
   apply (subst unat_power_lower[symmetric, where 'a='a])
    apply simp
   apply (erule unat_mono)
  apply (subst word_unat_power)
  apply (rule of_nat_mono_maybe)
   apply (rule power_strict_increasing)
    apply simp
   apply simp
  apply assumption
  done

lemma ucast_less:
  "LENGTH('b) < LENGTH('a) 
   (ucast (x :: 'b :: len word) :: ('a :: len word)) < 2 ^ LENGTH('b)"
  by transfer simp

lemma ucast_range_less:
  "LENGTH('a :: len) < LENGTH('b :: len) 
   range (ucast :: 'a word  'b word) = {x. x < 2 ^ len_of TYPE ('a)}"
  apply safe
   apply (erule ucast_less)
  apply (simp add: image_def)
  apply (rule_tac x="ucast x" in exI)
  apply (rule bit_word_eqI)
  apply (auto simp add: bit_simps)
  apply (metis bit_take_bit_iff less_mask_eq not_less take_bit_eq_mask)
  done

lemma word_power_less_diff:
  "2 ^ n * q < (2::'a::len word) ^ m; q < 2 ^ (LENGTH('a) - n)  q < 2 ^ (m - n)"
  apply (case_tac "m  LENGTH('a)")
   apply (simp add: power_overflow)
  apply (case_tac "n  LENGTH('a)")
   apply (simp add: power_overflow)
  apply (cases "n = 0")
   apply simp
  apply (subst word_less_nat_alt)
  apply (subst unat_power_lower)
   apply simp
  apply (rule nat_power_less_diff)
  apply (simp add: word_less_nat_alt)
  apply (subst (asm) iffD1 [OF unat_mult_lem])
   apply (simp add:nat_less_power_trans)
  apply simp
  done

lemma word_less_sub_1:
  "x < (y :: 'a :: len word)  x  y - 1"
  by (fact word_le_minus_one_leq)

lemma word_sub_mono2:
  " a + b  c + d; c  a; b  a + b; d  c + d 
     b  (d :: 'a :: len word)"
  apply (drule(1) word_sub_mono)
    apply simp
   apply simp
  apply simp
  done

lemma word_not_le:
  "(¬ x  (y :: 'a :: len word)) = (y < x)"
  by fastforce

lemma word_subset_less:
  " {x .. x + r - 1}  {y .. y + s - 1};
     x  x + r - 1; y  y + (s :: 'a :: len word) - 1;
     s  0 
      r  s"
  apply (frule subsetD[where c=x])
   apply simp
  apply (drule subsetD[where c="x + r - 1"])
   apply simp
  apply (clarsimp simp: add_diff_eq[symmetric])
  apply (drule(1) word_sub_mono2)
    apply (simp_all add: olen_add_eqv[symmetric])
  apply (erule word_le_minus_cancel)
  apply (rule ccontr)
  apply (simp add: word_not_le)
  done

lemma uint_power_lower:
  "n < LENGTH('a)  uint (2 ^ n :: 'a :: len word) = (2 ^ n :: int)"
  by (rule uint_2p_alt)

lemma power_le_mono:
  "2 ^ n  (2::'a::len word) ^ m; n < LENGTH('a); m < LENGTH('a)
    n  m"
  apply (clarsimp simp add: le_less)
  apply safe
  apply (simp add: word_less_nat_alt)
  apply (simp only: uint_arith_simps(3))
  apply (drule uint_power_lower)+
  apply simp
  done

lemma two_power_eq:
  "n < LENGTH('a); m < LENGTH('a)
    ((2::'a::len word) ^ n = 2 ^ m) = (n = m)"
  apply safe
  apply (rule order_antisym)
   apply (simp add: power_le_mono[where 'a='a])+
  done

lemma unat_less_helper:
  "x < of_nat n  unat x < n"
  apply (simp add: word_less_nat_alt)
  apply (erule order_less_le_trans)
  apply (simp add: take_bit_eq_mod)
  done

lemma nat_uint_less_helper:
  "nat (uint y) = z  x < y  nat (uint x) < z"
  apply (erule subst)
  apply (subst unat_eq_nat_uint [symmetric])
  apply (subst unat_eq_nat_uint [symmetric])
  by (simp add: unat_mono)

lemma of_nat_0:
  "of_nat n = (0::'a::len word); n < 2 ^ LENGTH('a)  n = 0"
  by transfer (simp add: take_bit_eq_mod)

lemma of_nat_inj:
  "x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a) 
   (of_nat x = (of_nat y :: 'a :: len word)) = (x = y)"
  by (metis unat_of_nat_len)

lemma div_to_mult_word_lt:
  " (x :: 'a :: len word)  y div z   x * z  y"
  apply (cases "z = 0")
   apply simp
  apply (simp add: word_neq_0_conv)
  apply (rule order_trans)
   apply (erule(1) word_mult_le_mono1)
   apply (simp add: unat_div)
   apply (rule order_le_less_trans [OF div_mult_le])
   apply simp
  apply (rule word_div_mult_le)
  done

lemma ucast_ucast_mask:
  "(ucast :: 'a :: len word  'b :: len word) (ucast x) = x AND mask (len_of TYPE ('a))"
  apply (simp flip: take_bit_eq_mask)
  apply transfer
  apply (simp add: ac_simps)
  done

lemma ucast_ucast_len:
  " x < 2 ^ LENGTH('b)   ucast (ucast x::'b::len word) = (x::'a::len word)"
  apply (subst ucast_ucast_mask)
  apply (erule less_mask_eq)
  done

lemma ucast_ucast_id:
  "LENGTH('a) < LENGTH('b)  ucast (ucast (x::'a::len word)::'b::len word) = x"
  by (auto intro: ucast_up_ucast_id simp: is_up_def source_size_def target_size_def word_size)

lemma unat_ucast:
  "unat (ucast x :: ('a :: len) word) = unat x mod 2 ^ (LENGTH('a))"
proof -
  have 2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))
    by simp
  moreover have ‹unat (ucast x :: 'a word) = unat x mod nat (2 ^ LENGTH('a))
    by transfer (simp flip: nat_mod_distrib take_bit_eq_mod)
  ultimately show ?thesis
    by (simp only:)
qed

lemma ucast_less_ucast:
  "LENGTH('a)  LENGTH('b) 
   (ucast x < ((ucast (y :: 'a::len word)) :: 'b::len word)) = (x < y)"
  apply (simp add: word_less_nat_alt unat_ucast)
  apply (subst mod_less)
   apply(rule less_le_trans[OF unat_lt2p], simp)
  apply (subst mod_less)
   apply(rule less_le_trans[OF unat_lt2p], simp)
  apply simp
  done

― ‹This weaker version was previously called @{text ucast_less_ucast}. We retain it to
    support existing proofs.›
lemmas ucast_less_ucast_weak = ucast_less_ucast[OF order.strict_implies_order]

lemma unat_Suc2:
  fixes n :: "'a :: len word"
  shows
  "n  -1  unat (n + 1) = Suc (unat n)"
  apply (subst add.commute, rule unatSuc)
  apply (subst eq_diff_eq[symmetric], simp add: minus_equation_iff)
  done

lemma word_div_1:
  "(n :: 'a :: len word) div 1 = n"
  by (fact bits_div_by_1)

lemma word_minus_one_le:
  "-1  (x :: 'a :: len word) = (x = -1)"
  by (fact word_order.extremum_unique)

lemma up_scast_inj:
      " scast x = (scast y :: 'b :: len word); size x  LENGTH('b) 
          x = y"
  apply transfer
  apply (cases LENGTH('a))
  apply simp_all
  apply (metis order_refl take_bit_signed_take_bit take_bit_tightened)
  done

lemma up_scast_inj_eq:
  "LENGTH('a)  len_of TYPE ('b) 
  (scast x = (scast y::'b::len word)) = (x = (y::'a::len word))"
  by (fastforce dest: up_scast_inj simp: word_size)

lemma word_le_add:
  fixes x :: "'a :: len word"
  shows "x  y  n. y = x + of_nat n"
  by (rule exI [where x = "unat (y - x)"]) simp

lemma word_plus_mcs_4':
  fixes x :: "'a :: len word"
  shows "x + v  x + w; x  x + v  v  w"
  apply (rule word_plus_mcs_4)
   apply (simp add: add.commute)
  apply (simp add: add.commute)
  done

lemma unat_eq_1:
  ‹unat x = Suc 0  x = 1
  by (auto intro!: unsigned_word_eqI [where ?'a = nat])

lemma word_unat_Rep_inject1:
  ‹unat x = unat 1  x = 1
  by (simp add: unat_eq_1)

lemma and_not_mask_twice:
  "(w AND NOT (mask n)) AND NOT (mask m) = w AND NOT (mask (max m n))"
  for w :: 'a::len word›
  by (rule bit_word_eqI) (auto simp add: bit_simps)

lemma word_less_cases:
  "x < y  x = y - 1  x < y - (1 ::'a::len word)"
  apply (drule word_less_sub_1)
  apply (drule order_le_imp_less_or_eq)
  apply auto
  done

lemma mask_and_mask:
  "mask a AND mask b = (mask (min a b) :: 'a::len word)"
  by (simp flip: take_bit_eq_mask ac_simps)

lemma mask_eq_0_eq_x:
  "(x AND w = 0) = (x AND NOT w = x)"
  for x w :: 'a::len word›
  using word_plus_and_or_coroll2[where x=x and w=w]
  by auto

lemma mask_eq_x_eq_0:
  "(x AND w = x) = (x AND NOT w = 0)"
  for x w :: 'a::len word›
  using word_plus_and_or_coroll2[where x=x and w=w]
  by auto

lemma compl_of_1: "NOT 1 = (-2 :: 'a :: len word)"
  by (fact not_one)

lemma split_word_eq_on_mask:
  "(x = y) = (x AND m = y AND m  x AND NOT m = y AND NOT m)"
  for x y m :: 'a::len word›
  apply transfer
  apply (simp add: bit_eq_iff)
  apply (auto simp add: bit_simps ac_simps)
  done

lemma word_FF_is_mask:
  "0xFF = (mask 8 :: 'a::len word)"
  by (simp add: mask_eq_decr_exp)

lemma word_1FF_is_mask:
  "0x1FF = (mask 9 :: 'a::len word)"
  by (simp add: mask_eq_decr_exp)

lemma ucast_of_nat_small:
  "x < 2 ^ LENGTH('a)  ucast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)"
  apply transfer
  apply (auto simp add: take_bit_of_nat min_def not_le)
  apply (metis linorder_not_less min_def take_bit_nat_eq_self take_bit_take_bit)
  done

lemma word_le_make_less:
  fixes x :: "'a :: len word"
  shows "y  -1  (x  y) = (x < (y + 1))"
  apply safe
  apply (erule plus_one_helper2)
  apply (simp add: eq_diff_eq[symmetric])
  done

lemmas finite_word = finite [where 'a="'a::len word"]

lemma word_to_1_set:
  "{0 ..< (1 :: 'a :: len word)} = {0}"
  by fastforce

lemma word_leq_minus_one_le:
  fixes x :: "'a::len word"
  shows "y  0; x  y - 1   x < y"
  using le_m1_iff_lt word_neq_0_conv by blast

lemma word_count_from_top:
  "n  0  {0 ..< n :: 'a :: len word} = {0 ..< n - 1}  {n - 1}"
  apply (rule set_eqI, rule iffI)
   apply simp
   apply (drule word_le_minus_one_leq)
   apply (rule disjCI)
   apply simp
  apply simp
  apply (erule word_leq_minus_one_le)
  apply fastforce
  done

lemma word_minus_one_le_leq:
  " x - 1 < y   x  (y :: 'a :: len word)"
  apply (cases "x = 0")
   apply simp
  apply (simp add: word_less_nat_alt word_le_nat_alt)
  apply (subst(asm) unat_minus_one)
   apply (simp add: word_less_nat_alt)
  apply (cases "unat x")
   apply (simp add: unat_eq_zero)
  apply arith
  done

lemma word_div_less:
  "m < n  m div n = 0" for m :: "'a :: len word"
  by (simp add: unat_mono word_arith_nat_defs(6))

lemma word_must_wrap:
  " x  n - 1; n  x   n = (0 :: 'a :: len word)"
  using dual_order.trans sub_wrap word_less_1 by blast

lemma range_subset_card:
  " {a :: 'a :: len word .. b}  {c .. d}; b  a   d  c  d - c  b - a"
  using word_sub_le word_sub_mono by fastforce

lemma less_1_simp:
  "n - 1 < m = (n  (m :: 'a :: len word)  n  0)"
  by unat_arith

lemma word_power_mod_div:
  fixes x :: "'a::len word"
  shows " n < LENGTH('a); m < LENGTH('a)
   x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)"
  apply (simp add: word_arith_nat_div unat_mod power_mod_div)
  apply (subst unat_arith_simps(3))
  apply (subst unat_mod)
  apply (subst unat_of_nat)+
  apply (simp add: mod_mod_power min.commute)
  done

lemma word_range_minus_1':
  fixes a :: "'a :: len word"
  shows "a  0  {a - 1<..b} = {a..b}"
  by (simp add: greaterThanAtMost_def atLeastAtMost_def greaterThan_def atLeast_def less_1_simp)

lemma word_range_minus_1:
  fixes a :: "'a :: len word"
  shows "b  0  {a..b - 1} = {a..<b}"
  apply (simp add: atLeastLessThan_def atLeastAtMost_def atMost_def lessThan_def)
  apply (rule arg_cong [where f = "λx. {a..}  x"])
  apply rule
   apply clarsimp
   apply (erule contrapos_pp)
   apply (simp add: linorder_not_less linorder_not_le word_must_wrap)
  apply (clarsimp)
  apply (drule word_le_minus_one_leq)
  apply (auto simp: word_less_sub_1)
  done

lemma ucast_nat_def:
  "of_nat (unat x) = (ucast :: 'a :: len word  'b :: len word) x"
  by transfer simp

lemma overflow_plus_one_self:
  "(1 + p  p) = (p = (-1 :: 'a :: len word))"
  apply rule
  apply (rule ccontr)
   apply (drule plus_one_helper2)
   apply (rule notI)
   apply (drule arg_cong[where f="λx. x - 1"])
   apply simp
   apply (simp add: field_simps)
  apply simp
  done

lemma plus_1_less:
  "(x + 1  (x :: 'a :: len word)) = (x = -1)"
  apply (rule iffI)
   apply (rule ccontr)
   apply (cut_tac plus_one_helper2[where x=x, OF order_refl])
    apply simp
   apply clarsimp
   apply (drule arg_cong[where f="λx. x - 1"])
   apply simp
  apply simp
  done

lemma pos_mult_pos_ge:
  "[|x > (0::int); n>=0 |] ==> n * x >= n*1"
  apply (simp only: mult_left_mono)
  done

lemma word_plus_strict_mono_right:
  fixes x :: "'a :: len word"
  shows "y < z; x  x + z  x + y < x + z"
  by unat_arith

lemma word_div_mult:
  "0 < c  a < b * c  a div c < b" for a b c :: "'a::len word"
  by (rule classical)
     (use div_to_mult_word_lt [of b a c] in
      auto simp add: word_less_nat_alt word_le_nat_alt unat_div›)

lemma word_less_power_trans_ofnat:
  "n < 2 ^ (m - k); k  m; m < LENGTH('a)
    of_nat n * 2 ^ k < (2::'a::len word) ^ m"
  apply (subst mult.commute)
  apply (rule word_less_power_trans)
    apply (simp_all add: word_less_nat_alt less_le_trans take_bit_eq_mod)
  done

lemma word_1_le_power:
  "n < LENGTH('a)  (1 :: 'a :: len word)  2 ^ n"
  by (rule inc_le[where i=0, simplified], erule iffD2[OF p2_gt_0])

lemma unat_1_0:
  "1  (x::'a::len word) = (0 < unat x)"
  by (auto simp add: word_le_nat_alt)

lemma x_less_2_0_1':
  fixes x :: "'a::len word"
  shows "LENGTH('a)  1; x < 2  x = 0  x = 1"
  apply (cases 2  LENGTH('a))
  apply simp_all
  apply transfer
  apply auto
  apply (metis add.commute add.right_neutral even_two_times_div_two mod_div_trivial mod_pos_pos_trivial mult.commute mult_zero_left not_less not_take_bit_negative odd_two_times_div_two_succ)
  done

lemmas word_add_le_iff2 = word_add_le_iff [folded no_olen_add_nat]

lemma of_nat_power:
  shows " p < 2 ^ x; x < len_of TYPE ('a)   of_nat p < (2 :: 'a :: len word) ^ x"
  apply (rule order_less_le_trans)
   apply (rule of_nat_mono_maybe)
    apply (erule power_strict_increasing)
    apply simp
   apply assumption
  apply (simp add: word_unat_power del: of_nat_power)
  done

lemma of_nat_n_less_equal_power_2:
  "n < LENGTH('a::len)  ((of_nat n)::'a word) < 2 ^ n"
  apply (induct n)
   apply clarsimp
  apply clarsimp
  apply (metis of_nat_power n_less_equal_power_2 of_nat_Suc power_Suc)
  done

lemma eq_mask_less:
  fixes w :: "'a::len word"
  assumes eqm: "w = w AND mask n"
  and      sz: "n < len_of TYPE ('a)"
  shows "w < (2::'a word) ^ n"
  by (subst eqm, rule and_mask_less' [OF sz])

lemma of_nat_mono_maybe':
  fixes Y :: "nat"
  assumes xlt: "x < 2 ^ len_of TYPE ('a)"
  assumes ylt: "y < 2 ^ len_of TYPE ('a)"
  shows   "(y < x) = (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 (rule ylt)
  apply (subst mod_less)
   apply (rule xlt)
  apply simp
  done

lemma of_nat_mono_maybe_le:
  "x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a) 
  (y  x) = ((of_nat y :: 'a :: len word)  of_nat x)"
  apply (clarsimp simp: le_less)
  apply (rule disj_cong)
   apply (rule of_nat_mono_maybe', assumption+)
  apply auto
  using of_nat_inj apply blast
  done

lemma mask_AND_NOT_mask:
  "(w AND NOT (mask n)) AND mask n = 0"
  for w :: 'a::len word›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma AND_NOT_mask_plus_AND_mask_eq:
  "(w AND NOT (mask n)) + (w AND mask n) = w"
  for w :: 'a::len word›
  apply (subst disjunctive_add)
  apply (auto simp add: bit_simps)
  apply (rule bit_word_eqI)
  apply (auto simp add: bit_simps)
  done

lemma mask_eqI:
  fixes x :: "'a :: len word"
  assumes m1: "x AND mask n = y AND mask n"
  and     m2: "x AND NOT (mask n) = y AND NOT (mask n)"
  shows "x = y"
proof -
  have *: x = x AND mask n OR x AND NOT (mask n) for x :: 'a word›
    by (rule bit_word_eqI) (auto simp add: bit_simps)
  from assms * [of x] * [of y] show ?thesis
    by simp
qed

lemma neq_0_no_wrap:
  fixes x :: "'a :: len word"
  shows " x  x + y; x  0   x + y  0"
  by clarsimp

lemma unatSuc2:
  fixes n :: "'a :: len word"
  shows "n + 1  0  unat (n + 1) = Suc (unat n)"
  by (simp add: add.commute unatSuc)

lemma word_of_nat_le:
  "n  unat x  of_nat n  x"
  apply (simp add: word_le_nat_alt unat_of_nat)
  apply (erule order_trans[rotated])
  apply (simp add: take_bit_eq_mod)
  done

lemma word_unat_less_le:
  "a  of_nat b  unat a  b"
  by (metis eq_iff le_cases le_unat_uoi word_of_nat_le)

lemma mask_Suc_0 : "mask (Suc 0) = (1 :: 'a::len word)"
  by (simp add: mask_eq_decr_exp)

lemma bool_mask':
  fixes x :: "'a :: len word"
  shows "2 < LENGTH('a)  (0 < x AND 1) = (x AND 1 = 1)"
  by (simp add: and_one_eq mod_2_eq_odd)

lemma ucast_ucast_add:
  fixes x :: "'a :: len word"
  fixes y :: "'b :: len word"
  shows
  "LENGTH('b)  LENGTH('a) 
    ucast (ucast x + y) = x + ucast y"
  apply transfer
  apply simp
  apply (subst (2) take_bit_add [symmetric])
  apply (subst take_bit_add [symmetric])
  apply simp
  done

lemma lt1_neq0:
  fixes x :: "'a :: len word"
  shows "(1  x) = (x  0)" by unat_arith

lemma word_plus_one_nonzero:
  fixes x :: "'a :: len word"
  shows "x  x + y; y  0  x + 1  0"
  apply (subst lt1_neq0 [symmetric])
  apply (subst olen_add_eqv [symmetric])
  apply (erule word_random)
  apply (simp add: lt1_neq0)
  done

lemma word_sub_plus_one_nonzero:
  fixes n :: "'a :: len word"
  shows "n'  n; n'  0  (n - n') + 1  0"
  apply (subst lt1_neq0 [symmetric])
  apply (subst olen_add_eqv [symmetric])
  apply (rule word_random [where x' = n'])
   apply simp
   apply (erule word_sub_le)
  apply (simp add: lt1_neq0)
  done

lemma word_le_minus_mono_right:
  fixes x :: "'a :: len word"
  shows " z  y; y  x; z  x   x - y  x - z"
  apply (rule word_sub_mono)
     apply simp
    apply assumption
   apply (erule word_sub_le)
  apply (erule word_sub_le)
  done

lemma word_0_sle_from_less:
  0 ≤s x if x < 2 ^ (LENGTH('a) - 1) for x :: 'a::len word›
  using that
  apply transfer
  apply (cases LENGTH('a))
   apply simp_all
  apply (metis bit_take_bit_iff min_def nat_less_le not_less_eq take_bit_int_eq_self_iff take_bit_take_bit)
  done

lemma ucast_sub_ucast:
  fixes x :: "'a::len word"
  assumes "y  x"
  assumes T: "LENGTH('a)  LENGTH('b)"
  shows "ucast (x - y) = (ucast x - ucast y :: 'b::len word)"
proof -
  from T
  have P: "unat x < 2 ^ LENGTH('b)" "unat y < 2 ^ LENGTH('b)"
    by (fastforce intro!: less_le_trans[OF unat_lt2p])+
  then show ?thesis
    by (simp add: unat_arith_simps unat_ucast assms[simplified unat_arith_simps])
qed

lemma word_1_0:
  "a + (1::('a::len) word)  b; a < of_nat x  a < b"
  apply transfer
  apply (subst (asm) take_bit_incr_eq)
   apply (auto simp add: diff_less_eq)
  using take_bit_int_less_exp le_less_trans by blast

lemma unat_of_nat_less:" a < b; unat b = c   a < of_nat c"
  by fastforce

lemma word_le_plus_1: " (y::('a::len) word) < y + n; a < n   y + a  y + a + 1"
  by unat_arith

lemma word_le_plus:"(a::('a::len) word) < a + b; c < b  a  a + c"
  by (metis order_less_imp_le word_random)

lemma sint_minus1 [simp]: "(sint x = -1) = (x = -1)"
  apply (cases LENGTH('a))
   apply simp_all
  apply transfer
  apply (simp flip: signed_take_bit_eq_iff_take_bit_eq)
  done

lemma sint_0 [simp]: "(sint x = 0) = (x = 0)"
  by (fact signed_eq_0_iff)

(* It is not always that case that "sint 1 = 1", because of 1-bit word sizes.
 * This lemma produces the different cases. *)
lemma sint_1_cases:
  P if  len_of TYPE ('a::len) = 1; (a::'a word) = 0; sint a = 0   P
      len_of TYPE ('a) = 1; a = 1; sint (1 :: 'a word) = -1   P
      len_of TYPE ('a) > 1; sint (1 :: 'a word) = 1   P
proof (cases LENGTH('a) = 1)
  case True
  then have a = 0  a = 1
    by transfer auto
  with True that show ?thesis
    by auto
next
  case False
  with that show ?thesis
    by (simp add: less_le Suc_le_eq)
qed

lemma sint_int_min:
  "sint (- (2 ^ (LENGTH('a) - Suc 0)) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))"
  apply (cases LENGTH('a))
   apply simp_all
  apply transfer
  apply (simp add: signed_take_bit_int_eq_self)
  done

lemma sint_int_max_plus_1:
  "sint (2 ^ (LENGTH('a) - Suc 0) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))"
  apply (cases LENGTH('a))
   apply simp_all
  apply (subst word_of_int_2p [symmetric])
  apply (subst int_word_sint)
  apply simp
  done

lemma uint_range':
  0  uint x  uint x < 2 ^ LENGTH('a)
  for x :: 'a::len word›
  by transfer simp

lemma sint_of_int_eq:
  " - (2 ^ (LENGTH('a) - 1))  x; x < 2 ^ (LENGTH('a) - 1)   sint (of_int x :: ('a::len) word) = x"
  by (simp add: signed_take_bit_int_eq_self)

lemma of_int_sint:
  "of_int (sint a) = a"
  by simp

lemma sint_ucast_eq_uint:
    " ¬ is_down (ucast :: ('a::len word  'b::len word)) 
             sint ((ucast :: ('a::len word  'b::len word)) x) = uint x"
  apply transfer
  apply (simp add: signed_take_bit_take_bit)
  done

lemma word_less_nowrapI':
  "(x :: 'a :: len word)  z - k  k  z  0 < k  x < x + k"
  by uint_arith

lemma mask_plus_1:
  "mask n + 1 = (2 ^ n :: 'a::len word)"
  by (clarsimp simp: mask_eq_decr_exp)

lemma unat_inj: "inj unat"
  by (metis eq_iff injI word_le_nat_alt)

lemma unat_ucast_upcast:
  "is_up (ucast :: 'b word  'a word)
       unat (ucast x :: ('a::len) word) = unat (x :: ('b::len) word)"
  unfolding ucast_eq unat_eq_nat_uint
  apply transfer
  apply simp
  done

lemma ucast_mono:
  " (x :: 'b :: len word) < y; y < 2 ^ LENGTH('a) 
    ucast x < ((ucast y) :: 'a :: len word)"
  apply (simp only: flip: ucast_nat_def)
  apply (rule of_nat_mono_maybe)
  apply (rule unat_less_helper)
  apply simp
  apply (simp add: word_less_nat_alt)
  done

lemma ucast_mono_le:
  "x  y; y < 2 ^ LENGTH('b)  (ucast (x :: 'a :: len word) :: 'b :: len word)  ucast y"
  apply (simp only: flip: ucast_nat_def)
  apply (subst of_nat_mono_maybe_le[symmetric])
    apply (rule unat_less_helper)
    apply simp
   apply (rule unat_less_helper)
   apply (erule le_less_trans)
  apply (simp_all add: word_le_nat_alt)
  done

lemma ucast_mono_le':
  " unat y < 2 ^ LENGTH('b); LENGTH('b::len) < LENGTH('a::len); x  y 
    ucast x  (ucast y :: 'b word)" for x y :: 'a::len word›
  by (auto simp: word_less_nat_alt intro: ucast_mono_le)

lemma neg_mask_add_mask:
  "((x:: 'a :: len word) AND NOT (mask n)) + (2 ^ n - 1) = x OR mask n"
  unfolding mask_2pm1 [symmetric]
  apply (subst word_plus_and_or_coroll; rule bit_word_eqI)
   apply (auto simp add: bit_simps)
  done

lemma le_step_down_word:"(i::('a::len) word)  n; i = n  P; i  n - 1  P  P"
  by unat_arith

lemma le_step_down_word_2:
  fixes x :: "'a::len word"
  shows "x   y; x  y  x  y - 1"
  by (subst (asm) word_le_less_eq,
      clarsimp,
      simp add: word_le_minus_one_leq)

lemma NOT_mask_AND_mask[simp]: "(w AND mask n) AND NOT (mask n) = 0"
  by (clarsimp simp add: mask_eq_decr_exp Parity.bit_eq_iff bit_and_iff bit_not_iff bit_mask_iff)

lemma and_and_not[simp]:"(a AND b) AND NOT b = 0"
  for a b :: 'a::len word›
  apply (subst word_bw_assocs(1))
  apply clarsimp
  done

lemma ex_mask_1[simp]: "(x. mask x = (1 :: 'a::len word))"
  apply (rule_tac x=1 in exI)
  apply (simp add:mask_eq_decr_exp)
  done

lemma not_switch:"NOT a = x  a = NOT x"
  by auto

end

Theory Signed_Words

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Signed Words"

theory Signed_Words
  imports "HOL-Library.Word"
begin

text ‹Signed words as separate (isomorphic) word length class. Useful for tagging words in C.›

typedef ('a::len0) signed = "UNIV :: 'a set" ..

lemma card_signed [simp]: "CARD (('a::len0) signed) = CARD('a)"
  unfolding type_definition.card [OF type_definition_signed]
  by simp

instantiation signed :: (len0) len0
begin

definition
  len_signed [simp]: "len_of (x::'a::len0 signed itself) = LENGTH('a)"

instance ..

end

instance signed :: (len) len
  by (intro_classes, simp)

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 ucast_scast_id [simp]:
  "ucast (scast (x :: 'a::len signed word) :: 'a word) = x"
  by transfer (simp add: take_bit_signed_take_bit)

lemma scast_of_nat [simp]:
  "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)"
  by transfer (simp add: take_bit_signed_take_bit)

lemma scast_ucast_id [simp]:
  "scast (ucast (x :: 'a::len word) :: 'a signed word) = x"
  by transfer (simp add: take_bit_signed_take_bit) 

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 scast_2_power [simp]: "scast ((2 :: 'a::len signed word) ^ x) = ((2 :: 'a word) ^ x)"
  by (rule bit_word_eqI) (auto simp add: bit_simps)

lemma ucast_nat_def':
  "of_nat (unat x) = (ucast :: 'a :: len word  ('b :: len) signed word) x"
  by (fact of_nat_unat)

lemma zero_sle_ucast_up:
  "¬ is_down (ucast :: 'a word  'b signed word) 
          (0 <=s ((ucast (b::('a::len) word)) :: ('b::len) signed word))"
  by transfer (simp add: bit_simps)

lemma word_le_ucast_sless:
  " x  y; y  -1; LENGTH('a) < LENGTH('b)  
    (ucast x :: ('b :: len) signed word) <s ucast (y + 1)"
  for x y :: 'a::len word›
  apply (cases LENGTH('b))
  apply simp_all
  apply transfer
  apply (simp add: signed_take_bit_take_bit)
  apply (metis add.commute mask_eq_exp_minus_1 mask_eq_take_bit_minus_one take_bit_incr_eq zle_add1_eq_le)
  done

lemma zero_sle_ucast:
  "(0 <=s ((ucast (b::('a::len) word)) :: ('a::len) signed word))
                = (uint b < 2 ^ (LENGTH('a) - 1))"
  apply transfer
  apply (cases LENGTH('a))
   apply (simp_all add: take_bit_Suc_from_most bit_simps)
  apply (simp_all add: bit_simps disjunctive_add)
  done

type_synonym 'a sword = "'a signed word"

end

Theory Traditional_Infix_Syntax

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* Author: Jeremy Dawson, NICTA *)

section ‹Operation variants with traditional syntax›

theory Traditional_Infix_Syntax
  imports "HOL-Library.Word" More_Word Signed_Words
begin

class semiring_bit_syntax = semiring_bit_shifts
begin

definition test_bit :: 'a  nat  bool›  (infixl "!!" 100)
  where test_bit_eq_bit: test_bit = bit›

definition shiftl :: 'a  nat  'a  (infixl "<<" 55)
  where shiftl_eq_push_bit: a << n = push_bit n a

definition shiftr :: 'a  nat  'a  (infixl ">>" 55)
  where shiftr_eq_drop_bit: a >> n = drop_bit n a

end

instance word :: (len) semiring_bit_syntax ..

context
  includes lifting_syntax
begin

lemma test_bit_word_transfer [transfer_rule]:
  (pcr_word ===> (=)) (λk n. n < LENGTH('a)  bit k n) (test_bit :: 'a::len word  _)
  by (unfold test_bit_eq_bit) transfer_prover

lemma shiftl_word_transfer [transfer_rule]:
  (pcr_word ===> (=) ===> pcr_word) (λk n. push_bit n k) shiftl›
  by (unfold shiftl_eq_push_bit) transfer_prover

lemma shiftr_word_transfer [transfer_rule]:
  (pcr_word ===> (=) ===> pcr_word) (λk n. (drop_bit n  take_bit LENGTH('a)) k) (shiftr :: 'a::len word  _)
  by (unfold shiftr_eq_drop_bit) transfer_prover

end


lemma test_bit_word_eq:
  ‹test_bit = (bit :: 'a::len word  _)
  by (fact test_bit_eq_bit)

lemma shiftl_word_eq:
  w << n = push_bit n w for w :: 'a::len word›
  by (fact shiftl_eq_push_bit)

lemma shiftr_word_eq:
  w >> n = drop_bit n w for w :: 'a::len word›
  by (fact shiftr_eq_drop_bit)

lemma test_bit_eq_iff: "test_bit u = test_bit v  u = v"
  for u v :: "'a::len word"
  by (simp add: bit_eq_iff test_bit_eq_bit fun_eq_iff)

lemma test_bit_size: "w !! n  n < size w"
  for w :: "'a::len word"
  by transfer simp

lemma word_eq_iff: "x = y  (n<LENGTH('a). x !! n = y !! n)" (is ?P  ?Q)
  for x y :: "'a::len word"
  by transfer (auto simp add: bit_eq_iff bit_take_bit_iff)

lemma word_eqI: "(n. n < size u  u !! n = v !! n)  u = v"
  for u :: "'a::len word"
  by (simp add: word_size word_eq_iff)

lemma word_eqD: "u = v  u !! x = v !! x"
  for u v :: "'a::len word"
  by simp

lemma test_bit_bin': "w !! n  n < size w  bit (uint w) n"
  by transfer (simp add: bit_take_bit_iff)

lemmas test_bit_bin = test_bit_bin' [unfolded word_size]

lemma word_test_bit_def:
  ‹test_bit a = bit (uint a)
  by transfer (simp add: fun_eq_iff bit_take_bit_iff)

lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]

lemma word_test_bit_transfer [transfer_rule]:
  "(rel_fun pcr_word (rel_fun (=) (=)))
    (λx n. n < LENGTH('a)  bit x n) (test_bit :: 'a::len word  _)"
  by (simp only: test_bit_eq_bit) transfer_prover

lemma test_bit_wi [simp]:
  "(word_of_int x :: 'a::len word) !! n  n < LENGTH('a)  bit x n"
  by transfer simp

lemma word_ops_nth_size:
  "n < size x 
    (x OR y) !! n = (x !! n | y !! n) 
    (x AND y) !! n = (x !! n  y !! n) 
    (x XOR y) !! n = (x !! n  y !! n) 
    (NOT x) !! n = (¬ x !! n)"
  for x :: "'a::len word"
  by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff)

lemma word_ao_nth:
  "(x OR y) !! n = (x !! n | y !! n) 
    (x AND y) !! n = (x !! n  y !! n)"
  for x :: "'a::len word"
  by transfer (auto simp add: bit_or_iff bit_and_iff)

lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
lemmas msb1 = msb0 [where i = 0]

lemma test_bit_numeral [simp]:
  "(numeral w :: 'a::len word) !! n 
    n < LENGTH('a)  bit (numeral w :: int) n"
  by transfer (rule refl)

lemma test_bit_neg_numeral [simp]:
  "(- numeral w :: 'a::len word) !! n 
    n < LENGTH('a)  bit (- numeral w :: int) n"
  by transfer (rule refl)

lemma test_bit_1 [iff]: "(1 :: 'a::len word) !! n  n = 0"
  by transfer (auto simp add: bit_1_iff)

lemma nth_0 [simp]: "¬ (0 :: 'a::len word) !! n"
  by transfer simp

lemma nth_minus1 [simp]: "(-1 :: 'a::len word) !! n  n < LENGTH('a)"
  by transfer simp

lemma shiftl1_code [code]:
  ‹shiftl1 w = push_bit 1 w
  by transfer (simp add: ac_simps)

lemma uint_shiftr_eq:
  ‹uint (w >> n) = uint w div 2 ^ n
  by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv)

lemma shiftr1_code [code]:
  ‹shiftr1 w = drop_bit 1 w
  by transfer (simp add: drop_bit_Suc)

lemma shiftl_def:
  w << n = (shiftl1 ^^ n) w
proof -
  have ‹push_bit n = (((*) 2 ^^ n) :: int  int) for n
    by (induction n) (simp_all add: fun_eq_iff funpow_swap1, simp add: ac_simps)
  then show ?thesis
    by transfer simp
qed

lemma shiftr_def:
  w >> n = (shiftr1 ^^ n) w
proof -
  have ‹shiftr1 ^^ n = (drop_bit n :: 'a word  'a word)
    apply (induction n)
    apply simp
    apply (simp only: shiftr1_eq_div_2 [abs_def] drop_bit_eq_div [abs_def] funpow_Suc_right)
    apply (use div_exp_eq [of _ 1, where ?'a = 'a word›] in simp)
    done
  then show ?thesis
    by (simp add: shiftr_eq_drop_bit)
qed

lemma bit_shiftl_word_iff [bit_simps]:
  ‹bit (w << m) n  m  n  n < LENGTH('a)  bit w (n - m)
  for w :: 'a::len word›
  by (simp add: shiftl_word_eq bit_push_bit_iff not_le)

lemma bit_shiftr_word_iff [bit_simps]:
  ‹bit (w >> m) n  bit w (m + n)
  for w :: 'a::len word›
  by (simp add: shiftr_word_eq bit_drop_bit_eq)

lift_definition sshiftr :: 'a::len word  nat  'a word›  (infixl >>> 55)
  is λk n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))
  by (simp flip: signed_take_bit_decr_length_iff)

lemma sshiftr_eq [code]:
  w >>> n = signed_drop_bit n w
  by transfer simp

lemma sshiftr_eq_funpow_sshiftr1:
  w >>> n = (sshiftr1 ^^ n) w
  apply (rule sym)
  apply (simp add: sshiftr1_eq_signed_drop_bit_Suc_0 sshiftr_eq)
  apply (induction n)
   apply simp_all
  done

lemma uint_sshiftr_eq:
  ‹uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^  n)
  for w :: 'a::len word›
  by transfer (simp flip: drop_bit_eq_div)

lemma sshift1_code [code]:
  ‹sshiftr1 w = signed_drop_bit 1 w
  by transfer (simp add: drop_bit_Suc)

lemma sshiftr_0 [simp]: "0 >>> n = 0"
  by transfer simp

lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
  by transfer simp

lemma bit_sshiftr_word_iff [bit_simps]:
  ‹bit (w >>> m) n  bit w (if LENGTH('a) - m  n  n < LENGTH('a) then LENGTH('a) - 1 else (m + n))
  for w :: 'a::len word›
  apply transfer
  apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le simp flip: bit_Suc)
  using le_less_Suc_eq apply fastforce
  using le_less_Suc_eq apply fastforce
  done

lemma nth_sshiftr :
  "(w >>> m) !! n =
    (n < size w  (if n + m  size w then w !! (size w - 1) else w !! (n + m)))"
  apply transfer
  apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le ac_simps)
  using le_less_Suc_eq apply fastforce
  using le_less_Suc_eq apply fastforce
  done

lemma sshiftr_numeral [simp]:
  (numeral k >>> numeral n :: 'a::len word) =
    word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k)))
  apply (rule word_eqI)
  apply (cases LENGTH('a))
   apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps)
  done

setup ‹
  Context.theory_map (fold SMT_Word.add_word_shift' [
    (term‹shiftl :: 'a::len word  _, "bvshl"),
    (term‹shiftr :: 'a::len word  _, "bvlshr"),
    (term‹sshiftr :: 'a::len word  _, "bvashr")
  ])

lemma revcast_down_us [OF refl]:
  "rc = revcast  source_size rc = target_size rc + n  rc w = ucast (w >>> n)"
  for w :: "'a::len word"
  apply (simp add: source_size_def target_size_def)
  apply (rule bit_word_eqI)
  apply (simp add: bit_revcast_iff bit_ucast_iff bit_sshiftr_word_iff ac_simps)
  done

lemma revcast_down_ss [OF refl]:
  "rc = revcast  source_size rc = target_size rc + n  rc w = scast (w >>> n)"
  for w :: "'a::len word"
  apply (simp add: source_size_def target_size_def)
  apply (rule bit_word_eqI)
  apply (simp add: bit_revcast_iff bit_word_scast_iff bit_sshiftr_word_iff ac_simps)
  done

lemma sshiftr_div_2n: "sint (w >>> n) = sint w div 2 ^ n"
  using sint_signed_drop_bit_eq [of n w]
  by (simp add: drop_bit_eq_div sshiftr_eq)

lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]

lemma nth_sint:
  fixes w :: "'a::len word"
  defines "l  LENGTH('a)"
  shows "bit (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  unfolding sint_uint l_def
  by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def)

lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m  m = n  m < LENGTH('a)"
  by transfer (auto simp add: bit_exp_iff)

lemma nth_w2p: "((2::'a::len word) ^ n) !! m  m = n  m < LENGTH('a::len)"
  by transfer (auto simp add: bit_exp_iff)

lemma bang_is_le: "x !! m  2 ^ m  x"
  for x :: "'a::len word"
  apply (rule xtrans(3))
   apply (rule_tac [2] y = "x" in le_word_or2)
  apply (rule word_eqI)
  apply (auto simp add: word_ao_nth nth_w2p word_size)
  done

lemma mask_eq:
  ‹mask n = (1 << n) - (1 :: 'a::len word)
  by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1)

lemma nth_ucast:
  "(ucast w::'a::len word) !! n = (w !! n  n < LENGTH('a))"
  by transfer (simp add: bit_take_bit_iff ac_simps)

lemma shiftl_0 [simp]: "(0::'a::len word) << n = 0"
  by transfer simp

lemma shiftr_0 [simp]: "(0::'a::len word) >> n = 0"
  by transfer simp

lemma nth_shiftl1: "shiftl1 w !! n  n < size w  n > 0  w !! (n - 1)"
  by transfer (auto simp add: bit_double_iff)

lemma nth_shiftl': "(w << m) !! n  n < size w  n >= m  w !! (n - m)"
  for w :: "'a::len word"
  by transfer (auto simp add: bit_push_bit_iff)

lemmas nth_shiftl = nth_shiftl' [unfolded word_size]

lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
  by transfer (auto simp add: bit_take_bit_iff simp flip: bit_Suc)

lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
  for w :: "'a::len word"
  apply (unfold shiftr_def)
  apply (induct "m" arbitrary: n)
   apply (auto simp add: nth_shiftr1)
  done

lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  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

lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  by (fact uint_shiftr_eq)

lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)

lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  by (simp add: shiftl_rev)

lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
  by (simp add: rev_shiftl)

lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  by (simp add: shiftr_rev)

lemma shiftl_numeral [simp]:
  ‹numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)
  by (fact shiftl_word_eq)

lemma shiftl_zero_size: "size x  n  x << n = 0"
  for x :: "'a::len word"
  apply transfer
  apply (simp add: take_bit_push_bit)
  done

lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
  for w :: "'a::len word"
  by (induct n) (auto simp: shiftl_def shiftl1_2t)

lemma shiftr_numeral [simp]:
  (numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)
  by (fact shiftr_word_eq)

lemma shiftr_numeral_Suc [simp]:
  (numeral k >> Suc 0 :: 'a::len word) = drop_bit (Suc 0) (numeral k)
  by (fact shiftr_word_eq)

lemma drop_bit_numeral_bit0_1 [simp]:
  ‹drop_bit (Suc 0) (numeral k) =
    (word_of_int (drop_bit (Suc 0) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)
  by (metis Word_eq_word_of_int drop_bit_word.abs_eq of_int_numeral)

lemma nth_mask [simp]:
  (mask n :: 'a::len word) !! i  i < n  i < size (mask n :: 'a word)
  by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff)

lemma slice_shiftr: "slice n w = ucast (w >> n)"
  apply (rule bit_word_eqI)
  apply (cases n  LENGTH('b))
   apply (auto simp add: bit_slice_iff bit_ucast_iff bit_shiftr_word_iff ac_simps
    dest: bit_imp_le_length)
  done

lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n)  m < LENGTH('a))"
  by (simp add: slice_shiftr nth_ucast nth_shiftr)

lemma revcast_down_uu [OF refl]:
  "rc = revcast  source_size rc = target_size rc + n  rc w = ucast (w >> n)"
  for w :: "'a::len word"
  apply (simp add: source_size_def target_size_def)
  apply (rule bit_word_eqI)
  apply (simp add: bit_revcast_iff bit_ucast_iff bit_shiftr_word_iff ac_simps)
  done

lemma revcast_down_su [OF refl]:
  "rc = revcast  source_size rc = target_size rc + n  rc w = scast (w >> n)"
  for w :: "'a::len word"
  apply (simp add: source_size_def target_size_def)
  apply (rule bit_word_eqI)
  apply (simp add: bit_revcast_iff bit_word_scast_iff bit_shiftr_word_iff ac_simps)
  done

lemma cast_down_rev [OF refl]:
  "uc = ucast  source_size uc = target_size uc + n  uc w = revcast (w << n)"
  for w :: "'a::len word"
  apply (simp add: source_size_def target_size_def)
  apply (rule bit_word_eqI)
  apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
  done

lemma revcast_up [OF refl]:
  "rc = revcast  source_size rc + n = target_size rc 
    rc w = (ucast w :: 'a::len word) << n"
  apply (simp add: source_size_def target_size_def)
  apply (rule bit_word_eqI)
  apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
  apply auto
  apply (metis add.commute add_diff_cancel_right)
  apply (metis diff_add_inverse2 diff_diff_add)
  done

lemmas rc1 = revcast_up [THEN
  revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
lemmas rc2 = revcast_down_uu [THEN
  revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]

lemmas ucast_up =
  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
lemmas ucast_down =
  rc2 [simplified rev_shiftr revcast_ucast [symmetric]]

― ‹problem posed by TPHOLs referee:
      criterion for overflow of addition of signed integers›

lemma sofl_test:
  ‹sint x + sint y = sint (x + y) 
    (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0
  for x y :: 'a::len word›
proof -
  obtain n where n: LENGTH('a) = Suc n
    by (cases LENGTH('a)) simp_all
  have *: ‹sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y)  sint x + sint y  - (2 ^ n)
    ‹signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n  2 ^ n > sint x + sint y
    using signed_take_bit_int_greater_eq [of ‹sint x + sint y n] signed_take_bit_int_less_eq [of n ‹sint x + sint y]
    by (auto intro: ccontr)
  have ‹sint x + sint y = sint (x + y) 
    (sint (x + y) < 0  sint x < 0) 
    (sint (x + y) < 0  sint y < 0)
    using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y]
    signed_take_bit_int_eq_self [of LENGTH('a) - 1 ‹sint x + sint y]
    apply (auto simp add: not_less)
       apply (unfold sint_word_ariths)
       apply (subst signed_take_bit_int_eq_self)
         prefer 4
         apply (subst signed_take_bit_int_eq_self)
           prefer 7
           apply (subst signed_take_bit_int_eq_self)
             prefer 10
             apply (subst signed_take_bit_int_eq_self)
               apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
       apply (smt (z3) take_bit_nonnegative)
      apply (smt (z3) take_bit_int_less_exp)
     apply (smt (z3) take_bit_nonnegative)
    apply (smt (z3) take_bit_int_less_exp)
    done
  then show ?thesis
    apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
    apply (simp add: bit_last_iff)
    done
qed

lemma shiftr_zero_size: "size x  n  x >> n = 0"
  for x :: "'a :: len word"
  by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size)

lemma test_bit_cat [OF refl]:
  "wc = word_cat a b  wc !! n = (n < size wc 
    (if n < size b then b !! n else a !! (n - size b)))"
  apply (simp add: word_size not_less; transfer)
       apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)
  done

― ‹keep quantifiers for use in simplification›
lemma test_bit_split':
  "word_split c = (a, b) 
    (n m.
      b !! n = (n < size b  c !! n) 
      a !! m = (m < size a  c !! (m + size b)))"
  by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size bit_drop_bit_eq ac_simps
           dest: bit_imp_le_length)

lemma test_bit_split:
  "word_split c = (a, b) 
    (n::nat. b !! n  n < size b  c !! n) 
    (m::nat. a !! m  m < size a  c !! (m + size b))"
  by (simp add: test_bit_split')

lemma test_bit_split_eq:
  "word_split c = (a, b) 
    ((n::nat. b !! n = (n < size b  c !! n)) 
     (m::nat. a !! m = (m < size a  c !! (m + size b))))"
  apply (rule_tac iffI)
   apply (rule_tac conjI)
    apply (erule test_bit_split [THEN conjunct1])
   apply (erule test_bit_split [THEN conjunct2])
  apply (case_tac "word_split c")
  apply (frule test_bit_split)
  apply (erule trans)
  apply (fastforce intro!: word_eqI simp add: word_size)
  done

lemma test_bit_rcat:
  "sw = size (hd wl)  rc = word_rcat wl  rc !! n =
    (n < size rc  n div sw < size wl  (rev wl) ! (n div sw) !! (n mod sw))"
  for wl :: "'a::len word list"
  by (simp add: word_size word_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
    (simp add: test_bit_eq_bit)

lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]

lemma max_test_bit: "(max_word::'a::len word) !! n  n < LENGTH('a)"
  by (fact nth_minus1)

lemma shiftr_x_0 [iff]: "x >> 0 = x"
  for x :: "'a::len word"
  by transfer simp

lemma shiftl_x_0 [simp]: "x << 0 = x"
  for x :: "'a::len word"
  by (simp add: shiftl_t2n)

lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
  by (simp add: shiftl_t2n)

lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
  by (induct n) (auto simp: shiftr_def)

lemma map_nth_0 [simp]: "map ((!!) (0::'a::len word)) xs = replicate (length xs) False"
  by (induct xs) auto

lemma word_and_1:
  "n AND 1 = (if n !! 0 then 1 else 0)" for n :: "_ word"
  by (rule bit_word_eqI) (auto simp add: bit_and_iff test_bit_eq_bit bit_1_iff intro: gr0I)

lemma test_bit_1' [simp]:
  "(1 :: 'a :: len word) !! n  0 < LENGTH('a)  n = 0"
  by simp

lemma shiftl0:
  "x << 0 = (x :: 'a :: len word)"
  by (fact shiftl_x_0)

lemma word_ops_nth [simp]:
  fixes x y :: 'a::len word›
  shows
  word_or_nth:  "(x OR y) !! n = (x !! n  y !! n)" and
  word_and_nth: "(x AND y) !! n = (x !! n  y !! n)" and
  word_xor_nth: "(x XOR y) !! n = (x !! n  y !! n)"
  by ((cases "n < size x",
      auto dest: test_bit_size simp: word_ops_nth_size word_size)[1])+

lemma and_not_mask:
  "w AND NOT (mask n) = (w >> n) << n"
  for w :: 'a::len word›
  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 :: 'a::len word›
  apply (rule word_eqI)
  apply (simp add : word_ops_nth_size word_size)
  apply (simp add : nth_shiftr nth_shiftl)
  by auto

lemma nth_w2p_same:
  "(2^n :: 'a :: len word) !! n = (n < LENGTH('a))"
  by (simp add : nth_w2p)

lemma shiftr_div_2n_w: "n < size w  w >> n = w div (2^n :: 'a :: len word)"
  apply (unfold word_div_def)
  apply (simp add: uint_2p_alt word_size)
  apply (metis uint_shiftr_eq word_of_int_uint)
  done

lemma le_shiftr:
  "u  v  u >> (n :: nat)  (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  mask n >> m = (0 :: 'a::len word)"
  apply (rule word_eqI)
  apply (simp add: word_size nth_shiftr)
  done

lemma shiftr_mask [simp]:
  ‹mask m >> m = (0::'a::len word)
  by (rule shiftr_mask_le) simp

lemma word_leI:
  "(n.  n < size (u::'a::len word); u !! n   (v::'a::len word) !! n)  u <= v"
  apply (rule xtrans(4))
   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  mask n) = (w >> n = 0)"
  for w :: 'a::len word›
  apply safe
   apply (rule word_le_0_iff [THEN iffD1])
   apply (rule xtrans(3))
    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 :: 'a::len word›
  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 transfer
  apply (auto simp add: fun_eq_iff bit_simps)
  apply (metis add_diff_inverse_nat)
  done

lemma mask_shiftl_decompose:
  "mask m << n = mask (m + n) AND NOT (mask n :: 'a::len word)"
  by (auto intro!: word_eqI simp: and_not_mask nth_shiftl nth_shiftr word_size)

lemma bang_eq:
  fixes x :: "'a::len word"
  shows "(x = y) = (n. x !! n = y !! n)"
  by (subst test_bit_eq_iff[symmetric]) fastforce

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  b  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  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  b  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  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 shiftr_mask2:
  "n  LENGTH('a)  (mask n >> m :: ('a :: len) word) = mask (n - m)"
  apply (rule word_eqI)
  apply (simp add: nth_shiftr word_size)
  apply arith
  done

lemma word_shiftl_add_distrib:
  fixes x :: "'a :: len word"
  shows "(x + y) << n = (x << n) + (y << n)"
  by (simp add: shiftl_t2n ring_distribs)

lemma mask_shift:
  "(x AND NOT (mask y)) >> y = x >> y"
  for x :: 'a::len word›
  apply (rule bit_eqI)
  apply (simp add: bit_and_iff bit_not_iff bit_shiftr_word_iff bit_mask_iff not_le)
  using bit_imp_le_length apply auto
  done

lemma shiftr_div_2n':
  "unat (w >> n) = unat w div 2 ^ n"
  apply (unfold unat_eq_nat_uint)
  apply (subst shiftr_div_2n)
  apply (subst nat_div_distrib)
   apply simp
  apply (simp add: nat_power_eq)
  done

lemma shiftl_shiftr_id:
  assumes nv: "n < LENGTH('a)"
  and     xv: "x < 2 ^ (LENGTH('a) - n)"
  shows "x << n >> n = (x::'a::len word)"
  apply (simp add: shiftl_t2n)
  apply (rule word_eq_unatI)
  apply (subst shiftr_div_2n')
  apply (cases n)
   apply simp
  apply (subst iffD1 [OF unat_mult_lem])+
   apply (subst unat_power_lower[OF nv])
   apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]])
   apply (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl])
   apply (rule unat_power_lower)
   apply simp
  apply (subst unat_power_lower[OF nv])
  apply simp
  done

lemma ucast_shiftl_eq_0:
  fixes w :: "'a :: len word"
  shows " n  LENGTH('b)   ucast (w << n) = (0 :: 'b :: len word)"
  by transfer (simp add: take_bit_push_bit)

lemma word_shift_nonzero:
  " (x::'a::len word)  2 ^ m; m + n < LENGTH('a::len); x  0
    x << n  0"
  apply (simp only: word_neq_0_conv word_less_nat_alt
                    shiftl_t2n mod_0 unat_word_ariths
                    unat_power_lower word_le_nat_alt)
  apply (subst mod_less)
   apply (rule order_le_less_trans)
    apply (erule mult_le_mono2)
   apply (subst power_add[symmetric])
   apply (rule power_strict_increasing)
    apply simp
   apply simp
  apply simp
  done

lemma word_shiftr_lt:
  fixes w :: "'a::len word"
  shows "unat (w >> n) < (2 ^ (LENGTH('a) - n))"
  apply (subst shiftr_div_2n')
  apply transfer
  apply (simp flip: drop_bit_eq_div add: drop_bit_nat_eq drop_bit_take_bit)
  done

lemma neg_mask_test_bit:
  "(NOT(mask n) :: 'a :: len word) !! m = (n  m  m < LENGTH('a))"
  by (metis not_le nth_mask test_bit_bin word_ops_nth_size word_size)

lemma upper_bits_unset_is_l2p:
  (n'  n. n' < LENGTH('a)  ¬ p !! n')  (p < 2 ^ n) (is ?P  ?Q)
    if n < LENGTH('a)
    for p :: "'a :: len word"
proof
  assume ?Q
  then show ?P
    by (meson bang_is_le le_less_trans not_le word_power_increasing)
next
  assume ?P
  have ‹take_bit n p = p
  proof (rule bit_word_eqI)
    fix q
    assume q < LENGTH('a)
    show ‹bit (take_bit n p) q  bit p q
    proof (cases q < n)
      case True
      then show ?thesis
        by (auto simp add: bit_simps)
    next
      case False
      then have n  q
        by simp
      with ?P q < LENGTH('a) have ¬ bit p q
        by (simp add: test_bit_eq_bit)
      then show ?thesis
        by (simp add: bit_simps)
    qed
  qed
  with that show ?Q
    using take_bit_word_eq_self_iff [of n p] by auto
qed

lemma less_2p_is_upper_bits_unset:
  "p < 2 ^ n  n < LENGTH('a)  (n'  n. n' < LENGTH('a)  ¬ p !! n')" for p :: "'a :: len word"
  by (meson le_less_trans le_mask_iff_lt_2n upper_bits_unset_is_l2p word_zero_le)

lemma test_bit_over:
  "n  size (x::'a::len word)  (x !! n) = False"
  by transfer auto

lemma le_mask_high_bits:
  "w  mask n  (i  {n ..< size w}. ¬ w !! i)"
  for w :: 'a::len word›
  by (auto simp: word_size and_mask_eq_iff_le_mask[symmetric] word_eq_iff)

lemma test_bit_conj_lt:
  "(x !! m  m < LENGTH('a)) = x !! m" for x :: "'a :: len word"
  using test_bit_bin by blast

lemma neg_test_bit:
  "(NOT x) !! n = (¬ x !! n  n < LENGTH('a))" for x :: "'a::len word"
  by (cases "n < LENGTH('a)") (auto simp add: test_bit_over word_ops_nth_size word_size)

lemma shiftr_less_t2n':
  " x AND mask (n + m) = x; m < LENGTH('a)   x >> n < 2 ^ m" for x :: "'a :: len word"
  apply (simp add: word_size mask_eq_iff_w2p [symmetric] flip: take_bit_eq_mask)
  apply transfer
  apply (simp add: take_bit_drop_bit ac_simps)
  done

lemma shiftr_less_t2n:
  "x < 2 ^ (n + m)  x >> n < 2 ^ m" for x :: "'a :: len word"
  apply (rule shiftr_less_t2n')
   apply (erule less_mask_eq)
  apply (rule ccontr)
  apply (simp add: not_less)
  apply (subst (asm) p2_eq_0[symmetric])
  apply (simp add: power_add)
  done

lemma shiftr_eq_0:
  "n  LENGTH('a)  ((w::'a::len word) >> n) = 0"
  apply (cut_tac shiftr_less_t2n'[of w n 0], simp)
   apply (simp add: mask_eq_iff)
  apply (simp add: lt2p_lem)
  apply simp
  done

lemma shiftr_not_mask_0:
  "n+m  LENGTH('a :: len)  ((w::'a::len word) >> n) AND NOT (mask m) = 0"
  by (rule bit_word_eqI) (auto simp add: bit_simps dest: bit_imp_le_length)

lemma shiftl_less_t2n:
  fixes x :: "'a :: len word"
  shows " x < (2 ^ (m - n)); m < LENGTH('a)   (x << n) < 2 ^ m"
  apply (simp add: word_size mask_eq_iff_w2p [symmetric] flip: take_bit_eq_mask)
  apply transfer
  apply (simp add: take_bit_push_bit)
  done

lemma shiftl_less_t2n':
  "(x::'a::len word) < 2 ^ m  m+n < LENGTH('a)  x << n < 2 ^ (m + n)"
  by (rule shiftl_less_t2n) simp_all

lemma nth_w2p_scast [simp]:
  "((scast ((2::'a::len signed word) ^ n) :: 'a word) !! m)
          ((((2::'a::len  word) ^ n) :: 'a word) !! m)"
  by transfer (auto simp add: bit_simps)

lemma scast_bit_test [simp]:
    "scast ((1 :: 'a::len signed word) << n) = (1 :: 'a word) << n"
  by (clarsimp simp: word_eq_iff)

lemma signed_shift_guard_to_word:
  " n < len_of TYPE ('a); n > 0 
     (unat (x :: 'a :: len word) * 2 ^ y < 2 ^ n)
    = (x = 0  x < (1 << n >> y))"
  apply (simp only: nat_mult_power_less_eq)
  apply (cases "y  n")
   apply (simp only: shiftl_shiftr1)
   apply (subst less_mask_eq)
    apply (simp add: word_less_nat_alt word_size)
    apply (rule order_less_le_trans[rotated], rule power_increasing[where n=1])
      apply simp
     apply simp
    apply simp
   apply (simp add: nat_mult_power_less_eq word_less_nat_alt word_size)
   apply auto[1]
  apply (simp only: shiftl_shiftr2, simp add: unat_eq_0)
  done

lemma nth_bounded:
  "(x :: 'a :: len word) !! n; x < 2 ^ m; m  len_of TYPE ('a)  n < m"
  apply (rule ccontr)
  apply (auto simp add: not_less test_bit_word_eq)
  apply (meson bit_imp_le_length bit_uint_iff less_2p_is_upper_bits_unset test_bit_bin)
  done

lemma shiftl_mask_is_0[simp]:
  "(x << n) AND mask n = 0"
  for x :: 'a::len word›
  by (simp flip: take_bit_eq_mask add: shiftl_eq_push_bit take_bit_push_bit)

lemma rshift_sub_mask_eq:
  "(a >> (size a - b)) AND mask b = a >> (size a - b)"
  for a :: 'a::len word›
  using shiftl_shiftr2[where a=a and b=0 and c="size a - b"]
  apply (cases "b < size a")
   apply simp
  apply (simp add: linorder_not_less mask_eq_decr_exp word_size
                   p2_eq_0[THEN iffD2])
  done

lemma shiftl_shiftr3:
  "b  c  a << b >> c = (a >> c - b) AND mask (size a - c)"
  for a :: 'a::len word›
  apply (cases "b = c")
   apply (simp add: shiftl_shiftr1)
  apply (simp add: shiftl_shiftr2)
  done

lemma and_mask_shiftr_comm:
  "m  size w  (w AND mask m) >> n = (w >> n) AND mask (m-n)"
  for w :: 'a::len word›
  by (simp add: and_mask shiftr_shiftr) (simp add: word_size shiftl_shiftr3)

lemma and_mask_shiftl_comm:
  "m+n  size w  (w AND mask m) << n = (w << n) AND mask (m+n)"
  for w :: 'a::len word›
  by (simp add: and_mask word_size shiftl_shiftl) (simp add: shiftl_shiftr1)

lemma le_mask_shiftl_le_mask: "s = m + n  x  mask n  x << m  mask s"
  for x :: 'a::len word›
  by (simp add: le_mask_iff shiftl_shiftr3)

lemma word_and_1_shiftl:
  "x AND (1 << n) = (if x !! n then (1 << n) else 0)" for x :: "'a :: len word"
  apply (rule bit_word_eqI; transfer)
  apply (auto simp add: bit_simps not_le ac_simps)
  done

lemmas word_and_1_shiftls'
    = word_and_1_shiftl[where n=0]
      word_and_1_shiftl[where n=1]
      word_and_1_shiftl[where n=2]

lemmas word_and_1_shiftls = word_and_1_shiftls' [simplified]

lemma word_and_mask_shiftl:
  "x AND (mask n << m) = ((x >> m) AND mask n) << m"
  for x :: 'a::len word›
  apply (rule bit_word_eqI; transfer)
  apply (auto simp add: bit_simps not_le ac_simps)
  done

lemma shift_times_fold:
  "(x :: 'a :: len word) * (2 ^ n) << m = x << (m + n)"
  by (simp add: shiftl_t2n ac_simps power_add)

lemma of_bool_nth:
  "of_bool (x !! v) = (x >> v) AND 1"
  for x :: 'a::len word›
  by (simp add: test_bit_word_eq shiftr_word_eq bit_eq_iff)
    (auto simp add: bit_1_iff bit_and_iff bit_drop_bit_eq intro: ccontr)

lemma shiftr_mask_eq:
  "(x >> n) AND mask (size x - n) = x >> n" for x :: "'a :: len word"
  apply (simp flip: take_bit_eq_mask)
  apply transfer
  apply (simp add: take_bit_drop_bit)
  done

lemma shiftr_mask_eq':
  "m = (size x - n)  (x >> n) AND mask m = x >> n" for x :: "'a :: len word"
  by (simp add: shiftr_mask_eq)

lemma and_eq_0_is_nth:
  fixes x :: "'a :: len word"
  shows "y = 1 << n  ((x AND y) = 0) = (¬ (x !! n))"
  apply safe
   apply (drule_tac u="(x AND (1 << n))" and x=n in word_eqD)
   apply (simp add: nth_w2p)
   apply (simp add: test_bit_bin)
  apply (rule bit_word_eqI)
  apply (auto simp add: bit_simps test_bit_eq_bit)
  done

lemma and_neq_0_is_nth:
  x AND y  0  x !! n if y = 2 ^ n for x y :: 'a::len word›
  apply (simp add: bit_eq_iff bit_simps)
  using that apply (simp add: bit_simps not_le)
  apply transfer
  apply auto
  done

lemma nth_is_and_neq_0:
  "(x::'a::len word) !! n = (x AND 2 ^ n  0)"
  by (subst and_neq_0_is_nth; rule refl)

lemma word_shift_zero:
  " x << n = 0; x  2^m; m + n < LENGTH('a)  (x::'a::len word) = 0"
  apply (rule ccontr)
  apply (drule (2) word_shift_nonzero)
  apply simp
  done

lemma mask_shift_and_negate[simp]:"(w AND mask n << m) AND NOT (mask n << m) = 0"
  for w :: 'a::len word›
  by (clarsimp simp add: mask_eq_decr_exp Parity.bit_eq_iff bit_and_iff bit_not_iff shiftl_word_eq bit_push_bit_iff)

end

Theory Word_EqI

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Solving Word Equalities"

theory Word_EqI
  imports
    More_Word
    Traditional_Infix_Syntax
    "HOL-Eisbach.Eisbach_Tools"
begin

text ‹
  Some word equalities can be solved by considering the problem bitwise for all
  @{prop "n < LENGTH('a::len)"}, which is different to running @{text word_bitwise}
  and expanding into an explicit list of bits.
›

named_theorems word_eqI_simps

lemmas [word_eqI_simps] =
  word_ops_nth_size
  word_size
  word_or_zero
  neg_mask_test_bit
  nth_ucast
  nth_w2p nth_shiftl
  nth_shiftr
  less_2p_is_upper_bits_unset
  le_mask_high_bits
  bang_eq
  neg_test_bit
  is_up
  is_down

lemmas word_eqI_rule = word_eqI [rule_format]

lemma test_bit_lenD:
  "x !! n  n < LENGTH('a)  x !! n" for x :: "'a :: len word"
  by (fastforce dest: test_bit_size simp: word_size)

method word_eqI uses simp simp_del split split_del cong flip =
  ((* reduce conclusion to test_bit: *)
   rule word_eqI_rule,
   (* make sure we're in clarsimp normal form: *)
   (clarsimp simp: simp simp del: simp_del simp flip: flip split: split split del: split_del cong: cong)?,
   (* turn x < 2^n assumptions into mask equations: *)
   ((drule less_mask_eq)+)?,
   (* expand and distribute test_bit everywhere: *)
   (clarsimp simp: word_eqI_simps simp simp del: simp_del simp flip: flip
             split: split split del: split_del cong: cong)?,
   (* add any additional word size constraints to new indices: *)
   ((drule test_bit_lenD)+)?,
   (* try to make progress (can't use +, would loop): *)
   (clarsimp simp: word_eqI_simps simp simp del: simp_del simp flip: flip
             split: split split del: split_del cong: cong)?,
   (* helps sometimes, rarely: *)
   (simp add: simp test_bit_conj_lt del: simp_del flip: flip split: split split del: split_del cong: cong)?)

method word_eqI_solve uses simp simp_del split split_del cong flip =
  solves word_eqI simp: simp simp_del: simp_del split: split split_del: split_del
                   cong: cong simp flip: flip;
          (fastforce dest: test_bit_size simp: word_eqI_simps simp flip: flip
                     simp: simp simp del: simp_del split: split split del: split_del cong: cong)?

end

Theory Bit_Comprehension

(*
 * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Comprehension syntax for bit expressions›

theory Bit_Comprehension
  imports "HOL-Library.Word"
begin

class bit_comprehension = ring_bit_operations +
  fixes set_bits :: (nat  bool)  'a  (binder BITS 10)
  assumes set_bits_bit_eq: set_bits (bit a) = a
begin

lemma set_bits_False_eq [simp]:
  (BITS _. False) = 0
  using set_bits_bit_eq [of 0] by (simp add: bot_fun_def)

end

instantiation int :: bit_comprehension
begin

definition
  ‹set_bits f = (
      if n. mn. f m = f n then
      let n = LEAST n. mn. f m = f n
      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<Suc n]))
     else 0 :: int)

instance proof
  fix k :: int
  from int_bit_bound [of k]
  obtain n where *: m. n  m  bit k m  bit k n
    and **: n > 0  bit k (n - 1)  bit k n
    by blast
  then have ***: n. n'n. bit k n'  bit k n
    by meson
  have l: (LEAST q. mq. bit k m  bit k q) = n
    apply (rule Least_equality)
    using * apply blast
    apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq)
    done
  show ‹set_bits (bit k) = k
    apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l)
    apply simp
    apply (rule bit_eqI)
    apply (simp add: bit_signed_take_bit_iff min_def)
    apply (auto simp add: not_le bit_take_bit_iff dest: *<