kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas_Internal

lemma word_le_1:
  fixes w :: "'a::len word"
  shows "w \<le> 1 \<longleftrightarrow> w = 0 \<or> w = 1" using dual_order.antisym lt1_neq0 word_zero_le by blast

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

goal (1 subgoal):
 1. (w \<le> 1) = (w = 0 \<or> w = 1)
theory Word_Lemmas_Internal

lemma less_ucast_ucast_less':
  "x < UCAST('b \<rightarrow> 'a) y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x < y"
  for x :: "'a::len word" and y :: "'b::len word" by (clarsimp simp: order.strict_iff_order dual_order.antisym le_ucast_ucast_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < UCAST('b \<rightarrow> 'a) y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x < y
theory Word_Lemmas_Internal

lemma ucast_up_less_bounded_implies_less_ucast_down':
  assumes len: "LENGTH('a::len) < LENGTH('b::len)"
  assumes bound: "y < 2 ^ LENGTH('a)"
  assumes less: "UCAST('a \<rightarrow> 'b) x < y"
  shows "x < UCAST('b \<rightarrow> 'a) y" apply (rule le_less_trans[OF _ ucast_mono[OF less bound]]) using len by (simp add: is_down ucast_down_ucast_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < UCAST('b \<rightarrow> 'a) y proof (prove)
goal (1 subgoal):
 1. x \<le> UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) proof (prove)
using this:
LENGTH('a) < LENGTH('b)

goal (1 subgoal):
 1. x \<le> UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x)
theory Word_Lemmas_Internal

lemma ucast_up_less_bounded_iff_less_ucast_down':
  assumes len: "LENGTH('a::len) < LENGTH('b::len)"
  assumes bound: "y < 2 ^ LENGTH('a)"
  shows "UCAST('a \<rightarrow> 'b) x < y \<longleftrightarrow> x < UCAST('b \<rightarrow> 'a) y" apply (rule iffI) prefer 2 apply (simp add: less_ucast_ucast_less') using assms by (rule ucast_up_less_bounded_implies_less_ucast_down')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST('a \<rightarrow> 'b) x < y) = (x < UCAST('b \<rightarrow> 'a) y) proof (prove)
goal (2 subgoals):
 1. UCAST('a \<rightarrow> 'b) x < y \<Longrightarrow> x < UCAST('b \<rightarrow> 'a) y
 2. x < UCAST('b \<rightarrow> 'a) y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x < y proof (prove)
goal (2 subgoals):
 1. x < UCAST('b \<rightarrow> 'a) y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x < y
 2. UCAST('a \<rightarrow> 'b) x < y \<Longrightarrow> x < UCAST('b \<rightarrow> 'a) y proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) x < y \<Longrightarrow> x < UCAST('b \<rightarrow> 'a) y proof (prove)
using this:
LENGTH('a) < LENGTH('b)
y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) x < y \<Longrightarrow> x < UCAST('b \<rightarrow> 'a) y
theory Word_Lemmas_Internal

lemma word_of_int_word_of_nat_eqD:
  "\<lbrakk> word_of_int x = (word_of_nat y :: 'a :: len word); 0 \<le> x; x < 2^LENGTH('a); y < 2^LENGTH('a) \<rbrakk>
   \<Longrightarrow> nat x = y" by (metis nat_eq_numeral_power_cancel_iff of_nat_inj word_of_int_nat zless2p zless_nat_conj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_int x = word_of_nat y; 0 \<le> x; x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> nat x = y
theory Word_Lemmas_Internal

