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 v∈V then RETURN (V,False)
        else do {
          let V=insert v V;
          if tgt v then
            RETURN (V,True)
          else
            FOREACH⇩C (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 ⟷ reachable∩Collect tgt≠{}) ∧ (¬r ⟶ V=reachable))"
  
  lemma dfs_correct:
    assumes fr: "finite reachable"
    shows "dfs ≤ dfs_spec"
  proof -
    have F: "⋀v. v∈reachable ⟹ 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). 
        v∈reachable 
      ∧ V⊆reachable
      ∧ S⊆V
      ∧ (V ∩ Collect tgt = {})
      ∧ E``(V-S) ⊆ V)"

    define rpost where "rpost = (λS (V,v) (V',r). 
          (r⟷V'∩Collect tgt ≠ {}) 
        ∧ V⊆V' 
        ∧ v∈V'
        ∧ V'⊆reachable
        ∧ (¬r ⟶ (E``(V'-S) ⊆ V')))
      "

    define fe_inv where "fe_inv = (λS V v it (V',r).
        (r⟷V'∩Collect tgt ≠ {})
      ∧ insert v V⊆V'
      ∧ E``{v} - it ⊆ V'
      ∧ V'⊆reachable
      ∧ S⊆insert 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 "v∈V"
      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 ≠ {}) ∧ (¬r⟶V=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) → ⟨Id⟩nres_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_assn⇧k*⇩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