kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas

lemma shiftl_shiftr2:
  fixes a::"'a::len word"
  shows "b < c \<Longrightarrow> a << b >> c = (a >> (c - b)) AND (mask (size a - c))" by word_eqI_solve

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

lemma shiftr_shiftl1:
  fixes a::"'a::len word"
  shows "c \<le> b \<Longrightarrow> a >> b << c = (a >> (b - c)) AND (NOT (mask c))" by word_eqI_solve

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

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

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

lemma shiftr_mask2:
  "n \<le> LENGTH('a) \<Longrightarrow> (mask n >> m :: ('a :: len) word) = mask (n - m)" by word_eqI_solve

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

lemma word_shiftl_add_distrib:
  fixes x :: "'a :: len word"
  shows "(x + y) << n = (x << n) + (y << n)" by (simp add: shiftl_t2n ring_distribs)

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

lemma mask_shift:
  "(x AND NOT (mask y)) >> y = x >> y"
  for x :: \<open>'a::len word\<close> by word_eqI

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

lemma shiftr_div_2n':
  "unat (w >> n) = unat w div 2 ^ n" by word_eqI

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

lemma ucast_shiftl_eq_0:
  fixes w :: "'a :: len word"
  shows "\<lbrakk> n \<ge> LENGTH('b) \<rbrakk> \<Longrightarrow> ucast (w << n) = (0 :: 'b :: len word)" by (transfer fixing: n) (simp add: take_bit_push_bit)

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

