theory Rsplit

lemma word_rsplit_rcat_size [OF refl]:
  "word_rcat ws = frcw \<Longrightarrow>
    size frcw = length ws * LENGTH('a) \<Longrightarrow> word_rsplit frcw = ws"
  for ws :: "'a::len word list" apply (frule size_word_rsplit_rcat_size, assumption) apply (clarsimp simp add : word_size) apply (rule nth_equalityI, assumption) apply clarsimp apply (rule word_eqI [rule_format]) apply (rule trans) apply (rule test_bit_rsplit_alt) apply (clarsimp simp: word_size)+ apply (rule trans) apply (rule test_bit_rcat [OF refl refl]) apply (simp add: word_size) apply (subst rev_nth) apply arith apply (simp add: le0 [THEN [2] xtrans(7), THEN diff_Suc_less]) apply safe apply (simp add: diff_mult_distrib) apply (cases "size ws") apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_rcat ws = frcw; size frcw = length ws * LENGTH('a)\<rbrakk> \<Longrightarrow> word_rsplit frcw = ws proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_rcat ws = frcw; size frcw = length ws * LENGTH('a); length (word_rsplit frcw) = length ws\<rbrakk> \<Longrightarrow> word_rsplit frcw = ws proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws\<rbrakk> \<Longrightarrow> word_rsplit (word_rcat ws) = ws proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length (word_rsplit (word_rcat ws))\<rbrakk> \<Longrightarrow> word_rsplit (word_rcat ws) ! i = ws ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws\<rbrakk> \<Longrightarrow> word_rsplit (word_rcat ws) ! i = ws ! i proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> bit (word_rsplit (word_rcat ws) ! i) n = bit (ws ! i) n proof (prove)
goal (2 subgoals):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> bit (word_rsplit (word_rcat ws) ! i) n = ?s11 i n
 2. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> ?s11 i n = bit (ws ! i) n proof (prove)
goal (4 subgoals):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> i < length (word_rsplit (word_rcat ws))
 2. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> n < size (hd (word_rsplit (word_rcat ws)))
 3. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> 0 < length (word_rsplit (word_rcat ws))
 4. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < size (word_rsplit (word_rcat ws) ! i)\<rbrakk> \<Longrightarrow> bit (word_rcat ws) ((length (word_rsplit (word_rcat ws)) - Suc i) * size (hd (word_rsplit (word_rcat ws))) + n) = bit (ws ! i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rcat ws) ((length ws - Suc i) * LENGTH('a) + n) = bit (ws ! i) n proof (prove)
goal (2 subgoals):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rcat ws) ((length ws - Suc i) * LENGTH('a) + n) = ?s23 i n
 2. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ?s23 i n = bit (ws ! i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ((length ws - Suc i) * LENGTH('a) + n < size (word_rcat ws) \<and> ((length ws - Suc i) * LENGTH('a) + n) div size (hd ws) < length ws \<and> bit (rev ws ! (((length ws - Suc i) * LENGTH('a) + n) div size (hd ws))) (((length ws - Suc i) * LENGTH('a) + n) mod size (hd ws))) = bit (ws ! i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ((length ws - Suc i) * LENGTH('a) + n < length ws * LENGTH('a) \<and> length ws - Suc i < length ws \<and> bit (rev ws ! (length ws - Suc i)) n) = bit (ws ! i) n proof (prove)
goal (2 subgoals):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> length ws - Suc i < length ws
 2. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ((length ws - Suc i) * LENGTH('a) + n < length ws * LENGTH('a) \<and> length ws - Suc i < length ws \<and> bit (ws ! (length ws - Suc (length ws - Suc i))) n) = bit (ws ! i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ((length ws - Suc i) * LENGTH('a) + n < length ws * LENGTH('a) \<and> length ws - Suc i < length ws \<and> bit (ws ! (length ws - Suc (length ws - Suc i))) n) = bit (ws ! i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ((length ws - Suc i) * LENGTH('a) + n < length ws * LENGTH('a) \<and> bit (ws ! i) n) = bit (ws ! i) n proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a); bit (ws ! i) n\<rbrakk> \<Longrightarrow> (length ws - Suc i) * LENGTH('a) + n < length ws * LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a); bit (ws ! i) n\<rbrakk> \<Longrightarrow> length ws * LENGTH('a) - (LENGTH('a) + i * LENGTH('a)) + n < length ws * LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<And>i n. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a); bit (ws ! i) n; length ws = 0\<rbrakk> \<Longrightarrow> length ws * LENGTH('a) - (LENGTH('a) + i * LENGTH('a)) + n < length ws * LENGTH('a)
 2. \<And>i n nat. \<lbrakk>LENGTH('b) = length ws * LENGTH('a); length (word_rsplit (word_rcat ws)) = length ws; frcw = word_rcat ws; i < length ws; n < LENGTH('a); bit (ws ! i) n; length ws = Suc nat\<rbrakk> \<Longrightarrow> length ws * LENGTH('a) - (LENGTH('a) + i * LENGTH('a)) + n < length ws * LENGTH('a) proof (prove)
goal:
No subgoals!