kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word_Operations

lemma limited_and_eq_0:
  "\<lbrakk> limited_and x z; y AND NOT z = y \<rbrakk> \<Longrightarrow> x AND y = 0" unfolding limited_and_def apply (subst arg_cong2[where f="(AND)"]) apply (erule sym)+ apply (simp(no_asm) add: word_bw_assocs word_bw_comms word_bw_lcs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limited_and x z; y AND NOT z = y\<rbrakk> \<Longrightarrow> x AND y = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> x AND y = 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> x = ?b
 2. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> y = ?d
 3. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> ?b AND ?d = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> (x AND z) AND y AND NOT z = 0 proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma limited_and_eq_id:
  "\<lbrakk> limited_and x z; y AND z = z \<rbrakk> \<Longrightarrow> x AND y = x" unfolding limited_and_def by (erule subst, fastforce simp: word_bw_lcs word_bw_assocs word_bw_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limited_and x z; y AND z = z\<rbrakk> \<Longrightarrow> x AND y = x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND z = x; y AND z = z\<rbrakk> \<Longrightarrow> x AND y = x
theory More_Word_Operations

lemma lshift_limited_and:
  "limited_and x z \<Longrightarrow> limited_and (x << n) (z << n)" using push_bit_and [of n x z] by (simp add: limited_and_def shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x << n) (z << n) proof (prove)
using this:
push_bit n (x AND z) = push_bit n x AND push_bit n z

goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x << n) (z << n)
theory More_Word_Operations

lemma rshift_limited_and:
  "limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n)" using drop_bit_and [of n x z] by (simp add: limited_and_def shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n) proof (prove)
using this:
drop_bit n (x AND z) = drop_bit n x AND drop_bit n z

goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n)
theory More_Word_Operations

