kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas

lemma ucast_less_shiftl_helper:
  "\<lbrakk> LENGTH('b) + 2 < LENGTH('a); 2 ^ (LENGTH('b) + 2) \<le> n\<rbrakk>
    \<Longrightarrow> (ucast (x :: 'b::len word) << 2) < (n :: 'a::len word)" apply (erule order_less_le_trans[rotated]) using ucast_less[where x=x and 'a='a] apply (simp only: shiftl_t2n field_simps) apply (rule word_less_power_trans2; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) + 2 < LENGTH('a); 2 ^ (LENGTH('b) + 2) \<le> n\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'a) x << 2 < n proof (prove)
goal (1 subgoal):
 1. LENGTH('b) + 2 < LENGTH('a) \<Longrightarrow> UCAST('b \<rightarrow> 'a) x << 2 < 2 ^ (LENGTH('b) + 2) proof (prove)
using this:
LENGTH('b) < LENGTH('a) \<Longrightarrow> UCAST('b \<rightarrow> 'a) x < 2 ^ LENGTH('b)

goal (1 subgoal):
 1. LENGTH('b) + 2 < LENGTH('a) \<Longrightarrow> UCAST('b \<rightarrow> 'a) x << 2 < 2 ^ (LENGTH('b) + 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) + 2 < LENGTH('a); LENGTH('b) < LENGTH('a) \<Longrightarrow> UCAST('b \<rightarrow> 'a) x < 2 ^ LENGTH('b)\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'a) x * 2\<^sup>2 < 2 ^ (LENGTH('b) + 2) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma NOT_mask_shifted_lenword:
  "NOT (mask len << (LENGTH('a) - len) ::'a::len word) = mask (LENGTH('a) - len)" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (mask len << LENGTH('a) - len) = mask (LENGTH('a) - len)
theory Word_Lemmas

lemma shiftr_less:
  "(w::'a::len word) < k \<Longrightarrow> w >> n < k" by (metis div_le_dividend le_less_trans shiftr_div_2n' unat_arith_simps(2))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w < k \<Longrightarrow> w >> n < k
theory Word_Lemmas

lemma word_and_notzeroD:
  "w AND w' \<noteq> 0 \<Longrightarrow> w \<noteq> 0 \<and> w' \<noteq> 0" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w AND w' \<noteq> (0::'a) \<Longrightarrow> w \<noteq> (0::'a) \<and> w' \<noteq> (0::'a)
theory Word_Lemmas

lemma shiftr_le_0:
  "unat (w::'a::len word) < 2 ^ n \<Longrightarrow> w >> n = (0::'a::len word)" by (auto simp add: take_bit_word_eq_self_iff word_less_nat_alt shiftr_def
           simp flip: take_bit_eq_self_iff_drop_bit_eq_0
           intro: ccontr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat w < 2 ^ n \<Longrightarrow> w >> n = 0
theory Word_Lemmas

lemma of_nat_shiftl:
  "(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)" proof - have "(of_nat x::'a word) << n = of_nat (2 ^ n) * of_nat x" using shiftl_t2n by (metis word_unat_power) thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat x << n = word_of_nat (x * 2 ^ n) proof (state)
goal (1 subgoal):
 1. word_of_nat x << n = word_of_nat (x * 2 ^ n) proof (prove)
goal (1 subgoal):
 1. word_of_nat x << n = word_of_nat (2 ^ n) * word_of_nat x proof (prove)
using this:
?w << ?n = 2 ^ ?n * ?w

goal (1 subgoal):
 1. word_of_nat x << n = word_of_nat (2 ^ n) * word_of_nat x proof (state)
this:
word_of_nat x << n = word_of_nat (2 ^ n) * word_of_nat x

goal (1 subgoal):
 1. word_of_nat x << n = word_of_nat (x * 2 ^ n) proof (prove)
using this:
word_of_nat x << n = word_of_nat (2 ^ n) * word_of_nat x

goal (1 subgoal):
 1. word_of_nat x << n = word_of_nat (x * 2 ^ n) proof (state)
this:
word_of_nat x << n = word_of_nat (x * 2 ^ n)

goal:
No subgoals!
theory Word_Lemmas

lemma shiftl_1_not_0:
  "n < LENGTH('a) \<Longrightarrow> (1::'a::len word) << n \<noteq> 0" by (simp add: shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 1 << n \<noteq> 0
theory Word_Lemmas

lemma bitmagic_zeroLast_leq_or1Last:
  "(a::('a::len) word) AND (mask len << x - len) \<le> a OR mask (y - len)" by (meson le_word_or2 order_trans word_and_le2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a AND (mask len << x - len) \<le> a OR mask (y - len)
theory Word_Lemmas

lemma of_nat_eq_signed_scast:
  "(of_nat x = (y :: ('a::len) signed word))
   = (of_nat x = (scast y :: 'a word))" by (metis scast_of_nat scast_scast_id(2))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (word_of_nat x = y) = (word_of_nat x = SCAST('a signed \<rightarrow> 'a) y)
theory Word_Lemmas

lemma word_aligned_add_no_wrap_bounded:
  "\<lbrakk> w + 2^n \<le> x; w + 2^n \<noteq> 0; is_aligned w n \<rbrakk> \<Longrightarrow> (w::'a::len word) < x" by (blast dest: is_aligned_no_overflow le_less_trans word_leq_le_minus_one)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w + 2 ^ n \<le> x; w + 2 ^ n \<noteq> 0; is_aligned w n\<rbrakk> \<Longrightarrow> w < x
theory Word_Lemmas

lemma mask_Suc:
  "mask (Suc n) = (2 :: 'a::len word) ^ n + mask n" by (simp add: mask_eq_decr_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask (Suc n) = 2 ^ n + mask n
theory Word_Lemmas

lemma mask_mono:
  "sz' \<le> sz \<Longrightarrow> mask sz' \<le> (mask sz :: 'a::len word)" by (simp add: le_mask_iff shiftr_mask_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> mask sz' \<le> mask sz
theory Word_Lemmas

lemma aligned_mask_disjoint:
  "\<lbrakk> is_aligned (a :: 'a :: len word) n; b \<le> mask n \<rbrakk> \<Longrightarrow> a AND b = 0" by (metis and_zero_eq is_aligned_mask le_mask_imp_and_mask word_bw_lcs(1))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; b \<le> mask n\<rbrakk> \<Longrightarrow> a AND b = 0
theory Word_Lemmas

lemma word_and_or_mask_aligned:
  "\<lbrakk> is_aligned a n; b \<le> mask n \<rbrakk> \<Longrightarrow> a + b = a OR b" by (simp add: aligned_mask_disjoint word_plus_and_or_coroll)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; b \<le> mask n\<rbrakk> \<Longrightarrow> a + b = a OR b
theory Word_Lemmas

lemma word_and_or_mask_aligned2:
  \<open>is_aligned b n \<Longrightarrow> a \<le> mask n \<Longrightarrow> a + b = a OR b\<close> using word_and_or_mask_aligned [of b n a] by (simp add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned b n; a \<le> mask n\<rbrakk> \<Longrightarrow> a + b = a OR b proof (prove)
using this:
\<lbrakk>is_aligned b n; a \<le> mask n\<rbrakk> \<Longrightarrow> b + a = b OR a

goal (1 subgoal):
 1. \<lbrakk>is_aligned b n; a \<le> mask n\<rbrakk> \<Longrightarrow> a + b = a OR b
theory Word_Lemmas

lemma is_aligned_ucastI:
  "is_aligned w n \<Longrightarrow> is_aligned (ucast w) n" by (simp add: bit_ucast_iff is_aligned_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w n \<Longrightarrow> is_aligned (UCAST('a \<rightarrow> 'b) w) n
theory Word_Lemmas

lemma ucast_le_maskI:
  "a \<le> mask n \<Longrightarrow> UCAST('a::len \<rightarrow> 'b::len) a \<le> mask n" by (metis and_mask_eq_iff_le_mask ucast_and_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> mask n \<Longrightarrow> UCAST('a \<rightarrow> 'b) a \<le> mask n
theory Word_Lemmas

lemma ucast_add_mask_aligned:
  "\<lbrakk> a \<le> mask n; is_aligned b n \<rbrakk> \<Longrightarrow> UCAST ('a::len \<rightarrow> 'b::len) (a + b) = ucast a + ucast b" by (metis add.commute is_aligned_ucastI ucast_le_maskI ucast_or_distrib word_and_or_mask_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> mask n; is_aligned b n\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (a + b) = UCAST('a \<rightarrow> 'b) a + UCAST('a \<rightarrow> 'b) b
theory Word_Lemmas

lemma ucast_shiftl:
  "LENGTH('b) \<le> LENGTH ('a) \<Longrightarrow> UCAST ('a::len \<rightarrow> 'b::len) x << n = ucast (x << n)" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> UCAST('a \<rightarrow> 'b) x << n = UCAST('a \<rightarrow> 'b) (x << n)
theory Word_Lemmas

lemma ucast_leq_mask:
  "LENGTH('a) \<le> n \<Longrightarrow> ucast (x::'a::len word) \<le> mask n" apply (simp add: less_eq_mask_iff_take_bit_eq_self) apply transfer apply (simp add: ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> mask n proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> take_bit n (UCAST('a \<rightarrow> 'b) x) = UCAST('a \<rightarrow> 'b) x proof (prove)
goal (1 subgoal):
 1. \<And>n x. LENGTH('a) \<le> n \<Longrightarrow> take_bit LENGTH('b) (take_bit (min LENGTH('b) n) (take_bit LENGTH('a) x)) = take_bit LENGTH('b) (take_bit LENGTH('a) x) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftl_inj:
  \<open>x = y\<close>
    if \<open>x << n = y << n\<close> \<open>x \<le> mask (LENGTH('a) - n)\<close> \<open>y \<le> mask (LENGTH('a) - n)\<close>
    for x y :: \<open>'a::len word\<close> proof (cases \<open>n < LENGTH('a)\<close>) case False with that show ?thesis by simp next case True moreover from that have \<open>take_bit (LENGTH('a) - n) x = x\<close> \<open>take_bit (LENGTH('a) - n) y = y\<close> by (simp_all add: less_eq_mask_iff_take_bit_eq_self) ultimately show ?thesis using \<open>x << n = y << n\<close> by (metis diff_less gr_implies_not0 linorder_cases linorder_not_le shiftl_shiftr_id shiftl_x_0 take_bit_word_eq_self_iff) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (state)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> x = y
 2. \<not> n < LENGTH('a) \<Longrightarrow> x = y proof (state)
this:
\<not> n < LENGTH('a)

goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> x = y
 2. \<not> n < LENGTH('a) \<Longrightarrow> x = y proof (chain)
picking this:
x << n = y << n
x \<le> mask (LENGTH('a) - n)
y \<le> mask (LENGTH('a) - n)
\<not> n < LENGTH('a) proof (prove)
using this:
x << n = y << n
x \<le> mask (LENGTH('a) - n)
y \<le> mask (LENGTH('a) - n)
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. x = y proof (state)
this:
x = y

goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> x = y proof (state)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> x = y proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> x = y proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> x = y proof (chain)
picking this:
x << n = y << n
x \<le> mask (LENGTH('a) - n)
y \<le> mask (LENGTH('a) - n) proof (prove)
using this:
x << n = y << n
x \<le> mask (LENGTH('a) - n)
y \<le> mask (LENGTH('a) - n)

goal (1 subgoal):
 1. take_bit (LENGTH('a) - n) x = x &&& take_bit (LENGTH('a) - n) y = y proof (state)
this:
take_bit (LENGTH('a) - n) x = x
take_bit (LENGTH('a) - n) y = y

goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> x = y proof (chain)
picking this:
n < LENGTH('a)
take_bit (LENGTH('a) - n) x = x
take_bit (LENGTH('a) - n) y = y proof (prove)
using this:
n < LENGTH('a)
take_bit (LENGTH('a) - n) x = x
take_bit (LENGTH('a) - n) y = y

goal (1 subgoal):
 1. x = y proof (prove)
using this:
n < LENGTH('a)
take_bit (LENGTH('a) - n) x = x
take_bit (LENGTH('a) - n) y = y
x << n = y << n

goal (1 subgoal):
 1. x = y proof (state)
this:
x = y

goal:
No subgoals!
theory Word_Lemmas

lemma word_upto_Nil:
  "y < x \<Longrightarrow> [x .e. y ::'a::len word] = []" by (simp add: upto_enum_red not_le word_less_nat_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y < x \<Longrightarrow> [x .e. y] = []
theory Word_Lemmas

lemma word_enum_decomp_set:
  "[x .e. (y ::'a::len word)] = as @ a # bs \<Longrightarrow> a \<notin> set as" by (metis distinct_append distinct_enum_upto' not_distinct_conv_prefix)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [x .e. y] = as @ a # bs \<Longrightarrow> a \<notin> set as
theory Word_Lemmas

lemma word_enum_decomp:
  assumes "[x .e. (y ::'a::len word)] = as @ a # bs"
  shows "x \<le> a \<and> a \<le> y \<and> a \<notin> set as \<and> (\<forall>z \<in> set as. x \<le> z \<and> z \<le> y)" proof - from assms have "set as \<subseteq> set [x .e. y] \<and> a \<in> set [x .e. y]" by (auto dest: arg_cong[where f=set]) with word_enum_decomp_set[OF assms] show ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> a \<and> a \<le> y \<and> a \<notin> set as \<and> (\<forall>z\<in>set as. x \<le> z \<and> z \<le> y) proof (state)
goal (1 subgoal):
 1. x \<le> a \<and> a \<le> y \<and> a \<notin> set as \<and> (\<forall>z\<in>set as. x \<le> z \<and> z \<le> y) proof (chain)
picking this:
[x .e. y] = as @ a # bs proof (prove)
using this:
[x .e. y] = as @ a # bs

goal (1 subgoal):
 1. set as \<subseteq> set [x .e. y] \<and> a \<in> set [x .e. y] proof (state)
this:
set as \<subseteq> set [x .e. y] \<and> a \<in> set [x .e. y]

goal (1 subgoal):
 1. x \<le> a \<and> a \<le> y \<and> a \<notin> set as \<and> (\<forall>z\<in>set as. x \<le> z \<and> z \<le> y) proof (chain)
picking this:
a \<notin> set as
set as \<subseteq> set [x .e. y] \<and> a \<in> set [x .e. y] proof (prove)
using this:
a \<notin> set as
set as \<subseteq> set [x .e. y] \<and> a \<in> set [x .e. y]

goal (1 subgoal):
 1. x \<le> a \<and> a \<le> y \<and> a \<notin> set as \<and> (\<forall>z\<in>set as. x \<le> z \<and> z \<le> y) proof (state)
this:
x \<le> a \<and> a \<le> y \<and> a \<notin> set as \<and> (\<forall>z\<in>set as. x \<le> z \<and> z \<le> y)

goal:
No subgoals!
theory Word_Lemmas

lemma less_diff_gt0:
  "a < b \<Longrightarrow> (0 :: 'a :: len word) < b - a" by unat_arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> 0 < b - a
theory Word_Lemmas

lemma unat_plus_gt:
  "unat ((a :: 'a :: len word) + b) \<le> unat a + unat b" by (clarsimp simp: unat_plus_if_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (a + b) \<le> unat a + unat b
theory Word_Lemmas

lemma const_less:
  "\<lbrakk> (a :: 'a :: len word) - 1 < b; a \<noteq> b \<rbrakk> \<Longrightarrow> a < b" by (metis less_1_simp word_le_less_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a - 1 < b; a \<noteq> b\<rbrakk> \<Longrightarrow> a < b
theory Word_Lemmas

lemma add_mult_aligned_neg_mask:
  \<open>(x + y * m) AND NOT(mask n) = (x AND NOT(mask n)) + y * m\<close>
  if \<open>m AND (2 ^ n - 1) = 0\<close>
  for x y m :: \<open>'a::len word\<close> by (metis (no_types, opaque_lifting)
            add.assoc add.commute add.right_neutral add_uminus_conv_diff
            mask_eq_decr_exp mask_eqs(2) mask_eqs(6) mult.commute mult_zero_left
            subtract_mask(1) that)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + y * m AND NOT (mask n) = (x AND NOT (mask n)) + y * m
theory Word_Lemmas

lemma unat_of_nat_minus_1:
  "\<lbrakk> n < 2 ^ LENGTH('a); n \<noteq> 0 \<rbrakk> \<Longrightarrow> unat ((of_nat n:: 'a :: len word) - 1) = n - 1" by (simp add: of_nat_diff unat_eq_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ LENGTH('a); n \<noteq> 0\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) = n - 1
theory Word_Lemmas

lemma word_eq_zeroI:
  "a \<le> a - 1 \<Longrightarrow> a = 0" for a :: "'a :: len word" by (simp add: word_must_wrap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> a - 1 \<Longrightarrow> a = 0
theory Word_Lemmas

lemma word_add_format:
  "(-1 :: 'a :: len  word) + b + c = b + (c - 1)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 + b + c = b + (c - 1)
theory Word_Lemmas

lemma upto_enum_word_nth:
  "\<lbrakk> i \<le> j; k \<le> unat (j - i) \<rbrakk> \<Longrightarrow> [i .e. j] ! k = i + of_nat k" apply (clarsimp simp: upto_enum_def nth_append) apply (clarsimp simp: word_le_nat_alt[symmetric]) apply (rule conjI, clarsimp) apply (subst toEnum_of_nat, unat_arith) apply unat_arith apply (clarsimp simp: not_less unat_sub[symmetric]) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; k \<le> unat (j - i)\<rbrakk> \<Longrightarrow> [i .e. j] ! k = i + word_of_nat k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; k \<le> unat (j - i)\<rbrakk> \<Longrightarrow> (k < unat j - unat i \<longrightarrow> (unat i \<le> unat j \<longrightarrow> toEnum (unat i + k) = i + word_of_nat k) \<and> (\<not> unat i \<le> unat j \<longrightarrow> [] ! k = i + word_of_nat k)) \<and> (\<not> k < unat j - unat i \<longrightarrow> (unat i \<le> unat j \<longrightarrow> [j] ! (k + unat i - unat j) = i + word_of_nat k) \<and> (\<not> unat i \<le> unat j \<longrightarrow> [] ! k = i + word_of_nat k)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; k \<le> unat (j - i)\<rbrakk> \<Longrightarrow> (k < unat j - unat i \<longrightarrow> toEnum (unat i + k) = i + word_of_nat k) \<and> (\<not> k < unat j - unat i \<longrightarrow> [j] ! (k + unat i - unat j) = i + word_of_nat k) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<le> j; k \<le> unat (j - i); k < unat j - unat i\<rbrakk> \<Longrightarrow> toEnum (unat i + k) = i + word_of_nat k
 2. \<lbrakk>i \<le> j; k \<le> unat (j - i)\<rbrakk> \<Longrightarrow> \<not> k < unat j - unat i \<longrightarrow> [j] ! (k + unat i - unat j) = i + word_of_nat k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<le> j; k \<le> unat (j - i); k < unat j - unat i\<rbrakk> \<Longrightarrow> word_of_nat (unat i + k) = i + word_of_nat k
 2. \<lbrakk>i \<le> j; k \<le> unat (j - i)\<rbrakk> \<Longrightarrow> \<not> k < unat j - unat i \<longrightarrow> [j] ! (k + unat i - unat j) = i + word_of_nat k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; k \<le> unat (j - i)\<rbrakk> \<Longrightarrow> \<not> k < unat j - unat i \<longrightarrow> [j] ! (k + unat i - unat j) = i + word_of_nat k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; k = unat (j - i)\<rbrakk> \<Longrightarrow> [j] ! (unat (j - i) + unat i - unat j) = j proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma upto_enum_step_nth:
  "\<lbrakk> a \<le> c; n \<le> unat ((c - a) div (b - a)) \<rbrakk>
   \<Longrightarrow> [a, b .e. c] ! n = a + of_nat n * (b - a)" by (clarsimp simp: upto_enum_step_def not_less[symmetric] upto_enum_word_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; n \<le> unat ((c - a) div (b - a))\<rbrakk> \<Longrightarrow> [a , b .e. c] ! n = a + word_of_nat n * (b - a)
theory Word_Lemmas

lemma upto_enum_inc_1_len:
  "a < - 1 \<Longrightarrow> [(0 :: 'a :: len word) .e. 1 + a] = [0 .e. a] @ [1 + a]" apply (simp add: upto_enum_word) apply (subgoal_tac "unat (1+a) = 1 + unat a") apply simp apply (subst unat_plus_simple[THEN iffD1]) apply (metis add.commute no_plus_overflow_neg olen_add_eqv) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < - 1 \<Longrightarrow> [0 .e. 1 + a] = [0 .e. a] @ [1 + a] proof (prove)
goal (1 subgoal):
 1. a < - 1 \<Longrightarrow> map word_of_nat [0..<unat (1 + a)] = map word_of_nat [0..<unat a] @ [a] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a < - 1; unat (1 + a) = 1 + unat a\<rbrakk> \<Longrightarrow> map word_of_nat [0..<unat (1 + a)] = map word_of_nat [0..<unat a] @ [a]
 2. a < - 1 \<Longrightarrow> unat (1 + a) = 1 + unat a proof (prove)
goal (1 subgoal):
 1. a < - 1 \<Longrightarrow> unat (1 + a) = 1 + unat a proof (prove)
goal (2 subgoals):
 1. a < - 1 \<Longrightarrow> 1 \<le> 1 + a
 2. a < - 1 \<Longrightarrow> unat 1 + unat a = 1 + unat a proof (prove)
goal (1 subgoal):
 1. a < - 1 \<Longrightarrow> unat 1 + unat a = 1 + unat a proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma add_right_shift:
  "\<lbrakk> x AND mask n = 0; y AND mask n = 0; x \<le> x + y \<rbrakk>
   \<Longrightarrow> (x + y :: ('a :: len) word) >> n = (x >> n) + (y >> n)" apply (simp add: no_olen_add_nat is_aligned_mask[symmetric]) apply (simp add: unat_arith_simps shiftr_div_2n' split del: if_split) apply (subst if_P) apply (erule order_le_less_trans[rotated]) apply (simp add: add_mono) apply (simp add: shiftr_div_2n' is_aligned_iff_dvd_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND mask n = 0; y AND mask n = 0; x \<le> x + y\<rbrakk> \<Longrightarrow> x + y >> n = (x >> n) + (y >> n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; unat x + unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x + y >> n = (x >> n) + (y >> n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; unat x + unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (unat x + unat y) div 2 ^ n = (if unat x div 2 ^ n + unat y div 2 ^ n < 2 ^ LENGTH('a) then unat (x >> n) + unat (y >> n) else unat (x >> n) + unat (y >> n) - 2 ^ LENGTH('a)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; is_aligned y n; unat x + unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat x div 2 ^ n + unat y div 2 ^ n < 2 ^ LENGTH('a)
 2. \<lbrakk>is_aligned x n; is_aligned y n; unat x + unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (unat x + unat y) div 2 ^ n = unat (x >> n) + unat (y >> n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; is_aligned y n\<rbrakk> \<Longrightarrow> unat x div 2 ^ n + unat y div 2 ^ n \<le> unat x + unat y
 2. \<lbrakk>is_aligned x n; is_aligned y n; unat x + unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (unat x + unat y) div 2 ^ n = unat (x >> n) + unat (y >> n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; unat x + unat y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (unat x + unat y) div 2 ^ n = unat (x >> n) + unat (y >> n) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma and_and_mask_simple:
  "y AND mask n = mask n \<Longrightarrow> (x AND y) AND mask n = x AND mask n" by (simp add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y AND mask n = mask n \<Longrightarrow> (x AND y) AND mask n = x AND mask n
theory Word_Lemmas

lemma and_and_mask_simple_not:
  "y AND mask n = 0 \<Longrightarrow> (x AND y) AND mask n = 0" by (simp add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y AND mask n = (0::'a) \<Longrightarrow> (x AND y) AND mask n = (0::'a)
theory Word_Lemmas

lemma word_and_le':
  "b \<le> c \<Longrightarrow> (a :: 'a :: len word) AND b \<le> c" by (metis word_and_le1 order_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> c \<Longrightarrow> a AND b \<le> c
theory Word_Lemmas

lemma word_and_less':
  "b < c \<Longrightarrow> (a :: 'a :: len word) AND b < c" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b < c \<Longrightarrow> a AND b < c
theory Word_Lemmas

lemma shiftr_w2p:
  "x < LENGTH('a) \<Longrightarrow> 2 ^ x = (2 ^ (LENGTH('a) - 1) >> (LENGTH('a) - 1 - x) :: 'a :: len word)" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < LENGTH('a) \<Longrightarrow> 2 ^ x = 2 ^ (LENGTH('a) - 1) >> LENGTH('a) - 1 - x
theory Word_Lemmas

lemma t2p_shiftr:
  "\<lbrakk> b \<le> a; a < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 :: 'a :: len word) ^ a >> b = 2 ^ (a - b)" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; a < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ a >> b = 2 ^ (a - b)
theory Word_Lemmas

lemma scast_1[simp]:
  "scast (1 :: 'a :: len signed word) = (1 :: 'a word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST('a signed \<rightarrow> 'a) 1 = 1
theory Word_Lemmas

lemma unsigned_uminus1 [simp]:
  \<open>(unsigned (-1::'b::len word)::'c::len word) = mask LENGTH('b)\<close> by (fact unsigned_minus_1_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('b \<rightarrow> 'c) (- 1) = mask LENGTH('b)
theory Word_Lemmas

lemma ucast_ucast_mask_eq:
  "\<lbrakk> UCAST('a::len \<rightarrow> 'b::len) x = y; x AND mask LENGTH('b) = x \<rbrakk> \<Longrightarrow> x = ucast y" by (drule sym) (simp flip: take_bit_eq_mask add: unsigned_ucast_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x = y; x AND mask LENGTH('b) = x\<rbrakk> \<Longrightarrow> x = UCAST('b \<rightarrow> 'a) y