theory Reversed_Bit_Lists

lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs" apply (induct n arbitrary: xs) apply clarsimp apply clarsimp apply (rule trans [OF _ hd_Cons_tl]) apply (frule Suc_le_lessD) apply (simp add: rev_nth trans [OF drop_Suc drop_tl, symmetric]) apply (subst hd_drop_conv_nth) apply force apply simp_all apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs proof (prove)
goal (2 subgoals):
 1. \<And>xs. 0 \<le> length xs \<Longrightarrow> bl_of_nth 0 ((!) (rev xs)) = drop (length xs - 0) xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> bl_of_nth (Suc n) ((!) (rev xs)) = drop (length xs - Suc n) xs proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> bl_of_nth (Suc n) ((!) (rev xs)) = drop (length xs - Suc n) xs proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> rev xs ! n # drop (length xs - n) xs = drop (length xs - Suc n) xs proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> rev xs ! n # drop (length xs - n) xs = hd (drop (length xs - Suc n) xs) # tl (drop (length xs - Suc n) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs; n < length xs\<rbrakk> \<Longrightarrow> rev xs ! n # drop (length xs - n) xs = hd (drop (length xs - Suc n) xs) # tl (drop (length xs - Suc n) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc n) = hd (drop (length xs - Suc n) xs) \<and> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> [] proof (prove)
goal (3 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> length xs - Suc n < length xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc n) = xs ! (length xs - Suc n) \<and> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
 3. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc n) = xs ! (length xs - Suc n) \<and> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> length xs - n = Suc (length xs - Suc n) proof (prove)
goal:
No subgoals!