[STATEMENT]
lemma establish_invarI'[case_names init new_root finish cross_edge back_edge discover]:
    \<comment> \<open>Establish a DFS invariant (symbolic preconditions).\<close>
    assumes init: "on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))"
    assumes new_root: "\<And>s' v0. pre_on_new_root v0 s'
         \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n
             SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                         \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes finish: "\<And>s' u. pre_on_finish u s'
         \<Longrightarrow> on_finish param u s' \<le>\<^sub>n
              SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes cross_edge: "\<And>s' u v. pre_on_cross_edge u v s'
       \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes back_edge: "\<And>s' u v. pre_on_back_edge u v s'
       \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes discover: "\<And>s' u v. pre_on_discover u v s'
       \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    shows "is_invar I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I
[PROOF STEP]
apply (rule establish_invarI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
pre_on_new_root ?v0.1 ?s'1 \<Longrightarrow> on_new_root param ?v0.1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
pre_on_finish ?u1 ?s'1 \<Longrightarrow> on_finish param ?u1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
pre_on_cross_edge ?u1 ?v1 ?s'1 \<Longrightarrow> on_cross_edge param ?u1 ?v1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
pre_on_back_edge ?u1 ?v1 ?s'1 \<Longrightarrow> on_back_edge param ?u1 ?v1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
pre_on_discover ?u1 ?v1 ?s'1 \<Longrightarrow> on_discover param ?u1 ?v1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))

goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
unfolding pre_on_defs
[PROOF STATE]
proof (prove)
using this:
on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
\<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> ?v0.1 \<in> V0 \<and> ?v0.1 \<notin> dom (discovered s) \<and> ?s'1 = new_root ?v0.1 s \<Longrightarrow> on_new_root param ?v0.1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
\<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> ?u1 = hd (stack s) \<and> pending s `` {?u1} = {} \<and> ?s'1 = finish ?u1 s \<Longrightarrow> on_finish param ?u1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
\<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> ?u1 = hd (stack s) \<and> (?u1, ?v1) \<in> pending s) \<and> ?v1 \<in> dom (discovered s) \<and> ?v1 \<in> dom (finished s) \<and> ?s'1 = cross_edge ?u1 ?v1 (s\<lparr>pending := pending s - {(?u1, ?v1)}\<rparr>) \<Longrightarrow> on_cross_edge param ?u1 ?v1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
\<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> ?u1 = hd (stack s) \<and> (?u1, ?v1) \<in> pending s) \<and> ?v1 \<in> dom (discovered s) \<and> ?v1 \<notin> dom (finished s) \<and> ?s'1 = back_edge ?u1 ?v1 (s\<lparr>pending := pending s - {(?u1, ?v1)}\<rparr>) \<Longrightarrow> on_back_edge param ?u1 ?v1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))
\<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> ?u1 = hd (stack s) \<and> (?u1, ?v1) \<in> pending s) \<and> ?v1 \<notin> dom (discovered s) \<and> ?s'1 = discover ?u1 ?v1 (s\<lparr>pending := pending s - {(?u1, ?v1)}\<rparr>) \<Longrightarrow> on_discover param ?u1 ?v1 ?s'1 \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (?s'1\<lparr>state.more := x\<rparr>) \<longrightarrow> I (?s'1\<lparr>state.more := x\<rparr>))

goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s; on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s; on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>); on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>); on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>); on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s; on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 2. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s; on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>); on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>); on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>); on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x)); \<And>v0 s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s = [] \<and> v0 \<in> V0 \<and> v0 \<notin> dom (discovered s) \<and> s' = new_root v0 s \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u s'. \<exists>s. DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> pending s `` {u} = {} \<and> s' = finish u s \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<in> dom (finished s) \<and> s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<in> dom (discovered s) \<and> v \<notin> dom (finished s) \<and> s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>)); \<And>u v s'. \<exists>s. (DFS_invar G param s \<and> cond s \<and> stack s \<noteq> [] \<and> u = hd (stack s) \<and> (u, v) \<in> pending s) \<and> v \<notin> dom (discovered s) \<and> s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>) \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
apply (rprems,blast)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma establish_invarI_ND [case_names prereq init new_discover finish cross_edge back_edge]:
    \<comment> \<open>Establish a DFS invariant (new-root and discover cases are combined).\<close>
    assumes prereq: "\<And>u v s. on_discover param u v s = on_new_root param v s"
    assumes init: "on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))"
    assumes new_discover: "\<And>s s' v.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       v \<notin> dom (discovered s);
       discovered s' = (discovered s)(v\<mapsto>counter s); finished s' = finished s;
       counter s' = Suc (counter s); stack s' = v#stack s;
       back_edges s' = back_edges s; cross_edges s' = cross_edges s;
       tree_edges s' \<supseteq> tree_edges s;
       state.more s' = state.more s\<rbrakk>
         \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n
             SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                         \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes finish: "\<And>s s' u.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       stack s \<noteq> []; u = hd (stack s);
       pending s `` {u} = {};
       s' = finish u s\<rbrakk>
         \<Longrightarrow> on_finish param u s' \<le>\<^sub>n
              SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes cross_edge: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s);
        v \<in> dom (discovered s); v\<in>dom (finished s);
        s' = cross_edge u v (s\<lparr>pending := pending s - {(u,v)}\<rparr>)\<rbrakk>
       \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes back_edge: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s);
        v \<in> dom (discovered s); v\<notin>dom (finished s);
        s' = back_edge u v (s\<lparr>pending := pending s - {(u,v)}\<rparr>)\<rbrakk>
       \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    shows "is_invar I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I
