kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma word_minus_one_le_leq:
  "\<lbrakk> x - 1 < y \<rbrakk> \<Longrightarrow> x \<le> (y :: 'a :: len word)" apply (cases "x = 0") apply simp apply (simp add: word_less_nat_alt word_le_nat_alt) apply (subst(asm) unat_minus_one) apply (simp add: word_less_nat_alt) apply (cases "unat x") apply (simp add: unat_eq_zero) apply arith done

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

lemma word_must_wrap:
  "\<lbrakk> x \<le> n - 1; n \<le> x \<rbrakk> \<Longrightarrow> n = (0 :: 'a :: len word)" using dual_order.trans sub_wrap word_less_1 by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> n - 1; n \<le> x\<rbrakk> \<Longrightarrow> n = 0 proof (prove)
using this:
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
(?x \<le> ?x - ?z) = (?z = 0 \<or> ?x < ?z)
(?x < 1) = (?x = 0)

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

lemma range_subset_card:
  "\<lbrakk> {a :: 'a :: len word .. b} \<subseteq> {c .. d}; b \<ge> a \<rbrakk> \<Longrightarrow> d \<ge> c \<and> d - c \<ge> b - a" using word_sub_le word_sub_mono by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; a \<le> b\<rbrakk> \<Longrightarrow> c \<le> d \<and> b - a \<le> d - c proof (prove)
using this:
?y \<le> ?x \<Longrightarrow> ?x - ?y \<le> ?x
\<lbrakk>?a \<le> ?c; ?d \<le> ?b; ?a - ?b \<le> ?a; ?c - ?d \<le> ?c\<rbrakk> \<Longrightarrow> ?a - ?b \<le> ?c - ?d

goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; a \<le> b\<rbrakk> \<Longrightarrow> c \<le> d \<and> b - a \<le> d - c
theory More_Word

lemma word_power_mod_div:
  fixes x :: "'a::len word"
  shows "\<lbrakk> n < LENGTH('a); m < LENGTH('a)\<rbrakk>
  \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)" apply (simp add: word_arith_nat_div unat_mod power_mod_div) apply (subst unat_arith_simps(3)) apply (subst unat_mod) apply (subst unat_of_nat)+ apply (simp add: mod_mod_power min.commute) done

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

lemma word_range_minus_1':
  fixes a :: "'a :: len word"
  shows "a \<noteq> 0 \<Longrightarrow> {a - 1<..b} = {a..b}" by (simp add: greaterThanAtMost_def atLeastAtMost_def greaterThan_def atLeast_def less_1_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> {a - 1<..b} = {a..b}
theory More_Word

lemma word_range_minus_1:
  fixes a :: "'a :: len word"
  shows "b \<noteq> 0 \<Longrightarrow> {a..b - 1} = {a..<b}" apply (simp add: atLeastLessThan_def atLeastAtMost_def atMost_def lessThan_def) apply (rule arg_cong [where f = "\<lambda>x. {a..} \<inter> x"]) apply rule apply clarsimp apply (erule contrapos_pp) apply (simp add: linorder_not_less linorder_not_le word_must_wrap) apply (clarsimp) apply (drule word_le_minus_one_leq) apply (auto simp: word_less_sub_1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> {a..b - 1} = {a..<b} proof (prove)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> {a..} \<inter> {x. x \<le> b - 1} = {a..} \<inter> {x. x < b} proof (prove)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> {x. x \<le> b - 1} = {x. x < b} proof (prove)
goal (2 subgoals):
 1. b \<noteq> 0 \<Longrightarrow> {x. x \<le> b - 1} \<subseteq> {x. x < b}
 2. b \<noteq> 0 \<Longrightarrow> {x. x < b} \<subseteq> {x. x \<le> b - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>b \<noteq> 0; x \<le> b - 1\<rbrakk> \<Longrightarrow> x < b
 2. b \<noteq> 0 \<Longrightarrow> {x. x < b} \<subseteq> {x. x \<le> b - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> b - 1; \<not> x < b\<rbrakk> \<Longrightarrow> \<not> b \<noteq> 0
 2. b \<noteq> 0 \<Longrightarrow> {x. x < b} \<subseteq> {x. x \<le> b - 1} proof (prove)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> {x. x < b} \<subseteq> {x. x \<le> b - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>b \<noteq> 0; x < b\<rbrakk> \<Longrightarrow> x \<le> b - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>b \<noteq> 0; x \<le> b - 1\<rbrakk> \<Longrightarrow> x \<le> b - 1 proof (prove)
goal:
No subgoals!
theory More_Word

lemma ucast_nat_def:
  "of_nat (unat x) = (ucast :: 'a :: len word \<Rightarrow> 'b :: len word) x" by transfer simp

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

lemma overflow_plus_one_self:
  "(1 + p \<le> p) = (p = (-1 :: 'a :: len word))" apply rule apply (rule ccontr) apply (drule plus_one_helper2) apply (rule notI) apply (drule arg_cong[where f="\<lambda>x. x - 1"]) apply simp apply (simp add: field_simps) apply simp done

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

lemma plus_1_less:
  "(x + 1 \<le> (x :: 'a :: len word)) = (x = -1)" apply (rule iffI) apply (rule ccontr) apply (cut_tac plus_one_helper2[where x=x, OF order_refl]) apply simp apply clarsimp apply (drule arg_cong[where f="\<lambda>x. x - 1"]) apply simp apply simp done

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

lemma pos_mult_pos_ge:
  "[|x > (0::int); n>=0 |] ==> n * x >= n*1" apply (simp only: mult_left_mono) done

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

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

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

lemma word_div_mult:
  "0 < c \<Longrightarrow> a < b * c \<Longrightarrow> a div c < b" for a b c :: "'a::len word" by (rule classical)
     (use div_to_mult_word_lt [of b a c] in
      \<open>auto simp add: word_less_nat_alt word_le_nat_alt unat_div\<close>)

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

lemma word_less_power_trans_ofnat:
  "\<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk>
   \<Longrightarrow> of_nat n * 2 ^ k < (2::'a::len word) ^ m" apply (subst mult.commute) apply (rule word_less_power_trans) apply (simp_all add: word_less_nat_alt unsigned_of_nat) using take_bit_nat_less_eq_self apply (rule le_less_trans) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat n * 2 ^ k < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ k * word_of_nat n < 2 ^ m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ (m - k)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> m
 3. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> m < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) n < 2 ^ (m - k) proof (prove)
using this:
take_bit ?n ?m \<le> ?m

goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) n < 2 ^ (m - k) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> n < 2 ^ (m - k) proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_1_le_power:
  "n < LENGTH('a) \<Longrightarrow> (1 :: 'a :: len word) \<le> 2 ^ n" by (rule inc_le[where i=0, simplified], erule iffD2[OF p2_gt_0])

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

lemma unat_1_0:
  "1 \<le> (x::'a::len word) = (0 < unat x)" by (auto simp add: word_le_nat_alt)

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

lemma x_less_2_0_1':
  fixes x :: "'a::len word"
  shows "\<lbrakk>LENGTH('a) \<noteq> 1; x < 2\<rbrakk> \<Longrightarrow> x = 0 \<or> x = 1" apply (cases \<open>2 \<le> LENGTH('a)\<close>; simp) apply transfer apply clarsimp apply (metis add.commute add.right_neutral even_two_times_div_two mod_div_trivial
               mod_pos_pos_trivial mult.commute mult_zero_left not_less not_take_bit_negative
               odd_two_times_div_two_succ) done

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

lemma of_nat_n_less_equal_power_2:
  "n < LENGTH('a::len) \<Longrightarrow> ((of_nat n)::'a word) < 2 ^ n" apply (induct n) apply clarsimp apply clarsimp apply (metis of_nat_power n_less_equal_power_2 of_nat_Suc power_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat n < 2 ^ n proof (prove)
goal (2 subgoals):
 1. 0 < LENGTH('a) \<Longrightarrow> word_of_nat 0 < 2 ^ 0
 2. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> word_of_nat n < 2 ^ n; Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat (Suc n) < 2 ^ Suc n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a) \<Longrightarrow> word_of_nat n < 2 ^ n; Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat (Suc n) < 2 ^ Suc n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>word_of_nat n < 2 ^ n; Suc n < LENGTH('a)\<rbrakk> \<Longrightarrow> 1 + word_of_nat n < 2 * 2 ^ n proof (prove)
goal:
No subgoals!
theory More_Word

lemma eq_mask_less:
  fixes w :: "'a::len word"
  assumes eqm: "w = w AND mask n"
  and      sz: "n < len_of TYPE ('a)"
  shows "w < (2::'a word) ^ n" by (subst eqm, rule and_mask_less' [OF sz])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w < 2 ^ n
theory More_Word

lemma of_nat_mono_maybe':
  fixes Y :: "nat"
  assumes xlt: "x < 2 ^ len_of TYPE ('a)"
  assumes ylt: "y < 2 ^ len_of TYPE ('a)"
  shows   "(y < x) = (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 (rule ylt) apply (subst mod_less) apply (rule xlt) apply simp done

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

lemma of_nat_mono_maybe_le:
  "\<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow>
  (y \<le> x) = ((of_nat y :: 'a :: len word) \<le> of_nat x)" apply (clarsimp simp: le_less) apply (rule disj_cong) apply (rule of_nat_mono_maybe', assumption+) apply auto using of_nat_inj apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (y \<le> x) = (word_of_nat y \<le> word_of_nat x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (y < x \<or> y = x) = (word_of_nat y < word_of_nat x \<or> word_of_nat y = word_of_nat x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (y < x) = (word_of_nat y < word_of_nat x)
 2. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a); \<not> word_of_nat y < word_of_nat x\<rbrakk> \<Longrightarrow> (y = x) = (word_of_nat y = word_of_nat x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a); \<not> word_of_nat y < word_of_nat x\<rbrakk> \<Longrightarrow> (y = x) = (word_of_nat y = word_of_nat x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a); word_of_nat y = word_of_nat x\<rbrakk> \<Longrightarrow> y = x proof (prove)
using this:
\<lbrakk>?x < 2 ^ LENGTH(?'a); ?y < 2 ^ LENGTH(?'a)\<rbrakk> \<Longrightarrow> (word_of_nat ?x = word_of_nat ?y) = (?x = ?y)

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

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

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

lemma AND_NOT_mask_plus_AND_mask_eq:
  "(w AND NOT (mask n)) + (w AND mask n) = w"
  for w :: \<open>'a::len word\<close> apply (subst disjunctive_add) apply (auto simp add: bit_simps) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) done

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

lemma mask_eqI:
  fixes x :: "'a :: len word"
  assumes m1: "x AND mask n = y AND mask n"
  and     m2: "x AND NOT (mask n) = y AND NOT (mask n)"
  shows "x = y" proof - have *: \<open>x = x AND mask n OR x AND NOT (mask n)\<close> for x :: \<open>'a word\<close> by (rule bit_word_eqI) (auto simp add: bit_simps) from assms * [of x] * [of y] show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (state)
goal (1 subgoal):
 1. x = y proof (prove)
goal (1 subgoal):
 1. x = x AND mask n OR x AND NOT (mask n) proof (state)
this:
?x = ?x AND mask n OR ?x AND NOT (mask n)

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
x AND mask n = y AND mask n
x AND NOT (mask n) = y AND NOT (mask n)
x = x AND mask n OR x AND NOT (mask n)
y = y AND mask n OR y AND NOT (mask n) proof (prove)
using this:
x AND mask n = y AND mask n
x AND NOT (mask n) = y AND NOT (mask n)
x = x AND mask n OR x AND NOT (mask n)
y = y AND mask n OR y AND NOT (mask n)

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

goal:
No subgoals!
theory More_Word

lemma neq_0_no_wrap:
  fixes x :: "'a :: len word"
  shows "\<lbrakk> x \<le> x + y; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x + y \<noteq> 0" by clarsimp

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

lemma word_of_nat_le:
  "n \<le> unat x \<Longrightarrow> of_nat n \<le> x" apply (simp add: word_le_nat_alt unat_of_nat) apply (erule order_trans[rotated]) apply (simp add: take_bit_eq_mod) done

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

lemma word_unat_less_le:
  "a \<le> of_nat b \<Longrightarrow> unat a \<le> b" by (metis eq_iff le_cases le_unat_uoi word_of_nat_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> word_of_nat b \<Longrightarrow> unat a \<le> b
theory More_Word

lemma mask_Suc_0 : "mask (Suc 0) = (1 :: 'a::len word)" by (simp add: mask_eq_decr_exp)

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

lemma bool_mask':
  fixes x :: "'a :: len word"
  shows "2 < LENGTH('a) \<Longrightarrow> (0 < x AND 1) = (x AND 1 = 1)" by (simp add: and_one_eq mod_2_eq_odd)

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

lemma ucast_ucast_add:
  fixes x :: "'a :: len word"
  fixes y :: "'b :: len word"
  shows
  "LENGTH('b) \<ge> LENGTH('a) \<Longrightarrow>
    ucast (ucast x + y) = x + ucast y" apply transfer apply simp apply (subst (2) take_bit_add [symmetric]) apply (subst take_bit_add [symmetric]) apply simp done

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

lemma lt1_neq0:
  fixes x :: "'a :: len word"
  shows "(1 \<le> x) = (x \<noteq> 0)" by unat_arith

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

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

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