Theory Nested_DFS
section ‹Nested DFS›
theory Nested_DFS
imports DFS_Find_Path
begin
text ‹Nested DFS is a standard method for Buchi-Automaton emptiness check.›
subsection ‹Auxiliary Lemmas›
lemma closed_restrict_aux:
assumes CL: "E``F ⊆ F ∪ S"
assumes NR: "E⇧*``U ∩ S = {}"
assumes SS: "U ⊆ F"
shows "E⇧*``U ⊆ F"
proof clarify
fix u v
assume A: "(u,v)∈E⇧*" "u∈U"
hence M: "E⇧*``{u} ∩ S = {}" "u∈F" using NR SS by blast+
from A(1) M show "v∈F"
apply (induct rule: converse_rtrancl_induct)
using CL apply (auto dest: rtrancl_Image_advance_ss)
done
qed
subsection ‹Instantiation of the Framework›
record 'v blue_dfs_state = "'v state" +
lasso :: "('v list × 'v list) option"
red :: "'v set"
type_synonym 'v blue_dfs_param = "('v, ('v,unit) blue_dfs_state_ext) parameterization"
lemma lasso_more_cong[cong]:"state.more s = state.more s' ⟹ lasso s = lasso s'"
by (cases s, cases s') simp
lemma red_more_cong[cong]: "state.more s = state.more s' ⟹ red s = red s'"
by (cases s, cases s') simp
lemma [simp]: "s⦇ state.more := ⦇ lasso = foo, red = bar ⦈ ⦈ = s ⦇ lasso := foo, red := bar ⦈"
by (cases s) simp
abbreviation "dropWhileNot v ≡ dropWhile ((≠) v)"
abbreviation "takeWhileNot v ≡ takeWhile ((≠) v)"
locale BlueDFS_defs = graph_defs G
for G :: "('v, 'more) graph_rec_scheme" +
fixes accpt :: "'v ⇒ bool"
begin
definition "blue s ≡ dom (finished s) - red s"
definition "cyan s ≡ set (stack s)"
definition "white s ≡ - dom (discovered s)"
abbreviation "red_dfs R ss x ≡ find_path1_restr_spec (G ⦇ g_V0 := {x} ⦈) ss R"
definition mk_blue_witness
:: "'v blue_dfs_state ⇒ 'v fpr_result ⇒ ('v,unit) blue_dfs_state_ext"
where
"mk_blue_witness s redS ≡ case redS of
Inl R' ⇒ ⦇ lasso = None, red = (R' ) ⦈
| Inr (vs, v) ⇒ let rs = rev (stack s) in
⦇ lasso = Some (rs, vs@dropWhileNot v rs), red = red s⦈"
definition run_red_dfs
:: "'v ⇒ 'v blue_dfs_state ⇒ ('v,unit) blue_dfs_state_ext nres"
where
"run_red_dfs u s ≡ case lasso s of None ⇒ do {
redS ← red_dfs (red s) (λx. x = u ∨ x ∈ cyan s) u;
RETURN (mk_blue_witness s redS)
}
| _ ⇒ NOOP s"
text ‹ Schwoon-Esparza extension ›
definition "se_back_edge u v s ≡ case lasso s of
None ⇒
if accpt u then
let rs = rev (tl (stack s));
ur = rs;
ul = u#dropWhileNot v rs
in RETURN ⦇lasso = Some (ur,ul), red = red s⦈
else if accpt v then
let rs = rev (stack s);
vr = takeWhileNot v rs;
vl = dropWhileNot v rs
in RETURN ⦇lasso = Some (vr,vl), red = red s⦈
else NOOP s
| _ ⇒ NOOP s"
definition blue_dfs_params :: "'v blue_dfs_param"
where "blue_dfs_params = ⦇
on_init = RETURN ⦇ lasso = None, red = {} ⦈,
on_new_root = λv0 s. NOOP s,
on_discover = λu v s. NOOP s,
on_finish = λu s. if accpt u then run_red_dfs u s else NOOP s,
on_back_edge = se_back_edge,
on_cross_edge = λu v s. NOOP s,
is_break = λs. lasso s ≠ None ⦈"
schematic_goal blue_dfs_params_simps[simp]:
"on_init blue_dfs_params = ?OI"
"on_new_root blue_dfs_params = ?ONR"
"on_discover blue_dfs_params = ?OD"
"on_finish blue_dfs_params = ?OF"
"on_back_edge blue_dfs_params = ?OBE"
"on_cross_edge blue_dfs_params = ?OCE"
"is_break blue_dfs_params = ?IB"
unfolding blue_dfs_params_def gen_parameterization.simps
by (rule refl)+
sublocale param_DFS_defs G blue_dfs_params
by unfold_locales
end
locale BlueDFS = BlueDFS_defs G accpt + param_DFS G blue_dfs_params
for G :: "('v, 'more) graph_rec_scheme" and accpt :: "'v ⇒ bool"
lemma BlueDFSI:
assumes "fb_graph G"
shows "BlueDFS G"
proof -
interpret fb_graph G by fact
show ?thesis by unfold_locales
qed
locale BlueDFS_invar = BlueDFS +
DFS_invar where param = blue_dfs_params
context BlueDFS_defs begin
lemma BlueDFS_invar_eq[simp]:
shows "DFS_invar G blue_dfs_params s ⟷ BlueDFS_invar G accpt s"
proof
assume "DFS_invar G blue_dfs_params s"
interpret DFS_invar G blue_dfs_params s by fact
show "BlueDFS_invar G accpt s" by unfold_locales
next
assume "BlueDFS_invar G accpt s"
then interpret BlueDFS_invar G accpt s .
show "DFS_invar G blue_dfs_params s" by unfold_locales
qed
end
subsection ‹Correctness Proof›
context BlueDFS begin
definition "blue_basic_invar s ≡
case lasso s of
None ⇒ restr_invar E (red s) (λx. x∈set (stack s))
∧ red s ⊆ dom (finished s)
| Some l ⇒ True"
lemma (in BlueDFS_invar) red_DFS_precond_aux:
assumes BI: "blue_basic_invar s"
assumes [simp]: "lasso s = None"
assumes SNE: "stack s ≠ []"
shows
"fb_graph (G ⦇ g_V0 := {hd (stack s)} ⦈)"
and "fb_graph (G ⦇ g_E := E ∩ UNIV × - red s, g_V0 := {hd (stack s)} ⦈)"
and "restr_invar E (red s) (λx. x ∈ set (stack s))"
using stack_reachable ‹stack s ≠ []›
apply (rule_tac fb_graph_subset, auto) []
using stack_reachable ‹stack s ≠ []›
apply (rule_tac fb_graph_subset, auto) []
using BI apply (simp add: blue_basic_invar_def)
done
lemma (in BlueDFS_invar) red_dfs_pres_bbi:
assumes BI: "blue_basic_invar s"
assumes [simp]: "lasso s = None" and SNE: "stack s ≠ []"
assumes "pending s `` {hd (stack s)} = {}"
shows "run_red_dfs (hd (stack s)) (finish (hd (stack s)) s) ≤⇩n
SPEC (λe.
DFS_invar G blue_dfs_params (finish (hd (stack s)) s⦇state.more := e⦈)
⟶ blue_basic_invar (finish (hd (stack s)) s⦇state.more := e⦈))"
proof -
have [simp]: "(λx. x = hd (stack s) ∨ x ∈ cyan (finish (hd (stack s)) s)) =
(λx. x∈set (stack s))"
using ‹stack s ≠ []›
unfolding finish_def cyan_def by (auto simp: neq_Nil_conv)
show ?thesis
unfolding run_red_dfs_def
apply simp
apply (refine_vcg)
apply simp
proof -
fix fp1
define s' where "s' = finish (hd (stack s)) s"
assume FP_spec:
"find_path1_restr_pred (G ⦇ g_V0 := {hd (stack s)} ⦈) (λx. x ∈ set (stack s)) (red s) fp1"
assume "BlueDFS_invar G accpt (s'⦇state.more := mk_blue_witness s' fp1⦈)"
then interpret i: BlueDFS_invar G accpt "(s'⦇state.more := mk_blue_witness s' fp1⦈)"
by simp
have [simp]:
"red s' = red s"
"discovered s' = discovered s"
"dom (finished s') = insert (hd (stack s)) (dom (finished s))"
unfolding s'_def finish_def by auto
{
fix R'
assume [simp]: "fp1 = Inl R'"
from FP_spec[unfolded find_path1_restr_pred_def, simplified]
have
R'FMT: "R' = red s ∪ E⇧+ `` {hd (stack s)}"
and RI: "restr_invar E R' (λx. x ∈ set (stack s))"
by auto
from BI have "red s ⊆ dom (finished s)"
unfolding blue_basic_invar_def by auto
also have "E⇧+ `` {hd (stack s)} ⊆ dom (finished s)"
proof (intro subsetI, elim ImageE, simp)
fix v
assume "(hd (stack s),v)∈E⇧+"
then obtain u where "(hd (stack s),u)∈E" and "(u,v)∈E⇧*"
by (auto simp: trancl_unfold_left)
from RI have NR: "E⇧+ `` {hd (stack s)} ∩ set (stack s) = {}"
unfolding restr_invar_def by (auto simp: R'FMT)
with ‹(hd (stack s),u)∈E› have "u∉set (stack s)" by auto
with i.finished_closed[simplified] ‹(hd (stack s),u)∈E›
have UID: "u∈dom (finished s)" by (auto simp: stack_set_def)
from NR ‹(hd (stack s),u)∈E› have NR': "E⇧*``{u} ∩ set (stack s) = {}"
by (auto simp: trancl_unfold_left)
have CL: "E `` dom (finished s) ⊆ dom (finished s) ∪ set (stack s)"
using finished_closed discovered_eq_finished_un_stack
by simp
from closed_restrict_aux[OF CL NR'] UID
have "E⇧* `` {u} ⊆ dom (finished s)" by simp
with ‹(u,v)∈E⇧*› show "v ∈ dom (finished s)" by auto
qed
finally (sup_least)
have "R' ⊆ dom (finished s) ∧ red s ⊆ dom (finished s)"
by (simp add: R'FMT)
} note aux1 = this
show "blue_basic_invar (s'⦇state.more := mk_blue_witness s' fp1⦈)"
unfolding blue_basic_invar_def mk_blue_witness_def
apply (simp split: option.splits sum.splits)
apply (intro allI conjI impI)
using FP_spec SNE
apply (auto
simp: s'_def blue_basic_invar_def find_path1_restr_pred_def
simp: restr_invar_def
simp: neq_Nil_conv) []
apply (auto dest!: aux1) []
done
qed
qed
lemma blue_basic_invar: "is_invar blue_basic_invar"
proof (induct rule: establish_invarI)
case (finish s) then interpret BlueDFS_invar where s=s by simp
have [simp]: "(λx. x = hd (stack s) ∨ x ∈ cyan (finish (hd (stack s)) s)) =
(λx. x∈set (stack s))"
using ‹stack s ≠ []›
unfolding finish_def cyan_def by (auto simp: neq_Nil_conv)
from finish show ?case
apply (simp)
apply (intro conjI impI)
apply (rule leof_trans[OF red_dfs_pres_bbi], assumption+, simp)
apply (auto simp: restr_invar_def blue_basic_invar_def neq_Nil_conv) []
done
qed (auto simp: blue_basic_invar_def cond_def se_back_edge_def
simp: restr_invar_def empty_state_def pred_defs
simp: DFS_invar.discovered_eq_finished_un_stack
simp del: BlueDFS_invar_eq
split: option.splits)
lemmas (in BlueDFS_invar) s_blue_basic_invar
= blue_basic_invar[THEN make_invar_thm]
lemmas (in BlueDFS_invar) red_DFS_precond
= red_DFS_precond_aux[OF s_blue_basic_invar]
sublocale DFS G blue_dfs_params
apply unfold_locales
apply (clarsimp_all
simp: se_back_edge_def run_red_dfs_def refine_pw_simps pre_on_defs
split: option.splits)
unfolding nofail_SPEC_iff
apply (refine_vcg)
apply (erule BlueDFS_invar.red_DFS_precond, auto) []
apply (simp add: cyan_def finish_def)
apply (erule BlueDFS_invar.red_DFS_precond, auto) []
apply (rule TrueI)
done
end
context BlueDFS_invar
begin
context assumes [simp]: "lasso s = None"
begin
lemma red_closed:
"E `` red s ⊆ red s"
using s_blue_basic_invar
unfolding blue_basic_invar_def restr_invar_def
by simp
lemma red_stack_disjoint:
"set (stack s) ∩ red s = {}"
using s_blue_basic_invar
unfolding blue_basic_invar_def restr_invar_def
by auto
lemma red_finished: "red s ⊆ dom (finished s)"
using s_blue_basic_invar
unfolding blue_basic_invar_def
by auto
lemma all_nodes_colored: "white s ∪ blue s ∪ cyan s ∪ red s = UNIV "
unfolding white_def blue_def cyan_def
by (auto simp: stack_set_def)
lemma colors_disjoint:
"white s ∩ (blue s ∪ cyan s ∪ red s) = {}"
"blue s ∩ (white s ∪ cyan s ∪ red s) = {}"
"cyan s ∩ (white s ∪ blue s ∪ red s) = {}"
"red s ∩ (white s ∪ blue s ∪ cyan s) = {}"
unfolding white_def blue_def cyan_def
using finished_discovered red_finished
unfolding stack_set_def
by blast+
end
lemma (in BlueDFS) i_no_accpt_cyle_in_finish:
"is_invar (λs. lasso s = None ⟶ (∀x. accpt x ∧ x ∈ dom (finished s) ⟶ (x,x) ∉ E⇧+))"
proof (induct rule: establish_invarI)
case (finish s s' u) then interpret BlueDFS_invar where s=s by simp
let ?onstack = "λx. x∈set (stack s)"
let ?rE = "rel_restrict E (red s)"
from finish obtain sh st where [simp]: "stack s = sh#st"
by (auto simp: neq_Nil_conv)
have 1: "g_E (G ⦇ g_V0 := {hd (stack s)} ⦈) = E" by simp
{
fix R'::"'v set"
let ?R' = "R' "
let ?s = "s'⦇ lasso := None, red := ?R'⦈"
assume "⋀v. (hd (stack s), v) ∈ ?rE⇧+ ⟹ ¬ ?onstack v"
and accpt: "accpt u"
and NL[simp]: "lasso s = None"
hence no_hd_cycle: "(hd (stack s), hd (stack s)) ∉ ?rE⇧+"
by auto
from finish have "stack s ≠ []" by simp
from hd_in_set[OF this] have "hd (stack s) ∉ red s"
using red_stack_disjoint
by auto
hence "(hd (stack s),hd (stack s)) ∉ E⇧+"
using no_hd_cycle rel_restrict_tranclI red_closed[OF NL]
by metis
with accpt finish have
"∀x. accpt x ∧ x ∈ dom (finished ?s) ⟶ (x,x) ∉ E⇧+"
by auto
} with finish have
"red_dfs (red s) ?onstack (hd (stack s))
≤ SPEC (λx. ∀R. x = Inl R ⟶
DFS_invar G blue_dfs_params (lasso_update Map.empty s'⦇red := R ⦈) ⟶
(∀x. accpt x ∧ x∈dom (finished s') ⟶ (x, x) ∉ E⇧+))"
apply -
apply (rule find_path1_restr_spec_rule, intro conjI)
apply (rule red_DFS_precond, simp_all) []
unfolding 1
apply (rule red_DFS_precond, simp_all) []
apply (auto simp: find_path1_restr_pred_def restr_invar_def)
done
note aux = leof_trans[OF this[simplified,THEN leof_lift]]
note [refine_vcg del] = find_path1_restr_spec_rule
from finish show ?case
apply simp
apply (intro conjI impI)
unfolding run_red_dfs_def mk_blue_witness_def cyan_def
apply clarsimp
apply (refine_vcg aux)
apply (auto split: sum.splits)
done
next
case back_edge thus ?case
by (simp add: se_back_edge_def split: option.split)
qed simp_all
lemma no_accpt_cycle_in_finish:
"⟦lasso s = None; accpt v; v ∈ dom (finished s)⟧ ⟹ (v,v) ∉ E⇧+"
using i_no_accpt_cyle_in_finish[THEN make_invar_thm]
by blast
end
context BlueDFS
begin
definition lasso_inv where
"lasso_inv s ≡ ∀pr pl. lasso s = Some (pr,pl) ⟶
pl ≠ []
∧ (∃v0∈V0. path E v0 pr (hd pl))
∧ accpt (hd pl)
∧ path E (hd pl) pl (hd pl)"
lemma (in BlueDFS_invar) se_back_edge_lasso_inv:
assumes b_inv: "lasso_inv s"
and ne: "stack s ≠ []"
and R: "lasso s = None"
and p:"(hd (stack s), v) ∈ pending s"
and v: "v ∈ dom (discovered s)" "v ∉ dom (finished s)"
and s': "s' = back_edge (hd (stack s)) v (s⦇pending := pending s - {(u,v)}⦈)"
shows "se_back_edge (hd (stack s)) v s'
≤ SPEC (λe. DFS_invar G blue_dfs_params (s'⦇state.more := e⦈) ⟶
lasso_inv (s'⦇state.more := e⦈))"
proof -
from v stack_set_def have v_in: "v ∈ set (stack s)" by simp
from p have uv_edg: "(hd (stack s), v) ∈ E" by (auto dest: pendingD)
{
assume accpt: "accpt (hd (stack s))"
let ?ur = "rev (tl (stack s))"
let ?ul = "hd (stack s)#dropWhileNot v (rev (tl (stack s)))"
let ?s = "s'⦇lasso := Some (?ur, ?ul), red := red s⦈"
assume "DFS_invar G blue_dfs_params ?s"
have [simp]: "stack ?s = stack s"
by (simp add: s')
have hd_ul[simp]: "hd ?ul = hd (stack s)" by simp
have "?ul ≠ []" by simp
moreover have P:"∃v0∈V0. path E v0 ?ur (hd ?ul)"
using stack_is_path[OF ne]
by auto
moreover
from accpt have "accpt (hd ?ul)" by simp
moreover have "path E (hd ?ul) ?ul (hd ?ul)"
proof (cases "v = hd (stack s)")
case True
with distinct_hd_tl stack_distinct have ul: "?ul = [hd (stack s)]"
by force
from True uv_edg show ?thesis
by (subst ul)+ (simp add: path1)
next
case False with v_in ne have "v ∈ set ?ur"
by (auto simp add: neq_Nil_conv)
with P show ?thesis
by (fastforce intro: path_prepend
dropWhileNot_path[where p="?ur"]
uv_edg)
qed
ultimately have "lasso_inv ?s" by (simp add: lasso_inv_def)
}
moreover
{
assume accpt: "accpt v"
let ?vr = "takeWhileNot v (rev (stack s))"
let ?vl = "dropWhileNot v (rev (stack s))"
let ?s = "s'⦇lasso := Some(?vr, ?vl), red := red s⦈"
assume "DFS_invar G blue_dfs_params ?s"
have [simp]: "stack ?s = stack s"
by (simp add: s')
from ne v_in have hd_vl[simp]: "hd ?vl = v"
by (induct ("stack s") rule: rev_nonempty_induct) auto
from v_in have "?vl ≠ []" by simp
moreover from hd_succ_stack_is_path[OF ne] uv_edg have
P: "∃v0∈V0. path E v0 (rev (stack s)) v"
by auto
with ne v_in have "∃v0∈V0. path E v0 ?vr (hd ?vl)"
by (force intro: takeWhileNot_path)
moreover from accpt have "accpt (hd ?vl)" by simp
moreover from P ne v_in have "path E (hd ?vl) ?vl (hd ?vl)"
by (force intro: dropWhileNot_path)
ultimately have "lasso_inv ?s" by (simp add: lasso_inv_def)
}
moreover
{
assume "¬ accpt (hd (stack s))" "¬ accpt v"
let ?s = "s'⦇state.more := state.more s'⦈"
assume "DFS_invar G blue_dfs_params ?s"
from assms have "lasso_inv ?s"
by (auto simp add: lasso_inv_def)
}
ultimately show ?thesis
using R s'
unfolding se_back_edge_def
by (auto split: option.splits)
qed
lemma lasso_inv:
"is_invar lasso_inv"
proof (induct rule: establish_invarI)
case (finish s s' u) then interpret BlueDFS_invar where s=s by simp
let ?onstack = "λx. x ∈ set (stack s)"
let ?rE = "rel_restrict E (red s)"
let ?revs = "rev (tl (stack s))"
note ne = ‹stack s ≠ []›
note [simp] = ‹u=hd (stack s)›
from finish have [simp]:
"⋀x. x = hd (stack s) ∨ x ∈ set (stack s') ⟷ x∈set (stack s)"
"red s' = red s"
"lasso s' = lasso s"
by (auto simp: neq_Nil_conv)
{
fix v vs
let ?cyc = "vs @ dropWhileNot v ?revs"
let ?s = "s'⦇lasso := Some (?revs, ?cyc), red := red s⦈"
assume "DFS_invar G blue_dfs_params ?s"
and vs: "vs ≠ []" "path ?rE (hd (stack s)) vs v"
and v: "?onstack v"
and accpt: "accpt (hd (stack s))"
from vs have P: "path E (hd (stack s)) vs v"
by (metis path_mono rel_restrict_sub)
have hds[simp]: "hd vs = hd (stack s)" "hd ?cyc = hd (stack s)"
using vs path_hd
by simp_all
from vs have "?cyc ≠ []" by simp
moreover have P0: "∃v0∈V0. path E v0 ?revs (hd ?cyc)"
using stack_is_path[OF ne]
by auto
moreover from accpt have "accpt (hd ?cyc)" by simp
moreover have "path E (hd ?cyc) ?cyc (hd ?cyc)"
proof (cases "tl (stack s) = []")
case True with ne last_stack_in_V0 obtain v0 where "v0 ∈ V0"
and [simp]: "stack s = [v0]"
by (auto simp: neq_Nil_conv)
with v True finish have [simp]: "v = v0" by simp
from True P show ?thesis by simp
next
case False note tl_ne = this
show ?thesis
proof (cases "v = hd (stack s)")
case True hence "v ∉ set ?revs"
using ne stack_distinct by (auto simp: neq_Nil_conv)
hence "?cyc = vs" by fastforce
with P True show ?thesis by (simp del: dropWhile_eq_Nil_conv)
next
case False with finish v have "v ∈ set ?revs"
by (auto simp: neq_Nil_conv)
with tl_ne False P0 show ?thesis
by (force intro: path_conc[OF P]
dropWhileNot_path[where p="?revs"])
qed
qed
ultimately have "lasso_inv ?s" by (simp add: lasso_inv_def)
}
hence "accpt (hd (stack s)) ⟶ lasso s = None ⟶
red_dfs (red s) ?onstack (hd (stack s)) ≤ SPEC (λrs. ∀vs v.
rs = Inr (vs,v) ⟶
DFS_invar G blue_dfs_params (s'⦇lasso := Some (?revs, vs @ dropWhileNot v ?revs), red:= red s⦈) ⟶
lasso_inv (s'⦇lasso := Some (?revs, vs @ dropWhileNot v ?revs), red:=red s⦈))"
apply clarsimp
apply (rule find_path1_restr_spec_rule, intro conjI)
apply (rule red_DFS_precond, simp_all add: ne) []
apply (simp, rule red_DFS_precond, simp_all add: ne) []
using red_stack_disjoint ne
apply clarsimp
apply rprems
apply (simp_all add: find_path1_restr_pred_def restr_invar_def)
apply (fastforce intro: path_restrict_tl rel_restrictI)
done
note aux1 = this[rule_format,THEN leof_lift]
show ?case
apply simp
unfolding run_red_dfs_def mk_blue_witness_def cyan_def
apply (simp
add: run_red_dfs_def mk_blue_witness_def cyan_def
split: option.splits)
apply (intro conjI impI)
apply (refine_vcg leof_trans[OF aux1])
using finish
apply (auto simp add: lasso_inv_def split: sum.split)
done
next
case (back_edge s s' u v) then interpret BlueDFS_invar where s=s by simp
from back_edge se_back_edge_lasso_inv[THEN leof_lift] show ?case
by auto
qed (simp_all add: lasso_inv_def empty_state_def)
end
context BlueDFS_invar
begin
lemmas s_lasso_inv = lasso_inv[THEN make_invar_thm]
lemma
assumes "lasso s = Some (pr,pl)"
shows loop_nonempty: "pl ≠ []"
and accpt_loop: "accpt (hd pl)"
and loop_is_path: "path E (hd pl) pl (hd pl)"
and loop_reachable: "∃v0∈V0. path E v0 pr (hd pl)"
using assms s_lasso_inv
by (simp_all add: lasso_inv_def)
lemma blue_dfs_correct:
assumes NC: "¬ cond s"
shows "case lasso s of
None ⇒ ¬(∃v0∈V0. ∃v. (v0,v) ∈ E⇧* ∧ accpt v ∧ (v,v) ∈ E⇧+)
| Some (pr,pl) ⇒ (∃v0∈V0. ∃v.
path E v0 pr v ∧ accpt v ∧ pl≠[] ∧ path E v pl v)"
proof (cases "lasso s")
case None
moreover
{
fix v v0
assume "v0 ∈ V0" "(v0,v) ∈ E⇧*" "accpt v" "(v,v) ∈ E⇧+"
moreover
hence "v ∈ reachable" by (auto)
with nc_finished_eq_reachable NC None have "v ∈ dom (finished s)"
by simp
moreover note no_accpt_cycle_in_finish None
ultimately have False by blast
}
ultimately show ?thesis by auto
next
case (Some prpl) with s_lasso_inv show ?thesis
by (cases prpl)
(auto intro: path_is_rtrancl path_is_trancl simp: lasso_inv_def)
qed
end
subsection ‹Interface›
interpretation BlueDFS_defs for G accpt