Theory Dijkstra

section ‹Dijkstra's Algorithm›
theory Dijkstra
imports
Graph
Dijkstra_Misc
Collections.Refine_Dflt_ICF
Weight
begin
text ‹
This theory defines Dijkstra's algorithm. First, a correct result of
Dijkstra's algorithm w.r.t. a graph and a start vertex is specified.
Then, the refinement
framework is used to specify Dijkstra's Algorithm, prove it correct, and
finally refine it to datatypes that are closer to an implementation than
the original specification.
›

subsection "Graph's for Dijkstra's Algorithm"
text ‹A graph annotated with weights.›
locale weighted_graph = valid_graph G
for G :: "('V,'W::weight) graph"

subsection "Specification of Correct Result"
context weighted_graph
begin
text ‹
A result of Dijkstra's algorithm is correct, if it is a map from nodes
‹v› to the shortest path from the start node ‹v0› to
‹v›. Iff there is no such path, the node is not in the map.
›
definition is_shortest_path_map :: "'V ⇒ ('V ⇀ ('V,'W) path) ⇒ bool"
where
"is_shortest_path_map v0 res ≡ ∀v∈V. (case res v of
None ⇒ ¬(∃p. is_path v0 p v) |
Some p ⇒ is_path v0 p v
∧ (∀p'. is_path v0 p' v ⟶ path_weight p ≤ path_weight p')
)"
end

text ‹
The following function returns the weight of an optional path,
where ‹None› is interpreted as infinity.
›
fun path_weight' where
"path_weight' None = top" |
"path_weight' (Some p) = Num (path_weight p)"

subsection "Dijkstra's Algorithm"
text ‹
The state in the main loop of the algorithm consists of a workset
‹wl› of vertexes that still need to be explored, and a map
‹res› that contains the current shortest path for each vertex.
›
type_synonym ('V,'W) state = "('V set) × ('V ⇀ ('V,'W) path)"

text ‹
The preconditions of Dijkstra's algorithm, i.e., that it operates on a
valid and finite graph, and that the start node is a node of the graph,
are summarized in a locale.
›
locale Dijkstra = weighted_graph G
for G :: "('V,'W::weight) graph"+
fixes v0 :: 'V
assumes finite[simp,intro!]: "finite V" "finite E"
assumes v0_in_V[simp, intro!]: "v0∈V"
assumes nonneg_weights[simp, intro]: "(v,w,v')∈edges G ⟹ 0≤w"
begin

text ‹Paths have non-negative weights.›
lemma path_nonneg_weight: "is_path v p v' ⟹ 0 ≤ path_weight p"
by (induct rule: is_path.induct) auto

text ‹Invariant of the main loop:
\begin{itemize}
\item The workset only contains nodes of the graph.
\item If the result set contains a path for a node, it is actually a path,
and uses only intermediate vertices outside the workset.
\item For all vertices outside the workset, the result map contains the
shortest path.
\item For all vertices in the workset, the result map contains the
shortest path among all paths that only use intermediate vertices outside
the workset.
\end{itemize}
›
definition "dinvar σ ≡ let (wl,res)=σ in
wl ⊆ V ∧
(∀v∈V. ∀p. res v = Some p ⟶ is_path v0 p v ∧ int_vertices p ⊆ V-wl) ∧
(∀v∈V-wl. ∀p. is_path v0 p v
⟶ path_weight' (res v) ≤ path_weight' (Some p)) ∧
(∀v∈wl. ∀p. is_path v0 p v ∧ int_vertices p ⊆ V-wl
⟶ path_weight' (res v) ≤ path_weight' (Some p)
)
"

text ‹Sanity check: The invariant is strong enough to imply correctness
of result.›
lemma invar_imp_correct: "dinvar ({},res) ⟹ is_shortest_path_map v0 res"
unfolding dinvar_def is_shortest_path_map_def
by (auto simp: infty_unbox split: option.split)

text ‹
The initial workset contains all vertices. The initial result maps
‹v0› to the empty path, and all other vertices to ‹None›.
›
definition dinit :: "('V,'W) state nres" where
"dinit ≡ SPEC ( λ(wl,res) .
wl=V ∧ res v0 = Some [] ∧ (∀v∈V-{v0}. res v = None))"

text ‹
The initial state satisfies the invariant.
›
lemma dinit_invar: "dinit ≤ SPEC dinvar"
unfolding dinit_def
apply (intro refine_vcg)
apply (force simp: dinvar_def split: option.split)
done

text ‹
In each iteration, the main loop of the algorithm pops a minimal node from
the workset, and then updates the result map accordingly.
›

