theory Rsplit

lemma test_bit_rsplit:
  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
    k < length sw \<Longrightarrow> bit (rev sw ! k) m = bit w (k * size (hd sw) + m)"
  for sw :: "'a::len word list" apply (unfold word_rsplit_def word_test_bit_def) apply (rule trans) apply (rule_tac f = "\<lambda>x. bit x m" in arg_cong) apply (rule nth_map [symmetric]) apply simp apply (rule bin_nth_rsplit) apply simp_all apply (simp add : word_size rev_map) apply (rule trans) defer apply (rule map_ident [THEN fun_cong]) apply (rule refl [THEN map_cong]) apply (simp add: unsigned_of_int take_bit_int_eq_self_iff) using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = word_rsplit w; m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> bit (rev sw ! k) m = bit w (k * size (hd sw) + m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> bit (uint (rev sw ! k)) m = bit (uint w) (k * size (hd sw) + m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> bit (uint (rev sw ! k)) m = ?s
 2. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> ?s = bit (uint w) (k * size (hd sw) + m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> uint (rev sw ! k) = ?y3
 2. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> bit ?y3 m = bit (uint w) (k * size (hd sw) + m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> k < length (rev sw)
 2. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> bit (map uint (rev sw) ! k) m = bit (uint w) (k * size (hd sw) + m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> bit (map uint (rev sw) ! k) m = bit (uint w) (k * size (hd sw) + m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> 0 < size (hd sw)
 2. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> m < size (hd sw)
 3. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> rev (map uint (rev sw)) = bin_rsplit (size (hd sw)) (?nw7, uint w)
 4. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd sw); k < length sw\<rbrakk> \<Longrightarrow> k < length (map uint (rev sw)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < size (hd (map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)))); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> rev (map uint (rev (map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w))))) = bin_rsplit (size (hd (map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w))))) (?nw7, uint w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> map (uint \<circ> word_of_int) (bin_rsplit LENGTH('a) (LENGTH('b), uint w)) = bin_rsplit LENGTH('a) (?nw7, uint w) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> map (uint \<circ> word_of_int) (bin_rsplit LENGTH('a) (LENGTH('b), uint w)) = ?s12
 2. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> ?s12 = bin_rsplit LENGTH('a) (?nw7, uint w) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> ?s12 = bin_rsplit LENGTH('a) (?nw7, uint w)
 2. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> map (uint \<circ> word_of_int) (bin_rsplit LENGTH('a) (LENGTH('b), uint w)) = ?s12 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> map (uint \<circ> word_of_int) (bin_rsplit LENGTH('a) (LENGTH('b), uint w)) = map (\<lambda>x. x) (bin_rsplit LENGTH('a) (?nw7, uint w)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); x \<in> set (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> (uint \<circ> word_of_int) x = x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); x \<in> set (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> 0 \<le> x \<and> x < 2 ^ LENGTH('a) proof (prove)
using this:
\<lbrakk>0 < ?n; ?xs = bin_rsplit ?n (?nw, ?w); ?v \<in> set ?xs\<rbrakk> \<Longrightarrow> take_bit ?n ?v = ?v
(take_bit ?n ?k = ?k) = (0 \<le> ?k \<and> ?k < 2 ^ ?n)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>sw = map word_of_int (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); m < LENGTH('a); k < length (bin_rsplit LENGTH('a) (LENGTH('b), uint w)); x \<in> set (bin_rsplit LENGTH('a) (LENGTH('b), uint w))\<rbrakk> \<Longrightarrow> 0 \<le> x \<and> x < 2 ^ LENGTH('a)