Theory Prim_Impl

section ‹Implementation of Prim's Algorithm›
theory Prim_Impl
imports 
  Prim_Abstract
  Undirected_Graph_Impl
  "HOL-Library.While_Combinator"
  "Priority_Search_Trees.PST_RBT"
  "HOL-Data_Structures.RBT_Map"
begin


subsection ‹Implementation using ADT Interfaces\label{sec:prim_data_structs}›

locale Prim_Impl_Adts = 
  G: adt_wgraph G_αw G_αg G_invar G_adj G_empty G_add_edge 
+ M: Map M_empty M_update M_delete M_lookup M_invar
(*+ S: Set S_empty S_insert S_delete S_isin S_α S_invar*)
+ Q: PrioMap Q_empty Q_update Q_delete Q_invar Q_lookup Q_is_empty Q_getmin
  
  for typG :: "'g itself" and typM :: "'m itself" and typQ :: "'q itself"
  and G_αw and G_αg :: "'g ⇒ ('v) ugraph" and G_invar G_adj G_empty G_add_edge
  
  and M_empty M_update M_delete and M_lookup :: "'m ⇒ 'v ⇒ 'v option" and M_invar
  
  and Q_empty Q_update Q_delete Q_invar and Q_lookup :: "'q ⇒ 'v ⇒ nat option" 
  and Q_is_empty Q_getmin
  
begin

text ‹Simplifier setup›
lemmas [simp] = G.wgraph_specs
lemmas [simp] = M.map_specs
lemmas [simp] = Q.prio_map_specs

end  

locale Prim_Impl_Defs = Prim_Impl_Adts  
  where typG = typG and typM = typM and typQ = typQ and G_αw = G_αw and G_αg = G_αg
  for typG :: "'g itself" and typM :: "'m itself" and typQ :: "'q itself" 
  and G_αw and G_αg :: "'g ⇒ ('v::linorder) ugraph" and g :: 'g and r :: 'v
begin
  
subsubsection ‹Concrete Algorithm›
term M_lookup
definition "foreach_impl_body u ≡ (λ(v,d) (Qi,πi).
  if v=r then (Qi,πi)
  else 
    case (Q_lookup Qi v, M_lookup πi v) of
      (None,None) ⇒ (Q_update v d Qi, M_update v u πi)
    | (Some d',_) ⇒ (if d<d' then (Q_update v d Qi, M_update v u πi) else (Qi,πi))
    | (None, Some _) ⇒ (Qi,πi)
  )"

definition foreach_impl :: "'q ⇒ 'm ⇒ 'v ⇒ ('v×nat) list ⇒ 'q × 'm" where
  "foreach_impl Qi πi u adjs = foldr (foreach_impl_body u) adjs (Qi,πi)"


definition "outer_loop_impl Qi πi ≡ while (λ(Qi,πi). ¬Q_is_empty Qi) (λ(Qi,πi). 
  let
    (u,_) = Q_getmin Qi;
    adjs = G_adj g u;
    (Qi,πi) = foreach_impl Qi πi u adjs;
    Qi = Q_delete u Qi
  in (Qi,πi)) (Qi,πi)"

definition "prim_impl = (let
  Qi = Q_update r 0 Q_empty;
  πi = M_empty;
  (Qi,πi) = outer_loop_impl Qi πi
  in πi)
"

text ‹The whole algorithm as one function›
lemma prim_impl_alt: "prim_impl = (let 
  ― ‹Initialization›
  (Q,π) = (Q_update r 0 Q_empty, M_empty);
  ― ‹Main loop: Iterate until PQ is empty›
  (Q, π) = 
  while (λ(Q, π). ¬ Q_is_empty Q) (λ(Q, π). let 
    (u, _) = Q_getmin Q;
    ― ‹Inner loop: Update for adjacent nodes›
    (Q, π) = 
    foldr ((λ(v, d) (Q, π). let
        qv = Q_lookup Q v;
        πv = M_lookup π v
      in
        if v≠r ∧ (qv≠None ∨ πv=None) ∧ enat d < enat_of_option qv 
        then (Q_update v d Q, M_update v u π) 
        else (Q, π))
    ) (G_adj g u) (Q, π); 
    Q = Q_delete u Q
    in (Q, π)) (Q, π)
  in π
)"
proof -

  have 1: "foreach_impl_body u = (λ(v,d) (Qi,πi). let
        qiv = (Q_lookup Qi v);
        πiv = M_lookup πi v
      in
        if v≠r ∧ (qiv≠None ∨ πiv=None) ∧ enat d < enat_of_option qiv 
        then (Q_update v d Qi, M_update v u πi) 
        else (Qi, πi))" for u
    unfolding foreach_impl_body_def
    apply (intro ext)
    by (auto split: option.split)
    
  show ?thesis
    unfolding prim_impl_def outer_loop_impl_def foreach_impl_def 1
    by (simp)
qed  
  

subsubsection ‹Abstraction of Result›

text ‹Invariant for the result, and its interpretation as (minimum spanning) tree:
  ▪ The map ‹πi› and set ‹Vi› satisfy their implementation invariants
  ▪ The ‹πi› encodes irreflexive edges consistent with the nodes determined 
    by ‹Vi›. Note that the edges in ‹πi› will not be symmetric, thus we take 
    their symmetric closure ‹E∪E¯›.
    
›
  
definition "invar_MST πi ≡ M_invar πi"

definition "α_MST πi ≡ graph {r} {(u,v) | u v. M_lookup πi u = Some v}"

end


subsection ‹Refinement of State›

locale Prim_Impl = Prim_Impl_Defs 
  where typG = typG and typM = typM and typQ = typQ and G_αw = G_αw and G_αg = G_αg
  for typG :: "'g itself" and typM :: "'m itself" and typQ :: "'q itself" 
  and G_αw and G_αg :: "'g ⇒ ('v::linorder) ugraph" 
  +
  assumes G_invar[simp]: "G_invar g"
begin
               
sublocale Prim2 "G_αw g" "G_αg g" r .

subsubsection ‹Abstraction of ‹Q››
text ‹The priority map implements a function of type @{typ ‹'v⇒enat›}, 
  mapping @{const None} to @{term ∞}.
›

definition "Q_α Qi ≡ enat_of_option o Q_lookup Qi :: 'v ⇒ enat"

lemma Q_α_empty: "Q_α Q_empty = (λ_. ∞)"
  unfolding Q_α_def by (auto)

lemma Q_α_update: "Q_invar Q ⟹ Q_α (Q_update u d Q) = (Q_α Q)(u := enat d)"
  unfolding Q_α_def by (auto)

lemma Q_α_is_empty: "Q_invar Q ⟹ Q_lookup Q = Map.empty ⟷ Q_α Q = (λ_. ∞)"
  unfolding Q_α_def by (auto simp: fun_eq_iff)

lemma Q_α_delete: "Q_invar Q ⟹ Q_α (Q_delete u Q) = (Q_α Q)(u:=∞)"
  unfolding Q_α_def by (auto simp: fun_eq_iff)

lemma Q_α_min:
  assumes MIN: "Q_getmin Qi = (u, d)"
  assumes I: "Q_invar Qi"
  assumes NE: "¬ Q_is_empty Qi"
  shows "Q_α Qi u = enat d" (is ?G1) and
        "∀v. enat d ≤ Q_α Qi v" (is ?G2)
proof -
  from Q.map_getmin[OF MIN] 
    have "Q_lookup Qi u = Some d" "(∀x∈ran (Q_lookup Qi). d ≤ x)"
    using NE I by auto
  thus "?G1" "?G2"
    unfolding Q_α_def apply simp_all
    by (metis enat_of_option.elims enat_ord_simps(1) enat_ord_simps(3) ranI)
qed


lemmas Q_α_specs = Q_α_empty Q_α_update Q_α_is_empty Q_α_delete


subsubsection ‹Concrete Invariant›

text ‹The implementation invariants of the concrete state's components,
  and the abstract invariant of the state's abstraction›
definition "prim_invar_impl Qi πi ≡ 
    Q_invar Qi ∧ M_invar πi ∧ prim_invar2 (Q_α Qi) (M_lookup πi)"


end


subsection ‹Refinement of Algorithm›

context Prim_Impl
begin

lemma foreach_impl_correct:
  fixes Qi Vi πi defines "Q ≡ Q_α Qi" and "π ≡ M_lookup πi"
  assumes A: "foreach_impl Qi πi u (G_adj g u) = (Qi',πi')" 
  assumes I: "prim_invar_impl Qi πi"
  shows "Q_invar Qi'" and "M_invar πi'" 
    and "Q_α Qi' = Qinter Q π u" and "M_lookup πi' = π' Q π u"
proof -
  from I have [simp]: "Q_invar Qi" "M_invar πi" 
    unfolding prim_invar_impl_def Q_def π_def by auto

  {
    fix Qi πi d v and adjs :: "('v × nat) list"
    assume "Q_invar Qi" "M_invar πi" "(v, d) ∈ set adjs"
    then have 
      "(case foreach_impl_body u (v, d) (Qi, πi) of 
         (Qi, πi) ⇒ Q_invar Qi ∧ M_invar πi) 
              ∧ map_prod Q_α M_lookup (foreach_impl_body u (v, d) (Qi, πi)) 
                = foreach_body u (v, d) (Q_α Qi, M_lookup πi)"
      unfolding foreach_impl_body_def foreach_body_def  
      unfolding Q_α_def
      by (auto simp: fun_eq_iff split: option.split)

  } note aux=this

  from foldr_refine[
    where I="λ(Qi,πi). Q_invar Qi ∧ M_invar πi" and α="map_prod Q_α M_lookup",
    of "(Qi,πi)" "(G_adj g u)" "foreach_impl_body u" "foreach_body u"
    ]
  and A aux[where ?adjs3="(G_adj g u)"] 
    have "Q_invar Qi'" "M_invar πi'" 
      and 1: "foreach u (G_adj g u) (Q_α Qi, M_lookup πi) 
              = (Q_α Qi', M_lookup πi')"
    unfolding foreach_impl_def foreach_def 
    unfolding Q_def π_def
    by (auto split: prod.splits) 
  then show "Q_invar Qi'" "M_invar πi'" by auto

  from 1 foreach_refine[where adjs="G_adj g u" and u=u] show 
    "Q_α Qi' = Qinter Q π u" and "M_lookup πi' = π' Q π u"
    by (auto simp: Q_def π_def)
    