text ‹
Pop a minimal node from the workset. The node is minimal in the sense that
the length of the current path for that node is minimal.
›
definition pop_min :: "('V,'W) state ⇒ ('V × ('V,'W) state) nres" where
"pop_min σ ≡ do {
let (wl,res)=σ;
ASSERT (wl≠{});
v ← RES (least_map (path_weight' ∘ res) wl);
RETURN (v,(wl-{v},res))
}"

text ‹
Updating the result according to a node ‹v› is done by checking,
for each successor node, whether the path over ‹v› is shorter than
the path currently stored into the result map.
›
inductive update_spec :: "'V ⇒ ('V,'W) state ⇒ ('V,'W) state ⇒ bool"
where
"⟦ ∀v'∈V.
res' v' ∈ least_map path_weight' (
{ res v' } ∪ { Some (p@[(v,w,v')]) | p w. res v = Some p ∧ (v,w,v')∈E }
)
⟧ ⟹ update_spec v (wl,res) (wl,res')"

text ‹
In order to ease the refinement proof, we will assert the following
precondition for updating.
›
definition update_pre :: "'V ⇒ ('V,'W) state ⇒ bool" where
"update_pre v σ ≡ let (wl,res)=σ in v∈V
∧ (∀v'∈V-wl. v'≠v ⟶ (∀p. is_path v0 p v'
⟶ path_weight' (res v') ≤ path_weight' (Some p)))
∧ (∀v'∈V. ∀p. res v' = Some p ⟶ is_path v0 p v')"

definition update :: "'V ⇒ ('V,'W) state ⇒ ('V,'W) state nres" where
"update v σ ≡ do {ASSERT (update_pre v σ); SPEC (update_spec v σ)}"

text ‹Finally, we define Dijkstra's algorithm:›
definition dijkstra where
"dijkstra ≡ do {
σ0←dinit;
(_,res) ← WHILE⇩T⇗dinvar⇖ (λ(wl,_). wl≠{})
(λσ.
do { (v,σ') ← pop_min σ; update v σ' }
)
σ0;
RETURN res }
"

text ‹The following theorem states (total) correctness of Dijkstra's
algorithm.›

theorem dijkstra_correct: "dijkstra ≤ SPEC (is_shortest_path_map v0)"
unfolding dijkstra_def
unfolding dinit_def
unfolding pop_min_def update_def [abs_def]
thm refine_vcg

apply (refine_rcg
WHILEIT_rule[where R="inv_image {(x,y). x<y} (card ∘ fst)"]
refine_vcg
)

(* TODO/FIXME: Should we built in such massaging of the goal into
refine_rcg ?*)
supply [[simproc del: defined_all]]
apply (simp_all split: prod.split_asm)
apply (tactic ‹
ALLGOALS ((REPEAT_DETERM o Hypsubst.bound_hyp_subst_tac @{context})
THEN' asm_full_simp_tac @{context}
)›)

proof -
fix wl res v
assume INV: "dinvar (wl,res)"
and LM: "v∈least_map (path_weight' ∘ res) wl"
hence "v∈V" unfolding dinvar_def by (auto dest: least_map_elemD)
moreover
from INV have " ∀v'∈V - (wl-{v}). v' ≠ v ⟶
(∀p. is_path v0 p v' ⟶ path_weight' (res v') ≤ Num (path_weight p))"
by (auto simp: dinvar_def)
moreover from INV have "∀v'∈V. ∀p. res v'=Some p ⟶ is_path v0 p v'"
by (auto simp: dinvar_def)
ultimately show "update_pre v (wl-{v},res)" by (auto simp: update_pre_def)
next
fix res
assume "dinvar ({}, res)"
thus "is_shortest_path_map v0 res"
by (rule invar_imp_correct)
next
show "wf (inv_image {(x, y). x < y} (card ∘ fst))"
by (blast intro: wf_less)
next
fix wl res v σ''
assume
LM: "v∈least_map (path_weight' ∘ res) wl" and
UD: "update_spec v (wl-{v},res) σ''" and
INV: "dinvar (wl,res)"

from LM have "v∈wl" by (auto dest: least_map_elemD)
moreover from UD have "fst σ'' = wl-{v}" by (auto elim: update_spec.cases)
moreover from INV have "finite wl"
unfolding dinvar_def by (auto dest: finite_subset)
ultimately show "card (fst σ'') < card wl"
apply simp
by (metis card_gt_0_iff diff_Suc_less empty_iff)
next
fix a and res :: "'V ⇀ ('V,'W) path"
assume "a = V ∧ res v0 = Some [] ∧ (∀v∈V-{v0}. res v = None)"
thus "dinvar (V,res)"
by (force simp: dinvar_def split: option.split)
next
fix wl res
assume INV: "dinvar (wl,res)"
hence
WL_SUBSET: "wl ⊆ V" and
PATH_VALID: "∀v∈V. ∀p. res v = Some p
⟶ is_path v0 p v ∧ int_vertices p ⊆ V - wl" and
NWL_MIN: "∀v∈V - wl. ∀p. is_path v0 p v
⟶ path_weight' (res v) ≤ Num (path_weight p)" and
WL_MIN: "∀v∈wl. ∀p. is_path v0 p v ∧ int_vertices p ⊆ V - wl
⟶ path_weight' (res v) ≤ Num (path_weight p)"
unfolding dinvar_def by auto

fix v σ''
assume V_LEAST: "v∈least_map (path_weight' o res) wl"
and "update_spec v (wl-{v},res) σ''"
then obtain res' where
[simp]: "σ''=(wl-{v},res')"
and CONSIDERED_NEW_PATHS: "∀v'∈V. res' v' ∈ least_map path_weight'
(insert (res v')
({ Some (p@[(v,w,v')]) | p w. res v = Some p ∧ (v,w,v')∈E }))"
by (auto elim!: update_spec.cases)

from V_LEAST have V_MEM: "v∈wl" by (blast intro: least_map_elemD)

show "dinvar σ''"
apply (unfold dinvar_def, simp)
apply (intro conjI)
proof -
from WL_SUBSET show "wl-{v} ⊆ V" by auto

show "∀va∈V. ∀p. res' va = Some p
⟶ is_path v0 p va ∧ int_vertices p ⊆ V - (wl - {v})"
proof (intro ballI conjI impI allI)
fix v' p
assume V'_MEM: "v'∈V" and [simp]: "res' v' = Some p"
txt ‹The new paths that we have added are valid and only use
intermediate vertices outside the workset.

This proof works as follows: A path @{term "res' v'"} is either
the old path, or has been assembled as a path over node @{term v}.
In the former case the proposition follows straightforwardly from the
invariant for the old state. In the latter case we get, by the invariant
for the old state, that the path over node @{term v} is valid.
Then, we observe that appending an edge to a valid path yields a valid
path again. Also, adding @{term v} as intermediate node is legal, as we
just removed @{term v} from the workset.
›
with CONSIDERED_NEW_PATHS have "res' v' ∈ (insert (res v')
({ Some (p@[(v,w,v')]) | p w. res v = Some p ∧ (v,w,v')∈E }))"
by (rule_tac least_map_elemD) blast
moreover {
assume [symmetric,simp]: "res' v' = res v'"
from V'_MEM PATH_VALID have
"is_path v0 p v'"
"int_vertices p ⊆ V - (wl-{v})"
by force+
} moreover {
fix pv w
assume "res' v' = Some (pv@[(v,w,v')])"
and [simp]: "res v = Some pv"
and EDGE: "(v,w,v')∈E"
hence [simp]: "p = pv@[(v,w,v')]" by simp

from bspec[OF PATH_VALID rev_subsetD[OF V_MEM WL_SUBSET]] have
PATHV: "is_path v0 pv v" and IVV: "int_vertices pv ⊆ V - wl" by auto
hence
"is_path v0 p v'"
"int_vertices p ⊆ V - (wl-{v})"
by (auto simp: EDGE V'_MEM)
}
ultimately show
"is_path v0 p v'"
"int_vertices p ⊆ V - (wl-{v})"
by blast+
qed

txt ‹
We show that already the {\em original} result stores the minimal
path for all vertices not in the {\em new} workset.
For vertices also not in the original workset, this follows
straightforwardly from the invariant.

For the vertex ‹v›, that has been removed from the
workset, we split a path ‹p'› to ‹v› at the point
‹u› where it first enters the original workset.

As we chose ‹v› to be the vertex in the workset with the
minimal weight, its weight is less than the current weight of
‹u›.  As the vertices of the prefix of ‹p'› up to
‹u› are not in the workset, the current weight of
‹u› is less than the weight of the prefix of ‹p'›, and thus less than the weight of ‹p'›.
Together, the current weight of ‹v› is less than the weight of
‹p'›.›
have RES_MIN: "∀v∈V - (wl - {v}). ∀p. is_path v0 p v
⟶ path_weight' (res v) ≤ Num (path_weight p)"
proof (intro ballI allI impI)
fix v' p'
assume NOT_IN_WL: "v' ∈ V - (wl - {v})"
and PATH: "is_path v0 p' v'"
hence [simp, intro!]: "v'∈V" by auto

show "path_weight' (res v') ≤ Num (path_weight p')"
proof (cases "v' = v")
assume NE[simp]: "v'≠v"
from bspec[OF NWL_MIN, of v'] NOT_IN_WL PATH show
"path_weight' (res v') ≤ Num (path_weight p')" by auto
next
assume EQ[simp]: "v'=v"

from path_split_set'[OF PATH, of wl] V_MEM obtain p1 p2 u where
[simp]: "p'=p1@p2"
and P1: "is_path v0 p1 u"
and P2: "is_path u p2 v'"
and P1V: "int_vertices p1 ⊆ -wl"
and [simp]: "u∈wl"
by auto

from least_map_leD[OF V_LEAST]
have "path_weight' (res v') ≤ path_weight' (res u)"by auto
also from bspec[OF WL_MIN, of u] P1 P1V int_vertices_subset[OF P1]
have "path_weight' (res u) ≤ Num (path_weight p1)" by auto
also have "… ≤ Num (path_weight p')"
using path_nonneg_weight[OF P2]
apply (auto simp: infty_unbox )
finally show ?thesis .
qed
qed

txt ‹With the previous statement, we easily show the
third part of the invariant, as the new paths are not longer than the
old ones.
›
show "∀v∈V - (wl - {v}). ∀p. is_path v0 p v
⟶ path_weight' (res' v) ≤ Num (path_weight p)"
proof (intro allI ballI impI)
fix v' p
assume NOT_IN_WL: "v' ∈ V - (wl - {v})"
and PATH: "is_path v0 p v'"
hence [simp, intro!]: "v'∈V" by auto
from bspec[OF CONSIDERED_NEW_PATHS, of v']
have "path_weight' (res' v') ≤ path_weight' (res v')"
by (auto dest: least_map_leD)
also from bspec[OF RES_MIN NOT_IN_WL] PATH
have "path_weight' (res v') ≤ Num (path_weight p)" by blast
finally show "path_weight' (res' v') ≤ Num (path_weight p)" .
qed

txt ‹
Finally, we have to show that for nodes on the worklist,
the stored paths are not longer than any path using only nodes not
on the worklist. Compared to the situation before the step, those
path may also use the node ‹v›.
›
show "∀va∈wl - {v}. ∀p.
is_path v0 p va ∧ int_vertices p ⊆ V - (wl - {v})
⟶ path_weight' (res' va) ≤ Num (path_weight p)"
proof (intro allI impI ballI, elim conjE)
fix v' p
assume IWS: "v'∈wl - {v}"
and PATH: "is_path v0 p v'"
and VERTICES: "int_vertices p ⊆ V - (wl - {v})"
from IWS WL_SUBSET have [simp, intro!]: "v'∈V" by auto

{
txt ‹
If the path is empty, the proposition follows easily from the
invariant for the original states, as no intermediate nodes are
used at all.
›
assume [simp]: "p=[]"
from bspec[OF CONSIDERED_NEW_PATHS, of v'] have
"path_weight' (res' v') ≤ path_weight' (res v')"
using IWS WL_SUBSET by (auto dest: least_map_leD)
also have "int_vertices p ⊆ V-wl" by auto
with WL_MIN IWS PATH
have "path_weight' (res v') ≤ Num (path_weight p)"
by (auto simp del: path_weight_empty)
finally have "path_weight' (res' v') ≤ Num (path_weight p)" .
} moreover {
fix p1 u w
assume [simp]: "p = p1@[(u,w,v')]"
txt ‹If the path is not empty, we pick the last but one vertex, and
call it @{term u}.›
from PATH have PATH1: "is_path v0 p1 u" and EDGE: "(u,w,v')∈E" by auto
from VERTICES have NIV: "u∈V - (wl-{v})" by simp
hence U_MEM[simp]: "u∈V" by auto

txt ‹From @{thm [source] RES_MIN}, we know that @{term "res u"} holds
the shortest path to @{term u}. Thus ‹p› is longer than the
path that is constructed by replacing the prefix of @{term p} by
{term "res u"}›
from NIV RES_MIN PATH1
have G: "Num (path_weight p1) ≥ path_weight' (res u)" by simp
then obtain pu where [simp]: "res u = Some pu"
by (cases "res u") (auto simp: infty_unbox)
from G have "Num (path_weight p) ≥ path_weight' (res u) + Num w"
also
have "path_weight' (res u) + Num w ≥ path_weight' (res' v')"
txt ‹
The remaining argument depends on wether @{term u}
equals @{term v}.
In the case @{term "u≠v"}, all vertices of @{term "res u"} are
outside the original workset. Thus, appending the edge
@{term "(u,w,v')"} to @{term "res u"} yields a path to @{term v}
over intermediate nodes only outside the workset. By the invariant
for the original state, @{term "res v'"} is shorter than this path.
As a step does not replace paths by longer ones, also
@{term "res' v'"} is shorter.

In the case @{term "u=v"}, the step has
considered the path to ‹v'› over ‹v›, and thus the
result path is not longer.
›
proof (cases "u=v")
assume "u≠v"
with NIV have NIV': "u∈V-wl" by auto
from bspec[OF PATH_VALID U_MEM] NIV'
have "is_path v0 pu u" and VU: "int_vertices (pu@[(u,w,v')]) ⊆ V-wl"
by auto
with EDGE have PV': "is_path v0 (pu@[(u,w,v')]) v'" by auto
with bspec[OF WL_MIN, of v'] IWS VU have
"path_weight' (res v') ≤ Num (path_weight (pu@[(u,w,v')]))"
by blast
hence "path_weight' (res u) + Num w ≥ path_weight' (res v')"
by (auto simp: infty_unbox)
also from CONSIDERED_NEW_PATHS have
"path_weight' (res v') ≥ path_weight' (res' v')"
by (auto dest: least_map_leD)
finally (order_trans[rotated]) show ?thesis .
next
assume [symmetric,simp]: "u=v"
from CONSIDERED_NEW_PATHS EDGE have
"path_weight' (res' v') ≤ path_weight' (Some (pu@[(v,w,v')]))"
by (rule_tac least_map_leD) auto
thus ?thesis by (auto simp: infty_unbox)
qed
finally (order_trans[rotated]) have
"path_weight' (res' v') ≤ Num (path_weight p)" .
} ultimately show "path_weight' (res' v') ≤ Num (path_weight p)"
using PATH apply (cases p rule: rev_cases) by auto
qed
qed
qed

subsection ‹Structural Refinement of Update›
text ‹
Now that we have proved correct the initial version of the algorithm, we start
refinement towards an efficient implementation.
›

text ‹
First, the update function is refined to iterate over each successor of the
selected node, and update the result on demand.
›
definition uinvar
:: "'V ⇒ 'V set ⇒ _ ⇒ ('W×'V) set ⇒ ('V,'W) state ⇒ bool" where
"uinvar v wl res it σ ≡ let (wl',res')=σ in wl'=wl
∧ (∀v'∈V.
res' v' ∈ least_map path_weight' (
{ res v' } ∪ { Some (p@[(v,w,v')]) | p w. res v = Some p
∧ (w,v') ∈ succ G v - it }
))
∧ (∀v'∈V. ∀p. res' v' = Some p ⟶ is_path v0 p v')
∧ res' v = res v
"

definition update' :: "'V ⇒ ('V,'W) state ⇒ ('V,'W) state nres" where
"update' v σ ≡ do {
ASSERT (update_pre v σ);
let (wl,res) = σ;
let wv = path_weight' (res v);
let pv = res v;
FOREACH⇗uinvar v wl res⇖ (succ G v) (λ(w',v') (wl,res).
if (wv + Num w' < path_weight' (res v')) then do {
ASSERT (v'∈wl ∧ pv≠None);
RETURN (wl,res(v' ↦ the pv@[(v,w',v')]))
} else RETURN (wl,res)
) (wl,res)}"

lemma update'_refines:
assumes "v'=v" and "σ'=σ"
shows "update' v' σ' ≤ ⇓Id (update v σ)"
apply (simp only: assms)
unfolding update'_def update_def
apply (refine_rcg refine_vcg)

(*apply (intro refine_vcg conjI)*)
apply (simp_all only: singleton_iff)
proof -
fix wl res
assume "update_pre v (wl,res)"
thus "uinvar v wl res (succ G v) (wl,res)"
next

fix wl res it wl' res' v' w'
assume PRE: "update_pre v (wl,res)"
assume INV: "uinvar v wl res it (wl',res')"
assume MEM: "(w',v')∈it"
assume IT_SS: "it⊆ succ G v"
assume LESS: "path_weight' (res v) + Num w' < path_weight' (res' v')"

from PRE have [simp, intro!]: "v∈V" by (simp add: update_pre_def)

from MEM IT_SS have [simp,intro!]: "v'∈V" using succ_subset
by auto

from LESS obtain pv where [simp]: "res v = Some pv"
by (cases "res v") auto

thus "res v ≠ None" by simp

have [simp]: "wl'=wl" and [simp]: "res' v = res v"
using INV unfolding uinvar_def by auto

from MEM IT_SS have EDGE[simp]: "(v,w',v')∈E"
unfolding succ_def by auto
with INV have [simp]: "is_path v0 pv v"
unfolding uinvar_def by auto

have "0≤w'" by (rule nonneg_weights[OF EDGE])
hence [simp]: "v'≠v" using LESS
by auto
hence [simp]: "v≠v'" by blast

show [simp]: "v'∈wl'" proof (rule ccontr)
assume [simp]: "v'∉wl'"
hence [simp]: "v'∈V-wl" and [simp]: "v'∉wl" by auto
note LESS
also
from INV have "path_weight' (res' v') ≤ path_weight' (res v')"
unfolding uinvar_def by (auto dest: least_map_leD)
also
from PRE have PW: "⋀p. is_path v0 p v' ⟹
path_weight' (res v') ≤ path_weight' (Some p)"
unfolding update_pre_def
by auto
have P: "is_path v0 (pv@[(v,w',v')]) v'" by simp
from PW[OF P] have
"path_weight' (res v') ≤ Num (path_weight (pv@[(v,w',v')]))"
by auto
finally show False by (simp add: infty_unbox)
qed

show "uinvar v wl res (it-{(w',v')}) (wl',res'(v'↦the (res v)@[(v,w',v')]))"
proof -
have "(res'(v'↦the (res v)@[(v,w',v')])) v = res' v" by simp
moreover {
fix v'' assume VMEM: "v''∈V"
have "(res'(v'↦the (res v)@[(v,w',v')])) v'' ∈ least_map path_weight' (
{ res v'' } ∪ { Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - (it - {(w',v')}) }
) ∧ (∀p. (res'(v'↦the (res v)@[(v,w',v')])) v'' = Some p
⟶ is_path v0 p v'')"
proof (cases "v''=v'")
case [simp]: False
have "{ Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - (it - {(w',v')}) } =
{ Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - it }"
by auto
with INV VMEM show ?thesis unfolding uinvar_def
by simp
next
case [simp]: True
have EQ: "{ res v'' } ∪ { Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - (it - {(w',v')}) } =
insert (Some (pv@[(v,w',v')])) (
{ res v'' } ∪ { Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - it })"
using MEM IT_SS
by auto
show ?thesis
apply (subst EQ)
apply simp
apply (rule least_map_insert_min)
apply (rule ballI)
proof -
fix r'
assume A:
"r' ∈ insert (res v')
{Some (pv @ [(v, w, v')]) |w. (w, v') ∈ succ G v ∧ (w, v') ∉ it}"

from LESS have
"path_weight' (Some (pv @ [(v, w', v')])) < path_weight' (res' v')"
by (auto simp: infty_unbox)
also from INV[unfolded uinvar_def] have
"res' v' ∈ least_map path_weight' (
insert (res v')
{Some (pv @ [(v, w, v')]) |w. (w, v') ∈ succ G v ∧ (w, v') ∉ it}
)"
by auto
with A have "path_weight' (res' v') ≤ path_weight' r'"
by (auto dest: least_map_leD)
finally show
"path_weight' (Some (pv @ [(v, w', v')])) ≤ path_weight' r'"
by simp
qed
qed
}
ultimately show ?thesis
unfolding uinvar_def Let_def
by auto
qed
next
fix wl res it w' v' wl' res'
assume INV: "uinvar v wl res it (wl',res')"
and NLESS: "¬ path_weight' (res v) + Num w' < path_weight' (res' v')"
and IN_IT: "(w',v')∈it"
and IT_SS: "it ⊆ succ G v"

from IN_IT IT_SS have [simp, intro!]: "(w',v')∈succ G v" by auto
hence [simp,intro!]: "v'∈V" using succ_subset
by auto

show "uinvar v wl res (it - {(w',v')}) (wl',res')"
proof (cases "res v")
case [simp]: None
from INV show ?thesis
unfolding uinvar_def by auto
next
case [simp]: (Some p)
{
fix v''
assume [simp, intro!]: "v''∈V"
have "res' v'' ∈ least_map path_weight' (
{ res v'' } ∪ { Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - (it - {(w',v')}) }
)" (is "_ ∈ least_map path_weight' ?S")
proof (cases "v''=v'")
case False with INV show ?thesis
unfolding uinvar_def by auto
next
case [simp]: True

have EQ: "?S = insert (Some (p@[(v,w',v')])) (
{ res v' } ∪ { Some (p@[(v,w,v'')]) | p w. res v = Some p
∧ (w,v'') ∈ succ G v - it }
)"
by auto
from NLESS have
"path_weight' (res' v') ≤ path_weight' (Some (p@[(v,w',v')]))"
by (auto simp: infty_unbox)
thus ?thesis
apply (subst EQ)
apply (rule least_map_insert_nmin)
using INV unfolding uinvar_def apply auto []
apply simp
done
qed
} with INV
show ?thesis
unfolding uinvar_def by auto
qed
next
fix wl res σ'

assume "uinvar v wl res {} σ'"
thus "update_spec v (wl,res) σ'"
unfolding uinvar_def
apply (cases σ')
apply (auto intro: update_spec.intros simp: succ_def)
done
next
show "finite (succ G v)" by simp
qed

text ‹We integrate the new update function into the main algorithm:›
definition dijkstra' where
"dijkstra' ≡ do {
σ0 ← dinit;
(_,res) ← WHILE⇩T⇗dinvar⇖ (λ(wl,_). wl≠{})
(λσ. do {(v,σ') ← pop_min σ; update' v σ'})
σ0;
RETURN res
}"

lemma dijkstra'_refines: "dijkstra' ≤ ⇓Id dijkstra"
proof -
note [refine] = update'_refines
have [refine]: "⋀σ σ'. σ=σ' ⟹ pop_min σ ≤ ⇓Id (pop_min σ')" by simp
show ?thesis
unfolding dijkstra_def dijkstra'_def
apply (refine_rcg)
apply simp_all
done
qed
end

subsection ‹Refinement to Cached Weights›
text ‹
Next, we refine the data types of the workset and the result map.
The workset becomes a map from nodes to their current weights.
The result map stores, in addition to the shortest path, also the
weight of the shortest path. Moreover, we store the shortest paths
in reversed order, which makes appending new edges more effcient.

These refinements allow to implement the workset as a priority queue,
and save recomputation of the path weights in the inner loop of the
algorithm.
›

type_synonym ('V,'W) mwl = "('V ⇀ 'W infty)"
type_synonym ('V,'W) mres = "('V ⇀ (('V,'W) path × 'W))"
type_synonym ('V,'W) mstate = "('V,'W) mwl × ('V,'W) mres"

text ‹
Map a path with cached weight to one without cached weight.
›
fun mpath' :: "(('V,'W) path × 'W) option ⇀ ('V,'W) path" where
"mpath' None = None" |
"mpath' (Some (p,w)) = Some p"

fun mpath_weight' :: "(('V,'W) path × 'W) option ⇒ ('W::weight) infty" where
"mpath_weight' None = top" |
"mpath_weight' (Some (p,w)) = Num w"

context Dijkstra
begin
definition αw::"('V,'W) mwl ⇒ 'V set" where "αw ≡ dom"
definition αr::"('V,'W) mres ⇒ 'V ⇀ ('V,'W) path" where
"αr ≡ λres v. case res v of None ⇒ None | Some (p,w) ⇒ Some (rev p)"
definition αs:: "('V,'W) mstate ⇒ ('V,'W) state" where
"αs ≡ map_prod αw αr"

text ‹Additional invariants for the new state. They guarantee that
the cached weights are consistent.›
definition res_invarm :: "('V ⇀ (('V,'W) path×'W)) ⇒ bool" where
"res_invarm res ≡ (∀v. case res v of
None ⇒ True |
Some (p,w) ⇒ w = path_weight (rev p))"
definition dinvarm :: "('V,'W) mstate ⇒ bool" where
"dinvarm σ ≡ let (wl,res) = σ in
(∀v∈dom wl. the (wl v) = mpath_weight' (res v)) ∧ res_invarm res
"
lemma mpath_weight'_correct: "⟦dinvarm (wl,res)⟧ ⟹
mpath_weight' (res v) = path_weight' (αr res v)
"
unfolding dinvarm_def res_invarm_def αr_def
by (auto split: option.split option.split_asm)

lemma mpath'_correct: "⟦dinvarm (wl,res)⟧ ⟹
mpath' (res v) = map_option rev (αr res v)"
unfolding dinvarm_def αr_def
by (auto split: option.split option.split_asm)

lemma wl_weight_correct:
assumes INV: "dinvarm (wl,res)"
assumes WLV: "wl v = Some w"
shows "path_weight' (αr res v) = w"
proof -
from INV WLV have "w = mpath_weight' (res v)"
unfolding dinvarm_def by force
also from mpath_weight'_correct[OF INV] have
"… = path_weight' (αr res v)" .
finally show ?thesis by simp
qed

text ‹The initial state is constructed using an iterator:›
definition mdinit :: "('V,'W) mstate nres" where
"mdinit ≡ do {
wl ← FOREACH V (λv wl. RETURN (wl(v↦Infty))) Map.empty;
RETURN (wl(v0↦Num 0),[v0 ↦ ([],0)])
}"

lemma mdinit_refines: "mdinit ≤ ⇓(build_rel αs dinvarm) dinit"
unfolding mdinit_def dinit_def
apply (rule build_rel_SPEC)
apply (intro FOREACH_rule[where I="λit wl. (∀v∈V-it. wl v = Some Infty) ∧
dom wl = V-it"]
refine_vcg)
apply (auto
simp: αs_def αw_def αr_def dinvarm_def res_invarm_def infty_unbox
split: if_split_asm
)
done

text ‹The new pop function:›
definition
mpop_min :: "('V,'W) mstate ⇒ ('V × 'W infty × ('V,'W) mstate) nres"
where
"mpop_min σ ≡ do {
let (wl,res) = σ;
(v,w,wl')←prio_pop_min wl;
RETURN (v,w,(wl',res))
}"

lemma mpop_min_refines:
"⟦ (σ,σ') ∈ build_rel αs dinvarm ⟧ ⟹
mpop_min σ ≤
⇓(build_rel
(λ(v,w,σ). (v,αs σ))
(λ(v,w,σ). dinvarm σ ∧ w = mpath_weight' (snd σ v)))
(pop_min σ')"
― ‹The two algorithms are structurally different, so we use the
nofail/inres method to prove refinement.›
unfolding mpop_min_def pop_min_def prio_pop_min_def

apply (rule pw_ref_I)
apply rule
apply (auto simp add: refine_pw_simps αs_def αw_def refine_rel_defs
split: prod.split prod.split_asm)

apply (auto simp: dinvarm_def) []

apply (auto simp: mpath_weight'_correct wl_weight_correct) []

apply (auto
simp: wl_weight_correct
intro!: least_map.intros
) []
apply (metis restrict_map_eq(2))

done

text ‹The new update function:›
definition "uinvarm v wl res it σ ≡
uinvar v wl res it (αs σ) ∧ dinvarm σ"

definition mupdate :: "'V ⇒ 'W infty ⇒ ('V,'W) mstate ⇒ ('V,'W) mstate nres"
where
"mupdate v wv σ ≡ do {
ASSERT (update_pre v (αs σ) ∧ wv=mpath_weight' (snd σ v));
let (wl,res) = σ;
let pv = mpath' (res v);
FOREACH⇗uinvarm v (αw wl) (αr res)⇖ (succ G v) (λ(w',v') (wl,res).
if (wv + Num w' < mpath_weight' (res v')) then do {
ASSERT (v'∈dom wl ∧ pv ≠ None);
ASSERT (wv ≠ Infty);
RETURN (wl(v'↦wv + Num w'),
res(v' ↦ ((v,w',v')#the pv,val wv + w') ))
} else RETURN (wl,res)
) (wl,res)
}"

lemma mupdate_refines:
assumes SREF: "(σ,σ')∈build_rel αs dinvarm"
assumes WV: "wv = mpath_weight' (snd σ v)"
assumes VV': "v'=v"
shows "mupdate v wv σ ≤ ⇓(build_rel αs dinvarm) (update' v' σ')"
proof (simp only: VV')
{
txt ‹Show that IF-condition is a refinement:›
fix wl res wl' res' it w' v'
assume "uinvarm v (αw wl) (αr res) it (wl',res')"
and "dinvarm (wl,res)"
hence "mpath_weight' (res v) + Num w' < mpath_weight' (res' v') ⟷
path_weight' (αr res v) + Num w' < path_weight' (αr res' v')"
unfolding uinvarm_def
} note COND_refine=this

{
txt ‹THEN-case:›
fix wl res wl' res' it w' v'
assume UINV: "uinvarm v (αw wl) (αr res) it (wl',res')"
and DINV: "dinvarm (wl,res)"
and "mpath_weight' (res v) + Num w' < mpath_weight' (res' v')"
and "path_weight' (αr res v) + Num w' < path_weight' (αr res' v')"
and V'MEM: "v'∈αw wl'"
and NN: "αr res v ≠ None"

from NN obtain pv wv where
ARV: "αr res v = Some (rev pv)" and
RV: "res v = Some (pv,wv)"
unfolding αr_def by (auto split: option.split_asm)

with DINV have [simp]: "wv = path_weight (rev pv)"
unfolding dinvarm_def res_invarm_def by (auto split: option.split_asm)

note [simp] = ARV RV

from V'MEM NN have "v'∈dom wl'" (is "?G1")
and "mpath' (res v) ≠ None" (is "?G2")
unfolding αw_def αr_def by (auto split: option.split_asm)

hence "⋀x. αw wl' = αw (wl'(v'↦x))" by (auto simp: αw_def)
moreover have "mpath' (res v) = map_option rev (αr res v)" using DINV
ultimately have
"αw wl' = αw (wl'(v' ↦ mpath_weight' (res v) + Num w'))
∧ (αr res')(v' ↦ the (αr res v)@[(v, w', v')])
= αr (res'(v' ↦ ((v, w', v')#the (mpath' (res v)),
val (mpath_weight' (res v)) + w')))" (is ?G3)
by (auto simp add: αr_def intro!: ext)
have
"(dinvarm (wl'(v'↦mpath_weight' (res v) + Num w'),
res'(v' ↦ ((v,w',v') # the (mpath' (res v)),
val (mpath_weight' (res v)) + w'
))))" (is ?G4)
using UINV unfolding uinvarm_def dinvarm_def res_invarm_def
by (auto simp: infty_unbox split: option.split option.split_asm)
note ‹?G1› ‹?G2› ‹?G3› ‹?G4›
} note THEN_refine=this

note [refine2] = inj_on_id

note [simp] = refine_rel_defs

show "mupdate v wv σ ≤ ⇓(build_rel αs dinvarm) (update' v σ')"
using SREF WV
unfolding mupdate_def update'_def
apply -

apply (refine_rcg)

apply simp_all [3]
apply (simp_all add: αs_def COND_refine THEN_refine(1-2)) [3]
apply (rule ccontr,simp)
using THEN_refine(3,4)
apply (auto simp: αs_def) []
txt ‹The ELSE-case is trivial:›
apply simp
done
qed

text ‹Finally, we assemble the refined algorithm:›
definition mdijkstra where
"mdijkstra ≡ do {
σ0 ← mdinit;
(_,res) ← WHILE⇩T⇗dinvarm⇖ (λ(wl,_). dom wl≠{})
(λσ. do { (v,wv,σ') ← mpop_min σ; mupdate v wv σ' } )
σ0;
RETURN res
}"

lemma mdijkstra_refines: "mdijkstra ≤ ⇓(build_rel αr res_invarm) dijkstra'"
proof -
note [refine] = mdinit_refines mpop_min_refines mupdate_refines
show ?thesis
unfolding mdijkstra_def dijkstra'_def
apply (refine_rcg)
apply (simp_all split: prod.split