Prim draft
authornipkow
Mon, 21 Jan 2019 16:00:30 +0100
changeset 69956 821d9a48fbd2
parent 69955 db5ebc272bcf
child 69957 c6741e49d33b
Prim
Thys/Prim.thy
Thys/Weighted_UGraph_Specs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Thys/Prim.thy	Mon Jan 21 16:00:30 2019 +0100
@@ -0,0 +1,639 @@
+section \<open>Prim's Algorithm\<close>
+theory Prim
+imports 
+  Main 
+  "Weighted_UGraph_Specs"
+  "HOL-Eisbach.Eisbach"
+  Prio_Map_Specs 
+  "HOL-Library.While_Combinator"
+  RBT_Heap
+  "HOL-Data_Structures.RBT_Map"
+begin
+
+declare [[coercion_enabled = false]]
+
+
+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)
+
+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)
+
+  
+
+  
+subsection \<open>Abstract Prim Algorithm\<close>  
+
+type_synonym 'v estimate = "'v \<Rightarrow> enat"
+
+
+context WGraph begin
+  (* TODO: Move *)
+
+  lemma edges_01[simp]: "{}\<notin>edges" "{u}\<notin>edges" unfolding edges_def by (auto intro!: w_card2)
+
+end
+
+text \<open>We fix a start node and a weighted graph\<close>
+locale Prim = WGraph w for w :: "('v) wgraph" +
+  fixes r :: 'v
+begin
+
+  text \<open>Initialization\<close>
+  definition initQ :: "'v \<Rightarrow> enat"  where "initQ \<equiv> (\<lambda>_. \<infinity>)(r := 0)"
+  definition init\<pi> :: "'v \<Rightarrow> 'v option" where "init\<pi> \<equiv> Map.empty"  
+  definition initV :: "'v set" where "initV \<equiv> {}"
+
+
+  text \<open>Next loop step\<close>  
+
+  (* After inner loop *)
+  definition "Q' Q V u v = (if {u,v} \<in> edges \<and> v \<notin> V \<and> w {u,v} < Q v then w {u,v} else Q v)"
+  definition "\<pi>' Q \<pi> V u v = (if {u,v} \<in> edges \<and> v \<notin> V \<and> w {u,v} < Q v then Some u else \<pi> v)"
+
+  (* At end of loop iteration *)
+  definition "nextQ Q V u \<equiv> (Q' Q V u)(u:=\<infinity>)"
+  definition "next\<pi> Q \<pi> V u \<equiv> (\<pi>' Q \<pi> V u)"
+  definition "nextV V u \<equiv> Set.insert u V"
+
+
+  text \<open>Abstraction of state\<close>  
+  definition "A \<pi> V = { {v,u} |v u. v \<in> V \<and> \<pi> v = Some u}"
+
+
+end
+
+context WGraph
+begin
+
+definition is_MST :: "'v set set \<Rightarrow> bool" where "is_MST = undefined"
+
+lemma ex_MST: "\<exists>T. is_MST T" sorry
+
+
+definition "is_subset_MST A = (\<exists>T. is_MST T \<and> A \<subseteq> T)"
+
+lemma is_subset_MST_empty: "is_subset_MST {}"
+  unfolding is_subset_MST_def using ex_MST by blast
+
+
+lemma light_edge_is_safe: (* Can we get this from Kruskal's formalization? *)
+  fixes A :: "'v set set" and S :: "'v set"
+  assumes subset_MST: "is_subset_MST A"
+  assumes respects_cut: "\<forall>e\<in>A. e\<subseteq>S" (* Stricter than in Cormen l23.1*)
+  assumes crossing_edge: "u\<in>S" "v\<notin>S" "w {u,v} = enat d"
+  assumes light_edge: "\<forall>u'\<in>S. \<forall>v'\<in>-S. enat d \<le> w {u',v'}"
+  shows "is_subset_MST (Set.insert {u,v} A)"
+  sorry  
+
+
+
+end
+
+subsubsection \<open>Invariant\<close>
+text \<open>The invariant is defined as locale\<close>
+
+
+(*context Prim begin
+  sublocale S: PrimState w r Q \<pi> V for Q \<pi> V by unfold_locales
+end
+*)
+
+context Prim begin
+
+  definition "Q_alt V v \<equiv> if v\<in>V then \<infinity> else MIN u\<in>V. w {u,v}"
+
+end
+
+locale Prim_Invar = 
+  Prim w r for w and r :: 'v +
+  fixes Q :: "'v \<Rightarrow> enat" and \<pi> :: "'v \<Rightarrow> 'v option" and V :: "'v set"
+
+  assumes subset_MST: \<open>is_subset_MST (A \<pi> V)\<close> \<comment> \<open>\<open>A\<close> is a subtree of a MST\<close>
+  assumes r_inv: "\<pi> r = None"
+  assumes \<pi>_in_V: "\<pi> v = Some u \<Longrightarrow> u\<in>V"
+  assumes \<pi>_defined: "\<lbrakk>u\<in>V; v\<notin>V; w {u,v} = enat d\<rbrakk> \<Longrightarrow> \<exists>u'. \<pi> v = Some u' \<and> w {u',v} \<le> enat d"
+  assumes Q_alt: "(r\<in>V \<and> Q = Q_alt V) \<or> (r\<notin>V \<and> Q=initQ \<and> V=initV \<and> \<pi>=init\<pi>)"
+  assumes finiteV[simp,intro!]: "finite V" 
+begin
+
+  abbreviation (in Prim) "P_invar \<equiv> Prim_Invar w r"
+
+  text \<open>The invariant holds for the initial state\<close>  
+  theorem (in Prim) invar_init: "P_invar initQ init\<pi> initV"
+    apply unfold_locales
+    unfolding initQ_def init\<pi>_def initV_def
+    by (auto simp: ex_MST is_subset_MST_def A_def)
+
+  lemma Q_altE:
+    assumes UNS: "Q_alt V v = enat d" assumes NO_INIT: "r\<in>V"
+    obtains u where "w {u,v} = enat d" "u\<in>V" "v\<notin>V" "\<forall>u'\<in>V. enat d \<le> w {u',v}"
+    using assms apply (auto simp: Q_alt_def split: if_splits)
+    by (smt Min_in Min_le finiteV empty_iff finite_imageI image_iff)
+
+
+  abbreviation (input) "nextA u \<equiv> A (next\<pi> Q \<pi> V u) (nextV V u)"
+
+  (*sublocale "next": PrimState w r "(Q' u)(u:=\<infinity>)" "(\<pi>' u)" "(Set.insert u V)" for u::'v by unfold_locales*)
+  
+
+  text \<open>A step of Prim's algorithm maintains the invariant.\<close>    
+  theorem maintain_P_invar:
+    assumes UNS: "Q u = enat d"
+    assumes MIN: "\<forall>v. enat d \<le> Q v"
+    shows "P_invar ((Q' Q V u)(u:=\<infinity>)) (\<pi>' Q \<pi> V u) (Set.insert u V)"
+  proof -
+    show ?thesis proof (cases "r\<in>V")
+      assume [simp]: "r\<notin>V"
+
+      have INIT: "Q = initQ" "V=initV" "\<pi>=init\<pi>" using Q_alt UNS by auto
+      hence [simp]: "Q=(\<lambda>_. \<infinity>)(r:=0)" "V={}" "\<pi>=Map.empty" "u=r" using UNS by (simp_all add: initV_def initQ_def init\<pi>_def split: if_splits)
+
+      show ?thesis 
+        apply unfold_locales
+        
+        subgoal unfolding A_def \<pi>'_def Q'_def by (simp add: is_subset_MST_empty)
+        subgoal unfolding A_def \<pi>'_def Q'_def by (auto)
+        subgoal unfolding A_def \<pi>'_def Q'_def by (auto split: if_splits)
+        subgoal unfolding \<pi>'_def by (auto simp: edges_def)
+        subgoal unfolding Q_alt_def unfolding A_def \<pi>'_def Q'_def by (auto split: if_splits simp: edges_def fun_eq_iff)
+        subgoal by auto
+        done
+
+    next
+      assume "r\<in>V" 
+
+      hence Q: "Q=Q_alt V" and \<open>V\<noteq>{}\<close> using Q_alt by auto
+
+      from Q_altE[OF UNS[unfolded Q] \<open>r\<in>V\<close>] obtain u0' where d_local_min: "u0'\<in>V" "u\<notin>V" "w {u0',u} = enat d" "\<forall>u0'\<in>V. enat d \<le> w {u0',u}" by blast
+
+      from \<pi>_defined[OF d_local_min(1-3)] obtain u0 where 
+        \<pi>u: "\<pi> u = Some u0" and "w {u0,u} \<le> enat d" "u0\<in>V" using \<pi>_in_V by auto
+      with d_local_min(4) have "w {u0,u} = enat d" by auto
+      
+
+      have global_min: "enat d \<le> w {u',v'}" if "u'\<in>V" "v'\<notin>V" for u' v'
+        apply (cases "v'=u") 
+        subgoal using d_local_min that by auto
+        subgoal proof -
+          assume "v'\<noteq>u"
+          have "Q v' \<le> w {u',v'}" unfolding Q Q_alt_def using that by simp
+          with MIN show ?thesis using order_trans by auto
+        qed
+        done
+          
+      have nextA: "nextA u = Set.insert {u0,u} (A \<pi> V)"
+        unfolding A_def \<pi>'_def nextV_def next\<pi>_def
+        by (fastforce simp: \<pi>u intro: exI[where x=u])
+
+      have AssV: "\<forall>e\<in>A \<pi> V. e \<subseteq> V" unfolding A_def using \<pi>_in_V by auto
+
+      { fix v d'
+        assume "w {u, v} = enat d'" "v \<noteq> u" "v \<notin> V" "\<not> enat d' < Q v"
+
+        then obtain dd where "Q_alt V v = enat dd" "dd\<le>d'" unfolding Q by (cases "Q_alt V v") auto
+        from Q_altE[OF this(1) \<open>r\<in>V\<close>] this(2) have "\<exists>u'. \<pi> v = Some u' \<and> w {u', v} \<le> enat d'"
+          by (smt \<pi>_defined dual_order.trans enat_ord_simps(2) leD not_le_imp_less)
+      } note aux1=this
+
+      { fix u' v d' d''
+        assume "w {u', v} = enat d'" "v \<noteq> u" "v \<notin> V" "u' \<in> V" "enat d'' < Q v" "w {u, v} = enat d''"
+        have "Q v \<le> enat d'" unfolding Q
+          by (metis (mono_tags, lifting) Min_le Q_alt_def \<open>u' \<in> V\<close> \<open>v \<notin> V\<close> \<open>w {u', v} = enat d'\<close> finiteV finite_imageI image_eqI)
+
+        hence "d'' \<le> d'" using \<open>enat d'' < Q v\<close>
+          by (meson order.order_iff_strict enat_ord_simps(2) less_le_trans)
+      } note aux2=this
+
+      show ?thesis
+        apply unfold_locales
+        subgoal thm nextA[unfolded next\<pi>_def nextV_def]
+          apply (subst nextA[unfolded next\<pi>_def nextV_def])
+          apply (rule light_edge_is_safe[where S=V, OF subset_MST AssV \<open>u0\<in>V\<close> \<open>u\<notin>V\<close> \<open>w {u0,u} = enat d\<close>]) 
+          using global_min by blast
+        subgoal unfolding \<pi>'_def using \<open>r\<in>V\<close> r_inv by (auto)
+        subgoal unfolding \<pi>'_def using \<pi>_in_V by (auto split: if_splits)
+        subgoal for u' v d' unfolding \<pi>'_def edges_def using \<pi>_defined apply (auto split: if_splits intro: aux1 aux2) done
+        subgoal using \<open>r\<in>V\<close> apply simp
+          unfolding Q'_def Q_alt_def
+          apply (auto simp: fun_eq_iff Q)
+          apply (auto simp: Q_alt_def \<open>V\<noteq>{}\<close> min_def edges_def not_less Min_eq_iff)
+          using antisym by blast
+        subgoal by auto
+        done  
+      qed
+    qed
+
+    
+
+  lemma (in -) Min_enat_inf_iff: "\<lbrakk> finite V; V\<noteq>{} \<rbrakk> \<Longrightarrow> Min V = \<infinity> \<longleftrightarrow> V={\<infinity>}" for V::"enat set" by (auto simp: Min_eq_iff)
+
+  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: "Q = (\<lambda>_. \<infinity>)"
+    shows "is_MST (A \<pi> V)"
+  proof -
+    show ?thesis proof (cases "r\<in>V")
+      assume [simp]: "r\<notin>V" 
+      from F Q_alt have False unfolding initQ_def by (auto simp: fun_eq_iff split: if_splits)
+      thus ?thesis ..
+    next
+      assume "r\<in>V" 
+      hence Q: "Q=Q_alt V" and \<open>V\<noteq>{}\<close> using Q_alt by auto
+  
+      from F[unfolded Q Q_alt_def] have "w {u,v} = \<infinity>" if "u\<in>V" "v\<notin>V" for u v using that
+        by (auto simp: fun_eq_iff \<open>V\<noteq>{}\<close> Min_eq_iff  edges_def split: if_splits)
+      (*hence "\<forall>e\<in>edges. e\<subseteq>V \<or> e\<subseteq>-V" apply (auto simp: edges_def) *)
+
+      (*
+        assume: A\<subseteq>T, T is MST
+
+        assume (u,v):T show (u,v):A
+
+        case u,v \<notin> V: Exclude by connectedness of graph argument
+        case u\<in>V, v\<notin>V and sym: see above
+        case u,v \<in> V: 
+          u,v are nodes of A. A is connected.
+          path u--v in A. Hence u--v in T. as edge u-v also in T, this path is edge.
+
+      *)
+      show ?thesis sorry
+    qed
+  qed
+    
+  definition (in Prim) "remaining_edges \<pi> V = edges - A \<pi> V"
+
+  text \<open>A step decreases the set of unfinished nodes.\<close>
+  lemma unfinished_nodes_decr:
+    assumes UNS: "Q u = enat d"
+    assumes MIN: "\<forall>v. enat d \<le> Q v"
+    shows "remaining_edges (next\<pi> Q \<pi> V u) (nextV V u) \<subset> remaining_edges \<pi> V"
+  proof -
+    have "remaining_edges (next\<pi> Q \<pi> V u) (nextV V u) \<subseteq> remaining_edges \<pi> V"
+      using assms unfolding remaining_edges_def A_def \<pi>'_def edges_def nextV_def next\<pi>_def
+      by auto 
+
+    moreover obtain e where "e \<in> nextA u - A \<pi> V" "e\<in>edges" sorry
+    ultimately show ?thesis unfolding remaining_edges_def by blast
+  qed      
+
+        
+end  
+
+
+subsection \<open>Refinement by Priority Map and Map\<close>
+
+subsubsection \<open>Implementing \<open>enat\<close> by Option\<close>
+
+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 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)
+
+  
+  
+subsection \<open>Implementation using ADT Interfaces\<close>
+
+locale Prim_Impl_Adts = 
+  G: adt_finite_wgraph G_invar G_adj G_empty G_\<alpha>
++ M: Map M_empty M_update M_delete M_lookup M_invar
++ S: Set S_empty S_insert S_delete S_isin S_\<alpha> S_invar
++ Q: PrioMap Q_empty Q_update Q_delete Q_invar Q_lookup Q_is_empty Q_getmin
+  
+  for G_\<alpha> :: "'g \<Rightarrow> ('v) wgraph" and G_invar G_adj G_empty
+  and M_empty M_update M_delete and M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> 'v option" and M_invar
+  and S_empty S_insert S_delete S_isin and S_\<alpha> :: "'s \<Rightarrow> 'v set" and S_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  
+  
+(* TODO: Move *)
+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 Prim_Impl_Defs = Prim_Impl_Adts where G_\<alpha> = G_\<alpha>
+  + Prim \<open>G_\<alpha> g\<close> r
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder) wgraph" and g r
+  + constrains M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> 'v option" and S_\<alpha> :: "'s \<Rightarrow> 'v set" and Q_lookup :: "'q \<Rightarrow> 'v \<Rightarrow> nat option"
+begin
+  (* definitions of concrete operations *)
+
+definition foreach :: "'q \<Rightarrow> 'm \<Rightarrow> 's \<Rightarrow> 'v \<Rightarrow> (nat \<times> 'v) list \<Rightarrow> 'q \<times> 'm" where
+"foreach Qi \<pi>i Vi u adjs = fold (\<lambda>(d,v) (Qi,\<pi>i).
+  if \<not> S_isin Vi v \<and> enat d < enat_of_option(Q_lookup Qi v)
+  then (Q_update v d Qi, M_update v u \<pi>i)
+  else (Qi,\<pi>i)) adjs (Qi,\<pi>i)"
+
+end
+
+(*
+locale Prim_Impl = Prim_Impl_Defs where G_\<alpha> = G_\<alpha>  
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder) wgraph" 
+  +
+  assumes G_invar[simp]: "G_invar g"
+
+locale PrimState_Impl = Prim_Impl where G_\<alpha> = G_\<alpha> and M_lookup = M_lookup and S_\<alpha> = S_\<alpha> and Q_lookup = Q_lookup
+  for G_\<alpha> :: "'g \<Rightarrow> ('v::linorder) wgraph"
+  and M_lookup :: "'m \<Rightarrow> 'v \<Rightarrow> 'v option" and S_\<alpha> :: "'s \<Rightarrow> 'v set" and Q_lookup :: "'q \<Rightarrow> 'v \<Rightarrow> nat option" +
+  fixes Qi::'q and \<pi>i::'m and Vi::'s
+begin
+  definition "Q \<equiv> enat_of_option o Q_lookup Qi :: 'v \<Rightarrow> enat"
+  definition "\<pi> \<equiv> M_lookup \<pi>i :: 'v \<Rightarrow> 'v option"
+  definition "V \<equiv> S_\<alpha> Vi :: 'v set"
+  
+  sublocale abs: PrimState \<open>G_\<alpha> g\<close> r Q \<pi> V by unfold_locales
+
+end
+*)
+
+
+context Prim_Invar begin
+
+  definition "foreach_body u \<equiv> \<lambda>(d,v) (Q,\<pi>).
+    if v\<notin>V \<and> enat d < Q v
+    then (Q(v:=enat d), \<pi>(v\<mapsto>u))
+    else (Q,\<pi>)"
+
+  definition foreach where
+    "foreach u adjs = foldr (foreach_body u) adjs (Q,\<pi>)"
+
+  thm Q'_def \<pi>'_def
+
+  definition "\<And>Q V. Q'i Q V u adjs v = (if v \<notin> snd`set adjs then Q v else Q' Q V u v)"
+  definition "\<And>Q V \<pi>. \<pi>'i Q \<pi> V u adjs v = (if v \<notin> snd`set adjs then \<pi> v else \<pi>' Q \<pi> V u v)"
+
+  lemma 
+    assumes "set adjs = {(d,v). w {u,v} = enat d}"
+    shows "foreach u adjs = (Q' Q V u,\<pi>' Q \<pi> V u)"
+  proof -
+
+    have INVAR_INIT: "Q'i Q V u [] = Q" "\<pi>'i Q \<pi> V u [] = \<pi>" for Q \<pi>
+      unfolding assms Q'i_def \<pi>'i_def by (auto simp: fun_eq_iff image_def Q'_def \<pi>'_def edges_def)
+
+    from assms have "set adjs \<subseteq> {(d,v). w {u,v} = enat d}" by simp
+    then have 1: "foreach u adjs = (Q'i Q V u adjs,\<pi>'i Q \<pi> V u adjs)"
+      unfolding foreach_def
+    proof (induction adjs arbitrary: Q \<pi>)
+      case Nil
+      then show ?case by (simp add: INVAR_INIT)
+    next
+      case (Cons a adjs)
+      show ?case using Cons.prems
+        apply (simp add: Cons.IH)
+        apply (auto simp: foreach_body_def Q'i_def \<pi>'i_def \<pi>'_def fun_eq_iff Q'_def edges_def split!: prod.split)
+        done
+    qed
+    show ?thesis unfolding 1 unfolding Q'i_def \<pi>'i_def assms 
+      apply (auto simp: fun_eq_iff image_def)
+
+
+
+
+
+end
+
+
+
+oops
+begin  
+  lemma finite_all_dnodes[simp, intro!]: "finite all_dnodes"
+  proof -  
+    have "all_dnodes \<subseteq> Set.insert s (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 .
+  qed
+
+  lemma finite_unfinished_dnodes[simp, intro!]: "finite (unfinished_dnodes S)"
+    using finite_subset[OF unfinished_nodes_subset] by auto
+    
+
+  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
+  
+  definition (in Prim_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_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 Prim_Impl_Defs) "P_invar_impl Q V \<equiv> 
+    Q_invar Q \<and> M_invar V \<and> P_invar' (Q_lookup Q) (M_lookup V)"
+
+  definition (in Prim_Impl_Defs)
+    "Q_initQ \<equiv> Q_update s 0 Q_empty"
+            
+  lemma Q_init_Q[simp]:
+    shows "Q_invar (Q_initQ)" "Q_lookup (Q_initQ) = initQ"
+    by (auto simp: Q_initQ_def initQ_def)
+    
+  definition (in Prim_Impl_Defs)
+    "M_initV \<equiv> 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
+  
+  definition (in Prim_Impl_Defs) 
+    "dijkstra_loop \<equiv> while (\<lambda>(Q,V). \<not> Q_is_empty Q) (\<lambda>(Q,V). 
+      let
+        (u,du) = Q_getmin 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,M_initV)"
+  
+  definition (in Prim_Impl_Defs) "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> P_invar_impl Q V \<and> Q_is_empty Q"
+    unfolding dijkstra_loop_def
+    apply (rule while_rule[where 
+          P="case_prod P_invar_impl" 
+      and r="inv_image finite_psubset (unfinished_dnodes' o M_lookup o snd)"])
+    apply (all \<open>(clarsimp split: prod.splits)?\<close>) (* TODO: Move to own lemma! *)
+    subgoal
+      apply (simp add: P_invar_impl_def)
+      apply (simp add: P_invar'_def)
+      apply (intro exI conjI)
+      apply (rule coupling_init)
+      using initD_def initS_def invar_init by auto
+  proof -  
+    fix Q V u du
+    assume "\<not> Q_is_empty Q" "P_invar_impl Q V" "Q_getmin Q = (u, du)"
+    hence "Q_lookup Q \<noteq> Map.empty" "P_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: P_invar_impl_def elim: Q.map_getminE)
+      
+    then obtain D S where "P_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: P_invar'_def transfer_preconditions less_eq_enat_def split: enat.splits) 
+      
+    then interpret Prim_Invar "G_\<alpha> g" s D S by simp
+      
+    have COUPLING': "coupling 
+        ((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>] . 
+      
+    show "P_invar_impl (Q_delete u (Q_relax_outgoing u du V Q)) (M_update u du V)"
+      using maintain_P_invar[OF \<open>u\<notin>S\<close>] ABS_PRE
+      using COUPLING'
+      by (auto simp: P_invar_impl_def P_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] coupling_unfinished[OF COUPLING']
+      using unfinished_nodes_decr[OF \<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: P_invar_impl_def\<close>)
+    apply (clarsimp simp: P_invar'_def)
+    subgoal for Q V D S  
+      using Prim_Invar.invar_finish_imp_correct[of "G_\<alpha> g" s D S u]
+      apply (clarsimp simp: coupling_def)
+      by (auto simp: domIff)
+    done
+  
+    
+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
+  defines G_empty = G.empty_graph
+      and G_add_edge = G.add_edge
+      and G_succ = G.succ
+  by unfold_locales
+
+global_interpretation Prim_Impl_Adts
+  G.\<alpha> G.invar G.succ G.empty_graph G.add_edge
+  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+  RBT_Heap.empty RBT_Heap.update RBT_Heap.delete RBT_Heap.PM.invar Lookup2.lookup RBT_Heap.rbt_is_empty RBT_Heap.rbt_getmin
+  ..
+
+global_interpretation D: Prim_Impl_Defs  
+  G.invar G.succ G.empty_graph G.add_edge
+  RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+  RBT_Heap.empty RBT_Heap.update RBT_Heap.delete RBT_Heap.PM.invar Lookup2.lookup RBT_Heap.rbt_is_empty RBT_Heap.rbt_getmin
+  G.\<alpha> g s for g and s::"'v::linorder"
+  defines dijkstra = D.dijkstra
+      and dijkstra_loop = D.dijkstra_loop
+      and Q_relax_outgoing = D.Q_relax_outgoing
+      and M_initV = D.M_initV
+      and Q_initQ = D.Q_initQ
+  ..
+  
+(* TODO: Why is this fix necessary? *)
+lemmas [code] =    
+  D.dijkstra_def D.dijkstra_loop_def  
+  
+context
+  fixes g
+  assumes [simp]: "G.invar g"  
+begin  
+  
+  interpretation AUX: Prim_Impl
+    G.invar G.succ G.empty_graph G.add_edge
+    RBT_Set.empty RBT_Map.update RBT_Map.delete Lookup2.lookup RBT_Map.M.invar
+    RBT_Heap.empty RBT_Heap.update RBT_Heap.delete RBT_Heap.PM.invar Lookup2.lookup RBT_Heap.rbt_is_empty RBT_Heap.rbt_getmin
+    g s G.\<alpha> for s
+    by unfold_locales simp_all
+  
+  lemmas dijkstra_correct = AUX.dijkstra_correct[folded dijkstra_def]
+  
+end  
+  
+export_code dijkstra in SML 
+
+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
+  ..
+  
+  
+definition "dijkstra_list l s \<equiv> if valid_graph_rep l then Some (dijkstra (from_list l) s) else None"
+
+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)
+
+export_code dijkstra_list in OCaml
+  
+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_UGraph_Specs.thy	Mon Jan 21 16:00:30 2019 +0100
@@ -0,0 +1,345 @@
+section \<open>Weighted Undirected Graphs\<close>
+theory Weighted_UGraph_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 set \<Rightarrow> enat"
+
+text \<open>We encapsulate weighted graphs into a locale that fixes a graph\<close>
+locale WGraph = fixes w :: "'v wgraph"
+assumes w_card2: "card e \<noteq> 2 \<Longrightarrow> w e = \<infinity>"
+begin
+  text \<open>Set of edges with finite weight\<close>
+  definition "edges \<equiv> {e . w e \<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>
+(*
+  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.
+    Note: The \<open>< \<infinity>\<close> conditions are required to avoid saturation in adding to \<open>\<infinity>\<close>!
+  \<close>
+  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  
+  *)
+      
+  lemma edges_empty_iff: "edges = {} \<longleftrightarrow> w=(\<lambda>_. \<infinity>)"
+    unfolding edges_def by auto
+
+
+end
+
+
+lemma wgraph_empty_edges[simp]: "WGraph.edges (\<lambda>e. \<infinity>) = {}"
+proof -
+  interpret WGraph "\<lambda>e. \<infinity>" apply standard by auto
+  show ?thesis using edges_empty_iff by simp
+qed
+
+
+subsection \<open>Abstract Data Type\<close>
+
+definition "adj_sym m = (\<forall>u v d. (d,v)\<in>set(m u) \<longrightarrow> (d,u) \<in> set(m v))"
+definition "adj_loop_free m = (\<forall>d u. (d,u)\<notin>set (m u))"
+
+locale adt_wgraph =
+  fixes \<alpha> :: "'g \<Rightarrow> ('v) wgraph"
+    and invar :: "'g \<Rightarrow> bool"
+    and adj :: "'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 abs_invar: "invar g \<Longrightarrow> WGraph (\<alpha> g)"
+  assumes adj_correct: "invar g \<Longrightarrow> set (adj 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 {u,v} = \<infinity> \<Longrightarrow> u \<noteq> v \<Longrightarrow> invar (add_edge (u,v) d g)"
+    "invar g \<Longrightarrow> \<alpha> g {u,v} = \<infinity> \<Longrightarrow>  u \<noteq> v \<Longrightarrow> \<alpha> (add_edge (u,v) d g) = (\<alpha> g)({u,v}:=enat d)"
+  *)
+begin
+
+  
+  lemmas wgraph_specs = abs_invar adj_correct empty_graph_correct (*add_edge_correct*)
+  
+  lemma adj_symmetric: assumes "invar g" 
+        shows "adj_sym(adj g)"
+  proof -
+    interpret WGraph "\<alpha> g" using assms abs_invar by blast
+    show ?thesis unfolding adj_sym_def
+      by (metis (no_types, lifting) adj_correct[OF assms] case_prodD case_prodI doubleton_eq_iff mem_Collect_eq)
+  qed
+
+  lemma assumes "invar g"
+    shows "adj_loop_free (adj g)"
+  proof -
+    interpret WGraph "\<alpha> g" using assms abs_invar by blast
+    show ?thesis
+      by (simp add: adj_correct[OF \<open>invar g\<close>] w_card2 adj_loop_free_def)
+  qed    
+
+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))
+(*>*)
+
+definition "epair e = (SOME (u,v). e={u,v})"
+
+lemma epair_eq_iff: "card e = 2 \<Longrightarrow> epair e = (x,y) \<longleftrightarrow> e = {x,y}"
+sorry
+
+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>e. 
+      if card e = 2 then let (u,v) = epair e in
+        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>
+      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))
+       \<and> adj_sym (the_default [] o (M_lookup g))
+       \<and> adj_loop_free (the_default [] o (M_lookup g))"
+
+  definition adj :: "'m \<Rightarrow> 'v \<Rightarrow> (nat \<times> 'v) list" where
+    "adj g v = the_default [] (M_lookup g v)"
+    
+  definition empty_graph :: "'m" where "empty_graph = M_empty"
+  
+  definition add_edge1 :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'm \<Rightarrow> 'm" where
+    "add_edge1 \<equiv> \<lambda>(u,v) d g. M_update u ((d,v) # the_default [] (M_lookup g u)) g"
+  
+  definition add_edge :: "'v\<times>'v \<Rightarrow> nat \<Rightarrow> 'm \<Rightarrow> 'm" where
+    "add_edge \<equiv> \<lambda>(u,v) d g. add_edge1 (v,u) d (add_edge1 (u,v) d g)"
+  
+  lemma adj_sym_concD: "\<lbrakk>adj_sym (the_default [] \<circ> m); (d, u) \<in> set l; m v = Some l\<rbrakk> \<Longrightarrow> \<exists>l'. m u = Some l' \<and> (d,v)\<in>set l'"
+    unfolding adj_sym_def apply auto 
+    by (metis (no_types, hide_lams) empty_iff set_empty the_default.elims the_default.simps(2))
+        
+  lemma adj_correct_aux:
+    assumes "invar g" "(d, v) \<in> set a" and gu: "M_lookup g u = Some a"  
+    shows "\<alpha> g {u, v} = enat d"
+  proof -
+    from \<open>invar g\<close> obtain l' where gv: "M_lookup g v = Some l'" 
+      apply (cases "M_lookup g v")
+      unfolding invar_def adj_loop_free_def apply auto 
+      apply (metis adj_sym_concD assms(2) assms(3) option.discI)
+      done
+
+    have "(d,u)\<in>set l'" sorry (* symmetry *)
+
+    have d_uniq: "d=d'" if "(d,v)\<in>set a" and "(d',v)\<in>set a" "a\<in>ran (M_lookup g)" for a d d' v sorry
+    have d_uniqa: "d'=d" if "(d',v)\<in>set a" for d' using d_uniq[OF that assms(2)] gu by (auto simp: ran_def)
+    have d_uniql': "d'=d" if "(d',u)\<in>set l'" for d' using d_uniq[OF that \<open>(d,u)\<in>set l'\<close>] gv by (auto simp: ran_def)
+
+
+    have [simp]: "u\<noteq>v" sorry
+    show ?thesis
+      using \<open>(d,v)\<in>set a\<close>
+      using \<open>(d,u)\<in>set l'\<close>
+      unfolding \<alpha>_def apply (auto split: prod.split option.splits simp: epair_eq_iff doubleton_eq_iff gu gv)
+      using d_uniqa apply blast
+      using d_uniql' apply blast
+      done
+  qed
+
+  lemma adj_correct_aux2: assumes "invar g" "\<alpha> g {u, v} = enat d"
+    obtains l where "M_lookup g u = Some l" "(d,v)\<in>set l"
+    using assms apply (auto simp: \<alpha>_def epair_eq_iff doubleton_eq_iff split: if_splits prod.splits option.splits)
+    apply (meson verit_sko_ex_indirect)
+    by (metis (mono_tags) adj_sym_concD invar_def tfl_some)
+
+
+  sublocale adt_finite_wgraph invar adj empty_graph \<alpha>
+    apply unfold_locales
+    subgoal by(auto simp: \<alpha>_def)
+    subgoal for g u
+      apply (auto simp: adj_def)
+      subgoal for d v by (cases "M_lookup g u") (auto simp: adj_correct_aux)
+      subgoal for d v apply (cases "M_lookup g u") apply (auto elim: adj_correct_aux2) done
+      done  
+
+    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs adj_sym_def adj_loop_free_def cong: if_cong split: option.split)
+    subgoal by (auto simp: invar_def \<alpha>_def empty_graph_def add_edge_def M.map_specs split: option.split)
+    subgoal by (simp add: invar_def)     
+    done
+
+end  
+ 
+  
+end