[STATEMENT]
lemma i_stack_is_tree_path:
    "is_invar (\<lambda>s. stack s \<noteq> [] \<longrightarrow> (\<exists>v0 \<in> V0.
        path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))))
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 5. \<And>s s' u v e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (5 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 5. \<And>s s' u v e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
hence EQ[simp]: "stack s' = v # stack s"
                    "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. stack s' = v # stack s &&& tree_edges s' = insert (hd (stack s), v) (tree_edges s)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
stack s' = v # stack s
tree_edges s' = insert (hd (stack s), v) (tree_edges s)

goal (5 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 5. \<And>s s' u v e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
have NE[simp]: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. stack s \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stack s \<noteq> []

goal (5 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 5. \<And>s s' u v e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
obtain v0 where
      "v0 \<in> V0"
      "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v0 \<in> V0
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))

goal (5 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 5. \<And>s s' u v e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
with path_mono[OF _ this(2)] EQ
[PROOF STATE]
proof (chain)
picking this:
tree_edges s \<subseteq> ?E' \<Longrightarrow> path ?E' v0 (rev (tl (stack s))) (hd (stack s))
stack s' = v # stack s
tree_edges s' = insert (hd (stack s), v) (tree_edges s)
v0 \<in> V0
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))
[PROOF STEP]
have
      "path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))"
[PROOF STATE]
proof (prove)
using this:
tree_edges s \<subseteq> ?E' \<Longrightarrow> path ?E' v0 (rev (tl (stack s))) (hd (stack s))
stack s' = v # stack s
tree_edges s' = insert (hd (stack s), v) (tree_edges s)
v0 \<in> V0
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))

goal (1 subgoal):
 1. path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))

goal (5 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 5. \<And>s s' u v e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
with \<open>v0 \<in> V0\<close>
[PROOF STATE]
proof (chain)
picking this:
v0 \<in> V0
path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V0
path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))

goal (1 subgoal):
 1. stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
by (cases "stack s") (auto simp: path_simps)
[PROOF STATE]
proof (state)
this:
stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))

goal (4 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
case (finish s s')
[PROOF STATE]
proof (state)
this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u_} = {}
u_ = hd (stack s)
s' = finish u_ s\<lparr>state.more := e_\<rparr>

goal (4 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
hence EQ[simp]: "stack s' = tl (stack s)"
                    "tree_edges s' = tree_edges s"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u_} = {}
u_ = hd (stack s)
s' = finish u_ s\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. stack s' = tl (stack s) &&& tree_edges s' = tree_edges s
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
stack s' = tl (stack s)
tree_edges s' = tree_edges s

goal (4 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u_} = {}
u_ = hd (stack s)
s' = finish u_ s\<lparr>state.more := e_\<rparr>
[PROOF STEP]
obtain v0 where
      "v0 \<in> V0"
      "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)))
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u_} = {}
u_ = hd (stack s)
s' = finish u_ s\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v0 \<in> V0
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))

goal (4 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
hence P: "path (tree_edges s') v0 (rev (stack s')) (hd (stack s))"
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V0
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))

goal (1 subgoal):
 1. path (tree_edges s') v0 (rev (stack s')) (hd (stack s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
path (tree_edges s') v0 (rev (stack s')) (hd (stack s))

goal (4 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 4. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
assume A: "stack s' \<noteq> []"
[PROOF STATE]
proof (state)
this:
stack s' \<noteq> []

goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
with P
[PROOF STATE]
proof (chain)
picking this:
path (tree_edges s') v0 (rev (stack s')) (hd (stack s))
stack s' \<noteq> []
[PROOF STEP]
have "(hd (stack s'), hd (stack s)) \<in> tree_edges s'"
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s') v0 (rev (stack s')) (hd (stack s))
stack s' \<noteq> []

goal (1 subgoal):
 1. (hd (stack s'), hd (stack s)) \<in> tree_edges s'
[PROOF STEP]
by (auto simp: neq_Nil_conv path_simps)
[PROOF STATE]
proof (state)
this:
(hd (stack s'), hd (stack s)) \<in> tree_edges s'

goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(hd (stack s'), hd (stack s)) \<in> tree_edges s'

goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
from P A
[PROOF STATE]
proof (chain)
picking this:
path (tree_edges s') v0 (rev (stack s')) (hd (stack s))
stack s' \<noteq> []
[PROOF STEP]
have
        "path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))"
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s') v0 (rev (stack s')) (hd (stack s))
stack s' \<noteq> []

goal (1 subgoal):
 1. path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))

goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))

goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
note \<open>v0 \<in> V0\<close>
[PROOF STATE]
proof (state)
this:
v0 \<in> V0

goal (1 subgoal):
 1. stack s' \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(hd (stack s'), hd (stack s)) \<in> tree_edges s'
path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))
v0 \<in> V0
[PROOF STEP]
show "\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))"
[PROOF STATE]
proof (prove)
using this:
(hd (stack s'), hd (stack s)) \<in> tree_edges s'
path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))
v0 \<in> V0

goal (1 subgoal):
 1. \<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))
[PROOF STEP]
by (auto simp add: path_append_conv)
[PROOF STATE]
proof (state)
this:
\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))

goal (3 subgoals):
 1. \<And>e. stack (empty_state e) \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges (empty_state e)) v0 (rev (tl (stack (empty_state e)))) (hd (stack (empty_state e))))
 2. \<And>s s' v0 e. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
 3. \<And>s s' u v e c b. \<lbrakk>stack s \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> stack s' \<noteq> [] \<longrightarrow> (\<exists>v0\<in>V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s')))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma stack_is_path:
    "stack s \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path E v0 (rev (tl (stack s))) (hd (stack s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack s \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path E v0 (rev (tl (stack s))) (hd (stack s))
[PROOF STEP]
using stack_is_tree_path path_mono[OF tree_edges_ssE]
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))
path (tree_edges s) ?u ?p ?v \<Longrightarrow> path E ?u ?p ?v

goal (1 subgoal):
 1. stack s \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path E v0 (rev (tl (stack s))) (hd (stack s))
[PROOF STEP]
by blast


[STATEMENT]
lemma hd_succ_stack_is_path:
    assumes ne: "stack s \<noteq> []"
    and succ: "v \<in> succ (hd (stack s))"
    shows "\<exists>v0\<in>V0. path E v0 (rev (stack s)) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v0\<in>V0. path E v0 (rev (stack s)) v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v0\<in>V0. path E v0 (rev (stack s)) v
[PROOF STEP]
from stack_is_path[OF ne] succ
[PROOF STATE]
proof (chain)
picking this:
\<exists>v0\<in>V0. path E v0 (rev (tl (stack s))) (hd (stack s))
v \<in> E `` {hd (stack s)}
[PROOF STEP]
obtain v0 where
      "v0 \<in> V0"
      "path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v"
[PROOF STATE]
proof (prove)
using this:
\<exists>v0\<in>V0. path E v0 (rev (tl (stack s))) (hd (stack s))
v \<in> E `` {hd (stack s)}

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: path_append_conv)
[PROOF STATE]
proof (state)
this:
v0 \<in> V0
path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v

goal (1 subgoal):
 1. \<exists>v0\<in>V0. path E v0 (rev (stack s)) v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V0
path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v

goal (1 subgoal):
 1. \<exists>v0\<in>V0. path E v0 (rev (stack s)) v
[PROOF STEP]
using ne
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V0
path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v
stack s \<noteq> []

goal (1 subgoal):
 1. \<exists>v0\<in>V0. path E v0 (rev (stack s)) v
[PROOF STEP]
by (cases "stack s") auto
[PROOF STATE]
proof (state)
this:
\<exists>v0\<in>V0. path E v0 (rev (stack s)) v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tl_stack_hd_tree_path:
    assumes "stack s \<noteq> []"
    and "v \<in> set (tl (stack s))"
    shows "(v, hd (stack s)) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from stack_is_tree_path assms
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))
stack s \<noteq> []
v \<in> set (tl (stack s))
[PROOF STEP]
obtain v0 where
      "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> [] \<Longrightarrow> \<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))
stack s \<noteq> []
v \<in> set (tl (stack s))

goal (1 subgoal):
 1. (\<And>v0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))

goal (1 subgoal):
 1. (v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from assms path_member_reach_end[OF this]
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> []
v \<in> set (tl (stack s))
?v \<in> set (rev (tl (stack s))) \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []
v \<in> set (tl (stack s))
?v \<in> set (rev (tl (stack s))) \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v, hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed