kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma of_nat_mono_maybe:
  assumes xlt: "x < 2 ^ len_of TYPE ('a)"
  shows   "y < x \<Longrightarrow> of_nat y < (of_nat x :: 'a :: len word)" apply (subst word_less_nat_alt) apply (subst unat_of_nat)+ apply (subst mod_less) apply (erule order_less_trans [OF _ xlt]) apply (subst mod_less [OF xlt]) apply assumption done

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

lemma word_and_max_word:
  fixes a::"'a::len word"
  shows "x = - 1 \<Longrightarrow> a AND x = a" by simp

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

lemma word_and_full_mask_simp:
  \<open>x AND mask LENGTH('a) = x\<close> for x :: \<open>'a::len word\<close> by (simp add: bit_eq_iff bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND mask LENGTH('a) = x
theory More_Word

lemma of_int_uint:
  "of_int (uint x) = x" by (fact word_of_int_uint)

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

lemma unat_mask_eq:
  \<open>unat (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close> by transfer (simp add: nat_mask_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (mask n) = mask (min LENGTH('a) n)
theory More_Word

lemma word_plus_mono_left:
  fixes x :: "'a :: len word"
  shows "\<lbrakk>y \<le> z; x \<le> x + z\<rbrakk> \<Longrightarrow> y + x \<le> z + x" by unat_arith

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

lemma less_Suc_unat_less_bound:
  "n < Suc (unat (x :: 'a :: len word)) \<Longrightarrow> n < 2 ^ LENGTH('a)" by (auto elim!: order_less_le_trans intro: Suc_leI)

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

lemma up_ucast_inj:
  "\<lbrakk> ucast x = (ucast y::'b::len word); LENGTH('a) \<le> len_of TYPE ('b) \<rbrakk> \<Longrightarrow> x = (y::'a::len word)" by transfer (simp add: min_def split: if_splits)

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

lemma up_ucast_inj_eq:
  "LENGTH('a) \<le> len_of TYPE ('b) \<Longrightarrow> (ucast x = (ucast y::'b::len word)) = (x = (y::'a::len word))" by (fastforce dest: up_ucast_inj)

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

lemma no_plus_overflow_neg:
  "(x :: 'a :: len word) < -y \<Longrightarrow> x \<le> x + y" by (metis diff_minus_eq_add less_imp_le sub_wrap_lt)

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

lemma ucast_ucast_eq:
  "\<lbrakk> ucast x = (ucast (ucast y::'a word)::'c::len word); LENGTH('a) \<le> LENGTH('b);
     LENGTH('b) \<le> LENGTH('c) \<rbrakk> \<Longrightarrow>
   x = ucast y" for x :: "'a::len word" and y :: "'b::len word" apply transfer apply (cases \<open>LENGTH('c) = LENGTH('a)\<close>) apply (auto simp add: min_def) done

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

lemma ucast_0_I:
  "x = 0 \<Longrightarrow> ucast x = 0" by simp

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

lemma  word_less_power_trans2:
  fixes n :: "'a::len word"
  shows "\<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> n * 2 ^ k < 2 ^ m" by (subst field_simps, rule word_less_power_trans)

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

lemma Suc_unat_diff_1:
  fixes x :: "'a :: len word"
  assumes lt: "1 \<le> x"
  shows "Suc (unat (x - 1)) = unat x" proof - have "0 < unat x" by (rule order_less_le_trans [where y = 1], simp, subst unat_1 [symmetric],
        rule iffD1 [OF word_le_nat_alt lt]) then show ?thesis by ((subst unat_sub [OF lt])+, simp only:  unat_1) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc (unat (x - 1)) = unat x proof (state)
goal (1 subgoal):
 1. Suc (unat (x - 1)) = unat x proof (prove)
goal (1 subgoal):
 1. 0 < unat x proof (state)
this:
0 < unat x

goal (1 subgoal):
 1. Suc (unat (x - 1)) = unat x proof (chain)
picking this:
0 < unat x proof (prove)
using this:
0 < unat x

goal (1 subgoal):
 1. Suc (unat (x - 1)) = unat x proof (state)
this:
Suc (unat (x - 1)) = unat x

goal:
No subgoals!
theory More_Word

lemma word_eq_unatI:
  \<open>v = w\<close> if \<open>unat v = unat w\<close> using that by transfer (simp add: nat_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v = w proof (prove)
using this:
unat v = unat w

goal (1 subgoal):
 1. v = w
theory More_Word

lemma word_mult_less_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i < j"
  and    knz: "0 < k"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "i * k < j * k" proof - from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)" by (auto intro: order_less_subst2 simp: word_less_nat_alt elim: mult_less_mono1) then show ?thesis using ujk knz ij by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i * k < j * k proof (state)
goal (1 subgoal):
 1. i * k < j * k proof (chain)
picking this:
i < j
unat j * unat k < 2 ^ LENGTH('a)
0 < k proof (prove)
using this:
i < j
unat j * unat k < 2 ^ LENGTH('a)
0 < k

goal (1 subgoal):
 1. unat i * unat k < 2 ^ LENGTH('a) proof (state)
this:
unat i * unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i * k < j * k proof (chain)
picking this:
unat i * unat k < 2 ^ LENGTH('a) proof (prove)
using this:
unat i * unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i * k < j * k proof (prove)
using this:
unat i * unat k < 2 ^ LENGTH('a)
unat j * unat k < 2 ^ LENGTH('a)
0 < k
i < j

goal (1 subgoal):
 1. i * k < j * k proof (state)
this:
i * k < j * k

goal:
No subgoals!
theory More_Word

lemma word_mult_less_dest:
  fixes i :: "'a :: len word"
  assumes ij: "i * k < j * k"
  and    uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "i < j" using uik ujk ij by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem] elim: mult_less_mono1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < j proof (prove)
using this:
unat i * unat k < 2 ^ LENGTH('a)
unat j * unat k < 2 ^ LENGTH('a)
i * k < j * k

goal (1 subgoal):
 1. i < j
theory More_Word

lemma word_mult_less_cancel:
  fixes k :: "'a :: len word"
  assumes knz: "0 < k"
  and    uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows "(i * k < j * k) = (i < j)" by (rule iffI [OF word_mult_less_dest [OF _ uik ujk] word_mult_less_mono1 [OF _ knz ujk]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (i * k < j * k) = (i < j)
theory More_Word

lemma enum_word_nth_eq:
  \<open>(Enum.enum :: 'a::len word list) ! n = word_of_nat n\<close>
    if \<open>n < 2 ^ LENGTH('a)\<close>
    for n using that by (simp add: enum_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enum_class.enum ! n = word_of_nat n proof (prove)
using this:
n < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. enum_class.enum ! n = word_of_nat n
theory More_Word

lemma length_enum_word_eq:
  \<open>length (Enum.enum :: 'a::len word list) = 2 ^ LENGTH('a)\<close> by (simp add: enum_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length enum_class.enum = 2 ^ LENGTH('a)
theory More_Word

lemma unat_lt2p [iff]:
  \<open>unat x < 2 ^ LENGTH('a)\<close> for x :: \<open>'a::len word\<close> by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH('a)
theory More_Word

lemma Suc_unat_minus_one [simp]:
  "x \<noteq> 0 \<Longrightarrow> Suc (unat (x - 1)) = unat x" by (metis Suc_diff_1 unat_gt_0 unat_minus_one)

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

lemma word_add_le_dest:
  fixes i :: "'a :: len word"
  assumes le: "i + k \<le> j + k"
  and    uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i \<le> j" using uik ujk le by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem] elim: add_le_mono1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i \<le> j proof (prove)
using this:
unat i + unat k < 2 ^ LENGTH('a)
unat j + unat k < 2 ^ LENGTH('a)
i + k \<le> j + k

goal (1 subgoal):
 1. i \<le> j
theory More_Word

lemma word_add_le_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i \<le> j"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i + k \<le> j + k" proof - from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)" by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: add_le_mono1) then show ?thesis using ujk ij by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i + k \<le> j + k proof (state)
goal (1 subgoal):
 1. i + k \<le> j + k proof (chain)
picking this:
i \<le> j
unat j + unat k < 2 ^ LENGTH('a) proof (prove)
using this:
i \<le> j
unat j + unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat i + unat k < 2 ^ LENGTH('a) proof (state)
this:
unat i + unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i + k \<le> j + k proof (chain)
picking this:
unat i + unat k < 2 ^ LENGTH('a) proof (prove)
using this:
unat i + unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i + k \<le> j + k proof (prove)
using this:
unat i + unat k < 2 ^ LENGTH('a)
unat j + unat k < 2 ^ LENGTH('a)
i \<le> j

goal (1 subgoal):
 1. i + k \<le> j + k proof (state)
this:
i + k \<le> j + k

goal:
No subgoals!
theory More_Word

lemma word_add_le_mono2:
  fixes i :: "'a :: len word"
  shows "\<lbrakk>i \<le> j; unat j + unat k < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> k + i \<le> k + j" by (subst field_simps, subst field_simps, erule (1) word_add_le_mono1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; unat j + unat k < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> k + i \<le> k + j
theory More_Word

lemma word_add_le_iff:
  fixes i :: "'a :: len word"
  assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i + k \<le> j + k) = (i \<le> j)" proof assume "i \<le> j" show "i + k \<le> j + k" by (rule word_add_le_mono1) fact+ next assume "i + k \<le> j + k" show "i \<le> j" by (rule word_add_le_dest) fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (i + k \<le> j + k) = (i \<le> j) proof (state)
goal (2 subgoals):
 1. i + k \<le> j + k \<Longrightarrow> i \<le> j
 2. i \<le> j \<Longrightarrow> i + k \<le> j + k proof (state)
this:
i \<le> j

goal (2 subgoals):
 1. i + k \<le> j + k \<Longrightarrow> i \<le> j
 2. i \<le> j \<Longrightarrow> i + k \<le> j + k proof (prove)
goal (1 subgoal):
 1. i + k \<le> j + k proof (state)
this:
i + k \<le> j + k

goal (1 subgoal):
 1. i + k \<le> j + k \<Longrightarrow> i \<le> j proof (state)
goal (1 subgoal):
 1. i + k \<le> j + k \<Longrightarrow> i \<le> j proof (state)
this:
i + k \<le> j + k

goal (1 subgoal):
 1. i + k \<le> j + k \<Longrightarrow> i \<le> j proof (prove)
goal (1 subgoal):
 1. i \<le> j proof (state)
this:
i \<le> j

goal:
No subgoals!
theory More_Word

lemma word_add_less_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i < j"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i + k < j + k" proof - from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)" by (auto elim: order_le_less_subst2 simp: word_less_nat_alt elim: add_less_mono1) then show ?thesis using ujk ij by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i + k < j + k proof (state)
goal (1 subgoal):
 1. i + k < j + k proof (chain)
picking this:
i < j
unat j + unat k < 2 ^ LENGTH('a) proof (prove)
using this:
i < j
unat j + unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat i + unat k < 2 ^ LENGTH('a) proof (state)
this:
unat i + unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i + k < j + k proof (chain)
picking this:
unat i + unat k < 2 ^ LENGTH('a) proof (prove)
using this:
unat i + unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i + k < j + k proof (prove)
using this:
unat i + unat k < 2 ^ LENGTH('a)
unat j + unat k < 2 ^ LENGTH('a)
i < j

goal (1 subgoal):
 1. i + k < j + k proof (state)
this:
i + k < j + k

goal:
No subgoals!
theory More_Word

lemma word_add_less_dest:
  fixes i :: "'a :: len word"
  assumes le: "i + k < j + k"
  and    uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "i < j" using uik ujk le by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem] elim: add_less_mono1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < j proof (prove)
using this:
unat i + unat k < 2 ^ LENGTH('a)
unat j + unat k < 2 ^ LENGTH('a)
i + k < j + k

goal (1 subgoal):
 1. i < j
theory More_Word

lemma word_add_less_iff:
  fixes i :: "'a :: len word"
  assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i + k < j + k) = (i < j)" proof assume "i < j" show "i + k < j + k" by (rule word_add_less_mono1) fact+ next assume "i + k < j + k" show "i < j" by (rule word_add_less_dest) fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (i + k < j + k) = (i < j) proof (state)
goal (2 subgoals):
 1. i + k < j + k \<Longrightarrow> i < j
 2. i < j \<Longrightarrow> i + k < j + k proof (state)
this:
i < j

goal (2 subgoals):
 1. i + k < j + k \<Longrightarrow> i < j
 2. i < j \<Longrightarrow> i + k < j + k proof (prove)
goal (1 subgoal):
 1. i + k < j + k proof (state)
this:
i + k < j + k

goal (1 subgoal):
 1. i + k < j + k \<Longrightarrow> i < j proof (state)
goal (1 subgoal):
 1. i + k < j + k \<Longrightarrow> i < j proof (state)
this:
i + k < j + k

goal (1 subgoal):
 1. i + k < j + k \<Longrightarrow> i < j proof (prove)
goal (1 subgoal):
 1. i < j proof (state)
this:
i < j

goal:
No subgoals!
theory More_Word

lemma word_mult_less_iff:
  fixes i :: "'a :: len word"
  assumes knz: "0 < k"
  and     uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i * k < j * k) = (i < j)" using assms by (rule word_mult_less_cancel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (i * k < j * k) = (i < j) proof (prove)
using this:
0 < k
unat i * unat k < 2 ^ LENGTH('a)
unat j * unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. (i * k < j * k) = (i < j)
theory More_Word

lemma word_le_imp_diff_le:
  fixes n :: "'a::len word"
  shows "\<lbrakk>k \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> n - k \<le> m" by (auto simp: unat_sub word_le_nat_alt)

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

lemma word_less_imp_diff_less:
  fixes n :: "'a::len word"
  shows "\<lbrakk>k \<le> n; n < m\<rbrakk> \<Longrightarrow> n - k < m" by (clarsimp simp: unat_sub word_less_nat_alt
             intro!: less_imp_diff_less)

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

lemma word_mult_le_mono1:
  fixes i :: "'a :: len word"
  assumes ij: "i \<le> j"
  and    knz: "0 < k"
  and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "i * k \<le> j * k" proof - from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)" by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: mult_le_mono1) then show ?thesis using ujk knz ij by (auto simp: word_le_nat_alt iffD1 [OF unat_mult_lem]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i * k \<le> j * k proof (state)
goal (1 subgoal):
 1. i * k \<le> j * k proof (chain)
picking this:
i \<le> j
unat j * unat k < 2 ^ LENGTH('a)
0 < k proof (prove)
using this:
i \<le> j
unat j * unat k < 2 ^ LENGTH('a)
0 < k

goal (1 subgoal):
 1. unat i * unat k < 2 ^ LENGTH('a) proof (state)
this:
unat i * unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i * k \<le> j * k proof (chain)
picking this:
unat i * unat k < 2 ^ LENGTH('a) proof (prove)
using this:
unat i * unat k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. i * k \<le> j * k proof (prove)
using this:
unat i * unat k < 2 ^ LENGTH('a)
unat j * unat k < 2 ^ LENGTH('a)
0 < k
i \<le> j

goal (1 subgoal):
 1. i * k \<le> j * k proof (state)
this:
i * k \<le> j * k

goal:
No subgoals!
theory More_Word

lemma word_mult_le_iff:
  fixes i :: "'a :: len word"
  assumes knz: "0 < k"
  and     uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
  and     ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
  shows  "(i * k \<le> j * k) = (i \<le> j)" proof assume "i \<le> j" show "i * k \<le> j * k" by (rule word_mult_le_mono1) fact+ next assume p: "i * k \<le> j * k" have "0 < unat k" using knz by (simp add: word_less_nat_alt) then show "i \<le> j" using p by (clarsimp simp: word_le_nat_alt iffD1 [OF unat_mult_lem uik]
      iffD1 [OF unat_mult_lem ujk]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (i * k \<le> j * k) = (i \<le> j) proof (state)
goal (2 subgoals):
 1. i * k \<le> j * k \<Longrightarrow> i \<le> j
 2. i \<le> j \<Longrightarrow> i * k \<le> j * k proof (state)
this:
i \<le> j

goal (2 subgoals):
 1. i * k \<le> j * k \<Longrightarrow> i \<le> j
 2. i \<le> j \<Longrightarrow> i * k \<le> j * k proof (prove)
goal (1 subgoal):
 1. i * k \<le> j * k proof (state)
this:
i * k \<le> j * k

goal (1 subgoal):
 1. i * k \<le> j * k \<Longrightarrow> i \<le> j proof (state)
goal (1 subgoal):
 1. i * k \<le> j * k \<Longrightarrow> i \<le> j proof (state)
this:
i * k \<le> j * k

goal (1 subgoal):
 1. i * k \<le> j * k \<Longrightarrow> i \<le> j proof (prove)
goal (1 subgoal):
 1. 0 < unat k proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. 0 < unat k proof (state)
this:
0 < unat k

goal (1 subgoal):
 1. i * k \<le> j * k \<Longrightarrow> i \<le> j proof (chain)
picking this:
0 < unat k proof (prove)
using this:
0 < unat k

goal (1 subgoal):
 1. i \<le> j proof (prove)
using this:
0 < unat k
i * k \<le> j * k

goal (1 subgoal):
 1. i \<le> j proof (state)
this:
i \<le> j

goal:
No subgoals!
theory More_Word

lemma word_diff_less:
  fixes n :: "'a :: len word"
  shows "\<lbrakk>0 < n; 0 < m; n \<le> m\<rbrakk> \<Longrightarrow> m - n < m" apply (subst word_less_nat_alt) apply (subst unat_sub) apply assumption apply (rule diff_less) apply (simp_all add: word_less_nat_alt) done

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

lemma word_add_increasing:
  fixes x :: "'a :: len word"
  shows "\<lbrakk> p + w \<le> x; p \<le> p + w \<rbrakk> \<Longrightarrow> p \<le> x" by unat_arith

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

lemma word_random:
  fixes x :: "'a :: len word"
  shows "\<lbrakk> p \<le> p + x'; x \<le> x' \<rbrakk> \<Longrightarrow> p \<le> p + x" by unat_arith

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

lemma word_sub_mono:
  "\<lbrakk> a \<le> c; d \<le> b; a - b \<le> a; c - d \<le> c \<rbrakk>
    \<Longrightarrow> (a - b) \<le> (c - d :: 'a :: len word)" by unat_arith

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

lemma power_not_zero:
  "n < LENGTH('a::len) \<Longrightarrow> (2 :: 'a word) ^ n \<noteq> 0" by (metis p2_gt_0 word_neq_0_conv)

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

lemma word_gt_a_gt_0:
  "a < n \<Longrightarrow> (0 :: 'a::len word) < n" apply (case_tac "n = 0") apply clarsimp apply (clarsimp simp: word_neq_0_conv) done

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

lemma word_power_less_1 [simp]:
  "sz < LENGTH('a::len) \<Longrightarrow> (2::'a word) ^ sz - 1 < 2 ^ sz" apply (simp add: word_less_nat_alt) apply (subst unat_minus_one) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz - 1 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz - 1) < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz \<noteq> 0
 2. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz) - 1 < 2 ^ sz proof (prove)
goal:
No subgoals!