Theory Dijkstra_Abstract

section ‹Abstract Dijkstra Algorithm›
theory Dijkstra_Abstract
imports Directed_Graph
begin

subsection ‹Abstract Algorithm›

type_synonym 'v estimate = "'v ⇒ enat"
text ‹We fix a start node and a weighted graph›
locale Dijkstra = WGraph w for w :: "('v) wgraph" +
  fixes s :: 'v
begin

text ‹Relax all outgoing edges of node ‹u››
definition relax_outgoing :: "'v ⇒ 'v estimate ⇒ 'v estimate"
  where "relax_outgoing u D ≡ λv. min (D v) (D u + w (u,v))"

text ‹Initialization›
definition "initD ≡ (λ_. ∞)(s:=0)"
definition "initS ≡ {}"  
  
      
text ‹Relaxing will never increase estimates›
lemma relax_mono: "relax_outgoing u D v ≤ D v"
  by (auto simp: relax_outgoing_def)


definition "all_dnodes ≡ Set.insert s { v . ∃u. w (u,v)≠∞ }"
definition "unfinished_dnodes S ≡ all_dnodes - S "

lemma unfinished_nodes_subset: "unfinished_dnodes S ⊆ all_dnodes"
  by (auto simp: unfinished_dnodes_def)

end  

subsubsection ‹Invariant›
text ‹The invariant is defined as locale›
  
locale Dijkstra_Invar = Dijkstra w s for w and s :: 'v +
  fixes D :: "'v estimate" and S :: "'v set"
  assumes upper_bound: ‹δ s u ≤ D u› ― ‹‹D› is a valid estimate›
  assumes s_in_S: ‹s∈S ∨ (D=(λ_. ∞)(s:=0) ∧ S={})› ― ‹The start node is 
    finished, or we are in initial state›  
  assumes S_precise: "u∈S ⟹ D u = δ s u" ― ‹Finished nodes have precise 
    estimate›
  assumes S_relaxed: ‹v∈S ⟹ D u ≤ δ s v + w (v,u)› ― ‹Outgoing edges of 
    finished nodes have been relaxed, using precise distance›
begin

abbreviation (in Dijkstra) "D_invar ≡ Dijkstra_Invar w s"

text ‹The invariant holds for the initial state›  
theorem (in Dijkstra) invar_init: "D_invar initD initS"
  apply unfold_locales
  unfolding initD_def initS_def
  by (auto simp: relax_outgoing_def distance_direct)


text ‹Relaxing some edges maintains the upper bound property›    
lemma maintain_upper_bound: "δ s u ≤ (relax_outgoing v D) u"
  apply (clarsimp simp: relax_outgoing_def upper_bound split: prod.splits)
  using triangle upper_bound add_right_mono dual_order.trans by blast

text ‹Relaxing edges will not affect nodes with already precise estimates›
lemma relax_precise_id: "D v = δ s v ⟹ relax_outgoing u D v = δ s v"
  using maintain_upper_bound upper_bound relax_mono
  by (metis antisym)

text ‹In particular, relaxing edges will not affect finished nodes›  
lemma relax_finished_id: "v∈S ⟹ relax_outgoing u D v = D v"
  by (simp add: S_precise relax_precise_id)  
      
text ‹The least (finite) estimate among all nodes ‹u› not in ‹S› is already precise.
  This will allow us to add the node ‹u› to ‹S›. ›
lemma maintain_S_precise_and_connected:  
  assumes UNS: "u∉S"
  assumes MIN: "∀v. v∉S ⟶ D u ≤ D v"
  shows "D u = δ s u"
  text ‹We start with a case distinction whether we are in the first 
    step of the loop, where we process the start node, or in subsequent steps,
    where the start node has already been finished.›
proof (cases "u=s")  
  assume [simp]: "u=s" ― ‹First step of loop›
  then show ?thesis using ‹u∉S› s_in_S by simp
