kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma word_sub_1_le:
  "x \<noteq> 0 \<Longrightarrow> x - 1 \<le> (x :: 'a :: len word)" apply (subst no_ulen_sub) apply simp apply (cases "uint x = 0") apply (simp add: uint_0_iff) apply (insert uint_ge_0[where x=x]) apply arith done

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

lemma push_bit_word_eq_nonzero:
  \<open>push_bit n w \<noteq> 0\<close> if \<open>w < 2 ^ m\<close> \<open>m + n < LENGTH('a)\<close> \<open>w \<noteq> 0\<close>
    for w :: \<open>'a::len word\<close> using that apply (simp only: word_neq_0_conv word_less_nat_alt
                    mod_0 unat_word_ariths
                    unat_power_lower word_le_nat_alt) apply (metis add_diff_cancel_right' gr0I gr_implies_not0 less_or_eq_imp_le min_def push_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_push_bit take_bit_take_bit unsigned_push_bit_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_bit n w \<noteq> 0 proof (prove)
using this:
w < 2 ^ m
m + n < LENGTH('a)
w \<noteq> 0

goal (1 subgoal):
 1. push_bit n w \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat w < 2 ^ m; m + n < LENGTH('a); 0 < unat w\<rbrakk> \<Longrightarrow> 0 < unat (push_bit n w) proof (prove)
goal:
No subgoals!
theory More_Word

lemma unat_less_power:
  fixes k :: "'a::len word"
  assumes szv: "sz < LENGTH('a)"
  and     kv:  "k < 2 ^ sz"
  shows   "unat k < 2 ^ sz" using szv unat_mono [OF kv] by simp

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

goal (1 subgoal):
 1. unat k < 2 ^ sz
theory More_Word

lemma unat_mult_power_lem:
  assumes kv: "k < 2 ^ (LENGTH('a::len) - sz)"
  shows "unat (2 ^ sz * of_nat k :: (('a::len) word)) = 2 ^ sz * k" proof (cases \<open>sz < LENGTH('a)\<close>) case True with assms show ?thesis by (simp add: unat_word_ariths take_bit_eq_mod mod_simps unsigned_of_nat)
      (simp add: take_bit_nat_eq_self_iff nat_less_power_trans flip: take_bit_eq_mod) next case False with assms show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (state)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k
 2. \<not> sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k
 2. \<not> sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (chain)
picking this:
k < 2 ^ (LENGTH('a) - sz)
sz < LENGTH('a) proof (prove)
using this:
k < 2 ^ (LENGTH('a) - sz)
sz < LENGTH('a)

goal (1 subgoal):
 1. unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (state)
this:
unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (chain)
picking this:
k < 2 ^ (LENGTH('a) - sz)
\<not> sz < LENGTH('a) proof (prove)
using this:
k < 2 ^ (LENGTH('a) - sz)
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k proof (state)
this:
unat (2 ^ sz * word_of_nat k) = 2 ^ sz * k

goal:
No subgoals!
theory More_Word

lemma word_plus_mcs_4:
  "\<lbrakk>v + x \<le> w + x; x \<le> v + x\<rbrakk> \<Longrightarrow> v \<le> (w::'a::len word)" by uint_arith

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

lemma word_plus_mcs_3:
  "\<lbrakk>v \<le> w; x \<le> w + x\<rbrakk> \<Longrightarrow> v + x \<le> w + (x::'a::len word)" by unat_arith

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

lemma word_le_minus_one_leq:
  "x < y \<Longrightarrow> x \<le> y - 1" for x :: "'a :: len word" by transfer (metis le_less_trans less_irrefl take_bit_decr_eq take_bit_nonnegative zle_diff1_eq)

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

lemma word_less_sub_le[simp]:
  fixes x :: "'a :: len word"
  assumes nv: "n < LENGTH('a)"
  shows "(x \<le> 2 ^ n - 1) = (x < 2 ^ n)" using le_less_trans word_le_minus_one_leq nv power_2_ge_iff by blast

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

goal (1 subgoal):
 1. (x \<le> 2 ^ n - 1) = (x < 2 ^ n)
theory More_Word

lemma unat_of_nat_len:
  "x < 2 ^ LENGTH('a) \<Longrightarrow> unat (of_nat x :: 'a::len word) = x" by (simp add: unsigned_of_nat take_bit_nat_eq_self_iff)

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

lemma unat_of_nat_eq:
  "x < 2 ^ LENGTH('a) \<Longrightarrow> unat (of_nat x ::'a::len word) = x" by (rule unat_of_nat_len)

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

lemma unat_eq_of_nat:
  "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat (x :: 'a::len word) = n) = (x = of_nat n)" by transfer
    (auto simp add: take_bit_of_nat nat_eq_iff take_bit_nat_eq_self_iff intro: sym)

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

lemma mask_out_sub_mask:
  "(x AND NOT (mask n)) = x - (x AND (mask n))"
  for x :: \<open>'a::len word\<close> by (fact and_not_eq_minus_and)

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

lemma subtract_mask:
  "p - (p AND mask n) = (p AND NOT (mask n))"
  "p - (p AND NOT (mask n)) = (p AND mask n)"
  for p :: \<open>'a::len word\<close> by (auto simp: and_not_eq_minus_and)

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

lemma take_bit_word_eq_self_iff:
  \<open>take_bit n w = w \<longleftrightarrow> n \<ge> LENGTH('a) \<or> w < 2 ^ n\<close>
  for w :: \<open>'a::len word\<close> using take_bit_int_eq_self_iff [of n \<open>take_bit LENGTH('a) (uint w)\<close>] by (transfer fixing: n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (take_bit n w = w) = (LENGTH('a) \<le> n \<or> w < 2 ^ n) proof (prove)
using this:
(take_bit n (take_bit LENGTH('a) (uint w)) = take_bit LENGTH('a) (uint w)) = (0 \<le> take_bit LENGTH('a) (uint w) \<and> take_bit LENGTH('a) (uint w) < 2 ^ n)

goal (1 subgoal):
 1. (take_bit n w = w) = (LENGTH('a) \<le> n \<or> w < 2 ^ n)
theory More_Word

lemma word_power_increasing:
  assumes x: "2 ^ x < (2 ^ y::'a::len word)" "x < LENGTH('a)" "y < LENGTH('a)"
  shows "x < y" using x using assms by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y proof (prove)
using this:
2 ^ x < 2 ^ y
x < LENGTH('a)
y < LENGTH('a)

goal (1 subgoal):
 1. x < y proof (prove)
using this:
2 ^ x < 2 ^ y
x < LENGTH('a)
y < LENGTH('a)
2 ^ x < 2 ^ y
x < LENGTH('a)
y < LENGTH('a)

goal (1 subgoal):
 1. x < y
theory More_Word

lemma plus_one_helper[elim!]:
  "x < n + (1 :: 'a :: len word) \<Longrightarrow> x \<le> n" apply (simp add: word_less_nat_alt word_le_nat_alt field_simps) apply (case_tac "1 + n = 0") apply simp_all apply (subst(asm) unatSuc, assumption) apply arith done

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

lemma plus_one_helper2:
  "\<lbrakk> x \<le> n; n + 1 \<noteq> 0 \<rbrakk> \<Longrightarrow> x < n + (1 :: 'a :: len word)" by (simp add: word_less_nat_alt word_le_nat_alt field_simps
                unatSuc)

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

lemma less_x_plus_1:
  "x \<noteq> - 1 \<Longrightarrow> (y < x + 1) = (y < x \<or> y = x)" for x :: "'a::len word" by (meson max_word_wrap plus_one_helper plus_one_helper2 word_le_less_eq)

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

lemma word_Suc_leq:
  fixes k::"'a::len word" shows "k \<noteq> - 1 \<Longrightarrow> x < k + 1 \<longleftrightarrow> x \<le> k" using less_x_plus_1 word_le_less_eq by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k \<noteq> - 1 \<Longrightarrow> (x < k + 1) = (x \<le> k) proof (prove)
using this:
?x \<noteq> - 1 \<Longrightarrow> (?y < ?x + 1) = (?y < ?x \<or> ?y = ?x)
(?x \<le> ?y) = (?x = ?y \<or> ?x < ?y)

goal (1 subgoal):
 1. k \<noteq> - 1 \<Longrightarrow> (x < k + 1) = (x \<le> k)
theory More_Word

lemma word_Suc_le:
   fixes k::"'a::len word" shows "x \<noteq> - 1 \<Longrightarrow> x + 1 \<le> k \<longleftrightarrow> x < k" by (meson not_less word_Suc_leq)

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

lemma word_lessThan_Suc_atMost:
  \<open>{..< k + 1} = {..k}\<close> if \<open>k \<noteq> - 1\<close> for k :: \<open>'a::len word\<close> using that by (simp add: lessThan_def atMost_def word_Suc_leq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {..<k + 1} = {..k} proof (prove)
using this:
k \<noteq> - 1

goal (1 subgoal):
 1. {..<k + 1} = {..k}
theory More_Word

lemma word_atLeastLessThan_Suc_atLeastAtMost:
  \<open>{l ..< u + 1} = {l..u}\<close> if \<open>u \<noteq> - 1\<close> for l :: \<open>'a::len word\<close> using that by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {l..<u + 1} = {l..u} proof (prove)
using this:
u \<noteq> - 1

goal (1 subgoal):
 1. {l..<u + 1} = {l..u}
theory More_Word

lemma word_atLeastAtMost_Suc_greaterThanAtMost:
  \<open>{m<..u} = {m + 1..u}\<close> if \<open>m \<noteq> - 1\<close> for m :: \<open>'a::len word\<close> using that by (simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {m<..u} = {m + 1..u} proof (prove)
using this:
m \<noteq> - 1

goal (1 subgoal):
 1. {m<..u} = {m + 1..u}
theory More_Word

lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
  fixes l::"'a::len word"
  assumes "m \<noteq> - 1" and "l \<le> m" and "m \<le> u"
  shows "{l..m} \<union> {m+1..u} = {l..u}" proof - from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} \<union> {m<..u}" by blast with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {l..m} \<union> {m + 1..u} = {l..u} proof (state)
goal (1 subgoal):
 1. {l..m} \<union> {m + 1..u} = {l..u} proof (chain)
picking this:
{l..m} \<union> {m<..u} = {l..u} proof (prove)
using this:
{l..m} \<union> {m<..u} = {l..u}

goal (1 subgoal):
 1. {l..u} = {l..m} \<union> {m<..u} proof (state)
this:
{l..u} = {l..m} \<union> {m<..u}

goal (1 subgoal):
 1. {l..m} \<union> {m + 1..u} = {l..u} proof (chain)
picking this:
m \<noteq> - 1
l \<le> m
m \<le> u
{l..u} = {l..m} \<union> {m<..u} proof (prove)
using this:
m \<noteq> - 1
l \<le> m
m \<le> u
{l..u} = {l..m} \<union> {m<..u}

goal (1 subgoal):
 1. {l..m} \<union> {m + 1..u} = {l..u} proof (state)
this:
{l..m} \<union> {m + 1..u} = {l..u}

goal:
No subgoals!
theory More_Word

lemma max_word_less_eq_iff [simp]:
  \<open>- 1 \<le> w \<longleftrightarrow> w = - 1\<close> for w :: \<open>'a::len word\<close> by (fact word_order.extremum_unique)

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

lemma word_or_zero:
  "(a OR b = 0) = (a = 0 \<and> b = 0)"
  for a b :: \<open>'a::len word\<close> by (fact or_eq_0_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a OR b = 0) = (a = 0 \<and> b = 0)
theory More_Word

lemma word_2p_mult_inc:
  assumes x: "2 * 2 ^ n < (2::'a::len word) * 2 ^ m"
  assumes suc_n: "Suc n < LENGTH('a::len)"
  shows "2^n < (2::'a::len word)^m" by (smt suc_n le_less_trans lessI nat_less_le nat_mult_less_cancel_disj p2_gt_0
          power_Suc power_Suc unat_power_lower word_less_nat_alt x)

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

lemma power_overflow:
  "n \<ge> LENGTH('a) \<Longrightarrow> 2 ^ n = (0 :: 'a::len word)" by simp

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

lemma word_sint_1:
  "sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)" by (fact signed_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint 1 = (if LENGTH('a) = 1 then - 1 else 1)
theory More_Word

lemma ucast_of_nat:
  "is_down (ucast :: 'a :: len word \<Rightarrow> 'b :: len word)
    \<Longrightarrow> ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)" by transfer simp

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

lemma scast_1':
  "(scast (1::'a::len word) :: 'b::len word) =
   (word_of_int (signed_take_bit (LENGTH('a::len) - Suc 0) (1::int)))" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast 1 = word_of_int (signed_take_bit (LENGTH('a) - Suc 0) 1)
theory More_Word

lemma scast_1:
  "(scast (1::'a::len word) :: 'b::len word) = (if LENGTH('a) = 1 then -1 else 1)" by (fact signed_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scast 1 = (if LENGTH('a) = 1 then - 1 else 1)
theory More_Word

lemma unat_minus_one_word:
  "unat (-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1" by (simp add: mask_eq_exp_minus_1 unsigned_minus_1_eq_mask)

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

lemma two_power_increasing:
  "\<lbrakk> n \<le> m; m < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 :: 'a :: len word) ^ n \<le> 2 ^ m" by (simp add: word_le_nat_alt)

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

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

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

lemma neg_mask_combine:
  "NOT(mask a) AND NOT(mask b) = NOT(mask (max a b) :: 'a::len word)" by (rule bit_word_eqI) (auto simp add: bit_simps)

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

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

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

lemma multiple_mask_trivia:
  "n \<ge> m \<Longrightarrow> (x AND NOT(mask n)) + (x AND mask n AND NOT(mask m)) = x AND NOT(mask m)"
  for x :: \<open>'a::len word\<close> apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2) apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice
                   max_absorb2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> (x AND NOT (mask n)) + (x AND mask n AND NOT (mask m)) = x AND NOT (mask m) proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> (x AND NOT (mask n)) + (x AND mask n AND NOT (mask m)) = ((x AND NOT (mask m)) AND mask n) + ((x AND NOT (mask m)) AND NOT (mask n)) proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_of_nat_less:
  "\<lbrakk> n < unat x \<rbrakk> \<Longrightarrow> of_nat n < x" apply (simp add: word_less_nat_alt) apply (erule order_le_less_trans[rotated]) apply (simp add: unsigned_of_nat take_bit_eq_mod) done

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

lemma unat_mask:
  "unat (mask n :: 'a :: len word) = 2 ^ (min n (LENGTH('a))) - 1" apply (subst min.commute) apply (simp add: mask_eq_decr_exp not_less min_def  split: if_split_asm) apply (intro conjI impI) apply (simp add: unat_sub_if_size) apply (simp add: power_overflow word_size) apply (simp add: unat_sub_if_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (mask n) = 2 ^ min n LENGTH('a) - 1 proof (prove)
goal (1 subgoal):
 1. unat (mask n) = 2 ^ min LENGTH('a) n - 1 proof (prove)
goal (1 subgoal):
 1. (LENGTH('a) \<le> n \<longrightarrow> unat (2 ^ n - 1) = 2 ^ LENGTH('a) - Suc 0) \<and> (\<not> LENGTH('a) \<le> n \<longrightarrow> unat (2 ^ n - 1) = 2 ^ n - Suc 0) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> n \<Longrightarrow> unat (2 ^ n - 1) = 2 ^ LENGTH('a) - Suc 0
 2. \<not> LENGTH('a) \<le> n \<Longrightarrow> unat (2 ^ n - 1) = 2 ^ n - Suc 0 proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> n \<Longrightarrow> (Suc 0 \<le> unat (2 ^ n) \<longrightarrow> unat (2 ^ n) - Suc 0 = 2 ^ LENGTH('a) - Suc 0) \<and> (\<not> Suc 0 \<le> unat (2 ^ n) \<longrightarrow> unat (2 ^ n) + 2 ^ size (2 ^ n) - Suc 0 = 2 ^ LENGTH('a) - Suc 0)
 2. \<not> LENGTH('a) \<le> n \<Longrightarrow> unat (2 ^ n - 1) = 2 ^ n - Suc 0 proof (prove)
goal (1 subgoal):
 1. \<not> LENGTH('a) \<le> n \<Longrightarrow> unat (2 ^ n - 1) = 2 ^ n - Suc 0 proof (prove)
goal:
No subgoals!
theory More_Word

lemma mask_over_length:
  "LENGTH('a) \<le> n \<Longrightarrow> mask n = (-1::'a::len word)" by (simp add: mask_eq_decr_exp)

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

lemma Suc_2p_unat_mask:
  "n < LENGTH('a) \<Longrightarrow> Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)" by (simp add: unat_mask)

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

lemma sint_of_nat_ge_zero:
  "x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (of_nat x :: 'a :: len word) \<ge> 0" by (simp add: bit_iff_odd signed_of_nat)

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

lemma int_eq_sint:
  "x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (of_nat x :: 'a :: len word) = int x" apply transfer apply (rule signed_take_bit_int_eq_self) apply simp_all apply (metis negative_zle numeral_power_eq_of_nat_cancel_iff) done

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

lemma word_le_not_less:
  "((b::'a::len word) \<le> a) = (\<not>(a < b))" by fastforce

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

lemma less_is_non_zero_p1:
  fixes a :: "'a :: len word"
  shows "a < k \<Longrightarrow> a + 1 \<noteq> 0" apply (erule contrapos_pn) apply (drule max_word_wrap) apply (simp add: not_less) done

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

lemma unat_add_lem':
  "(unat x + unat y < 2 ^ LENGTH('a)) \<Longrightarrow>
    (unat (x + y :: 'a :: len word) = unat x + unat y)" by (subst unat_add_lem[symmetric], assumption)

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

lemma ucast_less:
  "LENGTH('b) < LENGTH('a) \<Longrightarrow>
   (ucast (x :: 'b :: len word) :: ('a :: len word)) < 2 ^ LENGTH('b)" by transfer simp

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