Theory Augmenting_Path_BFS

section ‹Breadth First Search›
theory Augmenting_Path_BFS
imports 
  Flow_Networks.Refine_Add_Fofu
  Flow_Networks.Graph_Impl
begin
  text ‹
    In this theory, we present a verified breadth-first search
    with an efficient imperative implementation.
    It is parametric in the successor function.
    ›

  subsection ‹Algorithm›
  locale pre_bfs_invar = Graph +    
    fixes src dst :: node
  begin  

    abbreviation "ndist v ≡ min_dist src v"

    definition Vd :: "nat ⇒ node set"
    where
      "⋀d. Vd d ≡ {v. connected src v ∧ ndist v = d}"

    lemma Vd_disj: "⋀d d'. d≠d' ⟹ Vd d ∩ Vd d' = {}"  
      by (auto simp: Vd_def)

    lemma src_Vd0[simp]: "Vd 0 = {src}"  
      by (auto simp: Vd_def)

    lemma in_Vd_conv: "v∈Vd d ⟷ connected src v ∧ ndist v = d"
      by (auto simp: Vd_def)

    lemma Vd_succ: 
      assumes "u∈Vd d"  
      assumes "(u,v)∈E"
      assumes "∀i≤d. v∉Vd i"
      shows "v∈Vd (Suc d)"
      using assms
      by (metis connected_append_edge in_Vd_conv le_SucE min_dist_succ)

  end

  locale valid_PRED = pre_bfs_invar +
    fixes PRED :: "node ⇀ node"
    assumes SRC_IN_V[simp]: "src∈V"
    assumes FIN_V[simp, intro!]: "finite V"
    assumes PRED_src[simp]: "PRED src = Some src"
    assumes PRED_dist: "⟦v≠src; PRED v = Some u⟧ ⟹ ndist v = Suc (ndist u)"
    assumes PRED_E: "⟦v≠src; PRED v = Some u⟧ ⟹ (u,v)∈E"
    assumes PRED_closed: "⟦ PRED v = Some u ⟧ ⟹ u∈dom PRED"
  begin
    lemma FIN_E[simp, intro!]: "finite E" using E_ss_VxV by simp
    lemma FIN_succ[simp, intro!]: "finite (E``{u})" 
      by (auto intro: finite_Image)
  end  
    
  locale nf_invar' = valid_PRED c src dst PRED for c src dst 
    and PRED :: "node ⇀ node"
    and C N :: "node set"
    and d :: nat 
    +
    assumes VIS_eq: "dom PRED = N ∪ {u. ∃i≤d. u∈Vd i}"
    assumes C_ss: "C ⊆ Vd d"
    assumes N_eq: "N = Vd (d+1) ∩ E``(Vd d - C)"
      
    assumes dst_ne_VIS: "dst ∉ dom PRED"

  locale nf_invar = nf_invar' +   
    assumes empty_assm: "C={} ⟹ N={}"

  locale f_invar = valid_PRED c src dst PRED for c src dst 
    and PRED :: "node ⇀ node"
    and d :: nat   
    + 
    assumes dst_found: "dst ∈ dom PRED ∩ Vd d"

  context Graph begin

    abbreviation "outer_loop_invar src dst ≡ λ(f,PRED,C,N,d). 
      (f ⟶ f_invar c src dst PRED d) ∧
      (¬f ⟶ nf_invar c src dst PRED C N d)

      "
    abbreviation "assn1 src dst ≡ λ(f,PRED,C,N,d). 
      ¬f ∧ nf_invar' c src dst PRED C N d"

  definition "add_succ_spec dst succ v PRED N ≡ ASSERT (N ⊆ dom PRED) ⪢ 
    SPEC (λ(f,PRED',N').
      case f of
        False ⇒ dst ∉ succ - dom PRED 
          ∧ PRED' = map_mmupd PRED (succ - dom PRED) v 
          ∧ N' = N ∪ (succ - dom PRED)
      | True ⇒ dst ∈ succ - dom PRED 
        ∧ PRED ⊆⇩m PRED' 
        ∧ PRED' ⊆⇩m map_mmupd PRED (succ - dom PRED) v 
        ∧ dst∈dom PRED'
  )"

  definition pre_bfs :: "node ⇒ node ⇒ (nat × (node⇀node)) option nres"
    where "pre_bfs src dst ≡ do {
    (f,PRED,_,_,d) ← WHILEIT (outer_loop_invar src dst) 
      (λ(f,PRED,C,N,d). f=False ∧ C≠{})
      (λ(f,PRED,C,N,d). do {
        v ← SPEC (λv. v∈C); let C = C-{v};
        ASSERT (v∈V);
        let succ = (E``{v});
        ASSERT (finite succ);
        (f,PRED,N) ← add_succ_spec dst succ v PRED N;
        if f then
          RETURN (f,PRED,C,N,d+1)
        else do {
          ASSERT (assn1 src dst (f,PRED,C,N,d));
          if (C={}) then do {
            let C=N; 
            let N={}; 
            let d=d+1;
            RETURN (f,PRED,C,N,d)
          } else RETURN (f,PRED,C,N,d)
        }  
      })
      (False,[src↦src],{src},{},0::nat);
    if f then RETURN (Some (d, PRED)) else RETURN None
    }"

  subsection "Correctness Proof"

  lemma (in nf_invar') ndist_C[simp]: "⟦v∈C⟧ ⟹ ndist v = d"  
    using C_ss by (auto simp: Vd_def)
  lemma (in nf_invar) CVdI: "⟦u∈C⟧ ⟹ u∈Vd d"
    using C_ss by (auto)

  lemma (in nf_invar) inPREDD: 
    "⟦PRED v = Some u⟧ ⟹ v∈N ∨ (∃i≤d. v∈Vd i)"   
    using VIS_eq by (auto)

  lemma (in nf_invar') C_ss_VIS: "⟦v∈C⟧ ⟹ v∈dom PRED"
    using C_ss VIS_eq by blast  

  lemma (in nf_invar) invar_succ_step:
    assumes "v∈C"
    assumes "dst ∉ E``{v} - dom PRED"
    shows "nf_invar' c src dst 
      (map_mmupd PRED (E``{v} - dom PRED) v) 
      (C-{v}) 
      (N ∪ (E``{v} - dom PRED)) 
      d"
  proof -
    from C_ss_VIS[OF ‹v∈C›] dst_ne_VIS have "v≠dst" by auto

    show ?thesis  
      using ‹v∈C› ‹v≠dst›
      apply unfold_locales
      apply simp
      apply simp
      apply (auto simp: map_mmupd_def) []
  
      apply (erule map_mmupdE)
      using PRED_dist apply blast
      apply (unfold VIS_eq) []
      apply clarify
      apply (metis CVdI Vd_succ in_Vd_conv)
  
      using PRED_E apply (auto elim!: map_mmupdE) []   
      using PRED_closed apply (auto elim!: map_mmupdE dest: C_ss_VIS) [] 
  
      using VIS_eq apply auto []
      using C_ss apply auto []
  
      apply (unfold N_eq) []
      apply (frule CVdI)
      apply (auto) []
      apply (erule (1) Vd_succ)
      using VIS_eq apply (auto) []
      apply (auto dest!: inPREDD simp: N_eq in_Vd_conv) []
  
      using dst_ne_VIS assms(2) apply auto []
      done
  qed  

  lemma invar_init: "⟦src≠dst; src∈V; finite V⟧ 
    ⟹ nf_invar c src dst [src ↦ src] {src} {} 0"            
    apply unfold_locales
    apply (auto)
    apply (auto simp: pre_bfs_invar.Vd_def split: if_split_asm)
    done

  lemma (in nf_invar) invar_exit:
    assumes "dst∈C"
    shows "f_invar c src dst PRED d"  
    apply unfold_locales
    using assms VIS_eq C_ss by auto

  lemma (in nf_invar) invar_C_ss_V: "u∈C ⟹ u∈V"  
    apply (drule CVdI)
    apply (auto simp: in_Vd_conv connected_inV_iff)
    done

  lemma (in nf_invar) invar_N_ss_Vis: "u∈N ⟹ ∃v. PRED u = Some v"
    using VIS_eq by auto  
    
  lemma (in pre_bfs_invar) Vdsucinter_conv[simp]: 
    "Vd (Suc d) ∩ E `` Vd d = Vd (Suc d)"
    apply (auto)
    by (metis Image_iff in_Vd_conv min_dist_suc)  

  lemma (in nf_invar') invar_shift:
    assumes [simp]: "C={}"
    shows "nf_invar c src dst PRED N {} (Suc d)"  
    apply unfold_locales
    apply vc_solve
    using VIS_eq N_eq[simplified] apply (auto simp add: le_Suc_eq) []
    using N_eq apply auto []
    using N_eq[simplified] apply auto []
    using dst_ne_VIS apply auto []
    done    

  lemma (in nf_invar') invar_restore:
    assumes [simp]: "C≠{}"
    shows "nf_invar c src dst PRED C N d"
    apply unfold_locales by auto

  definition "bfs_spec src dst r ≡ (
    case r of None ⇒ ¬ connected src dst
            | Some (d,PRED) ⇒ connected src dst 
                ∧ min_dist src dst = d 
                ∧ valid_PRED c src PRED 
                ∧ dst∈dom PRED)"

  lemma (in f_invar) invar_found:
    shows "bfs_spec src dst (Some (d,PRED))"
    unfolding bfs_spec_def
    apply simp
    using dst_found 
    apply (auto simp: in_Vd_conv)
    by unfold_locales

  lemma (in nf_invar) invar_not_found:
    assumes [simp]: "C={}"
    shows "bfs_spec src dst None"
    unfolding bfs_spec_def
    apply simp
  proof (rule notI)
    have [simp]: "N={}" using empty_assm by simp

    assume C: "connected src dst"
    then obtain d' where dstd': "dst ∈ Vd d'"
      by (auto simp: in_Vd_conv)

    txt ‹We make a case-distinction whether ‹d'≤d›:›
    have "d'≤d ∨ Suc d ≤ d'" by auto  
    moreover {
      assume "d'≤d"
      with VIS_eq dstd' have "dst ∈ dom PRED" by auto
      with dst_ne_VIS have False by auto
    } moreover {
      assume "Suc d ≤ d'"
      txt ‹In the case ‹d+1 ≤ d'›, we also obtain a node
        that has a shortest path of length ‹d+1›:›
      with min_dist_le[OF C] dstd' obtain v' where "v' ∈ Vd (Suc d)"
        by (auto simp: in_Vd_conv)
      txt ‹However, the invariant states that such nodes are either in
        ‹N› or are successors of ‹C›. As ‹N› 
        and ‹C› are both empty, we again get a contradiction.›
      with N_eq have False by auto  
    } ultimately show False by blast
  qed

  lemma map_le_mp: "⟦m⊆⇩mm'; m k = Some v⟧ ⟹ m' k = Some v"
    by (force simp: map_le_def)

  lemma (in nf_invar) dst_notin_Vdd[intro, simp]: "i≤d ⟹ dst∉Vd i"
    using VIS_eq dst_ne_VIS by auto 

  lemma (in nf_invar) invar_exit':
    assumes "u∈C" "(u,dst) ∈ E" "dst ∈ dom PRED'"
    assumes SS1: "PRED ⊆⇩m PRED'" 
      and SS2: "PRED' ⊆⇩m map_mmupd PRED (E``{u} - dom PRED) u"
    shows "f_invar c src dst PRED' (Suc d)"
    apply unfold_locales
    apply simp_all

    using map_le_mp[OF SS1 PRED_src] apply simp

    apply (drule map_le_mp[OF SS2])
    apply (erule map_mmupdE)
    using PRED_dist apply auto []
    apply (unfold VIS_eq) []
    apply clarify
    using ‹u∈C›
    apply (metis CVdI Vd_succ in_Vd_conv)

    apply (drule map_le_mp[OF SS2])
    using PRED_E apply (auto elim!: map_mmupdE) []   
    
    apply (drule map_le_mp[OF SS2])
    apply (erule map_mmupdE)
    using map_le_implies_dom_le[OF SS1]
    using PRED_closed apply (blast) []
    using C_ss_VIS[OF ‹u∈C›] map_le_implies_dom_le[OF SS1] apply blast
    using ‹dst ∈ dom PRED'› apply simp

    using ‹u∈C› CVdI[OF ‹u∈C›] ‹(u,dst)∈E›
    apply (auto) []
    apply (erule (1) Vd_succ)
    using VIS_eq apply (auto) []
    done



  definition "max_dist src ≡ Max (min_dist src`V)"

  definition "outer_loop_rel src ≡ 
    inv_image (
        less_than_bool 
        <*lex*> greater_bounded (max_dist src + 1) 
        <*lex*> finite_psubset) 
      (λ(f,PRED,C,N,d). (¬f,d,C))"
  lemma outer_loop_rel_wf: 
    assumes "finite V"
    shows "wf (outer_loop_rel src)"
    using assms
    unfolding outer_loop_rel_def
    by auto

  lemma (in nf_invar) C_ne_max_dist:
    assumes "C≠{}"
    shows "d ≤ max_dist src"
  proof -
    from assms obtain u where "u∈C" by auto
    with C_ss have "u∈Vd d" by auto
    hence "min_dist src u = d" "u∈V" 
      by (auto simp: in_Vd_conv connected_inV_iff)
    thus "d≤max_dist src" 
      unfolding max_dist_def by auto
  qed    

  lemma (in nf_invar) Vd_ss_V: "Vd d ⊆ V"
    by (auto simp: Vd_def connected_inV_iff)

  lemma (in nf_invar) finite_C[simp, intro!]: "finite C"
    using C_ss FIN_V Vd_ss_V by (blast intro: finite_subset)
  
  lemma (in nf_invar) finite_succ: "finite (E``{u})"  
    by auto

  theorem pre_bfs_correct: 
    assumes [simp]: "src∈V" "src≠dst"       
    assumes [simp]: "finite V"
    shows "pre_bfs src dst ≤ SPEC (bfs_spec src dst)"
    unfolding pre_bfs_def add_succ_spec_def
    apply (intro refine_vcg)
    apply (rule outer_loop_rel_wf[where src=src])
    apply (vc_solve simp:
      invar_init 
      nf_invar.invar_exit' 
      nf_invar.invar_C_ss_V 
      nf_invar.invar_succ_step
      nf_invar'.invar_shift
      nf_invar'.invar_restore        
      f_invar.invar_found
      nf_invar.invar_not_found
      nf_invar.invar_N_ss_Vis
      nf_invar.finite_succ
      )
    apply (vc_solve 
      simp: remove_subset outer_loop_rel_def 
      simp: nf_invar.C_ne_max_dist nf_invar.finite_C)
    done



  (* Presentation for Paper *)  
  definition bfs_core :: "node ⇒ node ⇒ (nat × (node⇀node)) option nres"
    where "bfs_core src dst ≡ do {
    (f,P,_,_,d) ← while⇩T (λ(f,P,C,N,d). f=False ∧ C≠{})
      (λ(f,P,C,N,d). do {
        v ← spec v. v∈C; let C = C-{v};
        let succ = (E``{v});
        (f,P,N) ← add_succ_spec dst succ v P N;
        if f then
          return (f,P,C,N,d+1)
        else do {
          if (C={}) then do {
            let C=N; let N={}; let d=d+1;
            return (f,P,C,N,d)
          } else return (f,P,C,N,d)
        }  
      })
      (False,[src↦src],{src},{},0::nat);
    if f then return (Some (d, P)) else return None
    }"

  theorem 
    assumes "src∈V" "src≠dst" "finite V"
    shows "bfs_core src dst ≤ (spec p. bfs_spec src dst p)"
    apply (rule order_trans[OF _ pre_bfs_correct])
    apply (rule refine_IdD)
    unfolding bfs_core_def pre_bfs_def
    apply refine_rcg
    apply refine_dref_type
    apply (vc_solve simp: assms)
    done


      
  subsection ‹Extraction of Result Path›

    definition "extract_rpath src dst PRED ≡ do {
      (_,p) ← WHILEIT
        (λ(v,p). 
          v∈dom PRED 
        ∧ isPath v p dst
        ∧ distinct (pathVertices v p)
        ∧ (∀v'∈set (pathVertices v p). 
            pre_bfs_invar.ndist c src v ≤ pre_bfs_invar.ndist c src v')
        ∧ pre_bfs_invar.ndist c src v + length p 
          = pre_bfs_invar.ndist c src dst)
        (λ(v,p). v≠src) (λ(v,p). do {
        ASSERT (v∈dom PRED);
        let u=the (PRED v);
        let p = (u,v)#p;
        let v=u;
        RETURN (v,p)
      }) (dst,[]);
      RETURN p
    }"

  end  

  context valid_PRED begin
    lemma extract_rpath_correct:
      assumes "dst∈dom PRED"
      shows "extract_rpath src dst PRED 
        ≤ SPEC (λp. isSimplePath src p dst ∧ length p = ndist dst)"
      using assms unfolding extract_rpath_def isSimplePath_def
      apply (refine_vcg wf_measure[where f="λ(d,_). ndist d"])
      apply (vc_solve simp: PRED_closed[THEN domD] PRED_E PRED_dist)
      apply auto
      done

  end

  context Graph begin

    definition "bfs src dst ≡ do {
      if src=dst then RETURN (Some [])
      else do {
        br ← pre_bfs src dst;
        case br of
          None ⇒ RETURN None
        | Some (d,PRED) ⇒ do {
            p ← extract_rpath src dst PRED;
            RETURN (Some p)
          }  
      }    
    }"

    lemma bfs_correct:
      assumes "src∈V" "finite V" 
      shows "bfs src dst 
        ≤ SPEC (λ
          None ⇒ ¬connected src dst 
        | Some p ⇒ isShortestPath src p dst)"
      unfolding bfs_def
      apply (refine_vcg
        pre_bfs_correct[THEN order_trans]
        valid_PRED.extract_rpath_correct[THEN order_trans]
        )
      using assms
      apply (vc_solve 
        simp: bfs_spec_def isShortestPath_min_dist_def isSimplePath_def)
      done      
  end

  (* Snippet for paper *)  
  context Finite_Graph begin
    interpretation Refine_Monadic_Syntax .
    theorem
      assumes "src∈V" 
      shows "bfs src dst ≤ (spec p. case p of 
          None ⇒ ¬connected src dst 
        | Some p ⇒ isShortestPath src p dst)"
      unfolding bfs_def
      apply (refine_vcg
        pre_bfs_correct[THEN order_trans]
        valid_PRED.extract_rpath_correct[THEN order_trans]
        )
      using assms
      apply (vc_solve 
        simp: bfs_spec_def isShortestPath_min_dist_def isSimplePath_def)
      done      

  end  

  subsection ‹Inserting inner Loop and Successor Function›
  context Graph begin

  definition "inner_loop dst succ u PRED N ≡ FOREACHci
    (λit (f,PRED',N'). 
        PRED' = map_mmupd PRED ((succ - it) - dom PRED) u 
      ∧ N' = N ∪ ((succ - it) - dom PRED)
      ∧ f = (dst∈(succ - it) - dom PRED)
    )
    (succ)
    (λ(f,PRED,N). ¬f)
    (λv (f,PRED,N). do {
      if v∈dom PRED then RETURN (f,PRED,N)
      else do {
        let PRED = PRED(v ↦ u);
        ASSERT (v∉N);
        let N = insert v N;
        RETURN (v=dst,PRED,N)
      }
    }) 
    (False,PRED,N)"


  lemma inner_loop_refine[refine]: 
    (*assumes NSS: "N ⊆ dom PRED"*)
    assumes [simp]: "finite succ"
    assumes [simplified, simp]: 
      "(succi,succ)∈Id" "(ui,u)∈Id" "(PREDi,PRED)∈Id" "(Ni,N)∈Id"
    shows "inner_loop dst succi ui PREDi Ni 
      ≤ ⇓Id (add_succ_spec dst succ u PRED N)"
    unfolding inner_loop_def add_succ_spec_def
    apply refine_vcg
    apply (auto simp: it_step_insert_iff; fail) +
    apply (auto simp: it_step_insert_iff fun_neq_ext_iff map_mmupd_def 
      split: if_split_asm) []
    apply (auto simp: it_step_insert_iff split: bool.split; fail)
    apply (auto simp: it_step_insert_iff split: bool.split; fail)
    apply (auto simp: it_step_insert_iff split: bool.split; fail)
    apply (auto simp: it_step_insert_iff intro: map_mmupd_update_less 
      split: bool.split; fail)
    done


  definition "inner_loop2 dst succl u PRED N ≡ nfoldli
    (succl) (λ(f,_,_). ¬f) (λv (f,PRED,N). do {
    if PRED v ≠ None then RETURN (f,PRED,N)
    else do {
      let PRED = PRED(v ↦ u);
      ASSERT (v∉N);
      let N = insert v N;
      RETURN ((v=dst),PRED,N)
    }
  }) (False,PRED,N)"

  lemma inner_loop2_refine:
    assumes SR: "(succl,succ)∈⟨Id⟩list_set_rel"
    shows "inner_loop2 dst succl u PRED N ≤ ⇓Id (inner_loop dst succ u PRED N)"
    using assms
    unfolding inner_loop2_def inner_loop_def
    apply (refine_rcg LFOci_refine SR)
    apply (vc_solve)
    apply auto
    done

  thm conc_trans[OF inner_loop2_refine inner_loop_refine, no_vars]

  lemma inner_loop2_correct:
    assumes "(succl, succ) ∈ ⟨Id⟩list_set_rel"
    (*assumes "N ⊆ dom PRED"*)
    assumes [simplified, simp]: 
      "(dsti,dst)∈Id" "(ui, u) ∈ Id" "(PREDi, PRED) ∈ Id" "(Ni, N) ∈ Id"
    shows "inner_loop2 dsti succl ui PREDi Ni 
      ≤ ⇓ Id (add_succ_spec dst succ u PRED N)"
    apply simp
    apply (rule conc_trans[OF inner_loop2_refine inner_loop_refine, simplified])
    using assms(1-2)
    apply (simp_all)
    done


  type_synonym bfs_state = "bool × (node ⇀ node) × node set × node set × nat"  

    context
      fixes succ :: "node ⇒ node list nres"
    begin
      definition init_state :: "node ⇒ bfs_state nres"
      where 
        "init_state src ≡ RETURN (False,[src↦src],{src},{},0::nat)"
  
      definition pre_bfs2 :: "node ⇒ node ⇒ (nat × (node⇀node)) option nres"
        where "pre_bfs2 src dst ≡ do {
        s ← init_state src;
        (f,PRED,_,_,d) ← WHILET (λ(f,PRED,C,N,d). f=False ∧ C≠{})
          (λ(f,PRED,C,N,d). do {
            ASSERT (C≠{});
            v ← op_set_pick C; let C = C-{v};
            ASSERT (v∈V);
            sl ← succ v;
            (f,PRED,N) ← inner_loop2 dst sl v PRED N;
            if f then
              RETURN (f,PRED,C,N,d+1)
            else do {
              ASSERT (assn1 src dst (f,PRED,C,N,d));
              if (C={}) then do {
                let C=N; 
                let N={}; 
                let d=d+1;
                RETURN (f,PRED,C,N,d)
              } else RETURN (f,PRED,C,N,d)
            }  
          })
          s;
        if f then RETURN (Some (d, PRED)) else RETURN None
        }"
    
      lemma pre_bfs2_refine: 
        assumes succ_impl: "⋀ui u. ⟦(ui,u)∈Id; u∈V⟧ 
          ⟹ succ ui ≤ SPEC (λl. (l,E``{u}) ∈ ⟨Id⟩list_set_rel)"
        shows "pre_bfs2 src dst ≤⇓Id (pre_bfs src dst)"
        unfolding pre_bfs_def pre_bfs2_def init_state_def
        apply (subst nres_monad1)
        apply (refine_rcg inner_loop2_correct succ_impl)
        apply refine_dref_type
        apply vc_solve (* Takes some time *)
        done
  
    end    
  
    definition "bfs2 succ src dst ≡ do {
      if src=dst then 
        RETURN (Some [])
      else do {  
        br ← pre_bfs2 succ src dst;
        case br of
          None ⇒ RETURN None
        | Some (d,PRED) ⇒ do {
            p ← extract_rpath src dst PRED;
            RETURN (Some p)
          }  
      }    
    }"

    lemma bfs2_refine:
      assumes succ_impl: "⋀ui u. ⟦(ui,u)∈Id; u∈V⟧ 
        ⟹ succ ui ≤ SPEC (λl. (l,E``{u}) ∈ ⟨Id⟩list_set_rel)"
      shows "bfs2 succ src dst ≤ ⇓Id (bfs src dst)"
      unfolding bfs_def bfs2_def
      apply (refine_vcg pre_bfs2_refine)
      apply refine_dref_type
      using assms
      apply (vc_solve)
      done      

  end  

  
  lemma bfs2_refine_succ: 
    assumes [refine]: "⋀ui u. ⟦(ui,u)∈Id; u∈Graph.V c⟧ 
      ⟹ succi ui ≤ ⇓Id (succ u)"
    assumes [simplified, simp]: "(si,s)∈Id" "(ti,t)∈Id" "(ci,c)∈Id"
    shows "Graph.bfs2 ci succi si ti ≤ ⇓Id (Graph.bfs2 c succ s t)"
    unfolding Graph.bfs2_def Graph.pre_bfs2_def
    apply (refine_rcg 
      param_nfoldli[param_fo, THEN nres_relD] nres_relI fun_relI)
    apply refine_dref_type
    apply vc_solve
    done