next
  assume ‹u≠s› ― ‹Later step of loop›
  text ‹The start node has already been finished›   
  with s_in_S MIN have ‹s∈S› apply clarsimp using infinity_ne_i0 by metis
  
  show ?thesis
  text ‹Next, we handle the case that ‹u› is unreachable.›
  proof (cases ‹δ s u < ∞›)
    assume "¬(δ s u < ∞)" ― ‹Node is unreachable (infinite distance)›
    text ‹By the upper-bound property, we get ‹D u = δ s u = ∞››
    then show ?thesis using upper_bound[of u] by auto
  next
    assume "δ s u < ∞" ― ‹Main case: Node has finite distance›
 
    text ‹Consider a shortest path from ‹s› to ‹u››        
    obtain p where "path s p u" and DSU: "δ s u = sum_list p"
      by (rule obtain_shortest_path)
    text ‹It goes from inside ‹S› to outside ‹S›, so there must be an edge at the border.
      Let ‹(x,y)› be such an edge, with ‹x∈S› and ‹y∉S›.›
    from find_leave_edgeE[OF ‹path s p u› ‹s∈S› ‹u∉S›] obtain p1 x y p2 where
      [simp]: "p = p1 @ w (x, y) # p2" 
      and DECOMP: "x ∈ S" "y ∉ S" "path s p1 x" "path y p2 u" .
    text ‹As prefixes of shortest paths are again shortest paths, the shortest 
          path to ‹y› ends with edge ‹(x,y)› ›  
    have DSX: "δ s x = sum_list p1" and DSY: "δ s y = δ s x + w (x, y)"
      using shortest_path_prefix[of s p1 x "w (x,y)#p2" u] 
        and shortest_path_prefix[of s "p1@[w (x,y)]" y p2 u]
        and ‹δ s u < ∞› DECOMP 
        by (force simp: DSU)+
    text ‹Upon adding ‹x› to ‹S›, this edge has been relaxed with the precise
       estimate for ‹x›. At this point the estimate for ‹y› has become 
       precise, too›  
    with ‹x∈S› have "D y = δ s y"  
      by (metis S_relaxed antisym_conv upper_bound)
    moreover text ‹The shortest path to ‹y› is a prefix of that to ‹u›, thus 
      it shorter or equal›
    have "… ≤ δ s u" using DSU by (simp add: DSX DSY)
    moreover text ‹The estimate for ‹u› is an upper bound›
    have "… ≤ D u" using upper_bound by (auto)
    moreover text ‹‹u› was a node with smallest estimate›
    have "… ≤ D y" using ‹u∉S› ‹y∉S› MIN by auto
    ultimately text ‹This closed a cycle in the inequation chain. Thus, by 
      antisymmetry, all items are equal. In particular, ‹D u = δ s u›, qed.›
    show "D u = δ s u" by simp
  qed    
qed
  
text ‹A step of Dijkstra's algorithm maintains the invariant.
  More precisely, in a step of Dijkstra's algorithm, 
  we pick a node ‹u∉S› with least finite estimate, relax the outgoing 
  edges of ‹u›, and add ‹u› to ‹S›.›    
theorem maintain_D_invar:
  assumes UNS: "u∉S"
  assumes UNI: "D u < ∞"
  assumes MIN: "∀v. v∉S ⟶ D u ≤ D v"
  shows "D_invar (relax_outgoing u D) (Set.insert u S)"
  apply (cases ‹s∈S›)
  subgoal
    apply (unfold_locales)
    subgoal by (simp add: maintain_upper_bound)
    subgoal by simp
    subgoal 
      using maintain_S_precise_and_connected[OF UNS MIN] S_precise        
      by (auto simp: relax_precise_id) 
    subgoal
      using maintain_S_precise_and_connected[OF UNS MIN]
      by (auto simp: relax_outgoing_def S_relaxed min.coboundedI1)
    done
  subgoal
    apply unfold_locales
    using s_in_S UNI distance_direct 
    by (auto simp: relax_outgoing_def split: if_splits)
  done
  

text ‹When the algorithm is finished, i.e., when there are 
  no unfinished nodes with finite estimates left,
  then all estimates are accurate.›  
lemma invar_finish_imp_correct:
  assumes F: "∀u. u∉S ⟶ D u = ∞"
  shows "D u = δ s u"
proof (cases "u∈S")
  assume "u∈S" text ‹The estimates of finished nodes are accurate›
  then show ?thesis using S_precise by simp
