theory Reversed_Bit_Lists

lemma nth_rcat_lem:
  "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
    rev (concat (map to_bl wl)) ! n =
    rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))" apply (induct wl) apply clarsimp apply (clarsimp simp add : nth_append size_rcat_lem) apply (simp flip: mult_Suc minus_div_mult_eq_mod add: less_Suc_eq_le not_less) apply (metis (no_types, lifting) diff_is_0_eq div_le_mono len_not_eq_0 less_Suc_eq less_mult_imp_div_less nonzero_mult_div_cancel_right not_le nth_Cons_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)) proof (prove)
goal (2 subgoals):
 1. n < length [] * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl [])) ! n = rev (to_bl (rev [] ! (n div LENGTH('a)))) ! (n mod LENGTH('a))
 2. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)); n < length (a # wl) * LENGTH('a)\<rbrakk> \<Longrightarrow> rev (concat (map to_bl (a # wl))) ! n = rev (to_bl (rev (a # wl) ! (n div LENGTH('a)))) ! (n mod LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)); n < length (a # wl) * LENGTH('a)\<rbrakk> \<Longrightarrow> rev (concat (map to_bl (a # wl))) ! n = rev (to_bl (rev (a # wl) ! (n div LENGTH('a)))) ! (n mod LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)); n < LENGTH('a) + length wl * LENGTH('a)\<rbrakk> \<Longrightarrow> (n div LENGTH('a) < length wl \<longrightarrow> \<not> n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))) \<and> (\<not> n div LENGTH('a) < length wl \<longrightarrow> (n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n mod LENGTH('a))) \<and> (\<not> n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n mod LENGTH('a)))) proof (prove)
goal (1 subgoal):
 1. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n - n div LENGTH('a) * LENGTH('a)); n < Suc (length wl) * LENGTH('a)\<rbrakk> \<Longrightarrow> (n div LENGTH('a) < length wl \<longrightarrow> length wl * LENGTH('a) \<le> n \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n - n div LENGTH('a) * LENGTH('a))) \<and> (length wl \<le> n div LENGTH('a) \<longrightarrow> (n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n - n div LENGTH('a) * LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n - n div LENGTH('a) * LENGTH('a))) \<and> (length wl * LENGTH('a) \<le> n \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n - n div LENGTH('a) * LENGTH('a)))) proof (prove)
goal:
No subgoals!