kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma word_sub_plus_one_nonzero:
  fixes n :: "'a :: len word"
  shows "\<lbrakk>n' \<le> n; n' \<noteq> 0\<rbrakk> \<Longrightarrow> (n - n') + 1 \<noteq> 0" apply (subst lt1_neq0 [symmetric]) apply (subst olen_add_eqv [symmetric]) apply (rule word_random [where x' = n']) apply simp apply (erule word_sub_le) apply (simp add: lt1_neq0) done

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

lemma word_le_minus_mono_right:
  fixes x :: "'a :: len word"
  shows "\<lbrakk> z \<le> y; y \<le> x; z \<le> x \<rbrakk> \<Longrightarrow> x - y \<le> x - z" apply (rule word_sub_mono) apply simp apply assumption apply (erule word_sub_le) apply (erule word_sub_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - y \<le> x - z proof (prove)
goal (4 subgoals):
 1. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x \<le> x
 2. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> z \<le> y
 3. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - y \<le> x
 4. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - z \<le> x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> z \<le> y
 2. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - y \<le> x
 3. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - z \<le> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - y \<le> x
 2. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - z \<le> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<le> y; y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> x - z \<le> x proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_0_sle_from_less:
  \<open>0 \<le>s x\<close> if \<open>x < 2 ^ (LENGTH('a) - 1)\<close> for x :: \<open>'a::len word\<close> using that apply transfer apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply (metis bit_take_bit_iff min_def nat_less_le not_less_eq take_bit_int_eq_self_iff take_bit_take_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le>s x proof (prove)
using this:
x < 2 ^ (LENGTH('a) - 1)

goal (1 subgoal):
 1. 0 \<le>s x proof (prove)
goal (1 subgoal):
 1. \<And>x. take_bit LENGTH('a) x < take_bit LENGTH('a) (2 ^ (LENGTH('a) - 1)) \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a) - Suc 0) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>take_bit LENGTH('a) x < take_bit LENGTH('a) (2 ^ (LENGTH('a) - 1)); LENGTH('a) = 0\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a) - Suc 0) x
 2. \<And>x nat. \<lbrakk>take_bit LENGTH('a) x < take_bit LENGTH('a) (2 ^ (LENGTH('a) - 1)); LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) 0 \<le> signed_take_bit (LENGTH('a) - Suc 0) x proof (prove)
goal (1 subgoal):
 1. \<And>x nat. \<lbrakk>take_bit (Suc nat) x < 2 ^ nat; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> \<not> bit x nat proof (prove)
goal:
No subgoals!
theory More_Word

lemma ucast_sub_ucast:
  fixes x :: "'a::len word"
  assumes "y \<le> x"
  assumes T: "LENGTH('a) \<le> LENGTH('b)"
  shows "ucast (x - y) = (ucast x - ucast y :: 'b::len word)" proof - from T have P: "unat x < 2 ^ LENGTH('b)" "unat y < 2 ^ LENGTH('b)" by (fastforce intro!: less_le_trans[OF unat_lt2p])+ then show ?thesis by (simp add: unat_arith_simps unat_ucast assms[simplified unat_arith_simps]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (x - y) = ucast x - ucast y proof (state)
goal (1 subgoal):
 1. ucast (x - y) = ucast x - ucast y proof (chain)
picking this:
LENGTH('a) \<le> LENGTH('b) proof (prove)
using this:
LENGTH('a) \<le> LENGTH('b)

goal (1 subgoal):
 1. unat x < 2 ^ LENGTH('b) &&& unat y < 2 ^ LENGTH('b) proof (state)
this:
unat x < 2 ^ LENGTH('b)
unat y < 2 ^ LENGTH('b)

goal (1 subgoal):
 1. ucast (x - y) = ucast x - ucast y proof (chain)
picking this:
unat x < 2 ^ LENGTH('b)
unat y < 2 ^ LENGTH('b) proof (prove)
using this:
unat x < 2 ^ LENGTH('b)
unat y < 2 ^ LENGTH('b)

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

goal:
No subgoals!
theory More_Word

lemma word_1_0:
  "\<lbrakk>a + (1::('a::len) word) \<le> b; a < of_nat x\<rbrakk> \<Longrightarrow> a < b" apply transfer apply (subst (asm) take_bit_incr_eq) apply (auto simp add: diff_less_eq) using take_bit_int_less_exp le_less_trans by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + 1 \<le> b; a < word_of_nat x\<rbrakk> \<Longrightarrow> a < b proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>take_bit LENGTH('a) (a + 1) \<le> take_bit LENGTH('a) b; take_bit LENGTH('a) a < take_bit LENGTH('a) (int x)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) a < take_bit LENGTH('a) b proof (prove)
goal (2 subgoals):
 1. \<And>a b x. take_bit LENGTH('a) a < take_bit LENGTH('a) (int x) \<Longrightarrow> take_bit LENGTH('a) a \<noteq> 2 ^ LENGTH('a) - 1
 2. \<And>a b x. \<lbrakk>1 + take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b; take_bit LENGTH('a) a < take_bit LENGTH('a) (int x)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) a < take_bit LENGTH('a) b proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>2 ^ LENGTH('a) \<le> take_bit LENGTH('a) (int x); take_bit LENGTH('a) a = 2 ^ LENGTH('a) - 1\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
take_bit ?n ?k < 2 ^ ?n
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. \<And>a x. \<lbrakk>2 ^ LENGTH('a) \<le> take_bit LENGTH('a) (int x); take_bit LENGTH('a) a = 2 ^ LENGTH('a) - 1\<rbrakk> \<Longrightarrow> False
theory More_Word

lemma unat_of_nat_less:"\<lbrakk> a < b; unat b = c \<rbrakk> \<Longrightarrow> a < of_nat c" by fastforce

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

lemma word_le_plus_1: "\<lbrakk> (y::('a::len) word) < y + n; a < n \<rbrakk> \<Longrightarrow> y + a \<le> y + a + 1" by unat_arith

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

lemma word_le_plus:"\<lbrakk>(a::('a::len) word) < a + b; c < b\<rbrakk> \<Longrightarrow> a \<le> a + c" by (metis order_less_imp_le word_random)

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

lemma sint_minus1 [simp]: "(sint x = -1) = (x = -1)" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply transfer apply (simp only: flip: signed_take_bit_eq_iff_take_bit_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sint x = - 1) = (x = - 1) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> (sint x = - 1) = (x = - 1)
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> (sint x = - 1) = (x = - 1) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> (sint x = - 1) = (x = - 1) proof (prove)
goal (1 subgoal):
 1. \<And>nat x. LENGTH('a) = Suc nat \<Longrightarrow> (signed_take_bit (LENGTH('a) - Suc 0) x = - 1) = (take_bit LENGTH('a) x = take_bit LENGTH('a) (- 1)) proof (prove)
goal (1 subgoal):
 1. \<And>nat x. LENGTH('a) = Suc nat \<Longrightarrow> (signed_take_bit (Suc nat - Suc 0) x = - 1) = (signed_take_bit nat x = signed_take_bit nat (- 1)) proof (prove)
goal:
No subgoals!
theory More_Word

lemma sint_0 [simp]: "(sint x = 0) = (x = 0)" by (fact signed_eq_0_iff)

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

lemma sint_1_cases:
  P if \<open>\<lbrakk> len_of TYPE ('a::len) = 1; (a::'a word) = 0; sint a = 0 \<rbrakk> \<Longrightarrow> P\<close>
     \<open>\<lbrakk> len_of TYPE ('a) = 1; a = 1; sint (1 :: 'a word) = -1 \<rbrakk> \<Longrightarrow> P\<close>
     \<open>\<lbrakk> len_of TYPE ('a) > 1; sint (1 :: 'a word) = 1 \<rbrakk> \<Longrightarrow> P\<close> proof (cases \<open>LENGTH('a) = 1\<close>) case True then have \<open>a = 0 \<or> a = 1\<close> by transfer auto with True that show ?thesis by auto next case False with that show ?thesis by (simp add: less_le Suc_le_eq) qed

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

goal (2 subgoals):
 1. LENGTH('a) = 1 \<Longrightarrow> P
 2. LENGTH('a) \<noteq> 1 \<Longrightarrow> P proof (chain)
picking this:
LENGTH('a) = 1 proof (prove)
using this:
LENGTH('a) = 1

goal (1 subgoal):
 1. a = 0 \<or> a = 1 proof (state)
this:
a = 0 \<or> a = 1

goal (2 subgoals):
 1. LENGTH('a) = 1 \<Longrightarrow> P
 2. LENGTH('a) \<noteq> 1 \<Longrightarrow> P proof (chain)
picking this:
LENGTH('a) = 1
\<lbrakk>LENGTH('a) = 1; a = 0; sint a = 0\<rbrakk> \<Longrightarrow> P
\<lbrakk>LENGTH('a) = 1; a = 1; sint 1 = - 1\<rbrakk> \<Longrightarrow> P
\<lbrakk>1 < LENGTH('a); sint 1 = 1\<rbrakk> \<Longrightarrow> P
a = 0 \<or> a = 1 proof (prove)
using this:
LENGTH('a) = 1
\<lbrakk>LENGTH('a) = 1; a = 0; sint a = 0\<rbrakk> \<Longrightarrow> P
\<lbrakk>LENGTH('a) = 1; a = 1; sint 1 = - 1\<rbrakk> \<Longrightarrow> P
\<lbrakk>1 < LENGTH('a); sint 1 = 1\<rbrakk> \<Longrightarrow> P
a = 0 \<or> a = 1

goal (1 subgoal):
 1. P proof (state)
this:
P

goal (1 subgoal):
 1. LENGTH('a) \<noteq> 1 \<Longrightarrow> P proof (state)
goal (1 subgoal):
 1. LENGTH('a) \<noteq> 1 \<Longrightarrow> P proof (state)
this:
LENGTH('a) \<noteq> 1

goal (1 subgoal):
 1. LENGTH('a) \<noteq> 1 \<Longrightarrow> P proof (chain)
picking this:
\<lbrakk>LENGTH('a) = 1; a = 0; sint a = 0\<rbrakk> \<Longrightarrow> P
\<lbrakk>LENGTH('a) = 1; a = 1; sint 1 = - 1\<rbrakk> \<Longrightarrow> P
\<lbrakk>1 < LENGTH('a); sint 1 = 1\<rbrakk> \<Longrightarrow> P
LENGTH('a) \<noteq> 1 proof (prove)
using this:
\<lbrakk>LENGTH('a) = 1; a = 0; sint a = 0\<rbrakk> \<Longrightarrow> P
\<lbrakk>LENGTH('a) = 1; a = 1; sint 1 = - 1\<rbrakk> \<Longrightarrow> P
\<lbrakk>1 < LENGTH('a); sint 1 = 1\<rbrakk> \<Longrightarrow> P
LENGTH('a) \<noteq> 1

goal (1 subgoal):
 1. P proof (state)
this:
P

goal:
No subgoals!
theory More_Word

lemma sint_int_min:
  "sint (- (2 ^ (LENGTH('a) - Suc 0)) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply transfer apply (simp add: signed_take_bit_int_eq_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (- (2 ^ (LENGTH('a) - Suc 0))) = - (2 ^ (LENGTH('a) - Suc 0)) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> sint (- (2 ^ (LENGTH('a) - Suc 0))) = - (2 ^ (LENGTH('a) - Suc 0))
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sint (- (2 ^ (LENGTH('a) - Suc 0))) = - (2 ^ (LENGTH('a) - Suc 0)) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sint (- (2 ^ nat)) = - (2 ^ nat) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) (- (2 ^ nat)) = - (2 ^ nat) proof (prove)
goal:
No subgoals!
theory More_Word

lemma sint_int_max_plus_1:
  "sint (2 ^ (LENGTH('a) - Suc 0) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply (subst word_of_int_2p [symmetric]) apply (subst int_word_sint) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (2 ^ (LENGTH('a) - Suc 0)) = - (2 ^ (LENGTH('a) - Suc 0)) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> sint (2 ^ (LENGTH('a) - Suc 0)) = - (2 ^ (LENGTH('a) - Suc 0))
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sint (2 ^ (LENGTH('a) - Suc 0)) = - (2 ^ (LENGTH('a) - Suc 0)) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sint (2 ^ nat) = - (2 ^ nat) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sint (word_of_int (2 ^ nat)) = - (2 ^ nat) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> (2 ^ nat + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1) = - (2 ^ nat) proof (prove)
goal:
No subgoals!
theory More_Word

lemma uint_range':
  \<open>0 \<le> uint x \<and> uint x < 2 ^ LENGTH('a)\<close>
  for x :: \<open>'a::len word\<close> by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> uint x \<and> uint x < 2 ^ LENGTH('a)
theory More_Word

lemma sint_of_int_eq:
  "\<lbrakk> - (2 ^ (LENGTH('a) - 1)) \<le> x; x < 2 ^ (LENGTH('a) - 1) \<rbrakk> \<Longrightarrow> sint (of_int x :: ('a::len) word) = x" by (simp add: signed_take_bit_int_eq_self signed_of_int)

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

lemma of_int_sint:
  "of_int (sint a) = a" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_int (sint a) = a
theory More_Word

lemma sint_ucast_eq_uint:
    "\<lbrakk> \<not> is_down (ucast :: ('a::len word \<Rightarrow> 'b::len word)) \<rbrakk>
            \<Longrightarrow> sint ((ucast :: ('a::len word \<Rightarrow> 'b::len word)) x) = uint x" apply transfer apply (simp add: signed_take_bit_take_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_down ucast \<Longrightarrow> sint (ucast x) = uint x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> signed_take_bit (LENGTH('b) - Suc 0) (take_bit LENGTH('a) x) = take_bit LENGTH('a) x proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_less_nowrapI':
  "(x :: 'a :: len word) \<le> z - k \<Longrightarrow> k \<le> z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k" by uint_arith

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

lemma mask_plus_1:
  "mask n + 1 = (2 ^ n :: 'a::len word)" by (clarsimp simp: mask_eq_decr_exp)

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

lemma unat_inj: "inj unat" by (metis eq_iff injI word_le_nat_alt)

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

lemma unat_ucast_upcast:
  "is_up (ucast :: 'b word \<Rightarrow> 'a word)
      \<Longrightarrow> unat (ucast x :: ('a::len) word) = unat (x :: ('b::len) word)" unfolding ucast_eq unat_eq_nat_uint apply transfer apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up ucast \<Longrightarrow> unat (ucast x) = unat x proof (prove)
goal (1 subgoal):
 1. is_up (\<lambda>w. word_of_int (uint w)) \<Longrightarrow> nat (uint (word_of_int (uint x))) = nat (uint x) proof (prove)
goal (1 subgoal):
 1. \<And>x. LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> nat (take_bit LENGTH('a) (take_bit LENGTH('b) x)) = nat (take_bit LENGTH('b) x) proof (prove)
goal:
No subgoals!
theory More_Word

lemma ucast_mono:
  "\<lbrakk> (x :: 'b :: len word) < y; y < 2 ^ LENGTH('a) \<rbrakk>
   \<Longrightarrow> ucast x < ((ucast y) :: 'a :: len word)" apply (simp only: flip: ucast_nat_def) apply (rule of_nat_mono_maybe) apply (rule unat_less_helper) apply simp apply (simp add: word_less_nat_alt) done

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

lemma ucast_mono_le:
  "\<lbrakk>x \<le> y; y < 2 ^ LENGTH('b)\<rbrakk> \<Longrightarrow> (ucast (x :: 'a :: len word) :: 'b :: len word) \<le> ucast y" apply (simp only: flip: ucast_nat_def) apply (subst of_nat_mono_maybe_le[symmetric]) apply (rule unat_less_helper) apply simp apply (rule unat_less_helper) apply (erule le_less_trans) apply (simp_all add: word_le_nat_alt) done

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

lemma ucast_mono_le':
  "\<lbrakk> unat y < 2 ^ LENGTH('b); LENGTH('b::len) < LENGTH('a::len); x \<le> y \<rbrakk>
   \<Longrightarrow> ucast x \<le> (ucast y :: 'b word)" for x y :: \<open>'a::len word\<close> by (auto simp: word_less_nat_alt intro: ucast_mono_le)

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

lemma neg_mask_add_mask:
  "((x:: 'a :: len word) AND NOT (mask n)) + (2 ^ n - 1) = x OR mask n" unfolding mask_2pm1 [symmetric] apply (subst word_plus_and_or_coroll; rule bit_word_eqI) apply (auto simp add: bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND NOT (mask n)) + (2 ^ n - 1) = x OR mask n proof (prove)
goal (1 subgoal):
 1. (x AND NOT (mask n)) + mask n = x OR mask n proof (prove)
goal (2 subgoals):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit ((x AND NOT (mask n)) AND mask n) na = bit 0 na
 2. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (x AND NOT (mask n) OR mask n) na = bit (x OR mask n) na proof (prove)
goal:
No subgoals!
theory More_Word

lemma le_step_down_word:"\<lbrakk>(i::('a::len) word) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" by unat_arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory More_Word

lemma le_step_down_word_2:
  fixes x :: "'a::len word"
  shows "\<lbrakk>x \<le>  y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1" by (subst (asm) word_le_less_eq,
      clarsimp,
      simp add: word_le_minus_one_leq)

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

lemma NOT_mask_AND_mask[simp]: "(w AND mask n) AND NOT (mask n) = 0" by (rule bit_eqI) (simp add: bit_simps)

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

lemma ex_mask_1[simp]: "(\<exists>x. mask x = (1 :: 'a::len word))" apply (rule_tac x=1 in exI) apply (simp add:mask_eq_decr_exp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. mask x = 1 proof (prove)
goal (1 subgoal):
 1. mask 1 = 1 proof (prove)
goal:
No subgoals!
theory More_Word

lemma not_switch:"NOT a = x \<Longrightarrow> a = NOT x" by auto

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

lemma test_bit_eq_iff: "bit u = bit v \<longleftrightarrow> u = v"
  for u v :: "'a::len word" by (auto intro: bit_eqI simp add: fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (bit u = bit v) = (u = v)
theory More_Word

lemma test_bit_size: "bit w n \<Longrightarrow> n < size w"
  for w :: "'a::len word" by transfer simp

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

lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). bit x n = bit y n)"
  for x y :: "'a::len word" by transfer (auto simp add: bit_eq_iff bit_take_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x = y) = (\<forall>n<LENGTH('a). bit x n = bit y n)
theory More_Word

lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> bit u n = bit v n) \<Longrightarrow> u = v"
  for u :: "'a::len word" by (simp add: word_size word_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n < size u \<longrightarrow> bit u n = bit v n) \<Longrightarrow> u = v
theory More_Word

lemma word_eqD: "u = v \<Longrightarrow> bit u x = bit v x"
  for u v :: "'a::len word" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. u = v \<Longrightarrow> bit u x = bit v x
theory More_Word

lemma test_bit_bin': "bit w n \<longleftrightarrow> n < size w \<and> bit (uint w) n" by transfer (simp add: bit_take_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit w n = (n < size w \<and> bit (uint w) n)
theory More_Word

lemma word_test_bit_def:
  \<open>bit a = bit (uint a)\<close> by transfer (simp add: fun_eq_iff bit_take_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit a = bit (uint a)
theory More_Word

lemma word_test_bit_transfer [transfer_rule]:
  "(rel_fun pcr_word (rel_fun (=) (=)))
    (\<lambda>x n. n < LENGTH('a) \<and> bit x n) (bit :: 'a::len word \<Rightarrow> _)" by transfer_prover

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_fun pcr_word (rel_fun (=) (=)) (\<lambda>x n. n < LENGTH('a) \<and> bit x n) bit