next
  assume ‹u∉S› text ‹‹D u› is minimal, and minimal estimates are precise›
  then show ?thesis 
    using F maintain_S_precise_and_connected[of u] by auto
  
qed  
  
  
text ‹A step decreases the set of unfinished nodes.›
lemma unfinished_nodes_decr:
  assumes UNS: "u∉S"
  assumes UNI: "D u < ∞"
  shows "unfinished_dnodes (Set.insert u S) ⊂ unfinished_dnodes S"
proof -
  text ‹There is a path to ‹u››
  from UNI have "δ s u < ∞" using upper_bound[of u] leD by fastforce
  
  text ‹Thus, ‹u› is among ‹all_dnodes››
  have "u∈all_dnodes" 
  proof -
    obtain p where "path s p u" "sum_list p < ∞"
      apply (rule obtain_shortest_path[of s u])
      using ‹δ s u < ∞› by auto
    with ‹u∉S› show ?thesis 
      apply (cases p rule: rev_cases) 
      by (auto simp: Dijkstra.all_dnodes_def)
  qed
  text ‹Which implies the proposition›
  with ‹u∉S› show ?thesis by (auto simp: unfinished_dnodes_def)
qed
  
        
end  


subsection ‹Refinement by Priority Map and Map›
text ‹
  In a second step, we implement ‹D› and ‹S› by a priority map ‹Q› and a map ‹V›.
  Both map nodes to finite weights, where ‹Q› maps unfinished nodes, and ‹V› 
  maps finished nodes.

  Note that this implementation is slightly non-standard: 
  In the standard implementation, ‹Q› contains also unfinished nodes with 
  infinite weight.
  
  We chose this implementation because it avoids enumerating all nodes of 
  the graph upon initialization of ‹Q›.
  However, on relaxing an edge to a node not in ‹Q›, we require an extra 
  lookup to check whether the node is finished. 
›  

subsubsection ‹Implementing ‹enat› by Option›

text ‹Our maps are functions to ‹nat option›,which are interpreted as ‹enat›,
  ‹None› being ‹∞››

fun enat_of_option :: "nat option ⇒ enat" where
  "enat_of_option None = ∞" 
| "enat_of_option (Some n) = enat n"  
  
lemma enat_of_option_inj[simp]: "enat_of_option x = enat_of_option y ⟷ x=y"
  by (cases x; cases y; simp)

lemma enat_of_option_simps[simp]:
  "enat_of_option x = enat n ⟷ x = Some n"
  "enat_of_option x = ∞ ⟷ x = None"
  "enat n = enat_of_option x ⟷ x = Some n"
  "∞ = enat_of_option x ⟷ x = None"
  by (cases x; auto; fail)+
  
lemma enat_of_option_le_conv: 
  "enat_of_option m ≤ enat_of_option n ⟷ (case (m,n) of 
      (_,None) ⇒ True
    | (Some a, Some b) ⇒ a≤b
    | (_, _) ⇒ False
  )"
  by (auto split: option.split)

  
  
subsubsection ‹Implementing ‹D,S› by Priority Map and Map›
context Dijkstra begin

text ‹We define a coupling relation, that connects the concrete with the 
  abstract data. ›
definition "coupling Q V D S ≡ 
  D = enat_of_option o (V ++ Q)
∧ S = dom V
∧ dom V ∩ dom Q = {}"

text ‹Note that our coupling relation is functional.›
(* TODO: Why not use functions instead? *)
lemma coupling_fun: "coupling Q V D S ⟹ coupling Q V D' S' ⟹ D'=D ∧ S'=S"
  by (auto simp: coupling_def)

text ‹The concrete version of the invariant.›  
definition "D_invar' Q V ≡
  ∃D S. coupling Q V D S ∧ D_invar D S"

  
text ‹Refinement of ‹relax-outgoing››

definition "relax_outgoing' u du V Q v ≡ 
  case w (u,v) of
    ∞ ⇒ Q v
  | enat d ⇒ (case Q v of
      None ⇒ if v∈dom V then None else Some (du+d)
    | Some d' ⇒ Some (min d' (du+d)))
