Dijkstra, up to PrioMap-Locale draft
authorlammich <lammich@in.tum.de>
Wed, 04 Jul 2018 19:00:02 +0200
changeset 69942 3c344ec103ae
parent 69941 af2719b74080
child 69943 d5860fb818f1
Dijkstra, up to PrioMap-Locale
Thys/Dijkstra.thy
Thys/Prio_Map_Specs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Thys/Dijkstra.thy	Wed Jul 04 19:00:02 2018 +0200
@@ -0,0 +1,703 @@
+theory Dijkstra
+imports Main "HOL-Library.Extended_Nat" "HOL-Eisbach.Eisbach"
+  Prio_Map_Specs "HOL-Library.While_Combinator"
+begin
+
+hide_const (open) connected
+
+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)
+
+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)
+
+  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
+
+  
+  
+
+locale Dijkstra = WGraph w for w :: "('v,enat) wgraph" +
+  fixes s :: 'v
+begin
+  
+  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)
+
+    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    
+  
+    
+  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) (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> insert u S" unfolding D_invar_def by simp
+  next
+    fix v 
+    assume "v\<in>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>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 
+  
+  
+  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)
+  
+  lemma unfinished_nodes_decr:
+    assumes I: "D_invar D S"
+    assumes UNS: "u\<notin>S"
+    assumes UNI: "D u < \<infinity>"
+    shows "unfinished_dnodes (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)
+  
+    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)
+    
+    text \<open>Thus, \<open>u\<close> must have incoming edge\<close>
+    have "u\<in>all_dnodes" 
+    proof -
+      obtain p where "path s p u" "sum_list p < \<infinity>"
+        apply (rule obtain_shortest_path[of s u])
+        using \<open>\<delta> s u < \<infinity>\<close> by auto
+      with \<open>s\<in>S\<close> \<open>u\<notin>S\<close> show ?thesis 
+        apply (cases p rule: rev_cases) 
+        apply (auto simp: all_dnodes_def)
+        using not_infinity_eq by fastforce
+    qed
+    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 *)
+
+
+lemma Abs_enat_inj[simp]: "Abs_enat x = Abs_enat y \<longleftrightarrow> x=y"
+  by (metis Abs_enat_inverse UNIV_I)
+
+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
+  
+lemma Abs_enat_le_conv: "Abs_enat m \<le> Abs_enat n \<longleftrightarrow> (case (m,n) of 
+    (_,None) \<Rightarrow> True
+  | (Some a, Some b) \<Rightarrow> a\<le>b
+  | (_, _) \<Rightarrow> False
+)"
+  by (auto split: option.split)
+
+
+
+
+context Dijkstra begin
+  definition "coupling Q V D S \<equiv> 
+    D = Abs_enat o (V ++ Q)
+  \<and> S = dom V
+  \<and> dom V \<inter> dom Q = {}"
+
+
+  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  
+  "
+  
+  
+  lemma coupling_step:
+    assumes I: "D_invar D S"
+    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) (insert u S)"
+      and "Q u = Some du" "V u = None"
+    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" 
+       and DD: "dom V \<inter> dom Q = {}"
+     
+    show "insert u S = dom (V(u \<mapsto> du))"   
+      by (auto simp: \<alpha>)
+       
+    show [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)
+    
+    fix v
+    
+    show "relax_adjs u D v = (Abs_enat \<circ> V(u \<mapsto> du) ++ (relax_adjs' 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])
+        by (auto 
+          simp: relax_adjs'_def map_add_apply \<alpha> decrease_point_def 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
+          split: option.splits enat.splits)
+    qed
+  qed    
+    
+  definition "initQ v \<equiv> if s=v then None else case w (s,v) of \<infinity> \<Rightarrow> None | enat d \<Rightarrow> Some d"
+    
+  lemma coupling_init:
+    "coupling initQ [s\<mapsto>0] (relax_adjs s ((\<lambda>_. \<infinity>)(s:=0))) {s}"    
+    unfolding coupling_def
+    by (auto 
+      simp: coupling_def relax_adjs_def initQ_def map_add_apply enat_0 
+      split: option.split enat.split
+      del: ext intro!: ext)
+    
+  lemma coupling_cond:
+    assumes "coupling Q V D S"
+    shows "(Q = Map.empty) \<longleftrightarrow> (\<forall>u. u\<notin>S \<longrightarrow> D u = \<infinity>)"
+    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')"
+  
+  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"
+
+  lemma relax_adjs''_refine:
+    assumes "set l = {(d,v). w (u,v) = enat d}"  
+    shows "relax_adjs'' l du V Q = relax_adjs' 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)"
+    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
+        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)
+    
+    show "relax_adjs'' l du V Q v = relax_adjs' u du V Q v"
+      using aux1
+      apply (cases "w (u,v)")
+      by (all \<open>force simp: aux2 assms\<close>)
+  qed
+    
+  
+  definition "initQ' l \<equiv> fold (\<lambda>(d,v) Q. if s=v then Q else Q(v\<mapsto>d)) l Map.empty"
+
+  lemma initQ'_refine: 
+    assumes "set l = {(d,v). w (s,v) = enat d}"  
+    shows "initQ' l = initQ"
+  proof -
+    have aux1: "fold (\<lambda>(d,v) Q. if s=v then Q else Q(v\<mapsto>d)) l Q v = (
+      if s\<noteq>v \<and> v\<in>snd`set l then case w(s,v) of \<infinity> \<Rightarrow> Q v | enat d \<Rightarrow> Some d
+      else Q v)" 
+    if "set l \<subseteq> {(d,v). w (s,v) = enat d}"
+    for Q v
+      using that
+      apply (induction l arbitrary: Q)
+      apply (auto split!: enat.splits)
+      done
+      
+    show ?thesis proof
+      fix v
+      
+      have "initQ' l v = (if s\<noteq>v \<and> v\<in>snd`set l then case w(s,v) of \<infinity> \<Rightarrow> Map.empty v | enat d \<Rightarrow> Some d
+        else Map.empty v)"
+        using aux1[of Map.empty v]
+        by (simp add: assms initQ'_def)
+      also have "\<dots> = initQ v"  
+        by (auto simp: initQ_def assms image_iff split: enat.split)
+      finally show "initQ' l v = initQ v" .
+    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
+  
+
+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 v) = {(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> invar (add_edge e d g)"
+    "invar g \<Longrightarrow> \<alpha> (add_edge e d g) = (\<alpha> g)(e:=enat d)"
+begin
+
+  definition "edges g \<equiv> {(u,v) . (\<alpha> g) (u,v) \<noteq> \<infinity>}"
+  
+  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: "finite (edges g)"
+
+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
+  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
+  (* Simplifier setup *)
+  lemmas [simp] = G.wgraph_specs
+  lemmas [simp] = M.map_specs
+  lemmas [simp] = Q.prio_map_specs
+end  
+  
+
+context PrioMap begin
+
+  lemma map_getminE:
+    assumes "getmin m = (k,p)" "invar m" "lookup m \<noteq> Map.empty" 
+    obtains "lookup m k = Some p" "\<forall>k' p'. lookup m k' = Some p' \<longrightarrow> p\<le>p'"  
+    using map_getmin[OF assms]
+    by (auto simp: ran_def)
+    
+
+
+end
+
+locale Dijkstra_Impl = Dijkstra_Impl_Adts where G_\<alpha> = G_\<alpha>  
+  + Dijkstra \<open>G_\<alpha> g\<close> s
+  for G_\<alpha> :: "'g \<Rightarrow> ('v,enat) wgraph" and g s 
+  +
+  assumes G_invar[simp]: "G_invar g"
+begin  
+  lemma finite_all_dnodes[simp, intro!]: "finite all_dnodes"
+  proof -  
+    have "all_dnodes \<subseteq> snd ` G.edges g"
+      by (fastforce simp: all_dnodes_def G.edges_def image_iff)
+    also have "finite \<dots>" by (auto simp: G.finite)
+    finally (finite_subset) show ?thesis .
+  qed
+
+  lemma finite_unfinished_dnodes[simp, intro!]: "finite (unfinished_dnodes S)"
+    using finite_subset[OF unfinished_nodes_subset] by auto
+    
+
+  definition "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)  
+    
+  definition "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 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 "Q_relax_adjs u du V Q \<equiv> Q_relax_adjs1 (G_succ g u) du V Q"   
+  
+  lemma Q_relax_adjs[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
+    
+  definition "D_invar_impl Q V \<equiv> 
+    Q_invar Q \<and> M_invar V \<and> D_invar' (Q_lookup Q) (M_lookup V)"
+
+  definition "Q_initQ \<equiv> fold (\<lambda>(d,v) Q. if s=v then Q else Q_update v d Q) (G_succ g s) Q_empty"
+    
+            
+  lemma Q_init_Q[simp]:
+    shows "Q_invar Q_initQ" "Q_lookup Q_initQ = initQ"
+  proof -
+    let ?QiQ = "fold (\<lambda>(d,v) Q. if s=v then Q else Q_update v d Q)"
+    let ?iQ' = "fold (\<lambda>(d,v) Q. if s=v then Q else Q(v\<mapsto>d))"
+  
+    have aux: "Q_invar (?QiQ l Q) \<and> Q_lookup (?QiQ l Q) = ?iQ' l (Q_lookup Q)"
+      if "Q_invar Q"
+      for l Q
+      using that apply (induction l arbitrary: Q) apply simp
+      apply clarsimp
+      done
+      
+    from aux show "Q_invar Q_initQ" unfolding Q_initQ_def by auto
+      
+    from aux have "Q_lookup Q_initQ = initQ' (G_succ g s)"    
+      unfolding Q_initQ_def initQ'_def by auto
+    also have "\<dots> = initQ" by (rule initQ'_refine) auto
+    finally show "Q_lookup Q_initQ = initQ" .
+  qed
+  
+  
+  term Q_getmin
+  
+  definition "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_delete u Q;
+      V = M_update u du V
+    in
+      (Q,V)
+  ) (Q_initQ,M_update s 0 M_empty)"
+  
+  definition "dijkstra \<equiv> snd dijkstra_loop"
+  
+  lemma transfer_preconditions:
+    assumes "coupling Q V D S"
+    shows "Q u = Some du \<longleftrightarrow> D u = enat du \<and> u\<notin>S"
+    using assms
+    by (auto simp: coupling_def)
+  
+  
+  lemma dijkstra_loop_invar_and_empty:
+    shows "case dijkstra_loop of (Q,V) \<Rightarrow> D_invar_impl Q V \<and> Q_is_empty Q"
+    unfolding dijkstra_loop_def
+    apply (rule while_rule[where 
+          P="case_prod D_invar_impl" 
+      and r="inv_image finite_psubset (unfinished_dnodes' o M_lookup o snd)"])
+    apply (all \<open>(clarsimp split: prod.splits)?\<close>)
+    subgoal
+      apply (simp add: D_invar_impl_def)
+      apply (simp add: D_invar'_def)
+      apply (intro exI conjI)
+      apply (rule coupling_init)
+      apply (rule D_invar_init)
+      done
+  proof -  
+    fix Q V u du
+    assume "\<not> Q_is_empty Q" "D_invar_impl Q V" "Q_getmin Q = (u, du)"
+    hence "Q_lookup Q \<noteq> Map.empty" "D_invar' (Q_lookup Q) (M_lookup V)"
+      and [simp]: "Q_invar Q" "M_invar V"
+      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"  
+      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) 
+      
+    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) (insert u S)"  
+      using coupling_step(1)[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
+      using coupling_step(1)[OF COUPLING \<open>u\<notin>S\<close> \<open>D u = enat du\<close>, simplified]
+      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
+      by simp
+  qed  
+    
+  lemma dijkstra_correct: "M_invar dijkstra" "M_lookup dijkstra u = Some d \<longleftrightarrow> \<delta> s u = enat d"
+    using dijkstra_loop_invar_and_empty
+    unfolding dijkstra_def
+    apply -
+    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]
+      apply (clarsimp simp: coupling_def)
+      by (auto simp: domIff)
+    done
+  
+    
+end       
+
+end
--- a/Thys/Prio_Map_Specs.thy	Tue Jul 03 16:50:01 2018 +0200
+++ b/Thys/Prio_Map_Specs.thy	Wed Jul 04 19:00:02 2018 +0200
@@ -21,8 +21,14 @@
 fixes is_empty :: "'m \<Rightarrow> bool"
 fixes getmin :: "'m \<Rightarrow> 'a \<times> 'b"
 assumes map_is_empty: "invar m \<Longrightarrow> is_empty m \<longleftrightarrow> lookup m = Map.empty"
-and map_getmin: "invar m \<Longrightarrow> lookup m \<noteq> Map.empty \<Longrightarrow> getmin m = (k,p) \<Longrightarrow> lookup m k = Some p \<and> p=Min (ran (lookup m))"
+and map_getmin: "getmin m = (k,p) \<Longrightarrow> invar m \<Longrightarrow> lookup m \<noteq> Map.empty 
+  \<Longrightarrow> lookup m k = Some p \<and> (\<forall>p'\<in>ran (lookup m). p\<le>p')"
+begin
 
+  lemmas prio_map_specs = map_specs map_is_empty 
+
+
+end
 
 definition is_min2 :: "(_\<times>'a::linorder) \<Rightarrow> (_\<times>'a) set \<Rightarrow> bool"
   where "is_min2 x xs \<equiv> x\<in>xs \<and> (\<forall>y\<in>xs. snd x \<le> snd y)"