# Theory DFS_Framework.Restr_Impl

```section ‹Restricting Nodes by Pre-Initializing Visited Set›
theory Restr_Impl
imports Simple_Impl
begin
text ‹
Implementation of node and edge restriction via pre-initialized visited set.

We now further refine the simple implementation in case that the graph has
the form ‹G'=(rel_restrict E R, V0-R)› for some ‹fb_graph G=(E,V0)›.
If, additionally, the parameterization is not "too sensitive" to the
visited set, we can pre-initialize the visited set with ‹R›, and use the
‹V0› and ‹E› of ‹G›. This may be a more efficient implementation
than explicitely
restricting ‹V0› and ‹E›, as it saves additional membership queries in ‹R›
on each successor function call.

Moreover, in applications where the restriction is updated between multiple
calls, we can use one linearly accessed restriction set.
›

definition "restr_rel R ≡ { (s,s').
(ss_stack s, ss_stack s')∈⟨Id ×⇩r {(U,U'). U-R = U'}⟩list_rel
∧ on_stack s = on_stack s'
∧ visited s = visited s' ∪ R ∧ visited s' ∩ R = {}
∧ simple_state.more s = simple_state.more s' }"

lemma restr_rel_simps:
assumes "(s,s')∈restr_rel R"
shows "visited s = visited s' ∪ R"
and "simple_state.more s = simple_state.more s'"
using assms unfolding restr_rel_def by auto

lemma
assumes "(s,s')∈restr_rel R"
shows restr_rel_stackD: "(ss_stack s, ss_stack s') ∈ ⟨Id ×⇩r {(U,U'). U-R = U'}⟩list_rel"
and restr_rel_vis_djD: "visited s' ∩ R = {}"
using assms unfolding restr_rel_def by auto

context fixes R :: "'v set" begin
definition [to_relAPP]: "restr_simple_state_rel ES ≡ { (s,s') .
(ss_stack s, map (λu. (u,pending s' `` {u})) (stack s'))
∈ ⟨Id ×⇩r {(U,U'). U-R = U'}⟩list_rel ∧
on_stack s = set (stack s') ∧
visited s = dom (discovered s') ∪ R ∧ dom (discovered s') ∩ R = {} ∧
dom (finished s') = dom (discovered s') - set (stack s') ∧
set (stack s') ⊆ dom (discovered s') ∧
(simple_state.more s, state.more s') ∈ ES
}"
end

lemma restr_simple_state_rel_combine:
"⟨ES⟩restr_simple_state_rel R = restr_rel R O ⟨ES⟩simple_state_rel"
unfolding restr_simple_state_rel_def
apply (intro equalityI subsetI)
apply clarify
apply (rule relcompI[OF _ simple_state_relI], auto simp: restr_rel_def) []

apply (auto simp: restr_rel_def simple_state_rel_def) []
done

text ‹
Locale that assumes a simple implementation, makes some
additional assumptions on the parameterization (intuitively, that it
is not too sensitive to adding nodes from R to the visited set), and then
provides a new implementation with pre-initialized visited set.
›
(*
TODO/FIXME: The refinement step from simple_impl is not yet clean,
as the parameterizatioin refinement is not handled properly.
Ideally, one would assume the required parameterization refinement
w.r.t. restr_simple_state_rel, and derive the refinement for
simple_state_rel.

*)

locale restricted_impl_defs =
graph_defs G +
a: simple_impl_defs "graph_restrict G R"
for G :: "('v, 'more) graph_rec_scheme"
and R
begin
sublocale pre_simple_impl G .

abbreviation "rel ≡ restr_rel R"

definition "gbs' ≡ gbs ⦇
gbs_init := λe. RETURN
⦇ ss_stack=[], on_stack={}, visited = R, …=e ⦈ ⦈"

lemmas gbs'_simps[simp, DFS_code_unfold]
= gen_basic_dfs_struct.simps[mk_record_simp, OF gbs'_def[unfolded gbs_simps]]

sublocale gen_param_dfs_defs gbs' parami simple_state.more_update V0 .

(* Seems to be fixed in Isabelle-2016
(* Some ad-hoc fix for locale abbreviations not being properly printed *)
abbreviation (output) "abbrev_gen_dfs ≡ gen_dfs"
abbreviation (output) "abbrev__gen_cond ≡ gen_cond"
abbreviation (output) "abbrev__gen_step ≡ gen_step"

abbreviation (output) "abbrev__ac_gen_dfs ≡ a.c.gen_dfs"
abbreviation (output) "abbrev__ac_gen_cond ≡ a.c.gen_cond"
abbreviation (output) "abbrev__ac_gen_step ≡ a.c.gen_step"

abbreviation "abbrev_do_new_root ≡ do_new_root"
abbreviation "abbrev_do_cross_edge ≡ do_cross_edge"
abbreviation "abbrev_do_back_edge ≡ do_back_edge"
abbreviation "abbrev_do_discover ≡ do_discover"
abbreviation "abbrev_do_finish ≡ do_finish"

abbreviation "abbrev_ac_do_new_root ≡ a.c.do_new_root"
abbreviation "abbrev_ac_do_cross_edge ≡ a.c.do_cross_edge"
abbreviation "abbrev_ac_do_back_edge ≡ a.c.do_back_edge"
abbreviation "abbrev_ac_do_discover ≡ a.c.do_discover"
abbreviation "abbrev_ac_do_finish ≡ a.c.do_finish"
*)

sublocale tailrec_impl_defs G gds .
end

locale restricted_impl =
fb_graph +
a: simple_impl "graph_restrict G R" +
restricted_impl_defs +

(* Cross and back edges must not cause any effect.
Intuitively, we will see spurious cross edges to nodes from R.
TODO/FIXME: The condition here is a quite crude over-approximation!
*)
assumes [simp]: "on_cross_edge parami = (λu v s. RETURN (simple_state.more s))"
assumes [simp]: "on_back_edge parami = (λu v s. RETURN (simple_state.more s))"

(* TODO/FIXME: The next 4 are crude approximations. One should include
some precondition! *)
assumes is_break_refine:
"⟦ (s,s')∈restr_rel R ⟧
⟹ is_break parami s ⟷ is_break parami s'"

assumes on_new_root_refine:
"⟦ (s,s')∈restr_rel R ⟧
⟹ on_new_root parami v0 s ≤ on_new_root parami v0 s'"

assumes on_finish_refine:
"⟦ (s,s')∈restr_rel R ⟧
⟹ on_finish parami u s ≤ on_finish parami u s'"

assumes on_discover_refine:
"⟦ (s,s')∈restr_rel R ⟧
⟹ on_discover parami u v s ≤ on_discover parami u v s'"

begin

lemmas rel_def = restr_rel_def[where R=R]
sublocale gen_param_dfs gbs' parami simple_state.more_update V0 .

lemma is_break_param'[param]: "(is_break parami, is_break parami)∈rel → bool_rel"
using is_break_refine unfolding rel_def by auto

lemma do_init_refine[refine]: "do_init ≤ ⇓ rel (a.c.do_init)"
unfolding do_action_defs a.c.do_action_defs
apply refine_rcg
apply simp
done

lemma gen_cond_param: "(gen_cond,a.c.gen_cond)∈rel → bool_rel"
apply (clarsimp simp del: graph_restrict_simps)
apply (frule is_break_param'[param_fo])
unfolding gen_cond_def a.c.gen_cond_def rel_def
apply simp
unfolding a.c.is_discovered_impl_def a.c.is_empty_stack_impl_def
by auto

lemma cross_back_id[simp]:
"do_cross_edge u v s = RETURN s"
"do_back_edge u v s = RETURN s"
"a.c.do_cross_edge u v s = RETURN s"
"a.c.do_back_edge u v s = RETURN s"
unfolding do_action_defs a.c.do_action_defs
by simp_all

lemma pred_rel_simps:
assumes "(s,s')∈rel"
shows "a.c.is_discovered_impl u s ⟷ a.c.is_discovered_impl u s' ∨ u∈R"
and "a.c.is_empty_stack_impl s ⟷ a.c.is_empty_stack_impl s'"
using assms
unfolding a.c.is_discovered_impl_def a.c.is_empty_stack_impl_def
unfolding rel_def
by auto

lemma no_pending_refine:
assumes "(s,s')∈rel" "¬a.c.is_empty_stack_impl s'"
shows "(hd (ss_stack s) = (u,{})) ⟹ hd (ss_stack s') = (u,{})"
using assms
unfolding a.c.is_empty_stack_impl_def rel_def
apply (cases "ss_stack s'", simp)
apply (auto elim: list_relE)
done

lemma do_new_root_refine[refine]:
"⟦ (v0i,v0)∈Id; (si,s)∈rel; v0∉R ⟧
⟹ do_new_root v0i si ≤ ⇓ rel (a.c.do_new_root v0 s)"
unfolding do_action_defs a.c.do_action_defs
apply refine_rcg
apply (rule intro_prgR[where R=rel])
apply (refine_rcg,auto simp: rel_def rel_restrict_def) []

apply (rule intro_prgR[where R=Id])
done

lemma do_finish_refine[refine]:
"⟦(s, s') ∈ rel; (u,u')∈Id⟧
⟹ do_finish u s ≤ ⇓ rel (a.c.do_finish u' s')"
unfolding do_action_defs a.c.do_action_defs
apply refine_rcg
apply (rule intro_prgR[where R=rel])
apply (refine_rcg,auto simp: rel_def rel_restrict_def) []
apply parametricity

apply (rule intro_prgR[where R=Id])
done

lemma aux_cnv_pending:
"⟦ (s, s') ∈ rel;
¬ is_empty_stack_impl s; vs∈Vs; vs∉R;
hd (ss_stack s) = (u,Vs) ⟧ ⟹
hd (ss_stack s') = (u,insert vs (Vs-R))"
(* Conc-Pending node that is also in abs-visited is also abs-pending *)
unfolding rel_def is_empty_stack_impl_def
apply (cases "ss_stack s'", simp)
apply (auto elim: list_relE)
done

lemma get_pending_refine:
assumes "(s, s') ∈ rel" "gen_cond s" "¬ is_empty_stack_impl s"
shows "
get_pending_impl s ≤ (sup
(⇓(Id ×⇩r ⟨Id⟩option_rel ×⇩r rel) (inf
(get_pending_impl s')
(SPEC (λ(_,Vs,_). case Vs of None ⇒ True | Some v ⇒ v∉R))))
(⇓(Id ×⇩r ⟨Id⟩option_rel ×⇩r rel) (
SPEC (λ(u,Vs,s''). ∃v. Vs=Some v ∧ v∈R ∧ s''=s')
)))"
proof -
from assms have
[simp]: "ss_stack s' ≠ []"
and [simp]: "ss_stack s ≠ []"
unfolding rel_def impl_defs
apply (auto)
done

from assms show ?thesis
unfolding get_pending_impl_def
apply (subst Let_def, subst Let_def)
apply (rule ASSERT_leI)
apply (auto simp: impl_defs gen_cond_def rel_def) []

apply (split prod.split, intro allI impI)
apply (rule lhs_step_If)
(* No pending *)
apply (rule le_supI1)
apply (simp add: pred_rel_simps no_pending_refine restr_rel_simps
RETURN_RES_refine_iff)

(* Pending *)
apply (rule lhs_step_bind, simp)
apply (simp split del: if_split)
apply (rename_tac v)
apply (case_tac "v∈R")
(* Spurious node from R *)
apply (rule le_supI2)
apply (rule RETURN_SPEC_refine)
apply (auto simp: rel_def is_empty_stack_impl_def neq_Nil_conv) []
apply (cases "ss_stack s'", simp) apply (auto elim!: list_relE) []

(* Non-spurious node *)
apply (rule le_supI1)
apply (frule (4) aux_cnv_pending)
apply (simp add: no_pending_refine pred_rel_simps memb_imp_not_empty)
apply (subst nofail_inf_serialize,
(simp_all add: refine_pw_simps split: prod.splits) [2])
apply simp
apply (rule rhs_step_bind_RES, blast)
apply (simp add: rel_def is_empty_stack_impl_def) []
apply (cases "ss_stack s'", simp)
apply (auto elim: list_relE) []
done
qed

lemma do_discover_refine[refine]:
"⟦ (s, s') ∈ rel; (u,u')∈Id; (v,v')∈Id; v' ∉ R ⟧
⟹ do_discover u v s ≤ ⇓ rel (a.c.do_discover u' v' s')"
unfolding do_action_defs a.c.do_action_defs
apply refine_rcg
apply (rule intro_prgR[where R=rel])
apply (refine_rcg,auto simp: rel_def rel_restrict_def) []

apply (rule intro_prgR[where R=Id])

apply (auto simp: rel_def) []
done

lemma aux_R_node_discovered: "⟦(s,s')∈rel; v∈R⟧ ⟹ is_discovered_impl v s"
by (auto simp: pred_rel_simps)

lemma re_refine_aux: "gen_dfs ≤ ⇓rel a.c.gen_dfs"
unfolding a.c.gen_dfs_def gen_dfs_def
apply (simp del: graph_restrict_simps)
(* Some manual refinements for finer control *)
apply (rule bind_refine)
apply (refine_rcg)
apply (erule WHILE_invisible_refine)

(* Condition *)
apply (frule gen_cond_param[param_fo], fastforce)

(* Step *)
apply (frule (1) gen_cond_param[param_fo, THEN IdD, THEN iffD1])
apply (simp del: graph_restrict_simps)
unfolding gen_step_def
apply (simp del: graph_restrict_simps cong: if_cong option.case_cong split del: if_split)
apply (rule lhs_step_If)
(* new_root *)
apply (frule (1) pred_rel_simps[THEN iffD1])
apply (rule le_supI1)
apply (simp add: a.c.gen_step_def del: graph_restrict_simps)
apply refine_rcg
apply (auto simp: pred_rel_simps) [2]

(* pending edges *)
apply (frule (1) pred_rel_simps[THEN Not_eq_iff[symmetric, THEN iffD1], THEN iffD1])
thm order_trans[OF bind_mono(1)[OF get_pending_refine order_refl]]
apply (rule order_trans[OF bind_mono(1)[OF get_pending_refine order_refl]])
apply assumption+

apply (unfold bind_distrib_sup1)
apply (rule sup_least)
(* Non-spurious node *)
apply (rule le_supI1)
apply (simp add: a.c.gen_step_def del: graph_restrict_simps cong: option.case_cong if_cong)
apply (rule bind_refine'[OF conc_fun_mono[THEN monoD]], simp)
apply (clarsimp simp: refine_pw_simps)
apply (refine_rcg, refine_dref_type, simp_all add: pred_rel_simps) []

(* Spurious node *)
apply (rule le_supI2)
apply (rule RETURN_as_SPEC_refine)
apply (refine_rcg refine_vcg bind_refine', simp_all) []
apply (clarsimp)
apply (frule (1) aux_R_node_discovered, blast)
done

theorem re_refine_aux2: "gen_dfs ≤⇓(rel O ⟨ES⟩simple_state_rel) a.a.it_dfs"
proof -
note re_refine_aux
also note a.gen_dfs_refine
finally show ?thesis by (simp add: conc_fun_chain del: graph_restrict_simps)
qed

theorem re_refine: "gen_dfs ≤⇓(⟨ES⟩restr_simple_state_rel R) a.a.it_dfs"
unfolding restr_simple_state_rel_combine
by (rule re_refine_aux2)

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

lemma tailrec_refine: "tailrec_impl ≤ ⇓(⟨ES⟩restr_simple_state_rel R) a.a.it_dfs"
proof -
note tailrec_impl also note re_refine finally show ?thesis .
qed

(* TODO: Link to rec_impl *)
end

end

```