Theory DFS_Framework.Feedback_Arcs

section ‹Find a Feedback Arc Set›
theory Feedback_Arcs
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
  fix u v0
  assume 1: "v0g_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

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)"

  sublocale DFS G fas_params
    apply unfold_locales
    apply (simp_all add: fas_params_def)


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

subsection ‹Correctness Proof›

locale fas_invar = DFS_invar where param = fas_params + fas

  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)
    apply (simp add: empty_state_def)
  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


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
  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_erelsimple_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)

  lemmas impl_refine = simple_tailrec_refine simple_tailrecT_refine simple_rec_refine
  thm simple_refine

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)
  apply (simp_all add: fas_impl fasI)
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}"

  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,erelfas_state_erelss_impl_rel"
    "(fas_state_impl'_ext, fas_state_impl_ext)  frel  erel  frel,erelfas_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, Vg_impl_rel_ext"
  notes [autoref_tyrel] = 
    TYRELI[where R="Vahs_rel bhc"]
    TYRELI[where R="V ×r Vahs_rel (prod_bhc bhc bhc)"]
    TYRELI[where R="V ×r Vlist_set_relras_rel"]
  shows "RETURN (?c::?'c) ?R (find_fas_impl G)"
  unfolding DFS_code_unfold
  using [[autoref_trace_failed_id, goals_limit=1]]
  apply (autoref_monadic (trace))
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, Vg_impl_rel_ext"
  shows "RETURN (find_fas_code eq bhc sz Gi)  (V×rVahs_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 .

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×rVahs_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, Vg_impl_rel_ext"
  shows "(RETURN (find_fas_code eq bhc sz Gi),
    (OP find_fas 
      ::: Rm, Vg_impl_rel_ext  RR)$G)RR"
  unfolding RR_def
  apply (rule nres_relI)
  using assms 
  by (simp add: find_fas_code_refine)  


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

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 
  apply (simp add: is_fas_join[where ?F2.0=FI] Un_commute)

lemma gen_cast_set[autoref_rules_raw]:
  assumes INS: "GEN_OP ins Set.insert (RkRkRs2RkRs2)"
  assumes EM: "GEN_OP emp {} (RkRs2)"
  assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
  shows "(λs. gen_union (λx. foldli (tsl x)) ins s emp,CAST) 
     (RkRs1)  (RkRs2)"
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

lemma gen_cast_fun_set_rel[autoref_rules_raw]:
  assumes INS: "GEN_OP mem (∈) (RkRkRsbool_rel)"
  shows "(λs x. mem x s,CAST)  (RkRs)  (Rkfun_set_rel)"
proof -
  have A: "s. (λx. xs,CAST s)  br Collect (λ_. True)"
    by (auto simp: br_def)
  show ?thesis
    unfolding fun_set_rel_def
    apply rule
    apply rule
    apply (rule A)
    using INS[simplified]
    apply parametricity

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, Vg_impl_rel_ext"
  shows "RETURN (?c::?'c) ?R (find_fas_init G FI)"
  unfolding find_fas_init_def
  unfolding find_fas_init_impl_aux_unfolds
  by (autoref_monadic (plain,trace))

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×rVfun_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, Vg_impl_rel_ext  RR  RRnres_rel"
  unfolding RR_def
  apply (intro fun_relI nres_relI)
  using assms
  by (simp add: find_fas_init_code.refine)


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