# 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"
― ‹Auxiliary lemma to show that nodes reachable from a finished node must
be finished if, additionally, no stack node is reachable›
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" (* pr × pl *)
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' ⌦‹∪ red s›) ⦈
| 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 ⇒
― ‹it's a back edge, so ‹u› and ‹v› are both on stack›
― ‹we differentiate whether ‹u› or ‹v› is the 'culprit'›
― ‹to generate a better counter example›
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)"
} 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 (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

(* Play of Colors *)
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

{ (* TODO/FIXME: Ughly proof structure! *)
fix R'::"'v set"
let ?R' = "R' ⌦‹∪ red s›"
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 ⌦‹∪ red s›⦈) ⟶
(∀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"

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"
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"

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"
}

(* TODO: Clean up this proof, separate logical arguments from framework
boilerplate! *)
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
(* TODO/FIXME: Ughly proof structure *)
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 (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
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
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

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 .

definition "nested_dfs_spec G accpt ≡ λr. case r of
None ⇒ ¬(∃v0∈g_V0 G. ∃v. (v0,v) ∈ (g_E G)⇧* ∧ accpt v ∧ (v,v) ∈ (g_E G)⇧+)
| Some (pr,pl) ⇒ (∃v0∈g_V0 G. ∃v.
path (g_E G) v0 pr v ∧ accpt v ∧ pl≠[] ∧ path (g_E G) v pl v)"

definition "nested_dfs G accpt ≡ do {
ASSERT (fb_graph G);
s ← it_dfs TYPE('a) G accpt;
RETURN (lasso s)
}"

theorem nested_dfs_correct:
assumes "fb_graph G"
shows "nested_dfs G accpt ≤ SPEC (nested_dfs_spec G accpt)"
proof -
interpret fb_graph G by fact
interpret BlueDFS G accpt by unfold_locales

show ?thesis
unfolding nested_dfs_def
apply (refine_rcg refine_vcg)
apply fact
apply (rule weaken_SPEC[OF it_dfs_correct])
apply clarsimp
proof -
fix s
assume "BlueDFS_invar G accpt s"
then interpret BlueDFS_invar G accpt s .

assume "¬cond TYPE('b) G accpt s"
from blue_dfs_correct[OF this] show "nested_dfs_spec G accpt (lasso s)"
unfolding nested_dfs_spec_def by simp
qed
qed

subsection ‹Implementation›

record 'v bdfs_state_impl = "'v simple_state" +
lasso_impl :: "('v list × 'v list) option"
red_impl :: "'v set"

definition "bdfs_erel ≡ {(⦇lasso_impl=li,red_impl=ri⦈,⦇lasso=l, red=r⦈)
| li ri l r. li=l ∧ ri=r}"

abbreviation "bdfs_rel ≡ ⟨bdfs_erel⟩simple_state_rel"

definition mk_blue_witness_impl
:: "'v bdfs_state_impl ⇒ 'v fpr_result ⇒ ('v,unit) bdfs_state_impl_ext"
where
"mk_blue_witness_impl s redS ≡
case redS of
Inl R' ⇒ ⦇ lasso_impl = None, red_impl = (R' ⌦‹∪ red_impl s›) ⦈
| Inr (vs, v) ⇒ let
rs = rev (map fst (CAST (ss_stack s)))
in ⦇
lasso_impl = Some (rs, vs@dropWhileNot v rs),
red_impl = red_impl s⦈"

lemma mk_blue_witness_impl[refine]:
"⟦ (si,s)∈bdfs_rel; (ri,r)∈⟨Id, ⟨Id⟩list_rel ×⇩r Id⟩sum_rel ⟧
⟹ (mk_blue_witness_impl si ri, mk_blue_witness s r)∈bdfs_erel"
unfolding mk_blue_witness_impl_def mk_blue_witness_def
apply parametricity
apply (cases si, cases s)
apply (auto simp: bdfs_erel_def simple_state_rel_def) []
apply (rule introR[where R="⟨Id⟩list_rel"])
apply (cases si, cases s)
apply (auto simp: bdfs_erel_def simple_state_rel_def comp_def) []
apply (cases si, cases s)
apply (auto simp: bdfs_erel_def simple_state_rel_def) []
done

definition "cyan_impl s ≡ on_stack s"
lemma cyan_impl[refine]: "⟦(si,s)∈bdfs_rel⟧ ⟹ (cyan_impl si, cyan s)∈Id"
unfolding cyan_impl_def cyan_def
by (auto simp: bdfs_erel_def simple_state_rel_def)

