kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Sublist

lemma take_prefix:
  "(take (length xs) ys = xs) = prefix xs ys" proof (induct xs arbitrary: ys) case Nil then show ?case by simp next case Cons then show ?case by (cases ys) auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (take (length xs) ys = xs) = prefix xs ys proof (state)
goal (2 subgoals):
 1. \<And>ys. (take (length []) ys = []) = prefix [] ys
 2. \<And>a xs ys. (\<And>ys. (take (length xs) ys = xs) = prefix xs ys) \<Longrightarrow> (take (length (a # xs)) ys = a # xs) = prefix (a # xs) ys proof (state)
this:


goal (2 subgoals):
 1. \<And>ys. (take (length []) ys = []) = prefix [] ys
 2. \<And>a xs ys. (\<And>ys. (take (length xs) ys = xs) = prefix xs ys) \<Longrightarrow> (take (length (a # xs)) ys = a # xs) = prefix (a # xs) ys proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. (take (length []) ys = []) = prefix [] ys proof (state)
this:
(take (length []) ys = []) = prefix [] ys

goal (1 subgoal):
 1. \<And>a xs ys. (\<And>ys. (take (length xs) ys = xs) = prefix xs ys) \<Longrightarrow> (take (length (a # xs)) ys = a # xs) = prefix (a # xs) ys proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. (\<And>ys. (take (length xs) ys = xs) = prefix xs ys) \<Longrightarrow> (take (length (a # xs)) ys = a # xs) = prefix (a # xs) ys proof (state)
this:
(take (length xs_) ?ys = xs_) = prefix xs_ ?ys

goal (1 subgoal):
 1. \<And>a xs ys. (\<And>ys. (take (length xs) ys = xs) = prefix xs ys) \<Longrightarrow> (take (length (a # xs)) ys = a # xs) = prefix (a # xs) ys proof (chain)
picking this:
(take (length xs_) ?ys = xs_) = prefix xs_ ?ys proof (prove)
using this:
(take (length xs_) ?ys = xs_) = prefix xs_ ?ys

goal (1 subgoal):
 1. (take (length (a_ # xs_)) ys = a_ # xs_) = prefix (a_ # xs_) ys proof (state)
this:
(take (length (a_ # xs_)) ys = a_ # xs_) = prefix (a_ # xs_) ys

goal:
No subgoals!
theory Strict_part_mono

lemma strict_part_mono_by_steps:
  "strict_part_mono {..n :: nat} f = (n \<noteq> 0 \<longrightarrow> f (n - 1) < f n \<and> strict_part_mono {.. n - 1} f)" apply (cases n; simp add: strict_part_mono_def) apply (safe; clarsimp) apply (case_tac "B = Suc nat"; simp) apply (case_tac "A = nat"; clarsimp) apply (erule order_less_trans [rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strict_part_mono {..n} f = (n \<noteq> 0 \<longrightarrow> f (n - 1) < f n \<and> strict_part_mono {..n - 1} f) proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> (\<forall>A\<in>{..Suc nat}. \<forall>B\<in>{..Suc nat}. A < B \<longrightarrow> f A < f B) = (f nat < f (Suc nat) \<and> (\<forall>A\<in>{..nat}. \<forall>B\<in>{..nat}. A < B \<longrightarrow> f A < f B)) proof (prove)
goal (1 subgoal):
 1. \<And>nat A B. \<lbrakk>n = Suc nat; B \<le> Suc nat; f nat < f (Suc nat); \<forall>A\<in>{..nat}. \<forall>B\<in>{..nat}. A < B \<longrightarrow> f A < f B; A < B\<rbrakk> \<Longrightarrow> f A < f B proof (prove)
goal (1 subgoal):
 1. \<And>nat A B. \<lbrakk>n = Suc nat; f nat < f (Suc nat); \<forall>A\<in>{..nat}. \<forall>B\<in>{..nat}. A < B \<longrightarrow> f A < f B; A < Suc nat; B = Suc nat\<rbrakk> \<Longrightarrow> f A < f (Suc nat) proof (prove)
goal (1 subgoal):
 1. \<And>nat A. \<lbrakk>n = Suc nat; f nat < f (Suc nat); \<forall>A\<in>{..nat}. \<forall>B\<in>{..nat}. A < B \<longrightarrow> f A < f B; A < Suc nat; A \<noteq> nat\<rbrakk> \<Longrightarrow> f A < f (Suc nat) proof (prove)
goal (1 subgoal):
 1. \<And>nat A. \<lbrakk>n = Suc nat; \<forall>A\<in>{..nat}. \<forall>B\<in>{..nat}. A < B \<longrightarrow> f A < f B; A < Suc nat; A \<noteq> nat\<rbrakk> \<Longrightarrow> f A < f nat proof (prove)
goal:
No subgoals!
theory Strict_part_mono

lemma strict_part_mono_singleton[simp]:
  "strict_part_mono {x} f" by (simp add: strict_part_mono_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strict_part_mono {x} f
theory Strict_part_mono

lemma strict_part_mono_lt:
  "\<lbrakk> x < f 0; strict_part_mono {.. n :: nat} f \<rbrakk> \<Longrightarrow> \<forall>m \<le> n. x < f m" by (auto simp add: strict_part_mono_def Ball_def intro: order.strict_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < f 0; strict_part_mono {..n} f\<rbrakk> \<Longrightarrow> \<forall>m\<le>n. x < f m
theory Strict_part_mono

lemma strict_part_mono_reverseE:
  "\<lbrakk> f n \<le> f m; strict_part_mono {.. N :: nat} f; n \<le> N \<rbrakk> \<Longrightarrow> n \<le> m" by (rule ccontr) (fastforce simp: linorder_not_le strict_part_mono_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f n \<le> f m; strict_part_mono {..N} f; n \<le> N\<rbrakk> \<Longrightarrow> n \<le> m
theory Next_and_Prev

lemma word_next_unfold:
  \<open>word_next w = (if w = - 1 then - 1 else w + 1)\<close> by transfer (simp flip: take_bit_eq_mask_iff_exp_dvd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_next w = (if w = - 1 then - 1 else w + 1)
theory Next_and_Prev

lemma [code]:
  \<open>Word.the_int (word_next w :: 'a::len word) =
    (if w = - 1 then Word.the_int w else Word.the_int w + 1)\<close> by transfer
    (simp add: mask_eq_exp_minus_1 take_bit_incr_eq flip: take_bit_eq_mask_iff_exp_dvd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Word.the_int (word_next w) = (if w = - 1 then Word.the_int w else Word.the_int w + 1)
theory Next_and_Prev

lemma [code]:
  \<open>Word.the_int (word_prev w :: 'a::len word) =
    (if w = 0 then Word.the_int w else Word.the_int w - 1)\<close> by transfer (simp add: take_bit_eq_0_iff take_bit_decr_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Word.the_int (word_prev w) = (if w = 0 then Word.the_int w else Word.the_int w - 1)
theory Next_and_Prev

lemma word_adjacent_union:
  "word_next e = s' \<Longrightarrow> s \<le> e \<Longrightarrow> s' \<le> e' \<Longrightarrow> {s..e} \<union> {s'..e'} = {s .. e'}" apply (simp add: word_next_unfold ivl_disj_un_two_touch split: if_splits) apply (drule sym) apply simp apply (subst word_atLeastLessThan_Suc_atLeastAtMost_union) apply (simp_all add: word_Suc_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_next e = s'; s \<le> e; s' \<le> e'\<rbrakk> \<Longrightarrow> {s..e} \<union> {s'..e'} = {s..e'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> e; s' \<le> e'; e \<noteq> - 1; e + 1 = s'\<rbrakk> \<Longrightarrow> {s..e} \<union> {s'..e'} = {s..e'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> e; s' \<le> e'; e \<noteq> - 1; s' = e + 1\<rbrakk> \<Longrightarrow> {s..e} \<union> {s'..e'} = {s..e'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<le> e; e + 1 \<le> e'; e \<noteq> - 1; s' = e + 1\<rbrakk> \<Longrightarrow> {s..e} \<union> {e + 1..e'} = {s..e'} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>s \<le> e; e + 1 \<le> e'; e \<noteq> - 1; s' = e + 1\<rbrakk> \<Longrightarrow> e \<noteq> - 1
 2. \<lbrakk>s \<le> e; e + 1 \<le> e'; e \<noteq> - 1; s' = e + 1\<rbrakk> \<Longrightarrow> s \<le> e
 3. \<lbrakk>s \<le> e; e + 1 \<le> e'; e \<noteq> - 1; s' = e + 1\<rbrakk> \<Longrightarrow> e \<le> e'
 4. \<lbrakk>s \<le> e; e + 1 \<le> e'; e \<noteq> - 1; s' = e + 1\<rbrakk> \<Longrightarrow> {s..e'} = {s..e'} proof (prove)
goal:
No subgoals!
theory Norm_Words

lemma bintrunc_numeral:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) x = of_bool (odd x) + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (x div 2)" by (simp add: numeral_eq_Suc take_bit_Suc mod_2_eq_odd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit (numeral k) x = of_bool (odd x) + 2 * take_bit (pred_numeral k) (x div 2)
theory Norm_Words

lemma neg_num_bintr:
  "(- numeral x :: 'a::len word) = word_of_int (take_bit LENGTH('a) (- numeral x))" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral x = word_of_int (take_bit LENGTH('a) (- numeral x))
theory Norm_Words

lemma minus_one_norm:
  "(-1 :: 'a :: len word) = of_nat (2 ^ LENGTH('a) - 1)" by (simp add:of_nat_diff)

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

lemma "f (7 :: 2 word) = f 3" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f 7 = f 3
theory Norm_Words

lemma "f 7 = f (3 :: 2 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f 7 = f 3
theory Norm_Words

lemma "f (-2) = f (21 + 1 :: 3 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 2) = f (21 + 1)
theory Norm_Words

lemma "f (-2) = f (13 + 1 :: 'a::len word)" apply simp  (* does not touch generic word length *)
   oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 2) = f (13 + 1) proof (prove)
goal (1 subgoal):
 1. f (word_of_int (take_bit LENGTH('a) (- 2))) = f 14 proof (prove)
goal (1 subgoal):
 1. f (word_of_int (take_bit LENGTH('a) (- 2))) = f 14
theory Norm_Words

lemma "(-1 :: 2 word) = 3" by simp

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

lemma "f (-2) = f (0xFFFFFFFE :: 32 signed word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 2) = f 4294967294
theory Norm_Words

lemma "f (-1) = f (15 :: 4 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 1) = f 15
theory Norm_Words

lemma "f (-1) = f (7 :: 3 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 1) = f 7
theory Norm_Words

lemma "f (-1) = f (0xFFFF :: 16 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 1) = f 65535
theory Norm_Words

lemma "f (-1) = f (0xFFFF + 1 :: 'a::len word)" apply simp  (* does not touch generic -1 *)
   oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (- 1) = f (65535 + 1) proof (prove)
goal (1 subgoal):
 1. f (- 1) = f 65536 proof (prove)
goal (1 subgoal):
 1. f (- 1) = f 65536
theory Rsplit

lemma word_rsplit_no:
  "(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
    map word_of_int (bin_rsplit (LENGTH('a::len))
      (LENGTH('b), take_bit (LENGTH('b)) (numeral bin)))" by (simp add: word_rsplit_def of_nat_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rsplit (numeral bin) = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), take_bit LENGTH('b) (numeral bin)))
theory Rsplit

lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0" by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
      split: prod.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (word_rsplit w = []) = (size w = 0)
theory Rsplit

lemma test_bit_rsplit_alt:
  \<open>bit ((word_rsplit w  :: 'b::len word list) ! i) m \<longleftrightarrow>
    bit w ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
  if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
  for w :: \<open>'a::len word\<close> apply (rule trans) apply (rule test_bit_cong) apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, simplified rev_rev_ident]) apply simp apply (rule that(1)) apply simp apply (rule test_bit_rsplit) apply (rule refl) apply (rule asm_rl) apply (rule that(2)) apply (rule diff_Suc_less) apply (rule that(3)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (word_rsplit w ! i) m = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (2 subgoals):
 1. bit (word_rsplit w ! i) m = ?s
 2. ?s = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (2 subgoals):
 1. word_rsplit w ! i = ?y3
 2. bit ?y3 m = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (2 subgoals):
 1. i < length (rev (word_rsplit w))
 2. bit (rev (word_rsplit w) ! (length (rev (word_rsplit w)) - Suc i)) m = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (2 subgoals):
 1. i < length (word_rsplit w)
 2. bit (rev (word_rsplit w) ! (length (rev (word_rsplit w)) - Suc i)) m = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (1 subgoal):
 1. bit (rev (word_rsplit w) ! (length (rev (word_rsplit w)) - Suc i)) m = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (1 subgoal):
 1. bit (rev (word_rsplit w) ! (length (word_rsplit w) - Suc i)) m = bit w ((length (word_rsplit w) - Suc i) * size (hd (word_rsplit w)) + m) proof (prove)
goal (3 subgoals):
 1. word_rsplit w = word_rsplit w
 2. m < size (hd (word_rsplit w))
 3. length (word_rsplit w) - Suc i < length (word_rsplit w) proof (prove)
goal (2 subgoals):
 1. m < size (hd (word_rsplit w))
 2. length (word_rsplit w) - Suc i < length (word_rsplit w) proof (prove)
goal (2 subgoals):
 1. m < size (hd (word_rsplit w))
 2. length (word_rsplit w) - Suc i < length (word_rsplit w) proof (prove)
goal (1 subgoal):
 1. length (word_rsplit w) - Suc i < length (word_rsplit w) proof (prove)
goal (1 subgoal):
 1. 0 < length (word_rsplit w) proof (prove)
goal:
No subgoals!
theory Rsplit

lemma word_rsplit_len_indep [OF refl refl refl refl]:
  "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
    word_rsplit v = sv \<Longrightarrow> length su = length sv" by (auto simp: word_rsplit_def bin_rsplit_len_indep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[u, v] = p; [su, sv] = q; word_rsplit u = su; word_rsplit v = sv\<rbrakk> \<Longrightarrow> length su = length sv
theory Rsplit

lemma length_word_rsplit_size:
  "n = LENGTH('a::len) \<Longrightarrow>
    length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n" by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = LENGTH('a) \<Longrightarrow> (length (word_rsplit w) \<le> m) = (size w \<le> m * n)
theory Rsplit

lemma length_word_rsplit_exp_size:
  "n = LENGTH('a::len) \<Longrightarrow>
    length (word_rsplit w :: 'a word list) = (size w + n - 1) div n" by (auto simp: word_rsplit_def word_size bin_rsplit_len)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = LENGTH('a) \<Longrightarrow> length (word_rsplit w) = (size w + n - 1) div n
theory Rsplit

lemma length_word_rsplit_even_size:
  "n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
    length (word_rsplit w :: 'a word list) = m" by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = LENGTH('a); size w = m * n\<rbrakk> \<Longrightarrow> length (word_rsplit w) = m
theory Rsplit

lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w" apply (rule word_eqI) apply (clarsimp simp: test_bit_rcat word_size) apply (subst refl [THEN test_bit_rsplit]) apply (simp_all add: word_size
      refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]]) apply safe apply (erule xtrans(7), rule dtle)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rcat (word_rsplit w) = w proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (word_rcat (word_rsplit w)) \<longrightarrow> bit (word_rcat (word_rsplit w)) n = bit w n proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> (n div LENGTH('b) < length (word_rsplit w) \<and> bit (rev (word_rsplit w) ! (n div LENGTH('b))) (n mod LENGTH('b))) = bit w n proof (prove)
goal (3 subgoals):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> n mod LENGTH('b) < size (hd (word_rsplit w))
 2. \<And>n. n < LENGTH('a) \<Longrightarrow> n div LENGTH('b) < length (word_rsplit w)
 3. \<And>n. n < LENGTH('a) \<Longrightarrow> (n div LENGTH('b) < length (word_rsplit w) \<and> bit w (n div LENGTH('b) * size (hd (word_rsplit w)) + n mod LENGTH('b))) = bit w n proof (prove)
goal (2 subgoals):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> n div LENGTH('b) * LENGTH('b) < LENGTH('a)
 2. \<And>n. n < LENGTH('a) \<Longrightarrow> (n div LENGTH('b) * LENGTH('b) < LENGTH('a) \<and> bit w n) = bit w n proof (prove)
goal (2 subgoals):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> n div LENGTH('b) * LENGTH('b) < LENGTH('a)
 2. \<And>n. \<lbrakk>n < LENGTH('a); bit w n\<rbrakk> \<Longrightarrow> n div LENGTH('b) * LENGTH('b) < LENGTH('a) proof (prove)
goal:
No subgoals!
theory Rsplit

lemma size_word_rsplit_rcat_size:
  "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a)
    \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
  for ws :: "'a::len word list" and frcw :: "'b::len word" by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_rcat ws = frcw; size frcw = length ws * LENGTH('a)\<rbrakk> \<Longrightarrow> length (word_rsplit frcw) = length ws
theory Rsplit

lemma word_rsplit_upt:
  "\<lbrakk> size x = LENGTH('a :: len) * n; n \<noteq> 0 \<rbrakk>
    \<Longrightarrow> word_rsplit x = map (\<lambda>i. ucast (x >> (i * LENGTH('a))) :: 'a word) (rev [0 ..< n])" apply (subgoal_tac "length (word_rsplit x :: 'a word list) = n") apply (rule nth_equalityI, simp) apply (intro allI word_eqI impI) apply (simp add: test_bit_rsplit_alt word_size) apply (simp add: nth_ucast bit_simps rev_nth field_simps) apply (simp add: length_word_rsplit_exp_size word_size) apply (subst diff_add_assoc) apply (simp flip: less_eq_Suc_le) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0\<rbrakk> \<Longrightarrow> word_rsplit x = map (\<lambda>i. ucast (x >> i * LENGTH('a))) (rev [0..<n]) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0; length (word_rsplit x) = n\<rbrakk> \<Longrightarrow> word_rsplit x = map (\<lambda>i. ucast (x >> i * LENGTH('a))) (rev [0..<n])
 2. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (word_rsplit x) = n proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0; length (word_rsplit x) = n; i < length (word_rsplit x)\<rbrakk> \<Longrightarrow> word_rsplit x ! i = map (\<lambda>i. ucast (x >> i * LENGTH('a))) (rev [0..<n]) ! i
 2. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (word_rsplit x) = n proof (prove)
goal (2 subgoals):
 1. \<And>i na. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0; length (word_rsplit x) = n; i < length (word_rsplit x); na < size (word_rsplit x ! i)\<rbrakk> \<Longrightarrow> bit (word_rsplit x ! i) na = bit (map (\<lambda>i. ucast (x >> i * LENGTH('a))) (rev [0..<n]) ! i) na
 2. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (word_rsplit x) = n proof (prove)
goal (2 subgoals):
 1. \<And>i na. \<lbrakk>LENGTH('b) = LENGTH('a) * n; length (word_rsplit x) = n; i < n; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit x ((n - Suc i) * LENGTH('a) + na) = bit (ucast (x >> rev [0..<n] ! i * LENGTH('a))) na
 2. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (word_rsplit x) = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x = LENGTH('a) * n; n \<noteq> 0\<rbrakk> \<Longrightarrow> length (word_rsplit x) = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) = LENGTH('a) * n; 0 < n\<rbrakk> \<Longrightarrow> (LENGTH('a) * n + LENGTH('a) - Suc 0) div LENGTH('a) = n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>LENGTH('b) = LENGTH('a) * n; 0 < n\<rbrakk> \<Longrightarrow> Suc 0 \<le> LENGTH('a)
 2. \<lbrakk>LENGTH('b) = LENGTH('a) * n; 0 < n\<rbrakk> \<Longrightarrow> (LENGTH('a) * n + (LENGTH('a) - Suc 0)) div LENGTH('a) = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) = LENGTH('a) * n; 0 < n\<rbrakk> \<Longrightarrow> (LENGTH('a) * n + (LENGTH('a) - Suc 0)) div LENGTH('a) = n proof (prove)
goal:
No subgoals!
theory Sgn_Abs

lemma word_sgn_0[simp]:
  "sgn 0 = (0::'a::len word)" by (simp add: sgn_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sgn 0 = 0
theory Sgn_Abs

lemma word_sgn_1[simp]:
  "sgn 1 = (1::'a::len word)" by (simp add: sgn_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sgn 1 = 1
theory Sgn_Abs

lemma word_sgn_max_word[simp]:
  "sgn (- 1) = (-1::'a::len word)" by (clarsimp simp: sgn_word_def word_sless_alt)

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

lemma word_abs_0[simp]:
  "\<bar>0\<bar> = (0::'a::len word)" by (simp add: abs_word_def)

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

lemma word_abs_1[simp]:
  "\<bar>1\<bar> = (1::'a::len word)" by (simp add: abs_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<bar>1\<bar> = 1
theory Sgn_Abs

lemma word_abs_max_word[simp]:
  "\<bar>- 1\<bar> = (1::'a::len word)" by (clarsimp simp: abs_word_def word_sle_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<bar>- 1\<bar> = 1
theory Sgn_Abs

lemma word_abs_msb:
  "\<bar>w\<bar> = (if msb w then -w else w)" for w::"'a::len word" by (simp add: abs_word_def msb_word_iff_sless_0 word_sless_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<bar>w\<bar> = (if msb w then - w else w)
theory Sgn_Abs

lemma word_sgn_0_0:
  "sgn a = 0 \<longleftrightarrow> a = 0" for a::"'a::len word" by (simp add: sgn_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sgn a = 0) = (a = 0)
theory Sgn_Abs

lemma word_sgn_1_pos:
  "1 < LENGTH('a) \<Longrightarrow> sgn a = 1 \<longleftrightarrow> 0 <s a" for a::"'a::len word" unfolding sgn_word_def by simp

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

lemma word_sgn_1_neg:
  "sgn a = - 1 \<longleftrightarrow> a <s 0" unfolding sgn_word_def using sint_1_cases by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sgn a = - 1) = (a <s 0) proof (prove)
goal (1 subgoal):
 1. ((if a = 0 then 0 else if 0 <s a then 1 else - 1) = - 1) = (a <s 0) proof (prove)
using this:
\<lbrakk>\<lbrakk>LENGTH(?'a) = 1; ?a = 0; sint ?a = 0\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>LENGTH(?'a) = 1; ?a = 1; sint 1 = - 1\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>1 < LENGTH(?'a); sint 1 = 1\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

lemma word_sgn_pos[simp]:
  "0 <s a \<Longrightarrow> sgn a = 1" by (simp add: sgn_word_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 <s a \<Longrightarrow> sgn a = 1
theory Sgn_Abs

lemma word_sgn_neg[simp]:
  "a <s 0 \<Longrightarrow> sgn a = - 1" by (simp only: word_sgn_1_neg)

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

lemma word_abs_sgn:
  "\<bar>k\<bar> = k * sgn k" for k :: "'a::len word" unfolding sgn_word_def abs_word_def by auto

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

lemma word_sgn_greater[simp]:
  "0 <s sgn a \<longleftrightarrow> 0 <s a" for a::"'a::len word" by (smt (verit) signed_eq_0_iff sint_1_cases sint_n1 word_sgn_0_0 word_sgn_neg word_sgn_pos
                  word_sless_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 <s sgn a) = (0 <s a)