Theory Sepref_DFS

section ‹Simple DFS Algorithm›
theory Sepref_DFS
imports 
  "../Sepref"
  Sepref_Graph
begin

text ‹
  We define a simple DFS-algorithm, prove a simple correctness
  property, and do data refinement to an efficient implementation.
›

subsection ‹Definition›

text ‹Recursive DFS-Algorithm. 
  E› is the edge relation of the graph, vd› the node to 
  search for, and v0› the start node.
  Already explored nodes are stored in V›.›

context 
  fixes E :: "'v rel" and v0 :: 'v and tgt :: "'v  bool"
begin
  definition dfs :: "('v set × bool) nres" where
    "dfs  do {
      (V,r)  RECT (λdfs (V,v). 
        if vV then RETURN (V,False)
        else do {
          let V=insert v V;
          if tgt v then
            RETURN (V,True)
          else
            FOREACHC (E``{v}) (λ(_,b). ¬b) (λv' (V,_). dfs (V,v')) (V,False)
        }
      ) ({},v0);
      RETURN (V,r)
    }"

  definition "reachable  {v. (v0,v)E*}"

  definition "dfs_spec  SPEC (λ(V,r). (r  reachableCollect tgt{})  (¬r  V=reachable))"
  
  lemma dfs_correct:
    assumes fr: "finite reachable"
    shows "dfs  dfs_spec"
  proof -
    have F: "v. vreachable  finite (E``{v})"
      using fr
      apply (auto simp: reachable_def)
      by (metis (mono_tags) Image_singleton Image_singleton_iff
        finite_subset rtrancl.rtrancl_into_rtrancl subsetI)

  
    define rpre where "rpre = (λS (V,v). 
        vreachable 
       Vreachable
       SV
       (V  Collect tgt = {})
       E``(V-S)  V)"

    define rpost where "rpost = (λS (V,v) (V',r). 
          (rV'Collect tgt  {}) 
         VV' 
         vV'
         V'reachable
         (¬r  (E``(V'-S)  V')))
      "

    define fe_inv where "fe_inv = (λS V v it (V',r).
        (rV'Collect tgt  {})
       insert v VV'
       E``{v} - it  V'
       V'reachable
       Sinsert v V
       (¬r  E``(V'-S)  V'  it  E``(V'-insert v S)  V'))"

    have vc_pre_initial: "rpre {} ({}, v0)"
      by (auto simp: rpre_def reachable_def)

    {
      (* Case: Node already visited *)
      fix S V v
      assume "rpre S (V,v)"
        and "vV"
      hence "rpost S (V,v) (V,False)"
        unfolding rpre_def rpost_def
        by auto
    } note vc_node_visited = this

    {
      (* Case: Found node *)
      fix S V v
      assume "tgt v"
      and "rpre S (V,v)"
      hence "rpost S (V,v) (insert v V, True)"
        unfolding rpre_def rpost_def
        by auto
    } note vc_node_found = this

    { 
      fix S V v
      assume "rpre S (V, v)"
      hence "finite (E``{v})"
        unfolding rpre_def using F by (auto)
    } note vc_foreach_finite = this
  
    {
      (* fe_inv initial *)
      fix S V v
      assume A: "v  V" "¬tgt v"
        and PRE: "rpre S (V, v)"
      hence "fe_inv S V v (E``{v}) (insert v V, False)"
        unfolding fe_inv_def rpre_def by (auto)
    } note vc_enter_foreach = this

    {
      (* fe_inv ensures rpre *)
      fix S V v v' it V'
      assume A: "v  V" "¬tgt v" "v'  it" "it  E``{v}"
        and FEI: "fe_inv S V v it (V', False)"
        and PRE: "rpre S (V, v)"

      from A have "v'  E``{v}" by auto
      moreover from PRE have "v  reachable" by (auto simp: rpre_def)
      hence "E``{v}  reachable" by (auto simp: reachable_def)
      ultimately have [simp]: "v'reachable" by blast

      have "rpre (insert v S) (V', v')"
        unfolding rpre_def
        using FEI PRE by (auto simp: fe_inv_def rpre_def) []
    } note vc_rec_pre = this

    {
      (* rpost implies fe_inv *)
      fix S V V' v v' it Vr''
      assume "fe_inv S V v it (V', False)"
        and "rpost (insert v S) (V', v') Vr''"
      hence "fe_inv S V v (it - {v'}) Vr''"
        unfolding rpre_def rpost_def fe_inv_def
        by clarsimp blast
    } note vc_iterate_foreach = this

    {
      (* fe_inv (completed) implies rpost *)
      fix S V v V'
      assume PRE: "rpre S (V, v)" 
      assume A: "v  V" "¬tgt v"
      assume FEI: "fe_inv S V v {} (V', False)"
      have "rpost S (V, v) (V', False)"
        unfolding rpost_def
        using FEI by (auto simp: fe_inv_def) []
    } note vc_foreach_completed_imp_post = this

    {
      (* fe_inv (interrupted) implies rpost *)
      fix S V v V' it
      assume PRE: "rpre S (V, v)" 
        and A: "v  V" "¬tgt v" "it  E``{v}"
        and FEI: "fe_inv S V v it (V', True)"
      hence "rpost S (V, v) (V', True)"
        by (auto simp add: rpre_def rpost_def fe_inv_def) []
    } note vc_foreach_interrupted_imp_post = this

    {
      fix V r
      assume "rpost {} ({}, v0) (V, r)"
      hence "(r  reachable  Collect tgt  {})  (¬rV=reachable)"
        by (auto 
          simp: rpost_def reachable_def 
          dest: Image_closed_trancl 
          intro: rev_ImageI)
    } note vc_rpost_imp_spec = this

    show ?thesis
      unfolding dfs_def dfs_spec_def
      apply (refine_rcg refine_vcg)
      apply (rule order_trans)
      
      apply(rule RECT_rule_arb[where 
          pre=rpre 
          and M="λa x. SPEC (rpost a x)"
          and V="finite_psupset reachable <*lex*> {}"
          ])
      apply refine_mono
      apply (blast intro: fr)
      apply (rule vc_pre_initial)
      
      apply (refine_rcg refine_vcg 
        FOREACHc_rule'[where I="fe_inv S v s" for S v s]
        )
      apply (simp_all add: vc_node_visited vc_node_found)

      apply (simp add: vc_foreach_finite)

      apply (auto intro: vc_enter_foreach) []

      apply (rule order_trans)
      apply (rprems)
      apply (erule (5) vc_rec_pre)
        apply (auto simp add: fe_inv_def finite_psupset_def) []
        apply (refine_rcg refine_vcg)
        apply (simp add: vc_iterate_foreach)

      apply (auto simp add: vc_foreach_completed_imp_post) []

      apply (auto simp add: vc_foreach_interrupted_imp_post) []

      apply (auto dest: vc_rpost_imp_spec) []
      done
  qed

end

lemma dfs_correct': "(uncurry2 dfs, uncurry2 dfs_spec) 
   [λ((E,s),t). finite (reachable E s)]f ((Id×rId)×rId)  Idnres_rel"  
  apply (intro frefI nres_relI; clarsimp)
  by (rule dfs_correct)


subsection ‹Refinement to Imperative/HOL›

text ‹We set up a schematic proof goal,
  and use the sepref-tool to synthesize the implementation.
›

sepref_definition dfs_impl is 
  "uncurry2 dfs" :: "(adjg_assn nat_assn)k*anat_assnk*a(pure (nat_rel  bool_rel))k a prod_assn (ias.assn nat_assn) bool_assn"
  unfolding dfs_def[abs_def] ― ‹Unfold definition of DFS›
  using [[goals_limit = 1]]
  apply (rewrite in "RECT _ (,_)" ias.fold_custom_empty) ― ‹Select impls›
  apply (rewrite in "if  then RETURN (_,True) else _" fold_pho_apply)
  apply sepref ― ‹Invoke sepref-tool›
  done
export_code dfs_impl checking SML_imp
  ― ‹Generate SML code with Imperative/HOL›

export_code dfs_impl in Haskell module_name DFS


text ‹Finally, correctness is shown by combining the 
  generated refinement theorem with the abstract correctness theorem.›

lemmas dfs_impl_correct' = dfs_impl.refine[FCOMP dfs_correct']

corollary dfs_impl_correct:
  "finite (reachable E s)  
  <adjg_assn nat_assn E Ei> 
    dfs_impl Ei s tgt
  < λ(Vi,r). AV. adjg_assn nat_assn E Ei * ias.assn nat_assn V Vi * ((r  reachable E s  Collect tgt  {})  (¬r  V=reachable E s) ) >t"
  using dfs_impl_correct'[THEN hfrefD, THEN hn_refineD, of "((E,s),tgt)" "((Ei,s),tgt)", simplified]
  apply (rule cons_rule[rotated -1])
  apply (sep_auto intro!: ent_ex_preI simp: dfs_spec_def pure_def)+
  done


end