lemma from_bool_eq:
  \<open>from_bool = of_bool\<close> by (simp add: fun_eq_iff from_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. from_bool = of_bool
theory More_Word_Operations

lemma from_bool_0:
  "(from_bool x = 0) = (\<not> x)" by (simp add: from_bool_def split: bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (from_bool x = 0) = (\<not> x)
theory More_Word_Operations

lemma from_bool_eq_if':
  "((if P then 1 else 0) = from_bool Q) = (P = Q)" by (cases Q) (simp_all add: from_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then 1 else 0) = from_bool Q) = (P = Q)
theory More_Word_Operations

lemma to_bool_and_1:
  "to_bool (x AND 1) \<longleftrightarrow> bit x 0" by (simp add: to_bool_def word_and_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool (x AND 1) = bit x 0
theory More_Word_Operations

lemma to_bool_from_bool [simp]:
  "to_bool (from_bool r) = r" unfolding from_bool_def to_bool_def by (simp split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool (from_bool r) = r proof (prove)
goal (1 subgoal):
 1. (0 \<noteq> (case r of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0)) = r
theory More_Word_Operations

lemma from_bool_neq_0 [simp]:
  "(from_bool b \<noteq> 0) = b" by (simp add: from_bool_def split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (from_bool b \<noteq> 0) = b
theory More_Word_Operations

lemma from_bool_mask_simp [simp]:
  "(from_bool r :: 'a::len word) AND 1 = from_bool r" unfolding from_bool_def by (clarsimp split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. from_bool r AND 1 = from_bool r proof (prove)
goal (1 subgoal):
 1. (case r of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) AND 1 = (case r of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0)
theory More_Word_Operations

lemma from_bool_1 [simp]:
  "(from_bool P = 1) = P" by (simp add: from_bool_def split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (from_bool P = 1) = P
theory More_Word_Operations

lemma ge_0_from_bool [simp]:
  "(0 < from_bool P) = P" by (simp add: from_bool_def split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 < from_bool P) = P
theory More_Word_Operations

lemma limited_and_from_bool:
  "limited_and (from_bool b) 1" by (simp add: from_bool_def limited_and_def split: bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. limited_and (from_bool b) 1
theory More_Word_Operations

lemma to_bool_1 [simp]: "to_bool 1" by (simp add: to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool 1
theory More_Word_Operations

lemma to_bool_0 [simp]: "\<not>to_bool 0" by (simp add: to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> to_bool 0
theory More_Word_Operations

lemma from_bool_eq_if:
  "(from_bool Q = (if P then 1 else 0)) = (P = Q)" by (cases Q) (simp_all add: from_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (from_bool Q = (if P then 1 else 0)) = (P = Q)
theory More_Word_Operations

lemma to_bool_eq_0:
  "(\<not> to_bool x) = (x = 0)" by (simp add: to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> to_bool x) = (x = 0)
theory More_Word_Operations

lemma from_bool_all_helper:
  "(\<forall>bool. from_bool bool = val \<longrightarrow> P bool)
      = ((\<exists>bool. from_bool bool = val) \<longrightarrow> P (val \<noteq> 0))" by (auto simp: from_bool_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>bool. from_bool bool = val \<longrightarrow> P bool) = ((\<exists>bool. from_bool bool = val) \<longrightarrow> P (val \<noteq> 0))
theory More_Word_Operations

lemma fold_eq_0_to_bool:
  "(v = 0) = (\<not> to_bool v)" by (simp add: to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v = 0) = (\<not> to_bool v)
theory More_Word_Operations

lemma from_bool_to_bool_iff:
  "w = from_bool b \<longleftrightarrow> to_bool w = b \<and> (w = 0 \<or> w = 1)" by (cases b) (auto simp: from_bool_def to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w = from_bool b) = (to_bool w = b \<and> (w = 0 \<or> w = 1))
theory More_Word_Operations

lemma from_bool_odd_eq_and:
  "from_bool (odd w) = w AND 1" unfolding from_bool_def by (simp add: word_and_1 bit_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. from_bool (odd w) = w AND 1 proof (prove)
goal (1 subgoal):
 1. (case odd w of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) = w AND 1
theory More_Word_Operations

lemma mask_range_to_bl:
  "is_aligned (ptr :: 'a :: len word) bits
   \<Longrightarrow> mask_range ptr bits
        = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}" apply (erule is_aligned_get_word_bits) apply (erule(1) mask_range_to_bl') apply (rule set_eqI) apply (simp add: power_overflow mask_eq_decr_exp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (x \<in> mask_range ptr bits) = (x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}) proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma aligned_mask_ranges_disjoint:
  "\<lbrakk> is_aligned (p :: 'a :: len word) n; is_aligned (p' :: 'a :: len word) n';
     p AND NOT(mask n') \<noteq> p'; p' AND NOT(mask n) \<noteq> p \<rbrakk>
   \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {}" using aligned_mask_range_cases by (auto simp: neg_mask_in_mask_range)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; p AND NOT (mask n') \<noteq> p'; p' AND NOT (mask n) \<noteq> p\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {} proof (prove)
using this:
\<lbrakk>is_aligned ?p ?n; is_aligned ?p' ?n'\<rbrakk> \<Longrightarrow> mask_range ?p ?n \<inter> mask_range ?p' ?n' = {} \<or> mask_range ?p ?n \<subseteq> mask_range ?p' ?n' \<or> mask_range ?p' ?n' \<subseteq> mask_range ?p ?n

goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; p AND NOT (mask n') \<noteq> p'; p' AND NOT (mask n) \<noteq> p\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {}
theory More_Word_Operations

lemma word_clz_sint_upper[simp]:
  "LENGTH('a) \<ge> 3 \<Longrightarrow> sint (of_nat (word_clz (w :: 'a :: len word)) :: 'a sword) \<le> int (LENGTH('a))" using word_clz_max [of w] apply (simp add: word_size signed_of_nat) apply (subst signed_take_bit_int_eq_self) apply simp_all apply (metis negative_zle of_nat_numeral semiring_1_class.of_nat_power) apply (drule small_powers_of_2) apply (erule le_less_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> sint (word_of_nat (word_clz w)) \<le> int LENGTH('a) proof (prove)
using this:
word_clz w \<le> size w

goal (1 subgoal):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> sint (word_of_nat (word_clz w)) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) (int (word_clz w)) \<le> int LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> int (word_clz w)
 2. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> int (word_clz w) < 2 ^ (LENGTH('a) - Suc 0)
 3. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> int (word_clz w) \<le> int LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> int (word_clz w)
 2. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_clz w \<le> LENGTH('a); LENGTH('a) < 2 ^ (LENGTH('a) - 1)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma word_clz_sint_lower[simp]:
  "LENGTH('a) \<ge> 3
   \<Longrightarrow> - sint (of_nat (word_clz (w :: 'a :: len word)) :: 'a signed word) \<le> int (LENGTH('a))" apply (subst sint_eq_uint) using word_clz_max [of w] apply (simp_all add: word_size unsigned_of_nat) apply (rule not_msb_from_less) apply (simp add: word_less_nat_alt unsigned_of_nat) apply (subst take_bit_nat_eq_self) apply (simp add: le_less_trans) apply (drule small_powers_of_2) apply (erule le_less_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> - sint (word_of_nat (word_clz w)) \<le> int LENGTH('a) proof (prove)
goal (2 subgoals):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> \<not> msb (word_of_nat (word_clz w))
 2. 3 \<le> LENGTH('a) \<Longrightarrow> - uint (word_of_nat (word_clz w)) \<le> int LENGTH('a) proof (prove)
using this:
word_clz w \<le> size w

goal (2 subgoals):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> \<not> msb (word_of_nat (word_clz w))
 2. 3 \<le> LENGTH('a) \<Longrightarrow> - uint (word_of_nat (word_clz w)) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> msb (word_of_nat (word_clz w)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat (word_clz w) < 2 ^ (LENGTH('a signed) - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (word_clz w) < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ LENGTH('a)
 2. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_clz w \<le> LENGTH('a); LENGTH('a) < 2 ^ (LENGTH('a) - 1)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma mask_range_subsetD:
  "\<lbrakk> p' \<in> mask_range p n; x' \<in> mask_range p' n'; n' \<le> n; is_aligned p n; is_aligned p' n' \<rbrakk> \<Longrightarrow>
   x' \<in> mask_range p n" using aligned_mask_step by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<in> mask_range p n; x' \<in> mask_range p' n'; n' \<le> n; is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> x' \<in> mask_range p n proof (prove)
using this:
\<lbrakk>?n' \<le> ?n; ?p' \<le> ?p + mask ?n; is_aligned ?p ?n; is_aligned ?p' ?n'\<rbrakk> \<Longrightarrow> ?p' + mask ?n' \<le> ?p + mask ?n

goal (1 subgoal):
 1. \<lbrakk>p' \<in> mask_range p n; x' \<in> mask_range p' n'; n' \<le> n; is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> x' \<in> mask_range p n
theory More_Word_Operations

lemma add_mult_in_mask_range:
  "\<lbrakk> is_aligned (base :: 'a :: len word) n; n < LENGTH('a); bits \<le> n; x < 2 ^ (n - bits) \<rbrakk>
   \<Longrightarrow> base + x * 2^bits \<in> mask_range base n" by (simp add: is_aligned_no_wrap' mask_2pm1 nasty_split_lt word_less_power_trans2
                word_plus_mono_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned base n; n < LENGTH('a); bits \<le> n; x < 2 ^ (n - bits)\<rbrakk> \<Longrightarrow> base + x * 2 ^ bits \<in> mask_range base n
theory More_Word_Operations

lemma unat_of_nat_word_log2:
  "LENGTH('a) < 2 ^ LENGTH('b)
   \<Longrightarrow> unat (of_nat (word_log2 (n :: 'a :: len word)) :: 'b :: len word) = word_log2 n" by (metis less_trans unat_of_nat_eq word_log2_max word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ LENGTH('b) \<Longrightarrow> unat (word_of_nat (word_log2 n)) = word_log2 n
theory More_Word_Operations

lemma Suc_mask_eq_mask:
  "\<not>bit a n \<Longrightarrow> a AND mask (Suc n) = a AND mask n" for a::"'a::len word" by (metis sign_extend_def sign_extend_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit a n \<Longrightarrow> a AND mask (Suc n) = a AND mask n
theory More_Word_Operations

lemma word_less_high_bits:
  fixes a::"'a::len word"
  assumes high_bits: "\<forall>i > n. bit a i = bit b i"
  assumes less: "a AND mask (Suc n) < b AND mask (Suc n)"
  shows "a < b" proof - let ?masked = "\<lambda>x. x AND NOT (mask (Suc n))" from high_bits have "?masked a = ?masked b" by - word_eqI_solve then have "?masked a + (a AND mask (Suc n)) < ?masked b + (b AND mask (Suc n))" by (metis AND_NOT_mask_plus_AND_mask_eq less word_and_le2 word_plus_strict_mono_right) then show ?thesis by (simp add: AND_NOT_mask_plus_AND_mask_eq) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < b proof (state)
goal (1 subgoal):
 1. a < b proof (state)
goal (1 subgoal):
 1. a < b proof (chain)
picking this:
\<forall>i>n. bit a i = bit b i proof (prove)
using this:
\<forall>i>n. bit a i = bit b i

goal (1 subgoal):
 1. a AND NOT (mask (Suc n)) = b AND NOT (mask (Suc n)) proof (state)
this:
a AND NOT (mask (Suc n)) = b AND NOT (mask (Suc n))

goal (1 subgoal):
 1. a < b proof (chain)
picking this:
a AND NOT (mask (Suc n)) = b AND NOT (mask (Suc n)) proof (prove)
using this:
a AND NOT (mask (Suc n)) = b AND NOT (mask (Suc n))

goal (1 subgoal):
 1. (a AND NOT (mask (Suc n))) + (a AND mask (Suc n)) < (b AND NOT (mask (Suc n))) + (b AND mask (Suc n)) proof (state)
this:
(a AND NOT (mask (Suc n))) + (a AND mask (Suc n)) < (b AND NOT (mask (Suc n))) + (b AND mask (Suc n))

goal (1 subgoal):
 1. a < b proof (chain)
picking this:
(a AND NOT (mask (Suc n))) + (a AND mask (Suc n)) < (b AND NOT (mask (Suc n))) + (b AND mask (Suc n)) proof (prove)
using this:
(a AND NOT (mask (Suc n))) + (a AND mask (Suc n)) < (b AND NOT (mask (Suc n))) + (b AND mask (Suc n))

goal (1 subgoal):
 1. a < b proof (state)
this:
a < b

goal:
No subgoals!
theory More_Word_Operations

lemma word_less_bitI:
  fixes a :: "'a::len word"
  assumes hi_bits: "\<forall>i > n. bit a i = bit b i"
  assumes a_bits: "\<not>bit a n"
  assumes b_bits: "bit b n" "n < LENGTH('a)"
  shows "a < b" proof - from b_bits have "a AND mask n < b AND mask (Suc n)" by (metis bit_mask_iff impossible_bit le2p_bits_unset leI lessI less_Suc_eq_le mask_eq_decr_exp
              word_and_less' word_ao_nth) with a_bits have "a AND mask (Suc n) < b AND mask (Suc n)" by (simp add: Suc_mask_eq_mask) with hi_bits show ?thesis by (rule word_less_high_bits) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < b proof (state)
goal (1 subgoal):
 1. a < b proof (chain)
picking this:
bit b n
n < LENGTH('a) proof (prove)
using this:
bit b n
n < LENGTH('a)

goal (1 subgoal):
 1. a AND mask n < b AND mask (Suc n) proof (state)
this:
a AND mask n < b AND mask (Suc n)

goal (1 subgoal):
 1. a < b proof (chain)
picking this:
\<not> bit a n
a AND mask n < b AND mask (Suc n) proof (prove)
using this:
\<not> bit a n
a AND mask n < b AND mask (Suc n)

goal (1 subgoal):
 1. a AND mask (Suc n) < b AND mask (Suc n) proof (state)
this:
a AND mask (Suc n) < b AND mask (Suc n)

goal (1 subgoal):
 1. a < b proof (chain)
picking this:
\<forall>i>n. bit a i = bit b i
a AND mask (Suc n) < b AND mask (Suc n) proof (prove)
using this:
\<forall>i>n. bit a i = bit b i
a AND mask (Suc n) < b AND mask (Suc n)

goal (1 subgoal):
 1. a < b proof (state)
this:
a < b

goal:
No subgoals!
theory More_Word_Operations

lemma word_less_bit_eq:
  "(a < b) = (\<exists>n < LENGTH('a). (\<forall>i > n. bit a i = bit b i) \<and> \<not>bit a n \<and> bit b n)" for a::"'a::len word" by (meson bit_imp_le_length word_less_bitD word_less_bitI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a < b) = (\<exists>n<LENGTH('a). (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n)
theory Word_32

lemma len32: "len_of (x :: 32 itself) = 32" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. len_of x = 32
theory Word_32

lemma ucast_8_32_inj:
  "inj (ucast ::  8 word \<Rightarrow> 32 word)" by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj UCAST(8 \<rightarrow> 32)
theory Word_32

lemma unat_ucast_8_32:
  fixes x :: "8 word"
  shows "unat (ucast x :: word32) = unat x" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) x) = unat x
theory Word_32

lemma eq_2_32_0:
  "(2 ^ 32 :: word32) = 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ 32 = 0
theory Word_32

lemma of_nat32_n_less_equal_power_2:
 "n < 32 \<Longrightarrow> ((of_nat n)::32 word) < 2 ^ n" by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 32 \<Longrightarrow> word_of_nat n < 2 ^ n
theory Word_32

lemma unat_ucast_10_32 :
  fixes x :: "10 word"
  shows "unat (ucast x :: word32) = unat x" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(10 \<rightarrow> 32) x) = unat x
theory Word_32

lemma word32_bounds:
  "- (2 ^ (size (x :: word32) - 1)) = (-2147483648 :: int)"
  "((2 ^ (size (x :: word32) - 1)) - 1) = (2147483647 :: int)"
  "- (2 ^ (size (y :: 32 signed word) - 1)) = (-2147483648 :: int)"
  "((2 ^ (size (y :: 32 signed word) - 1)) - 1) = (2147483647 :: int)" by (simp_all add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- (2 ^ (size x - 1)) = - 2147483648 &&& 2 ^ (size x - 1) - 1 = 2147483647) &&& - (2 ^ (size y - 1)) = - 2147483648 &&& 2 ^ (size y - 1) - 1 = 2147483647
theory Word_32

lemma ucast_of_nats [simp]:
  "(ucast (of_nat x :: word32) :: sword32) = (of_nat x)"
  "(ucast (of_nat x :: word32) :: 16 sword) = (of_nat x)"
  "(ucast (of_nat x :: word32) :: 8 sword) = (of_nat x)"
  "(ucast (of_nat x :: 16 word) :: 16 sword) = (of_nat x)"
  "(ucast (of_nat x :: 16 word) :: 8 sword) = (of_nat x)"
  "(ucast (of_nat x :: 8 word) :: 8 sword) = (of_nat x)" by (simp_all add: of_nat_take_bit take_bit_word_eq_self unsigned_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST(32 \<rightarrow> 32 signed) (word_of_nat x) = word_of_nat x &&& UCAST(32 \<rightarrow> 16 signed) (word_of_nat x) = word_of_nat x &&& UCAST(32 \<rightarrow> 8 signed) (word_of_nat x) = word_of_nat x) &&& UCAST(16 \<rightarrow> 16 signed) (word_of_nat x) = word_of_nat x &&& UCAST(16 \<rightarrow> 8 signed) (word_of_nat x) = word_of_nat x &&& UCAST(8 \<rightarrow> 8 signed) (word_of_nat x) = word_of_nat x
theory Word_32

lemma word32_31_less:
  "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)"
  "31 < len_of TYPE (32)" "31 > (0 :: nat)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (31 < LENGTH(32 signed) &&& 0 < 31) &&& 31 < LENGTH(32) &&& 0 < 31
theory Word_32

lemma has_zero_byte:
  "~~ (((((v::word32) && 0x7f7f7f7f) + 0x7f7f7f7f) || v) || 0x7f7f7f7f) \<noteq> 0
    \<Longrightarrow> v && 0xff000000 = 0 \<or> v && 0xff0000 = 0 \<or> v && 0xff00 = 0 \<or> v && 0xff = 0" by word_bitwise auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ~~ (((v && 2139062143) + 2139062143 || v) || 2139062143) \<noteq> 0 \<Longrightarrow> v && 4278190080 = 0 \<or> v && 16711680 = 0 \<or> v && 65280 = 0 \<or> v && 255 = 0
theory Word_32

lemma unat_of_int_32:
  "\<lbrakk>i \<ge> 0; i \<le>2 ^ 31\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword32)) = nat i" by (simp add: unsigned_of_int nat_take_bit_eq take_bit_nat_eq_self)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> i; i \<le> 2 ^ 31\<rbrakk> \<Longrightarrow> unat (word_of_int i) = nat i
theory Word_32

lemma cast_chunk_assemble_id_64[simp]:
  "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_assemble_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 64) (UCAST(64 \<rightarrow> 32) x) || (UCAST(32 \<rightarrow> 64) (UCAST(64 \<rightarrow> 32) (x >> 32)) << 32) = x