lemma ucast_down_0:
  "\<lbrakk> UCAST('a::len \<rightarrow> 'b::len) x = 0; unat x < 2^LENGTH('b) \<rbrakk> \<Longrightarrow> x = 0" by (metis Word.of_nat_unat unat_0 unat_eq_of_nat word_unat_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST('a \<rightarrow> 'b) x = 0; unat x < 2 ^ LENGTH('b)\<rbrakk> \<Longrightarrow> x = 0
theory Word_Lemmas_Internal

lemma FF_eq_minus_1:
  \<open>0xFF = (- 1 :: 8 word)\<close> by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 255 = - 1
theory Word_Lemmas_Internal

lemma word_mask_shift_eqI:
  "\<lbrakk> x && mask n = y && mask n; x >> n = y >> n \<rbrakk> \<Longrightarrow> x = y" apply (subst mask_or_not_mask[of x n, symmetric]) apply (subst mask_or_not_mask[of y n, symmetric]) apply (rule arg_cong2[where f="(OR)"]; blast intro: shiftr_eq_neg_mask_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n = y && mask n; x >> n = y >> n\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n = y && mask n; x >> n = y >> n\<rbrakk> \<Longrightarrow> x && mask n || x && ~~ mask n = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n = y && mask n; x >> n = y >> n\<rbrakk> \<Longrightarrow> x && mask n || x && ~~ mask n = y && mask n || y && ~~ mask n proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma mask_shiftr_mask_eq:
  "m \<le> m' + n \<Longrightarrow> (w && mask m >> n) && mask m' = w && mask m >> n" for w :: "'a::len word" by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> m' + n \<Longrightarrow> (w && mask m >> n) && mask m' = w && mask m >> n
theory Word_Lemmas_Internal

lemma mask_alignment_ugliness:
  "\<lbrakk> x \<noteq> x + z && ~~ mask m;
     is_aligned (x + z && ~~ mask m) m;
     is_aligned x m;
     \<forall>n \<ge> m. \<not>z !! n\<rbrakk>
  \<Longrightarrow> False" apply (erule notE) apply (subst word_plus_and_or_coroll; word_eqI) apply (meson linorder_not_le) by (auto simp: le_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> x + z && ~~ mask m; is_aligned (x + z && ~~ mask m) m; is_aligned x m; \<forall>n\<ge>m. \<not> z !! n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (x + z && ~~ mask m) m; is_aligned x m; \<forall>n\<ge>m. \<not> z !! n\<rbrakk> \<Longrightarrow> x = x + z && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n<m. \<not> x !! n; \<forall>n\<ge>m. \<not> z !! n; x !! n; n < LENGTH('a); z !! n\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>\<forall>n<m. \<not> x !! n; \<forall>n\<ge>m. \<not> z !! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x !! n = ((x !! n \<or> z !! n) \<and> m \<le> n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<m. \<not> x !! n; \<forall>n\<ge>m. \<not> z !! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x !! n = ((x !! n \<or> z !! n) \<and> m \<le> n)
theory Word_Lemmas_Internal

lemma word_and_mask_shift_eq_0:
  "n \<le> m \<Longrightarrow> x && mask n >> m = 0" by word_eqI

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

lemma word_mask_and_neg_shift_eq_0:
  "n < m \<Longrightarrow> - (1 << m) && mask n = 0" by (metis NOT_mask_AND_mask add.inverse_neutral leD less_imp_le mask_AND_NOT_mask mask_eqs(10)
            shiftl_1 t2n_mask_eq_if)

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

lemma aligned_mask_plus_bounded:
  "\<lbrakk> is_aligned x m; m < n; n < LENGTH('a) \<rbrakk> \<Longrightarrow> (x && mask n) + 2^m \<le> 2^n" for x :: "'a::len word" by (metis add_mask_fold and_mask_less' is_aligned_add_step_le is_aligned_after_mask is_aligned_mask
            leD leI order_less_imp_le t2n_mask_eq_if word_less_sub_1)

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

lemma aligned_mask_le_mask_minus:
  "\<lbrakk> is_aligned x m; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x && mask n \<le> mask n - mask m" for x :: "'a::len word" by (metis and_mask_less' is_aligned_after_mask is_aligned_neg_mask_eq'
           mask_2pm1 mask_sub neg_mask_mono_le word_less_sub_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x && mask n \<le> mask n - mask m
theory Word_Lemmas_Internal

lemma shiftr_anti_mono:
  "m \<le> n \<Longrightarrow> w >> n \<le> w >> m" for w :: "'a::len word" apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_eq_div zdiv_mono2) done

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

lemma mask_shift_neg_mask_eq:
  "\<lbrakk> n' \<le> n; x \<le> mask (m+n') \<rbrakk> \<Longrightarrow> (x && ~~ mask n) && (mask m << n') = x && ~~ mask n" by word_eqI_solve

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

lemma from_bool_inj[simp]:
  "(from_bool x = from_bool y) = (x = y)" unfolding from_bool_def by (auto split: bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (from_bool x = from_bool y) = (x = y) proof (prove)
goal (1 subgoal):
 1. ((case x of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) = (case y of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0)) = (x = y)
theory Word_Lemmas_Internal

lemma word_le_1_and_idem:
  "w \<le> 1 \<Longrightarrow> w AND 1 = w" for w :: "_ word" by (metis word_bw_same(1) word_le_1 word_log_esimps(7))

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

lemma from_to_bool_le_1_idem:
  "w \<le> 1 \<Longrightarrow> from_bool (to_bool w) = w" apply (subst word_le_1_and_idem[symmetric], assumption) apply (simp add: from_to_bool_last_bit) apply (simp add: word_le_1_and_idem) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<le> 1 \<Longrightarrow> from_bool (to_bool w) = w proof (prove)
goal (1 subgoal):
 1. w \<le> 1 \<Longrightarrow> from_bool (to_bool (w && 1)) = w proof (prove)
goal (1 subgoal):
 1. w \<le> 1 \<Longrightarrow> w && 1 = w proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma and_1_0_not_bit_0:
  "(w && 1 = 0) = (\<not> (w::'a::len word) !! 0)" using to_bool_and_1[simplified to_bool_def, where x=w] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w && 1 = 0) = (\<not> w !! 0) proof (prove)
using this:
(0 \<noteq> w && 1) = w !! 0

goal (1 subgoal):
 1. (w && 1 = 0) = (\<not> w !! 0)
theory Word_Lemmas_Internal

lemma unat_scast_up:
  "\<lbrakk> LENGTH('a) \<le> LENGTH('b); 0 \<le> sint x \<rbrakk> \<Longrightarrow>unat (scast x::'b::len word) = unat x"
  for x :: "'a :: len  word" apply (simp flip: bit_last_iff not_less) apply word_eqI apply (clarsimp simp: min_def split: if_splits) apply (rule conjI; clarsimp) apply (drule test_bit_lenD) apply clarsimp apply (metis le_antisym nat_le_Suc_less_imp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) \<le> LENGTH('b); 0 \<le> sint x\<rbrakk> \<Longrightarrow> unat (SCAST('a \<rightarrow> 'b) x) = unat x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> LENGTH('b) < LENGTH('a); \<not> x !! (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> unat (SCAST('a \<rightarrow> 'b) x) = unat x proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> (n < LENGTH('b) \<and> x !! min (LENGTH('a) - Suc 0) n) = x !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> (LENGTH('a) - Suc 0 \<le> n \<longrightarrow> \<not> x !! n) \<and> (\<not> LENGTH('a) - Suc 0 \<le> n \<longrightarrow> (n < LENGTH('b) \<and> x !! n) = x !! n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); LENGTH('a) - Suc 0 \<le> n; x !! n\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); \<not> LENGTH('a) - Suc 0 \<le> n\<rbrakk> \<Longrightarrow> (n < LENGTH('b) \<and> x !! n) = x !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); LENGTH('a) - Suc 0 \<le> n; n < LENGTH('a) \<and> x !! n\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); \<not> LENGTH('a) - Suc 0 \<le> n\<rbrakk> \<Longrightarrow> (n < LENGTH('b) \<and> x !! n) = x !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); LENGTH('a) - Suc 0 \<le> n; n < LENGTH('a); x !! n\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); \<not> LENGTH('a) - Suc 0 \<le> n\<rbrakk> \<Longrightarrow> (n < LENGTH('b) \<and> x !! n) = x !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>LENGTH('a) \<le> LENGTH('b); \<not> x !! (LENGTH('a) - Suc 0); \<not> LENGTH('a) - Suc 0 \<le> n\<rbrakk> \<Longrightarrow> (n < LENGTH('b) \<and> x !! n) = x !! n proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma unat_uint_less:
  "unat x < nat i \<Longrightarrow> uint x < i" for x :: "'a :: len word" by (simp add: zless_nat_eq_int_zless)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < nat i \<Longrightarrow> uint x < i
theory Word_Lemmas_Internal

lemma sint_ge_zero_uint:
  "uint x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (x :: 'a :: len word) \<ge> 0" by (simp add: sint_eq_uint_2pl word_2p_lem wsst_TYs(3))

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

lemma sint_ge_zero_unat:
  "unat x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (x :: 'a :: len word) \<ge> 0" by (fastforce intro: sint_ge_zero_uint unat_uint_less simp: nat_power_eq)

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

lemma unat_ucast_unat_id:
  "unat x < 2 ^ LENGTH('b) \<Longrightarrow> unat (UCAST('a::len \<rightarrow> 'b::len) x) = unat x" by (simp add: unat_eq_of_nat)

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

lemma ucast_up_preserves_gt0:
  "\<lbrakk> 0 < x; LENGTH('a) < LENGTH('b) \<rbrakk> \<Longrightarrow> 0 < (ucast x :: 'b::len word)" for x :: "'a::len word" by (metis ucast_0 ucast_less_ucast_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < x; LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> 0 < UCAST('a \<rightarrow> 'b) x
theory Word_Lemmas_Internal

lemma ucast_up_preserves_not0:
  "\<lbrakk> x \<noteq> 0; LENGTH('a) < LENGTH('b::len) \<rbrakk> \<Longrightarrow> (ucast x :: 'b::len word) \<noteq> 0"
  for x :: "'a::len word" by (metis ucast_0 ucast_ucast_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<noteq> 0
theory Word_Lemmas_Internal

lemma unat_le_fold:
  "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat x \<le> n) = (x \<le> of_nat n)" for x::"'a::len word" by (simp add: word_le_nat_alt unat_of_nat_eq)

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

lemma ucast_and_mask_drop:
  "LENGTH('a) \<le> n \<Longrightarrow> (ucast w :: 'b::len word) && mask n = ucast w" for w::"'a::len word" by word_eqI (fastforce dest: test_bit_lenD)

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

lemma add_mask_ignore:
  "x && mask n = 0 \<Longrightarrow> v + x && mask n = v && mask n" by (metis add_0_right mask_eqs(2))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> v + x && mask n = v && mask n
theory Word_Lemmas_Internal

lemma word_ctz_upcast_id:
  "\<lbrakk> x \<noteq> 0; is_up (ucast::'a word \<Rightarrow>'b word) \<rbrakk> \<Longrightarrow>
  word_ctz (ucast x :: 'b::len word) = word_ctz x" for x :: "'a::len word" unfolding word_ctz_def by (simp add: ucast_up_app[where n="LENGTH('b) - LENGTH('a)"]
                source_size_def target_size_def is_up_def eq_zero_set_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; is_up UCAST('a \<rightarrow> 'b)\<rbrakk> \<Longrightarrow> word_ctz (UCAST('a \<rightarrow> 'b) x) = word_ctz x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; is_up UCAST('a \<rightarrow> 'b)\<rbrakk> \<Longrightarrow> length (takeWhile Not (rev (to_bl (UCAST('a \<rightarrow> 'b) x)))) = length (takeWhile Not (rev (to_bl x)))
theory Word_Lemmas_Internal

lemma ucast_ucast_mask_id:
  "\<lbrakk> LENGTH('b::len) < LENGTH('a); n = LENGTH('b) \<rbrakk> \<Longrightarrow>
   UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n" for x :: "'a::len word" by (simp add: ucast_ucast_len[OF eq_mask_less])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) < LENGTH('a); n = LENGTH('b)\<rbrakk> \<Longrightarrow> UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n
theory Word_Lib_Sumo

lemma distinct_lemma: "f x \<noteq> f y \<Longrightarrow> x \<noteq> y" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x \<noteq> f y \<Longrightarrow> x \<noteq> y
theory Word_Lib_Sumo

lemma word_fixed_sint_1[simp]:
  "sint (1::8 word) = 1"
  "sint (1::16 word) = 1"
  "sint (1::32 word) = 1"
  "sint (1::64 word) = 1" by (auto simp: sint_word_ariths)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sint 1 = 1 &&& sint 1 = 1) &&& sint 1 = 1 &&& sint 1 = 1
theory Machine_Word_32_Basics

lemma word_bits_conv [code]:
  \<open>word_bits = 32\<close> by (simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_bits = 32
theory Machine_Word_32_Basics

lemma n_less_word_bits:
  "(n < word_bits) = (n < 32)" by (simp add: word_bits_def word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n < word_bits) = (n < 32)
theory Machine_Word_32_Basics

lemma of_nat32_0:
  "\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0" by (erule of_nat_0, simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_nat n = 0; n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0
theory Machine_Word_32

lemma word_bits_len_of:
  \<open>LENGTH(machine_word_len) = word_bits\<close> by (simp add: word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH(32) = word_bits
theory Machine_Word_32

lemma word_bits_size:
  "size (w :: machine_word) = word_bits" by (simp add: word_bits_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size w = word_bits
theory Machine_Word_32

lemma word_bits_word_size_conv:
  \<open>word_bits = word_size * 8\<close> by (simp add: word_bits_def word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_bits = word_size * 8
theory Machine_Word_32

lemma lt_word_bits_lt_pow:
  "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits" by (simp add: word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits
theory Machine_Word_32

lemma if_then_1_else_0:
  "((if P then 1 else 0) = (0 :: machine_word)) = (\<not> P)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then 1 else 0) = 0) = (\<not> P)
theory Machine_Word_32

lemma if_then_0_else_1:
  "((if P then 0 else 1) = (0 :: machine_word)) = (P)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then 0 else 1) = 0) = P
theory Machine_Word_32

lemma bool_mask [simp]:
  \<open>0 < x AND 1 \<longleftrightarrow> x AND 1 = 1\<close> for x :: machine_word by (rule bool_mask') auto

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

lemma in_16_range:
  "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: machine_word)) ` S"
  "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: machine_word. r + x * 16) ` S" by (clarsimp simp: image_def elim!: bexI[rotated])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * 16) ` S) &&& (n - 1 \<in> S \<Longrightarrow> r + (16 * n - 16) \<in> (\<lambda>x. r + x * 16) ` S)
theory Machine_Word_32

lemma le_step_down_word_3:
  fixes x :: machine_word
  shows "\<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1" by (fact le_step_down_word_2)

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

lemma shiftr_1:
  "(x::machine_word) >> 1 = 0 \<Longrightarrow> x < 2" apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >> 1 = 0 \<Longrightarrow> x < 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. take_bit LENGTH(32) (drop_bit 1 (take_bit LENGTH(32) x)) = take_bit LENGTH(32) 0 \<Longrightarrow> take_bit LENGTH(32) x < take_bit LENGTH(32) 2 proof (prove)
goal (1 subgoal):
 1. \<And>x. drop_bit (Suc 0) (take_bit 32 x) = 0 \<Longrightarrow> take_bit 32 x < 2 proof (prove)
goal:
No subgoals!
theory Machine_Word_32

lemma Suc_unat_mask_div:
  "Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)" by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
    flip: drop_bit_eq_div word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc (unat (mask sz div word_size)) = 2 ^ (min sz word_bits - word_size_bits)
theory Machine_Word_32

lemma ucast_not_helper:
  fixes a::"8 word"
  assumes a: "a \<noteq> 0xFF"
  shows "ucast a \<noteq> (0xFF::machine_word)" proof assume "ucast a = (0xFF::machine_word)" also have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp finally show False using a apply - apply (drule up_ucast_inj, simp) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) a \<noteq> 255 proof (state)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) a = 255 \<Longrightarrow> False proof (state)
this:
UCAST(8 \<rightarrow> 32) a = 255

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) a = 255 \<Longrightarrow> False proof (state)
this:
UCAST(8 \<rightarrow> 32) a = 255

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) a = 255 \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. 255 = UCAST(8 \<rightarrow> 32) 255 proof (state)
this:
255 = UCAST(8 \<rightarrow> 32) 255

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 32) a = 255 \<Longrightarrow> False proof (chain)
picking this:
UCAST(8 \<rightarrow> 32) a = UCAST(8 \<rightarrow> 32) 255 proof (prove)
using this:
UCAST(8 \<rightarrow> 32) a = UCAST(8 \<rightarrow> 32) 255

goal (1 subgoal):
 1. False proof (prove)
using this:
UCAST(8 \<rightarrow> 32) a = UCAST(8 \<rightarrow> 32) 255
a \<noteq> 255

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(8 \<rightarrow> 32) a = UCAST(8 \<rightarrow> 32) 255; a \<noteq> 255\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 255; a = 255\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals!