author lammich Mon, 09 Jul 2018 11:56:29 +0200 changeset 69946 ed7c67f266ac parent 69945 c772b78fd6cd child 69947 cd8eb35f3c38
Dijkstra cleaned up
 Thys/Dijkstra.thy file | annotate | diff | comparison | revisions Thys/Weighted_Graph_Specs.thy file | annotate | diff | comparison | revisions
```--- a/Thys/Dijkstra.thy	Fri Jul 06 00:22:56 2018 +0200
+++ b/Thys/Dijkstra.thy	Mon Jul 09 11:56:29 2018 +0200
@@ -1,7 +1,8 @@
+section \<open>Dijstra's Algorithm\<close>
theory Dijkstra
imports
Main
-  "HOL-Library.Extended_Nat"
+  "Weighted_Graph_Specs"
"HOL-Eisbach.Eisbach"
Prio_Map_Specs
"HOL-Library.While_Combinator"
@@ -9,7 +10,7 @@
"HOL-Data_Structures.RBT_Map"
begin

-hide_const (open) connected
+subsection \<open>Miscellaneous\<close>

lemma least_antimono: "X\<noteq>{} \<Longrightarrow> X\<subseteq>Y \<Longrightarrow> (LEAST y::_::wellorder. y\<in>Y) \<le> (LEAST x. x\<in>X)"
by (metis LeastI_ex Least_le equals0I rev_subsetD)
@@ -17,269 +18,187 @@
lemma map_add_apply: "(m\<^sub>1 ++ m\<^sub>2) k = (case m\<^sub>2 k of None \<Rightarrow> m\<^sub>1 k | Some x \<Rightarrow> Some x)"

-
-
-type_synonym ('v,'w) wgraph = "('v \<times> 'v) \<Rightarrow> 'w"
-
-
-locale WGraph = fixes w :: "('v,enat) wgraph"
-begin
-
-  fun path :: "'v \<Rightarrow> enat list \<Rightarrow> 'v \<Rightarrow> bool" where
-    "path u [] v \<longleftrightarrow> u=v"
-  | "path u (l#ls) v \<longleftrightarrow> (\<exists>uh. l = w (u,uh) \<and> path uh ls v)"
-
-  lemma path_append[simp]: "path u (ls1@ls2) v \<longleftrightarrow> (\<exists>w. path u ls1 w \<and> path w ls2 v)"
-    by (induction ls1 arbitrary: u) auto
-
-  (*definition "connected u v \<equiv> \<exists>p. path u p v"  *)
-
-  definition "paths u v \<equiv> {p . path u p v}"
-
-  lemma triv_path: "path u [w (u,v)] v" by auto
-
-  lemma paths_ne: "paths u v \<noteq> {}" using triv_path unfolding paths_def by blast
-
-  lemma find_leave_edgeE:
-    assumes "path u p v"
-    assumes "u\<in>S" "v\<notin>S"
-    obtains p1 x y p2 where "p = p1@w (x,y)#p2" "x\<in>S" "y\<notin>S" "path u p1 x" "path y p2 v"
-  proof -
-    have "\<exists> p1 x y p2. p = p1@w (x,y)#p2 \<and> x\<in>S \<and> y\<notin>S \<and> path u p1 x \<and> path y p2 v"
-      using assms
-    proof (induction p arbitrary: u)
-      case Nil
-      then show ?case by auto
-    next
-      case (Cons a p)
-      from Cons.prems obtain x where [simp]: "a=w (u,x)" and PX: "path x p v" by auto
-
-      show ?case proof (cases "x\<in>S")
-        case False with PX \<open>u\<in>S\<close> show ?thesis by fastforce
-      next
-        case True from Cons.IH[OF PX True \<open>v\<notin>S\<close>] show ?thesis
-          by clarsimp (metis WGraph.path.simps(2) append_Cons)
-      qed
-    qed
-    thus ?thesis by (fast intro: that)
-  qed

-  definition "\<delta> u v \<equiv> LEAST w::enat. w\<in>sum_list`paths u v"

-  lemma obtain_shortest_path:
-    obtains p where "path s p u" "\<delta> s u = sum_list p"
-    unfolding \<delta>_def using paths_ne
-    by (smt Collect_empty_eq LeastI_ex WGraph.paths_def imageI image_iff mem_Collect_eq paths_def)
-
-  lemma shortest_path_least:
-    "path s p u \<Longrightarrow> \<delta> s u \<le> sum_list p"
-    unfolding \<delta>_def paths_def
+subsection \<open>Abstract Dijkstra Algorithm\<close>

-  lemma shortest_path_refl[simp]: "\<delta> s s = 0"
-    using shortest_path_least[of s "[]" s] by auto
-
-  lemma shortest_path_direct: "\<delta> s u \<le> w (s, u)"
-    using shortest_path_least[of s "[w (s,u)]" u] by auto
-
-  lemma triangle: "\<delta> s v \<le> \<delta> s u + w (u,v)"
-  proof -
-    have "path s (p@[w (u,v)]) v" if "path s p u" for p using that by auto
-    then have "(+) (w (u,v)) ` sum_list ` paths s u \<subseteq> sum_list ` paths s v"
-      by (fastforce simp: paths_def image_iff simp del: path.simps path_append)
-    from least_antimono[OF _ this] paths_ne have
-      "(LEAST y::enat. y \<in> sum_list ` paths s v) \<le> (LEAST x::enat. x \<in> (+) (w (u,v)) ` sum_list ` paths s u)"
-      by (auto simp: paths_def)
-    also have "\<dots> = (LEAST x. x \<in> sum_list ` paths s u) + w (u,v)"
-      apply (subst Least_mono[of "(+) (w (u,v))" "sum_list`paths s u"])
-      apply (auto simp: mono_def)
-      by (metis WGraph.paths_def mem_Collect_eq obtain_shortest_path shortest_path_least)
-    finally show ?thesis unfolding \<delta>_def .
-  qed
-
-  lemma shortest_subpath:
-    assumes "path s p\<^sub>1 x" "path x p\<^sub>2 u"
-    and DSU: "\<delta> s u = sum_list p\<^sub>1 + sum_list p\<^sub>2" "\<delta> s u < \<infinity>"
-    shows "\<delta> s x = sum_list p\<^sub>1" "\<delta> s x < \<infinity>"
-  proof -
-    have "\<delta> s x \<le> sum_list p\<^sub>1" using assms shortest_path_least by blast
-    moreover have "\<not>\<delta> s x < sum_list p\<^sub>1" proof
-      assume "\<delta> s x < sum_list p\<^sub>1"
-      then obtain p\<^sub>1' where "path s p\<^sub>1' x" "sum_list p\<^sub>1' < sum_list p\<^sub>1"
-        by (auto intro: obtain_shortest_path[of s x])
-      with \<open>path x p\<^sub>2 u\<close> shortest_path_least[of s "p\<^sub>1'@p\<^sub>2" u] DSU show False
-        by fastforce
-    qed
-    ultimately show "\<delta> s x = sum_list p\<^sub>1" by auto
-    with DSU show "\<delta> s x < \<infinity>" using le_iff_add by fastforce
-  qed
-
-
-end
+type_synonym 'v estimate = "'v \<Rightarrow> enat"

-
-
-
-locale Dijkstra = WGraph w for w :: "('v,enat) wgraph" +
+text \<open>We fix a start node and a weighted graph\<close>
+locale Dijkstra = WGraph w for w :: "('v) wgraph" +
fixes s :: 'v
begin
-
-  (* TODO: Unused *)
-  definition "relax \<equiv> \<lambda>(u,v) D. if D v > D u + w (u,v) then D(v := D u + w (u,v)) else D"
-
-  definition "relax_adjs u D v \<equiv> min (D v) (D u + w (u,v))"
-
-
-  definition "upper_bound D \<equiv>
-    (\<forall>u. D u \<ge> \<delta> s u) \<comment> \<open>upper bound property\<close>
-  "

-  lemma maintain_upper_bound: "upper_bound D \<Longrightarrow> upper_bound (relax e D)"
-    apply (auto simp: upper_bound_def relax_def split: prod.splits)
-
-  lemma maintain_upper_bound': "upper_bound D \<Longrightarrow> upper_bound (relax_adjs u D)"
-    apply (auto simp: upper_bound_def relax_adjs_def split: prod.splits)
-
-  definition "D_invar D S \<equiv>
-    upper_bound D
-  \<and> (s\<in>S)
-  \<and> (\<forall>u\<in>S. D u = \<delta> s u \<and> \<delta> s u < \<infinity> \<and> (\<forall>v. D v \<le> \<delta> s u + w (u,v)))"

-
-  text \<open>Once \<open>D v\<close> reaches \<open>\<delta> s v\<close>, it never changes thereafter\<close>
-  lemma maintain_upper_bound2': "upper_bound D \<Longrightarrow> D v = \<delta> s v \<Longrightarrow> relax_adjs u D v = \<delta> s v"
-    apply (auto simp: relax_adjs_def min_def upper_bound_def)
-    by (meson triangle add_mono_thms_linordered_semiring(3) order_trans)
-
-  lemma maintain_D_invar_aux:
-    assumes I: "D_invar D S"
-    assumes UNS: "u\<notin>S"
-    assumes UNI: "D u < \<infinity>"
-    assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
-    shows "D u = \<delta> s u" "\<delta> s u < \<infinity>"
-  proof -
-    from I have "s\<in>S" and UB: "upper_bound D" by (auto simp: D_invar_def)
+  text \<open>Relax all outgoing edges of node \<open>u\<close>\<close>
+  definition relax_outgoing :: "'v \<Rightarrow> 'v estimate \<Rightarrow> 'v estimate"
+    where "relax_outgoing u D \<equiv> \<lambda>v. min (D v) (D u + w (u,v))"

-    from UNI UB show DSUNI: "\<delta> s u < \<infinity>"
-      by (clarsimp simp: upper_bound_def) (metis enat_ile)
-
-    obtain p where "path s p u" and DSU: "\<delta> s u = sum_list p"
-      by (rule obtain_shortest_path)
-    hence "path s p u" by (auto simp: paths_def)
-    from find_leave_edgeE[OF this \<open>s\<in>S\<close> \<open>u\<notin>S\<close>] obtain p1 x y p2 where
-      FLE: "p = p1 @ w (x, y) # p2" "x \<in> S" "y \<notin> S" "path s p1 x" "path y p2 u"
-      .
-
-    from FLE shortest_subpath[of s p1 x "w (x,y)#p2" u] DSUNI have DSX: "\<delta> s x = sum_list p1" and DSXNI: "\<delta> s x<\<infinity>"
-      by (fastforce simp: DSU)+
-    from FLE shortest_subpath[of s "p1@[w (x,y)]" y p2 u] DSUNI have DSY: "\<delta> s y = \<delta> s x + w (x, y)"
-      by (fastforce simp: DSU DSX)
-
-    with I \<open>x\<in>S\<close> have "D y = \<delta> s y"
-      by (auto simp: D_invar_def upper_bound_def) (metis eq_iff)
-    moreover have "\<dots> \<le> \<delta> s u" by (auto simp: DSU DSX DSY FLE(1))
-    moreover have "\<dots> \<le> D u" using UB by (auto simp: upper_bound_def)
-    moreover have "\<dots> \<le> D y" using \<open>u\<notin>S\<close> \<open>y\<notin>S\<close> MIN by auto
-    ultimately show "D u = \<delta> s u" by simp
-  qed
-
+  text \<open>Initialization\<close>
+  definition "initD \<equiv> (relax_outgoing s ((\<lambda>_. \<infinity>)(s:=0)))"
+  definition "initS \<equiv> {s}"

-  lemma maintain_D_invar:
-    assumes I: "D_invar D S"
-    assumes UNS: "u\<notin>S"
-    assumes UNI: "D u < \<infinity>"
-    assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
-    shows "D_invar (relax_adjs u D) (Set.insert u S)"
-    unfolding D_invar_def
-  proof (intro conjI ballI allI)
-    from maintain_upper_bound' I show "upper_bound (relax_adjs u D)"
-      unfolding D_invar_def by simp
-  next
-    from I show "s \<in> Set.insert u S" unfolding D_invar_def by simp
-  next
-    fix v
-    assume "v\<in>Set.insert u S"
-    then show "relax_adjs u D v = \<delta> s v"
-    proof safe
-      assume "v\<in>S"
-      with I have "D v = \<delta> s v" by (auto simp: D_invar_def)
-      with maintain_upper_bound2' I show "relax_adjs u D v = \<delta> s v"
-        by (auto simp: D_invar_def)
-    next
-      show "relax_adjs u D u = \<delta> s u"
-        by (auto simp: relax_adjs_def min_def maintain_D_invar_aux[OF I UNS UNI MIN])
-    qed
-  next
-    fix v v'
-    assume "v\<in>Set.insert u S"
-    then show "relax_adjs u D v' \<le> \<delta> s v + w (v, v')" "\<delta> s v < \<infinity>"
-      (* TODO: Clean-up *)
-      apply (auto simp: relax_adjs_def min_def)
-      subgoal using I MIN UNS UNI maintain_D_invar_aux by auto
-      subgoal using I MIN UNS UNI maintain_D_invar_aux by auto
-      subgoal using D_invar_def I by auto
-      subgoal using D_invar_def I linear order.trans by fastforce
-      subgoal using I MIN UNI UNS maintain_D_invar_aux(1) by auto
-      subgoal using D_invar_def I by auto
-      done
-  qed
+
+  text \<open>Relaxing will never increase estimates\<close>
+  lemma relax_mono: "relax_outgoing u D v \<le> D v"
+    by (auto simp: relax_outgoing_def)

-
-  lemma D_invar_init: "D_invar (relax_adjs s ((\<lambda>_. \<infinity>)(s:=0))) {s}"
-    by (auto simp: D_invar_def upper_bound_def relax_adjs_def shortest_path_direct)
-
-
-  lemma finish_D_invar:
-    assumes I: "D_invar D S"
-    assumes F: "\<forall>u. u\<notin>S \<longrightarrow> D u = \<infinity>"
-    shows "D u = \<delta> s u"
-  proof (cases "u\<in>S")
-    case True
-    then show ?thesis using I unfolding D_invar_def by auto
-  next
-    case False
-    from I have "s\<in>S"
-      using I unfolding D_invar_def by auto
-    obtain p where "path s p u" and DSU: "\<delta> s u = sum_list p"
-      by (rule obtain_shortest_path)
-    from find_leave_edgeE[OF \<open>path s p u\<close> \<open>s\<in>S\<close> \<open>u\<notin>S\<close>] obtain p1 x y p2
-      where FLE: "p = p1 @ w (x, y) # p2" "x \<in> S" "y \<notin> S" "path s p1 x" "path y p2 u" .
-    have "w (x,y) = \<infinity>"
-    proof (rule ccontr)
-      assume "w (x,y) \<noteq> \<infinity>"
-      moreover from I \<open>x\<in>S\<close> have "\<delta> s x < \<infinity>" "D y \<le> \<delta> s x + w (x,y)"
-        unfolding D_invar_def by auto
-      ultimately have "D y \<noteq> \<infinity>" using enat_ile by auto
-      with F \<open>y\<notin>S\<close> show False by auto
-    qed
-    with FLE have "\<delta> s u = \<infinity>" by (auto simp: DSU)
-    with F \<open>u\<notin>S\<close> show ?thesis by auto
-  qed
-
-  (* Termination *)
-
+
definition "all_dnodes \<equiv> { v . \<exists>u. w (u,v)\<noteq>\<infinity> }"
definition "unfinished_dnodes S \<equiv> all_dnodes - S "

lemma unfinished_nodes_subset: "unfinished_dnodes S \<subseteq> all_dnodes"
by (auto simp: unfinished_dnodes_def)
+
+
+
+end
+
+subsubsection \<open>Invariant\<close>
+text \<open>The invariant is defined as locale\<close>

+locale Dijkstra_Invar = Dijkstra w s for w and s :: 'v +
+  fixes D :: "'v estimate" and S :: "'v set"
+  assumes upper_bound: \<open>\<delta> s u \<le> D u\<close> \<comment> \<open>\<open>D\<close> is a valid estimate\<close>
+  assumes s_in_S: \<open>s\<in>S\<close> \<comment> \<open>The start node is finished\<close>
+  (* TODO: CLRS starts with empty S *)
+  assumes S_precise: "u\<in>S \<Longrightarrow> D u = \<delta> s u" \<comment> \<open>Finished nodes have precise estimate\<close>
+  assumes S_connected: \<open>u\<in>S \<Longrightarrow> \<delta> s u < \<infinity>\<close> \<comment> \<open>Finished nodes have finite distance\<close>
+  assumes S_relaxed: \<open>u\<in>S \<Longrightarrow> D v \<le> \<delta> s u + w (u,v)\<close> \<comment> \<open>Outgoing edges of finished
+    nodes have been relaxed, using precise distance\<close>
+begin
+
+  abbreviation (in Dijkstra) "D_invar \<equiv> Dijkstra_Invar w s"
+
+  text \<open>The invariant holds for the initial state\<close>
+  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 \<open>Relaxing some edges maintains the upper bound property\<close>
+  lemma maintain_upper_bound: "\<delta> s u \<le> (relax_outgoing v D) u"
+    apply (auto simp: relax_outgoing_def upper_bound split: prod.splits)
+    using triangle upper_bound add_right_mono dual_order.trans by blast
+
+  text \<open>Relaxing edges will not affect nodes with already precise estimates\<close>
+  lemma relax_precise_id: "D v = \<delta> s v \<Longrightarrow> relax_outgoing u D v = \<delta> s v"
+    using maintain_upper_bound upper_bound relax_mono
+    by (metis antisym)
+
+  text \<open>In particular, relaxing edges will not affect finished nodes\<close>
+  lemma relax_finished_id: "v\<in>S \<Longrightarrow> relax_outgoing u D v = D v"
+    by (simp add: S_precise relax_precise_id)
+
+  text \<open>The least (finite) estimate among all nodes \<open>u\<close> not in \<open>S\<close> is already precise.
+    This will allow us to add the node \<open>u\<close> to \<open>S\<close>. \<close>
+  lemma maintain_S_precise_and_connected:
+    assumes UNS: "u\<notin>S"
+    assumes UNI: "D u < \<infinity>"
+    assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
+    shows "D u = \<delta> s u" (*"\<delta> s u < \<infinity>"*)
+  proof -
+    note s_in_S
+
+    text \<open>Node \<open>u\<close> has a finite estimate, thus it has a finite distance from \<open>s\<close>\<close>
+    from UNI upper_bound have DSUNI: "\<delta> s u < \<infinity>"
+      by (clarsimp) (metis enat_ile)
+
+    text \<open>Consider a shortest path from \<open>s\<close> to \<open>u\<close>\<close>
+    obtain p where "path s p u" and DSU: "\<delta> s u = sum_list p"
+      by (rule obtain_shortest_path)
+    text \<open>It goes from inside \<open>S\<close> to outside \<open>S\<close>, so there must be an edge at the border.
+      Let \<open>(x,y)\<close> be such an edge, with \<open>x\<in>S\<close> and \<open>y\<notin>S\<close>.\<close>
+    from find_leave_edgeE[OF \<open>path s p u\<close> \<open>s\<in>S\<close> \<open>u\<notin>S\<close>] obtain p1 x y p2 where
+      [simp]: "p = p1 @ w (x, y) # p2" and DECOMP: "x \<in> S" "y \<notin> S" "path s p1 x" "path y p2 u" .
+    text \<open>As prefixes of shortest paths are again shortest paths, the shortest path to \<open>y\<close> ends with edge \<open>(x,y)\<close> \<close>
+    have DSX: "\<delta> s x = sum_list p1" and DSY: "\<delta> s y = \<delta> 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 \<open>\<delta> s u < \<infinity>\<close> DECOMP
+        by (force simp: DSU)+
+    text \<open>Upon adding \<open>x\<close> to \<open>S\<close>, this edge has been relaxed with the precise estimate for \<open>x\<close>.
+      At this point the estimate for \<open>y\<close> has become precise, too\<close>
+    with \<open>x\<in>S\<close> have "D y = \<delta> s y"
+      by (metis S_relaxed antisym_conv upper_bound)
+    moreover text \<open>The shortest path to \<open>y\<close> is a prefix of that to \<open>u\<close>, thus it shorter or equal\<close>
+    have "\<dots> \<le> \<delta> s u" using DSU by (simp add: DSX DSY)
+    moreover text \<open>The estimate for \<open>u\<close> is an upper bound\<close>
+    have "\<dots> \<le> D u" using upper_bound by (auto)
+    moreover text \<open>\<open>u\<close> was a node with smallest estimate\<close>
+    have "\<dots> \<le> D y" using \<open>u\<notin>S\<close> \<open>y\<notin>S\<close> MIN by auto
+    ultimately text \<open>This closed a cycle in the inequation chain. Thus, by antisymmetry, all items are equal.
+      In particular, \<open>D u = \<delta> s u\<close>, qed.\<close>
+    show "D u = \<delta> s u" by simp
+  qed
+
+  text \<open>A step of Dijkstra's algorithm maintains the invariant.
+    More precisely, in a step of Dijkstra's algorithm,
+    we pick a node \<open>u\<notin>S\<close> with least finite estimate, relax the outgoing
+    edges of \<open>u\<close>, and add \<open>u\<close> to \<open>S\<close>.\<close>
+  theorem maintain_D_invar:
+    assumes UNS: "u\<notin>S"
+    assumes UNI: "D u < \<infinity>"
+    assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
+    shows "D_invar (relax_outgoing u D) (Set.insert u S)"
+    apply unfold_locales
+    using maintain_S_precise_and_connected[OF assms] UNI S_connected S_precise
+    apply (auto simp: maintain_upper_bound upper_bound s_in_S relax_precise_id)
+    using S_relaxed relax_mono le_less_trans not_less by blast
+
+
+  text \<open>When the algorithm is finished, i.e., when there are
+    no unfinished nodes with finite estimates left,
+    then all estimates are accurate.\<close>
+  lemma invar_finish_imp_correct:
+    assumes F: "\<forall>u. u\<notin>S \<longrightarrow> D u = \<infinity>"
+    shows "D u = \<delta> s u"
+  proof (cases)
+    assume "u\<in>S" text \<open>The estimates of finished nodes are accurate\<close>
+    then show ?thesis using S_precise by simp
+  next
+    assume \<open>u\<notin>S\<close> text \<open>So consider an unfinished node \<open>u\<close>\<close>
+    note s_in_S
+
+    {
+      text \<open>We will show that it is not connected to \<open>s\<close>\<close>
+      presume "\<delta> s u = \<infinity>"
+      text \<open>Thus, both its estimate and its distance must be \<open>\<infinity>\<close>\<close>
+      with upper_bound[of u] show "D u = \<delta> s u" by auto
+    }
+
+    text \<open>It remains to show that \<open>\<delta> s u = \<infinity>\<close>. For this, we obtain a shortest path to \<open>u\<close>\<close>
+    obtain p where "path s p u" and DSU: "\<delta> s u = sum_list p"
+      by (rule obtain_shortest_path)
+    text \<open>And find an edge where it leaves \<open>S\<close>\<close>
+    from find_leave_edgeE[OF \<open>path s p u\<close> \<open>s\<in>S\<close> \<open>u\<notin>S\<close>] obtain p1 x y p2
+      where [simp]: "p = p1 @ w (x, y) # p2" and DECOMP: "x \<in> S" "y \<notin> S" "path s p1 x" "path y p2 u" .
+    text \<open>As \<open>x\<in>S\<close>, it has a finite distance, and the edge \<open>(x,y)\<close> got relaxed
+      with a precise estimate for \<open>x\<close>. However, as we terminated and \<open>y\<notin>S\<close>,
+      the estimate for \<open>y\<close> is \<open>\<infinity>\<close>. Thus, the edge has infinite weight.\<close>
+    have "w (x,y) = \<infinity>"
+      using S_connected[OF \<open>x\<in>S\<close>] S_relaxed[OF \<open>x\<in>S\<close>, of y] F \<open>y\<notin>S\<close>
+      by (cases "w (x,y)") auto
+    text \<open>And so has the path on which this edge lays\<close>
+    then show "\<delta> s u = \<infinity>" by (auto simp: DSU)
+  qed
+
+
+  text \<open>A step decreases the set of unfinished nodes.\<close>
lemma unfinished_nodes_decr:
-    assumes I: "D_invar D S"
assumes UNS: "u\<notin>S"
assumes UNI: "D u < \<infinity>"
shows "unfinished_dnodes (Set.insert u S) \<subset> unfinished_dnodes S"
proof -
-    from I have \<open>s\<in>S\<close> and UB: "upper_bound D" by (auto simp: D_invar_def)
-
+    note s_in_S
+
text \<open>There is a path to \<open>u\<close>\<close>
-    from UNI UB have "\<delta> s u < \<infinity>"
-      by (auto simp: upper_bound_def) (metis enat_ile)
+    from UNI have "\<delta> s u < \<infinity>" using upper_bound[of u] leD by fastforce

-    text \<open>Thus, \<open>u\<close> must have incoming edge\<close>
+    text \<open>Thus, \<open>u\<close> must have an incoming edge and is among \<open>all_dnodes\<close>\<close>
have "u\<in>all_dnodes"
proof -
obtain p where "path s p u" "sum_list p < \<infinity>"
@@ -290,135 +209,137 @@
apply (auto simp: all_dnodes_def)
using not_infinity_eq by fastforce
qed
+    text \<open>Which implies the proposition\<close>
with \<open>u\<notin>S\<close> show ?thesis by (auto simp: unfinished_dnodes_def)
qed
-
-
-end
-
-(* Refinement: D and S by priority map and map *)
+
+
+end

-lemma Abs_enat_inj[simp]: "Abs_enat x = Abs_enat y \<longleftrightarrow> x=y"
-  by (metis Abs_enat_inverse UNIV_I)
+subsection \<open>Refinement by Priority Map and Map\<close>
+text \<open>
+  In a second step, we implement \<open>D\<close> and \<open>S\<close> by a priority map \<open>Q\<close> and a map \<open>V\<close>.
+  Both map nodes to finite weights, where \<open>Q\<close> maps unfinished nodes, and \<open>V\<close> maps
+  finished nodes.
+
+  Note that this implementation is slightly non-standard:
+  In the standard implementation, \<open>Q\<close> contains also unfinished nodes with
+  infinite weight.
+
+  We chose this implementation because it avoids enumerating all nodes of
+  the graph upon initialization of \<open>Q\<close>.
+  However, on relaxing an edge to a node not in \<open>Q\<close>, we require an extra
+  lookup to check whether the node is finished.
+\<close>
+
+subsubsection \<open>Implementing \<open>enat\<close> by Option\<close>

-lemma Abs_enat_simps[simp]:
-  "Abs_enat None = \<infinity>"
-  "Abs_enat (Some n) = enat n"
-  "Abs_enat x = enat n \<longleftrightarrow> x = Some n"
-  "Abs_enat x = \<infinity> \<longleftrightarrow> x = None"
-  "enat n = Abs_enat x \<longleftrightarrow> x = Some n"
-  "\<infinity> = Abs_enat x \<longleftrightarrow> x = None"
-  apply ((auto simp: enat_def infinity_enat_def; fail)+) [2]
-  apply (cases x; auto simp: enat_def infinity_enat_def; fail)+
-  done
+text \<open>Our maps are functions to \<open>nat option\<close>,which are interpreted as \<open>enat\<close>,
+  \<open>None\<close> being \<open>\<infinity>\<close>\<close>
+
+fun enat_of_option :: "nat option \<Rightarrow> enat" where
+  "enat_of_option None = \<infinity>"
+| "enat_of_option (Some n) = enat n"

-lemma Abs_enat_le_conv: "Abs_enat m \<le> Abs_enat n \<longleftrightarrow> (case (m,n) of
+lemma enat_of_option_inj[simp]: "enat_of_option x = enat_of_option y \<longleftrightarrow> x=y"
+  by (cases x; cases y; simp)
+
+lemma enat_of_option_simps[simp]:
+  "enat_of_option x = enat n \<longleftrightarrow> x = Some n"
+  "enat_of_option x = \<infinity> \<longleftrightarrow> x = None"
+  "enat n = enat_of_option x \<longleftrightarrow> x = Some n"
+  "\<infinity> = enat_of_option x \<longleftrightarrow> x = None"
+  by (cases x; auto; fail)+
+
+lemma enat_of_option_le_conv: "enat_of_option m \<le> enat_of_option n \<longleftrightarrow> (case (m,n) of
(_,None) \<Rightarrow> True
| (Some a, Some b) \<Rightarrow> a\<le>b
| (_, _) \<Rightarrow> False
)"
by (auto split: option.split)

