Dijkstra cleaned up draft
authorlammich <lammich@in.tum.de>
Mon, 09 Jul 2018 11:56:29 +0200
changeset 69946 ed7c67f266ac
parent 69945 c772b78fd6cd
child 69947 cd8eb35f3c38
Dijkstra cleaned up
Thys/Dijkstra.thy
Thys/Weighted_Graph_Specs.thy
--- 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)"
   by (auto simp: map_add_def)
 
-
-  
-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
-    by (simp add: Least_le)
+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)
-    by (metis add.commute enat_add_left_cancel_less less_le_trans not_less triangle)
-
-  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)
-    by (metis triangle add.commute add_mono_thms_linordered_semiring(2) dual_order.trans)
-
-  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)
+    apply (simp add: relax_outgoing_def)  
+    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"
-    by (auto simp: relax_adjs_def)
     
-  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"
-    by (auto simp: relax_adjs_def)
-    
-    
-  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
+        apply (simp add: relax_finished_id)
         by (auto 
-          simp: relax_adjs'_def map_add_apply \<alpha> decrease_point_def min_def
+          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_adjs_def relax_adjs'_def map_add_apply \<alpha> decrease_point_def min_def
+          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_adjs_def initQ_def map_add_apply enat_0 
+      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
     by (fastforce simp add: coupling_def)
 
-
-  (* 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>  
 
-  lemma relax_adjs''_refine:
+  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_adjs''_def relax_adjs'_def decrease_key_def decrease_point_def image_iff
+        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>}"
-
-locale adt_wgraph =
-  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>)"
-  assumes add_edge_correct:
-    "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))"
+subsection \<open>Implementation using ADT Interfaces\<close>
 
 locale Dijkstra_Impl_Adts = 
   G: adt_finite_wgraph G_invar G_succ G_empty G_add G_\<alpha>
 + 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
   
-  lemma Q_relax_adjs1[simp]:
-    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)
-    apply (simp add: Q_relax_adjs1_def relax_adjs''_def)
-    apply (clarsimp simp: Q_relax_adjs1_def relax_adjs''_def; safe; simp)
-    done
-
-  definition (in Dijkstra_Impl_Defs) "Q_relax_adjs u du V Q \<equiv> Q_relax_adjs1 (G_succ g u) du V Q"   
-  
-  lemma Q_relax_adjs[simp]:
+  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)"
-    apply (simp add: Q_relax_adjs_def)
-    apply (rule relax_adjs''_refine)
-    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 (simp add: D_invar'_def)
       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"
-  
-  sublocale adt_finite_wgraph invar succ empty_graph add_edge \<alpha>
-    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)      
-  qed (simp add: invar_def)     
-
-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_add_edge = G.add_edge
       and G_succ = G.succ
   by unfold_locales
-print_theorems
-
-export_code G_empty G_succ G_add_edge in SML
-
-
 
 global_interpretation Dijkstra_Impl_Adts
   G.\<alpha> G.invar G.succ G.empty_graph G.add_edge
@@ -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_adjs = D.Q_relax_adjs
-      and Q_relax_adjs1 = D.Q_relax_adjs1
+      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>"  
-    
-  
-locale wgraph_from_list_algo = adt_wgraph 
-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
+    by (simp add: Least_le)
+
+  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>
+
+locale adt_wgraph =
+  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>)"
+  assumes add_edge_correct:
+    "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"  
+
+locale wgraph_from_list_algo = adt_wgraph 
+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"
+  
+  sublocale adt_finite_wgraph invar succ empty_graph add_edge \<alpha>
+    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)      
+  qed (simp add: invar_def)     
+
+end  
+
+
+
+  
+  
+end