[STATEMENT]
lemma worklist_tree_aux_rule:
assumes "worklist_tree_aux succs f (ws,s) = Some(ws',s')"
and "invariant I succs"
and "\<forall>x \<in> set ws. I x"
and "\<And>s. P [] s s"
and "\<And>r x ws s. I x \<Longrightarrow> \<forall>x \<in> set ws. I x \<Longrightarrow> P ws (f x s) r \<Longrightarrow> P (x#ws) s r"
shows "\<exists>rs. set rs = ((Rel succs)\<^sup>* ) `` (set ws) \<and> P rs s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
let ?R = "(Rel succs)\<^sup>* `` set ws"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
from worklist_tree_aux_Some_foldl[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> s' = foldl (\<lambda>s x. f x s) s rs
[PROOF STEP]
obtain rs where
    rs: "set rs = ?R" "s' = foldl (\<lambda>s x. f x s) s rs"
[PROOF STATE]
proof (prove)
using this:
\<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> s' = foldl (\<lambda>s x. f x s) s rs

goal (1 subgoal):
 1. (\<And>rs. \<lbrakk>set rs = (Rel succs)\<^sup>* `` set ws; s' = foldl (\<lambda>s x. f x s) s rs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set rs = (Rel succs)\<^sup>* `` set ws
s' = foldl (\<lambda>s x. f x s) s rs

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set rs = (Rel succs)\<^sup>* `` set ws
s' = foldl (\<lambda>s x. f x s) s rs

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
have "(\<forall>x \<in> set xs. I x) \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. I x \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs)
[PROOF STEP]
proof(induct xs arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. Ball (set []) I \<Longrightarrow> P [] s (foldl (\<lambda>s x. f x s) s [])
 2. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set []. I a

goal (2 subgoals):
 1. \<And>s. Ball (set []) I \<Longrightarrow> P [] s (foldl (\<lambda>s x. f x s) s [])
 2. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P [] s (foldl (\<lambda>s x. f x s) s [])
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
P [] ?s ?s

goal (1 subgoal):
 1. P [] s (foldl (\<lambda>s x. f x s) s [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P [] s (foldl (\<lambda>s x. f x s) s [])

goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set xs_. I a \<Longrightarrow> P xs_ ?s (foldl (\<lambda>s x. f x s) ?s xs_)
\<forall>a\<in>set (a_ # xs_). I a

goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs_. I a \<Longrightarrow> P xs_ ?s (foldl (\<lambda>s x. f x s) ?s xs_)
\<forall>a\<in>set (a_ # xs_). I a

goal (1 subgoal):
 1. P (a_ # xs_) s (foldl (\<lambda>s x. f x s) s (a_ # xs_))
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs_. I a \<Longrightarrow> P xs_ ?s (foldl (\<lambda>s x. f x s) ?s xs_)
\<forall>a\<in>set (a_ # xs_). I a
\<lbrakk>I ?x; \<forall>x\<in>set ?ws. I x; P ?ws (f ?x ?s) ?r\<rbrakk> \<Longrightarrow> P (?x # ?ws) ?s ?r

goal (1 subgoal):
 1. P (a_ # xs_) s (foldl (\<lambda>s x. f x s) s (a_ # xs_))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (a_ # xs_) s (foldl (\<lambda>s x. f x s) s (a_ # xs_))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set xs. I x \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs)

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set ?xs2. I x \<Longrightarrow> P ?xs2 s (foldl (\<lambda>s x. f x s) s ?xs2)

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
with invariant_succs[OF assms(2,3)]
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>(Rel succs)\<^sup>* `` set ws. I x
\<forall>x\<in>set ?xs2. I x \<Longrightarrow> P ?xs2 s (foldl (\<lambda>s x. f x s) s ?xs2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>(Rel succs)\<^sup>* `` set ws. I x
\<forall>x\<in>set ?xs2. I x \<Longrightarrow> P ?xs2 s (foldl (\<lambda>s x. f x s) s ?xs2)

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
by (metis rs)
[PROOF STATE]
proof (state)
this:
\<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'

goal:
No subgoals!
[PROOF STEP]
qed