-
-
-
+
+
+subsubsection \<open>Implementing \<open>D,S\<close> by Priority Map and Map\<close>
context Dijkstra begin
+  text \<open>We define a coupling relation, that connects the concrete with the
+    abstract data. \<close>
definition "coupling Q V D S \<equiv>
-    D = Abs_enat o (V ++ Q)
+    D = enat_of_option o (V ++ Q)
\<and> S = dom V
\<and> dom V \<inter> dom Q = {}"

+  text \<open>Note that our coupling relation is functional.\<close>
+  (* TODO: Why not use functions instead? *)
+  lemma coupling_fun: "coupling Q V D S \<Longrightarrow> coupling Q V D' S' \<Longrightarrow> D'=D \<and> S'=S"
+    by (auto simp: coupling_def)

+  text \<open>The concrete version of the invariant.\<close>
definition "D_invar' Q V \<equiv>
\<exists>D S. coupling Q V D S \<and> D_invar D S"

-  text \<open>Relaxation does not change estimates for finished nodes\<close>
-  lemma relax_S_idem:
-    assumes I: "D_invar D S"
-    assumes "v\<in>S"
-    shows "relax_adjs u D v = D v"
-  proof -
-    have "D v = \<delta> s v" using I \<open>v\<in>S\<close> by (auto simp: D_invar_def)
-    also have "\<dots> \<le> \<delta> s u + w (u, v)" using triangle .
-    also have "\<delta> s u \<le> D u" using I by (auto simp: D_invar_def upper_bound_def)
-    finally have "D v \<le> D u + w (u, v)" by simp
-    thus ?thesis unfolding relax_adjs_def by (auto simp: min_def)
-  qed
-
-  text \<open>Relaxation of non-edge (infinite weight) does not change estimates\<close>
-  lemma relax_inf_edge_idem:
-    "w (u,v) = \<infinity> \<Longrightarrow> relax_adjs u D v = D v"

-  text \<open>Relaxation of edges from node with infinite estimate does not change estimates\<close>
-  lemma relax_inf_source_idem:
-    "D u = \<infinity> \<Longrightarrow> relax_adjs u D v = D v"
-
-
-  definition "decrease_point Q d v \<equiv> case Q v of None \<Rightarrow> Some d | Some d' \<Rightarrow> Some (min d' d)"
-
-  definition "relax_adjs' u du V Q v \<equiv>
-    if v\<in>dom V then Q v
-    else
-      case w (u,v) of
-        enat d \<Rightarrow> decrease_point Q (du+d) v
-      | _ \<Rightarrow> Q v
+  text \<open>Refinement of \<open>relax-outgoing\<close>\<close>
+
+  definition "relax_outgoing' u du V Q v \<equiv>
+    case w (u,v) of
+      \<infinity> \<Rightarrow> Q v
+    | enat d \<Rightarrow> (case Q v of
+        None \<Rightarrow> if v\<in>dom V then None else Some (du+d)
+      | Some d' \<Rightarrow> Some (min d' (du+d)))
"

-
-  lemma coupling_step:
-    assumes I: "D_invar D S"
+
+  text \<open>A step preserves the coupling relation.\<close>
+  lemma (in Dijkstra_Invar) coupling_step:
assumes C: "coupling Q V D S"
assumes UNS: "u\<notin>S"
assumes UNI: "D u = enat du"

-    shows "coupling ((relax_adjs' u du V Q)(u:=None)) (V(u\<mapsto>du)) (relax_adjs u D) (Set.insert u S)"
-      and "Q u = Some du" "V u = None" (* TODO: These are unused! *)
+    shows "coupling ((relax_outgoing' u du V Q)(u:=None)) (V(u\<mapsto>du)) (relax_outgoing u D) (Set.insert u S)"
using C unfolding coupling_def
-    apply -
-    apply (all \<open>(intro ext conjI)?\<close>)
-    apply (all \<open>elim conjE\<close>)
-  proof -
-    assume \<alpha>: "D = Abs_enat \<circ> V ++ Q" "S = dom V"
+  proof (intro ext conjI; elim conjE)
+    assume \<alpha>: "D = enat_of_option \<circ> V ++ Q" "S = dom V"
and DD: "dom V \<inter> dom Q = {}"

show "Set.insert u S = dom (V(u \<mapsto> du))"
by (auto simp: \<alpha>)

-    show [simp]: "Q u = Some du" "V u = None"
+    have [simp]: "Q u = Some du" "V u = None"
using DD UNI UNS by (auto simp: \<alpha>)

-    from DD show "dom (V(u \<mapsto> du)) \<inter> dom ((relax_adjs' u du V Q)(u := None)) = {}"
-      by (auto simp: relax_adjs'_def dom_def split: if_splits)
+    from DD show "dom (V(u \<mapsto> du)) \<inter> 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_adjs u D v = (Abs_enat \<circ> V(u \<mapsto> du) ++ (relax_adjs' u du V Q)(u := None)) v"
+    show "relax_outgoing u D v = (enat_of_option \<circ> V(u \<mapsto> du) ++ (relax_outgoing' u du V Q)(u := None)) v"
proof (cases "v\<in>S")
case True
-      then show ?thesis
-        apply (simp add: relax_S_idem[OF I])
+      then show ?thesis using DD
by (auto
+          simp: relax_outgoing'_def map_add_apply \<alpha> 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 \<alpha> min_def
split: option.splits enat.splits)
qed
qed

+  text \<open>Refinement of initial state\<close>
definition "initQ v \<equiv> if s=v then None else case w (s,v) of \<infinity> \<Rightarrow> None | enat d \<Rightarrow> Some d"
+  definition "initV \<equiv> [s\<mapsto>0]"

lemma coupling_init:
-    "coupling initQ [s\<mapsto>0] (relax_adjs s ((\<lambda>_. \<infinity>)(s:=0))) {s}"
-    unfolding coupling_def
+    "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)

@@ -428,34 +349,43 @@
using assms

-
-  (* Implementing relax_adjs' on successor list *)

-  definition "decrease_key v d Q \<equiv> Q(v \<mapsto> case Q v of None \<Rightarrow> d | Some d' \<Rightarrow> min d d')"
+  text \<open>Termination argument: Refinement of unfinished nodes.\<close>
+  definition "unfinished_dnodes' V \<equiv> unfinished_dnodes (dom V)"
+
+  lemma coupling_unfinished: "coupling Q V D S \<Longrightarrow> unfinished_dnodes' V = unfinished_dnodes S"
+    by (auto simp: coupling_def unfinished_dnodes'_def unfinished_dnodes_def)

-  definition "relax_adjs'' l du V Q = fold (\<lambda>(d,v) Q. if v\<in>dom V then Q else decrease_key v (du+d) Q) l Q"
+
+
+  subsubsection \<open>Implementing graph by successor list\<close>

+  definition "relax_outgoing'' l du V Q = fold (\<lambda>(d,v) Q.
+    case Q v of None \<Rightarrow> if v\<in>dom V then Q else Q(v\<mapsto>du+d)
+              | Some d' \<Rightarrow> Q(v\<mapsto>min (du+d) d')) l Q"
+
+
+  lemma relax_outgoing''_refine:
assumes "set l = {(d,v). w (u,v) = enat d}"
-    shows "relax_adjs'' l du V Q = relax_adjs' u du V Q"
+    shows "relax_outgoing'' l du V Q = relax_outgoing' u du V Q"
proof
fix v

have aux1:
-       "relax_adjs'' l du V Q v = (if v\<in>snd`set l then relax_adjs' u du V Q v else Q v)"
+       "relax_outgoing'' l du V Q v = (if v\<in>snd`set l then relax_outgoing' u du V Q v else Q v)"
if "set l \<subseteq> {(d,v). w (u,v) = enat d}"
using that
apply (induction l arbitrary: Q v)
apply (auto
+        simp: relax_outgoing''_def relax_outgoing'_def image_iff
split!: if_splits option.splits)
done

have aux2:
-      "relax_adjs' u du V Q v = Q v" if "w (u,v) = \<infinity>"
-      using that by (auto simp: relax_adjs'_def)
+      "relax_outgoing' u du V Q v = Q v" if "w (u,v) = \<infinity>"
+      using that by (auto simp: relax_outgoing'_def)

-    show "relax_adjs'' l du V Q v = relax_adjs' u du V Q v"
+    show "relax_outgoing'' l du V Q v = relax_outgoing' u du V Q v"
using aux1
apply (cases "w (u,v)")
by (all \<open>force simp: aux2 assms\<close>)
@@ -491,46 +421,16 @@
qed
qed

-
-  definition "unfinished_dnodes' V \<equiv> unfinished_dnodes (dom V)"
-
-  lemma coupling_unfinished: "coupling Q V D S \<Longrightarrow> unfinished_dnodes' V = unfinished_dnodes S"
-    by (auto simp: coupling_def unfinished_dnodes'_def unfinished_dnodes_def)
-
end

-
-definition "edges w \<equiv> {(u,v) . w (u,v) \<noteq> \<infinity>}"
-
-  fixes \<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph"
-    and invar :: "'g \<Rightarrow> bool"
-    and succ :: "'g \<Rightarrow> 'v \<Rightarrow> (nat\<times>'v) list"
-    and empty_graph :: 'g
-    and add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'g \<Rightarrow> 'g"
-  assumes succ_correct: "invar g \<Longrightarrow> set (succ g u) = {(d,v). \<alpha> g (u,v) = enat d}"
-  assumes empty_graph_correct:
-    "invar empty_graph"
-    "\<alpha> empty_graph = (\<lambda>_. \<infinity>)"
-    "invar g \<Longrightarrow> \<alpha> g e = \<infinity> \<Longrightarrow> invar (add_edge e d g)"
-    "invar g \<Longrightarrow> \<alpha> g e = \<infinity> \<Longrightarrow> \<alpha> (add_edge e d g) = (\<alpha> g)(e:=enat d)"
-begin
-
-
-  lemmas wgraph_specs = succ_correct empty_graph_correct add_edge_correct
-
-end
-
-locale adt_finite_wgraph = adt_wgraph where \<alpha>=\<alpha> for \<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph" +
-  assumes finite: "invar g \<Longrightarrow> finite (edges (\<alpha> g))"

+ M: Map M_empty M_update M_delete M_lookup M_invar
+ Q: PrioMap Q_empty Q_update Q_delete Q_invar Q_lookup Q_is_empty Q_getmin

-  for G_\<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph" and G_invar G_succ G_empty G_add
+  for G_\<alpha> :: "'g \<Rightarrow> ('v) wgraph" and G_invar G_succ G_empty G_add
and M_empty M_update M_delete and M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> nat option" and M_invar
and Q_empty Q_update Q_delete Q_invar and Q_lookup :: "'q \<Rightarrow> 'v \<Rightarrow> nat option" and Q_is_empty Q_getmin
begin
@@ -555,17 +455,17 @@

locale Dijkstra_Impl_Defs = Dijkstra_Impl_Adts where G_\<alpha> = G_\<alpha>
+ Dijkstra \<open>G_\<alpha> g\<close> s
-  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder,enat) wgraph" and g s
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder) wgraph" and g s

locale Dijkstra_Impl = Dijkstra_Impl_Defs where G_\<alpha> = G_\<alpha>
-  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder,enat) wgraph"
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder) wgraph"
+
assumes G_invar[simp]: "G_invar g"
begin
lemma finite_all_dnodes[simp, intro!]: "finite all_dnodes"
proof -
-    have "all_dnodes \<subseteq> snd ` edges (G_\<alpha> g)"
+    have "all_dnodes \<subseteq> snd ` edges"
by (fastforce simp: all_dnodes_def edges_def image_iff)
also have "finite \<dots>" by (auto simp: G.finite)
finally (finite_subset) show ?thesis .
@@ -575,45 +475,31 @@
using finite_subset[OF unfinished_nodes_subset] by auto

-  definition (in Dijkstra_Impl_Defs) "Q_decrease_key v d Q \<equiv> case Q_lookup Q v of
-    None \<Rightarrow> Q_update v d Q
-  | Some d' \<Rightarrow> Q_update v (min d d') Q"
-
-  lemma Q_decrease_key[simp]:
-    assumes [simp]: "Q_invar Q"
-    shows "Q_invar (Q_decrease_key v d Q)"
-      and "Q_lookup (Q_decrease_key v d Q) = decrease_key v d (Q_lookup Q)"
-    by (auto simp: Q_decrease_key_def decrease_key_def split: option.split)
-
-  (* TODO: Local definition in lemma? *)
-  definition (in Dijkstra_Impl_Defs)
-    "Q_relax_adjs1 l du V Q = fold (\<lambda>(d,v) Q. if M_lookup V v \<noteq> None then Q else Q_decrease_key v (du+d) Q) l Q"
+  lemma (in -) fold_refine:
+    assumes "I s"
+    assumes "\<And>s x. I s \<Longrightarrow> x\<in>set l \<Longrightarrow> I (f x s) \<and> \<alpha> (f x s) = f' x (\<alpha> s)"
+    shows "I (fold f l s) \<and> \<alpha> (fold f l s) = fold f' l (\<alpha> s)"
+    using assms
+    by (induction l arbitrary: s) auto

-    assumes "Q_invar Q"
-    shows "Q_invar (Q_relax_adjs1 l du V Q) \<and> Q_lookup (Q_relax_adjs1 l du V Q) = relax_adjs'' l du (M_lookup V) (Q_lookup Q)"
-    using assms
-    apply (induction l arbitrary: Q)
-    done
-
-  definition (in Dijkstra_Impl_Defs) "Q_relax_adjs u du V Q \<equiv> Q_relax_adjs1 (G_succ g u) du V Q"
-
+  definition (in Dijkstra_Impl_Defs) "Q_relax_outgoing u du V Q = fold (\<lambda>(d,v) Q.
+    case Q_lookup Q v of None \<Rightarrow> if M_lookup V v \<noteq> None then Q else Q_update v (du+d) Q
+              | Some d' \<Rightarrow> Q_update v (min (du+d) d') Q) ((G_succ g u)) Q"
+
+  lemma Q_relax_outgoing[simp]:
assumes [simp]: "Q_invar Q"
-    shows "Q_invar (Q_relax_adjs u du V Q) \<and> Q_lookup (Q_relax_adjs u du V Q) = relax_adjs' u du (M_lookup V) (Q_lookup Q)"
-    by simp
+    shows "Q_invar (Q_relax_outgoing u du V Q) \<and> Q_lookup (Q_relax_outgoing u du V Q) = relax_outgoing' u du (M_lookup V) (Q_lookup Q)"
+    apply (subst relax_outgoing''_refine[symmetric, where l="G_succ g u"])
+    apply simp
+    unfolding Q_relax_outgoing_def relax_outgoing''_def
+    apply (rule fold_refine[where I=Q_invar and \<alpha>=Q_lookup])
+    by (auto split: option.split)

definition (in Dijkstra_Impl_Defs) "D_invar_impl Q V \<equiv>
Q_invar Q \<and> M_invar V \<and> D_invar' (Q_lookup Q) (M_lookup V)"

definition (in Dijkstra_Impl_Defs)
"Q_initQ s' \<equiv> fold (\<lambda>(d,v) Q. if s'=v then Q else Q_update v d Q) (G_succ g s') Q_empty"
-
-  definition (in Dijkstra_Impl_Defs) "test \<equiv> (Q_initQ s)"

lemma Q_init_Q[simp]:
shows "Q_invar (Q_initQ s)" "Q_lookup (Q_initQ s) = initQ"
@@ -636,6 +522,12 @@
finally show "Q_lookup (Q_initQ s) = initQ" .
qed

+
+  definition (in Dijkstra_Impl_Defs)
+    "M_initV \<equiv> M_update s 0 M_empty"
+
+  lemma M_initS[simp]: "M_invar M_initV" "M_lookup M_initV = initV"
+    unfolding M_initV_def initV_def by auto

term Q_getmin

@@ -643,12 +535,12 @@
"dijkstra_loop \<equiv> while (\<lambda>(Q,V). \<not> Q_is_empty Q) (\<lambda>(Q,V).
let
(u,du) = Q_getmin Q;
-        Q = Q_relax_adjs u du V Q;
+        Q = Q_relax_outgoing u du V Q;
Q = Q_delete u Q;
V = M_update u du V
in
(Q,V)
-    ) (Q_initQ s,M_update s 0 M_empty)"
+    ) (Q_initQ s,M_initV)"

definition (in Dijkstra_Impl_Defs) "dijkstra \<equiv> snd dijkstra_loop"

@@ -671,8 +563,7 @@
apply (intro exI conjI)
apply (rule coupling_init)
-      apply (rule D_invar_init)
-      done
+      using initD_def initS_def invar_init by auto
proof -
fix Q V u du
assume "\<not> Q_is_empty Q" "D_invar_impl Q V" "Q_getmin Q = (u, du)"
@@ -681,24 +572,26 @@
and "Q_lookup Q u = Some du" "\<forall>k' p'. Q_lookup Q k' = Some p' \<longrightarrow> du \<le> p'"
by (auto simp: D_invar_impl_def elim: Q.map_getminE)