subsection ‹Imperative Implementation›

  context Impl_Succ begin
    definition op_bfs :: "'ga ⇒ node ⇒ node ⇒ path option nres" 
      where [simp]: "op_bfs c s t ≡ Graph.bfs2 (absG c) (succ c) s t"
  
    lemma pat_op_dfs[pat_rules]: 
      "Graph.bfs2$(absG$c)$(succ$c)$s$t ≡ UNPROTECT op_bfs$c$s$t" by simp 
  
    sepref_register "PR_CONST op_bfs" 
      :: "'ig ⇒ node ⇒ node ⇒ path option nres"  
  
    type_synonym ibfs_state 
      = "bool × (node,node) i_map × node set × node set × nat"

    sepref_register Graph.init_state :: "node ⇒ ibfs_state nres"
    schematic_goal init_state_impl:
      fixes src :: nat
      notes [id_rules] = 
        itypeI[Pure.of src "TYPE(nat)"]
      shows "hn_refine (hn_val nat_rel src srci) 
        (?c::?'c Heap) ?Γ' ?R (Graph.init_state src)"
      using [[id_debug, goals_limit = 1]]
      unfolding Graph.init_state_def
      apply (rewrite in "[src↦src]" iam.fold_custom_empty)
      apply (subst ls.fold_custom_empty)
      apply (subst ls.fold_custom_empty)
      apply (rewrite in "insert src _" fold_set_insert_dj)
      apply (rewrite in "_(⌑↦src)" fold_COPY)
      apply sepref
      done
    concrete_definition (in -) init_state_impl uses Impl_Succ.init_state_impl
    lemmas [sepref_fr_rules] = init_state_impl.refine[OF this_loc,to_hfref]

    schematic_goal bfs_impl:
      (*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 [sepref_opt_simps] = heap_WHILET_def
      fixes s t :: nat
      notes [id_rules] = 
        itypeI[Pure.of s "TYPE(nat)"]
        itypeI[Pure.of t "TYPE(nat)"]
        itypeI[Pure.of c "TYPE('ig)"]
        ― ‹Declare parameters to operation identification›
      shows "hn_refine (
        hn_ctxt (isG) c ci 
      * hn_val nat_rel s si 
      * hn_val nat_rel t ti) (?c::?'c Heap) ?Γ' ?R (PR_CONST op_bfs c s t)"
      unfolding op_bfs_def PR_CONST_def
      unfolding Graph.bfs2_def Graph.pre_bfs2_def 
        Graph.inner_loop2_def Graph.extract_rpath_def
      unfolding nres_monad_laws  
      apply (rewrite in "nfoldli _ _ ⌑ _" fold_set_insert_dj)
      apply (subst HOL_list.fold_custom_empty)+
      apply (rewrite in "let N={} in _" ls.fold_custom_empty)
      using [[id_debug, goals_limit = 1]]
      apply sepref
      done
    
    concrete_definition (in -) bfs_impl uses Impl_Succ.bfs_impl
      ― ‹Extract generated implementation into constant›
    prepare_code_thms (in -) bfs_impl_def
   
    lemmas bfs_impl_fr_rule = bfs_impl.refine[OF this_loc,to_hfref]  
  
  end

  export_code bfs_impl checking SML_imp

end