kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas

lemma word_plus_mono_right_split:
  "\<lbrakk> unat ((x :: 'a :: len word) AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a) \<rbrakk>
   \<Longrightarrow> x \<le> x + z" apply (subgoal_tac "(x AND NOT(mask sz)) + (x AND mask sz) \<le> (x AND NOT(mask sz)) + ((x AND mask sz) + z)") apply (simp add:word_plus_and_or_coroll2 field_simps) apply (rule word_plus_mono_right) apply (simp add: less_le_trans no_olen_add_nat) using of_nat_power is_aligned_no_wrap' by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> x + z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a); (x AND NOT (mask sz)) + (x AND mask sz) \<le> (x AND NOT (mask sz)) + ((x AND mask sz) + z)\<rbrakk> \<Longrightarrow> x \<le> x + z
 2. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> (x AND NOT (mask sz)) + (x AND mask sz) \<le> (x AND NOT (mask sz)) + ((x AND mask sz) + z) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> (x AND NOT (mask sz)) + (x AND mask sz) \<le> (x AND NOT (mask sz)) + ((x AND mask sz) + z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND mask sz \<le> (x AND mask sz) + z
 2. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND NOT (mask sz) \<le> (x AND NOT (mask sz)) + ((x AND mask sz) + z) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND NOT (mask sz) \<le> (x AND NOT (mask sz)) + ((x AND mask sz) + z) proof (prove)
using this:
\<lbrakk>?p < 2 ^ ?x; ?x < LENGTH(?'a)\<rbrakk> \<Longrightarrow> word_of_nat ?p < 2 ^ ?x
\<lbrakk>is_aligned ?ptr ?sz; ?off < 2 ^ ?sz\<rbrakk> \<Longrightarrow> ?ptr \<le> ?ptr + ?off

goal (1 subgoal):
 1. \<lbrakk>unat (x AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> x AND NOT (mask sz) \<le> (x AND NOT (mask sz)) + ((x AND mask sz) + z)
theory Word_Lemmas

lemma mul_not_mask_eq_neg_shiftl:
  "NOT(mask n :: 'a::len word) = -1 << n" by (simp add: NOT_mask shiftl_t2n)

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

lemma shiftr_mul_not_mask_eq_and_not_mask:
  "(x >> n) * NOT(mask n) = - (x AND NOT(mask n))"
  for x :: \<open>'a::len word\<close> by (metis NOT_mask and_not_mask mult_minus_left semiring_normalization_rules(7) shiftl_t2n)

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

lemma mask_eq_n1_shiftr:
  "n \<le> LENGTH('a) \<Longrightarrow> (mask n :: 'a :: len word) = -1 >> (LENGTH('a) - n)" by (metis diff_diff_cancel eq_refl mask_full shiftr_mask2)

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

lemma is_aligned_mask_out_add_eq:
  "is_aligned p n \<Longrightarrow> (p + x) AND NOT(mask n) = p + (x AND NOT(mask n))" by (simp add: mask_out_sub_mask mask_add_aligned)

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

lemma aligned_bump_down:
  "is_aligned x n \<Longrightarrow> (x - 1) AND NOT(mask n) = x - 2 ^ n" by (drule is_aligned_mask_out_add_eq[where x="-1"]) (simp add: NOT_mask)

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

lemma unat_2tp_if:
  "unat (2 ^ n :: ('a :: len) word) = (if n < LENGTH ('a) then 2 ^ n else 0)" by (split if_split, simp_all add: power_overflow)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ n) = (if n < LENGTH('a) then 2 ^ n else 0)
theory Word_Lemmas

lemma mask_of_mask:
  "mask (n::nat) AND mask (m::nat) = (mask (min m n) :: 'a::len word)" by word_eqI_solve

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

lemma unat_signed_ucast_less_ucast:
  "LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> unat (ucast (x :: 'a :: len word) :: 'b :: len signed word) = unat x" by (simp add: unat_ucast_up_simp)

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

lemma plus_mask_AND_NOT_mask_eq:
  "x AND NOT(mask n) = x \<Longrightarrow> (x + mask n) AND NOT(mask n) = x" for x::\<open>'a::len word\<close> apply (subst word_plus_and_or_coroll; word_eqI; fastforce?) apply (erule allE, drule (1) iffD2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND NOT (mask n) = x \<Longrightarrow> x + mask n AND NOT (mask n) = x proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>na. (bit x na \<and> na < LENGTH('a) \<and> (LENGTH('a) \<le> na \<or> n \<le> na)) = bit x na; na < n; na < LENGTH('a); bit x na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>na < n; na < LENGTH('a); bit x na; bit x na \<and> na < LENGTH('a) \<and> (LENGTH('a) \<le> na \<or> n \<le> na)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma t2n_mask_eq_if:
  "2 ^ n AND mask m = (if n < m then 2 ^ n else (0 :: 'a::len word))" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ n AND mask m = (if n < m then 2 ^ n else 0)
theory Word_Lemmas

lemma unat_ucast_le:
  "unat (ucast (x :: 'a :: len word) :: 'b :: len word) \<le> unat x" by (simp add: ucast_nat_def word_unat_less_le)

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

lemma ucast_le_up_down_iff:
  "\<lbrakk> LENGTH('a) \<le> LENGTH('b); (x :: 'b :: len word) \<le> ucast (- 1 :: 'a :: len word) \<rbrakk>
   \<Longrightarrow> (ucast x \<le> (y :: 'a word)) = (x \<le> ucast y)" using le_max_word_ucast_id ucast_le_ucast by metis

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

goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) \<le> LENGTH('b); x \<le> UCAST('a \<rightarrow> 'b) (- 1)\<rbrakk> \<Longrightarrow> (UCAST('b \<rightarrow> 'a) x \<le> y) = (x \<le> UCAST('a \<rightarrow> 'b) y)
theory Word_Lemmas

lemma ucast_ucast_mask_shift:
  "a \<le> LENGTH('a) + b
   \<Longrightarrow> ucast (ucast (p AND mask a >> b) :: 'a :: len word) = p AND mask a >> b" by (metis add.commute le_mask_iff shiftr_mask_le ucast_ucast_eq_mask_shift word_and_le')

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

lemma unat_ucast_mask_shift:
  "a \<le> LENGTH('a) + b
   \<Longrightarrow> unat (ucast (p AND mask a >> b) :: 'a :: len word) = unat (p AND mask a >> b)" by (metis linear ucast_ucast_mask_shift unat_ucast_up_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> LENGTH('a) + b \<Longrightarrow> unat (UCAST('b \<rightarrow> 'a) (p AND mask a >> b)) = unat (p AND mask a >> b)
theory Word_Lemmas

lemma mask_overlap_zero:
  "a \<le> b \<Longrightarrow> (p AND mask a) AND NOT(mask b) = 0"
  for p :: \<open>'a::len word\<close> by (metis NOT_mask_AND_mask mask_lower_twice2 max_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> (p AND mask a) AND NOT (mask b) = 0
theory Word_Lemmas

lemma mask_shifl_overlap_zero:
  "a + c \<le> b \<Longrightarrow> (p AND mask a << c) AND NOT(mask b) = 0"
  for p :: \<open>'a::len word\<close> by (metis and_mask_0_iff_le_mask mask_mono mask_shiftl_decompose order_trans shiftl_over_and_dist word_and_le' word_and_le2)

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

lemma mask_overlap_zero':
  "a \<ge> b \<Longrightarrow> (p AND NOT(mask a)) AND mask b = 0"
  for p :: \<open>'a::len word\<close> using mask_AND_NOT_mask mask_AND_less_0 by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> (p AND NOT (mask a)) AND mask b = 0 proof (prove)
using this:
(?w AND NOT (mask ?n)) AND mask ?n = 0
\<lbrakk>?x AND mask ?n = 0; ?m \<le> ?n\<rbrakk> \<Longrightarrow> ?x AND mask ?m = 0

goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> (p AND NOT (mask a)) AND mask b = 0
theory Word_Lemmas

lemma mask_rshift_mult_eq_rshift_lshift:
  "((a :: 'a :: len word) >> b) * (1 << c) = (a >> b << c)" by (simp add: shiftl_t2n)

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

lemma shift_alignment:
  "a \<ge> b \<Longrightarrow> is_aligned (p >> a << a) b" using is_aligned_shift is_aligned_weaken by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> is_aligned (p >> a << a) b proof (prove)
using this:
is_aligned (?k << ?m) ?m
\<lbrakk>is_aligned ?w ?x; ?y \<le> ?x\<rbrakk> \<Longrightarrow> is_aligned ?w ?y

goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> is_aligned (p >> a << a) b
theory Word_Lemmas

lemma mask_split_sum_twice:
  "a \<ge> b \<Longrightarrow> (p AND NOT(mask a)) + ((p AND mask a) AND NOT(mask b)) + (p AND mask b) = p"
  for p :: \<open>'a::len word\<close> by (simp add: add.commute multiple_mask_trivia word_bw_comms(1) word_bw_lcs(1) word_plus_and_or_coroll2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> (p AND NOT (mask a)) + ((p AND mask a) AND NOT (mask b)) + (p AND mask b) = p
theory Word_Lemmas

lemma mask_shift_eq_mask_mask:
  "(p AND mask a >> b << b) = (p AND mask a) AND NOT(mask b)"
  for p :: \<open>'a::len word\<close> by (simp add: and_not_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p AND mask a >> b << b = (p AND mask a) AND NOT (mask b)
theory Word_Lemmas

lemma of_int_sint_scast:
  "of_int (sint (x :: 'a :: len word)) = (scast x :: 'b :: len word)" by (fact Word.of_int_sint)

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

lemma scast_of_nat_to_signed [simp]:
  "scast (of_nat x :: 'a :: len word) = (of_nat x :: 'a signed word)" by (rule bit_word_eqI) (simp add: bit_simps)

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

lemma scast_of_nat_signed_to_unsigned_add:
  "scast (of_nat x + of_nat y :: 'a :: len signed word) = (of_nat x + of_nat y :: 'a :: len word)" by (metis of_nat_add scast_of_nat)

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

lemma scast_of_nat_unsigned_to_signed_add:
  "(scast (of_nat x + of_nat y :: 'a :: len word)) = (of_nat x + of_nat y :: 'a :: len signed word)" by (metis Abs_fnat_hom_add scast_of_nat_to_signed)

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

lemma and_mask_cases:
  fixes x :: "'a :: len word"
  assumes len: "n < LENGTH('a)"
  shows "x AND mask n \<in> of_nat ` set [0 ..< 2 ^ n]" apply (simp flip: take_bit_eq_mask) apply (rule image_eqI [of _ _ \<open>unat (take_bit n x)\<close>]) using len apply simp_all apply transfer apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND mask n \<in> word_of_nat ` set [0..<2 ^ n] proof (prove)
goal (1 subgoal):
 1. take_bit n x \<in> word_of_nat ` {0..<2 ^ n} proof (prove)
goal (2 subgoals):
 1. take_bit n x = word_of_nat (unat (take_bit n x))
 2. unat (take_bit n x) \<in> {0..<2 ^ n} proof (prove)
using this:
n < LENGTH('a)

goal (2 subgoals):
 1. take_bit n x = word_of_nat (unat (take_bit n x))
 2. unat (take_bit n x) \<in> {0..<2 ^ n} proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> unat (take_bit n x) < 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<And>n x. n < LENGTH('a) \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (take_bit (min LENGTH('a) n) x) < 2 ^ n proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma sint_eq_uint_2pl:
  "\<lbrakk> (a :: 'a :: len word) < 2 ^ (LENGTH('a) - 1) \<rbrakk>
   \<Longrightarrow> sint a = uint a" by (simp add: not_msb_from_less sint_eq_uint word_2p_lem word_size)

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

lemma pow_sub_less:
  "\<lbrakk> a + b \<le> LENGTH('a); unat (x :: 'a :: len word) = 2 ^ a \<rbrakk>
   \<Longrightarrow> unat (x * 2 ^ b - 1) < 2 ^ (a + b)" by (smt (z3) eq_or_less_helperD le_add2 le_eq_less_or_eq le_trans power_add unat_mult_lem unat_pow_le_intro unat_power_lower word_eq_unatI)

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

lemma sle_le_2pl:
  "\<lbrakk> (b :: 'a :: len word) < 2 ^ (LENGTH('a) - 1); a \<le> b \<rbrakk> \<Longrightarrow> a <=s b" by (simp add: not_msb_from_less word_sle_msb_le)

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

lemma sless_less_2pl:
  "\<lbrakk> (b :: 'a :: len word) < 2 ^ (LENGTH('a) - 1); a < b \<rbrakk> \<Longrightarrow> a <s b" using not_msb_from_less word_sless_msb_less by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < 2 ^ (LENGTH('a) - 1); a < b\<rbrakk> \<Longrightarrow> a <s b proof (prove)
using this:
?v < 2 ^ (LENGTH(?'a) - 1) \<Longrightarrow> \<not> msb ?v
(?x <s ?y) = ((msb ?y \<longrightarrow> msb ?x) \<and> (msb ?x \<and> \<not> msb ?y \<or> ?x < ?y))

goal (1 subgoal):
 1. \<lbrakk>b < 2 ^ (LENGTH('a) - 1); a < b\<rbrakk> \<Longrightarrow> a <s b
theory Word_Lemmas

lemma and_mask2:
  "w << n >> n = w AND mask (size w - n)"
  for w :: \<open>'a::len word\<close> by (rule bit_word_eqI) (auto simp add: bit_simps word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w << n >> n = w AND mask (size w - n)
theory Word_Lemmas

lemma aligned_sub_aligned_simple:
  "\<lbrakk> is_aligned a n; is_aligned b n \<rbrakk> \<Longrightarrow> is_aligned (a - b) n" by (simp add: aligned_sub_aligned)

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

lemma minus_one_shift:
  "- (1 << n) = (-1 << n :: 'a::len word)" by (simp add: shiftl_def minus_exp_eq_not_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (1 << n) = - 1 << n
theory Word_Lemmas

lemma ucast_eq_mask:
  "(UCAST('a::len \<rightarrow> 'b::len) x = UCAST('a \<rightarrow> 'b) y) =
   (x AND mask LENGTH('b) = y AND mask LENGTH('b))" by transfer (simp flip: take_bit_eq_mask add: ac_simps)

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

lemma test_bit_sbintrunc:
  assumes "i < LENGTH('a)"
  shows "bit (word_of_int (signed_take_bit n (uint w)) :: 'a word) i
           = (if n < i then bit w n else bit w i)" using assms by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (word_of_int (signed_take_bit n (uint w))) i = (if n < i then bit w n else bit w i) proof (prove)
using this:
i < LENGTH('a)

goal (1 subgoal):
 1. bit (word_of_int (signed_take_bit n (uint w))) i = (if n < i then bit w n else bit w i)
theory Word_Lemmas

lemma test_bit_sbintrunc_ucast:
  assumes len_a: "i < LENGTH('a)"
  shows "bit (word_of_int (signed_take_bit (LENGTH('b) - 1) (uint (ucast w :: 'b word))) :: 'a word) i
          = (if LENGTH('b::len) \<le> i then bit w (LENGTH('b) - 1) else bit w i)" using len_a by (auto simp add: sbintrunc_uint_ucast bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (word_of_int (signed_take_bit (LENGTH('b) - 1) (uint (UCAST('a \<rightarrow> 'b) w)))) i = (if LENGTH('b) \<le> i then bit w (LENGTH('b) - 1) else bit w i) proof (prove)
using this:
i < LENGTH('a)

goal (1 subgoal):
 1. bit (word_of_int (signed_take_bit (LENGTH('b) - 1) (uint (UCAST('a \<rightarrow> 'b) w)))) i = (if LENGTH('b) \<le> i then bit w (LENGTH('b) - 1) else bit w i)
theory Word_Lemmas

lemma scast_ucast_mask_compare:
  "scast (ucast w :: 'b::len word) = w
   \<longleftrightarrow> (w \<le> mask (LENGTH('b) - 1) \<or> NOT(mask (LENGTH('b) - 1)) \<le> w)" apply (clarsimp simp: le_mask_high_bits neg_mask_le_high_bits scast_ucast_high_bits word_size) apply (rule iffI; clarsimp) apply (rename_tac i j; case_tac "i = LENGTH('b) - 1"; case_tac "j = LENGTH('b) - 1") by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (SCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) w) = w) = (w \<le> mask (LENGTH('b) - 1) \<or> NOT (mask (LENGTH('b) - 1)) \<le> w) proof (prove)
goal (1 subgoal):
 1. (\<forall>i\<in>{LENGTH('b)..<LENGTH('a)}. bit w i = bit w (LENGTH('b) - Suc 0)) = ((\<forall>i\<in>{LENGTH('b) - Suc 0..<LENGTH('a)}. \<not> bit w i) \<or> (\<forall>i\<in>{LENGTH('b) - Suc 0..<LENGTH('a)}. bit w i)) proof (prove)
goal (2 subgoals):
 1. \<And>i ia. \<lbrakk>\<forall>i\<in>{LENGTH('b)..<LENGTH('a)}. bit w i = bit w (LENGTH('b) - Suc 0); \<not> bit w i; bit w ia; LENGTH('b) - Suc 0 \<le> i; i < LENGTH('a); LENGTH('b) - Suc 0 \<le> ia; ia < LENGTH('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>i. \<lbrakk>(\<forall>i\<in>{LENGTH('b) - Suc 0..<LENGTH('a)}. \<not> bit w i) \<or> (\<forall>i\<in>{LENGTH('b) - Suc 0..<LENGTH('a)}. bit w i); LENGTH('b) \<le> i; i < LENGTH('a)\<rbrakk> \<Longrightarrow> bit w i = bit w (LENGTH('b) - Suc 0) proof (prove)
goal (5 subgoals):
 1. \<And>i j. \<lbrakk>\<forall>i\<in>{LENGTH('b)..<LENGTH('a)}. bit w i = bit w (LENGTH('b) - Suc 0); \<not> bit w i; bit w j; LENGTH('b) - Suc 0 \<le> i; i < LENGTH('a); LENGTH('b) - Suc 0 \<le> j; j < LENGTH('a); i = LENGTH('b) - 1; j = LENGTH('b) - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>i j. \<lbrakk>\<forall>i\<in>{LENGTH('b)..<LENGTH('a)}. bit w i = bit w (LENGTH('b) - Suc 0); \<not> bit w i; bit w j; LENGTH('b) - Suc 0 \<le> i; i < LENGTH('a); LENGTH('b) - Suc 0 \<le> j; j < LENGTH('a); i = LENGTH('b) - 1; j \<noteq> LENGTH('b) - 1\<rbrakk> \<Longrightarrow> False
 3. \<And>i j. \<lbrakk>\<forall>i\<in>{LENGTH('b)..<LENGTH('a)}. bit w i = bit w (LENGTH('b) - Suc 0); \<not> bit w i; bit w j; LENGTH('b) - Suc 0 \<le> i; i < LENGTH('a); LENGTH('b) - Suc 0 \<le> j; j < LENGTH('a); i \<noteq> LENGTH('b) - 1; j = LENGTH('b) - 1\<rbrakk> \<Longrightarrow> False
 4. \<And>i j. \<lbrakk>\<forall>i\<in>{LENGTH('b)..<LENGTH('a)}. bit w i = bit w (LENGTH('b) - Suc 0); \<not> bit w i; bit w j; LENGTH('b) - Suc 0 \<le> i; i < LENGTH('a); LENGTH('b) - Suc 0 \<le> j; j < LENGTH('a); i \<noteq> LENGTH('b) - 1; j \<noteq> LENGTH('b) - 1\<rbrakk> \<Longrightarrow> False
 5. \<And>i. \<lbrakk>(\<forall>i\<in>{LENGTH('b) - Suc 0..<LENGTH('a)}. \<not> bit w i) \<or> (\<forall>i\<in>{LENGTH('b) - Suc 0..<LENGTH('a)}. bit w i); LENGTH('b) \<le> i; i < LENGTH('a)\<rbrakk> \<Longrightarrow> bit w i = bit w (LENGTH('b) - Suc 0)
theory Word_Lemmas

lemma ucast_ucast_mask2:
  "is_down (UCAST ('a \<rightarrow> 'b)) \<Longrightarrow>
   UCAST ('b::len \<rightarrow> 'c::len) (UCAST ('a::len \<rightarrow> 'b::len) x) = UCAST ('a \<rightarrow> 'c) (x AND mask LENGTH('b))" by word_eqI_solve

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

lemma ucast_NOT:
  "ucast (NOT x) = NOT(ucast x) AND mask (LENGTH('a))" for x::"'a::len word" by word_eqI_solve

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

lemma upto_enum_step_shift:
  "is_aligned p n \<Longrightarrow> ([p , p + 2 ^ m .e. p + 2 ^ n - 1]) = map ((+) p) [0, 2 ^ m .e. 2 ^ n - 1]" apply (erule is_aligned_get_word_bits) prefer 2 apply (simp add: map_idI) apply (clarsimp simp: upto_enum_step_def) apply (frule is_aligned_no_overflow) apply (simp add: linorder_not_le [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> [p , p + 2 ^ m .e. p + 2 ^ n - 1] = map ((+) p) [0 , 2 ^ m .e. 2 ^ n - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> [p , p + 2 ^ m .e. p + 2 ^ n - 1] = map ((+) p) [0 , 2 ^ m .e. 2 ^ n - 1]
 2. \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> [p , p + 2 ^ m .e. p + 2 ^ n - 1] = map ((+) p) [0 , 2 ^ m .e. 2 ^ n - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> [p , p + 2 ^ m .e. p + 2 ^ n - 1] = map ((+) p) [0 , 2 ^ m .e. 2 ^ n - 1]
 2. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> [p , p + 2 ^ m .e. p + 2 ^ n - 1] = map ((+) p) [0 , 2 ^ m .e. 2 ^ n - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> [p , p + 2 ^ m .e. p + 2 ^ n - 1] = map ((+) p) [0 , 2 ^ m .e. 2 ^ n - 1] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a); p + 2 ^ n - 1 < p\<rbrakk> \<Longrightarrow> [0 .e. (2 ^ n - 1) div 2 ^ m] = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a); p + 2 ^ n - 1 < p; p \<le> p + 2 ^ n - 1\<rbrakk> \<Longrightarrow> [0 .e. (2 ^ n - 1) div 2 ^ m] = [] proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma upto_enum_step_shift_red:
  "\<lbrakk> is_aligned p sz; sz < LENGTH('a); us \<le> sz \<rbrakk>
     \<Longrightarrow> [p :: 'a :: len word, p + 2 ^ us .e. p + 2 ^ sz - 1]
          = map (\<lambda>x. p + of_nat x * 2 ^ us) [0 ..< 2 ^ (sz - us)]" apply (subst upto_enum_step_shift, assumption) apply (simp add: upto_enum_step_red) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p sz; sz < LENGTH('a); us \<le> sz\<rbrakk> \<Longrightarrow> [p , p + 2 ^ us .e. p + 2 ^ sz - 1] = map (\<lambda>x. p + word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p sz; sz < LENGTH('a); us \<le> sz\<rbrakk> \<Longrightarrow> map ((+) p) [0 , 2 ^ us .e. 2 ^ sz - 1] = map (\<lambda>x. p + word_of_nat x * 2 ^ us) [0..<2 ^ (sz - us)] proof (prove)
goal:
No subgoals!