# Theory Feedback_Arcs

```section ‹Find a Feedback Arc Set›
theory Feedback_Arcs
imports
"../DFS_Framework"
CAVA_Automata.Digraph_Impl
Reachable_Nodes
begin
text ‹A feedback arc set is a set of edges that breaks all reachable cycles.
In this theory, we define an algorithm to find a feedback arc set.›
definition is_fas :: "('v, 'more) graph_rec_scheme ⇒ 'v rel ⇒ bool" where
"is_fas G EC ≡ ¬(∃ u ∈ (g_E G)⇧* `` g_V0 G. (u, u) ∈ (g_E G - EC)⇧+)"

lemma is_fas_alt:
"is_fas G EC = acyclic ((g_E G ∩ ((g_E G)⇧* `` g_V0 G × UNIV) - EC))"
unfolding is_fas_def acyclic_def
proof (clarsimp, safe)
fix u
assume A: "(u,u) ∈ (g_E G ∩ (g_E G)⇧* `` g_V0 G × UNIV - EC)⇧+"
hence "(u,u)∈(g_E G - EC)⇧+" by (rule trancl_mono) blast
moreover from A have "u ∈ (g_E G)⇧* `` g_V0 G" by (cases rule: converse_tranclE) auto
moreover assume "∀u∈(g_E G)⇧* `` g_V0 G. (u, u) ∉ (g_E G - EC)⇧+"
ultimately show False by blast
next
fix u v0
assume 1: "v0∈g_V0 G" and 2: "(v0,u)∈(g_E G)⇧*" and 3: "(u,u)∈(g_E G - EC)⇧+"
have "(u, u) ∈ (Restr (g_E G - EC) ((g_E G)⇧* `` g_V0 G))⇧+"
apply (rule trancl_restrict_reachable[OF 3, where S="(g_E G)⇧* `` g_V0 G"])
apply (rule order_trans[OF _ rtrancl_image_unfold_right])
using 1 2 by auto
hence "(u, u) ∈ (g_E G ∩ (g_E G)⇧* `` g_V0 G × UNIV - EC)⇧+"
by (rule trancl_mono) auto
moreover assume "∀x. (x, x) ∉ (g_E G ∩ (g_E G)⇧* `` g_V0 G × UNIV - EC)⇧+"
ultimately show False by blast
qed

subsection ‹Instantiation of the DFS-Framework›
record 'v fas_state = "'v state" +
fas :: "('v×'v) set"

(* Some utility lemmas for the simplifier, to handle idiosyncrasies of
the record package. *)
lemma fas_more_cong: "state.more s = state.more s' ⟹ fas s = fas s'"
by (cases s, cases s', simp)

lemma [simp]: "s⦇ state.more := ⦇ fas = foo ⦈ ⦈ = s ⦇ fas := foo ⦈"
by (cases s) simp

definition fas_params :: "('v,('v,unit) fas_state_ext) parameterization"
where "fas_params ≡ dflt_parametrization state.more
(RETURN ⦇ fas = {} ⦈) ⦇
on_back_edge := λu v s. RETURN ⦇ fas = insert (u,v) (fas s) ⦈
⦈"
lemmas fas_params_simp[simp] =
gen_parameterization.simps[mk_record_simp, OF fas_params_def[simplified]]

interpretation fas: param_DFS_defs where param=fas_params for G .

text ‹ Find feedback arc set ›
definition "find_fas G ≡ do {
ASSERT (graph G);
ASSERT (finite ((g_E G)⇧* `` g_V0 G));
s ← fas.it_dfsT TYPE('a) G;
RETURN (fas_state.fas s)
}"

locale fas =
param_DFS G fas_params
for G :: "('v, 'more) graph_rec_scheme"
+
assumes finite_reachable[simp, intro!]: "finite ((g_E G)⇧* `` g_V0 G)"
begin

sublocale DFS G fas_params
apply unfold_locales
done

end

lemma fasI:
assumes "graph G"
assumes "finite ((g_E G)⇧* `` g_V0 G)"
shows "fas G"
proof -
interpret graph G by fact
interpret fb_graph G by (rule fb_graphI_fr[OF assms(2)])
show ?thesis by unfold_locales fact
qed

subsection ‹Correctness Proof›

locale fas_invar = DFS_invar where param = fas_params + fas
begin

lemma (in fas) i_fas_eq_back: "is_invar (λs. fas_state.fas s = back_edges s)"
apply (induct rule: establish_invarI)
apply (simp_all add: cond_def cong: fas_more_cong)
done
lemmas fas_eq_back = i_fas_eq_back[THEN make_invar_thm]

lemma find_fas_correct_aux:
assumes NC: "¬cond s"
shows "is_fas G (fas_state.fas s)"
proof -
note [simp] = fas_eq_back

from nc_edges_covered[OF NC] edges_disjoint have
"E ∩ reachable × UNIV - back_edges s = tree_edges s ∪ cross_edges s"
by auto
with tree_cross_acyclic show "is_fas G (fas_state.fas s)"
unfolding is_fas_alt by simp
qed

end

lemma find_fas_correct:
assumes "graph G"
assumes "finite ((g_E G)⇧* `` g_V0 G)"
shows "find_fas G ≤ SPEC (is_fas G)"
unfolding find_fas_def
proof (refine_vcg le_ASSERTI order_trans[OF DFS.it_dfsT_correct], clarsimp_all)
interpret graph G by fact
assume "finite ((g_E G)⇧* `` g_V0 G)"
then interpret fb_graph G by (rule fb_graphI_fr)
interpret fas by unfold_locales fact
show "DFS G fas_params" by unfold_locales
next
fix s
assume "DFS_invar G fas_params s"
then interpret DFS_invar G fas_params s .
interpret fas_invar G s by unfold_locales fact
assume "¬fas.cond TYPE('b) G s"
thus "is_fas G (fas_state.fas s)"
by (rule find_fas_correct_aux)
qed (rule assms)+

subsection ‹Implementation›

(* Implementation with stack and sso_visited set *)
record 'v fas_state_impl = "'v simple_state" +
fas :: "('v×'v) set"

(* Definition of refinement relation: The break-flag is refined by identity.*)
definition "fas_erel ≡ {
(⦇ fas_state_impl.fas = f ⦈, ⦇ fas_state.fas = f⦈) | f. True }"
abbreviation "fas_rel ≡ ⟨fas_erel⟩simple_state_rel"

(* Implementation of the parameters *)
definition fas_params_impl
:: "('v,'v fas_state_impl,('v,unit) fas_state_impl_ext) gen_parameterization"
where "fas_params_impl
≡ dflt_parametrization simple_state.more (RETURN ⦇ fas = {} ⦈) ⦇
on_back_edge := λu v s. RETURN ⦇ fas = insert (u,v) (fas s) ⦈⦈"
lemmas fas_params_impl_simp[simp,DFS_code_unfold] =
gen_parameterization.simps[mk_record_simp, OF fas_params_impl_def[simplified]]

lemma fas_impl: "(si,s)∈fas_rel
⟹ fas_state_impl.fas si = fas_state.fas s"
by (cases si, cases s, simp add: simple_state_rel_def fas_erel_def)

interpretation fas_impl: simple_impl_defs G fas_params_impl fas_params
for G .

(* The above locale creates an iterative and a recursive implementation *)
term fas_impl.tailrec_impl term fas_impl.tailrec_implT term fas_impl.rec_impl

definition [DFS_code_unfold]: "find_fas_impl G ≡ do {
ASSERT (graph G);
ASSERT (finite ((g_E G)⇧* `` g_V0 G));
s ← fas_impl.tailrec_implT TYPE('a) G;
RETURN (fas s)
}"

context fas begin
(* Derive the implementation *)
sublocale simple_impl G fas_params fas_params_impl fas_erel
apply unfold_locales
apply (intro fun_relI, clarsimp simp: simple_state_rel_def, parametricity) []
apply (auto simp: fas_erel_def fas_impl simple_state_rel_def)
done

lemmas impl_refine = simple_tailrec_refine simple_tailrecT_refine simple_rec_refine
thm simple_refine
end

lemma find_fas_impl_refine: "find_fas_impl G ≤ ⇓Id (find_fas G)"
unfolding find_fas_impl_def find_fas_def
apply (refine_vcg fas.impl_refine)
done

subsection ‹Synthesis of Executable Code›
(* Autoref *)
record ('si,'nsi,'fsi)fas_state_impl' = "('si,'nsi)simple_state_impl" +
fas_impl :: 'fsi

definition [to_relAPP]: "fas_state_erel frel erel ≡ {
(⦇fas_impl = fi, … =  mi⦈,⦇fas = f, … = m⦈) | fi mi f m.
(fi,f)∈frel ∧ (mi,m)∈erel}"

consts
i_fas_state_ext :: "interface ⇒ interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of fas_state_erel i_fas_state_ext]

term fas_update
term fas_state_impl'.fas_impl_update
lemma [autoref_rules]:
fixes ns_rel vis_rel frel erel
defines "R ≡ ⟨ns_rel,vis_rel,⟨frel,erel⟩fas_state_erel⟩ss_impl_rel"
shows
"(fas_state_impl'_ext, fas_state_impl_ext) ∈ frel → erel → ⟨frel,erel⟩fas_state_erel"
"(fas_impl, fas_state_impl.fas) ∈ R → frel"
"(fas_state_impl'.fas_impl_update, fas_update) ∈ (frel → frel) → R → R"
unfolding fas_state_erel_def ss_impl_rel_def R_def
by (auto, parametricity)

schematic_goal find_fas_impl:
fixes V :: "('vi×'v) set"
assumes [autoref_ga_rules]: "is_bounded_hashcode V eq bhc"
assumes [autoref_rules]: "(eq,(=)) ∈ V → V → bool_rel"
assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE ('vi) sz"
assumes [autoref_rules]:
"(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
notes [autoref_tyrel] =
TYRELI[where R="⟨V⟩ahs_rel bhc"]
TYRELI[where R="⟨V ×⇩r V⟩ahs_rel (prod_bhc bhc bhc)"]
TYRELI[where R="⟨V ×⇩r ⟨V⟩list_set_rel⟩ras_rel"]
shows "RETURN (?c::?'c) ≤⇓?R (find_fas_impl G)"
unfolding DFS_code_unfold
using [[autoref_trace_failed_id, goals_limit=1]]
done
concrete_definition find_fas_code for eq bhc sz Gi uses find_fas_impl
export_code find_fas_code checking SML

thm find_fas_code.refine

lemma find_fas_code_refine[refine]:
fixes V :: "('vi×'v) set"
assumes "is_bounded_hashcode V eq bhc"
assumes "(eq,(=)) ∈ V → V → bool_rel"
assumes "is_valid_def_hm_size TYPE ('vi) sz"
assumes 2: "(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
shows "RETURN (find_fas_code eq bhc sz Gi) ≤ ⇓(⟨V×⇩rV⟩ahs_rel (prod_bhc bhc bhc)) (find_fas G)"
proof -
note find_fas_code.refine[OF assms]
also note find_fas_impl_refine
finally show ?thesis .
qed

context begin interpretation autoref_syn .

text ‹Declare this algorithm to Autoref:›
theorem find_fas_code_autoref[autoref_rules]:
fixes V :: "('vi×'v) set" and bhc
defines "RR ≡ ⟨⟨V×⇩rV⟩ahs_rel (prod_bhc bhc bhc)⟩nres_rel"
assumes BHC: "SIDE_GEN_ALGO (is_bounded_hashcode V eq bhc)"
assumes EQ: "GEN_OP eq (=) (V → V → bool_rel)"
assumes VDS: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE ('vi) sz)"
assumes 2: "(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
shows "(RETURN (find_fas_code eq bhc sz Gi),
(OP find_fas
::: ⟨Rm, V⟩g_impl_rel_ext → RR)\$G)∈RR"
unfolding RR_def
apply (rule nres_relI)
using assms

end

subsection ‹Feedback Arc Set with Initialization›
text ‹This algorithm extends a given set to a feedback arc set. It works in two steps:
▸ Determine set of reachable nodes
▸ Construct feedback arc set for graph without initial set
›

definition find_fas_init where
"find_fas_init G FI ≡ do {
ASSERT (graph G);
ASSERT (finite ((g_E G)⇧* `` g_V0 G));
let nodes = (g_E G)⇧* `` g_V0 G;
fas ← find_fas ⦇ g_V = g_V G, g_E = g_E G - FI, g_V0 = nodes ⦈;
RETURN (FI ∪ fas)
}"

text ‹The abstract idea:
To find a feedback arc set that contains some set F2,
we can find a feedback arc set for the graph with F2 removed,
and then join with F2.
›
lemma is_fas_join: "is_fas G (F1 ∪ F2) ⟷
is_fas ⦇ g_V = g_V G, g_E = g_E G - F2, g_V0 = (g_E G)⇧* `` g_V0 G ⦈ F1"
unfolding is_fas_def
apply (auto simp: set_diff_diff_left Un_commute)
by (metis ImageI rtrancl_trans subsetCE rtrancl_mono[of "g_E G - F2" "g_E G", OF Diff_subset])

lemma graphI_init:
assumes "graph G"
shows "graph ⦇ g_V = g_V G, g_E = g_E G - FI, g_V0 = (g_E G)⇧* `` g_V0 G ⦈"
proof -
interpret graph G by fact
show ?thesis
apply unfold_locales
using reachable_V apply simp
using E_ss apply force
done
qed

lemma find_fas_init_correct:
assumes [simp, intro!]: "graph G"
assumes [simp, intro!]: "finite ((g_E G)⇧* `` g_V0 G)"
shows "find_fas_init G FI ≤ SPEC (λfas. is_fas G fas ∧ FI ⊆ fas)"
unfolding find_fas_init_def
apply (refine_vcg order_trans[OF find_fas_correct])
apply clarsimp_all
apply (rule graphI_init)
apply simp
apply (rule finite_subset[rotated], rule assms)
apply (metis Diff_subset Image_closed_trancl reachable_mono
rtrancl_image_unfold_right rtrancl_reflcl rtrancl_trancl_reflcl
trancl_rtrancl_absorb)
apply (simp add: is_fas_join[where ?F2.0=FI] Un_commute)
done

lemma gen_cast_set[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes INS: "GEN_OP ins Set.insert (Rk→⟨Rk⟩Rs2→⟨Rk⟩Rs2)"
assumes EM: "GEN_OP emp {} (⟨Rk⟩Rs2)"
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
shows "(λs. gen_union (λx. foldli (tsl x)) ins s emp,CAST)
∈ (⟨Rk⟩Rs1) → (⟨Rk⟩Rs2)"
proof -
note [autoref_rules] = GEN_OP_D[OF INS]
note [autoref_rules] = GEN_OP_D[OF EM]
note [autoref_ga_rules] = SIDE_GEN_ALGO_D[OF IT]
have 1: "CAST = (λs. s ∪ {})" by auto
show ?thesis
unfolding 1
by autoref
qed

lemma gen_cast_fun_set_rel[autoref_rules_raw]:
assumes INS: "GEN_OP mem (∈) (Rk→⟨Rk⟩Rs→bool_rel)"
shows "(λs x. mem x s,CAST) ∈ (⟨Rk⟩Rs) → (⟨Rk⟩fun_set_rel)"
proof -
have A: "⋀s. (λx. x∈s,CAST s) ∈ br Collect (λ_. True)"
by (auto simp: br_def)

show ?thesis
unfolding fun_set_rel_def
apply rule
apply rule
defer
apply (rule A)
using INS[simplified]
apply parametricity
done
qed

lemma find_fas_init_impl_aux_unfolds:
"Let (E⇧*``V0) = Let (CAST (E⇧*``V0))"
"(λS. RETURN (FI ∪ S)) = (λS. RETURN (FI ∪ CAST S))"
by simp_all

schematic_goal find_fas_init_impl:
fixes V :: "('vi×'v) set" and bhc
assumes [autoref_ga_rules]: "is_bounded_hashcode V eq bhc"
assumes [autoref_rules]: "(eq,(=)) ∈ V → V → bool_rel"
assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE ('vi) sz"
assumes [autoref_rules]:
"(Gi, G) ∈ ⟨Rm, V⟩g_impl_rel_ext"
"(FIi,FI)∈⟨V×⇩rV⟩fun_set_rel"
shows "RETURN (?c::?'c) ≤⇓?R (find_fas_init G FI)"
unfolding find_fas_init_def
unfolding find_fas_init_impl_aux_unfolds

concrete_definition find_fas_init_code for eq bhc sz Gi FIi
uses find_fas_init_impl
export_code find_fas_init_code checking SML

context begin interpretation autoref_syn .

text ‹The following theorem declares our implementation to Autoref:›
theorem find_fas_init_code_autoref[autoref_rules]:
fixes V :: "('vi×'v) set" and bhc
defines "RR ≡ ⟨V×⇩rV⟩fun_set_rel"
assumes "SIDE_GEN_ALGO (is_bounded_hashcode V eq bhc)"
assumes "GEN_OP eq (=) (V → V → bool_rel)"
assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE ('vi) sz)"
shows "(λGi FIi. RETURN (find_fas_init_code eq bhc sz Gi FIi),find_fas_init)
∈ ⟨Rm, V⟩g_impl_rel_ext → RR → ⟨RR⟩nres_rel"
unfolding RR_def
apply (intro fun_relI nres_relI)
using assms

end

subsection ‹Conclusion›
text ‹
We have defined an algorithm to find a feedback arc set, and one to
extend a given set to a feedback arc set. We have registered them to Autoref
as implementations for @{const find_fas} and @{const find_fas_init}.

For preliminary refinement steps, you need the theorems
@{thm [source] find_fas_correct} and @{thm [source] find_fas_init_correct}.
›

thm find_fas_code_autoref find_fas_init_code_autoref
thm find_fas_correct thm find_fas_init_correct

end

```