# Theory Cyc_Check

section ‹Simple Cyclicity Checker›
theory Cyc_Check
imports "../DFS_Framework"
CAVA_Automata.Digraph_Impl
"../Misc/Impl_Rev_Array_Stack"
begin
text ‹
This example presents a simple cyclicity checker:
Given a directed graph with start nodes, decide whether it's reachable
part is cyclic.
The example tries to be a tutorial on using the DFS framework,
explaining every required step in detail.
We define two versions of the algorithm, a partial correct one assuming
only a finitely branching graph, and a total correct one assuming finitely
many reachable nodes.
›
subsection ‹Framework Instantiation›
text ‹ Define a state, based on the DFS-state.
In our case, we just add a break-flag.
›
record 'v cycc_state = "'v state" +
break :: bool
text ‹Some utility lemmas for the simplifier, to handle idiosyncrasies of
the record package. ›
lemma break_more_cong: "state.more s = state.more s' ⟹ break s = break s'"
by (cases s, cases s', simp)
lemma [simp]: "s⦇ state.more := ⦇ break = foo ⦈ ⦈ = s ⦇ break := foo ⦈"
by (cases s) simp
text ‹
Define the parameterization. We start at a default parameterization, where
all operations default to skip, and just add the operations we are
interested in: Initially, the break flag is false, it is set if we
encounter a back-edge, and once set, the algorithm shall terminate immediately. ›
definition cycc_params :: "('v,unit cycc_state_ext) parameterization"
where "cycc_params ≡ dflt_parametrization state.more
(RETURN ⦇ break = False ⦈) ⦇
on_back_edge := λ_ _ _. RETURN ⦇ break = True ⦈,
is_break := break ⦈"
lemmas cycc_params_simp[simp] =
gen_parameterization.simps[mk_record_simp, OF cycc_params_def[simplified]]