qed

(*<*)
lemma foreach_impl_correct_presentation:
  fixes Qi Vi πi defines "Q ≡ Q_α Qi" and "π ≡ M_lookup πi"
  assumes A: "foreach_impl Qi πi u (G_adj g u) = (Qi',πi')" 
  assumes I: "prim_invar_impl Qi πi"
  shows "Q_invar Qi' ∧ M_invar πi' 
        ∧ Q_α Qi' = Qinter Q π u ∧ M_lookup πi' = π' Q π u"
  using foreach_impl_correct assms by blast
(*>*)  

definition "T_measure_impl ≡ λ(Qi,πi). T_measure2 (Q_α Qi) (M_lookup πi)"

lemma prim_invar_impl_init: "prim_invar_impl (Q_update r 0 Q_empty) M_empty"
  using invar2_init 
  by (auto simp: prim_invar_impl_def Q_α_specs initQ_def initπ_def zero_enat_def)
  
lemma maintain_prim_invar_impl:  
  assumes 
      I: "prim_invar_impl Qi πi" and
      NE: "¬ Q_is_empty Qi" and
      MIN: "Q_getmin Qi = (u, d)" and
      FOREACH: "foreach_impl Qi πi u (G_adj g u) = (Qi', πi')"
  shows "prim_invar_impl (Q_delete u Qi') πi'" (is ?G1)
     and "T_measure_impl (Q_delete u Qi', πi') < T_measure_impl (Qi,πi)" (is "?G2")
