[STATEMENT]
lemma strip_while_dropWhile_commute:
  "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])
 2. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])
 2. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])

goal (1 subgoal):
 1. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)

goal (1 subgoal):
 1. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
proof (cases "\<forall>y\<in>set xs. P y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>y\<in>set xs. P y \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
 2. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set xs. P y

goal (2 subgoals):
 1. \<forall>y\<in>set xs. P y \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
 2. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
with dropWhile_append2 [of "rev xs"]
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> set (rev xs) \<Longrightarrow> ?P x) \<Longrightarrow> dropWhile ?P (rev xs @ ?ys) = dropWhile ?P ?ys
\<forall>y\<in>set xs. P y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set (rev xs) \<Longrightarrow> ?P x) \<Longrightarrow> dropWhile ?P (rev xs @ ?ys) = dropWhile ?P ?ys
\<forall>y\<in>set xs. P y

goal (1 subgoal):
 1. strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
by (auto simp add: strip_while_def dest: set_dropWhileD)
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))

goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y\<in>set xs. P y)

goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y\<in>set xs. P y)
[PROOF STEP]
obtain y where "y \<in> set xs" and "\<not> P y"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y\<in>set xs. P y)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> set xs; \<not> P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> set xs
\<not> P y

goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
with Cons dropWhile_append3 [of P y "rev xs"]
[PROOF STATE]
proof (chain)
picking this:
strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)
\<not> P y \<Longrightarrow> dropWhile P (rev xs @ y # ?ys) = dropWhile P (rev xs) @ y # ?ys
y \<in> set xs
\<not> P y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)
\<not> P y \<Longrightarrow> dropWhile P (rev xs @ y # ?ys) = dropWhile P (rev xs) @ y # ?ys
y \<in> set xs
\<not> P y

goal (1 subgoal):
 1. strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
by (simp add: strip_while_def)
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed