# Theory DFS_Find_Path

section ‹Finding a Path between Nodes›
theory DFS_Find_Path
imports
"../DFS_Framework"
CAVA_Automata.Digraph_Impl
"../Misc/Impl_Rev_Array_Stack"
begin
text ‹
We instantiate the DFS framework to find a path to some reachable node
that satisfies a given predicate. We present four variants of the algorithm:
Finding any path, and finding path of at least length one, combined with
searching the whole graph, and searching the graph restricted to a given set
of nodes. The restricted variants are efficiently implemented by
pre-initializing the visited set (cf. @{theory DFS_Framework.Restr_Impl}).
The restricted variants can be used for incremental search, ignoring already
searched nodes in further searches. This is required, e.g., for the inner
search of nested DFS (Buchi automaton emptiness check).
›
subsection ‹Including empty Path›
record 'v fp0_state = "'v state" +
ppath :: "('v list × 'v) option"
type_synonym 'v fp0_param = "('v, ('v,unit) fp0_state_ext) parameterization"
lemma [simp]: "s⦇ state.more := ⦇ ppath = foo ⦈ ⦈ = s ⦇ ppath := foo ⦈"
by (cases s) simp
abbreviation "no_path ≡ ⦇ ppath = None ⦈"
abbreviation "a_path p v ≡ ⦇ ppath = Some (p,v) ⦈"
definition fp0_params :: "('v ⇒ bool) ⇒ 'v fp0_param"
where "fp0_params P ≡ ⦇
on_init = RETURN no_path,
on_new_root = λv0 s. if P v0 then RETURN (a_path [] v0) else RETURN no_path,
on_discover = λu v s. if P v
then
RETURN (a_path (rev (tl (stack s))) v)
else RETURN no_path,
on_finish = λu s. RETURN (state.more s),
on_back_edge = λu v s. RETURN (state.more s),
on_cross_edge = λu v s. RETURN (state.more s),
is_break = λs. ppath s ≠ None ⦈"
lemmas fp0_params_simps[simp]
= gen_parameterization.simps[mk_record_simp, OF fp0_params_def]