Theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet

section ‹Implementation of Dijkstra's-Algorithm using Automatic Determinization›
theory Dijkstra_Impl_Adet
imports 
  Dijkstra 
  GraphSpec 
  HashGraphImpl 
  Collections.Refine_Dflt_ICF
  "HOL-Library.Code_Target_Numeral"
begin 


subsection ‹Setup›

subsubsection ‹Infinity›
definition infty_rel_internal_def: 
  "infty_rel R  {(Num a, Num a')| a a'. (a,a')R}  {(Infty,Infty)}"
lemma infty_rel_def[refine_rel_defs]: 
  "Rinfty_rel = {(Num a, Num a')| a a'. (a,a')R}  {(Infty,Infty)}"
  unfolding infty_rel_internal_def relAPP_def by simp

lemma infty_relI: 
  "(Infty,Infty)Rinfty_rel"
  "(a,a')R  (Num a, Num a')Rinfty_rel"
  unfolding infty_rel_def by auto

lemma infty_relE:
  assumes "(x,x')Rinfty_rel"
  obtains "x=Infty" and "x'=Infty"
  | a a' where "x=Num a" and "x'=Num a'" and "(a,a')R"
  using assms
  unfolding infty_rel_def
  by auto
  
lemma infty_rel_simps[simp]:
  "(Infty,x')Rinfty_rel  x'=Infty"
  "(x,Infty)Rinfty_rel  x=Infty"
  "(Num a, Num a')Rinfty_rel  (a,a')R"
  unfolding infty_rel_def by auto

lemma infty_rel_sv[relator_props]: 
  "single_valued R  single_valued (Rinfty_rel)"
  unfolding infty_rel_def
  by (auto intro: single_valuedI dest: single_valuedD)

lemma infty_rel_id[simp, relator_props]: "Idinfty_rel = Id"
  apply rule
  apply (auto elim: infty_relE) []
  apply safe
  apply (case_tac b) by auto

consts i_infty :: "interface  interface"
lemmas [autoref_rel_intf] = REL_INTFI[of infty_rel i_infty]

lemma autoref_infty[param,autoref_rules]:
  "(Infty,Infty)Rinfty_rel"
  "(Num,Num)RRinfty_rel"
  "(case_infty,case_infty)Rr(RRr)Rinfty_relRr"
  "(rec_infty,rec_infty)Rr(RRr)Rinfty_relRr"
  unfolding infty_rel_def
  by (auto dest: fun_relD)
  
definition [simp]: "is_Infty x  case x of Infty  True | _  False"

context begin interpretation autoref_syn .
lemma pat_is_Infty[autoref_op_pat]: 
  "x=Infty  (OP is_Infty :::i Iii_infty i i_bool)$x"
  "Infty=x  (OP is_Infty :::i Iii_infty i i_bool)$x"
  by (auto intro!: eq_reflection split: infty.splits)
end

lemma autoref_is_Infty[autoref_rules]: 
  "(is_Infty, is_Infty)Rinfty_rel  bool_rel"
  by (auto split: infty.splits)

definition "infty_eq eq v1 v2  
  case (v1,v2) of
    (Infty,Infty)  True
  | (Num a1, Num a2)  eq a1 a2
  | _  False"

lemma infty_eq_autoref[autoref_rules (overloaded)]:
  " GEN_OP eq (=) (RRbool_rel)  
   (infty_eq eq,(=))Rinfty_relRinfty_relbool_rel"
  unfolding infty_eq_def[abs_def]
  by (auto split: infty.splits dest: fun_relD elim!: infty_relE)

lemma infty_eq_expand[autoref_struct_expand]: "(=) = infty_eq (=)"
  by (auto intro!: ext simp: infty_eq_def split: infty.splits)

context begin interpretation autoref_syn .
lemma infty_val_autoref[autoref_rules]: 
  "SIDE_PRECOND (xInfty); (xi,x)Rinfty_rel 
   (val xi,(OP val ::: Rinfty_rel  R) $ x)R"
  apply (cases x) 
  apply (auto elim: infty_relE)
  done