lemma word_shift_nonzero:
  "\<lbrakk> (x::'a::len word) \<le> 2 ^ m; m + n < LENGTH('a::len); x \<noteq> 0\<rbrakk>
   \<Longrightarrow> x << n \<noteq> 0" apply (simp only: word_neq_0_conv word_less_nat_alt
                    shiftl_t2n mod_0 unat_word_ariths
                    unat_power_lower word_le_nat_alt) apply (subst mod_less) apply (rule order_le_less_trans) apply (erule mult_le_mono2) apply (subst power_add[symmetric]) apply (rule power_strict_increasing) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 2 ^ m; m + n < LENGTH('a); x \<noteq> 0\<rbrakk> \<Longrightarrow> x << n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x mod 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 2 ^ n * unat x \<le> ?y5
 2. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a)
 3. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 2 ^ n * 2 ^ m < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 2 ^ (n + m) < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> n + m < LENGTH('a)
 2. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x \<le> 2 ^ m; m + n < LENGTH('a); 0 < unat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ n * unat x proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma word_shiftr_lt:
  fixes w :: "'a::len word"
  shows "unat (w >> n) < (2 ^ (LENGTH('a) - n))" apply (subst shiftr_div_2n') apply transfer apply (simp flip: drop_bit_eq_div add: drop_bit_nat_eq drop_bit_take_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (w >> n) < 2 ^ (LENGTH('a) - n) proof (prove)
goal (1 subgoal):
 1. unat w div 2 ^ n < 2 ^ (LENGTH('a) - n) proof (prove)
goal (1 subgoal):
 1. \<And>w n. (nat \<circ> take_bit LENGTH('a)) w div 2 ^ n < 2 ^ (LENGTH('a) - n) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftr_less_t2n':
  "\<lbrakk> x AND mask (n + m) = x; m < LENGTH('a) \<rbrakk> \<Longrightarrow> x >> n < 2 ^ m" for x :: "'a :: len word" apply (simp add: word_size mask_eq_iff_w2p [symmetric] flip: take_bit_eq_mask) apply transfer apply (simp add: take_bit_drop_bit ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND mask (n + m) = x; m < LENGTH('a)\<rbrakk> \<Longrightarrow> x >> n < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit (n + m) x = x; m < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit m (x >> n) = x >> n proof (prove)
goal (1 subgoal):
 1. \<And>n m x. \<lbrakk>take_bit LENGTH('a) (take_bit (min LENGTH('a) (n + m)) x) = take_bit LENGTH('a) x; m < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (take_bit (min LENGTH('a) m) (drop_bit n (take_bit LENGTH('a) x))) = take_bit LENGTH('a) (drop_bit n (take_bit LENGTH('a) x)) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftr_less_t2n:
  "x < 2 ^ (n + m) \<Longrightarrow> x >> n < 2 ^ m" for x :: "'a :: len word" apply (rule shiftr_less_t2n') apply (erule less_mask_eq) apply (rule ccontr) apply (simp add: not_less) apply (subst (asm) p2_eq_0[symmetric]) apply (simp add: power_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (n + m) \<Longrightarrow> x >> n < 2 ^ m proof (prove)
goal (2 subgoals):
 1. x < 2 ^ (n + m) \<Longrightarrow> x AND mask (n + m) = x
 2. x < 2 ^ (n + m) \<Longrightarrow> m < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (n + m) \<Longrightarrow> m < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ (n + m); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ (n + m); LENGTH('a) \<le> m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ (n + m); 2 ^ m = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftr_eq_0:
  "n \<ge> LENGTH('a) \<Longrightarrow> ((w::'a::len word) >> n) = 0" apply (cut_tac shiftr_less_t2n'[of w n 0], simp) apply (simp add: mask_eq_iff) apply (simp add: lt2p_lem) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> w >> n = 0 proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> n \<Longrightarrow> w AND mask (n + 0) = w
 2. LENGTH('a) \<le> n \<Longrightarrow> 0 < LENGTH('a) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) \<le> n \<Longrightarrow> uint w < 2 ^ n
 2. LENGTH('a) \<le> n \<Longrightarrow> 0 < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> 0 < LENGTH('a) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftl_less_t2n:
  fixes x :: "'a :: len word"
  shows "\<lbrakk> x < (2 ^ (m - n)); m < LENGTH('a) \<rbrakk> \<Longrightarrow> (x << n) < 2 ^ m" apply (simp add: word_size mask_eq_iff_w2p [symmetric] flip: take_bit_eq_mask) apply transfer apply (simp add: take_bit_push_bit) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ (m - n); m < LENGTH('a)\<rbrakk> \<Longrightarrow> x << n < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit (m - n) x = x; m < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit m (x << n) = x << n proof (prove)
goal (1 subgoal):
 1. \<And>m n x. \<lbrakk>take_bit LENGTH('a) (take_bit (min LENGTH('a) (m - n)) x) = take_bit LENGTH('a) x; m < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (take_bit (min LENGTH('a) m) (push_bit n x)) = take_bit LENGTH('a) (push_bit n x) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma scast_bit_test [simp]:
  "scast ((1 :: 'a::len signed word) << n) = (1 :: 'a word) << n" by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST('a signed \<rightarrow> 'a) (1 << n) = 1 << n
theory Word_Lemmas

lemma shiftr_not_mask_0:
  "n+m \<ge> LENGTH('a :: len) \<Longrightarrow> ((w::'a::len word) >> n) AND NOT (mask m) = 0" by word_eqI

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n + m \<Longrightarrow> (w >> n) AND NOT (mask m) = 0
theory Word_Lemmas

lemma shiftl_mask_is_0[simp]:
  "(x << n) AND mask n = 0"
  for x :: \<open>'a::len word\<close> by (simp flip: take_bit_eq_mask add: take_bit_push_bit shiftl_def)

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

lemma rshift_sub_mask_eq:
  "(a >> (size a - b)) AND mask b = a >> (size a - b)"
  for a :: \<open>'a::len word\<close> using shiftl_shiftr2[where a=a and b=0 and c="size a - b"] apply (cases "b < size a") apply simp apply (simp add: linorder_not_less mask_eq_decr_exp word_size
                   p2_eq_0[THEN iffD2]) done

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

goal (1 subgoal):
 1. (a >> size a - b) AND mask b = a >> size a - b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < size a - b \<Longrightarrow> a << 0 >> size a - b = (a >> size a - b - 0) AND mask (size a - (size a - b)); b < size a\<rbrakk> \<Longrightarrow> (a >> size a - b) AND mask b = a >> size a - b
 2. \<lbrakk>0 < size a - b \<Longrightarrow> a << 0 >> size a - b = (a >> size a - b - 0) AND mask (size a - (size a - b)); \<not> b < size a\<rbrakk> \<Longrightarrow> (a >> size a - b) AND mask b = a >> size a - b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size a - b \<Longrightarrow> a << 0 >> size a - b = (a >> size a - b - 0) AND mask (size a - (size a - b)); \<not> b < size a\<rbrakk> \<Longrightarrow> (a >> size a - b) AND mask b = a >> size a - b proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftl_shiftr3:
  "b \<le> c \<Longrightarrow> a << b >> c = (a >> c - b) AND mask (size a - c)"
  for a :: \<open>'a::len word\<close> apply (cases "b = c") apply (simp add: shiftl_shiftr1) apply (simp add: shiftl_shiftr2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> c \<Longrightarrow> a << b >> c = (a >> c - b) AND mask (size a - c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> c; b = c\<rbrakk> \<Longrightarrow> a << b >> c = (a >> c - b) AND mask (size a - c)
 2. \<lbrakk>b \<le> c; b \<noteq> c\<rbrakk> \<Longrightarrow> a << b >> c = (a >> c - b) AND mask (size a - c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> c; b \<noteq> c\<rbrakk> \<Longrightarrow> a << b >> c = (a >> c - b) AND mask (size a - c) proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma and_mask_shiftr_comm:
  "m \<le> size w \<Longrightarrow> (w AND mask m) >> n = (w >> n) AND mask (m-n)"
  for w :: \<open>'a::len word\<close> by (simp add: and_mask shiftr_shiftr) (simp add: word_size shiftl_shiftr3)

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

lemma le_mask_shiftl_le_mask: "s = m + n \<Longrightarrow> x \<le> mask n \<Longrightarrow> x << m \<le> mask s"
  for x :: \<open>'a::len word\<close> by (simp add: le_mask_iff shiftl_shiftr3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = m + n; x \<le> mask n\<rbrakk> \<Longrightarrow> x << m \<le> mask s
theory Word_Lemmas

lemma word_and_1_shiftl:
  "x AND (1 << n) = (if bit x n then (1 << n) else 0)" for x :: "'a :: len word" by word_eqI_solve

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

lemma word_and_mask_shiftl:
  "x AND (mask n << m) = ((x >> m) AND mask n) << m"
  for x :: \<open>'a::len word\<close> by word_eqI_solve

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

lemma shift_times_fold:
  "(x :: 'a :: len word) * (2 ^ n) << m = x << (m + n)" by (simp add: shiftl_t2n ac_simps power_add)

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

lemma of_bool_nth:
  "of_bool (bit x v) = (x >> v) AND 1"
  for x :: \<open>'a::len word\<close> by (simp add: bit_iff_odd_drop_bit word_and_1 shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bool (bit x v) = (x >> v) AND 1
theory Word_Lemmas

lemma shiftr_mask_eq:
  "(x >> n) AND mask (size x - n) = x >> n" for x :: "'a :: len word" by (word_eqI_solve dest: test_bit_lenD)

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

lemma shiftr_mask_eq':
  "m = (size x - n) \<Longrightarrow> (x >> n) AND mask m = x >> n" for x :: "'a :: len word" by (simp add: shiftr_mask_eq)

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

lemma and_eq_0_is_nth:
  fixes x :: "'a :: len word"
  shows "y = 1 << n \<Longrightarrow> ((x AND y) = 0) = (\<not> (bit x n))" by (simp add: and_exp_eq_0_iff_not_bit shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y = 1 << n \<Longrightarrow> (x AND y = 0) = (\<not> bit x n)
theory Word_Lemmas

lemma word_shift_zero:
  "\<lbrakk> x << n = 0; x \<le> 2^m; m + n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x::'a::len word) = 0" apply (rule ccontr) apply (drule (2) word_shift_nonzero) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x << n = 0; x \<le> 2 ^ m; m + n < LENGTH('a)\<rbrakk> \<Longrightarrow> x = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x << n = 0; x \<le> 2 ^ m; m + n < LENGTH('a); x \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x << n = 0; m + n < LENGTH('a); x \<noteq> 0; x << n \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma mask_shift_and_negate[simp]:"(w AND mask n << m) AND NOT (mask n << m) = 0"
  for w :: \<open>'a::len word\<close> by word_eqI

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

lemma bitfield_op_twice:
  "(x AND NOT (mask n << m) OR ((y AND mask n) << m)) AND NOT (mask n << m) = x AND NOT (mask n << m)"
  for x :: \<open>'a::len word\<close> by word_eqI_solve

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

lemma bitfield_op_twice'':
  "\<lbrakk>NOT a = b << c; \<exists>x. b = mask x\<rbrakk> \<Longrightarrow> (x AND a OR (y AND b << c)) AND a = x AND a"
  for a b :: \<open>'a::len word\<close> by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>NOT a = b << c; \<exists>x. b = mask x\<rbrakk> \<Longrightarrow> (x AND a OR (y AND b << c)) AND a = x AND a
theory Word_Lemmas

lemma shiftr1_unfold: "x div 2 = x >> 1" by (simp add: drop_bit_eq_div shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x div (2::'a) = x >> 1
theory Word_Lemmas

lemma shiftr1_is_div_2: "(x::('a::len) word) >> 1 = x div 2" by (simp add: drop_bit_eq_div shiftr_def)

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

lemma shiftl1_is_mult: "(x << 1) = (x :: 'a::len word) * 2" by (metis One_nat_def mult_2 mult_2_right one_add_one
        power_0 power_Suc shiftl_t2n)

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

lemma shiftr1_lt:"x \<noteq> 0 \<Longrightarrow> (x::('a::len) word) >> 1 < x" apply (subst shiftr1_is_div_2) apply (rule div_less_dividend_word) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x >> 1 < x proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x div 2 < x proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> x \<noteq> 0
 2. x \<noteq> 0 \<Longrightarrow> 2 \<noteq> 1 proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma shiftr1_0_or_1:"(x::('a::len) word) >> 1 = 0 \<Longrightarrow> x = 0 \<or> x = 1" apply (subst (asm) shiftr1_is_div_2) apply (drule word_less_div) apply (case_tac "LENGTH('a) = 1") apply (simp add:degenerate_word) apply (erule disjE) apply (subgoal_tac "(2::'a word) \<noteq> 0") apply simp apply (rule not_degenerate_imp_2_neq_0) apply (subgoal_tac "LENGTH('a) \<noteq> 0") apply arith apply simp apply (rule x_less_2_0_1', simp+) done

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

lemma shiftr1_irrelevant_lsb: "bit (x::('a::len) word) 0 \<or> x >> 1 = (x + 1) >> 1" by (auto simp add: bit_0 shiftr_def drop_bit_Suc ac_simps elim: evenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit x 0 \<or> x >> 1 = x + 1 >> 1
theory Word_Lemmas

lemma shiftr1_0_imp_only_lsb:"((x::('a::len) word) + 1) >> 1 = 0 \<Longrightarrow> x = 0 \<or> x + 1 = 0" by (metis One_nat_def shiftr1_0_or_1 word_less_1 word_overflow)

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

lemma shiftr1_irrelevant_lsb': "\<not> (bit (x::('a::len) word) 0) \<Longrightarrow> x >> 1 = (x + 1) >> 1" using shiftr1_irrelevant_lsb [of x] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit x 0 \<Longrightarrow> x >> 1 = x + 1 >> 1 proof (prove)
using this:
bit x 0 \<or> x >> 1 = x + 1 >> 1

goal (1 subgoal):
 1. \<not> bit x 0 \<Longrightarrow> x >> 1 = x + 1 >> 1
theory Word_Lemmas

lemma cast_chunk_scast_assemble_id:
  "\<lbrakk>n = LENGTH('a::len); m = LENGTH('b::len); n * 2 = m\<rbrakk> \<Longrightarrow>
  (((ucast ((scast (x::'b word))::'a word))::'b word) OR
   (((ucast ((scast (x >> n))::'a word))::'b word) << n)) = x" apply (subgoal_tac "((scast x)::'a word) = ((ucast x)::'a word)") apply (subgoal_tac "((scast (x >> n))::'a word) = ((ucast (x >> n))::'a word)") apply (simp add:cast_chunk_assemble_id) apply (subst down_cast_same[symmetric], subst is_down, arith, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (SCAST('b \<rightarrow> 'a) x) OR (UCAST('a \<rightarrow> 'b) (SCAST('b \<rightarrow> 'a) (x >> n)) << n) = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m; SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (SCAST('b \<rightarrow> 'a) x) OR (UCAST('a \<rightarrow> 'b) (SCAST('b \<rightarrow> 'a) (x >> n)) << n) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m; SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x; SCAST('b \<rightarrow> 'a) (x >> n) = UCAST('b \<rightarrow> 'a) (x >> n)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (SCAST('b \<rightarrow> 'a) x) OR (UCAST('a \<rightarrow> 'b) (SCAST('b \<rightarrow> 'a) (x >> n)) << n) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m; SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'a) (x >> n) = UCAST('b \<rightarrow> 'a) (x >> n)
 3. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m; SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'a) (x >> n) = UCAST('b \<rightarrow> 'a) (x >> n)
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> SCAST('b \<rightarrow> 'a) x = UCAST('b \<rightarrow> 'a) x proof (prove)
goal:
No subgoals!
theory Word_Lemmas

lemma unat_shiftr_less_t2n:
  fixes x :: "'a :: len word"
  shows "unat x < 2 ^ (n + m) \<Longrightarrow> unat (x >> n) < 2 ^ m" by (simp add: shiftr_div_2n' power_add mult.commute less_mult_imp_div_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ (n + m) \<Longrightarrow> unat (x >> n) < 2 ^ m