# Theory DFS_Framework.Simple_Impl

```section ‹Simple Data Structures›
theory Simple_Impl
imports
"../Structural/Rec_Impl"
"../Structural/Tailrec_Impl"
begin

text ‹
We provide some very basic data structures to implement the DFS state
›

subsection ‹ Stack, Pending Stack, and Visited Set ›
record 'v simple_state =
ss_stack :: "('v × 'v set) list"
on_stack :: "'v set"
visited :: "'v set"

definition [to_relAPP]: "simple_state_rel erel ≡ { (s,s') .
ss_stack s = map (λu. (u,pending s' `` {u})) (stack s') ∧
on_stack s = set (stack s') ∧
visited s = dom (discovered s') ∧
dom (finished s') = dom (discovered s') - set (stack s') ∧ ― ‹TODO: Hmm, this is an invariant of the abstract›
set (stack s') ⊆ dom (discovered s') ∧
(simple_state.more s, state.more s') ∈ erel
}"

lemma simple_state_relI:
assumes
"dom (finished s') = dom (discovered s') - set (stack s')"
"set (stack s') ⊆ dom (discovered s')"
"(m', state.more s') ∈ erel"
shows "(⦇
ss_stack = map (λu. (u,pending s' `` {u})) (stack s'),
on_stack = set (stack s'),
visited = dom (discovered s'),
… = m'
⦈, s')∈⟨erel⟩simple_state_rel"
using assms
unfolding simple_state_rel_def
by auto

lemma simple_state_more_refine[param]:
"(simple_state.more_update, state.more_update)
∈ (R → R) → ⟨R⟩simple_state_rel → ⟨R⟩simple_state_rel"
apply (clarsimp simp: simple_state_rel_def)
apply parametricity
done

text ‹ We outsource the definitions in a separate locale, as we want to re-use them
for similar implementations ›
locale pre_simple_impl = graph_defs
begin

definition "init_impl e
≡ RETURN ⦇ ss_stack = [], on_stack = {}, visited = {}, … = e ⦈"

definition "is_empty_stack_impl s ≡ (ss_stack s = [])"
definition "is_discovered_impl u s ≡ (u∈visited s)"
definition "is_finished_impl u s ≡ (u∈visited s - (on_stack s))"

definition "finish_impl u s ≡ do {
ASSERT (ss_stack s ≠ [] ∧ u∈on_stack s);
let s = s⦇ss_stack := tl (ss_stack s)⦈;
let s = s⦇on_stack := on_stack s - {u}⦈;
RETURN s
}"

definition "get_pending_impl s ≡ do {
ASSERT (ss_stack s ≠ []);
let (u,Vs) = hd (ss_stack s);
if Vs = {} then
RETURN (u,None,s)
else do {
v ← SPEC (λv. v∈Vs);
let Vs = Vs - {v};
let s = s⦇ ss_stack := (u,Vs) # tl (ss_stack s) ⦈;
RETURN (u, Some v, s)
}
}"

definition "discover_impl u v s ≡ do {
ASSERT (v∉on_stack s ∧ v∉visited s);
let s = s⦇ss_stack := (v,E``{v}) # ss_stack s⦈;
let s = s⦇on_stack := insert v (on_stack s)⦈;
let s = s⦇visited := insert v (visited s)⦈;
RETURN s
}"

definition "new_root_impl v0 s ≡ do {
ASSERT (v0∉visited s);
let s = s⦇ss_stack := [(v0,E``{v0})]⦈;
let s = s⦇on_stack := {v0}⦈;
let s = s⦇visited := insert v0 (visited s)⦈;
RETURN s
}"

definition "gbs ≡ ⦇
gbs_init = init_impl,
gbs_is_empty_stack = is_empty_stack_impl ,
gbs_new_root =  new_root_impl ,
gbs_get_pending = get_pending_impl ,
gbs_finish =  finish_impl ,
gbs_is_discovered = is_discovered_impl ,
gbs_is_finished = is_finished_impl ,
gbs_back_edge = (λu v s. RETURN s) ,
gbs_cross_edge = (λu v s. RETURN s) ,
gbs_discover = discover_impl
⦈"

lemmas gbs_simps[simp, DFS_code_unfold] = gen_basic_dfs_struct.simps[mk_record_simp, OF gbs_def]

lemmas impl_defs[DFS_code_unfold]
= init_impl_def is_empty_stack_impl_def new_root_impl_def
get_pending_impl_def finish_impl_def is_discovered_impl_def
is_finished_impl_def discover_impl_def

end

text ‹
Simple implementation of a DFS. This locale assumes a refinement of the
parameters, and provides an implementation via a stack and a visited set.
›
locale simple_impl_defs =
a: param_DFS_defs G param
+ c: pre_simple_impl
+ gen_param_dfs_refine_defs
where gbsi = c.gbs
and gbs = a.gbs
and upd_exti = simple_state.more_update
and upd_ext = state.more_update
and V0i = a.V0
and V0 = a.V0
begin

sublocale tailrec_impl_defs G c.gds .

definition "get_pending s ≡ ⋃(set (map (λ(u,Vs). {u}×Vs) (ss_stack s)))"
definition "get_stack s ≡ map fst (ss_stack s)"
definition choose_pending
:: "'v ⇒ 'v option ⇒ ('v,'d) simple_state_scheme ⇒ ('v,'d) simple_state_scheme nres"
where [DFS_code_unfold]:
"choose_pending u vo s ≡
case vo of
None ⇒ RETURN s
| Some v ⇒ do {
ASSERT (ss_stack s ≠ []);
let (u,Vs) = hd (ss_stack s);
RETURN (s⦇ ss_stack := (u,Vs-{v})#tl (ss_stack s)⦈)
}"

sublocale rec_impl_defs G c.gds get_pending get_stack choose_pending .
end

locale simple_impl =
a: param_DFS
+ simple_impl_defs
+ param_refinement
where gbsi = c.gbs
and gbs = a.gbs
and upd_exti = simple_state.more_update
and upd_ext = state.more_update
and V0i = a.V0
and V0 = a.V0
and V=Id
and S = "⟨ES⟩simple_state_rel"
begin

lemma init_impl: "(ei, e) ∈ ES ⟹
c.init_impl ei ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.empty_state e))"
unfolding c.init_impl_def a.empty_state_def simple_state_rel_def
by (auto)

lemma new_root_impl:
"⟦a.gen_dfs.pre_new_root v0 s;
(v0i, v0)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
⟹ c.new_root_impl v0 si ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.new_root v0 s))"
unfolding simple_state_rel_def a.gen_dfs.pre_new_root_def c.new_root_impl_def

lemma get_pending_impl: "
⟦a.gen_dfs.pre_get_pending s; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
⟹ c.get_pending_impl si
≤ ⇓ (Id ×⇩r Id ×⇩r ⟨ES⟩simple_state_rel) (a.get_pending s)"
apply (unfold a.get_pending_def c.get_pending_impl_def) []
apply (refine_rcg bind_refine' Let_refine' IdI)
apply (refine_dref_type)
apply (auto
simp: simple_state_rel_def a.gen_dfs.pre_defs a.pred_defs neq_Nil_conv
dest: DFS_invar.stack_distinct
)
done

lemma inres_get_pending_None_conv: "inres (a.get_pending s0) (v, None, s)
⟷ s=s0 ∧ v=hd (stack s0) ∧ pending s0``{hd (stack s0)} = {}"
unfolding a.get_pending_def

lemma inres_get_pending_Some_conv: "inres (a.get_pending s0) (v,Some Vs,s)
⟷ v = hd (stack s) ∧ s = s0⦇pending := pending s0 - {(hd (stack s0), Vs)}⦈
∧ (hd (stack s0), Vs) ∈ pending s0"
unfolding a.get_pending_def

lemma finish_impl:
"⟦a.gen_dfs.pre_finish v s0 s; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
⟹ c.finish_impl v si ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.finish v s))"
unfolding simple_state_rel_def a.gen_dfs.pre_defs c.finish_impl_def

(* Proof is fine-tuned to optimize speed *)
apply (clarsimp simp: inres_get_pending_None_conv)
apply (frule DFS_invar.stack_distinct)
apply (clarsimp simp: neq_Nil_conv)
apply blast
done

lemma cross_edge_impl: "
⟦a.gen_dfs.pre_cross_edge u v s0 s;
(ui, u)∈Id; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
⟹ (si, a.cross_edge u v s) ∈ ⟨ES⟩simple_state_rel"
unfolding simple_state_rel_def a.gen_dfs.pre_defs
by simp

lemma back_edge_impl: "
⟦a.gen_dfs.pre_back_edge u v s0 s;
(ui, u)∈Id; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
⟹ (si, a.back_edge u v s) ∈ ⟨ES⟩simple_state_rel"
unfolding simple_state_rel_def a.gen_dfs.pre_defs
by simp

lemma discover_impl:
"⟦a.gen_dfs.pre_discover u v s0 s; (ui, u)∈Id; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
⟹ c.discover_impl ui vi si ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.discover u v s))"
unfolding simple_state_rel_def a.gen_dfs.pre_defs c.discover_impl_def
apply (rule ASSERT_leI)
apply (clarsimp simp: inres_get_pending_Some_conv)
apply (frule DFS_invar.stack_discovered)
apply (auto simp: a.pred_defs) []

apply (clarsimp simp: inres_get_pending_Some_conv)
apply (frule DFS_invar.stack_discovered)
apply (frule DFS_invar.pending_ssE)
apply (clarsimp simp: a.pred_defs)
apply blast
done

sublocale gen_param_dfs_refine
where gbsi = c.gbs
and gbs = a.gbs
and upd_exti = simple_state.more_update
and upd_ext = state.more_update
and V0i = a.V0
and V0 = a.V0
and V = Id
and S = "⟨ES⟩simple_state_rel"
apply unfold_locales
apply (simp_all add: is_break_param) (* TODO: Strange effect,
the is_break_param subgoal should not be visible at all!*)

apply (auto simp: a.is_discovered_def c.is_discovered_impl_def simple_state_rel_def) []

apply (auto simp: a.is_finished_def c.is_finished_impl_def simple_state_rel_def) []

apply (auto simp: a.is_empty_stack_def c.is_empty_stack_impl_def simple_state_rel_def) []

apply (refine_rcg init_impl)

apply (refine_rcg new_root_impl, simp_all) []

apply (refine_rcg get_pending_impl) []

apply (refine_rcg finish_impl, simp_all) []

apply (refine_rcg cross_edge_impl, simp_all) []

apply (refine_rcg back_edge_impl, simp_all) []

apply (refine_rcg discover_impl, simp_all) []
done

text ‹ Main outcome of this locale: The simple DFS-Algorithm, which is
a general DFS scheme itself (and thus open to further refinements),
and a refinement theorem that states correct refinement of the original DFS ›

lemma simple_refine[refine]: "c.gen_dfs ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfs"
using gen_dfs_refine
by simp

lemma simple_refineT[refine]: "c.gen_dfsT ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfsT"
using gen_dfsT_refine
by simp

sublocale tailrec_impl G c.gds
apply unfold_locales
apply (auto simp: pw_leof_iff refine_pw_simps split: prod.splits)
done

lemma simple_tailrec_refine[refine]: "tailrec_impl ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfs"
proof -
note tailrec_impl also note simple_refine finally show ?thesis .
qed

lemma simple_tailrecT_refine[refine]: "tailrec_implT ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfsT"
proof -
note tailrecT_impl also note simple_refineT finally show ?thesis .
qed

(* TODO: Currently, we have to prove this invar at several places.
Maybe it's worth to share in a common locale!?
*)
lemma reachable_invar:
assumes "c.gen_rwof s"
shows "set (map fst (ss_stack s)) ⊆ visited s
∧ distinct (map fst (ss_stack s))"
using assms
apply (induct rule: establish_rwof_invar[rotated -1, consumes 1])
apply (refine_rcg refine_vcg)
apply simp

unfolding c.gen_step_def c.do_action_defs c.impl_defs[abs_def] c.gds_simps c.gbs_simps
apply (refine_rcg refine_vcg)
apply simp_all
apply (fastforce simp: neq_Nil_conv) []
apply (fastforce simp: neq_Nil_conv) []
apply (fastforce simp: neq_Nil_conv) []
apply (fastforce simp: neq_Nil_conv) []
done

sublocale rec_impl G c.gds get_pending get_stack choose_pending
apply unfold_locales
unfolding get_pending_def get_stack_def choose_pending_def
apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def
split: prod.split) []
apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def
split: prod.split) []

apply (rule le_ASSERTI)
apply (unfold c.pre_defs, clarify) []
apply (frule reachable_invar)

apply (fastforce simp add: pw_leof_iff refine_pw_simps pw_le_iff neq_Nil_conv
split: prod.split option.split) []

apply (unfold c.pre_defs, clarify) []
apply (frule reachable_invar)
apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def c.impl_defs neq_Nil_conv
split: prod.split option.split) []

apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def neq_Nil_conv c.pre_defs c.impl_defs
split: prod.split if_split_asm) []

apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff split: prod.split) []

apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff split: prod.split) []

apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff split: prod.split) []
done

lemma simple_rec_refine[refine]: "rec_impl ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfs"
proof -
note rec_impl also note simple_refine finally show ?thesis .
qed

end

text ‹ Autoref Setup ›

record ('si,'nsi)simple_state_impl =
ss_stack_impl :: 'si
ss_on_stack_impl :: 'nsi
ss_visited_impl :: 'nsi

definition [to_relAPP]: "ss_impl_rel s_rel vis_rel erel ≡
{(⦇ss_stack_impl = si, ss_on_stack_impl = osi, ss_visited_impl = visi, … = mi⦈,
⦇ss_stack = s, on_stack = os, visited = vis, … = m⦈) |
si osi visi mi s os vis m.
(si, s) ∈ s_rel ∧
(osi, os) ∈ vis_rel ∧
(visi, vis) ∈ vis_rel ∧
(mi, m) ∈ erel
}"

consts
i_simple_state :: "interface ⇒ interface ⇒ interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of ss_impl_rel i_simple_state]

term simple_state_ext

lemma [autoref_rules, param]:
fixes s_rel ps_rel vis_rel erel
defines "R ≡ ⟨s_rel,vis_rel,erel⟩ss_impl_rel"
shows
"(ss_stack_impl, ss_stack) ∈  R → s_rel"
"(ss_on_stack_impl, on_stack) ∈  R → vis_rel"
"(ss_visited_impl, visited) ∈ R → vis_rel"
"(simple_state_impl.more, simple_state.more) ∈ R → erel"
"(ss_stack_impl_update, ss_stack_update) ∈ (s_rel → s_rel) → R → R"
"(ss_on_stack_impl_update, on_stack_update) ∈ (vis_rel → vis_rel) → R → R"
"(ss_visited_impl_update, visited_update) ∈ (vis_rel → vis_rel) → R → R"
"(simple_state_impl.more_update, simple_state.more_update) ∈ (erel → erel) → R → R"
"(simple_state_impl_ext, simple_state_ext) ∈ s_rel → vis_rel → vis_rel → erel → R"
unfolding ss_impl_rel_def R_def
apply auto
apply parametricity+
done

subsection ‹ Simple state without on-stack ›
text ‹ We can further refine the simple implementation and drop the on-stack set ›
record ('si,'nsi)simple_state_nos_impl =
ssnos_stack_impl :: 'si
ssnos_visited_impl :: 'nsi

definition [to_relAPP]: "ssnos_impl_rel s_rel vis_rel erel ≡
{(⦇ssnos_stack_impl = si, ssnos_visited_impl = visi, … = mi⦈,
⦇ss_stack = s, on_stack = os, visited = vis, … = m⦈) |
si visi mi s os vis m.
(si, s) ∈ s_rel ∧
(visi, vis) ∈ vis_rel ∧
(mi, m) ∈ erel
}"

lemmas [autoref_rel_intf] = REL_INTFI[of ssnos_impl_rel i_simple_state]

definition op_nos_on_stack_update
:: "(_ set ⇒ _ set) ⇒ (_,_)simple_state_scheme ⇒ _"
where "op_nos_on_stack_update ≡ on_stack_update"

context begin interpretation autoref_syn .
lemma [autoref_op_pat_def]: "op_nos_on_stack_update f s
≡ OP (op_nos_on_stack_update f)\$s" by simp

end

lemmas ssnos_unfolds ― ‹To be unfolded before autoref when using @{term ssnos_impl_rel}›
= op_nos_on_stack_update_def[symmetric]

lemma [autoref_rules, param]:
fixes s_rel vis_rel erel
defines "R ≡ ⟨s_rel,vis_rel,erel⟩ssnos_impl_rel"
shows
"(ssnos_stack_impl, ss_stack) ∈  R → s_rel"
"(ssnos_visited_impl, visited) ∈ R → vis_rel"
"(simple_state_nos_impl.more, simple_state.more) ∈ R → erel"
"(ssnos_stack_impl_update, ss_stack_update) ∈ (s_rel → s_rel) → R → R"
"(λx. x, op_nos_on_stack_update f) ∈ R → R"
"(ssnos_visited_impl_update, visited_update) ∈ (vis_rel → vis_rel) → R → R"
"(simple_state_nos_impl.more_update, simple_state.more_update) ∈ (erel → erel) → R → R"
"(λns _ ps vs. simple_state_nos_impl_ext ns ps vs, simple_state_ext)
∈ s_rel → ANY_rel → vis_rel → erel → R"
unfolding ssnos_impl_rel_def R_def op_nos_on_stack_update_def
apply auto
apply parametricity+
done

subsection ‹Simple state without stack and on-stack›
text ‹Even further refinement yields an implementation without a stack.
Note that this only works for structural implementations that provide their own
stack (e.g., recursive)!›
record ('si,'nsi)simple_state_ns_impl =
ssns_visited_impl :: 'nsi

definition [to_relAPP]: "ssns_impl_rel (R::('a×'b) set) vis_rel erel ≡
{(⦇ssns_visited_impl = visi, … = mi⦈,
⦇ss_stack = s, on_stack = os, visited = vis, … = m⦈) |
visi mi s os vis m.
(visi, vis) ∈ vis_rel ∧
(mi, m) ∈ erel
}"

lemmas [autoref_rel_intf] = REL_INTFI[of ssns_impl_rel i_simple_state]

definition op_ns_on_stack_update
:: "(_ set ⇒ _ set) ⇒ (_,_)simple_state_scheme ⇒ _"
where "op_ns_on_stack_update ≡ on_stack_update"

definition op_ns_stack_update
:: "(_ list ⇒ _ list) ⇒ (_,_)simple_state_scheme ⇒ _"
where "op_ns_stack_update ≡ ss_stack_update"

context begin interpretation autoref_syn .
lemma [autoref_op_pat_def]: "op_ns_on_stack_update f s
≡ OP (op_ns_on_stack_update f)\$s" by simp

lemma [autoref_op_pat_def]: "op_ns_stack_update f s
≡ OP (op_ns_stack_update f)\$s" by simp

end

context simple_impl_defs begin
thm choose_pending_def[unfolded op_ns_stack_update_def[symmetric], no_vars]

lemma choose_pending_ns_unfold: "choose_pending u vo s = (
case vo of None ⇒ RETURN s
| Some v ⇒ do {
_ ← ASSERT (ss_stack s ≠ []);
RETURN
(op_ns_stack_update
( let
(u, Vs) = hd (ss_stack s)
in (λ_. (u, Vs - {v}) # tl (ss_stack s))
)
s
)
})"
unfolding choose_pending_def op_ns_stack_update_def
by (auto split: option.split prod.split)

lemmas ssns_unfolds ― ‹To be unfolded before autoref when using @{term ssns_impl_rel}.
Attention: This lemma conflicts with the standard unfolding lemma in
@{text DFS_code_unfold}, so has to be placed first in an unfold-statement!›
= op_ns_on_stack_update_def[symmetric] op_ns_stack_update_def[symmetric]
choose_pending_ns_unfold

end

lemma [autoref_rules, param]:
fixes s_rel vis_rel erel ANY_rel
defines "R ≡ ⟨ANY_rel,vis_rel,erel⟩ssns_impl_rel"
shows
"(ssns_visited_impl, visited) ∈ R → vis_rel"
"(simple_state_ns_impl.more, simple_state.more) ∈ R → erel"
"⋀f. (λx. x, op_ns_stack_update f) ∈ R → R"
"⋀f. (λx. x, op_ns_on_stack_update f) ∈ R → R"
"(ssns_visited_impl_update, visited_update) ∈ (vis_rel → vis_rel) → R → R"
"(simple_state_ns_impl.more_update, simple_state.more_update) ∈ (erel → erel) → R → R"
"(λ_ _ ps vs. simple_state_ns_impl_ext ps vs, simple_state_ext)
∈ ANY1_rel → ANY2_rel → vis_rel → erel → R"
unfolding ssns_impl_rel_def R_def op_ns_on_stack_update_def op_ns_stack_update_def
apply auto
apply parametricity+
done

lemma [refine_transfer_post_simp]:
"⋀a m. a⦇simple_state_nos_impl.more := m::unit⦈ = a"
"⋀a m. a⦇simple_state_impl.more := m::unit⦈ = a"
"⋀a m. a⦇simple_state_ns_impl.more := m::unit⦈ = a"
by auto

end

```