Theory Dijkstra_Impl

section ‹Implementation of Dijkstra's-Algorithm using the ICF›
theory Dijkstra_Impl
  In this second refinement step, we use interfaces from the 
  Isabelle Collection Framework (ICF) to implement the priority queue and
  the result map. Moreover, we use a graph interface (that is not contained 
  in the ICF, but in this development) to represent the graph.

  The data types of the first refinement step were designed to fit the
  abstract data types of the used ICF-interfaces, which makes this refinement
  quite straightforward.

  Finally, we instantiate the ICF-interfaces by concrete implementations, 
  obtaining an executable algorithm, for that we generate code using 
  Isabelle/HOL's code generator.

locale dijkstraC =
  g: StdGraph g_ops + 
  mr: StdMap mr_ops +
  qw: StdUprio qw_ops
  for g_ops :: "('V,'W::weight,'G,'moreg) graph_ops_scheme"
  and mr_ops :: "('V, (('V,'W) path × 'W), 'mr,'more_mr) map_ops_scheme"
  and qw_ops :: "('V ,'W infty,'qw,'more_qw) uprio_ops_scheme" 
  definition "αsc == map_prod qw.α mr.α"
  definition "dinvarC_add == λ(wl,res). qw.invar wl  mr.invar res"

  definition cdinit :: "'G  'V  ('qw×'mr) nres" where
    "cdinit g v0  do {
      wl  FOREACH (nodes (g.α g)) 
        (λv wl. RETURN (qw.insert wl v Weight.Infty)) (qw.empty ());
      RETURN (qw.insert wl v0 (Num 0),mr.sng v0 ([],0))

  definition cpop_min :: "('qw×'mr)  ('V×'W infty×('qw×'mr)) nres" where
    "cpop_min σ  do {
      let (wl,res) = σ; 
      let (v,w,wl')=qw.pop wl;
      RETURN (v,w,(wl',res))

  definition cupdate :: "'G  'V  'W infty  ('qw×'mr)  ('qw×'mr) nres"
    "cupdate g v wv σ = do {
      ASSERT (dinvarC_add σ);
      let (wl,res)=σ;
      let pv=mpath' (mr.lookup v res);
      FOREACH (succ (g.α g) v) (λ(w',v') (wl,res).
        if (wv + Num w' < mpath_weight' (mr.lookup v' res)) then do {
          RETURN (qw.insert wl v' (wv+Num w'), 
                  mr.update v' ((v,w',v')#the pv,val wv + w') res)
        } else RETURN (wl,res)
      ) (wl,res)

  definition cdijkstra where
    "cdijkstra g v0  do {
      σ0  cdinit g v0; 
      (_,res)  WHILET (λ(wl,_). ¬ qw.isEmpty wl) 
            (λσ. do { (v,wv,σ')  cpop_min σ; cupdate g v wv σ' } )
      RETURN res


locale dijkstraC_fixg = dijkstraC g_ops mr_ops qw_ops +
  Dijkstra ga v0
  for g_ops :: "('V,'W::weight,'G,'moreg) graph_ops_scheme"
  and mr_ops :: "('V, (('V,'W) path × 'W), 'mr,'more_mr) map_ops_scheme"
  and qw_ops :: "('V ,'W infty,'qw,'more_qw) uprio_ops_scheme" 
  and ga :: "('V,'W) graph" 
  and v0 :: 'V +
  fixes g :: 'G
  assumes g_rel: "(g,ga)br g.α g.invar"
  schematic_goal cdinit_refines: 
    notes [refine] = inj_on_id
    shows "cdinit g v0 ?R mdinit"
    using g_rel
    unfolding cdinit_def mdinit_def
    apply (refine_rcg)
    apply (refine_dref_type)
    apply (simp_all add: αsc_def dinvarC_add_def refine_rel_defs
      qw.correct mr.correct refine_hsimp)

  schematic_goal cpop_min_refines:
    "(σ,σ')  build_rel αsc dinvarC_add
       cpop_min σ  ?R (mpop_min σ')"
    unfolding cpop_min_def mpop_min_def
    apply (refine_rcg)
    apply (refine_dref_type)
    apply (simp add: αsc_def dinvarC_add_def refine_hsimp refine_rel_defs)
    apply (simp add: αsc_def dinvarC_add_def refine_hsimp refine_rel_defs)

  schematic_goal cupdate_refines:
    notes [refine] = inj_on_id
    shows "(σ,σ')build_rel αsc dinvarC_add  v=v'  wv=wv'  
    cupdate g v wv σ  ?R (mupdate v' wv' σ')"
    unfolding cupdate_def mupdate_def
    using g_rel
    apply (refine_rcg)
    apply (refine_dref_type)
    apply (simp_all add: αsc_def dinvarC_add_def refine_rel_defs 
      qw.correct mr.correct refine_hsimp)

  lemma cdijkstra_refines: 
    "cdijkstra g v0  (build_rel mr.α mr.invar) mdijkstra"
  proof -
    note [refine] = cdinit_refines cpop_min_refines cupdate_refines
    show ?thesis
      unfolding cdijkstra_def mdijkstra_def
      using g_rel
      apply (refine_rcg)

      apply (auto
        split: prod.split prod.split_asm 
        simp add: qw.correct mr.correct dinvarC_add_def αsc_def refine_hsimp

context dijkstraC

  thm g.nodes_it_is_iterator

  schematic_goal idijkstra_refines_aux: 
    assumes "g.invar g"
    shows "RETURN ?f  cdijkstra g v0"
    using assms
    unfolding cdijkstra_def cdinit_def cpop_min_def cupdate_def 
    apply (refine_transfer)

  concrete_definition idijkstra for g ?v0.0 uses idijkstra_refines_aux 

  lemma idijkstra_refines: 
    assumes "g.invar g"
    shows "RETURN (idijkstra g v0)  cdijkstra g v0"
    using assms
    by (rule idijkstra.refine) 


text ‹
  The following theorem states correctness of the algorithm independent
  from the refinement framework.

  Intuitively, the first goal states that the abstraction of the returned 
  result is correct, the second goal states that the result
  datastructure satisfies its invariant, and the third goal states 
  that the cached weights in the returned result are correct.

  Note that this is the main theorem for a user of Dijkstra's algorithm in some 
  bigger context. It may also be specialized for concrete instances of the
  implementation, as exemplarily done below.
theorem (in dijkstraC_fixg) idijkstra_correct:
  "weighted_graph.is_shortest_path_map ga v0 (αr (mr.α (idijkstra g v0)))" 
    (is ?G1)
  and "mr.invar (idijkstra g v0)" (is ?G2) 
  and "Dijkstra.res_invarm (mr.α (idijkstra g v0))" (is ?G3)
proof -
  from g_rel have I: "g.invar g" by (simp add: refine_rel_defs)

  note idijkstra_refines[OF I]
  also note cdijkstra_refines
  also note mdijkstra_refines
  finally have Z: "RETURN (idijkstra g v0)  
    (build_rel (αr  mr.α) (λm. mr.invar m  res_invarm (mr.α m))) 
    apply (subst (asm) conc_fun_chain)
    apply (simp only: br_chain)
  also note dijkstra'_refines[simplified]
  also note dijkstra_correct 
  finally show ?G1 ?G2 ?G3 
    by (auto elim: RETURN_ref_SPECD simp: refine_rel_defs)

theorem (in dijkstraC) idijkstra_correct:
  assumes INV: "g.invar g"
  assumes V0: "v0  nodes (g.α g)"
  assumes nonneg_weights: "v w v'. (v,w,v')edges (g.α g)  0w"
  "weighted_graph.is_shortest_path_map (g.α g) v0 
      (Dijkstra.αr (mr.α (idijkstra g v0)))" (is ?G1)
  and "Dijkstra.res_invarm (mr.α (idijkstra g v0))" (is ?G2)
proof -
  interpret gv: valid_graph "g.α g" using g.valid INV .

  interpret dcg: dijkstraC_fixg g_ops mr_ops qw_ops "g.α g" v0 g
    apply (rule dijkstraC_fixg.intro)
    apply unfold_locales 
    apply (simp_all add: hlg.finite INV V0 hlg_ops_def 
      nonneg_weights refine_rel_defs)

  from dcg.idijkstra_correct show ?G1 ?G2 by simp_all

text ‹
  Example instantiation with HashSet.based graph, 
  red-black-tree based result map, and finger-tree based priority queue.
setup Locale_Code.open_block
interpretation hrf: dijkstraC hlg_ops rm_ops aluprioi_ops
  by unfold_locales
setup Locale_Code.close_block

definition "hrf_dijkstra  hrf.idijkstra"
lemmas hrf_dijkstra_correct = hrf.idijkstra_correct[folded hrf_dijkstra_def]

export_code hrf_dijkstra checking SML
export_code hrf_dijkstra in OCaml
export_code hrf_dijkstra in Haskell
export_code hrf_dijkstra checking Scala

definition hrfn_dijkstra :: "(nat,nat) hlg  _" 
  where "hrfn_dijkstra  hrf_dijkstra"

export_code hrfn_dijkstra in SML

lemmas hrfn_dijkstra_correct = 
  hrf_dijkstra_correct[where ?'a = nat and ?'b = nat, folded hrfn_dijkstra_def]

term hrfn_dijkstra
term hlg.from_list

definition "test_hrfn_dijkstra 
    (hrfn_dijkstra (hlg.from_list ([0..<4],[(0,3,1),(0,4,2),(2,1,3),(1,4,3)])) 0)"

ML_val @{code test_hrfn_dijkstra}