theory Aligned

lemma drop_minus_lem:
  "\<lbrakk> n \<le> length xs; 0 < n; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1)  # drop (Suc (n' - n)) xs" proof (induct xs arbitrary: n n') case Nil then show ?case by simp next case (Cons y ys) from Cons.prems show ?case apply simp apply (cases "n = Suc (length ys)") apply (simp add: nth_append) apply (simp add: Suc_diff_le Cons.hyps nth_append) apply clarsimp apply arith done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs proof (state)
goal (2 subgoals):
 1. \<And>n n'. \<lbrakk>n \<le> length []; 0 < n; n' = length []\<rbrakk> \<Longrightarrow> drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []
 2. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs) proof (state)
this:
n \<le> length []
0 < n
n' = length []

goal (2 subgoals):
 1. \<And>n n'. \<lbrakk>n \<le> length []; 0 < n; n' = length []\<rbrakk> \<Longrightarrow> drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []
 2. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs) proof (chain)
picking this:
n \<le> length []
0 < n
n' = length [] proof (prove)
using this:
n \<le> length []
0 < n
n' = length []

goal (1 subgoal):
 1. drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) [] proof (state)
this:
drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []

goal (1 subgoal):
 1. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs) proof (state)
goal (1 subgoal):
 1. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs) proof (state)
this:
\<lbrakk>?n \<le> length ys; 0 < ?n; ?n' = length ys\<rbrakk> \<Longrightarrow> drop (?n' - ?n) ys = rev ys ! (?n - 1) # drop (Suc (?n' - ?n)) ys
n \<le> length (y # ys)
0 < n
n' = length (y # ys)

goal (1 subgoal):
 1. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs) proof (chain)
picking this:
n \<le> length (y # ys)
0 < n
n' = length (y # ys) proof (prove)
using this:
n \<le> length (y # ys)
0 < n
n' = length (y # ys)

goal (1 subgoal):
 1. drop (n' - n) (y # ys) = rev (y # ys) ! (n - 1) # drop (Suc (n' - n)) (y # ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n = Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys
 2. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys)\<rbrakk> \<Longrightarrow> \<not> n - Suc 0 < length ys \<longrightarrow> rev ys ! 0 = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys); \<not> n - Suc 0 < length ys\<rbrakk> \<Longrightarrow> rev ys ! 0 = y proof (prove)
goal:
No subgoals! proof (state)
this:
drop (n' - n) (y # ys) = rev (y # ys) ! (n - 1) # drop (Suc (n' - n)) (y # ys)

goal:
No subgoals!