Theory Sepref_DFS

header {* Simple DFS Algorithm *}
theory Sepref_DFS
imports 
  "../../CAVA_Automata/CAVA_Base/CAVA_Base" 
  "../../../DFS_Framework/Misc/DFS_Framework_Refine_Aux"
  "../Sepref"
  Sepref_Graph
begin

(*<*)

(* TODO: Move! *)
(* TODO: We do not really need the lower-bound for D in most cases.
  So let the default rules be without lower bound *)
lemma REC_rule_arb':
  fixes x::"'x" and arb::'arb
  assumes M: "trimono body"
  assumes I0: "pre arb x"
  assumes IS: "!!f arb x. [|
    !!arb' x. pre arb' x ==> f x ≤ M arb' x; pre arb x
  |] ==> body f x ≤ M arb x"
  shows "REC body x ≤ M arb x"
  apply (rule REC_rule_arb[where M=M and pre=pre])
  apply fact
  apply fact
  apply (rule IS)
  apply assumption+
  done

lemma RECT_rule_arb':
  fixes x::"'x" and arb::'arb
  assumes "trimono body"
    and "wf V"
    and "pre arb x"
    and
    IS: "!!f arb x.
        [|!!arb' x'. [|pre arb' x'; (x', x) ∈ V|] ==> f x' ≤ M arb' x'; pre arb x;
         f ≤ REC⇩T body|]
        ==> body f x ≤ M arb x"
  shows "REC⇩T body x ≤ M arb x"
  apply (rule RECT_rule_arb[where M=M and pre=pre])
  apply fact
  apply fact
  apply fact
  apply (rule IS)
  apply assumption+
  apply simp
  done

(*>*)

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. 
  @{text "E"} is the edge relation of the graph, @{text "vd"} the node to 
  search for, and @{text "v0"} the start node.
  Already explored nodes are stored in @{text "V"}.*}

context 
  fixes E :: "'v rel" and v0 :: 'v and tgt :: 'v
begin
  definition dfs :: "bool nres" where
    "dfs ≡ do {
      (_,r) \<leftarrow> RECT (λdfs (V,v). 
        if v∈V then RETURN (V,False)
        else do {
          let V=insert v V;
          if v = tgt then
            RETURN (V,True)
          else
            FOREACH⇩C (E``{v}) (λ(_,b). ¬b) (λv' (V,_). dfs (V,v')) (V,False)
        }
      ) ({},v0);
      RETURN r
    }"

  definition "reachable ≡ {v. (v0,v)∈E⇧*}"
  
  lemma dfs_correct:
    assumes fr: "finite reachable"
    shows "dfs ≤ SPEC (λr. r <-> (v0,tgt)∈E⇧*)"
  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)

  
    def rpre ≡ "λS (V,v). 
        v∈reachable 
      ∧ V⊆reachable
      ∧ S⊆V
      ∧ tgt∉V
      ∧ E``(V-S) ⊆ V"

    def rpost ≡ "λS (V,v) (V',r). 
          (r<->tgt∈V') 
        ∧ V⊆V' 
        ∧ v∈V'
        ∧ V'⊆reachable
        ∧ (¬r --> (E``(V'-S) ⊆ V'))
      "

    def fe_inv ≡ "λS V v it (V',r).
        (r<->tgt∈V')
      ∧ 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
      assume "rpre S (V,tgt)"
      hence "rpost S (V,tgt) (insert tgt 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" "v ≠ tgt"
        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" "v ≠ tgt" "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" "v ≠ tgt"
      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" "v ≠ tgt" "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 = ((v0, tgt) ∈ E⇧*)"
        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
      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 simp add: vc_rpost_imp_spec) []
      done
    qed
end

subsection ‹Refinement to Imperative/HOL›

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

schematic_lemma dfs_impl:
  fixes s t :: nat
  notes [sepref_opt_simps del] = imp_nfoldli_def 
    -- ‹Prevent the foreach-loop to be unfolded to a fixed-point, 
        to produce more readable code for presentation purposes.›
  notes [id_rules] = 
    itypeI[of s "TYPE(nat)"]
    itypeI[of t "TYPE(nat)"]
    itypeI[of E "TYPE(nat i_slg)"]
    -- ‹Declare parameters to operation identification›
  shows "hn_refine (
    hn_ctxt (is_graph nat_rel) E Ei 
  * hn_val nat_rel s si 
  * hn_val nat_rel t ti) (?c::?'c Heap) ?Γ' ?R (dfs E s t)"
  unfolding dfs_def -- ‹Unfold definition of DFS›
  apply sepref -- ‹Invoke sepref-tool›
  done

concrete_definition dfs_impl uses dfs_impl
  -- ‹Extract generated implementation into constant›
prepare_code_thms dfs_impl_def
  -- ‹Set up code equations for recursion combinators›
export_code dfs_impl checking SML_imp
  -- ‹Generate SML code with Imperative/HOL›

text ‹Finally, correctness is shown by combining the 
  generated refinement theorem with the abstract correctness theorem.›
corollary dfs_impl_correct:
  "finite (reachable E s) ==> 
  <is_graph nat_rel E Ei> 
    dfs_impl Ei s t 
  < λr. is_graph nat_rel E Ei * \<up>(r <-> (s,t)∈E⇧* ) >⇩t"
proof -
  assume FIN: "finite (reachable E s)"
  note aux = hn_refine_ref[OF dfs_correct dfs_impl.refine, 
    unfolded hn_refine_def, simplified, OF FIN]
  show ?thesis 
    apply (rule cons_rule[OF _ _ aux])
    apply (sep_auto simp: hn_ctxt_def pure_def)+
    done
qed

end