proof -
  note II[simp] = I[unfolded prim_invar_impl_def]
  note FI[simp] = foreach_impl_correct[OF FOREACH I]
  note MIN' = Q_α_min[OF MIN _ NE, simplified]

  show ?G1 
    unfolding prim_invar_impl_def
    using Q_α_delete maintain_invar2[OF _ MIN'] 
    by (simp add: Q'_def)

  show ?G2
    unfolding prim_invar_impl_def T_measure_impl_def
    using Q_α_delete maintain_invar2[OF _ MIN'] 
    apply (simp add: Q'_def Q_α_def)
    by (metis FI(3) II Q'_def Q_α_def 
        ‹⋀π. prim_invar2 (Q_α Qi) π 
            ⟹ T_measure2 (Q' (Q_α Qi) π u) (π' (Q_α Qi) π u) 
                < T_measure2 (Q_α Qi) π›)
    
qed      

lemma maintain_prim_invar_impl_presentation:  
  assumes 
      I: "prim_invar_impl Qi πi" and
      NE: "¬ Q_is_empty Qi" and
      MIN: "Q_getmin Qi = (u, d)" and
      FOREACH: "foreach_impl Qi πi u (G_adj g u) = (Qi', πi')"
  shows "prim_invar_impl (Q_delete u Qi') πi'
       ∧ T_measure_impl (Q_delete u Qi', πi') < T_measure_impl (Qi,πi)"
  using maintain_prim_invar_impl assms by blast

lemma prim_invar_impl_finish:
  "⟦Q_is_empty Q; prim_invar_impl Q π⟧ 
    ⟹ invar_MST π ∧ is_MST (G_αw g) rg (α_MST π)"
  using invar2_finish
  by (auto simp: Q_α_specs prim_invar_impl_def invar_MST_def α_MST_def Let_def)
  
lemma prim_impl_correct:
  assumes "prim_impl = πi"
  shows 
    "invar_MST πi" (is ?G1)
    "is_MST (G_αw g) (component_of (G_αg g) r) (α_MST πi)" (is ?G2)
proof -
  have "let (Qi, πi) = outer_loop_impl (Q_update r 0 Q_empty) M_empty in 
    invar_MST πi ∧ is_MST (G_αw g) rg (α_MST πi)"
    unfolding outer_loop_impl_def
    apply (rule while_rule[where 
      P="λ(Qi,πi). prim_invar_impl Qi πi" and r="measure T_measure_impl"])
    apply (all ‹clarsimp split: prod.splits simp: Q_α_specs›)
    apply (simp_all add: prim_invar_impl_init maintain_prim_invar_impl 
                         prim_invar_impl_finish)
    done
  with assms show ?G1 ?G2 
    unfolding rg_def prim_impl_def by (simp_all split: prod.splits)
qed    

(*<*)
lemma prim_impl_correct_presentation:
  "invar_MST prim_impl 
  ∧ is_MST (G_αw g) (component_of (G_αg g) r) (α_MST prim_impl)"
  using prim_impl_correct by blast
(*>*)  
    
end


subsection ‹Instantiation with Actual Data Structures\label{sec:prim_inst_ds}›

global_interpretation 
  G: wgraph_by_map RBT_Set.empty RBT_Map.update RBT_Map.delete 
        Lookup2.lookup RBT_Map.M.invar
  defines G_empty = G.empty
      and G_add_edge = G.add_edge
      and G_add_edge1 = G.add_edge1
      and G_adj = G.adj
      and G_from_list = G.from_list
      and G_valid_wgraph_repr = G.valid_wgraph_repr
  by unfold_locales

(* FIXME: Something is strange with generated constants. *)
lemma G_from_list_unfold:  "G_from_list = G.from_list"
  by (simp add: G_add_edge_def G_empty_def G_from_list_def)
  
(* FIXME: The interpretation does not generate a code theorem at all!? *)
lemma [code]: "G_from_list l = foldr (λ(e, d). G_add_edge e d) l G_empty"
  by (simp add: G.from_list_def G_from_list_unfold)
  
  
global_interpretation Prim_Impl_Adts _ _ _
  G.αw G.αg G.invar G.adj G.empty G.add_edge
  
  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
  
  PST_RBT.empty PST_RBT.update PST_RBT.delete PST_RBT.PM.invar 
  Lookup2.lookup PST_RBT.rbt_is_empty pst_getmin
  ..

global_interpretation P: Prim_Impl_Defs G.invar G.adj G.empty G.add_edge
  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
  
  PST_RBT.empty PST_RBT.update PST_RBT.delete PST_RBT.PM.invar 
  Lookup2.lookup PST_RBT.rbt_is_empty pst_getmin
  
  _ _ _ G.αw G.αg g r  
  for g and r::"'a::linorder"
  defines prim_impl = P.prim_impl
      and outer_loop_impl = P.outer_loop_impl
      and foreach_impl = P.foreach_impl
      and foreach_impl_body = P.foreach_impl_body
  by unfold_locales 


lemmas [code] = P.prim_impl_alt  
  
  
context
  fixes g
  assumes [simp]: "G.invar g"  
begin  
  
interpretation AUX: Prim_Impl
  G.invar G.adj G.empty G.add_edge
  
  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
  
  PST_RBT.empty PST_RBT.update PST_RBT.delete PST_RBT.PM.invar 
  Lookup2.lookup PST_RBT.rbt_is_empty pst_getmin
  
  g r _ _ _ G.αw G.αg for r::"'a::linorder"
  by unfold_locales simp_all
  
lemmas prim_impl_correct = AUX.prim_impl_correct[folded prim_impl_def] 
  
end  

subsubsection ‹Adding a Graph-From-List Parser›
  
definition "prim_list_impl l r 
  ≡ if G_valid_wgraph_repr l then Some (prim_impl (G_from_list l) r) else None"

  
subsection ‹Main Correctness Theorem›
  
text ‹
  The @{const prim_list_impl} algorithm returns @{const None}, if the input was 
  invalid. Otherwise it returns @{term ‹Some (πi,Vi)›}, which satisfy the 
  map/set invariants and encode a minimum spanning tree of the component of the
  graph that contains ‹r›.
  
  Notes:
    ▪ If ‹r› is n ot a node of the graph, ‹component_of› will return the graph
      with the only node ‹r›. (@{thm [source] component_of_not_node})
›
  
theorem prim_list_impl_correct:
  shows "case prim_list_impl l r of 
    None ⇒ ¬G.valid_wgraph_repr l ― ‹Invalid input›
  | Some πi ⇒ 
        G.valid_wgraph_repr l ∧ (let Gi = G.from_list l in G.invar Gi ― ‹Valid input›
        ∧ P.invar_MST πi ― ‹Output satisfies invariants›
        ∧ is_MST (G.αw Gi) (component_of (G.αg Gi) r) (P.α_MST r πi)) ― ‹and represents MST›"
  unfolding prim_list_impl_def G_from_list_unfold
  using prim_impl_correct[of "G.from_list l" r] G.from_list_correct[of l]
  by (auto simp: Let_def)

theorem prim_list_impl_correct_presentation:
  shows "case prim_list_impl l r of 
    None ⇒ ¬G.valid_wgraph_repr l ― ‹Invalid input›
  | Some πi ⇒ let 
      g=G.αg (G.from_list l); 
      w=G.αw (G.from_list l); 
      rg=component_of g r;
      t=P.α_MST r πi
    in 
        G.valid_wgraph_repr l ― ‹Valid input› 
      ∧ P.invar_MST πi ― ‹Output satisfies invariants›
      ∧ is_MST w rg t ― ‹and represents MST›"
  using prim_list_impl_correct[of l r] unfolding Let_def 
  by (auto split: option.splits)
  
      
subsection ‹Code Generation and Test\label{sec:prim_exec}›

definition prim_list_impl_int :: "_ ⇒ int ⇒ _" 
  where "prim_list_impl_int ≡ prim_list_impl"


export_code prim_list_impl prim_list_impl_int checking SML


experiment begin

                                  
abbreviation "a ≡ 1"
abbreviation "b ≡ 2"
abbreviation "c ≡ 3"
abbreviation "d ≡ 4"
abbreviation "e ≡ 5"
abbreviation "f ≡ 6"
abbreviation "g ≡ 7"
abbreviation "h ≡ 8"
abbreviation "i ≡ 9"


value "(prim_list_impl_int [
  ((a,b),4),
  ((a,h),8),
  ((b,h),11),
  ((b,c),8),
  ((h,i),7),
  ((h,g),1),
  ((c,i),2),
  ((g,i),6),
  ((c,d),7),
  ((c,f),4),
  ((g,f),2),
  ((d,f),14),
  ((d,e),9),
  ((e,f),10)
] 1)"

end




end