kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_Lemmas_Internal

lemma word_wrap_of_natD:
  fixes x :: "'a :: len word"
  assumes wraps: "\<not> x \<le> x + of_nat n"
  shows   "\<exists>k. x + of_nat k = 0 \<and> k \<le> n" proof - show ?thesis proof (rule exI [where x = "unat (- x)"], intro conjI) show "x + of_nat (unat (-x)) = 0" by simp next show "unat (-x) \<le> n" proof (subst unat_minus') from wraps show "x \<noteq> 0" by (rule contrapos_pn, simp add: not_le) next show "2 ^ LENGTH('a) - unat x \<le> n" using wraps apply (simp add: no_olen_add_nat le_diff_conv not_less) apply (erule order_trans) apply (simp add: unat_of_nat) done qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>k. x + word_of_nat k = 0 \<and> k \<le> n proof (state)
goal (1 subgoal):
 1. \<exists>k. x + word_of_nat k = 0 \<and> k \<le> n proof (prove)
goal (1 subgoal):
 1. \<exists>k. x + word_of_nat k = 0 \<and> k \<le> n proof (state)
goal (2 subgoals):
 1. x + word_of_nat (unat (- x)) = 0
 2. unat (- x) \<le> n proof (prove)
goal (1 subgoal):
 1. x + word_of_nat (unat (- x)) = 0 proof (state)
this:
x + word_of_nat (unat (- x)) = 0

goal (1 subgoal):
 1. unat (- x) \<le> n proof (state)
goal (1 subgoal):
 1. unat (- x) \<le> n proof (prove)
goal (1 subgoal):
 1. unat (- x) \<le> n proof (state)
