kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> range ucast = {x. x < 2 ^ LENGTH('a)} proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>LENGTH('a) < LENGTH('b); xa \<in> UNIV\<rbrakk> \<Longrightarrow> ucast xa < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x \<in> range ucast proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x \<in> range ucast proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> \<exists>xa. x = ucast xa proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x = ucast (ucast x) proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('a); n < LENGTH('b)\<rbrakk> \<Longrightarrow> bit x n = bit (ucast (ucast x)) n proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('a); n < LENGTH('b); bit x n\<rbrakk> \<Longrightarrow> n < LENGTH('a) proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x \<le> y - 1
theory More_Word

lemma word_sub_mono2:
  "\<lbrakk> a + b \<le> c + d; c \<le> a; b \<le> a + b; d \<le> c + d \<rbrakk> \<Longrightarrow> b \<le> (d :: 'a :: len word)" by (drule(1) word_sub_mono; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + b \<le> c + d; c \<le> a; b \<le> a + b; d \<le> c + d\<rbrakk> \<Longrightarrow> b \<le> d
theory More_Word

lemma word_not_le:
  "(\<not> x \<le> (y :: 'a :: len word)) = (y < x)" by (fact not_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> x \<le> y) = (y < x)
theory More_Word

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

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

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n \<le> 2 ^ m; n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> n \<le> m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n < 2 ^ m \<or> 2 ^ n = 2 ^ m; n < LENGTH('a); m < LENGTH('a); n \<noteq> m\<rbrakk> \<Longrightarrow> n < m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a); n \<noteq> m; 2 ^ n < 2 ^ m\<rbrakk> \<Longrightarrow> n < m
 2. \<lbrakk>n < LENGTH('a); m < LENGTH('a); n \<noteq> m; 2 ^ n = 2 ^ m\<rbrakk> \<Longrightarrow> n < m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a); n \<noteq> m; 2 ^ n = 2 ^ m\<rbrakk> \<Longrightarrow> n < m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a); n \<noteq> m; uint (2 ^ n) = uint (2 ^ m)\<rbrakk> \<Longrightarrow> n < m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> m; uint (2 ^ n) = uint (2 ^ m); uint (2 ^ n) = 2 ^ n; uint (2 ^ m) = 2 ^ m\<rbrakk> \<Longrightarrow> n < m proof (prove)
goal:
No subgoals!
theory More_Word

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

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

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < word_of_nat n \<Longrightarrow> unat x < n proof (prove)
goal (1 subgoal):
 1. unat x < unat (word_of_nat n) \<Longrightarrow> unat x < n proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n) \<le> n proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nat (uint y) = z; x < y\<rbrakk> \<Longrightarrow> nat (uint x) < z proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> nat (uint x) < nat (uint y) proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> unat x < nat (uint y) proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> unat x < unat y
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (word_of_nat x = word_of_nat y) = (x = y)
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y div z \<Longrightarrow> x * z \<le> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y div z; z = 0\<rbrakk> \<Longrightarrow> x * z \<le> y
 2. \<lbrakk>x \<le> y div z; z \<noteq> 0\<rbrakk> \<Longrightarrow> x * z \<le> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y div z; z \<noteq> 0\<rbrakk> \<Longrightarrow> x * z \<le> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> x * z \<le> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> x * z \<le> ?y1
 2. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> ?y1 \<le> y proof (prove)
goal (2 subgoals):
 1. 0 < z \<Longrightarrow> unat (y div z) * unat z < 2 ^ LENGTH('a)
 2. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> y div z * z \<le> y proof (prove)
goal (2 subgoals):
 1. 0 < z \<Longrightarrow> unat y div unat z * unat z < 2 ^ LENGTH('a)
 2. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> y div z * z \<le> y proof (prove)
goal (2 subgoals):
 1. 0 < z \<Longrightarrow> unat y < 2 ^ LENGTH('a)
 2. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> y div z * z \<le> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y div z; 0 < z\<rbrakk> \<Longrightarrow> y div z * z \<le> y proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (ucast x) = x AND mask LENGTH('a) proof (prove)
goal (1 subgoal):
 1. ucast (ucast x) = take_bit LENGTH('a) x proof (prove)
goal (1 subgoal):
 1. \<And>x. take_bit LENGTH('b) (take_bit LENGTH('a) (take_bit LENGTH('b) x)) = take_bit LENGTH('b) (take_bit (min LENGTH('b) LENGTH('a)) x) proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ LENGTH('b) \<Longrightarrow> ucast (ucast x) = x proof (prove)
goal (1 subgoal):
 1. x < 2 ^ LENGTH('b) \<Longrightarrow> x AND mask LENGTH('b) = x proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> ucast (ucast x) = x
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (ucast x) = unat x mod 2 ^ LENGTH('a) proof (state)
goal (1 subgoal):
 1. unat (ucast x) = unat x mod 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH('a) = nat (2 ^ LENGTH('a)) proof (state)
this:
2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))

goal (1 subgoal):
 1. unat (ucast x) = unat x mod 2 ^ LENGTH('a) proof (state)
this:
2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))

goal (1 subgoal):
 1. unat (ucast x) = unat x mod 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat (ucast x) = unat x mod nat (2 ^ LENGTH('a)) proof (state)
this:
unat (ucast x) = unat x mod nat (2 ^ LENGTH('a))

goal (1 subgoal):
 1. unat (ucast x) = unat x mod 2 ^ LENGTH('a) proof (chain)
picking this:
2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))
unat (ucast x) = unat x mod nat (2 ^ LENGTH('a)) proof (prove)
using this:
2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))
unat (ucast x) = unat x mod nat (2 ^ LENGTH('a))

goal (1 subgoal):
 1. unat (ucast x) = unat x mod 2 ^ LENGTH('a) proof (state)
this:
unat (ucast x) = unat x mod 2 ^ LENGTH('a)

goal:
No subgoals!
theory More_Word

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

\<comment> \<open>This weaker version was previously called @{text ucast_less_ucast}. We retain it to
    support existing proofs.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (ucast x < ucast y) = (x < y) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (unat x mod 2 ^ LENGTH('b) < unat y mod 2 ^ LENGTH('b)) = (unat x < unat y) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> unat x < 2 ^ LENGTH('b)
 2. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (unat x < unat y mod 2 ^ LENGTH('b)) = (unat x < unat y) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (unat x < unat y mod 2 ^ LENGTH('b)) = (unat x < unat y) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> unat y < 2 ^ LENGTH('b)
 2. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (unat x < unat y) = (unat x < unat y) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (unat x < unat y) = (unat x < unat y) proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> - 1 \<Longrightarrow> unat (n + 1) = Suc (unat n) proof (prove)
goal (1 subgoal):
 1. n \<noteq> - 1 \<Longrightarrow> 1 + n \<noteq> 0 proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n div 1 = n
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- 1 \<le> x) = (x = - 1)
theory More_Word

lemma up_scast_inj:
  "\<lbrakk> scast x = (scast y :: 'b :: len word); size x \<le> LENGTH('b) \<rbrakk> \<Longrightarrow> x = y" apply transfer apply (cases \<open>LENGTH('a)\<close>; simp) apply (metis order_refl take_bit_signed_take_bit take_bit_tightened) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scast x = scast y; size x \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) x) = take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) y); LENGTH('a) \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) x = take_bit LENGTH('a) y proof (prove)
goal (1 subgoal):
 1. \<And>x y nat. \<lbrakk>take_bit LENGTH('b) (signed_take_bit nat x) = take_bit LENGTH('b) (signed_take_bit nat y); Suc nat \<le> LENGTH('b); LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (Suc nat) x = take_bit (Suc nat) y proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (scast x = scast y) = (x = y)
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<exists>n. y = x + word_of_nat n
theory More_Word

lemma word_plus_mcs_4':
  "\<lbrakk>x + v \<le> x + w; x \<le> x + v\<rbrakk> \<Longrightarrow> v \<le> w" for x :: "'a::len word" by (rule word_plus_mcs_4; simp add: add.commute)

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

lemma unat_eq_1:
  \<open>unat x = Suc 0 \<longleftrightarrow> x = 1\<close> by (auto intro!: unsigned_word_eqI [where ?'a = nat])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (unat x = Suc 0) = (x = 1)
theory More_Word

lemma word_unat_Rep_inject1:
  \<open>unat x = unat 1 \<longleftrightarrow> x = 1\<close> by (simp add: unat_eq_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (unat x = unat 1) = (x = 1)
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w AND NOT (mask n)) AND NOT (mask m) = w AND NOT (mask (max m n))
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x = y - 1 \<or> x < y - 1 proof (prove)
goal (1 subgoal):
 1. x \<le> y - 1 \<Longrightarrow> x = y - 1 \<or> x < y - 1 proof (prove)
goal (1 subgoal):
 1. x < y - 1 \<or> x = y - 1 \<Longrightarrow> x = y - 1 \<or> x < y - 1 proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask a AND mask b = mask (min a b)
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND w = 0) = (x AND NOT w = x) proof (prove)
using this:
(x AND w) + (x AND NOT w) = x

goal (1 subgoal):
 1. (x AND w = 0) = (x AND NOT w = x)
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND w = x) = (x AND NOT w = 0) proof (prove)
using this:
(x AND w) + (x AND NOT w) = x

goal (1 subgoal):
 1. (x AND w = x) = (x AND NOT w = 0)
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT 1 = - 2
theory More_Word

lemma split_word_eq_on_mask:
  "(x = y) = (x AND m = y AND m \<and> x AND NOT m = y AND NOT m)"
  for x y m :: \<open>'a::len word\<close> apply transfer apply (simp add: bit_eq_iff) apply (auto simp add: bit_simps ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x = y) = (x AND m = y AND m \<and> x AND NOT m = y AND NOT m) proof (prove)
goal (1 subgoal):
 1. \<And>x y m. (take_bit LENGTH('a) x = take_bit LENGTH('a) y) = (take_bit LENGTH('a) (x AND m) = take_bit LENGTH('a) (y AND m) \<and> take_bit LENGTH('a) (x AND NOT m) = take_bit LENGTH('a) (y AND NOT m)) proof (prove)
goal (1 subgoal):
 1. \<And>x y m. (\<forall>n. bit (take_bit LENGTH('a) x) n = bit (take_bit LENGTH('a) y) n) = ((\<forall>n. bit (take_bit LENGTH('a) x AND take_bit LENGTH('a) m) n = bit (take_bit LENGTH('a) y AND take_bit LENGTH('a) m) n) \<and> (\<forall>n. bit (take_bit LENGTH('a) x AND take_bit LENGTH('a) (NOT m)) n = bit (take_bit LENGTH('a) y AND take_bit LENGTH('a) (NOT m)) n)) proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 255 = mask 8
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 511 = mask 9
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ LENGTH('a) \<Longrightarrow> ucast (word_of_nat x) = word_of_nat x proof (prove)
goal (1 subgoal):
 1. \<And>x. x < 2 ^ LENGTH('a) \<Longrightarrow> take_bit LENGTH('b) (take_bit LENGTH('a) (int x)) = take_bit LENGTH('b) (int x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < 2 ^ LENGTH('a); LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) x = take_bit LENGTH('b) x proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<noteq> - 1 \<Longrightarrow> (x \<le> y) = (x < y + 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> - 1; x \<le> y\<rbrakk> \<Longrightarrow> x < y + 1 proof (prove)
goal (1 subgoal):
 1. y \<noteq> - 1 \<Longrightarrow> y + 1 \<noteq> 0 proof (prove)
goal:
No subgoals!
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {0..<1} = {0}
theory More_Word

lemma word_leq_minus_one_le:
  fixes x :: "'a::len word"
  shows "\<lbrakk>y \<noteq> 0; x \<le> y - 1 \<rbrakk> \<Longrightarrow> x < y" using le_m1_iff_lt word_neq_0_conv by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> 0; x \<le> y - 1\<rbrakk> \<Longrightarrow> x < y proof (prove)
using this:
(0 < ?x) = ((?y \<le> ?x - 1) = (?y < ?x))
(?w \<noteq> 0) = (0 < ?w)

goal (1 subgoal):
 1. \<lbrakk>y \<noteq> 0; x \<le> y - 1\<rbrakk> \<Longrightarrow> x < y
theory More_Word

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> {0..<n} = {0..<n - 1} \<union> {n - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n \<noteq> 0; x \<in> {0..<n}\<rbrakk> \<Longrightarrow> x \<in> {0..<n - 1} \<union> {n - 1}
 2. \<And>x. \<lbrakk>n \<noteq> 0; x \<in> {0..<n - 1} \<union> {n - 1}\<rbrakk> \<Longrightarrow> x \<in> {0..<n} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n \<noteq> 0; x < n\<rbrakk> \<Longrightarrow> x = n - 1 \<or> x < n - 1
 2. \<And>x. \<lbrakk>n \<noteq> 0; x \<in> {0..<n - 1} \<union> {n - 1}\<rbrakk> \<Longrightarrow> x \<in> {0..<n} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n \<noteq> 0; x \<le> n - 1\<rbrakk> \<Longrightarrow> x = n - 1 \<or> x < n - 1
 2. \<And>x. \<lbrakk>n \<noteq> 0; x \<in> {0..<n - 1} \<union> {n - 1}\<rbrakk> \<Longrightarrow> x \<in> {0..<n} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n \<noteq> 0; x \<le> n - 1; \<not> x < n - 1\<rbrakk> \<Longrightarrow> x = n - 1
 2. \<And>x. \<lbrakk>n \<noteq> 0; x \<in> {0..<n - 1} \<union> {n - 1}\<rbrakk> \<Longrightarrow> x \<in> {0..<n} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n \<noteq> 0; x \<in> {0..<n - 1} \<union> {n - 1}\<rbrakk> \<Longrightarrow> x \<in> {0..<n} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n \<noteq> 0; x = n - 1 \<or> x < n - 1\<rbrakk> \<Longrightarrow> x < n proof (prove)
goal (1 subgoal):
 1. \<And>x. x = n - 1 \<or> x < n - 1 \<Longrightarrow> x \<le> n - 1 proof (prove)
goal:
No subgoals!