[STATEMENT]
lemma drop_takeWhile:
    assumes "i\<le>length (takeWhile P l)"
    shows "drop i (takeWhile P l) = takeWhile P (drop i l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop i (takeWhile P l) = takeWhile P (drop i l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<le> length (takeWhile P l)

goal (1 subgoal):
 1. drop i (takeWhile P l) = takeWhile P (drop i l)
[PROOF STEP]
proof (induction l arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<le> length (takeWhile P []) \<Longrightarrow> drop i (takeWhile P []) = takeWhile P (drop i [])
 2. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
i \<le> length (takeWhile P [])

goal (2 subgoals):
 1. \<And>i. i \<le> length (takeWhile P []) \<Longrightarrow> drop i (takeWhile P []) = takeWhile P (drop i [])
 2. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i \<le> length (takeWhile P [])

goal (1 subgoal):
 1. drop i (takeWhile P []) = takeWhile P (drop i [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
drop i (takeWhile P []) = takeWhile P (drop i [])

goal (1 subgoal):
 1. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
case (Cons x l)
[PROOF STATE]
proof (state)
this:
?i \<le> length (takeWhile P l) \<Longrightarrow> drop ?i (takeWhile P l) = takeWhile P (drop ?i l)
i \<le> length (takeWhile P (x # l))

goal (1 subgoal):
 1. \<And>a l i. \<lbrakk>\<And>i. i \<le> length (takeWhile P l) \<Longrightarrow> drop i (takeWhile P l) = takeWhile P (drop i l); i \<le> length (takeWhile P (a # l))\<rbrakk> \<Longrightarrow> drop i (takeWhile P (a # l)) = takeWhile P (drop i (a # l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?i \<le> length (takeWhile P l) \<Longrightarrow> drop ?i (takeWhile P l) = takeWhile P (drop ?i l)
i \<le> length (takeWhile P (x # l))

goal (1 subgoal):
 1. drop i (takeWhile P (x # l)) = takeWhile P (drop i (x # l))
[PROOF STEP]
by (cases i) auto
[PROOF STATE]
proof (state)
this:
drop i (takeWhile P (x # l)) = takeWhile P (drop i (x # l))

goal:
No subgoals!
[PROOF STEP]
qed