end

definition infty_plus where
  "infty_plus pl a b  case (a,b) of (Num a, Num b)  Num (pl a b) | _  Infty "

lemma infty_plus_param[param]:
  "(infty_plus,infty_plus)  (RRR)  Rinfty_rel  Rinfty_rel  Rinfty_rel"
  unfolding infty_plus_def[abs_def]
  by parametricity

lemma infty_plus_eq_plus: "infty_plus (+) = (+)"
  unfolding infty_plus_def[abs_def] 
  by (auto intro!: ext split: infty.split)
  

lemma infty_plus_autoref[autoref_rules]:
  "GEN_OP pl (+) (RRR) 
   (infty_plus pl,(+))  Rinfty_rel  Rinfty_rel  Rinfty_rel"
  apply (fold infty_plus_eq_plus)
  apply simp
  apply parametricity
  done

subsubsection ‹Graph›
consts i_graph :: "interface  interface  interface"

definition graph_more_rel_internal_def:
  "graph_more_rel Rm Rv Rw  { (g,g'). 
    (graph.nodes g, graph.nodes g')Rvset_rel     
   (graph.edges g, graph.edges g')Rv,Rw,Rvprod_relprod_relset_rel
   (graph.more g, graph.more g')Rm}"

lemma graph_more_rel_def[refine_rel_defs]: 
  "Rm,Rv,Rwgraph_more_rel  { (g,g'). 
    (graph.nodes g, graph.nodes g')Rvset_rel     
   (graph.edges g, graph.edges g')Rv,Rw,Rvprod_relprod_relset_rel
   (graph.more g, graph.more g')Rm}"
  unfolding relAPP_def graph_more_rel_internal_def by simp
  
abbreviation "graph_rel  unit_relgraph_more_rel"
lemmas graph_rel_def = graph_more_rel_def[where Rm=unit_rel, simplified]

lemma graph_rel_id[simp]: "Id,Idgraph_rel = Id"
  unfolding graph_rel_def by auto

lemma graph_more_rel_sv[relator_props]: 
  "single_valued Rm; single_valued Rv; single_valued Rw 
   single_valued (Rm,Rv,Rwgraph_more_rel)"
  unfolding graph_more_rel_def
  apply (rule single_valuedI, clarsimp)
  apply (rule graph.equality)
  apply (erule (1) single_valuedD[rotated], tagged_solver)+
  done

lemma [autoref_itype]: 
  "graph.nodes ::i Iv,Iwii_graph i Ivii_set" 
  by simp_all

thm is_map_to_sorted_list_def

definition "nodes_to_list g  it_to_sorted_list (λ_ _. True) (graph.nodes g)"
lemma nodes_to_list_itype[autoref_itype]: "nodes_to_list ::i Iv,Iwii_graph i Ivii_listii_nres" by simp
lemma nodes_to_list_pat[autoref_op_pat]: "it_to_sorted_list (λ_ _. True) (graph.nodes g)  nodes_to_list g"
  unfolding nodes_to_list_def by simp

definition "succ_to_list g v  it_to_sorted_list (λ_ _. True) (Graph.succ g v)"
lemma succ_to_list_itype[autoref_itype]: 
  "succ_to_list ::i Iv,Iwii_graph i Iv i Iw,Ivii_prodii_listii_nres" by simp
lemma succ_to_list_pat[autoref_op_pat]: "it_to_sorted_list (λ_ _. True) (Graph.succ g v)  succ_to_list g v"
  unfolding succ_to_list_def by simp

context graph begin
  definition rel_def_internal: "rel Rv Rw  br α invar O Rv,Rwgraph_rel"
  lemma rel_def: "Rv,Rwrel  br α invar O Rv,Rwgraph_rel"
    unfolding relAPP_def rel_def_internal by simp

  lemma rel_id[simp]: "Id,Idrel = br α invar" by (simp add: rel_def)

  lemma rel_sv[relator_props]: 
    "single_valued Rv; single_valued Rw  single_valued (Rv,Rwrel)"
    unfolding rel_def
    by tagged_solver

  lemmas [autoref_rel_intf] = REL_INTFI[of rel i_graph]
end

lemma (in graph_nodes_it) autoref_nodes_it[autoref_rules]: 
  assumes ID: "PREFER_id Rv"
  shows "(λs. RETURN (it_to_list nodes_it s),nodes_to_list)  Rv,Rwrel  Rvlist_relnres_rel"
  unfolding nodes_to_list_def[abs_def]
proof (intro fun_relI nres_relI)
  fix s s'
  from ID have [simp]: "Rv = Id" by simp

  assume "(s,s')Rv,Rwrel"
  hence INV: "invar s" and [simp]: "nodes s' = nodes (α s)" unfolding rel_def 
    by (auto simp add: br_def graph_rel_def)

  obtain l where 
    [simp]: "distinct l" "nodes (α s) = set l" "it_to_list nodes_it s = l" 
    unfolding it_to_list_def
    by (metis nodes_it_correct[OF INV, unfolded set_iterator_def set_iterator_genord_def] 
      foldli_snoc_id self_append_conv2)
  
  show "RETURN (it_to_list nodes_it s)
            (Rvlist_rel) (it_to_sorted_list (λ_ _. True) (nodes s'))"
    by (simp add: it_to_sorted_list_def)
qed


lemma (in graph_succ_it) autoref_succ_it[autoref_rules]: 
  assumes ID: "PREFER_id Rv" "PREFER_id Rw"
  shows "(λs v. RETURN (it_to_list (λs. succ_it s v) s),succ_to_list) 
     Rv,Rwrel  Rv  Rw,Rvprod_rellist_relnres_rel"
  unfolding succ_to_list_def[abs_def]
proof (intro fun_relI nres_relI)
  fix s s' v v'
  from ID have [simp]: "Rv = Id" "Rw=Id" by simp_all

  assume "(v,v')Rv" hence [simp]: "v'=v" by simp

  assume "(s,s')Rv,Rwrel"
  hence INV: "invar s" and [simp]: "Graph.succ s' = Graph.succ (α s)" unfolding rel_def 
    by (auto simp add: br_def graph_rel_def succ_def)

  obtain l where 
    [simp]: "distinct l" "succ (α s) v = set l" "it_to_list (λs. succ_it s v) s = l" 
    unfolding it_to_list_def
    by (metis succ_it_correct[OF INV, unfolded set_iterator_def set_iterator_genord_def] 
      foldli_snoc_id self_append_conv2)
  
  show "RETURN (it_to_list (λs. succ_it s v) s)
            (Rw,Rvprod_rellist_rel) (it_to_sorted_list (λ_ _. True) (succ s' v'))"
    by (simp add: it_to_sorted_list_def)
qed

subsection ‹Refinement›

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" 
begin
end

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 and g :: 'G+
  assumes ga_trans: "(g,ga)br g.α g.invar"
begin
  abbreviation "v_rel  Id :: ('V×'V) set"
  abbreviation "w_rel  Id :: ('W×'W) set"

  definition i_node :: interface where "i_node  undefined"
  definition i_weight :: interface where "i_weight  undefined"

  lemmas [autoref_rel_intf] = REL_INTFI[of v_rel i_node]
  lemmas [autoref_rel_intf] = REL_INTFI[of w_rel i_weight]
  
  lemma weight_plus_autoref[autoref_rules]: 
    "(0,0)  w_rel"
    "((+),(+))  w_rel  w_rel  w_rel" 
    "((+),(+))  w_relinfty_rel  w_relinfty_rel  w_relinfty_rel" 
    "((<),(<))  w_relinfty_rel  w_relinfty_rel  bool_rel" 
    by simp_all

  lemma [autoref_rules]: "(g,ga)v_rel,w_relg.rel" using ga_trans
    by (simp add: g.rel_def)
   
  lemma [autoref_rules]: "(v0,v0)v_rel" by simp

  term mpath_weight'
  lemma [autoref_rules]: 
    "(mpath_weight',mpath_weight') 
       v_rel×rw_rel×rv_rellist_rel×rw_reloption_rel  w_relinfty_rel"
    "(mpath', mpath') 
       v_rel×rw_rel×rv_rellist_rel×rw_reloption_rel 
         v_rel×rw_rel×rv_rellist_reloption_rel"
    by auto

  term mdinit

  lemmas [autoref_tyrel] = 
    ty_REL[where R=v_rel]
    ty_REL[where R=w_rel]
    ty_REL[where R="w_relinfty_rel"]
    ty_REL[where R="v_rel,w_relinfty_relqw.rel"]
    ty_REL[where R="v_rel,v_rel×rw_rel×rv_rellist_rel×rw_relmr.rel"]
    ty_REL[where R="v_rel×rw_rel×rv_rellist_rel"]
    
  lemmas [autoref_op_pat] = uprio_pats[where 'e = 'V and 'a = "'W infty"]


  schematic_goal cdijkstra_refines_aux:
    shows "(?c::?'c, 
      mdijkstra
    )  ?R"
    apply (simp only: mdijkstra_def mdinit_def mpop_min_def[abs_def] mupdate_def)

    using [[goals_limit = 1]]

    apply (fold op_map_empty_def[where 'a="'V" and 'b = "('V×'W×'V) list × 'W"])
    apply (fold op_uprio_empty_def[where 'a="'V" and 'b = "'W infty"])

    (*using [[autoref_trace_intf_unif]]*)
    using [[autoref_trace_failed_id]]
  
    apply (autoref_monadic (plain,trace))
    done

end

context dijkstraC 
begin

  concrete_definition cdijkstra for g ?v0.0  
    uses dijkstraC_fixg.cdijkstra_refines_aux
    [of g_ops mr_ops qw_ops]

    term cdijkstra
end

context dijkstraC_fixg
begin

  term cdijkstra
  term mdijkstra

  lemma cdijkstra_refines: 
    "RETURN (cdijkstra g v0)  (build_rel mr.α mr.invar) mdijkstra"
    apply (rule cdijkstra.refine[THEN nres_relD, simplified])
    apply unfold_locales
    done

  theorem cdijkstra_correct:
    shows
    "weighted_graph.is_shortest_path_map ga v0 (αr (mr.α (cdijkstra g v0)))"
    (is ?G1)
    and "mr.invar (cdijkstra g v0)" (is ?G2) 
    and "res_invarm (mr.α (cdijkstra g v0))" (is ?G3)
  proof -
    note cdijkstra_refines
    also note mdijkstra_refines
    finally have Z: "RETURN (cdijkstra g v0)  
      (build_rel (αr  mr.α) (λm. mr.invar m  res_invarm (mr.α m))) 
        dijkstra'"
      apply (subst (asm) conc_fun_chain)
      apply (simp only: br_chain)
      done
    also note dijkstra'_refines[simplified]
    also note dijkstra_correct 
    finally show ?G1 ?G2 ?G3 
      by (auto elim: RETURN_ref_SPECD simp: refine_rel_defs)
  qed

end

theorem (in dijkstraC) cdijkstra_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"
  shows 
  "weighted_graph.is_shortest_path_map (g.α g) v0 
      (Dijkstra.αr (mr.α (cdijkstra g v0)))" (is ?G1)
  and "Dijkstra.res_invarm (mr.α (cdijkstra g v0))" (is ?G2)
proof -
  interpret hlgv: valid_graph "g.α g" using g.valid INV .

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

  from dc.cdijkstra_correct show ?G1 ?G2 by auto
qed

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.cdijkstra"
lemmas hrf_dijkstra_correct = hrf.cdijkstra_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 checking SML

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

end