kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas

lemma ucast_up_eq:
  "\<lbrakk> ucast x = (ucast y::'b::len word); LENGTH('a) \<le> LENGTH ('b) \<rbrakk>
   \<Longrightarrow> ucast x = (ucast y::'a::len word)" by (simp add: word_eq_iff bit_simps)

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

lemma ucast_up_neq:
  "\<lbrakk> ucast x \<noteq> (ucast y::'b::len word); LENGTH('b) \<le> LENGTH ('a) \<rbrakk>
   \<Longrightarrow> ucast x \<noteq> (ucast y::'a::len word)" by (fastforce dest: ucast_up_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST('c \<rightarrow> 'b) x \<noteq> UCAST('d \<rightarrow> 'b) y; LENGTH('b) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> UCAST('c \<rightarrow> 'a) x \<noteq> UCAST('d \<rightarrow> 'a) y
theory Word_Lemmas

lemma mask_AND_less_0:
  "\<lbrakk> x AND mask n = 0; m \<le> n \<rbrakk> \<Longrightarrow> x AND mask m = 0"
  for x :: \<open>'a::len word\<close> by (metis mask_twice2 word_and_notzeroD)

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

lemma mask_len_id [simp]:
  "(x :: 'a :: len word) AND mask LENGTH('a) = x" using uint_lt2p [of x] by (simp add: mask_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND mask LENGTH('a) = x proof (prove)
using this:
uint x < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. x AND mask LENGTH('a) = x
theory Word_Lemmas

lemma scast_ucast_down_same:
  "LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> SCAST('a \<rightarrow> 'b) = UCAST('a::len \<rightarrow> 'b::len)" by (simp add: down_cast_same is_down)

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

lemma word_aligned_0_sum:
  "\<lbrakk> a + b = 0; is_aligned (a :: 'a :: len word) n; b \<le> mask n; n < LENGTH('a) \<rbrakk>
   \<Longrightarrow> a = 0 \<and> b = 0" by (simp add: word_plus_and_or_coroll aligned_mask_disjoint word_or_zero)

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

lemma mask_eq1_nochoice:
  "\<lbrakk> LENGTH('a) > 1; (x :: 'a :: len word) AND 1 = x \<rbrakk> \<Longrightarrow> x = 0 \<or> x = 1" by (metis word_and_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < LENGTH('a); x AND 1 = x\<rbrakk> \<Longrightarrow> x = 0 \<or> x = 1
theory Word_Lemmas

lemma shiftr_and_eq_shiftl:
  "(w >> n) AND x = y \<Longrightarrow> w AND (x << n) = (y << n)" for y :: "'a:: len word" apply (drule sym) apply simp apply (rule bit_word_eqI) apply (auto simp add: bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w >> n) AND x = y \<Longrightarrow> w AND (x << n) = y << n proof (prove)
goal (1 subgoal):
 1. y = (w >> n) AND x \<Longrightarrow> w AND (x << n) = y << n proof (prove)
goal (1 subgoal):
 1. y = (w >> n) AND x \<Longrightarrow> w AND (x << n) = (w >> n) AND x << n proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>y = (w >> n) AND x; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (w AND (x << n)) na = bit ((w >> n) AND x << n) na proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma add_mask_lower_bits':
  "\<lbrakk> len = LENGTH('a); is_aligned (x :: 'a :: len word) n;
     \<forall>n' \<ge> n. n' < len \<longrightarrow> \<not> bit p n' \<rbrakk>
   \<Longrightarrow> x + p AND NOT(mask n) = x" using add_mask_lower_bits by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>len = LENGTH('a); is_aligned x n; \<forall>n'\<ge>n. n' < len \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x proof (prove)
using this:
\<lbrakk>is_aligned ?x ?n; \<forall>n'\<ge>?n. n' < LENGTH(?'a) \<longrightarrow> \<not> bit ?p n'\<rbrakk> \<Longrightarrow> ?x + ?p AND NOT (mask ?n) = ?x

goal (1 subgoal):
 1. \<lbrakk>len = LENGTH('a); is_aligned x n; \<forall>n'\<ge>n. n' < len \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x
theory Word_Lemmas

lemma leq_mask_shift:
  "(x :: 'a :: len word) \<le> mask (low_bits + high_bits) \<Longrightarrow> (x >> low_bits) \<le> mask high_bits" by (simp add: le_mask_iff shiftr_shiftr ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> mask (low_bits + high_bits) \<Longrightarrow> x >> low_bits \<le> mask high_bits
theory Word_Lemmas

lemma ucast_ucast_eq_mask_shift:
  "(x :: 'a :: len word) \<le> mask (low_bits + LENGTH('b))
   \<Longrightarrow> ucast((ucast (x >> low_bits)) :: 'b :: len word) = x >> low_bits" by (meson and_mask_eq_iff_le_mask eq_ucast_ucast_eq not_le_imp_less shiftr_less_t2n'
            ucast_ucast_len)

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

lemma const_le_unat:
  "\<lbrakk> b < 2 ^ LENGTH('a); of_nat b \<le> a \<rbrakk> \<Longrightarrow> b \<le> unat (a :: 'a :: len word)" by (simp add: word_le_nat_alt unsigned_of_nat take_bit_nat_eq_self)

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

lemma ucast_add:
  "ucast (a + (b :: 'a :: len word)) = ucast a + (ucast b :: ('a signed word))" by transfer (simp add: take_bit_add)

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

lemma ucast_minus:
  "ucast (a - (b :: 'a :: len word)) = ucast a - (ucast b :: ('a signed word))" apply (insert ucast_add[where a=a and b="-b"]) apply (metis (no_types, opaque_lifting) add_diff_eq diff_add_cancel ucast_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'a signed) (a - b) = UCAST('a \<rightarrow> 'a signed) a - UCAST('a \<rightarrow> 'a signed) b proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'a signed) (a + - b) = UCAST('a \<rightarrow> 'a signed) a + UCAST('a \<rightarrow> 'a signed) (- b) \<Longrightarrow> UCAST('a \<rightarrow> 'a signed) (a - b) = UCAST('a \<rightarrow> 'a signed) a - UCAST('a \<rightarrow> 'a signed) b proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_ucast_add_one [simp]:
  "scast (ucast (x :: 'a::len word) + (1 :: 'a signed word)) = x + 1" apply (subst ucast_1[symmetric]) apply (subst ucast_add[symmetric]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST('a signed \<rightarrow> 'a) (UCAST('a \<rightarrow> 'a signed) x + 1) = x + 1 proof (prove)
goal (1 subgoal):
 1. SCAST('a signed \<rightarrow> 'a) (UCAST('a \<rightarrow> 'a signed) x + UCAST(?'aa \<rightarrow> 'a signed) 1) = x + 1 proof (prove)
goal (1 subgoal):
 1. SCAST('a signed \<rightarrow> 'a) (UCAST('a \<rightarrow> 'a signed) (x + 1)) = x + 1 proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma word_and_le_plus_one:
  "a > 0 \<Longrightarrow> (x :: 'a :: len word) AND (a - 1) < a" by (simp add: gt0_iff_gem1 word_and_less')

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

lemma unat_of_ucast_then_shift_eq_unat_of_shift[simp]:
  "LENGTH('b) \<ge> LENGTH('a)
   \<Longrightarrow> unat ((ucast (x :: 'a :: len word) :: 'b :: len word) >> n) = unat (x >> n)" by (simp add: shiftr_div_2n' unat_ucast_up_simp)

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

lemma unat_of_ucast_then_mask_eq_unat_of_mask[simp]:
  "LENGTH('b) \<ge> LENGTH('a)
   \<Longrightarrow> unat ((ucast (x :: 'a :: len word) :: 'b :: len word) AND mask m) = unat (x AND mask m)" by (metis ucast_and_mask unat_ucast_up_simp)

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

lemma shiftr_less_t2n3:
  "\<lbrakk> (2 :: 'a word) ^ (n + m) = 0; m < LENGTH('a) \<rbrakk>
   \<Longrightarrow> (x :: 'a :: len word) >> n < 2 ^ m" by (fastforce intro: shiftr_less_t2n' simp: mask_eq_decr_exp power_overflow)

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

lemma unat_shiftr_le_bound:
  "\<lbrakk> 2 ^ (LENGTH('a :: len) - n) - 1 \<le> bnd; 0 < n \<rbrakk>
   \<Longrightarrow> unat ((x :: 'a word) >> n) \<le> bnd" apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_take_bit) apply (rule order_trans) defer apply assumption apply (simp add: nat_le_iff of_nat_diff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ (LENGTH('a) - n) - 1 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> unat (x >> n) \<le> bnd proof (prove)
goal (1 subgoal):
 1. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - 1 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (drop_bit n (take_bit LENGTH('a) x)) \<le> bnd proof (prove)
goal (1 subgoal):
 1. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> nat (drop_bit n (take_bit LENGTH('a) x)) \<le> bnd proof (prove)
goal (1 subgoal):
 1. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> nat (take_bit (LENGTH('a) - n) (drop_bit n x)) \<le> bnd proof (prove)
goal (2 subgoals):
 1. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> nat (take_bit (LENGTH('a) - n) (drop_bit n x)) \<le> ?y185 n bnd x
 2. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> ?y185 n bnd x \<le> bnd proof (prove)
goal (2 subgoals):
 1. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> ?y185 n bnd x \<le> bnd
 2. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> nat (take_bit (LENGTH('a) - n) (drop_bit n x)) \<le> ?y185 n bnd x proof (prove)
goal (1 subgoal):
 1. \<And>n bnd x. \<lbrakk>2 ^ (LENGTH('a) - n) - Suc 0 \<le> bnd; 0 < n\<rbrakk> \<Longrightarrow> nat (take_bit (LENGTH('a) - n) (drop_bit n x)) \<le> 2 ^ (LENGTH('a) - n) - Suc 0 proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftr_eqD:
  "\<lbrakk> x >> n = y >> n; is_aligned x n; is_aligned y n \<rbrakk>
   \<Longrightarrow> x = y" by (metis is_aligned_shiftr_shiftl)

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

lemma word_shiftr_shiftl_shiftr_eq_shiftr:
  "a \<ge> b \<Longrightarrow> (x :: 'a :: len word) >> a << b >> b = x >> a" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> x >> a << b >> b = x >> a proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b \<le> a; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (x >> a << b >> b) n = bit (x >> a) n proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma of_int_uint_ucast:
   "of_int (uint (x :: 'a::len word)) = (ucast x :: 'b::len word)" by (fact Word.of_int_uint)

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

lemma mod_mask_drop:
  "\<lbrakk> m = 2 ^ n; 0 < m; mask n AND msk = mask n \<rbrakk>
   \<Longrightarrow> (x mod m) AND msk = x mod m"
  for x :: \<open>'a::len word\<close> by (simp add: word_mod_2p_is_mask word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = 2 ^ n; 0 < m; mask n AND msk = mask n\<rbrakk> \<Longrightarrow> x mod m AND msk = x mod m
theory Word_Lemmas

lemma mask_eq_ucast_eq:
  "\<lbrakk> x AND mask LENGTH('a) = (x :: ('c :: len word));
     LENGTH('a) \<le> LENGTH('b)\<rbrakk>
    \<Longrightarrow> ucast (ucast x :: ('a :: len word)) = (ucast x :: ('b :: len word))" by (metis ucast_and_mask ucast_id ucast_ucast_mask ucast_up_eq)

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

lemma of_nat_less_t2n:
  "of_nat i < (2 :: ('a :: len) word) ^ n \<Longrightarrow> n < LENGTH('a) \<and> unat (of_nat i :: 'a word) < 2 ^ n" by (metis order_less_trans p2_gt_0 unat_less_power word_neq_0_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat i < 2 ^ n \<Longrightarrow> n < LENGTH('a) \<and> unat (word_of_nat i) < 2 ^ n
theory Word_Lemmas

lemma two_power_increasing_less_1:
  "\<lbrakk> n \<le> m; m \<le> LENGTH('a) \<rbrakk> \<Longrightarrow> (2 :: 'a :: len word) ^ n - 1 \<le> 2 ^ m - 1" by (metis diff_diff_cancel le_m1_iff_lt less_imp_diff_less p2_gt_0 two_power_increasing
            word_1_le_power word_le_minus_mono_left word_less_sub_1)

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

lemma word_sub_mono4:
  "\<lbrakk> y + x \<le> z + x; y \<le> y + x; z \<le> z + x \<rbrakk> \<Longrightarrow> y \<le> z" for y :: "'a :: len word" by (simp add: word_add_le_iff2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y + x \<le> z + x; y \<le> y + x; z \<le> z + x\<rbrakk> \<Longrightarrow> y \<le> z
theory Word_Lemmas

lemma eq_or_less_helperD:
  "\<lbrakk> n = unat (2 ^ m - 1 :: 'a :: len word) \<or> n < unat (2 ^ m - 1 :: 'a word); m < LENGTH('a) \<rbrakk>
   \<Longrightarrow> n < 2 ^ m" by (meson le_less_trans nat_less_le unat_less_power word_power_less_1)

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

lemma mask_sub:
  "n \<le> m \<Longrightarrow> mask m - mask n = mask m AND NOT(mask n :: 'a::len word)" by (metis (full_types) and_mask_eq_iff_shiftr_0 mask_out_sub_mask shiftr_mask_le word_bw_comms(1))

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

lemma neg_mask_diff_bound:
  "sz'\<le> sz \<Longrightarrow> (ptr AND NOT(mask sz')) - (ptr AND NOT(mask sz)) \<le> 2 ^ sz - 2 ^ sz'"
  (is "_ \<Longrightarrow> ?lhs \<le> ?rhs")
  for ptr :: \<open>'a::len word\<close> proof - assume lt: "sz' \<le> sz" hence "?lhs = ptr AND (mask sz AND NOT(mask sz'))" by (metis add_diff_cancel_left' multiple_mask_trivia) also have "\<dots> \<le> ?rhs" using lt by (metis (mono_tags) add_diff_eq diff_eq_eq eq_iff mask_2pm1 mask_sub word_and_le') finally show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (state)
goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (state)
this:
sz' \<le> sz

goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (prove)
using this:
sz' \<le> sz

goal (1 subgoal):
 1. (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) = ptr AND mask sz AND NOT (mask sz') proof (state)
this:
(ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) = ptr AND mask sz AND NOT (mask sz')

goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (state)
this:
(ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) = ptr AND mask sz AND NOT (mask sz')

goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (prove)
goal (1 subgoal):
 1. ptr AND mask sz AND NOT (mask sz') \<le> 2 ^ sz - 2 ^ sz' proof (prove)
using this:
sz' \<le> sz

goal (1 subgoal):
 1. ptr AND mask sz AND NOT (mask sz') \<le> 2 ^ sz - 2 ^ sz' proof (state)
this:
ptr AND mask sz AND NOT (mask sz') \<le> 2 ^ sz - 2 ^ sz'

goal (1 subgoal):
 1. sz' \<le> sz \<Longrightarrow> (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (chain)
picking this:
(ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (prove)
using this:
(ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz'

goal (1 subgoal):
 1. (ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz' proof (state)
this:
(ptr AND NOT (mask sz')) - (ptr AND NOT (mask sz)) \<le> 2 ^ sz - 2 ^ sz'

goal:
No subgoals!
theory Word_Lemmas

lemma mask_out_eq_0:
  "\<lbrakk> idx < 2 ^ sz; sz < LENGTH('a) \<rbrakk> \<Longrightarrow> (of_nat idx :: 'a :: len word) AND NOT(mask sz) = 0" by (simp add: of_nat_power less_mask_eq mask_eq_0_eq_x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx < 2 ^ sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat idx AND NOT (mask sz) = 0
theory Word_Lemmas

lemma is_aligned_neg_mask_eq':
  "is_aligned ptr sz = (ptr AND NOT(mask sz) = ptr)" using is_aligned_mask mask_eq_0_eq_x by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz = (ptr AND NOT (mask sz) = ptr) proof (prove)
using this:
is_aligned ?w ?n = (?w AND mask ?n = 0)
(?x AND ?w = 0) = (?x AND NOT ?w = ?x)

goal (1 subgoal):
 1. is_aligned ptr sz = (ptr AND NOT (mask sz) = ptr)
theory Word_Lemmas

lemma unat_pow_le_intro:
  "LENGTH('a) \<le> n \<Longrightarrow> unat (x :: 'a :: len word) < 2 ^ n" by (metis lt2p_lem not_le of_nat_le_iff of_nat_numeral semiring_1_class.of_nat_power uint_nat)

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

lemma unat_is_aligned_add:
  "\<lbrakk> is_aligned p n; unat d < 2 ^ n \<rbrakk>
   \<Longrightarrow> unat (p + d AND mask n) = unat d \<and> unat (p + d AND NOT(mask n)) = unat p" by (metis add.right_neutral and_mask_eq_iff_le_mask and_not_mask le_mask_iff mask_add_aligned
            mask_out_add_aligned mult_zero_right shiftl_t2n shiftr_le_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; unat d < 2 ^ n\<rbrakk> \<Longrightarrow> unat (p + d AND mask n) = unat d \<and> unat (p + d AND NOT (mask n)) = unat p
theory Word_Lemmas

lemma unat_shiftr_shiftl_mask_zero:
  "\<lbrakk> c + a \<ge> LENGTH('a) + b ; c < LENGTH('a) \<rbrakk>
   \<Longrightarrow> unat (((q :: 'a :: len word) >> a << b) AND NOT(mask c)) = 0" by (fastforce intro: unat_is_aligned_add[where p=0 and n=c, simplified, THEN conjunct2]
                       unat_shiftl_less_t2n unat_shiftr_less_t2n unat_pow_le_intro)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) + b \<le> c + a; c < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((q >> a << b) AND NOT (mask c)) = 0
theory Word_Lemmas

lemma shift_then_mask_eq_shift_low_bits:
  "x \<le> mask (low_bits + high_bits) \<Longrightarrow> (x >> low_bits) AND mask high_bits = x >> low_bits"
  for x :: \<open>'a::len word\<close> by (simp add: leq_mask_shift le_mask_imp_and_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> mask (low_bits + high_bits) \<Longrightarrow> (x >> low_bits) AND mask high_bits = x >> low_bits
theory Word_Lemmas

lemma leq_low_bits_iff_zero:
  "\<lbrakk> x \<le> mask (low bits + high bits); x >> low_bits = 0 \<rbrakk> \<Longrightarrow> (x AND mask low_bits = 0) = (x = 0)"
  for x :: \<open>'a::len word\<close> using and_mask_eq_iff_shiftr_0 by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> mask (low bits + high bits); x >> low_bits = 0\<rbrakk> \<Longrightarrow> (x AND mask low_bits = 0) = (x = 0) proof (prove)
using this:
(?w AND mask ?n = ?w) = (?w >> ?n = 0)

goal (1 subgoal):
 1. \<lbrakk>x \<le> mask (low bits + high bits); x >> low_bits = 0\<rbrakk> \<Longrightarrow> (x AND mask low_bits = 0) = (x = 0)
theory Word_Lemmas

lemma unat_less_iff:
  "\<lbrakk> unat (a :: 'a :: len word) = b; c < 2 ^ LENGTH('a) \<rbrakk> \<Longrightarrow> (a < of_nat c) = (b < c)" using unat_ucast_less_no_overflow_simp by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a = b; c < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (a < word_of_nat c) = (b < c) proof (prove)
using this:
?n < 2 ^ LENGTH(?'a) \<Longrightarrow> (unat ?f < ?n) = (?f < word_of_nat ?n)

goal (1 subgoal):
 1. \<lbrakk>unat a = b; c < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (a < word_of_nat c) = (b < c)
theory Word_Lemmas

lemma is_aligned_no_overflow3:
 "\<lbrakk> is_aligned (a :: 'a :: len word) n; n < LENGTH('a); b < 2 ^ n; c \<le> 2 ^ n; b < c \<rbrakk>
  \<Longrightarrow> a + b \<le> a + (c - 1)" by (meson is_aligned_no_wrap' le_m1_iff_lt not_le word_less_sub_1 word_plus_mono_right)

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

lemma leq_high_bits_shiftr_low_bits_leq_bits_mask:
  "x \<le> mask high_bits \<Longrightarrow> (x :: 'a :: len word) << low_bits \<le> mask (low_bits + high_bits)" by (metis le_mask_shiftl_le_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> mask high_bits \<Longrightarrow> x << low_bits \<le> mask (low_bits + high_bits)
theory Word_Lemmas

lemma word_two_power_neg_ineq:
  "2 ^ m \<noteq> (0 :: 'a word) \<Longrightarrow> 2 ^ n \<le> - (2 ^ m :: 'a :: len word)" apply (cases "n < LENGTH('a)"; simp add: power_overflow) apply (cases "m < LENGTH('a)"; simp add: power_overflow) apply (simp add: word_le_nat_alt unat_minus word_size) apply (cases "LENGTH('a)"; simp) apply (simp add: less_Suc_eq_le) apply (drule power_increasing[where a=2 and n=n] power_increasing[where a=2 and n=m], simp)+ apply (drule(1) add_le_mono) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ m \<noteq> 0 \<Longrightarrow> 2 ^ n \<le> - (2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> LENGTH('a) \<le> m; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n \<le> - (2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n \<le> - (2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 ^ LENGTH('a) - 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n < Suc nat; m < Suc nat; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 * 2 ^ nat - 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n \<le> nat; m \<le> nat; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 * 2 ^ nat - 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; (2::?'a28) ^ n \<le> (2::?'a28) ^ nat; (2::?'a31) ^ m \<le> (2::?'a31) ^ nat\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 * 2 ^ nat - 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; 2 ^ m \<le> 2 ^ nat; 2 ^ n + 2 ^ m \<le> 2 ^ nat + 2 ^ nat\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 * 2 ^ nat - 2 ^ m proof (prove)
goal:
No subgoals!