"

  
text ‹A step preserves the coupling relation.›
lemma (in Dijkstra_Invar) coupling_step:
  assumes C: "coupling Q V D S"
  assumes UNS: "u∉S"
  assumes UNI: "D u = enat du"
  
  shows "coupling 
    ((relax_outgoing' u du V Q)(u:=None)) (V(u↦du)) 
    (relax_outgoing u D) (Set.insert u S)"
  using C unfolding coupling_def 
proof (intro ext conjI; elim conjE)
  assume α: "D = enat_of_option ∘ V ++ Q" "S = dom V" 
     and DD: "dom V ∩ dom Q = {}"
   
  show "Set.insert u S = dom (V(u ↦ du))"   
    by (auto simp: α)
     
  have [simp]: "Q u = Some du" "V u = None" 
    using DD UNI UNS by (auto simp: α)
    
  from DD 
  show "dom (V(u ↦ du)) ∩ dom ((relax_outgoing' u du V Q)(u := None)) = {}"
    by (auto 0 3 
          simp: relax_outgoing'_def dom_def 
          split: if_splits enat.splits option.splits)
  
  fix v
  
  show "relax_outgoing u D v 
    = (enat_of_option ∘ V(u ↦ du) ++ (relax_outgoing' u du V Q)(u := None)) v"
  proof (cases "v∈S")
    case True
    then show ?thesis using DD
      apply (simp add: relax_finished_id)
      by (auto 
        simp: relax_outgoing'_def map_add_apply α min_def
        split: option.splits enat.splits)
  next
    case False
    then show ?thesis 
      by (auto 
        simp: relax_outgoing_def relax_outgoing'_def map_add_apply α min_def
        split: option.splits enat.splits)
  qed
qed    
  
text ‹Refinement of initial state›
definition "initQ ≡ Map.empty(s↦0)"
definition "initV ≡ Map.empty"
  
lemma coupling_init:
  "coupling initQ initV initD initS"    
  unfolding coupling_def initD_def initQ_def initS_def initV_def
  by (auto 
    simp: coupling_def relax_outgoing_def map_add_apply enat_0 
    split: option.split enat.split
    del: ext intro!: ext)
  
lemma coupling_cond:
  assumes "coupling Q V D S"
  shows "(Q = Map.empty) ⟷ (∀u. u∉S ⟶ D u = ∞)"
  using assms
  by (fastforce simp add: coupling_def)

  
text ‹Termination argument: Refinement of unfinished nodes.›  
definition "unfinished_dnodes' V ≡ unfinished_dnodes (dom V)"

lemma coupling_unfinished: 
  "coupling Q V D S ⟹ unfinished_dnodes' V = unfinished_dnodes S"
  by (auto simp: coupling_def unfinished_dnodes'_def unfinished_dnodes_def)

subsubsection ‹Implementing graph by successor list›  

definition "relax_outgoing'' l du V Q = fold (λ(d,v) Q.
  case Q v of None ⇒ if v∈dom V then Q else Q(v↦du+d)
            | Some d' ⇒ Q(v↦min (du+d) d')) l Q"


lemma relax_outgoing''_refine:
  assumes "set l = {(d,v). w (u,v) = enat d}"  
  shows "relax_outgoing'' l du V Q = relax_outgoing' u du V Q"
proof
  fix v
  
  have aux1:
     "relax_outgoing'' l du V Q v 
     = (if v∈snd`set l then relax_outgoing' u du V Q v else Q v)"
  if "set l ⊆ {(d,v). w (u,v) = enat d}"
    using that
    apply (induction l arbitrary: Q v)
    by (auto 
      simp: relax_outgoing''_def relax_outgoing'_def image_iff
      split!: if_splits option.splits)
  
  have aux2:  
    "relax_outgoing' u du V Q v = Q v" if "w (u,v) = ∞"
    using that by (auto simp: relax_outgoing'_def)
  
  show "relax_outgoing'' l du V Q v = relax_outgoing' u du V Q v"
    using aux1
    apply (cases "w (u,v)")
    by (all ‹force simp: aux2 assms›)
qed
  
end

end