[PROOF STEP]
proof (induct rule: establish_invarI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
case (new_root s)
[PROOF STATE]
proof (state)
this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s = []
v0_ \<in> V0
v0_ \<notin> dom (discovered s)
s'_ = new_root v0_ s

goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s = []
v0_ \<in> V0
v0_ \<notin> dom (discovered s)
s'_ = new_root v0_ s

goal (1 subgoal):
 1. on_new_root param v0_ s'_ \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'_\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'_\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by (auto intro!: new_discover)
[PROOF STATE]
proof (state)
this:
on_new_root param v0_ s'_ \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'_\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'_\<lparr>state.more := x\<rparr>))

goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s \<noteq> []
(u, v) \<in> pending s
u = hd (stack s)
v \<notin> dom (discovered s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)

goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
hence
      "on_new_root param v s' \<le>\<^sub>n
        SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                   \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s \<noteq> []
(u, v) \<in> pending s
u = hd (stack s)
v \<notin> dom (discovered s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)

goal (1 subgoal):
 1. on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by (auto intro!: new_discover)
[PROOF STATE]
proof (state)
this:
on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
with prereq
[PROOF STATE]
proof (chain)
picking this:
on_discover param ?u1 ?v1 ?s1 = on_new_root param ?v1 ?s1
on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
on_discover param ?u1 ?v1 ?s1 = on_new_root param ?v1 ?s1
on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (1 subgoal):
 1. on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (4 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
qed fact+


[STATEMENT]
lemma establish_invarI_CB [case_names prereq init new_root finish cross_back_edge discover]:
    \<comment> \<open>Establish a DFS invariant (cross and back edge cases are combined).\<close>
    assumes prereq: "\<And>u v s. on_back_edge param u v s = on_cross_edge param u v s"
    assumes init: "on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))"
    assumes new_root: "\<And>s s' v0.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s);
        s' = new_root v0 s\<rbrakk>
         \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n
             SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                         \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes finish: "\<And>s s' u.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       stack s \<noteq> []; u = hd (stack s);
       pending s `` {u} = {};
       s' = finish u s\<rbrakk>
         \<Longrightarrow> on_finish param u s' \<le>\<^sub>n
              SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes cross_back_edge: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s);
        v \<in> dom (discovered s);
        discovered s' = discovered s; finished s' = finished s;
        stack s' = stack s; tree_edges s' = tree_edges s; counter s' = counter s;
        pending s' = pending s - {(u,v)};
        cross_edges s' \<union> back_edges s' = cross_edges s \<union> back_edges s \<union> {(u,v)};
        state.more s' = state.more s \<rbrakk>
       \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes discover: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> [];  (u, v) \<in> pending s; u = hd (stack s);
        v \<notin> dom (discovered s);
        s' = discover u v (s\<lparr>pending := pending s - {(u,v)}\<rparr>)\<rbrakk>
       \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    shows "is_invar I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I
[PROOF STEP]
proof (induct rule: establish_invarI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
case cross_edge
[PROOF STATE]
proof (state)
this:
DFS_invar G param s_
I s_
cond s_
\<not> is_break param s_
stack s_ \<noteq> []
(u_, v_) \<in> pending s_
u_ = hd (stack s_)
v_ \<in> dom (discovered s_)
v_ \<in> dom (finished s_)
s'_ = cross_edge u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)

goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s_
I s_
cond s_
\<not> is_break param s_
stack s_ \<noteq> []
(u_, v_) \<in> pending s_
u_ = hd (stack s_)
v_ \<in> dom (discovered s_)
v_ \<in> dom (finished s_)
s'_ = cross_edge u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)

goal (1 subgoal):
 1. on_cross_edge param u_ v_ s'_ \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'_\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'_\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by (auto intro!: cross_back_edge)
[PROOF STATE]
proof (state)
this:
on_cross_edge param u_ v_ s'_ \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'_\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'_\<lparr>state.more := x\<rparr>))

goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
case (back_edge s s' u v)
[PROOF STATE]
proof (state)
this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s \<noteq> []
(u, v) \<in> pending s
u = hd (stack s)
v \<in> dom (discovered s)
v \<notin> dom (finished s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)

goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
hence
      "on_cross_edge param u v s' \<le>\<^sub>n
             SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                         \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s \<noteq> []
(u, v) \<in> pending s
u = hd (stack s)
v \<in> dom (discovered s)
v \<notin> dom (finished s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)

goal (1 subgoal):
 1. on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by (auto intro!: cross_back_edge)
[PROOF STATE]
proof (state)
this:
on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (5 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
with prereq
[PROOF STATE]
proof (chain)
picking this:
on_back_edge param ?u1 ?v1 ?s1 = on_cross_edge param ?u1 ?v1 ?s1
on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
on_back_edge param ?u1 ?v1 ?s1 = on_cross_edge param ?u1 ?v1 ?s1
on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (1 subgoal):
 1. on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (4 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
qed fact+


[STATEMENT]
lemma establish_invarI_ND_CB [case_names prereq_ND prereq_CB init new_discover finish cross_back_edge]:
    \<comment> \<open>Establish a DFS invariant (new-root/discover and cross/back-edge cases are combined).\<close>
    assumes prereq:
        "\<And>u v s. on_discover param u v s = on_new_root param v s"
        "\<And>u v s. on_back_edge param u v s = on_cross_edge param u v s"
    assumes init: "on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))"
    assumes new_discover: "\<And>s s' v.
     \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
      v \<notin> dom (discovered s);
      discovered s' = (discovered s)(v\<mapsto>counter s); finished s' = finished s;
      counter s' = Suc (counter s); stack s' = v#stack s;
      back_edges s' = back_edges s; cross_edges s' = cross_edges s;
      tree_edges s' \<supseteq> tree_edges s;
      state.more s' = state.more s\<rbrakk>
        \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n
            SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes finish: "\<And>s s' u.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       stack s \<noteq> []; u = hd (stack s);
       pending s `` {u} = {};
       s' = finish u s\<rbrakk>
         \<Longrightarrow> on_finish param u s' \<le>\<^sub>n
              SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes cross_back_edge: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s);
        v \<in> dom (discovered s);
        discovered s' = discovered s; finished s' = finished s;
        stack s' = stack s; tree_edges s' = tree_edges s; counter s' = counter s;
        pending s' = pending s - {(u,v)};
        cross_edges s' \<union> back_edges s' = cross_edges s \<union> back_edges s \<union> {(u,v)};
        state.more s' = state.more s \<rbrakk>
       \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    shows "is_invar I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I
[PROOF STEP]
proof (induct rule: establish_invarI_ND)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
case cross_edge
[PROOF STATE]
proof (state)
this:
DFS_invar G param s_
I s_
cond s_
\<not> is_break param s_
stack s_ \<noteq> []
(u_, v_) \<in> pending s_
u_ = hd (stack s_)
v_ \<in> dom (discovered s_)
v_ \<in> dom (finished s_)
s'_ = cross_edge u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)

goal (6 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s_
I s_
cond s_
\<not> is_break param s_
stack s_ \<noteq> []
(u_, v_) \<in> pending s_
u_ = hd (stack s_)
v_ \<in> dom (discovered s_)
v_ \<in> dom (finished s_)
s'_ = cross_edge u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)

goal (1 subgoal):
 1. on_cross_edge param u_ v_ s'_ \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'_\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'_\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by (auto intro!: cross_back_edge)
[PROOF STATE]
proof (state)
this:
on_cross_edge param u_ v_ s'_ \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'_\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'_\<lparr>state.more := x\<rparr>))

goal (5 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
case (back_edge s s' u v)
[PROOF STATE]
proof (state)
this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s \<noteq> []
(u, v) \<in> pending s
u = hd (stack s)
v \<in> dom (discovered s)
v \<notin> dom (finished s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)

goal (5 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
hence
      "on_cross_edge param u v s' \<le>\<^sub>n
             SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                         \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s
I s
cond s
\<not> is_break param s
stack s \<noteq> []
(u, v) \<in> pending s
u = hd (stack s)
v \<in> dom (discovered s)
v \<notin> dom (finished s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)

goal (1 subgoal):
 1. on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by (auto intro!: cross_back_edge)
[PROOF STATE]
proof (state)
this:
on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (5 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
with prereq
[PROOF STATE]
proof (chain)
picking this:
on_discover param ?u1 ?v1 ?s1 = on_new_root param ?v1 ?s1
on_back_edge param ?u1 ?v1 ?s1 = on_cross_edge param ?u1 ?v1 ?s1
on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
on_discover param ?u1 ?v1 ?s1 = on_new_root param ?v1 ?s1
on_back_edge param ?u1 ?v1 ?s1 = on_cross_edge param ?u1 ?v1 ?s1
on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (1 subgoal):
 1. on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))

goal (4 subgoals):
 1. \<And>u v s. on_discover param u v s = on_new_root param v s
 2. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 3. \<And>s s' v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; v \<notin> dom (discovered s); discovered s' = discovered s(v \<mapsto> counter s); finished s' = finished s; counter s' = Suc (counter s); stack s' = v # stack s; back_edges s' = back_edges s; cross_edges s' = cross_edges s; tree_edges s \<subseteq> tree_edges s'; state.more s' = state.more s\<rbrakk> \<Longrightarrow> on_new_root param v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
qed fact+


[STATEMENT]
lemma is_invarI_full [case_names init new_root finish cross_edge back_edge discover]:
    \<comment> \<open>Establish a DFS invariant not taking into account the parameterization.\<close>
    assumes init: "\<And>e. I (empty_state e)"
    assumes 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 cross_edge: "\<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'"
    and back_edge: "\<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'"
    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]
apply (rule establish_invarI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))
 2. \<And>s s' v0. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s); s' = new_root v0 s\<rbrakk> \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 3. \<And>s s' u. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; u = hd (stack s); pending s `` {u} = {}; s' = finish u s\<rbrakk> \<Longrightarrow> on_finish param u s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 4. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<in> dom (finished s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 5. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<in> dom (discovered s); v \<notin> dom (finished s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
 6. \<And>s s' u v. \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s; stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s); v \<notin> dom (discovered s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<rbrakk> \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>) \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))
[PROOF STEP]
apply (blast intro: indep_invar_rules assms)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done