definition run_red_dfs_impl
:: "('v, 'more) graph_rec_scheme ⇒ 'v ⇒ 'v bdfs_state_impl ⇒ ('v,unit) bdfs_state_impl_ext nres"
where
"run_red_dfs_impl G u s ≡ case lasso_impl s of None ⇒ do {
redS ← red_dfs TYPE('more) G (red_impl s) (λx. x = u ∨ x ∈ cyan_impl s) u;
RETURN (mk_blue_witness_impl s redS)
}
| _ ⇒ RETURN (simple_state.more s)"

lemma run_red_dfs_impl[refine]: "⟦(Gi,G)∈Id; (ui,u)∈Id; (si,s)∈bdfs_rel⟧
⟹ run_red_dfs_impl Gi ui si ≤⇓bdfs_erel (run_red_dfs TYPE('a) G u s)"
unfolding run_red_dfs_impl_def run_red_dfs_def
apply refine_rcg
apply refine_dref_type
apply (cases si, cases s, auto simp: bdfs_erel_def simple_state_rel_def) []
apply (cases si, cases s,
auto simp: bdfs_erel_def simple_state_rel_def cyan_impl_def cyan_def) []
apply (auto simp: bdfs_erel_def simple_state_rel_def) [2]
done

definition "se_back_edge_impl accpt u v s ≡ case lasso_impl s of
None ⇒
if accpt u then
let rs = rev (map fst (tl (CAST (ss_stack s))));
ur = rs;
ul = u#dropWhileNot v rs
in RETURN ⦇lasso_impl = Some (ur,ul), red_impl = red_impl s⦈
else if accpt v then
let rs = rev (map fst (CAST (ss_stack s)));
vr = takeWhileNot v rs;
vl = dropWhileNot v rs
in RETURN ⦇lasso_impl = Some (vr,vl), red_impl = red_impl s⦈
else RETURN (simple_state.more s)
| _ ⇒ RETURN (simple_state.more s)"

lemma se_back_edge_impl[refine]: "⟦ (accpti,accpt)∈Id; (ui,u)∈Id; (vi,v)∈Id; (si,s)∈bdfs_rel ⟧
⟹ se_back_edge_impl accpt ui vi si ≤⇓bdfs_erel (se_back_edge accpt u v s)"
unfolding se_back_edge_impl_def se_back_edge_def
apply refine_rcg
apply refine_dref_type
apply simp_all
apply (cases si, cases s, (auto) [])
apply (cases si, cases s, (auto simp: map_tl comp_def) [])
apply (cases si, cases s, (auto simp: comp_def) [])
done

lemma NOOP_impl: "(si, s) ∈ bdfs_rel
⟹ RETURN (simple_state.more si) ≤ ⇓ bdfs_erel (NOOP s)"
apply (auto simp: simple_state_rel_def)
done

definition bdfs_params_impl
:: "('v, 'more) graph_rec_scheme ⇒ ('v ⇒ bool) ⇒ ('v,'v bdfs_state_impl,('v,unit)bdfs_state_impl_ext) gen_parameterization"
where "bdfs_params_impl G accpt ≡ ⦇
on_init = RETURN ⦇lasso_impl = None, red_impl = {}⦈,
on_new_root = λv0 s. RETURN (simple_state.more s),
on_discover = λu v s. RETURN (simple_state.more s),
on_finish = λu s.
if accpt u then run_red_dfs_impl G u s else RETURN (simple_state.more s),
on_back_edge = se_back_edge_impl accpt,
on_cross_edge = λu v s. RETURN (simple_state.more s),
is_break = λs. lasso_impl s ≠ None ⦈"

lemmas bdfs_params_impl_simps[simp, DFS_code_unfold] =
gen_parameterization.simps[mk_record_simp, OF bdfs_params_impl_def]

interpretation impl: simple_impl_defs G "bdfs_params_impl G accpt" "blue_dfs_params TYPE('a) G accpt"
for G accpt .

context BlueDFS begin

sublocale impl: simple_impl G blue_dfs_params "bdfs_params_impl G accpt" bdfs_erel
apply unfold_locales

apply (simp_all
apply parametricity
apply (clarsimp_all simp: pw_le_iff refine_pw_simps bdfs_erel_def simple_state_rel_def)
apply (rename_tac si s x y, case_tac si, case_tac s)
apply (auto simp add: bdfs_erel_def simple_state_rel_def) []
done

lemmas impl = impl.simple_tailrec_refine
end

definition "nested_dfs_impl G accpt ≡ do {
ASSERT (fb_graph G);
s ← impl.tailrec_impl TYPE('a) G accpt;
RETURN (lasso_impl s)
}"

lemma nested_dfs_impl[refine]:
assumes "(Gi,G)∈Id"
assumes "(accpti,accpt)∈Id"
shows "nested_dfs_impl Gi accpti ≤⇓(⟨⟨Id⟩list_rel ×⇩r ⟨Id⟩list_rel⟩option_rel)
(nested_dfs G accpt)"
using assms
unfolding nested_dfs_impl_def nested_dfs_def
apply refine_rcg
apply simp_all
apply (rule intro_prgR[where R=bdfs_rel])
defer
apply (rename_tac si s)
apply (case_tac si, case_tac s)
apply (auto simp: bdfs_erel_def simple_state_rel_def) []
proof -
assume "fb_graph G"
then interpret fb_graph G .
interpret BlueDFS G by unfold_locales

from impl show "impl.tailrec_impl TYPE('b) G accpt ≤⇓bdfs_rel (it_dfs TYPE('b) G accpt)" .
qed

subsection ‹Synthesis of Executable Code›
(* Straightforward autoref implementation *)
record ('v,'si,'nsi)bdfs_state_impl' = "('si,'nsi)simple_state_impl" +
lasso_impl' :: "('v list × 'v list) option"
red_impl' :: 'nsi

definition [to_relAPP]: "bdfs_state_erel' Vi ≡ {
(⦇lasso_impl' = li, red_impl'=ri⦈,⦇lasso_impl = l, red_impl = r⦈) | li ri l r.
(li,l)∈⟨⟨Vi⟩list_rel ×⇩r ⟨Vi⟩list_rel⟩option_rel ∧ (ri,r)∈⟨Vi⟩dflt_ahs_rel}"

consts
i_bdfs_state_ext :: "interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of bdfs_state_erel' i_bdfs_state_ext]

lemma [autoref_rules]:
fixes ns_rel vis_rel Vi
defines "R ≡ ⟨ns_rel,vis_rel,⟨Vi⟩bdfs_state_erel'⟩ss_impl_rel"
shows
"(bdfs_state_impl'_ext, bdfs_state_impl_ext)
∈ ⟨⟨Vi⟩list_rel ×⇩r ⟨Vi⟩list_rel⟩option_rel → ⟨Vi⟩dflt_ahs_rel → unit_rel → ⟨Vi⟩bdfs_state_erel'"
"(lasso_impl', lasso_impl) ∈ R → ⟨⟨Vi⟩list_rel ×⇩r ⟨Vi⟩list_rel⟩option_rel"
"(red_impl', red_impl) ∈ R → ⟨Vi⟩dflt_ahs_rel"
unfolding bdfs_state_erel'_def ss_impl_rel_def R_def
by auto

schematic_goal nested_dfs_code:
assumes Vid: "V = (Id :: ('v::hashable × 'v) set)"
assumes [unfolded Vid, autoref_rules]:
"(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
"(accpti,accpt) ∈ (V → bool_rel)"
notes [unfolded Vid, autoref_tyrel] =
TYRELI[where R="⟨V⟩dflt_ahs_rel"]
TYRELI[where R="⟨V⟩ras_rel"]
shows "(nres_of ?c, nested_dfs_impl G accpt)
∈ ⟨⟨⟨V⟩list_rel ×⇩r ⟨V⟩list_rel⟩option_rel⟩nres_rel"
unfolding nested_dfs_impl_def[abs_def] Vid
se_back_edge_impl_def run_red_dfs_impl_def mk_blue_witness_impl_def
cyan_impl_def
DFS_code_unfold
(*apply (subst aux1)*)
using [[autoref_trace_failed_id]]
done

concrete_definition nested_dfs_code uses nested_dfs_code

export_code nested_dfs_code checking SML

subsection ‹Conclusion›
text ‹
We have implemented an efficiently executable nested DFS algorithm.
The following theorem declares this implementation to the Autoref tool,
such that it uses it to synthesize efficient code for @{const nested_dfs}.
Note that you will need the lemma @{thm [source] nested_dfs_correct} to link
@{const nested_dfs} to an abstract specification, which is usually done in
a previous refinement step.
›
theorem nested_dfs_autoref[autoref_rules]:
assumes "PREFER_id V"
shows "(λ G accpt. nres_of (nested_dfs_code G accpt),nested_dfs) ∈
⟨Rm, V⟩g_impl_rel_ext → (V → bool_rel) →
⟨⟨⟨V⟩list_rel ×⇩r ⟨V⟩list_rel⟩option_rel⟩nres_rel"
proof -
from assms have Vid: "V=Id" by simp
note nested_dfs_code.refine[OF Vid,param_fo, THEN nres_relD]
also note nested_dfs_impl
finally show ?thesis by (fastforce intro: nres_relI)
qed

end

```