[STATEMENT]
lemma is_invarI [case_names init new_root finish visited discover]:
    \<comment> \<open>Establish a DFS invariant not taking into account the parameterization, cross/back-edges combined.\<close>
    assumes init': "\<And>e. I (empty_state e)"
    and new_root': "\<And>s s' v0 e.
       \<lbrakk>I 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> I s'"
    and finish': "\<And>s s' u e.
       \<lbrakk>I 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> I s'"
    and visited': "\<And>s s' u v e c b.
       \<lbrakk>I 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> I s'"
    and discover': "\<And>s s' u v e.
       \<lbrakk>I 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> I s'"
    shows "is_invar I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I
[PROOF STEP]
proof (induct rule: is_invarI_full)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. I (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>I 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> I s'
 3. \<And>s s' u e. \<lbrakk>I 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> I s'
 4. \<And>s s' u v e. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 5. \<And>s s' u v e. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 6. \<And>s s' u v e. \<lbrakk>I 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> I s'
[PROOF STEP]
case (cross_edge s s' u v e)
[PROOF STATE]
proof (state)
this:
I 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)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>

goal (6 subgoals):
 1. \<And>e. I (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>I 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> I s'
 3. \<And>s s' u e. \<lbrakk>I 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> I s'
 4. \<And>s s' u v e. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 5. \<And>s s' u v e. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 6. \<And>s s' u v e. \<lbrakk>I 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> I s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
I 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)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>

goal (1 subgoal):
 1. I s'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
[PROOF STEP]
apply (rule visited'[of s s' v u "insert (u,v) (cross_edges s)" "back_edges s" e])
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s
 2. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> cond s
 3. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> DFS_invar G param s
 4. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> DFS_invar G param s'
 5. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s \<noteq> []
 6. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> v \<in> pending s `` {u}
 7. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> v \<in> dom (discovered s)
 8. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> u = hd (stack s)
 9. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> cross_edges s \<subseteq> insert (u, v) (cross_edges s)
 10. \<lbrakk>I 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> back_edges s \<subseteq> back_edges s
A total of 11 subgoals...
[PROOF STEP]
apply clarsimp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
I s'

goal (5 subgoals):
 1. \<And>e. I (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>I 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> I s'
 3. \<And>s s' u e. \<lbrakk>I 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> I s'
 4. \<And>s s' u v e. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 5. \<And>s s' u v e. \<lbrakk>I 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> I s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. I (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>I 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> I s'
 3. \<And>s s' u e. \<lbrakk>I 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> I s'
 4. \<And>s s' u v e. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 5. \<And>s s' u v e. \<lbrakk>I 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> I s'
[PROOF STEP]
case (back_edge s s' u v e)
[PROOF STATE]
proof (state)
this:
I 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)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>

goal (5 subgoals):
 1. \<And>e. I (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>I 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> I s'
 3. \<And>s s' u e. \<lbrakk>I 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> I s'
 4. \<And>s s' u v e. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
 5. \<And>s s' u v e. \<lbrakk>I 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> I s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
I 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)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>

goal (1 subgoal):
 1. I s'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s'
[PROOF STEP]
apply (rule visited'[of s s' v u "cross_edges s" "insert (u,v) (back_edges s)" e])
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> I s
 2. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> cond s
 3. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> DFS_invar G param s
 4. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> DFS_invar G param s'
 5. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> stack s \<noteq> []
 6. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> v \<in> pending s `` {u}
 7. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> v \<in> dom (discovered s)
 8. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> u = hd (stack s)
 9. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> cross_edges s \<subseteq> cross_edges s
 10. \<lbrakk>I 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> back_edges s \<subseteq> insert (u, v) (back_edges s)
A total of 11 subgoals...
[PROOF STEP]
apply clarsimp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
I s'

goal (4 subgoals):
 1. \<And>e. I (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>I 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> I s'
 3. \<And>s s' u e. \<lbrakk>I 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> I s'
 4. \<And>s s' u v e. \<lbrakk>I 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> I s'
[PROOF STEP]
qed fact+


[STATEMENT]
lemma i_basic_invar: "is_invar basic_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar basic_invar
[PROOF STEP]
unfolding basic_invar_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. set (stack s) = dom (discovered s) - dom (finished s) \<and> distinct (stack s) \<and> (stack s \<noteq> [] \<longrightarrow> last (stack s) \<in> V0) \<and> dom (finished s) \<subseteq> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s \<subseteq> E)
[PROOF STEP]
apply (induction rule: is_invarI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>e. set (stack (empty_state e)) = dom (discovered (empty_state e)) - dom (finished (empty_state e)) \<and> distinct (stack (empty_state e)) \<and> (stack (empty_state e) \<noteq> [] \<longrightarrow> last (stack (empty_state e)) \<in> V0) \<and> dom (finished (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> Domain (pending (empty_state e)) \<subseteq> dom (discovered (empty_state e)) - dom (finished (empty_state e)) \<and> pending (empty_state e) \<subseteq> E
 2. \<And>s s' v0 e. \<lbrakk>set (stack s) = dom (discovered s) - dom (finished s) \<and> distinct (stack s) \<and> (stack s \<noteq> [] \<longrightarrow> last (stack s) \<in> V0) \<and> dom (finished s) \<subseteq> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s \<subseteq> E; 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> set (stack s') = dom (discovered s') - dom (finished s') \<and> distinct (stack s') \<and> (stack s' \<noteq> [] \<longrightarrow> last (stack s') \<in> V0) \<and> dom (finished s') \<subseteq> dom (discovered s') \<and> Domain (pending s') \<subseteq> dom (discovered s') - dom (finished s') \<and> pending s' \<subseteq> E
 3. \<And>s s' u e. \<lbrakk>set (stack s) = dom (discovered s) - dom (finished s) \<and> distinct (stack s) \<and> (stack s \<noteq> [] \<longrightarrow> last (stack s) \<in> V0) \<and> dom (finished s) \<subseteq> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s \<subseteq> E; 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> set (stack s') = dom (discovered s') - dom (finished s') \<and> distinct (stack s') \<and> (stack s' \<noteq> [] \<longrightarrow> last (stack s') \<in> V0) \<and> dom (finished s') \<subseteq> dom (discovered s') \<and> Domain (pending s') \<subseteq> dom (discovered s') - dom (finished s') \<and> pending s' \<subseteq> E
 4. \<And>s s' u v e c b. \<lbrakk>set (stack s) = dom (discovered s) - dom (finished s) \<and> distinct (stack s) \<and> (stack s \<noteq> [] \<longrightarrow> last (stack s) \<in> V0) \<and> dom (finished s) \<subseteq> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s \<subseteq> E; 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> set (stack s') = dom (discovered s') - dom (finished s') \<and> distinct (stack s') \<and> (stack s' \<noteq> [] \<longrightarrow> last (stack s') \<in> V0) \<and> dom (finished s') \<subseteq> dom (discovered s') \<and> Domain (pending s') \<subseteq> dom (discovered s') - dom (finished s') \<and> pending s' \<subseteq> E
 5. \<And>s s' u v e. \<lbrakk>set (stack s) = dom (discovered s) - dom (finished s) \<and> distinct (stack s) \<and> (stack s \<noteq> [] \<longrightarrow> last (stack s) \<in> V0) \<and> dom (finished s) \<subseteq> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s \<subseteq> E; 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> set (stack s') = dom (discovered s') - dom (finished s') \<and> distinct (stack s') \<and> (stack s' \<noteq> [] \<longrightarrow> last (stack s') \<in> V0) \<and> dom (finished s') \<subseteq> dom (discovered s') \<and> Domain (pending s') \<subseteq> dom (discovered s') - dom (finished s') \<and> pending s' \<subseteq> E
[PROOF STEP]
apply (clarsimp_all simp: neq_Nil_conv last_tl)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s v0 e. \<lbrakk>cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e\<rparr>); stack s = []; v0 \<in> V0; Domain ({v0} \<times> E `` {v0}) \<subseteq> insert v0 (dom (discovered s)) - dom (finished s) \<longrightarrow> dom (finished s) \<subseteq> insert v0 (dom (discovered s)) \<longrightarrow> {v0} = insert v0 (dom (discovered s)) - dom (finished s) \<longrightarrow> \<not> (insert v0 (dom (discovered s)) - dom (finished s)) \<times> E `` (insert v0 (dom (discovered s)) - dom (finished s)) \<subseteq> E; {} = dom (discovered s) - dom (finished s); dom (finished s) \<subseteq> dom (discovered s); Domain (pending s) = {}; pending s \<subseteq> E\<rbrakk> \<Longrightarrow> \<exists>y. discovered s v0 = Some y
 2. \<And>s e y ys. \<lbrakk>cond s; DFS_invar G param s; DFS_invar G param (finish y s\<lparr>state.more := e\<rparr>); pending s `` {y} = {}; stack s = y # ys; insert y (set ys) = dom (discovered s) - dom (finished s); (if ys = [] then y else last ys) \<in> V0; dom (finished s) \<subseteq> dom (discovered s); Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s); pending s \<subseteq> E; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> set ys = dom (discovered s) - insert y (dom (finished s)) \<and> y \<in> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - insert y (dom (finished s))
 3. \<And>s v e c b y ya ys. \<lbrakk>cond s; DFS_invar G param s; DFS_invar G param (s\<lparr>pending := pending s - {(y, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>); (y, v) \<in> pending s; cross_edges s \<subseteq> c; back_edges s \<subseteq> b; discovered s v = Some ya; stack s = y # ys; insert y (set ys) = dom (discovered s) - dom (finished s); (if ys = [] then y else last ys) \<in> V0; dom (finished s) \<subseteq> dom (discovered s); Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s); pending s \<subseteq> E; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> Domain (pending s - {(y, v)}) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s - {(y, v)} \<subseteq> E
 4. \<And>s v e y ys. \<lbrakk>cond s; DFS_invar G param s; DFS_invar G param (discover y v (s\<lparr>pending := pending s - {(y, v)}\<rparr>)\<lparr>state.more := e\<rparr>); (y, v) \<in> pending s; pending s - {(y, v)} \<subseteq> E \<longrightarrow> Domain (pending s - {(y, v)} \<union> {v} \<times> E `` {v}) \<subseteq> insert v (dom (discovered s)) - dom (finished s) \<longrightarrow> dom (finished s) \<subseteq> insert v (dom (discovered s)) \<longrightarrow> insert v (dom (discovered s) - dom (finished s)) = insert v (dom (discovered s)) - dom (finished s) \<longrightarrow> \<not> {v} \<times> E `` {v} \<subseteq> E; stack s = y # ys; insert y (set ys) = dom (discovered s) - dom (finished s); (if ys = [] then y else last ys) \<in> V0; dom (finished s) \<subseteq> dom (discovered s); Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s); pending s \<subseteq> E; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> \<exists>y. discovered s v = Some y
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pending_ssE: "pending s \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pending s \<subseteq> E
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. pending s \<subseteq> E
[PROOF STEP]
by (auto simp: basic_invar_def)


[STATEMENT]
lemma pendingD:
    "(u,v)\<in>pending s \<Longrightarrow> (u,v)\<in>E \<and> u\<in>dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> pending s \<Longrightarrow> (u, v) \<in> E \<and> u \<in> dom (discovered s)
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. (u, v) \<in> pending s \<Longrightarrow> (u, v) \<in> E \<and> u \<in> dom (discovered s)
[PROOF STEP]
by (auto simp: basic_invar_def)


[STATEMENT]
lemma stack_set_def:
    "set (stack s) = dom (discovered s) - dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (stack s) = dom (discovered s) - dom (finished s)
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. set (stack s) = dom (discovered s) - dom (finished s)
[PROOF STEP]
by (simp add: basic_invar_def)


[STATEMENT]
lemma stack_discovered:
    "set (stack s) \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
using stack_set_def
[PROOF STATE]
proof (prove)
using this:
set (stack s) = dom (discovered s) - dom (finished s)

goal (1 subgoal):
 1. set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
by auto


[STATEMENT]
lemma stack_distinct:
    "distinct (stack s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (stack s)
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. distinct (stack s)
[PROOF STEP]
by (simp add: basic_invar_def)


[STATEMENT]
lemma last_stack_in_V0:
    "stack s \<noteq> [] \<Longrightarrow> last (stack s) \<in> V0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack s \<noteq> [] \<Longrightarrow> last (stack s) \<in> V0
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. stack s \<noteq> [] \<Longrightarrow> last (stack s) \<in> V0
[PROOF STEP]
by (simp add: basic_invar_def)


[STATEMENT]
lemma stack_not_finished:
    "x \<in> set (stack s) \<Longrightarrow> x \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (stack s) \<Longrightarrow> x \<notin> dom (finished s)
[PROOF STEP]
using stack_set_def
[PROOF STATE]
proof (prove)
using this:
set (stack s) = dom (discovered s) - dom (finished s)

goal (1 subgoal):
 1. x \<in> set (stack s) \<Longrightarrow> x \<notin> dom (finished s)
[PROOF STEP]
by auto


[STATEMENT]
lemma discovered_not_stack_imp_finished:
    "x \<in> dom (discovered s) \<Longrightarrow> x \<notin> set (stack s) \<Longrightarrow> x \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom (discovered s); x \<notin> set (stack s)\<rbrakk> \<Longrightarrow> x \<in> dom (finished s)
[PROOF STEP]
using stack_set_def
[PROOF STATE]
proof (prove)
using this:
set (stack s) = dom (discovered s) - dom (finished s)

goal (1 subgoal):
 1. \<lbrakk>x \<in> dom (discovered s); x \<notin> set (stack s)\<rbrakk> \<Longrightarrow> x \<in> dom (finished s)
[PROOF STEP]
by auto


[STATEMENT]
lemma finished_discovered:
    "dom (finished s) \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
by (auto simp add: basic_invar_def)


[STATEMENT]
lemma finished_no_pending:
    "v \<in> dom (finished s) \<Longrightarrow> pending s `` {v} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> dom (finished s) \<Longrightarrow> pending s `` {v} = {}
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. v \<in> dom (finished s) \<Longrightarrow> pending s `` {v} = {}
[PROOF STEP]
by (auto simp add: basic_invar_def)


[STATEMENT]
lemma discovered_eq_finished_un_stack:
    "dom (discovered s) = dom (finished s) \<union> set (stack s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (discovered s) = dom (finished s) \<union> set (stack s)
[PROOF STEP]
using stack_set_def finished_discovered
[PROOF STATE]
proof (prove)
using this:
set (stack s) = dom (discovered s) - dom (finished s)
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. dom (discovered s) = dom (finished s) \<union> set (stack s)
[PROOF STEP]
by auto


[STATEMENT]
lemma pending_on_stack:
    "(v,w) \<in> pending s \<Longrightarrow> v \<in> set (stack s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> pending s \<Longrightarrow> v \<in> set (stack s)
[PROOF STEP]
using basic_invar
[PROOF STATE]
proof (prove)
using this:
basic_invar s

goal (1 subgoal):
 1. (v, w) \<in> pending s \<Longrightarrow> v \<in> set (stack s)
[PROOF STEP]
by (auto simp add: basic_invar_def)


[STATEMENT]
lemma empty_stack_imp_empty_pending:
    "stack s = [] \<Longrightarrow> pending s = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack s = [] \<Longrightarrow> pending s = {}
[PROOF STEP]
using pending_on_stack
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> pending s \<Longrightarrow> ?v \<in> set (stack s)

goal (1 subgoal):
 1. stack s = [] \<Longrightarrow> pending s = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma i_discovered_reachable:
    "is_invar (\<lambda>s. dom (discovered s) \<subseteq> reachable)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. dom (discovered s) \<subseteq> reachable)
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. dom (discovered (empty_state e)) \<subseteq> reachable
 2. \<And>s s' v0 e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 3. \<And>s s' u e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 4. \<And>s s' u v e c b. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 5. \<And>s s' u v e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
[PROOF STEP]
case (discover s)
[PROOF STATE]
proof (state)
this:
dom (discovered s) \<subseteq> reachable
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. dom (discovered (empty_state e)) \<subseteq> reachable
 2. \<And>s s' v0 e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 3. \<And>s s' u e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 4. \<And>s s' u v e c b. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 5. \<And>s s' u v e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dom (discovered s) \<subseteq> reachable
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]
interpret i: DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable
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. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. dom (discovered (empty_state e)) \<subseteq> reachable
 2. \<And>s s' v0 e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 3. \<And>s s' u e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 4. \<And>s s' u v e c b. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 5. \<And>s s' u v e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
dom (discovered s) \<subseteq> reachable
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]
show ?case
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable
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. dom (discovered s'_) \<subseteq> reachable
[PROOF STEP]
apply (clarsimp dest!: i.pendingD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>dom (discovered s) \<subseteq> reachable; cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; u_ = hd (stack s); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; v_ \<notin> reachable; (hd (stack s), v_) \<in> E; discovered s (hd (stack s)) = Some y\<rbrakk> \<Longrightarrow> \<exists>y. discovered s v_ = Some y
[PROOF STEP]
by (metis contra_subsetD list.set_sel(1) rtrancl_image_advance i.stack_discovered)
[PROOF STATE]
proof (state)
this:
dom (discovered s'_) \<subseteq> reachable

goal (4 subgoals):
 1. \<And>e. dom (discovered (empty_state e)) \<subseteq> reachable
 2. \<And>s s' v0 e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 3. \<And>s s' u e. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
 4. \<And>s s' u v e c b. \<lbrakk>dom (discovered s) \<subseteq> reachable; 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> dom (discovered s') \<subseteq> reachable
[PROOF STEP]
qed auto


[STATEMENT]
lemma i_discovered_closed: "is_invar discovered_closed"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar discovered_closed
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
case (finish s s')
[PROOF STATE]
proof (state)
this:
discovered_closed 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 (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
hence "(E - pending s) `` set (stack s) \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
discovered_closed 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. (E - pending s) `` set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
by (simp add: discovered_closed_def)
[PROOF STATE]
proof (state)
this:
(E - pending s) `` set (stack s) \<subseteq> dom (discovered s)

goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(E - pending s) `` set (stack s) \<subseteq> dom (discovered s)

goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
discovered_closed 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]
have "set (stack s') \<subseteq> set (stack s)"
[PROOF STATE]
proof (prove)
using this:
discovered_closed 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. set (stack s') \<subseteq> set (stack s)
[PROOF STEP]
by (auto simp add: neq_Nil_conv cond_def)
[PROOF STATE]
proof (state)
this:
set (stack s') \<subseteq> set (stack s)

goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(E - pending s) `` set (stack s) \<subseteq> dom (discovered s)
set (stack s') \<subseteq> set (stack s)
[PROOF STEP]
have "(E - pending s') `` set (stack s') \<subseteq> dom (discovered s')"
[PROOF STATE]
proof (prove)
using this:
(E - pending s) `` set (stack s) \<subseteq> dom (discovered s)
set (stack s') \<subseteq> set (stack s)

goal (1 subgoal):
 1. (E - pending s') `` set (stack s') \<subseteq> dom (discovered s')
[PROOF STEP]
using finish
[PROOF STATE]
proof (prove)
using this:
(E - pending s) `` set (stack s) \<subseteq> dom (discovered s)
set (stack s') \<subseteq> set (stack s)
discovered_closed 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. (E - pending s') `` set (stack s') \<subseteq> dom (discovered s')
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
(E - pending s') `` set (stack s') \<subseteq> dom (discovered s')

goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(E - pending s') `` set (stack s') \<subseteq> dom (discovered s')

goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
from \<open>stack s \<noteq> []\<close> finish
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> []
discovered_closed 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]
have "E``dom (finished s') \<subseteq> dom (discovered s')"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []
discovered_closed 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. E `` dom (finished s') \<subseteq> dom (discovered s')
[PROOF STEP]
apply (cases "stack s")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>stack s \<noteq> []; discovered_closed 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>; stack s = []\<rbrakk> \<Longrightarrow> E `` dom (finished s') \<subseteq> dom (discovered s')
 2. \<And>a list. \<lbrakk>stack s \<noteq> []; discovered_closed 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>; stack s = a # list\<rbrakk> \<Longrightarrow> E `` dom (finished s') \<subseteq> dom (discovered s')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>stack s \<noteq> []; discovered_closed 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>; stack s = a # list\<rbrakk> \<Longrightarrow> E `` dom (finished s') \<subseteq> dom (discovered s')
[PROOF STEP]
apply (simp add: discovered_closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>E `` dom (finished s) \<subseteq> dom (discovered s) \<and> (E - pending s) `` insert a (set list) \<subseteq> dom (discovered s); cond s; DFS_invar G param s; DFS_invar G param (finish a s\<lparr>state.more := e_\<rparr>); pending s `` {a} = {}; u_ = a; s' = finish a s\<lparr>state.more := e_\<rparr>; stack s = a # list\<rbrakk> \<Longrightarrow> E `` insert a (dom (finished s)) \<subseteq> dom (discovered s)
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
E `` dom (finished s') \<subseteq> dom (discovered s')

goal (5 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u e. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 5. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(E - pending s') `` set (stack s') \<subseteq> dom (discovered s')
E `` dom (finished s') \<subseteq> dom (discovered s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(E - pending s') `` set (stack s') \<subseteq> dom (discovered s')
E `` dom (finished s') \<subseteq> dom (discovered s')

goal (1 subgoal):
 1. discovered_closed s'
[PROOF STEP]
by (simp add: discovered_closed_def)
[PROOF STATE]
proof (state)
this:
discovered_closed s'

goal (4 subgoals):
 1. \<And>e. discovered_closed (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>discovered_closed 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> discovered_closed s'
 3. \<And>s s' u v e c b. \<lbrakk>discovered_closed 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> discovered_closed s'
 4. \<And>s s' u v e. \<lbrakk>discovered_closed 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> discovered_closed s'
[PROOF STEP]
qed (auto simp add: discovered_closed_def cond_def)


[STATEMENT]
lemma i_discovered_finite: "is_invar (\<lambda>s. finite (dom (discovered s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. finite (dom (discovered s)))
[PROOF STEP]
by (induction rule: is_invarI) auto


[STATEMENT]
lemma stack_reachable: "set (stack s) \<subseteq> reachable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (stack s) \<subseteq> reachable
[PROOF STEP]
using stack_discovered discovered_reachable
[PROOF STATE]
proof (prove)
using this:
set (stack s) \<subseteq> dom (discovered s)
dom (discovered s) \<subseteq> reachable

goal (1 subgoal):
 1. set (stack s) \<subseteq> reachable
[PROOF STEP]
by blast


[STATEMENT]
lemma finished_finite[simp, intro!]: "finite (dom (finished s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom (finished s))
[PROOF STEP]
using finished_discovered discovered_finite
[PROOF STATE]
proof (prove)
using this:
dom (finished s) \<subseteq> dom (discovered s)
finite (dom (discovered s))

goal (1 subgoal):
 1. finite (dom (finished s))
[PROOF STEP]
by (rule finite_subset)


[STATEMENT]
lemma finished_closed:
    "E `` dom (finished s) \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
using discovered_closed[unfolded discovered_closed_def]
[PROOF STATE]
proof (prove)
using this:
E `` dom (finished s) \<subseteq> dom (discovered s) \<and> (E - pending s) `` set (stack s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. E `` dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
by auto


[STATEMENT]
lemma finished_imp_succ_discovered:
    "v \<in> dom (finished s) \<Longrightarrow> w \<in> succ v \<Longrightarrow> w \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> dom (finished s); w \<in> E `` {v}\<rbrakk> \<Longrightarrow> w \<in> dom (discovered s)
[PROOF STEP]
using discovered_closed[unfolded discovered_closed_def]
[PROOF STATE]
proof (prove)
using this:
E `` dom (finished s) \<subseteq> dom (discovered s) \<and> (E - pending s) `` set (stack s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. \<lbrakk>v \<in> dom (finished s); w \<in> E `` {v}\<rbrakk> \<Longrightarrow> w \<in> dom (discovered s)
[PROOF STEP]
by auto


[STATEMENT]
lemma pending_reachable: "pending s \<subseteq> reachable \<times> reachable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pending s \<subseteq> reachable \<times> reachable
[PROOF STEP]
using pendingD discovered_reachable
[PROOF STATE]
proof (prove)
using this:
(?u, ?v) \<in> pending s \<Longrightarrow> (?u, ?v) \<in> E \<and> ?u \<in> dom (discovered s)
dom (discovered s) \<subseteq> reachable

goal (1 subgoal):
 1. pending s \<subseteq> reachable \<times> reachable
[PROOF STEP]
by (fast intro: rtrancl_image_advance_rtrancl)


[STATEMENT]
lemma pending_finite[simp, intro!]: "finite (pending s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (pending s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (pending s)
[PROOF STEP]
have "pending s \<subseteq> (SIGMA u:dom (discovered s). E``{u})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pending s \<subseteq> (SIGMA u:dom (discovered s). E `` {u})
[PROOF STEP]
by (auto dest: pendingD)
[PROOF STATE]
proof (state)
this:
pending s \<subseteq> (SIGMA u:dom (discovered s). E `` {u})

goal (1 subgoal):
 1. finite (pending s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pending s \<subseteq> (SIGMA u:dom (discovered s). E `` {u})

goal (1 subgoal):
 1. finite (pending s)
[PROOF STEP]
have "finite \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (SIGMA u:dom (discovered s). E `` {u})
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (dom (discovered s))
 2. \<And>u. u \<in> dom (discovered s) \<Longrightarrow> finite (E `` {u})
[PROOF STEP]
apply (rule discovered_finite)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u. u \<in> dom (discovered s) \<Longrightarrow> finite (E `` {u})
[PROOF STEP]
using discovered_reachable
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable

goal (1 subgoal):
 1. \<And>u. u \<in> dom (discovered s) \<Longrightarrow> finite (E `` {u})
[PROOF STEP]
by (blast intro: finitely_branching)
[PROOF STATE]
proof (state)
this:
finite (SIGMA u:dom (discovered s). E `` {u})

goal (1 subgoal):
 1. finite (pending s)
[PROOF STEP]
finally (finite_subset)
[PROOF STATE]
proof (chain)
picking this:
finite (pending s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (pending s)

goal (1 subgoal):
 1. finite (pending s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite (pending s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_pending_imp_succ_discovered:
    assumes "u \<in> dom (discovered s)"
    and "pending s `` {u} = {}"
    and "v \<in> succ u"
    shows "v \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> dom (discovered s)
[PROOF STEP]
proof (cases "u \<in> dom (finished s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
 2. u \<notin> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u \<in> dom (finished s)

goal (2 subgoals):
 1. u \<in> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
 2. u \<notin> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
with finished_imp_succ_discovered assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)
u \<in> dom (discovered s)
pending s `` {u} = {}
v \<in> E `` {u}
u \<in> dom (finished s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)
u \<in> dom (discovered s)
pending s `` {u} = {}
v \<in> E `` {u}
u \<in> dom (finished s)

goal (1 subgoal):
 1. v \<in> dom (discovered s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> dom (discovered s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<notin> dom (finished s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
with stack_set_def assms
[PROOF STATE]
proof (chain)
picking this:
set (stack s) = dom (discovered s) - dom (finished s)
u \<in> dom (discovered s)
pending s `` {u} = {}
v \<in> E `` {u}
u \<notin> dom (finished s)
[PROOF STEP]
have "u \<in> set (stack s)"
[PROOF STATE]
proof (prove)
using this:
set (stack s) = dom (discovered s) - dom (finished s)
u \<in> dom (discovered s)
pending s `` {u} = {}
v \<in> E `` {u}
u \<notin> dom (finished s)

goal (1 subgoal):
 1. u \<in> set (stack s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> set (stack s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
with assms discovered_closed[unfolded discovered_closed_def]
[PROOF STATE]
proof (chain)
picking this:
u \<in> dom (discovered s)
pending s `` {u} = {}
v \<in> E `` {u}
E `` dom (finished s) \<subseteq> dom (discovered s) \<and> (E - pending s) `` set (stack s) \<subseteq> dom (discovered s)
u \<in> set (stack s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> dom (discovered s)
pending s `` {u} = {}
v \<in> E `` {u}
E `` dom (finished s) \<subseteq> dom (discovered s) \<and> (E - pending s) `` set (stack s) \<subseteq> dom (discovered s)
u \<in> set (stack s)

goal (1 subgoal):
 1. v \<in> dom (discovered s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> dom (discovered s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nc_finished_eq_reachable:
    assumes NC: "\<not>cond s" "\<not>is_break param s"
    shows "dom (finished s) = reachable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (finished s) = reachable
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom (finished s) = reachable
[PROOF STEP]
from NC basic_invar
[PROOF STATE]
proof (chain)
picking this:
\<not> cond s
\<not> is_break param s
basic_invar s
[PROOF STEP]
have [simp]: "stack s = []" "dom (discovered s) = dom (finished s)" and SS: "V0 \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
\<not> cond s
\<not> is_break param s
basic_invar s

goal (1 subgoal):
 1. (stack s = [] &&& dom (discovered s) = dom (finished s)) &&& V0 \<subseteq> dom (discovered s)
[PROOF STEP]
unfolding basic_invar_def cond_alt
[PROOF STATE]
proof (prove)
using this:
\<not> ((V0 \<subseteq> dom (discovered s) \<longrightarrow> stack s \<noteq> []) \<and> \<not> is_break param s)
\<not> is_break param s
set (stack s) = dom (discovered s) - dom (finished s) \<and> distinct (stack s) \<and> (stack s \<noteq> [] \<longrightarrow> last (stack s) \<in> V0) \<and> dom (finished s) \<subseteq> dom (discovered s) \<and> Domain (pending s) \<subseteq> dom (discovered s) - dom (finished s) \<and> pending s \<subseteq> E

goal (1 subgoal):
 1. (stack s = [] &&& dom (discovered s) = dom (finished s)) &&& V0 \<subseteq> dom (discovered s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stack s = []
dom (discovered s) = dom (finished s)
V0 \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. dom (finished s) = reachable
[PROOF STEP]
show "dom (finished s) = reachable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (finished s) = reachable
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dom (finished s) \<subseteq> reachable
 2. reachable \<subseteq> dom (finished s)
[PROOF STEP]
from discovered_reachable
[PROOF STATE]
proof (chain)
picking this:
dom (discovered s) \<subseteq> reachable
[PROOF STEP]
show "dom (finished s) \<subseteq> reachable"
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable

goal (1 subgoal):
 1. dom (finished s) \<subseteq> reachable
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (finished s) \<subseteq> reachable

goal (1 subgoal):
 1. reachable \<subseteq> dom (finished s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable \<subseteq> dom (finished s)
[PROOF STEP]
from discovered_closed
[PROOF STATE]
proof (chain)
picking this:
discovered_closed s
[PROOF STEP]
have "E``(dom (finished s)) \<subseteq> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
discovered_closed s

goal (1 subgoal):
 1. E `` dom (finished s) \<subseteq> dom (finished s)
[PROOF STEP]
unfolding discovered_closed_def
[PROOF STATE]
proof (prove)
using this:
E `` dom (finished s) \<subseteq> dom (discovered s) \<and> (E - pending s) `` set (stack s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. E `` dom (finished s) \<subseteq> dom (finished s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E `` dom (finished s) \<subseteq> dom (finished s)

goal (1 subgoal):
 1. reachable \<subseteq> dom (finished s)
[PROOF STEP]
with SS
[PROOF STATE]
proof (chain)
picking this:
V0 \<subseteq> dom (discovered s)
E `` dom (finished s) \<subseteq> dom (finished s)
[PROOF STEP]
show "reachable \<subseteq> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> dom (discovered s)
E `` dom (finished s) \<subseteq> dom (finished s)

goal (1 subgoal):
 1. reachable \<subseteq> dom (finished s)
[PROOF STEP]
by (simp, metis rtrancl_reachable_induct)
[PROOF STATE]
proof (state)
this:
reachable \<subseteq> dom (finished s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dom (finished s) = reachable

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nc_V0_finished:
    assumes NC: "\<not> cond s" "\<not> is_break param s"
    shows "V0 \<subseteq> dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V0 \<subseteq> dom (finished s)
[PROOF STEP]
using nc_finished_eq_reachable[OF NC]
[PROOF STATE]
proof (prove)
using this:
dom (finished s) = reachable

goal (1 subgoal):
 1. V0 \<subseteq> dom (finished s)
[PROOF STEP]
by blast


[STATEMENT]
lemma nc_discovered_eq_finished:
    assumes NC: "\<not> cond s" "\<not> is_break param s"
    shows "dom (discovered s) = dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (discovered s) = dom (finished s)
[PROOF STEP]
using finished_discovered
[PROOF STATE]
proof (prove)
using this:
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. dom (discovered s) = dom (finished s)
[PROOF STEP]
using nc_finished_eq_reachable[OF NC] discovered_reachable
[PROOF STATE]
proof (prove)
using this:
dom (finished s) \<subseteq> dom (discovered s)
dom (finished s) = reachable
dom (discovered s) \<subseteq> reachable

goal (1 subgoal):
 1. dom (discovered s) = dom (finished s)
[PROOF STEP]
by blast


[STATEMENT]
lemma nc_discovered_eq_reachable:
    assumes NC: "\<not> cond s" "\<not> is_break param s"
    shows "dom (discovered s) = reachable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (discovered s) = reachable
[PROOF STEP]
using NC
[PROOF STATE]
proof (prove)
using this:
\<not> cond s
\<not> is_break param s

goal (1 subgoal):
 1. dom (discovered s) = reachable
[PROOF STEP]
using nc_discovered_eq_finished nc_finished_eq_reachable
[PROOF STATE]
proof (prove)
using this:
\<not> cond s
\<not> is_break param s
\<lbrakk>\<not> cond s; \<not> is_break param s\<rbrakk> \<Longrightarrow> dom (discovered s) = dom (finished s)
\<lbrakk>\<not> cond s; \<not> is_break param s\<rbrakk> \<Longrightarrow> dom (finished s) = reachable

goal (1 subgoal):
 1. dom (discovered s) = reachable
[PROOF STEP]
by blast


[STATEMENT]
lemma nc_fin_closed:
    assumes NC: "\<not>cond s"
    assumes NB: "\<not>is_break param s"
    shows "E``dom (finished s) \<subseteq> dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` dom (finished s) \<subseteq> dom (finished s)
[PROOF STEP]
using finished_imp_succ_discovered
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)

goal (1 subgoal):
 1. E `` dom (finished s) \<subseteq> dom (finished s)
[PROOF STEP]
by (auto simp: nc_discovered_eq_finished[OF NC NB])


[STATEMENT]
lemma param_dfs_variant_wf[simp, intro!]:
    assumes [simp, intro!]: "finite reachable"
    shows "wf param_dfs_variant"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf param_dfs_variant
[PROOF STEP]
unfolding param_dfs_variant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s))))
[PROOF STEP]
by auto