-    then obtain D S where COUPLING: "D_invar D S" "coupling (Q_lookup Q) (M_lookup V) D S"
+    then obtain D S where "D_invar D S" and COUPLING: "coupling (Q_lookup Q) (M_lookup V) D S"
and ABS_PRE: "D u = enat du" "u\<notin>S" "\<forall>v. v \<notin> S \<longrightarrow> D u \<le> D v"
by (auto simp: D_invar'_def transfer_preconditions less_eq_enat_def split: enat.splits)

+    then interpret Dijkstra_Invar "G_\<alpha> g" s D S by simp
+
have COUPLING': "coupling
-        ((relax_adjs' u du (M_lookup V) (Q_lookup Q))(u := None)) (M_lookup V(u \<mapsto> du))
-        (relax_adjs u D) (Set.insert u S)"
-      using coupling_step(1)[OF COUPLING \<open>u\<notin>S\<close> \<open>D u = enat du\<close>] by auto
+        ((relax_outgoing' u du (M_lookup V) (Q_lookup Q))(u := None)) (M_lookup V(u \<mapsto> du))
+        (relax_outgoing u D) (Set.insert u S)"
+      using coupling_step[OF COUPLING \<open>u\<notin>S\<close> \<open>D u = enat du\<close>] by auto

-    show "D_invar_impl (Q_delete u (Q_relax_adjs u du V Q)) (M_update u du V)"
-      using maintain_D_invar[OF \<open>D_invar D S\<close> \<open>u\<notin>S\<close>] ABS_PRE
+    show "D_invar_impl (Q_delete u (Q_relax_outgoing u du V Q)) (M_update u du V)"
+      using maintain_D_invar[OF \<open>u\<notin>S\<close>] ABS_PRE
using COUPLING'
by (auto simp: D_invar_impl_def D_invar'_def)

show "unfinished_dnodes' (M_lookup (M_update u du V)) \<subset> unfinished_dnodes' (M_lookup V) \<and>
finite (unfinished_dnodes' (M_lookup V))"
-      using coupling_unfinished[OF COUPLING(2)] coupling_unfinished[OF COUPLING']
-      using unfinished_nodes_decr[OF \<open>D_invar D S\<close> \<open>u\<notin>S\<close>] ABS_PRE
+      using coupling_unfinished[OF COUPLING] coupling_unfinished[OF COUPLING']
+      using unfinished_nodes_decr[OF \<open>u\<notin>S\<close>] ABS_PRE
by simp
qed

@@ -709,7 +602,7 @@
apply (all \<open>clarsimp simp: D_invar_impl_def\<close>)
apply (clarsimp simp: D_invar'_def)
subgoal for Q V D S
-      using finish_D_invar[of D S u]
+      using Dijkstra_Invar.invar_finish_imp_correct[of "G_\<alpha> g" s D S u]
apply (clarsimp simp: coupling_def)
by (auto simp: domIff)
done
@@ -717,95 +610,8 @@

end

-(*
-  Maps with to-list interface.
-  Iterations can be optimized by deforestation lemmas in a later step ...
-  even in code-generator preprocessor.
-*)
-locale Iterable_Map = Map +
-  fixes to_list :: "'m \<Rightarrow> ('k \<times> 'v) list"
-  assumes map_to_list: "invar m \<Longrightarrow> lookup m = map_of (to_list m) \<and> distinct (map fst (to_list m))"

-locale Iterable_Ordered_Map = Iterable_Map +
-  assumes map_to_list_sorted: "invar m \<Longrightarrow> sorted1 (to_list m)"
-
-context Map_by_Ordered begin
-
-  sublocale Iterable_Ordered_Map empty update delete lookup invar inorder
-    apply unfold_locales
-    unfolding invar_def
-    apply (auto simp: inorder_lookup distinct_if_sorted)
-    done
-
-end
-
-
-fun the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
-  "the_default d None = d"
-| "the_default _ (Some x) = x"
-
-
-lemma distinct_map_snd_inj: "distinct (map snd l) \<Longrightarrow> (a,b)\<in>set l \<Longrightarrow> (a',b)\<in>set l \<Longrightarrow> a=a'"
-  by (metis distinct_map inj_onD prod.sel(2) prod.simps(1))
-
-(* TODO: Move *)
-lemma edges_empty[simp]: "edges (\<lambda>_. \<infinity>) = {}" by (auto simp: edges_def)
-lemma edges_insert[simp]: "edges (g(e:=enat d)) = Set.insert e (edges g)" by (auto simp: edges_def)
-
-lemma prod_case_const[simp]: "case_prod (\<lambda>_ _. c) = (\<lambda>_. c)" by auto
-
-locale wgraph_by_map =
-  M: Map M_empty M_update M_delete M_lookup M_invar
-
-  for M_empty M_update M_delete and M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> ((nat\<times>'v) list) option" and M_invar
-begin
-  definition \<alpha> :: "'m \<Rightarrow> ('v,enat) wgraph" where
-    "\<alpha> g \<equiv> \<lambda>(u,v). case M_lookup g u of
-      None \<Rightarrow> \<infinity>
-    | Some l \<Rightarrow> if \<exists>d. (d,v)\<in>set l then enat (SOME d. (d,v)\<in>set l) else \<infinity>"
-
-  definition invar :: "'m \<Rightarrow> bool" where
-    "invar g \<equiv> M_invar g \<and> (\<forall>l\<in>ran (M_lookup g). distinct (map snd l)) \<and> finite (edges (\<alpha> g))"
-
-  definition succ :: "'m \<Rightarrow> 'v \<Rightarrow> (nat \<times> 'v) list" where
-    "succ g v = the_default [] (M_lookup g v)"
-
-  definition empty_graph :: "'m" where "empty_graph = M_empty"
-
-  definition add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'm \<Rightarrow> 'm" where
-    "add_edge \<equiv> \<lambda>(u,v) d g. M_update u ((d,v) # the_default [] (M_lookup g u)) g"
-
-    apply unfold_locales
-    subgoal for g u
-      apply (cases "M_lookup g u")
-      apply (auto
-        simp: invar_def \<alpha>_def succ_def ran_def
-        intro: distinct_map_snd_inj someI
-        split: option.splits
-      )
-      done
-    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
-    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
-  proof -
-    (* Explicit proof to nicely handle finiteness constraint, using already proved shape of abstract result *)
-    fix g e d
-    assume A: "invar g" "\<alpha> g e = \<infinity>"
-    then show AAE: "\<alpha> (add_edge e d g) = (\<alpha> g)(e := enat d)"
-      by (auto
-        simp: invar_def \<alpha>_def add_edge_def M.map_specs
-        split: option.splits if_splits prod.splits
-      )
-
-    from A show "invar (add_edge e d g)"
-      apply (simp add: invar_def AAE)
-      by (force
-        simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs ran_def
-        split: option.splits if_splits prod.splits)
-
-end
-
+subsection \<open>Instantiation of ADTs and Code Generation\<close>

global_interpretation
G: wgraph_by_map RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
@@ -813,11 +619,6 @@
and G_succ = G.succ
by unfold_locales
-print_theorems
-
-export_code G_empty G_succ G_add_edge in SML
-
-

@@ -832,11 +633,9 @@
G.\<alpha> g s for g and s::"'v::linorder"
defines dijkstra = D.dijkstra
and dijkstra_loop = D.dijkstra_loop
+      and Q_relax_outgoing = D.Q_relax_outgoing
+      and M_initV = D.M_initV
and Q_initQ = D.Q_initQ
-      and Q_decrease_key = D.Q_decrease_key
-      and test = D.test
..

(* TODO: Why is this fix necessary? *)
@@ -859,107 +658,29 @@

end

-
-
export_code dijkstra in SML
-thm dijkstra_correct
-
-
-text \<open>A list represents a graph if there are no multi-edges or duplicate edges\<close>
-definition "valid_graph_rep l \<equiv>
-  (\<forall>u d d' v. (u,v,d)\<in>set l \<and> (u,v,d')\<in>set l \<longrightarrow> d=d')
-\<and> distinct l
-  "
-
-text \<open>Alternative characterization: all node pairs must be distinct\<close>
-lemma valid_graph_rep_code[code]: "valid_graph_rep l \<longleftrightarrow> distinct (map (\<lambda>(u,v,_). (u,v)) l)"
-  by (auto simp: valid_graph_rep_def distinct_map inj_on_def)
-
-lemma valid_graph_rep_simps[simp]:
-  "valid_graph_rep []"
-  "valid_graph_rep ((u,v,d) # l) \<longleftrightarrow> valid_graph_rep l \<and> (\<forall>d'. (u,v,d')\<notin>set l)"
-  by (auto simp: valid_graph_rep_def)
-
-
-text \<open>For a valid graph representation, there is exactly one graph that corresponds to it\<close>
-lemma valid_graph_rep_ex1: "valid_graph_rep l \<Longrightarrow> \<exists>! w. \<forall>u v d. w (u,v) = enat d \<longleftrightarrow> (u,v,d)\<in>set l"
-  unfolding valid_graph_rep_code
-  apply (auto)
-  subgoal
-    apply (rule exI[where x="\<lambda>(u,v). if \<exists>d. (u,v,d)\<in>set l then enat (SOME d. (u,v,d)\<in>set l) else \<infinity>"])
-    apply (auto intro: someI simp: distinct_map inj_on_def split: prod.splits; blast)
-    done
-  subgoal for w w'
-    apply (auto del: ext intro!: ext)
-    by (metis (mono_tags, hide_lams) not_enat_eq)
-  done

-text \<open>We define this graph using determinate choice\<close>
-definition "wgraph_of_list l \<equiv> \<lambda>(u,v). if \<exists>d. (u,v,d)\<in>set l then enat (THE d. (u,v,d)\<in>set l) else \<infinity>"
-
-
-begin
-
-  definition "from_list l \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l empty_graph"
-
-  definition "edges_undef l w \<equiv> \<forall>u v d. (u,v,d)\<in>set l \<longrightarrow> w (u,v) = \<infinity>"
-
-  lemma edges_undef_simps[simp]:
-    "edges_undef [] w"
-    "edges_undef l (\<lambda>_. \<infinity>)"
-    "edges_undef ((u,v,d)#l) w \<longleftrightarrow> edges_undef l w \<and> w (u,v) = \<infinity>"
-    "edges_undef l (w((u,v) := enat d)) \<longleftrightarrow> edges_undef l w \<and> (\<forall>d'. (u,v,d')\<notin>set l)"
-    by (auto simp: edges_undef_def)
-
-  lemma from_list_correct_aux:
-    assumes "valid_graph_rep l"
-    assumes "edges_undef l (\<alpha> g)"
-    assumes "invar g"
-    defines "g' \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l g"
-    shows "invar g'" "(\<forall>u v d. \<alpha> g' (u,v) = enat d \<longleftrightarrow> \<alpha> g (u,v) = enat d \<or> (u,v,d)\<in>set l)"
-    using assms(1-3) unfolding g'_def
-    apply (induction l arbitrary: g)
-    apply (auto simp: wgraph_specs split: if_splits)
-    done
-
-  lemma from_list_correct:
-    assumes "valid_graph_rep l"
-    shows "invar (from_list l)" "(u,v,d)\<in>set l \<longleftrightarrow> \<alpha> (from_list l) (u,v) = enat d"
-    unfolding from_list_def using from_list_correct_aux[OF assms, where g=empty_graph]
-    by (auto simp: wgraph_specs)
-
-  lemma from_list_correct':
-    assumes "valid_graph_rep l"
-    shows "invar (from_list l)" "\<alpha> (from_list l) = wgraph_of_list l"
-    using from_list_correct[OF assms] valid_graph_rep_ex1[OF assms]
-    unfolding wgraph_of_list_def
-    by fastforce+
-
-end
+subsection \<open>Combination with Graph Parser\<close>
+text \<open>We combine the algorithm with a parser from lists to graphs\<close>

global_interpretation G: wgraph_from_list_algo G.\<alpha> G.invar G.succ G.empty_graph G.add_edge
defines from_list = G.from_list
..

-export_code "G.from_list" in SML
-
-
-thm dijkstra_correct
-
+
definition "dijkstra_list l s \<equiv> if valid_graph_rep l then Some (dijkstra (from_list l) s) else None"

-lemma "case dijkstra_list l s of
-  None \<Rightarrow> \<not>valid_graph_rep l
-| Some D \<Rightarrow> valid_graph_rep l \<and> M.invar D \<and> (\<forall>u d. lookup D u = Some d \<longleftrightarrow> WGraph.\<delta> (wgraph_of_list l) s u = enat d)"
+theorem dijkstra_list_correct:
+  "case dijkstra_list l s of
+    None \<Rightarrow> \<not>valid_graph_rep l
+  | Some D \<Rightarrow> valid_graph_rep l \<and> M.invar D \<and> (\<forall>u d. lookup D u = Some d \<longleftrightarrow> WGraph.\<delta> (wgraph_of_list l) s u = enat d)"
unfolding dijkstra_list_def
-  by (auto simp: dijkstra_correct G.from_list_correct')
+  by (auto simp: dijkstra_correct G.from_list_correct)

-
-
-value "(dijkstra o G.from_list) [(1,2::nat,7),(1,3,1),(3,2,2)] 1"
-
+export_code dijkstra_list in SML
+
value "dijkstra_list [(1::nat,2,7),(1,3,1),(3,2,2)] 1"
+value "dijkstra_list [(1::nat,2,7),(1,3,1),(3,2,2)] 3"

end```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Thys/Weighted_Graph_Specs.thy	Mon Jul 09 11:56:29 2018 +0200
@@ -0,0 +1,319 @@
+section \<open>Weighted Graphs\<close>
+theory Weighted_Graph_Specs
+imports
+  "HOL-Data_Structures.Map_Specs"
+  "HOL-Library.Extended_Nat"
+begin
+
+(*<*)
+lemma least_antimono: "X\<noteq>{} \<Longrightarrow> X\<subseteq>Y \<Longrightarrow> (LEAST y::_::wellorder. y\<in>Y) \<le> (LEAST x. x\<in>X)"
+  by (metis LeastI_ex Least_le equals0I rev_subsetD)
+
+fun the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
+  "the_default d None = d"
+| "the_default _ (Some x) = x"
+
+lemma prod_case_const[simp]: "case_prod (\<lambda>_ _. c) = (\<lambda>_. c)" by auto
+
+
+(*>*)
+
+
+text \<open>
+  A weighted graph is represented by a function from edges to weights.
+
+  For simplicity, we use @{typ enat} as weights, @{term \<open>\<infinity>\<close>} meaning
+  that there is no edge.
+\<close>
+
+type_synonym ('v) wgraph = "('v \<times> 'v) \<Rightarrow> enat"
+
+text \<open>We encapsulate weighted graphs into a locale that fixes a graph\<close>
+locale WGraph = fixes w :: "'v wgraph"
+begin
+  text \<open>Set of edges with finite weight\<close>
+  definition "edges \<equiv> {(u,v) . w (u,v) \<noteq> \<infinity>}"
+
+  subsection \<open>Paths\<close>
+  text \<open>A path between nodes \<open>u\<close> and \<open>v\<close> is a list of edge weights
+    of a sequence of edges from \<open>u\<close> to \<open>v\<close>.
+
+    Note that a path may also contain edges with weight \<open>\<infinity>\<close>.
+  \<close>
+
+  fun path :: "'v \<Rightarrow> enat list \<Rightarrow> 'v \<Rightarrow> bool" where
+    "path u [] v \<longleftrightarrow> u=v"
+  | "path u (l#ls) v \<longleftrightarrow> (\<exists>uh. l = w (u,uh) \<and> path uh ls v)"
+
+  lemma path_append[simp]: "path u (ls1@ls2) v \<longleftrightarrow> (\<exists>w. path u ls1 w \<and> path w ls2 v)"
+    by (induction ls1 arbitrary: u) auto
+
+  text \<open>There is a singleton path between every two nodes (it's weight might be \<open>\<infinity>\<close>).\<close>
+  lemma triv_path: "path u [w (u,v)] v" by auto
+
+  text \<open>Shortcut for the set of all paths between two nodes\<close>
+  definition "paths u v \<equiv> {p . path u p v}"
+
+  lemma paths_ne: "paths u v \<noteq> {}" using triv_path unfolding paths_def by blast
+
+  text \<open>If there is a path from a node inside a set \<open>S\<close>, to a node outside a set \<open>S\<close>,
+    this path must contain an edge from inside \<open>S\<close> to outside \<open>S\<close>.
+  \<close>
+  lemma find_leave_edgeE:
+    assumes "path u p v"
+    assumes "u\<in>S" "v\<notin>S"
+    obtains p1 x y p2 where "p = p1@w (x,y)#p2" "x\<in>S" "y\<notin>S" "path u p1 x" "path y p2 v"
+  proof -
+    have "\<exists> p1 x y p2. p = p1@w (x,y)#p2 \<and> x\<in>S \<and> y\<notin>S \<and> path u p1 x \<and> path y p2 v"
+      using assms
+    proof (induction p arbitrary: u)
+      case Nil
+      then show ?case by auto
+    next
+      case (Cons a p)
+      from Cons.prems obtain x where [simp]: "a=w (u,x)" and PX: "path x p v" by auto
+
+      show ?case proof (cases "x\<in>S")
+        case False with PX \<open>u\<in>S\<close> show ?thesis by fastforce
+      next
+        case True from Cons.IH[OF PX True \<open>v\<notin>S\<close>] show ?thesis
+          by clarsimp (metis WGraph.path.simps(2) append_Cons)
+      qed
+    qed
+    thus ?thesis by (fast intro: that)
+  qed
+
+  subsection \<open>Distance\<close>
+
+  text \<open>The (minimum) distance between two nodes \<open>u\<close> and \<open>v\<close> is called \<open>\<delta> u v\<close>.\<close>
+
+  definition "\<delta> u v \<equiv> LEAST w::enat. w\<in>sum_list`paths u v"
+
+  lemma obtain_shortest_path:
+    obtains p where "path s p u" "\<delta> s u = sum_list p"
+    unfolding \<delta>_def using paths_ne
+    by (smt Collect_empty_eq LeastI_ex WGraph.paths_def imageI image_iff mem_Collect_eq paths_def)
+
+  lemma shortest_path_least:
+    "path s p u \<Longrightarrow> \<delta> s u \<le> sum_list p"
+    unfolding \<delta>_def paths_def
+
+  lemma distance_refl[simp]: "\<delta> s s = 0"
+    using shortest_path_least[of s "[]" s] by auto
+
+  lemma distance_direct: "\<delta> s u \<le> w (s, u)"
+    using shortest_path_least[of s "[w (s,u)]" u] by auto
+
+  text \<open>Triangle inequality: The distance from \<open>s\<close> to \<open>v\<close> is shorter than
+    the distance from \<open>s\<close> to \<open>u\<close> and the edge weight from \<open>u\<close> to \<open>v\<close>. \<close>
+  lemma triangle: "\<delta> s v \<le> \<delta> s u + w (u,v)"
+  proof -
+    have "path s (p@[w (u,v)]) v" if "path s p u" for p using that by auto
+    then have "(+) (w (u,v)) ` sum_list ` paths s u \<subseteq> sum_list ` paths s v"
+      by (fastforce simp: paths_def image_iff simp del: path.simps path_append)
+    from least_antimono[OF _ this] paths_ne have
+      "(LEAST y::enat. y \<in> sum_list ` paths s v) \<le> (LEAST x::enat. x \<in> (+) (w (u,v)) ` sum_list ` paths s u)"
+      by (auto simp: paths_def)
+    also have "\<dots> = (LEAST x. x \<in> sum_list ` paths s u) + w (u,v)"
+      apply (subst Least_mono[of "(+) (w (u,v))" "sum_list`paths s u"])
+      apply (auto simp: mono_def)
+      by (metis WGraph.paths_def mem_Collect_eq obtain_shortest_path shortest_path_least)
+    finally show ?thesis unfolding \<delta>_def .
+  qed
+
+  text \<open>Any prefix of a shortest path is a shortest path itself.\<close>
+  (* TODO: Do we need the < \<infinity> ? *)
+  lemma shortest_path_prefix:
+    assumes "path s p\<^sub>1 x" "path x p\<^sub>2 u"
+    and DSU: "\<delta> s u = sum_list p\<^sub>1 + sum_list p\<^sub>2" "\<delta> s u < \<infinity>"
+    shows "\<delta> s x = sum_list p\<^sub>1" "\<delta> s x < \<infinity>"
+  proof -
+    have "\<delta> s x \<le> sum_list p\<^sub>1" using assms shortest_path_least by blast
+    moreover have "\<not>\<delta> s x < sum_list p\<^sub>1" proof
+      assume "\<delta> s x < sum_list p\<^sub>1"
+      then obtain p\<^sub>1' where "path s p\<^sub>1' x" "sum_list p\<^sub>1' < sum_list p\<^sub>1"
+        by (auto intro: obtain_shortest_path[of s x])
+      with \<open>path x p\<^sub>2 u\<close> shortest_path_least[of s "p\<^sub>1'@p\<^sub>2" u] DSU show False
+        by fastforce
+    qed
+    ultimately show "\<delta> s x = sum_list p\<^sub>1" by auto
+    with DSU show "\<delta> s x < \<infinity>" using le_iff_add by fastforce
+  qed
+
+
+end
+
+
+subsection \<open>Abstract Data Type\<close>
+
+  fixes \<alpha> :: "'g \<Rightarrow> ('v) wgraph"
+    and invar :: "'g \<Rightarrow> bool"
+    and succ :: "'g \<Rightarrow> 'v \<Rightarrow> (nat\<times>'v) list"
+    and empty_graph :: 'g
+    and add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'g \<Rightarrow> 'g"
+  assumes succ_correct: "invar g \<Longrightarrow> set (succ g u) = {(d,v). \<alpha> g (u,v) = enat d}"
+  assumes empty_graph_correct:
+    "invar empty_graph"
+    "\<alpha> empty_graph = (\<lambda>_. \<infinity>)"
+    "invar g \<Longrightarrow> \<alpha> g e = \<infinity> \<Longrightarrow> invar (add_edge e d g)"
+    "invar g \<Longrightarrow> \<alpha> g e = \<infinity> \<Longrightarrow> \<alpha> (add_edge e d g) = (\<alpha> g)(e:=enat d)"
+begin
+
+
+  lemmas wgraph_specs = succ_correct empty_graph_correct add_edge_correct
+
+end
+
+locale adt_finite_wgraph = adt_wgraph where \<alpha>=\<alpha> for \<alpha> :: "'g \<Rightarrow> ('v) wgraph" +
+  assumes finite: "invar g \<Longrightarrow> finite (WGraph.edges (\<alpha> g))"
+
+
+subsection \<open>Constructing Weighted Graphs from Lists\<close>
+lemma edges_empty[simp]: "WGraph.edges (\<lambda>_. \<infinity>) = {}" by (auto simp: WGraph.edges_def)
+lemma edges_insert[simp]: "WGraph.edges (g(e:=enat d)) = Set.insert e (WGraph.edges g)" by (auto simp: WGraph.edges_def)
+
+text \<open>A list represents a graph if there are no multi-edges or duplicate edges\<close>
+definition "valid_graph_rep l \<equiv>
+  (\<forall>u d d' v. (u,v,d)\<in>set l \<and> (u,v,d')\<in>set l \<longrightarrow> d=d')
+\<and> distinct l
+  "
+
+text \<open>Alternative characterization: all node pairs must be distinct\<close>
+lemma valid_graph_rep_code[code]: "valid_graph_rep l \<longleftrightarrow> distinct (map (\<lambda>(u,v,_). (u,v)) l)"
+  by (auto simp: valid_graph_rep_def distinct_map inj_on_def)
+
+lemma valid_graph_rep_simps[simp]:
+  "valid_graph_rep []"
+  "valid_graph_rep ((u,v,d) # l) \<longleftrightarrow> valid_graph_rep l \<and> (\<forall>d'. (u,v,d')\<notin>set l)"
+  by (auto simp: valid_graph_rep_def)
+
+
+text \<open>For a valid graph representation, there is exactly one graph that corresponds to it\<close>
+lemma valid_graph_rep_ex1: "valid_graph_rep l \<Longrightarrow> \<exists>! w. \<forall>u v d. w (u,v) = enat d \<longleftrightarrow> (u,v,d)\<in>set l"
+  unfolding valid_graph_rep_code
+  apply (auto)
+  subgoal
+    apply (rule exI[where x="\<lambda>(u,v). if \<exists>d. (u,v,d)\<in>set l then enat (SOME d. (u,v,d)\<in>set l) else \<infinity>"])
+    apply (auto intro: someI simp: distinct_map inj_on_def split: prod.splits; blast)
+    done
+  subgoal for w w'
+    apply (auto del: ext intro!: ext)
+    by (metis (mono_tags, hide_lams) not_enat_eq)
+  done
+
+text \<open>We define this graph using determinate choice\<close>
+definition "wgraph_of_list l \<equiv> THE w. \<forall>u v d. w (u,v) = enat d \<longleftrightarrow> (u,v,d)\<in>set l"
+
+begin
+
+  definition "from_list l \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l empty_graph"
+
+  definition "edges_undef l w \<equiv> \<forall>u v d. (u,v,d)\<in>set l \<longrightarrow> w (u,v) = \<infinity>"
+
+  lemma edges_undef_simps[simp]:
+    "edges_undef [] w"
+    "edges_undef l (\<lambda>_. \<infinity>)"
+    "edges_undef ((u,v,d)#l) w \<longleftrightarrow> edges_undef l w \<and> w (u,v) = \<infinity>"
+    "edges_undef l (w((u,v) := enat d)) \<longleftrightarrow> edges_undef l w \<and> (\<forall>d'. (u,v,d')\<notin>set l)"
+    by (auto simp: edges_undef_def)
+
+  lemma from_list_correct_aux:
+    assumes "valid_graph_rep l"
+    assumes "edges_undef l (\<alpha> g)"
+    assumes "invar g"
+    defines "g' \<equiv> fold (\<lambda>(u,v,d). add_edge (u,v) d) l g"
+    shows "invar g'" "(\<forall>u v d. \<alpha> g' (u,v) = enat d \<longleftrightarrow> \<alpha> g (u,v) = enat d \<or> (u,v,d)\<in>set l)"
+    using assms(1-3) unfolding g'_def
+    apply (induction l arbitrary: g)
+    apply (auto simp: wgraph_specs split: if_splits)
+    done
+
+  lemma from_list_correct':
+    assumes "valid_graph_rep l"
+    shows "invar (from_list l)" "(u,v,d)\<in>set l \<longleftrightarrow> \<alpha> (from_list l) (u,v) = enat d"
+    unfolding from_list_def using from_list_correct_aux[OF assms, where g=empty_graph]
+    by (auto simp: wgraph_specs)
+
+  lemma from_list_correct:
+    assumes "valid_graph_rep l"
+    shows "invar (from_list l)" "\<alpha> (from_list l) = wgraph_of_list l"
+  proof -
+    from theI'[OF valid_graph_rep_ex1[OF assms], folded wgraph_of_list_def]
+    have "(wgraph_of_list l (u, v) = enat d) = ((u, v, d) \<in> set l)" for u v d
+      by blast
+
+    then show "\<alpha> (from_list l) = wgraph_of_list l" and "invar (from_list l)"
+      using from_list_correct_aux[OF assms, where g=empty_graph]
+      apply (auto simp: wgraph_specs from_list_def del: ext intro!: ext)
+      by (metis (no_types) enat.exhaust)
+  qed
+
+end
+
+subsection \<open>Implementing Weighted Graphs by Adjacency Map\<close>
+(*<*)
+lemma distinct_map_snd_inj: "distinct (map snd l) \<Longrightarrow> (a,b)\<in>set l \<Longrightarrow> (a',b)\<in>set l \<Longrightarrow> a=a'"
+  by (metis distinct_map inj_onD prod.sel(2) prod.simps(1))
+(*>*)
+
+locale wgraph_by_map =
+  M: Map M_empty M_update M_delete M_lookup M_invar
+
+  for M_empty M_update M_delete and M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> ((nat\<times>'v) list) option" and M_invar
+begin
+  definition \<alpha> :: "'m \<Rightarrow> ('v) wgraph" where
+    "\<alpha> g \<equiv> \<lambda>(u,v). case M_lookup g u of
+      None \<Rightarrow> \<infinity>
+    | Some l \<Rightarrow> if \<exists>d. (d,v)\<in>set l then enat (SOME d. (d,v)\<in>set l) else \<infinity>"
+
+  definition invar :: "'m \<Rightarrow> bool" where
+    "invar g \<equiv> M_invar g \<and> (\<forall>l\<in>ran (M_lookup g). distinct (map snd l)) \<and> finite (WGraph.edges (\<alpha> g))"
+
+  definition succ :: "'m \<Rightarrow> 'v \<Rightarrow> (nat \<times> 'v) list" where
+    "succ g v = the_default [] (M_lookup g v)"
+
+  definition empty_graph :: "'m" where "empty_graph = M_empty"
+
+  definition add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'm \<Rightarrow> 'm" where
+    "add_edge \<equiv> \<lambda>(u,v) d g. M_update u ((d,v) # the_default [] (M_lookup g u)) g"
+
+    apply unfold_locales
+    subgoal for g u
+      apply (cases "M_lookup g u")
+      apply (auto
+        simp: invar_def \<alpha>_def succ_def ran_def
+        intro: distinct_map_snd_inj someI
+        split: option.splits
+      )
+      done
+    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
+    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
+  proof -
+    (* Explicit proof to nicely handle finiteness constraint, using already proved shape of abstract result *)
+    fix g e d
+    assume A: "invar g" "\<alpha> g e = \<infinity>"
+    then show AAE: "\<alpha> (add_edge e d g) = (\<alpha> g)(e := enat d)"
+      by (auto
+        simp: invar_def \<alpha>_def add_edge_def M.map_specs
+        split: option.splits if_splits prod.splits
+      )
+
+    from A show "invar (add_edge e d g)"
+      apply (simp add: invar_def AAE)
+      by (force
+        simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs ran_def
+        split: option.splits if_splits prod.splits)