kings-crown/FVELER_Isabelle huggingface dataset:
theory Sgn_Abs

lemma word_sgn_less[simp]:
  "sgn a <s 0 \<longleftrightarrow> a <s 0" for a::"'a::len word" unfolding sgn_word_def using degenerate_word signed.antisym_conv3 word_sless_alt by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sgn a <s 0) = (a <s 0) proof (prove)
goal (1 subgoal):
 1. ((if a = 0 then 0 else if 0 <s a then 1 else - 1) <s 0) = (a <s 0) proof (prove)
using this:
LENGTH(?'a) = 1 \<Longrightarrow> ?x = 0 \<or> ?x = 1
\<not> ?y <s ?x \<Longrightarrow> (\<not> ?x <s ?y) = (?x = ?y)
(?a <s ?b) = (sint ?a < sint ?b)

goal (1 subgoal):
 1. ((if a = 0 then 0 else if 0 <s a then 1 else - 1) <s 0) = (a <s 0)
theory Sgn_Abs

lemma word_abs_sgn_eq_1[simp]:
  "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1" for a::"'a::len word" unfolding abs_word_def sgn_word_def by (clarsimp simp: word_sle_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1 proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> (if (if a = 0 then 0 else if 0 <s a then 1 else - 1) \<le>s 0 then - (if a = 0 then 0 else if 0 <s a then 1 else - 1) else if a = 0 then 0 else if 0 <s a then 1 else - 1) = 1
theory Sgn_Abs

lemma word_abs_sgn_eq:
  "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)" for a::"'a::len word" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<bar>sgn a\<bar> = (if a = 0 then 0 else 1)
theory Sgn_Abs

lemma word_sgn_mult_self_eq[simp]:
  "sgn a * sgn a = of_bool (a \<noteq> 0)" for a::"'a::len word" by (cases "0 <s a"; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sgn a * sgn a = of_bool (a \<noteq> 0)
theory Word_EqI

lemma test_bit_lenD:
  "bit x n \<Longrightarrow> n < LENGTH('a) \<and> bit x n" for x :: "'a :: len word" by (fastforce dest: test_bit_size simp: word_size)

\<comment> \<open>Method to reduce goals of the form @{prop "P \<Longrightarrow> x = y"} for words of abstract length to
    reasoning on bits of the words. Leaves open goal if unsolved.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit x n \<Longrightarrow> n < LENGTH('a) \<and> bit x n
theory Signed_Division_Word

lemma sdiv_smod_id:
  \<open>(a sdiv b) * b + (a smod b) = a\<close>
  for a b :: \<open>'a::len word\<close> by (fact sdiv_mult_smod_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a sdiv b * b + a smod b = a
theory Signed_Division_Word

lemma signed_div_arith:
    "sint ((a::('a::len) word) sdiv b) = signed_take_bit (LENGTH('a) - 1) (sint a sdiv sint b)" apply transfer apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (a sdiv b) = signed_take_bit (LENGTH('a) - 1) (sint a sdiv sint b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. signed_take_bit (LENGTH('a) - Suc 0) (signed_take_bit (LENGTH('a) - Suc 0) a sdiv signed_take_bit (LENGTH('a) - Suc 0) b) = signed_take_bit (LENGTH('a) - 1) (signed_take_bit (LENGTH('a) - Suc 0) a sdiv signed_take_bit (LENGTH('a) - Suc 0) b) proof (prove)
goal:
No subgoals!
theory Signed_Division_Word

lemma signed_mod_arith:
    "sint ((a::('a::len) word) smod b) = signed_take_bit (LENGTH('a) - 1) (sint a smod sint b)" apply transfer apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (a smod b) = signed_take_bit (LENGTH('a) - 1) (sint a smod sint b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. signed_take_bit (LENGTH('a) - Suc 0) (signed_take_bit (LENGTH('a) - Suc 0) a smod signed_take_bit (LENGTH('a) - Suc 0) b) = signed_take_bit (LENGTH('a) - 1) (signed_take_bit (LENGTH('a) - Suc 0) a smod signed_take_bit (LENGTH('a) - Suc 0) b) proof (prove)
goal:
No subgoals!
theory Signed_Division_Word

lemma word_sdiv_div0 [simp]:
    "(a :: ('a::len) word) sdiv 0 = 0" apply (auto simp: sdiv_word_def signed_divide_int_def sgn_if) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a sdiv 0 = 0 proof (prove)
goal:
No subgoals!
theory Signed_Division_Word

lemma smod_word_zero [simp]:
  \<open>w smod 0 = w\<close> for w :: \<open>'a::len word\<close> by transfer (simp add: take_bit_signed_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w smod 0 = w
theory Signed_Division_Word

lemma word_sdiv_div1 [simp]:
    "(a :: ('a::len) word) sdiv 1 = a" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply transfer apply simp apply (case_tac nat) apply simp_all apply (simp add: take_bit_signed_take_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a sdiv 1 = a proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> a sdiv 1 = a
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> a sdiv 1 = a proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> a sdiv 1 = a proof (prove)
goal (1 subgoal):
 1. \<And>nat a. LENGTH('a) = Suc nat \<Longrightarrow> take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) a sdiv signed_take_bit (LENGTH('a) - Suc 0) 1) = take_bit LENGTH('a) a proof (prove)
goal (1 subgoal):
 1. \<And>nat a. LENGTH('a) = Suc nat \<Longrightarrow> take_bit (Suc nat) (signed_take_bit nat a sdiv signed_take_bit nat 1) = take_bit (Suc nat) a proof (prove)
goal (2 subgoals):
 1. \<And>nat a. \<lbrakk>LENGTH('a) = Suc nat; nat = 0\<rbrakk> \<Longrightarrow> take_bit (Suc nat) (signed_take_bit nat a sdiv signed_take_bit nat 1) = take_bit (Suc nat) a
 2. \<And>nat a nata. \<lbrakk>LENGTH('a) = Suc nat; nat = Suc nata\<rbrakk> \<Longrightarrow> take_bit (Suc nat) (signed_take_bit nat a sdiv signed_take_bit nat 1) = take_bit (Suc nat) a proof (prove)
goal (1 subgoal):
 1. \<And>nat a nata. \<lbrakk>LENGTH('a) = Suc (Suc nata); nat = Suc nata\<rbrakk> \<Longrightarrow> take_bit (Suc (Suc nata)) (signed_take_bit (Suc nata) a) = take_bit (Suc (Suc nata)) a proof (prove)
goal:
No subgoals!
theory Signed_Division_Word

lemma smod_word_one [simp]:
  \<open>w smod 1 = 0\<close> for w :: \<open>'a::len word\<close> by (simp add: smod_word_def signed_modulo_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w smod 1 = 0
theory Signed_Division_Word

lemma smod_word_minus_one [simp]:
  \<open>w smod - 1 = 0\<close> for w :: \<open>'a::len word\<close> by (simp add: smod_word_def signed_modulo_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w smod - 1 = 0
theory Signed_Division_Word

lemma one_smod_word_eq [simp]:
  \<open>1 smod w = 1 - of_bool (w = 1 \<or> w = - 1)\<close> for w :: \<open>'a::len word\<close> using sdiv_smod_id [of 1 w] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 smod w = 1 - of_bool (w = 1 \<or> w = - 1) proof (prove)
using this:
1 sdiv w * w + 1 smod w = 1

goal (1 subgoal):
 1. 1 smod w = 1 - of_bool (w = 1 \<or> w = - 1)
theory Signed_Division_Word

lemma minus_one_smod_word_eq [simp]:
  \<open>- 1 smod w = - (1 smod w)\<close> for w :: \<open>'a::len word\<close> using sdiv_smod_id [of \<open>- 1\<close> w] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 smod w = - (1 smod w) proof (prove)
using this:
- 1 sdiv w * w + - 1 smod w = - 1

goal (1 subgoal):
 1. - 1 smod w = - (1 smod w)
theory Signed_Division_Word

lemma smod_word_alt_def:
  "(a :: ('a::len) word) smod b = a - (a sdiv b) * b" by (simp add: minus_sdiv_mult_eq_smod)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a smod b = a - a sdiv b * b
theory Signed_Division_Word

lemma smod_word_mod_0:
  "x smod (0 :: ('a::len) word) = x" by (fact smod_word_zero)

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

lemma smod_word_0_mod [simp]:
  "0 smod (x :: ('a::len) word) = 0" by (clarsimp simp: smod_word_def)

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

lemma word_xor_le_nand:
  "x XOR y \<le> NOT (x AND y)" for x :: "'a::len word" by (simp add: word_bool_le_funs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x XOR y \<le> NOT (x AND y)
theory Word_Lemmas

lemma word_max_le_or:
  "max x y \<le> x OR y" for x :: "'a::len word" by (simp add: word_bool_le_funs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. max x y \<le> x OR y
theory Word_Lemmas

lemma word_not_le_not_eq[simp]:
  "(NOT y \<le> NOT x) = (x \<le> y)" for x :: "'a::len word" by (subst word_not_le_eq) simp

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

lemma not_max_eq:
  "NOT (max x y) = min (NOT x) (NOT y)" for x :: "'a::len word" unfolding min_def max_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (max x y) = min (NOT x) (NOT y) proof (prove)
goal (1 subgoal):
 1. NOT (if x \<le> y then y else x) = (if NOT x \<le> NOT y then NOT x else NOT y)
theory Word_Lemmas

lemma ucast_zero_is_aligned:
  \<open>is_aligned w n\<close> if \<open>UCAST('a::len \<rightarrow> 'b::len) w = 0\<close> \<open>n \<le> LENGTH('b)\<close> proof (rule is_aligned_bitI) fix q assume \<open>q < n\<close> moreover have \<open>bit (UCAST('a::len \<rightarrow> 'b::len) w) q = bit 0 q\<close> using that by simp with \<open>q < n\<close> \<open>n \<le> LENGTH('b)\<close> show \<open>\<not> bit w q\<close> by (simp add: bit_simps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w n proof (state)
goal (1 subgoal):
 1. \<And>na. na < n \<Longrightarrow> \<not> bit w na proof (state)
goal (1 subgoal):
 1. \<And>na. na < n \<Longrightarrow> \<not> bit w na proof (state)
this:
q < n

goal (1 subgoal):
 1. \<And>na. na < n \<Longrightarrow> \<not> bit w na proof (state)
this:
q < n

goal (1 subgoal):
 1. \<And>na. na < n \<Longrightarrow> \<not> bit w na proof (prove)
goal (1 subgoal):
 1. bit (UCAST('a \<rightarrow> 'b) w) q = bit (0::'c) q proof (prove)
using this:
UCAST('a \<rightarrow> 'b) w = 0
n \<le> LENGTH('b)

goal (1 subgoal):
 1. bit (UCAST('a \<rightarrow> 'b) w) q = bit (0::'c) q proof (state)
this:
bit (UCAST('a \<rightarrow> 'b) w) q = bit (0::?'c1) q

goal (1 subgoal):
 1. \<And>na. na < n \<Longrightarrow> \<not> bit w na proof (chain)
picking this:
q < n
n \<le> LENGTH('b)
bit (UCAST('a \<rightarrow> 'b) w) q = bit (0::?'c1) q proof (prove)
using this:
q < n
n \<le> LENGTH('b)
bit (UCAST('a \<rightarrow> 'b) w) q = bit (0::?'c1) q

goal (1 subgoal):
 1. \<not> bit w q proof (state)
this:
\<not> bit w q

goal:
No subgoals!
theory Word_Lemmas

lemma unat_ucast_eq_unat_and_mask:
  "unat (UCAST('b::len \<rightarrow> 'a::len) w) = unat (w AND mask LENGTH('a))" apply (simp flip: take_bit_eq_mask) apply transfer apply (simp add: ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST('b \<rightarrow> 'a) w) = unat (w AND mask LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. unat (UCAST('b \<rightarrow> 'a) w) = unat (take_bit LENGTH('a) w) proof (prove)
goal (1 subgoal):
 1. \<And>w. (nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('b) w) = (nat \<circ> take_bit LENGTH('b)) (take_bit (min LENGTH('b) LENGTH('a)) w) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma uint_shiftr_eq:
  \<open>uint (w >> n) = uint w div 2 ^ n\<close> by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (w >> n) = uint w div 2 ^ n
theory Word_Lemmas

lemma bit_shiftl_word_iff [bit_simps]:
  \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close>
  for w :: \<open>'a::len word\<close> by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (w << m) n = (m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m))
theory Word_Lemmas

lemma bit_shiftr_word_iff:
  \<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
  for w :: \<open>'a::len word\<close> by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (w >> m) n = bit w (m + n)
theory Word_Lemmas

lemma sshiftr_n1: "-1 >>> n = -1" by (simp add: sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 >>> n = - 1
theory Word_Lemmas

lemma nth_sshiftr:
  "bit (w >>> m) n = (n < size w \<and> (if n + m \<ge> size w then bit w (size w - 1) else bit w (n + m)))" apply (auto simp add: bit_simps word_size ac_simps not_less) apply (meson bit_imp_le_length bit_shiftr_word_iff leD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (w >>> m) n = (n < size w \<and> (if size w \<le> n + m then bit w (size w - 1) else bit w (n + m))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) \<le> n; bit w (m + n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma sshiftr_numeral:
  \<open>(numeral k >>> numeral n :: 'a::len word) =
    word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral k) >> numeral n)\<close> using signed_drop_bit_word_numeral [of n k] by (simp add: sshiftr_def shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral k >>> numeral n = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral k) >> numeral n) proof (prove)
using this:
signed_drop_bit (numeral n) (numeral k) = word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH(?'a) - 1) (numeral k)))

goal (1 subgoal):
 1. numeral k >>> numeral n = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral k) >> numeral n)
theory Word_Lemmas

lemma sshiftr_div_2n: "sint (w >>> n) = sint w div 2 ^ n" by word_eqI (cases \<open>n < LENGTH('a)\<close>; fastforce simp: le_diff_conv2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (w >>> n) = sint w div 2 ^ n
theory Word_Lemmas

lemma mask_eq:
  \<open>mask n = (1 << n) - (1 :: 'a::len word)\<close> by (simp add: mask_eq_exp_minus_1 shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask n = (1 << n) - 1
theory Word_Lemmas

lemma nth_shiftl': "bit (w << m) n \<longleftrightarrow> n < size w \<and> n >= m \<and> bit w (n - m)"
  for w :: "'a::len word" by (simp add: bit_simps word_size ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (w << m) n = (n < size w \<and> m \<le> n \<and> bit w (n - m))
theory Word_Lemmas

lemma nth_shiftr: "bit (w >> m) n = bit w (n + m)"
  for w :: "'a::len word" by (simp add: bit_simps ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (w >> m) n = bit w (n + m)
theory Word_Lemmas

lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n" by (fact uint_shiftr_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (w >> n) = uint w div 2 ^ n
theory Word_Lemmas

lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w << n = word_reverse (word_reverse w >> n)
theory Word_Lemmas

lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)" by (simp add: shiftl_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_reverse w << n = word_reverse (w >> n)
theory Word_Lemmas

lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)" by (simp add: rev_shiftl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w >> n = word_reverse (word_reverse w << n)
theory Word_Lemmas

lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
  for x :: "'a::len word" by (simp add: shiftl_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size x \<le> n \<Longrightarrow> x << n = 0
theory Word_Lemmas

lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
  for w :: "'a::len word" by (simp add: shiftl_def push_bit_eq_mult)

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

lemma word_shift_by_2:
  "x * 4 = (x::'a::len word) << 2" by (simp add: shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x * 4 = x << 2
theory Word_Lemmas

lemma word_shift_by_3:
  "x * 8 = (x::'a::len word) << 3" by (simp add: shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x * 8 = x << 3
theory Word_Lemmas

lemma slice_shiftr: "slice n w = ucast (w >> n)" by word_eqI (cases \<open>n \<le> LENGTH('b)\<close>; fastforce simp: ac_simps dest: bit_imp_le_length)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slice n w = UCAST('b \<rightarrow> 'a) (w >> n)
theory Word_Lemmas

lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0"
  for x :: "'a :: len word" by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size x \<le> n \<Longrightarrow> x >> n = 0
theory Word_Lemmas

lemma shiftr_x_0 [simp]: "x >> 0 = x"
  for x :: "'a::len word" by (simp add: shiftr_def)

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

lemma shiftl_x_0 [simp]: "x << 0 = x"
  for x :: "'a::len word" by (simp add: shiftl_def)

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

lemma shiftr_1 [simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)" by (simp add: shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 >> n = (if n = 0 then 1 else 0)
theory Word_Lemmas

lemma and_not_mask:
  "w AND NOT (mask n) = (w >> n) << n"
  for w :: \<open>'a::len word\<close> by word_eqI_solve

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

lemma and_mask:
  "w AND mask n = (w << (size w - n)) >> (size w - n)"
  for w :: \<open>'a::len word\<close> by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w AND mask n = w << size w - n >> size w - n
theory Word_Lemmas

lemma le_shiftr:
  "u \<le> v \<Longrightarrow> u >> (n :: nat) \<le> (v :: 'a :: len word) >> n" apply (unfold shiftr_def) apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_eq_div zdiv_mono1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. u \<le> v \<Longrightarrow> u >> n \<le> v >> n proof (prove)
goal (1 subgoal):
 1. u \<le> v \<Longrightarrow> drop_bit n u \<le> drop_bit n v proof (prove)
goal (1 subgoal):
 1. \<And>u v n. take_bit LENGTH('a) u \<le> take_bit LENGTH('a) v \<Longrightarrow> take_bit LENGTH('a) ((drop_bit n \<circ> take_bit LENGTH('a)) u) \<le> take_bit LENGTH('a) ((drop_bit n \<circ> take_bit LENGTH('a)) v) proof (prove)
goal (1 subgoal):
 1. \<And>u v n. take_bit LENGTH('a) u \<le> take_bit LENGTH('a) v \<Longrightarrow> drop_bit n (take_bit LENGTH('a) u) \<le> drop_bit n (take_bit LENGTH('a) v) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma le_shiftr':
  "\<lbrakk> u >> n \<le> v >> n ; u >> n \<noteq> v >> n \<rbrakk> \<Longrightarrow> (u::'a::len word) \<le> v" by (metis le_cases le_shiftr verit_la_disequality)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u >> n \<le> v >> n; u >> n \<noteq> v >> n\<rbrakk> \<Longrightarrow> u \<le> v
theory Word_Lemmas

lemma shiftr_mask_le:
  "n <= m \<Longrightarrow> mask n >> m = (0 :: 'a::len word)" by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> mask n >> m = 0
theory Word_Lemmas

lemma shiftr_mask [simp]:
  \<open>mask m >> m = (0::'a::len word)\<close> by (rule shiftr_mask_le) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask m >> m = 0
theory Word_Lemmas

lemma le_mask_iff:
  "(w \<le> mask n) = (w >> n = 0)"
  for w :: \<open>'a::len word\<close> apply safe apply (rule word_le_0_iff [THEN iffD1]) apply (rule xtrans(3)) apply (erule_tac [2] le_shiftr) apply simp apply (rule word_leI) apply (rename_tac n') apply (drule_tac x = "n' - n" in word_eqD) apply (simp add : nth_shiftr word_size bit_simps) apply (case_tac "n <= n'") by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w \<le> mask n) = (w >> n = 0) proof (prove)
goal (2 subgoals):
 1. w \<le> mask n \<Longrightarrow> w >> n = 0
 2. w >> n = 0 \<Longrightarrow> w \<le> mask n proof (prove)
goal (2 subgoals):
 1. w \<le> mask n \<Longrightarrow> w >> n \<le> 0
 2. w >> n = 0 \<Longrightarrow> w \<le> mask n proof (prove)
goal (3 subgoals):
 1. w \<le> mask n \<Longrightarrow> 0 = ?b4
 2. w \<le> mask n \<Longrightarrow> w >> n \<le> ?b4
 3. w >> n = 0 \<Longrightarrow> w \<le> mask n proof (prove)
goal (2 subgoals):
 1. w \<le> mask n \<Longrightarrow> 0 = mask n >> n
 2. w >> n = 0 \<Longrightarrow> w \<le> mask n proof (prove)
goal (1 subgoal):
 1. w >> n = 0 \<Longrightarrow> w \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>w >> n = 0; na < size w; bit w na\<rbrakk> \<Longrightarrow> bit (mask n) na proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>w >> n = 0; n' < size w; bit w n'\<rbrakk> \<Longrightarrow> bit (mask n) n' proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>n' < size w; bit w n'; bit (w >> n) (n' - n) = bit 0 (n' - n)\<rbrakk> \<Longrightarrow> bit (mask n) n' proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>n' < LENGTH('a); bit w n'; \<not> bit w (n + (n' - n))\<rbrakk> \<Longrightarrow> n' < n proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>n' < LENGTH('a); bit w n'; \<not> bit w (n + (n' - n)); n \<le> n'\<rbrakk> \<Longrightarrow> n' < n
 2. \<And>n'. \<lbrakk>n' < LENGTH('a); bit w n'; \<not> bit w (n + (n' - n)); \<not> n \<le> n'\<rbrakk> \<Longrightarrow> n' < n
theory Word_Lemmas

lemma and_mask_eq_iff_shiftr_0:
  "(w AND mask n = w) = (w >> n = 0)"
  for w :: \<open>'a::len word\<close> by (simp flip: take_bit_eq_mask add: shiftr_def take_bit_eq_self_iff_drop_bit_eq_0)

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

lemma mask_shiftl_decompose:
  "mask m << n = mask (m + n) AND NOT (mask n :: 'a::len word)" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask m << n = mask (m + n) AND NOT (mask n)
theory Word_Lemmas

lemma shiftl_over_and_dist:
  fixes a::"'a::len word"
  shows "(a AND b) << c = (a << c) AND (b << c)" by (unfold shiftl_def) (fact push_bit_and)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a AND b << c = (a << c) AND (b << c)
theory Word_Lemmas

lemma shiftr_over_and_dist:
  fixes a::"'a::len word"
  shows "a AND b >> c = (a >> c) AND (b >> c)" by (unfold shiftr_def) (fact drop_bit_and)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a AND b >> c = (a >> c) AND (b >> c)
theory Word_Lemmas

lemma sshiftr_over_and_dist:
  fixes a::"'a::len word"
  shows "a AND b >>> c = (a >>> c) AND (b >>> c)" by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a AND b >>> c = (a >>> c) AND (b >>> c)
theory Word_Lemmas

lemma shiftl_over_or_dist:
  fixes a::"'a::len word"
  shows "a OR b << c = (a << c) OR (b << c)" by (unfold shiftl_def) (fact push_bit_or)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a OR b << c = (a << c) OR (b << c)
theory Word_Lemmas

lemma shiftr_over_or_dist:
  fixes a::"'a::len word"
  shows "a OR b >> c = (a >> c) OR (b >> c)" by (unfold shiftr_def) (fact drop_bit_or)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a OR b >> c = (a >> c) OR (b >> c)
theory Word_Lemmas

lemma sshiftr_over_or_dist:
  fixes a::"'a::len word"
  shows "a OR b >>> c = (a >>> c) OR (b >>> c)" by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a OR b >>> c = (a >>> c) OR (b >>> c)
theory Word_Lemmas

lemma shiftl_shiftl:
  fixes a::"'a::len word"
  shows "a << b << c = a << (b + c)" by (word_eqI_solve simp: add.commute add.left_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a << b << c = a << b + c
theory Word_Lemmas

lemma shiftr_shiftr:
  fixes a::"'a::len word"
  shows "a >> b >> c = a >> (b + c)" by word_eqI (simp add: add.left_commute add.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a >> b >> c = a >> b + c
theory Word_Lemmas

lemma shiftl_shiftr1:
  fixes a::"'a::len word"
  shows "c \<le> b \<Longrightarrow> a << b >> c = a AND (mask (size a - b)) << (b - c)" by word_eqI (auto simp: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<le> b \<Longrightarrow> a << b >> c = a AND mask (size a - b) << b - c