goal (2 subgoals):
 1. x \<noteq> 0
 2. 2 ^ LENGTH('a) - unat x \<le> n proof (chain)
picking this:
\<not> x \<le> x + word_of_nat n proof (prove)
using this:
\<not> x \<le> x + word_of_nat n

goal (1 subgoal):
 1. x \<noteq> 0 proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. 2 ^ LENGTH('a) - unat x \<le> n proof (state)
goal (1 subgoal):
 1. 2 ^ LENGTH('a) - unat x \<le> n proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH('a) - unat x \<le> n proof (prove)
using this:
\<not> x \<le> x + word_of_nat n

goal (1 subgoal):
 1. 2 ^ LENGTH('a) - unat x \<le> n proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH('a) \<le> unat x + unat (word_of_nat n) \<Longrightarrow> 2 ^ LENGTH('a) \<le> n + unat x proof (prove)
goal (1 subgoal):
 1. unat x + unat (word_of_nat n) \<le> n + unat x proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ LENGTH('a) - unat x \<le> n

goal:
No subgoals! proof (state)
this:
unat (- x) \<le> n

goal:
No subgoals! proof (state)
this:
\<exists>k. x + word_of_nat k = 0 \<and> k \<le> n

goal:
No subgoals!
theory Word_Lemmas_Internal

lemma two_bits_cases:
  "\<lbrakk> LENGTH('a) > 2; (x :: 'a :: len word) && 3 = 0 \<Longrightarrow> P; x && 3 = 1 \<Longrightarrow> P;
     x && 3 = 2 \<Longrightarrow> P; x && 3 = 3 \<Longrightarrow> P \<rbrakk>
   \<Longrightarrow> P" apply (frule and_mask_cases[where n=2 and x=x, simplified mask_eq]) using upt_conv_Cons by auto[1]

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 < LENGTH('a); x && 3 = 0 \<Longrightarrow> P; x && 3 = 1 \<Longrightarrow> P; x && 3 = 2 \<Longrightarrow> P; x && 3 = 3 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 < LENGTH('a); x && 3 = 0 \<Longrightarrow> P; x && 3 = 1 \<Longrightarrow> P; x && 3 = 2 \<Longrightarrow> P; x && 3 = 3 \<Longrightarrow> P; x && (1 << 2) - 1 \<in> word_of_nat ` set [0..<2\<^sup>2]\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
?i < ?j \<Longrightarrow> [?i..<?j] = ?i # [Suc ?i..<?j]

goal (1 subgoal):
 1. \<lbrakk>2 < LENGTH('a); x && 3 = 0 \<Longrightarrow> P; x && 3 = 1 \<Longrightarrow> P; x && 3 = 2 \<Longrightarrow> P; x && 3 = 3 \<Longrightarrow> P; x && (1 << 2) - 1 \<in> word_of_nat ` set [0..<2\<^sup>2]\<rbrakk> \<Longrightarrow> P
theory Word_Lemmas_Internal

lemma zero_OR_eq:
  "y = 0 \<Longrightarrow> (x || y) = x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y = 0 \<Longrightarrow> x || y = x
theory Word_Lemmas_Internal

lemma unat_and_mask_le:
  "n < LENGTH('a) \<Longrightarrow> unat (x && mask n) \<le> 2^n" for x::"'a::len word" by (simp add: and_mask_less' order_less_imp_le unat_less_power)

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

lemma sign_extend_less_mask_idem:
  "\<lbrakk> w \<le> mask n; n < size w \<rbrakk> \<Longrightarrow> sign_extend n w = w" by (simp add: sign_extend_def le_mask_imp_and_mask le_mask_high_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> mask n; n < size w\<rbrakk> \<Longrightarrow> sign_extend n w = w
theory Word_Lemmas_Internal

lemma word_and_le:
  "a \<le> c \<Longrightarrow> (a :: 'a :: len word) && b \<le> c" by (subst and.commute) (erule word_and_le')

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

lemma le_smaller_mask:
  "\<lbrakk> x \<le> mask n; n \<le> m \<rbrakk> \<Longrightarrow> x \<le> mask m" for x :: "'a::len word" by (erule (1) order.trans[OF _ mask_mono])

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

lemma upcast_less_unat_less:
  assumes less: "UCAST('a \<rightarrow> 'b) x < UCAST('a \<rightarrow> 'b) (of_nat y)"
  assumes len: "LENGTH('a::len) \<le> LENGTH('b::len)"
  assumes bound: "y < 2 ^ LENGTH('a)"
  shows "unat x < y" by (rule unat_mono[OF less, simplified unat_ucast_up_simp[OF len] unat_of_nat_eq[OF bound]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < y
theory Word_Lemmas_Internal

lemma word_ctz_max:
  "word_ctz w \<le> size w" unfolding word_ctz_def by (rule order_trans[OF List.length_takeWhile_le], clarsimp simp: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_ctz w \<le> size w proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (rev (to_bl w))) \<le> size w
theory Word_Lemmas_Internal

lemma scast_of_nat_small:
  "x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> scast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)" apply transfer apply simp by (metis One_nat_def id_apply int_eq_sint of_int_eq_id signed_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> SCAST('a \<rightarrow> 'b) (word_of_nat x) = word_of_nat x proof (prove)
goal (1 subgoal):
 1. \<And>x. x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) (int x)) = take_bit LENGTH('b) (int x) proof (prove)
goal (1 subgoal):
 1. \<And>x. x < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) (int x)) = take_bit LENGTH('b) (int x)
theory Word_Lemmas_Internal

lemma list_while_len_iff_takeWhile_eq_take:
  "list_while_len P n xs \<longleftrightarrow> takeWhile P xs = take n xs" unfolding list_while_len_def apply (rule iffI[OF takeWhile_eq_take_P_nth], simp+) apply (intro conjI allI impI) apply (rule takeWhile_take_has_property_nth, clarsimp) apply (drule_tac f=length in arg_cong, simp) apply (induct xs arbitrary: n; clarsimp split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_while_len P n xs = (takeWhile P xs = take n xs) proof (prove)
goal (1 subgoal):
 1. ((\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n))) = (takeWhile P xs = take n xs) proof (prove)
goal (1 subgoal):
 1. takeWhile P xs = take n xs \<Longrightarrow> (\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>takeWhile P xs = take n xs; i < n; i < length xs\<rbrakk> \<Longrightarrow> P (xs ! i)
 2. \<lbrakk>takeWhile P xs = take n xs; n < length xs\<rbrakk> \<Longrightarrow> \<not> P (xs ! n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>takeWhile P xs = take n xs; n < length xs\<rbrakk> \<Longrightarrow> \<not> P (xs ! n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; length (takeWhile P xs) = n\<rbrakk> \<Longrightarrow> \<not> P (xs ! n) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma list_while_len_exists:
  "\<exists>n. list_while_len P n xs" apply (induction xs; simp add: list_while_len_def) apply (rename_tac x xs) apply (erule exE) apply (case_tac "P x") apply (rule_tac x="Suc n" in exI, clarsimp) apply (case_tac i; simp) apply (rule_tac x=0 in exI, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>n. list_while_len P n xs proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<exists>n. (\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)) \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((a # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((a # xs) ! n)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<exists>n. (\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)) \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((x # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((x # xs) ! n)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs n. (\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)) \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((x # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((x # xs) ! n)) proof (prove)
goal (2 subgoals):
 1. \<And>x xs n. \<lbrakk>(\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)); P x\<rbrakk> \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((x # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((x # xs) ! n))
 2. \<And>x xs n. \<lbrakk>(\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)); \<not> P x\<rbrakk> \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((x # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((x # xs) ! n)) proof (prove)
goal (2 subgoals):
 1. \<And>x xs n i. \<lbrakk>P x; \<forall>i<n. i < length xs \<longrightarrow> P (xs ! i); n < length xs \<longrightarrow> \<not> P (xs ! n); i < Suc n; i < Suc (length xs)\<rbrakk> \<Longrightarrow> P ((x # xs) ! i)
 2. \<And>x xs n. \<lbrakk>(\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)); \<not> P x\<rbrakk> \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((x # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((x # xs) ! n)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs n. \<lbrakk>(\<forall>i<n. i < length xs \<longrightarrow> P (xs ! i)) \<and> (n < length xs \<longrightarrow> \<not> P (xs ! n)); \<not> P x\<rbrakk> \<Longrightarrow> \<exists>n. (\<forall>i<n. i < Suc (length xs) \<longrightarrow> P ((x # xs) ! i)) \<and> (n < Suc (length xs) \<longrightarrow> \<not> P ((x # xs) ! n)) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma takeWhile_truncate:
  "length (takeWhile P xs) \<le> m
   \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs" apply (cut_tac list_while_len_exists[where P=P and xs=xs], clarsimp) apply (case_tac "n \<le> m") apply (subgoal_tac "list_while_len P n (take m xs)") apply(simp add: list_while_len_iff_takeWhile_eq_take) apply (clarsimp simp: list_while_len_def) apply (simp add: list_while_len_iff_takeWhile_eq_take) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (takeWhile P xs) \<le> m \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; n \<le> m\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs
 2. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; \<not> n \<le> m\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; n \<le> m; list_while_len P n (take m xs)\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs
 2. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; n \<le> m\<rbrakk> \<Longrightarrow> list_while_len P n (take m xs)
 3. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; \<not> n \<le> m\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; n \<le> m\<rbrakk> \<Longrightarrow> list_while_len P n (take m xs)
 2. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; \<not> n \<le> m\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>length (takeWhile P xs) \<le> m; list_while_len P n xs; \<not> n \<le> m\<rbrakk> \<Longrightarrow> takeWhile P (take m xs) = takeWhile P xs proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma word_clz_shiftr_1:
  fixes z::"'a::len word"
  assumes wordsize: "1 < LENGTH('a)"
  shows "z \<noteq> 0 \<Longrightarrow> word_clz (z >> 1) = word_clz z + 1" supply word_size [simp] apply (clarsimp simp: word_clz_def) using wordsize apply (subst bl_shiftr, simp) apply (subst takeWhile_append2; simp add: wordsize) apply (subst takeWhile_truncate) using word_clz_nonzero_max[where w=z] apply (clarsimp simp: word_clz_def) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> word_clz (z >> 1) = word_clz z + 1 proof (prove)
goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> word_clz (z >> 1) = word_clz z + 1 proof (prove)
goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> length (takeWhile Not (to_bl (z >> Suc 0))) = Suc (length (takeWhile Not (to_bl z))) proof (prove)
using this:
1 < LENGTH('a)

goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> length (takeWhile Not (to_bl (z >> Suc 0))) = Suc (length (takeWhile Not (to_bl z))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<noteq> 0; 1 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (replicate (Suc 0) False @ take (size z - Suc 0) (to_bl z))) = Suc (length (takeWhile Not (to_bl z))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<noteq> 0; Suc 0 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (take (LENGTH('a) - Suc 0) (to_bl z))) = length (takeWhile Not (to_bl z)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>z \<noteq> 0; Suc 0 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (to_bl z)) \<le> LENGTH('a) - Suc 0
 2. \<lbrakk>z \<noteq> 0; Suc 0 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (to_bl z)) = length (takeWhile Not (to_bl z)) proof (prove)
using this:
z \<noteq> 0 \<Longrightarrow> word_clz z < size z

goal (2 subgoals):
 1. \<lbrakk>z \<noteq> 0; Suc 0 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (to_bl z)) \<le> LENGTH('a) - Suc 0
 2. \<lbrakk>z \<noteq> 0; Suc 0 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (to_bl z)) = length (takeWhile Not (to_bl z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<noteq> 0; Suc 0 < LENGTH('a)\<rbrakk> \<Longrightarrow> length (takeWhile Not (to_bl z)) = length (takeWhile Not (to_bl z)) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma shiftr_Suc:
  fixes x::"'a::len word"
  shows "x >> (Suc n) = x >> n >> 1" by (clarsimp simp: shiftr_shiftr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >> Suc n = x >> n >> 1
theory Word_Lemmas_Internal

lemma word_clz_shiftr:
  fixes z :: "'a::len word"
  shows "n < LENGTH('a) \<Longrightarrow> mask n < z \<Longrightarrow> word_clz (z >> n) = word_clz z + n" apply (simp add: le_mask_iff Not_eq_iff[THEN iffD2, OF le_mask_iff, simplified not_le]
                   word_neq_0_conv) apply (induction n; simp) apply (subgoal_tac "0 < z >> n") apply (subst shiftr_Suc) apply (subst word_clz_shiftr_1; simp) apply (clarsimp simp: word_less_nat_alt shiftr_div_2n' div_mult2_eq) apply (case_tac "unat z div 2 ^ n = 0"; simp) apply (clarsimp simp: div_eq_0_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); mask n < z\<rbrakk> \<Longrightarrow> word_clz (z >> n) = word_clz z + n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 0 < z >> n\<rbrakk> \<Longrightarrow> word_clz (z >> n) = word_clz z + n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < z >> n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < z >> Suc n\<rbrakk> \<Longrightarrow> word_clz (z >> Suc n) = Suc (word_clz z + n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < z >> n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < z >> Suc n; 0 < z >> n\<rbrakk> \<Longrightarrow> word_clz (z >> Suc n) = Suc (word_clz z + n)
 2. \<And>n. \<lbrakk>0 < z >> n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < z >> Suc n\<rbrakk> \<Longrightarrow> 0 < z >> n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < z >> n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < z >> Suc n; 0 < z >> n\<rbrakk> \<Longrightarrow> word_clz (z >> n >> 1) = Suc (word_clz z + n)
 2. \<And>n. \<lbrakk>0 < z >> n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < z >> Suc n\<rbrakk> \<Longrightarrow> 0 < z >> n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < z >> n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < z >> Suc n\<rbrakk> \<Longrightarrow> 0 < z >> n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < unat z div 2 ^ n \<Longrightarrow> word_clz (z >> n) = word_clz z + n; Suc n < LENGTH('a); 0 < unat z div 2 div 2 ^ n\<rbrakk> \<Longrightarrow> 0 < unat z div 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Suc n < LENGTH('a); 0 < unat z div 2 div 2 ^ n; unat z div 2 ^ n = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma mask_to_bl_exists_True:
  "x && mask n \<noteq> 0 \<Longrightarrow> \<exists>m. (rev (to_bl x)) ! m \<and> m < n" apply (subgoal_tac "\<not>(\<forall>m. m < n \<longrightarrow> \<not>(rev (to_bl x)) ! m)", fastforce) apply (intro notI) apply (subgoal_tac "x && mask n = 0", clarsimp) apply (clarsimp simp: eq_zero_set_bl in_set_conv_nth) apply (subst (asm) to_bl_nth, clarsimp simp: word_size) apply (clarsimp simp: word_size) by (meson nth_mask test_bit_bl word_and_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && mask n \<noteq> 0 \<Longrightarrow> \<exists>m. rev (to_bl x) ! m \<and> m < n proof (prove)
goal (1 subgoal):
 1. x && mask n \<noteq> 0 \<Longrightarrow> \<not> (\<forall>m<n. \<not> rev (to_bl x) ! m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n \<noteq> 0; \<forall>m<n. \<not> rev (to_bl x) ! m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n \<noteq> 0; \<forall>m<n. \<not> rev (to_bl x) ! m\<rbrakk> \<Longrightarrow> x && mask n = 0 proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>m<n. \<not> rev (to_bl x) ! m; i < LENGTH('a); to_bl (x && mask n) ! i\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>m<n. \<not> rev (to_bl x) ! m; i < LENGTH('a); (x && mask n) !! (size (x && mask n) - Suc i)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>m<n. \<not> rev (to_bl x) ! m; i < LENGTH('a); x !! (LENGTH('a) - Suc i); LENGTH('a) - Suc i < n\<rbrakk> \<Longrightarrow> False
theory Word_Lemmas_Internal

lemma word_ctz_bound_below_helper:
  fixes x :: "'a::len word"
  assumes sz: "n \<le> LENGTH('a)"
  shows "x && mask n = 0
         \<Longrightarrow> to_bl x = (take (LENGTH('a) - n) (to_bl x) @ replicate n False)" apply (subgoal_tac "replicate n False = drop (LENGTH('a) - n) (to_bl x)") apply (subgoal_tac "True \<notin> set (drop (LENGTH('a) - n) (to_bl x))") apply (drule list_of_false, clarsimp simp: sz) apply (drule_tac sym[where t="drop n x" for n x], clarsimp) apply (rule sym) apply (rule is_aligned_drop; clarsimp simp: is_aligned_mask sz) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> to_bl x = take (LENGTH('a) - n) (to_bl x) @ replicate n False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && mask n = 0; replicate n False = drop (LENGTH('a) - n) (to_bl x)\<rbrakk> \<Longrightarrow> to_bl x = take (LENGTH('a) - n) (to_bl x) @ replicate n False
 2. x && mask n = 0 \<Longrightarrow> replicate n False = drop (LENGTH('a) - n) (to_bl x) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && mask n = 0; replicate n False = drop (LENGTH('a) - n) (to_bl x); True \<notin> set (drop (LENGTH('a) - n) (to_bl x))\<rbrakk> \<Longrightarrow> to_bl x = take (LENGTH('a) - n) (to_bl x) @ replicate n False
 2. \<lbrakk>x && mask n = 0; replicate n False = drop (LENGTH('a) - n) (to_bl x)\<rbrakk> \<Longrightarrow> True \<notin> set (drop (LENGTH('a) - n) (to_bl x))
 3. x && mask n = 0 \<Longrightarrow> replicate n False = drop (LENGTH('a) - n) (to_bl x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && mask n = 0; replicate n False = drop (LENGTH('a) - n) (to_bl x)\<rbrakk> \<Longrightarrow> True \<notin> set (drop (LENGTH('a) - n) (to_bl x))
 2. x && mask n = 0 \<Longrightarrow> replicate n False = drop (LENGTH('a) - n) (to_bl x) proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> replicate n False = drop (LENGTH('a) - n) (to_bl x) proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> drop (LENGTH('a) - n) (to_bl x) = replicate n False proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma word_ctz_bound_below:
  fixes x :: "'a::len word"
  assumes sz[simp]: "n \<le> LENGTH('a)"
  shows "x && mask n = 0 \<Longrightarrow> n \<le> word_ctz x" apply (clarsimp simp: word_ctz_def) apply (subst word_ctz_bound_below_helper[OF sz]; simp) apply (subst takeWhile_append2; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> n \<le> word_ctz x proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> n \<le> length (takeWhile Not (rev (to_bl x))) proof (prove)
goal (1 subgoal):
 1. x && mask n = 0 \<Longrightarrow> n \<le> length (takeWhile Not (replicate n False @ rev (take (LENGTH('a) - n) (to_bl x)))) proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma word_less_max_simp:
  fixes w :: "'a::len word"
  assumes "max_w = -1"
  shows "w \<le> max_w" unfolding assms by simp

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

lemma word_and_mask_word_ctz_zero:
  assumes "l = word_ctz w"
  shows "w && mask l = 0" unfolding word_ctz_def assms apply (word_eqI) apply (drule takeWhile_take_has_property_nth) apply (simp add: test_bit_bl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && mask l = 0 proof (prove)
goal (1 subgoal):
 1. w && mask (length (takeWhile Not (rev (to_bl w)))) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < length (takeWhile Not (rev (to_bl w))); n < LENGTH('a); w !! n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a); w !! n; \<not> rev (to_bl w) ! n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Word_Lemmas_Internal

lemma word_ctz_len_word_and_mask_zero:
  fixes w :: "'a::len word"
  shows "word_ctz w = LENGTH('a) \<Longrightarrow> w = 0" by (drule sym, drule word_and_mask_word_ctz_zero, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_ctz w = LENGTH('a) \<Longrightarrow> w = 0