# Theory DFS_Framework.Param_DFS

```section ‹General DFS with Hooks›
theory Param_DFS
imports
CAVA_Base.CAVA_Base
CAVA_Automata.Digraph
"Misc/DFS_Framework_Refine_Aux"
begin

text ‹
We define a general DFS algorithm, which is parameterized over
hook functions at certain events during the DFS.
›

subsection ‹State and Parameterization›
(* A DFS with timing and a stack, phrased iteratively *)
text ‹The state of the general DFS.
Users may inherit from this state using the record package's
inheritance support.
›
record 'v state =
counter :: nat               ― ‹Node counter (timer)›
discovered :: "'v ⇀ nat"    ― ‹Discovered times of nodes›
finished :: "'v ⇀ nat"      ― ‹Finished times of nodes›
pending :: "('v × 'v) set"  ― ‹Edges to be processed next›
stack :: "'v list"          ― ‹Current DFS stack›
tree_edges :: "'v rel"      ― ‹Tree edges›
back_edges :: "'v rel"      ― ‹Back edges›
cross_edges :: "'v rel"     ― ‹Cross edges›

abbreviation "NOOP s ≡ RETURN (state.more s)"

text ‹Record holding the parameterization.›
record ('v,'s,'es) gen_parameterization =
on_init :: "'es nres"
on_new_root :: "'v ⇒ 's ⇒ 'es nres"
on_discover :: "'v ⇒ 'v ⇒ 's ⇒ 'es nres"
on_finish :: "'v ⇒ 's ⇒ 'es nres"
on_back_edge :: "'v ⇒ 'v ⇒ 's ⇒ 'es nres"
on_cross_edge :: "'v ⇒ 'v ⇒ 's ⇒ 'es nres"
is_break :: "'s ⇒ bool"

text ‹Default type restriction for parameterizations.
The event handler functions go from a complete state to
the user-defined part of the state (i.e. the fields added by inheritance).
›
type_synonym ('v,'es) parameterization
= "('v,('v,'es) state_scheme,'es) gen_parameterization"

text ‹Default parameterization, the functions do nothing.
This can be used as the basis for specialized parameterizations, which may
be derived by updating some fields.
›
definition "⋀more init. dflt_parametrization more init ≡ ⦇
on_init = init,
on_new_root = λ_. RETURN o more,
on_discover = λ_ _. RETURN o more,
on_finish = λ_. RETURN o more,
on_back_edge = λ_ _. RETURN o more,
on_cross_edge = λ_ _. RETURN o more,
is_break = λ_. False ⦈"
lemmas dflt_parametrization_simp[simp] =
gen_parameterization.simps[mk_record_simp, OF dflt_parametrization_def]

text ‹This locale builds a DFS algorithm from a graph and a parameterization.›
locale param_DFS_defs =
graph_defs G
for G :: "('v, 'more) graph_rec_scheme"
+
fixes param :: "('v,'es) parameterization"
begin
subsection ‹DFS operations›
subsubsection ‹Node predicates›
text ‹First, we define some predicates to check whether nodes are in certain sets›
definition is_discovered :: "'v ⇒ ('v,'es) state_scheme ⇒ bool"
where "is_discovered u s ≡ u ∈ dom (discovered s)"

definition is_finished :: "'v ⇒ ('v,'es) state_scheme ⇒ bool"
where "is_finished u s ≡ u ∈ dom (finished s)"

definition is_empty_stack :: "('v,'es) state_scheme ⇒ bool"
where "is_empty_stack s ≡ stack s = []"

(*definition top_pending :: "('v,'es) state_scheme ⇒ 'v × 'v set" where
"top_pending s ≡ (hd (stack s), pending s `` {hd (stack s)})"*)

subsubsection ‹Effects on Basic State›
text ‹We define the effect of the operations on the basic part of the state›
definition discover
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
where
"discover u v s ≡ let
d = (discovered s)(v ↦ counter s); c = counter s + 1;
st = v#stack s;
p = pending s ∪ {v} × E``{v};
t = insert (u,v) (tree_edges s)
in s⦇ discovered := d, counter := c, stack := st, pending := p, tree_edges := t⦈"

lemma discover_simps[simp]:
"counter (discover u v s) = Suc (counter s)"
"discovered (discover u v s) = (discovered s)(v ↦ counter s)"
"finished (discover u v s) = finished s"
"stack (discover u v s) = v#stack s"
"pending (discover u v s) = pending s ∪ {v} × E``{v}"
"tree_edges (discover u v s) = insert (u,v) (tree_edges s)"
"cross_edges (discover u v s) = cross_edges s"
"back_edges (discover u v s) = back_edges s"
"state.more (discover u v s) = state.more s"
by (simp_all add: discover_def)

definition finish
:: "'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
where
"finish u s ≡ let
f = (finished s)(u ↦ counter s); c = counter s + 1;
st = tl (stack s)
in s⦇ finished := f, counter := c, stack := st⦈"

lemma finish_simps[simp]:
"counter (finish u s) = Suc (counter s)"
"discovered (finish u s) = discovered s"
"finished (finish u s) = (finished s)(u ↦ counter s)"
"stack (finish u s) = tl (stack s)"
"pending (finish u s) = pending s"
"tree_edges (finish u s) = tree_edges s"
"cross_edges (finish u s) = cross_edges s"
"back_edges (finish u s) = back_edges s"
"state.more (finish u s) = state.more s"
by (simp_all add: finish_def)

definition back_edge
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
where
"back_edge u v s ≡ let
b = insert (u,v) (back_edges s)
in s⦇ back_edges := b ⦈"

lemma back_edge_simps[simp]:
"counter (back_edge u v s) = counter s"
"discovered (back_edge u v s) = discovered s"
"finished (back_edge u v s) = finished s"
"stack (back_edge u v s) = stack s"
"pending (back_edge u v s) = pending s"
"tree_edges (back_edge u v s) = tree_edges s"
"cross_edges (back_edge u v s) = cross_edges s"
"back_edges (back_edge u v s) = insert (u,v) (back_edges s)"
"state.more (back_edge u v s) = state.more s"
by (simp_all add: back_edge_def)

definition cross_edge
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
where
"cross_edge u v s ≡ let
c = insert (u,v) (cross_edges s)
in s⦇ cross_edges := c ⦈"

lemma cross_edge_simps[simp]:
"counter (cross_edge u v s) = counter s"
"discovered (cross_edge u v s) = discovered s"
"finished (cross_edge u v s) = finished s"
"stack (cross_edge u v s) = stack s"
"pending (cross_edge u v s) = pending s"
"tree_edges (cross_edge u v s) = tree_edges s"
"cross_edges (cross_edge u v s) = insert (u,v) (cross_edges s)"
"back_edges (cross_edge u v s) = back_edges s"
"state.more (cross_edge u v s) = state.more s"
by (simp_all add: cross_edge_def)

definition new_root
:: "'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
where
"new_root v0 s ≡ let
c = Suc (counter s);
d = (discovered s)(v0 ↦ counter s);
p = {v0}×E``{v0};
st = [v0]
in s⦇counter := c, discovered := d, pending := p, stack := st⦈"

lemma new_root_simps[simp]:
"counter (new_root v0 s) = Suc (counter s)"
"discovered (new_root v0 s) = (discovered s)(v0 ↦ counter s)"
"finished (new_root v0 s) = finished s"
"stack (new_root v0 s) = [v0]"
"pending (new_root v0 s) = ({v0}×E``{v0})"
"tree_edges (new_root v0 s) = tree_edges s"
"cross_edges (new_root v0 s) = cross_edges s"
"back_edges (new_root v0 s) = back_edges s"
"state.more (new_root v0 s) = state.more s"
by (simp_all add: new_root_def)

definition "empty_state e
≡ ⦇ counter = 0,
discovered = Map.empty,
finished = Map.empty,
pending = {},
stack = [],
tree_edges = {},
back_edges = {},
cross_edges = {},
… = e ⦈"

lemma empty_state_simps[simp]:
"counter (empty_state e) = 0"
"discovered (empty_state e) = Map.empty"
"finished (empty_state e) = Map.empty"
"pending (empty_state e) = {}"
"stack (empty_state e) = []"
"tree_edges (empty_state e) = {}"
"back_edges (empty_state e) = {}"
"cross_edges (empty_state e) = {}"
"state.more (empty_state e) = e"
by (simp_all add: empty_state_def)

subsubsection ‹Effects on Whole State›
text ‹The effects of the operations on the whole state are defined by
combining the effects of the basic state with the parameterization.›

definition do_cross_edge
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
where
"do_cross_edge u v s ≡ do {
let s = cross_edge u v s;
e ← on_cross_edge param u v s;
RETURN (s⦇state.more := e⦈)
}"

definition do_back_edge
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
where
"do_back_edge u v s ≡ do {
let s = back_edge u v s;
e ← on_back_edge param u v s;
RETURN (s⦇state.more := e⦈)
}"

definition do_known_edge
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
where
"do_known_edge u v s ≡
if is_finished v s then
do_cross_edge u v s
else
do_back_edge u v s"

definition do_discover
:: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
where
"do_discover u v s ≡ do {
let s = discover u v s;
e ← on_discover param u v s;
RETURN (s⦇state.more := e⦈)
}"

definition do_finish
:: "'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
where
"do_finish u s ≡ do {
let s = finish u s;
e ← on_finish param u s;
RETURN (s⦇state.more := e⦈)
}"

definition get_new_root where
"get_new_root s ≡ SPEC (λv. v∈V0 ∧ ¬is_discovered v s)"

definition do_new_root where
"do_new_root v0 s ≡ do {
let s = new_root v0 s;
e ← on_new_root param v0 s;
RETURN (s⦇state.more := e⦈)
}"

lemmas op_defs = discover_def finish_def back_edge_def cross_edge_def new_root_def
lemmas do_defs = do_discover_def do_finish_def do_known_edge_def
do_cross_edge_def do_back_edge_def do_new_root_def
lemmas pred_defs = is_discovered_def is_finished_def is_empty_stack_def

definition "init ≡ do {
e ← on_init param;
RETURN (empty_state e)
}"

subsection ‹DFS Algorithm›
text ‹We phrase the DFS algorithm iteratively:
While there are undiscovered root nodes or the stack is not empty,
inspect the topmost node on the stack:
Follow any pending edge, or finish the node if there
are no pending edges left.

›

definition cond :: "('v,'es) state_scheme ⇒ bool" where
"cond s ⟷ (V0 ⊆ {v. is_discovered v s} ⟶ ¬is_empty_stack s)
∧ ¬is_break param s"

lemma cond_alt:
"cond = (λs. (V0 ⊆ dom (discovered s) ⟶ stack s ≠ []) ∧ ¬is_break param s)"
apply (rule ext)
unfolding cond_def is_discovered_def is_empty_stack_def
by auto

definition get_pending ::
"('v, 'es) state_scheme ⇒ ('v × 'v option × ('v, 'es) state_scheme) nres"
― ‹Get topmost stack node and a pending edge if any. The pending
edge is removed.›
where "get_pending s ≡ do {
let u = hd (stack s);
let Vs = pending s `` {u};

if Vs = {} then
RETURN (u,None,s)
else do {
v ← RES Vs;
let s = s⦇ pending := pending s - {(u,v)}⦈;
RETURN (u,Some v,s)
}
}"

definition step :: "('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
where
"step s ≡
if is_empty_stack s then do {
v0 ← get_new_root s;
do_new_root v0 s
} else do {
(u,Vs,s) ← get_pending s;
case Vs of
None ⇒ do_finish u s
| Some v ⇒ do {
if is_discovered v s then
do_known_edge u v s
else
do_discover u v s
}
}"

definition "it_dfs ≡ init ⤜ WHILE cond step"
definition "it_dfsT ≡ init ⤜ WHILET cond step"

end

subsection ‹Invariants›
text ‹We now build the infrastructure for establishing invariants
of DFS algorithms. The infrastructure is modular and extensible, i.e.,
we can define re-usable libraries of invariants.
›

text ‹For technical reasons, invariants are established in a two-step process:
▸ First, we prove the invariant wrt. the parameterization in the ‹param_DFS› locale.
▸ Next, we transfer the invariant to the ‹DFS_invar›-locale.
›
(* This locale is required to establish new invariants.
We would like to directly establish new invariants in the
DFS_invar-locale, unfortunately this causes technical problems:
When interpreting the DFS_invar locale in a proof inside the
DFS_invar-locale itself, we get "duplicate constant" warnings,
unless we prefix the interpreted locale, which may be quite confusing
in a proof, as the user has to choose the prefixed lemmas, while the
unprefixed ones are also available, but for the wrong state.
*)
locale param_DFS =
fb_graph G + param_DFS_defs G param
for G :: "('v, 'more) graph_rec_scheme"
and param :: "('v,'es) parameterization"
begin

definition is_invar :: "(('v, 'es) state_scheme ⇒ bool) ⇒ bool"
― ‹Predicate that states that @{term I} is an invariant.›
where "is_invar I ≡ is_rwof_invar init cond step I"

end

text ‹Invariants are transferred to this locale, which is parameterized
with a state. ›
locale DFS_invar =
param_DFS G param
for G :: "('v, 'more) graph_rec_scheme"
and param :: "('v,'es) parameterization"
+
fixes s :: "('v,'es) state_scheme"
assumes rwof: "rwof init cond step s"
begin

lemma make_invar_thm: "is_invar I ⟹ I s"
― ‹Lemma to transfer an invariant into this locale›
using rwof_cons[OF _ rwof, folded is_invar_def] .

end

subsubsection ‹Establishing Invariants›
context param_DFS
begin
text ‹ Include this into refine-rules to discard any information about
parameterization ›
lemmas indep_invar_rules =
leof_True_rule[where m="on_init param"]
leof_True_rule[where m="on_new_root param v0 s'" for v0 s']
leof_True_rule[where m="on_discover param u v s'" for u v s']
leof_True_rule[where m="on_finish param v s'" for v s']
leof_True_rule[where m="on_cross_edge param u v s'" for u v s']
leof_True_rule[where m="on_back_edge param u v s'" for u v s']

lemma rwof_eq_DFS_invar[simp]:
"rwof init cond step = DFS_invar G param"
― ‹The DFS-invar locale is equivalent to the strongest invariant of the loop.›
apply (auto intro: DFS_invar.rwof intro!: ext)
by unfold_locales

lemma DFS_invar_step: "⟦nofail it_dfs; DFS_invar G param s; cond s⟧
⟹ step s ≤ SPEC (DFS_invar G param)"
― ‹A step preserves the (best) invariant.›
unfolding it_dfs_def rwof_eq_DFS_invar[symmetric]
by (rule rwof_step)

lemma DFS_invar_step': "⟦nofail (step s); DFS_invar G param s; cond s⟧
⟹ step s ≤ SPEC (DFS_invar G param)"
unfolding it_dfs_def rwof_eq_DFS_invar[symmetric]
by (rule rwof_step')

text ‹We define symbolic names for the preconditions of certain operations›
definition "pre_is_break s ≡ DFS_invar G param s"

definition "pre_on_new_root v0 s' ≡ ∃s.
DFS_invar G param s ∧ cond s ∧
stack s = [] ∧ v0 ∈ V0 ∧ v0 ∉ dom (discovered s) ∧
s' = new_root v0 s"

definition "pre_on_finish u s' ≡ ∃s.
DFS_invar G param s ∧ cond s ∧
stack s ≠ [] ∧ u = hd (stack s) ∧ pending s `` {u} = {} ∧ s' = finish u s"

definition "pre_edge_selected u v s ≡
DFS_invar G param s ∧ cond s ∧
stack s ≠ [] ∧ u = hd (stack s) ∧ (u, v) ∈ pending s"

definition "pre_on_cross_edge u v s' ≡ ∃s. pre_edge_selected u v s ∧
v ∈ dom (discovered s) ∧ v∈dom (finished s)
∧ s' = cross_edge u v (s⦇pending := pending s - {(u,v)}⦈)"

definition "pre_on_back_edge u v s' ≡ ∃s. pre_edge_selected u v s ∧
v ∈ dom (discovered s) ∧ v∉dom (finished s)
∧ s' = back_edge u v (s⦇pending := pending s - {(u,v)}⦈)"

definition "pre_on_discover u v s' ≡ ∃s. pre_edge_selected u v s ∧
v ∉ dom (discovered s)
∧ s' = discover u v (s⦇pending := pending s - {(u,v)}⦈)"

lemmas pre_on_defs = pre_on_new_root_def pre_on_finish_def
pre_edge_selected_def pre_on_cross_edge_def pre_on_back_edge_def
pre_on_discover_def pre_is_break_def

text ‹Next, we define a set of rules to establish an invariant.›

lemma establish_invarI[case_names init new_root finish cross_edge back_edge discover]:
― ‹Establish a DFS invariant (explicit preconditions).›
assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
assumes new_root: "⋀s s' v0.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s = []; v0 ∈ V0; v0 ∉ dom (discovered s);
s' = new_root v0 s⟧
⟹ on_new_root param v0 s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes finish: "⋀s s' u.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; u = hd (stack s);
pending s `` {u} = {};
s' = finish u s⟧
⟹ on_finish param u s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes cross_edge: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s);
v ∈ dom (discovered s); v∈dom (finished s);
s' = cross_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
⟹ on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes back_edge: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s);
v ∈ dom (discovered s); v∉dom (finished s);
s' = back_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
⟹ on_back_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes discover: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ [];  (u, v) ∈ pending s; u = hd (stack s);
v ∉ dom (discovered s);
s' = discover u v (s⦇pending := pending s - {(u,v)}⦈)⟧
⟹ on_discover param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
shows "is_invar I"
unfolding is_invar_def
proof
show "init ≤⇩n SPEC I"
unfolding init_def
by (refine_rcg refine_vcg) (simp add: init)
next
fix s
assume "rwof init cond step s" and IC: "I s" "cond s"
hence DI: "DFS_invar G param s" by unfold_locales
then interpret DFS_invar G param s .

from ‹cond s› have IB: "¬ is_break param s" by (simp add: cond_def)

have B: "step s ≤⇩n SPEC (DFS_invar G param)"
by rule (metis DFS_invar_step' DI ‹cond s›)

note rule_assms = DI IC IB

show "step s ≤⇩n SPEC I"
apply (rule leof_use_spec_rule[OF B])
unfolding step_def do_defs pred_defs get_pending_def get_new_root_def
apply (refine_rcg refine_vcg)
apply (simp_all)

apply (blast intro: new_root[OF rule_assms])
apply (blast intro: finish[OF rule_assms])
apply (rule cross_edge[OF rule_assms], auto) []
apply (rule back_edge[OF rule_assms], auto) []
apply (rule discover[OF rule_assms], auto) []
done
qed

lemma establish_invarI'[case_names init new_root finish cross_edge back_edge discover]:
― ‹Establish a DFS invariant (symbolic preconditions).›
assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
assumes new_root: "⋀s' v0. pre_on_new_root v0 s'
⟹ on_new_root param v0 s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes finish: "⋀s' u. pre_on_finish u s'
⟹ on_finish param u s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes cross_edge: "⋀s' u v. pre_on_cross_edge u v s'
⟹ on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes back_edge: "⋀s' u v. pre_on_back_edge u v s'
⟹ on_back_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes discover: "⋀s' u v. pre_on_discover u v s'
⟹ on_discover param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
shows "is_invar I"
apply (rule establish_invarI)
using assms
unfolding pre_on_defs
apply -
apply blast
apply (rprems,blast)+
done

lemma establish_invarI_ND [case_names prereq init new_discover finish cross_edge back_edge]:
― ‹Establish a DFS invariant (new-root and discover cases are combined).›
assumes prereq: "⋀u v s. on_discover param u v s = on_new_root param v s"
assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
assumes new_discover: "⋀s s' v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
v ∉ dom (discovered s);
discovered s' = (discovered s)(v↦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' ⊇ tree_edges s;
state.more s' = state.more s⟧
⟹ on_new_root param v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes finish: "⋀s s' u.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; u = hd (stack s);
pending s `` {u} = {};
s' = finish u s⟧
⟹ on_finish param u s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes cross_edge: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s);
v ∈ dom (discovered s); v∈dom (finished s);
s' = cross_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
⟹ on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes back_edge: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s);
v ∈ dom (discovered s); v∉dom (finished s);
s' = back_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
⟹ on_back_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
shows "is_invar I"
proof (induct rule: establish_invarI)
case (new_root s) thus ?case by (auto intro!: new_discover)
next
case (discover s s' u v) hence
"on_new_root param v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
by (auto intro!: new_discover)
with prereq show ?case by simp
qed fact+

(* Variant of establish_invarI, where cross_edge and back_edge are combined *)
lemma establish_invarI_CB [case_names prereq init new_root finish cross_back_edge discover]:
― ‹Establish a DFS invariant (cross and back edge cases are combined).›
assumes prereq: "⋀u v s. on_back_edge param u v s = on_cross_edge param u v s"
assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
assumes new_root: "⋀s s' v0.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s = []; v0 ∈ V0; v0 ∉ dom (discovered s);
s' = new_root v0 s⟧
⟹ on_new_root param v0 s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes finish: "⋀s s' u.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; u = hd (stack s);
pending s `` {u} = {};
s' = finish u s⟧
⟹ on_finish param u s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes cross_back_edge: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s);
v ∈ 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' ∪ back_edges s' = cross_edges s ∪ back_edges s ∪ {(u,v)};
state.more s' = state.more s ⟧
⟹ on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes discover: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ [];  (u, v) ∈ pending s; u = hd (stack s);
v ∉ dom (discovered s);
s' = discover u v (s⦇pending := pending s - {(u,v)}⦈)⟧
⟹ on_discover param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
shows "is_invar I"
proof (induct rule: establish_invarI)
case cross_edge thus ?case by (auto intro!: cross_back_edge)
next
case (back_edge s s' u v) hence
"on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
by (auto intro!: cross_back_edge)
with prereq show ?case by simp
qed fact+

(* Variant of establish_invarI, where cross_edge and back_edge, and discover and new_root are combined *)
lemma establish_invarI_ND_CB [case_names prereq_ND prereq_CB init new_discover finish cross_back_edge]:
― ‹Establish a DFS invariant (new-root/discover and cross/back-edge cases are combined).›
assumes prereq:
"⋀u v s. on_discover param u v s = on_new_root param v s"
"⋀u v s. on_back_edge param u v s = on_cross_edge param u v s"
assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
assumes new_discover: "⋀s s' v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
v ∉ dom (discovered s);
discovered s' = (discovered s)(v↦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' ⊇ tree_edges s;
state.more s' = state.more s⟧
⟹ on_new_root param v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes finish: "⋀s s' u.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; u = hd (stack s);
pending s `` {u} = {};
s' = finish u s⟧
⟹ on_finish param u s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
assumes cross_back_edge: "⋀s s' u v.
⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s);
v ∈ 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' ∪ back_edges s' = cross_edges s ∪ back_edges s ∪ {(u,v)};
state.more s' = state.more s ⟧
⟹ on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
shows "is_invar I"
proof (induct rule: establish_invarI_ND)
case cross_edge thus ?case by (auto intro!: cross_back_edge)
next
case (back_edge s s' u v) hence
"on_cross_edge param u v s' ≤⇩n
SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
⟶ I (s'⦇state.more := x⦈))"
by (auto intro!: cross_back_edge)
with prereq show ?case by simp
qed fact+

lemma is_invarI_full [case_names init new_root finish cross_edge back_edge discover]:
― ‹Establish a DFS invariant not taking into account the parameterization.›
assumes init: "⋀e. I (empty_state e)"
assumes new_root: "⋀s s' v0 e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s = []; v0 ∉ dom (discovered s); v0 ∈ V0;
s' = new_root v0 s⦇state.more := e⦈⟧
⟹ I s'"
and finish: "⋀s s' u e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; pending s `` {u} = {};
u = hd (stack s); s' = finish u s⦇state.more := e⦈⟧
⟹ I s'"
and cross_edge: "⋀s s' u v e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; v ∈ pending s `` {u}; v ∈ dom (discovered s);
v ∈ dom (finished s);
u = hd (stack s);
s' = (cross_edge u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
⟹ I s'"
and back_edge: "⋀s s' u v e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; v ∈ pending s `` {u}; v ∈ dom (discovered s); v ∉ dom (finished s);
u = hd (stack s);
s' = (back_edge u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
⟹ I s'"
and discover: "⋀s s' u v e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; v ∈ pending s `` {u}; v ∉ dom (discovered s);
u = hd (stack s);
s' = (discover u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
⟹ I s'"
shows "is_invar I"
apply (rule establish_invarI)
apply (blast intro: indep_invar_rules assms)+
done

lemma is_invarI [case_names init new_root finish visited discover]:
― ‹Establish a DFS invariant not taking into account the parameterization, cross/back-edges combined.›
assumes init': "⋀e. I (empty_state e)"
and new_root': "⋀s s' v0 e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s = []; v0 ∉ dom (discovered s); v0 ∈ V0;
s' = new_root v0 s⦇state.more := e⦈⟧
⟹ I s'"
and finish': "⋀s s' u e.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; pending s `` {u} = {};
u = hd (stack s); s' = finish u s⦇state.more := e⦈⟧
⟹ I s'"
and visited': "⋀s s' u v e c b.
⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; v ∈ pending s `` {u}; v ∈ dom (discovered s);
u = hd (stack s);
cross_edges s ⊆ c; back_edges s ⊆ b;
s' = s⦇
pending := pending s - {(u,v)},
state.more := e,
cross_edges := c,
back_edges := b⦈⟧
⟹ I s'"
and discover': "⋀s s' u v e.
⟦I s; cond s;  DFS_invar G param s; DFS_invar G param s';
stack s ≠ []; v ∈ pending s `` {u}; v ∉ dom (discovered s);
u = hd (stack s);
s' = (discover u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
⟹ I s'"
shows "is_invar I"
proof (induct rule: is_invarI_full)
case (cross_edge s s' u v e) thus ?case
apply -
apply (rule visited'[of s s' v u "insert (u,v) (cross_edges s)" "back_edges s" e])
apply clarsimp_all
done
next
case (back_edge s s' u v e) thus ?case
apply -
apply (rule visited'[of s s' v u "cross_edges s" "insert (u,v) (back_edges s)" e])
apply clarsimp_all
done
qed fact+

end

subsection ‹Basic Invariants›
text ‹We establish some basic invariants›

context param_DFS begin
(* Establish some invariants *)
definition "basic_invar s ≡
set (stack s) = dom (discovered s) - dom (finished s) ∧
distinct (stack s) ∧
(stack s ≠ [] ⟶ last (stack s) ∈ V0) ∧
dom (finished s) ⊆ dom (discovered s) ∧
Domain (pending s) ⊆ dom (discovered s) - dom (finished s) ∧
pending s ⊆ E"

lemma i_basic_invar: "is_invar basic_invar"
unfolding basic_invar_def[abs_def]
apply (induction rule: is_invarI)
apply (clarsimp_all simp: neq_Nil_conv last_tl)
apply blast+
done
end

context DFS_invar begin
lemmas basic_invar = make_invar_thm[OF i_basic_invar]

lemma pending_ssE: "pending s ⊆ E"
using basic_invar
by (auto simp: basic_invar_def)

lemma pendingD:
"(u,v)∈pending s ⟹ (u,v)∈E ∧ u∈dom (discovered s)"
using basic_invar
by (auto simp: basic_invar_def)

lemma stack_set_def:
"set (stack s) = dom (discovered s) - dom (finished s)"
using basic_invar
by (simp add: basic_invar_def)

lemma stack_discovered:
"set (stack s) ⊆ dom (discovered s)"
using stack_set_def
by auto

lemma stack_distinct:
"distinct (stack s)"
using basic_invar
by (simp add: basic_invar_def)

lemma last_stack_in_V0:
"stack s ≠ [] ⟹ last (stack s) ∈ V0"
using basic_invar
by (simp add: basic_invar_def)

lemma stack_not_finished:
"x ∈ set (stack s) ⟹ x ∉ dom (finished s)"
using stack_set_def
by auto

lemma discovered_not_stack_imp_finished:
"x ∈ dom (discovered s) ⟹ x ∉ set (stack s) ⟹ x ∈ dom (finished s)"
using stack_set_def
by auto

lemma finished_discovered:
"dom (finished s) ⊆ dom (discovered s)"
using basic_invar
by (auto simp add: basic_invar_def)

lemma finished_no_pending:
"v ∈ dom (finished s) ⟹ pending s `` {v} = {}"
using basic_invar
by (auto simp add: basic_invar_def)

lemma discovered_eq_finished_un_stack:
"dom (discovered s) = dom (finished s) ∪ set (stack s)"
using stack_set_def finished_discovered by auto

lemma pending_on_stack:
"(v,w) ∈ pending s ⟹ v ∈ set (stack s)"
using basic_invar
by (auto simp add: basic_invar_def)

lemma empty_stack_imp_empty_pending:
"stack s = [] ⟹ pending s = {}"
using pending_on_stack
by auto
end

context param_DFS begin

(* Establish some more invariants *)
lemma i_discovered_reachable:
"is_invar (λs. dom (discovered s) ⊆ reachable)"
proof (induct rule: is_invarI)
case (discover s) then interpret i: DFS_invar where s=s by simp
from discover show ?case
apply (clarsimp dest!: i.pendingD)
by (metis contra_subsetD list.set_sel(1) rtrancl_image_advance i.stack_discovered)
qed auto

definition "discovered_closed s ≡
E``dom (finished s) ⊆ dom (discovered s)
∧ (E - pending s) `` set (stack s) ⊆ dom (discovered s)"

lemma i_discovered_closed: "is_invar discovered_closed"
proof (induct rule: is_invarI)
case (finish s s')
hence "(E - pending s) `` set (stack s) ⊆ dom (discovered s)"
by (simp add: discovered_closed_def)
moreover from finish have "set (stack s') ⊆ set (stack s)"
by (auto simp add: neq_Nil_conv cond_def)
ultimately have "(E - pending s') `` set (stack s') ⊆ dom (discovered s')"
using finish
by simp blast

moreover
from ‹stack s ≠ []› finish have "E``dom (finished s') ⊆ dom (discovered s')"
apply (cases "stack s") apply simp
apply (simp add: discovered_closed_def)
apply (blast)
done
ultimately show ?case by (simp add: discovered_closed_def)
qed (auto simp add: discovered_closed_def cond_def)

lemma i_discovered_finite: "is_invar (λs. finite (dom (discovered s)))"
by (induction rule: is_invarI) auto

end

context DFS_invar
begin

lemmas discovered_reachable =
i_discovered_reachable [THEN make_invar_thm]

lemma stack_reachable: "set (stack s) ⊆ reachable"
using stack_discovered discovered_reachable by blast

lemmas discovered_closed = i_discovered_closed[THEN make_invar_thm]

lemmas discovered_finite[simp, intro!] = i_discovered_finite[THEN make_invar_thm]
lemma finished_finite[simp, intro!]: "finite (dom (finished s))"
using finished_discovered discovered_finite by (rule finite_subset)

lemma finished_closed:
"E `` dom (finished s) ⊆ dom (discovered s)"
using discovered_closed[unfolded discovered_closed_def]
by auto

lemma finished_imp_succ_discovered:
"v ∈ dom (finished s) ⟹ w ∈ succ v ⟹ w ∈ dom (discovered s)"
using discovered_closed[unfolded discovered_closed_def]
by auto

lemma pending_reachable: "pending s ⊆ reachable × reachable"
using pendingD discovered_reachable
by (fast intro: rtrancl_image_advance_rtrancl)

lemma pending_finite[simp, intro!]: "finite (pending s)"
proof -
have "pending s ⊆ (SIGMA u:dom (discovered s). E``{u})"
by (auto dest: pendingD)
also have "finite …"
apply rule
apply (rule discovered_finite)
using discovered_reachable
by (blast intro: finitely_branching)
finally (finite_subset) show ?thesis .
qed

lemma no_pending_imp_succ_discovered:
assumes "u ∈ dom (discovered s)"
and "pending s `` {u} = {}"
and "v ∈ succ u"
shows "v ∈ dom (discovered s)"
proof (cases "u ∈ dom (finished s)")
case True with finished_imp_succ_discovered assms show ?thesis by simp
next
case False with stack_set_def assms have "u ∈ set (stack s)" by auto
with assms discovered_closed[unfolded discovered_closed_def] show ?thesis by blast
qed

lemma nc_finished_eq_reachable:
assumes NC: "¬cond s" "¬is_break param s"
shows "dom (finished s) = reachable"
proof -
from NC basic_invar
have [simp]: "stack s = []" "dom (discovered s) = dom (finished s)" and SS: "V0 ⊆ dom (discovered s)"
unfolding basic_invar_def cond_alt by auto

show "dom (finished s) = reachable"
proof
from discovered_reachable show "dom (finished s) ⊆ reachable"
by simp
next
from discovered_closed have "E``(dom (finished s)) ⊆ dom (finished s)"
unfolding discovered_closed_def by auto
with SS show "reachable ⊆ dom (finished s)"
by (simp, metis rtrancl_reachable_induct)
qed
qed

lemma nc_V0_finished:
assumes NC: "¬ cond s" "¬ is_break param s"
shows "V0 ⊆ dom (finished s)"
using nc_finished_eq_reachable[OF NC]
by blast

lemma nc_discovered_eq_finished:
assumes NC: "¬ cond s" "¬ is_break param s"
shows "dom (discovered s) = dom (finished s)"
using finished_discovered
using nc_finished_eq_reachable[OF NC] discovered_reachable
by blast

lemma nc_discovered_eq_reachable:
assumes NC: "¬ cond s" "¬ is_break param s"
shows "dom (discovered s) = reachable"
using NC
using nc_discovered_eq_finished nc_finished_eq_reachable
by blast

lemma nc_fin_closed:
assumes NC: "¬cond s"
assumes NB: "¬is_break param s"
shows "E``dom (finished s) ⊆ dom (finished s)"
using finished_imp_succ_discovered
by (auto simp: nc_discovered_eq_finished[OF NC NB])

end

subsection ‹Total Correctness›
text ‹We can show termination of the DFS algorithm, independently of the parameterization›

context param_DFS begin
definition "param_dfs_variant ≡ inv_image
(finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than)
(λs. (dom (discovered s), pending s, length (stack s)))"

lemma param_dfs_variant_wf[simp, intro!]:
assumes [simp, intro!]: "finite reachable"
shows "wf param_dfs_variant"
unfolding param_dfs_variant_def
by auto

lemma param_dfs_variant_step:
assumes A: "DFS_invar G param s" "cond s" "nofail it_dfs"
shows "step s ≤ SPEC (λs'. (s',s)∈param_dfs_variant)"
proof -
interpret DFS_invar G param s by fact

from A show ?thesis
unfolding rwof_eq_DFS_invar[symmetric] it_dfs_def
apply -
apply (drule (2) WHILE_nofail_imp_rwof_nofail)
unfolding step_def get_new_root_def do_defs get_pending_def
unfolding param_dfs_variant_def
apply refine_vcg
using discovered_reachable (* TODO: Clean, up. *)
(* FIXME: auto-steps take loooong *)
apply (auto
split: option.splits
simp: refine_pw_simps pw_le_iff is_discovered_def finite_psupset_def
) [1]
apply (auto simp: refine_pw_simps pw_le_iff is_empty_stack_def) []
apply simp_all

apply (auto
simp: refine_pw_simps pw_le_iff is_discovered_def
split: if_split_asm
) [2]

apply (clarsimp simp: refine_pw_simps pw_le_iff is_discovered_def)
using discovered_reachable pending_reachable
apply (auto
simp: is_discovered_def
simp: refine_pw_simps pw_le_iff finite_psupset_def
split: if_split_asm)
done
qed

end

context param_DFS begin
lemma it_dfsT_eq_it_dfs:
assumes [simp, intro!]: "finite reachable"
shows "it_dfsT = it_dfs"
proof -
have "it_dfs ≤ it_dfsT"
unfolding it_dfs_def it_dfsT_def WHILE_def WHILET_def
apply (rule bind_mono)
apply simp
apply (rule WHILEI_le_WHILEIT)
done
also have "it_dfsT ≤ it_dfs"
proof (cases "nofail it_dfs")
case False thus ?thesis by (simp add: not_nofail_iff)
next
case True

show ?thesis
unfolding it_dfsT_def it_dfs_def
apply (rule bind_mono)
apply simp
apply (subst WHILET_eq_WHILE_tproof[
where I="DFS_invar G param"
and V="param_dfs_variant"
])
apply auto []

apply (subst rwof_eq_DFS_invar[symmetric])
using rwof_init[OF True[unfolded it_dfs_def]]
apply (fastforce dest: order_trans) []

apply (rule SPEC_rule_conjI)
apply (rule DFS_invar_step[OF True], assumption+) []
apply (rule param_dfs_variant_step, (assumption|rule True)+) []

apply simp
done
qed
finally show ?thesis by simp
qed
end

subsection ‹Non-Failing Parameterization›
text ‹
The proofs so far have been done modulo failure of the parameterization.
In this locale, we assume that the parameterization does not fail,
and derive the correctness proof of the DFS algorithm wrt. its invariant.
›
(* Locale that assumes that parameterization does not fail *)
locale DFS =
param_DFS G param
for G :: "('v, 'more) graph_rec_scheme"
and param :: "('v,'es) parameterization"
+
assumes nofail_on_init:
"nofail (on_init param)"

assumes nofail_on_new_root:
"pre_on_new_root v0 s ⟹ nofail (on_new_root param v0 s)"

assumes nofail_on_finish:
"pre_on_finish u s ⟹ nofail (on_finish param u s)"

assumes nofail_on_cross_edge:
"pre_on_cross_edge u v s ⟹ nofail (on_cross_edge param u v s)"

assumes nofail_on_back_edge:
"pre_on_back_edge u v s ⟹ nofail (on_back_edge param u v s)"

assumes nofail_on_discover:
"pre_on_discover u v s ⟹ nofail (on_discover param u v s)"

begin
lemmas nofails = nofail_on_init nofail_on_new_root nofail_on_finish
nofail_on_cross_edge nofail_on_back_edge nofail_on_discover

lemma init_leof_invar: "init ≤⇩n SPEC (DFS_invar G param)"
unfolding rwof_eq_DFS_invar[symmetric]
by (rule rwof_leof_init)

lemma it_dfs_eq_spec: "it_dfs = SPEC (λs. DFS_invar G param s ∧ ¬cond s)"
unfolding rwof_eq_DFS_invar[symmetric] it_dfs_def
apply (rule nofail_WHILE_eq_rwof)
apply (subst WHILE_eq_I_rwof)
unfolding rwof_eq_DFS_invar
apply (rule SPEC_nofail[where Φ="λ_. True"])
apply (refine_vcg leofD[OF _ init_leof_invar, THEN weaken_SPEC])
apply (simp add: init_def refine_pw_simps nofail_on_init)
apply (rule DFS_invar_step')
apply (simp add: step_def refine_pw_simps nofail_on_init do_defs
get_pending_def get_new_root_def pred_defs
split: option.split)
apply (intro allI conjI impI nofails)
apply (auto simp add: pre_on_defs)
done

lemma it_dfs_correct: "it_dfs ≤ SPEC (λs. DFS_invar G param s ∧ ¬cond s)"
by (simp add: it_dfs_eq_spec)

lemma it_dfs_SPEC:
assumes "⋀s. ⟦DFS_invar G param s; ¬cond s⟧ ⟹ P s"
shows "it_dfs ≤ SPEC P"
using weaken_SPEC[OF it_dfs_correct]
using assms
by blast

lemma it_dfsT_correct:
assumes "finite reachable"
shows "it_dfsT ≤ SPEC (λs. DFS_invar G param s ∧ ¬cond s)"
apply (subst it_dfsT_eq_it_dfs[OF assms])
by (rule it_dfs_correct)

lemma it_dfsT_SPEC:
assumes "finite reachable"
assumes "⋀s. ⟦DFS_invar G param s; ¬cond s⟧ ⟹ P s"
shows "it_dfsT ≤ SPEC P"
apply (subst it_dfsT_eq_it_dfs[OF assms(1)])
using assms(2)
by (rule it_dfs_SPEC)

end

end
```