Simplified initialization draft
authorlammich <lammich@in.tum.de>
Fri, 13 Jul 2018 20:33:36 +0200
changeset 69951 2c739672fa5d
parent 69950 dc55e8f7a9bd
child 69952 0f52de3ddf8f
Simplified initialization
Thys/Dijkstra.thy
--- a/Thys/Dijkstra.thy	Thu Jul 12 23:38:18 2018 +0200
+++ b/Thys/Dijkstra.thy	Fri Jul 13 20:33:36 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Dijstra's Algorithm\<close>
+section \<open>Dijkstra's Algorithm\<close>
 theory Dijkstra
 imports 
   Main 
@@ -36,8 +36,8 @@
     where "relax_outgoing u D \<equiv> \<lambda>v. min (D v) (D u + w (u,v))"
 
   text \<open>Initialization\<close>
-  definition "initD \<equiv> (relax_outgoing s ((\<lambda>_. \<infinity>)(s:=0)))"
-  definition "initS \<equiv> {s}"  
+  definition "initD \<equiv> (\<lambda>_. \<infinity>)(s:=0)"
+  definition "initS \<equiv> {}"  
     
         
   text \<open>Relaxing will never increase estimates\<close>
@@ -45,7 +45,7 @@
     by (auto simp: relax_outgoing_def)
   
 
-  definition "all_dnodes \<equiv> { v . \<exists>u. w (u,v)\<noteq>\<infinity> }"
+  definition "all_dnodes \<equiv> Set.insert s { 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"
@@ -61,17 +61,7 @@
 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 
-    We can also get rid of s\<in>S. However, the invariant then has to state
-    that node s is processed first, or, in other words, if there is any node \<noteq>s
-    with finite estimate, then s\<in>S.
-    
-    s\<in>S \<or> (\<forall>u. u\<noteq>s \<longrightarrow> D u = \<infinity>)
-    
-    This will yield slightly more complicated proofs, but initialization of 
-    the algorithm will get simpler!
-  *)
+  assumes s_in_S: \<open>s\<in>S \<or> (D=(\<lambda>_. \<infinity>)(s:=0) \<and> S={})\<close> \<comment> \<open>The start node is finished, or we are in initial state\<close>  
   assumes S_precise: "u\<in>S \<Longrightarrow> D u = \<delta> s u" \<comment> \<open>Finished nodes have precise estimate\<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>
@@ -106,40 +96,54 @@
     assumes UNS: "u\<notin>S"
     assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
     shows "D u = \<delta> s u"
-  proof (cases \<open>\<delta> s u < \<infinity>\<close>)
-    assume "\<not>(\<delta> s u < \<infinity>)"
-    then show ?thesis using upper_bound[of u] by auto
+    text \<open>We start with a case distinction whether we are in the first 
+      step of the loop, where we process the start node, or in subsequent steps,
+      where the start node has already been finished.\<close>
+  proof (cases "u=s")  
+    assume [simp]: "u=s" \<comment> \<open>First step of loop\<close>
+    then show ?thesis using \<open>u\<notin>S\<close> s_in_S by simp
   next
-    assume "\<delta> s u < \<infinity>"
-    note s_in_S
- 
-    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    
+    assume \<open>u\<noteq>s\<close> \<comment> \<open>Later step of loop\<close>
+    text \<open>The start node has already been finished\<close>   
+    with s_in_S MIN have \<open>s\<in>S\<close> apply clarsimp using infinity_ne_i0 by metis
+    
+    show ?thesis
+    text \<open>Next, we handle the case that \<open>u\<close> is unreachable.\<close>
+    proof (cases \<open>\<delta> s u < \<infinity>\<close>)
+      assume "\<not>(\<delta> s u < \<infinity>)" \<comment> \<open>Node is unreachable (infinite distance)\<close>
+      text \<open>By the upper-bound property, we get \<open>D u = \<delta> s u = \<infinity>\<close>\<close>
+      then show ?thesis using upper_bound[of u] by auto
+    next
+      assume "\<delta> s u < \<infinity>" \<comment> \<open>Main case: Node has finite distance\<close>
+   
+      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    
+  qed
     
   text \<open>A step of Dijkstra's algorithm maintains the invariant.
     More precisely, in a step of Dijkstra's algorithm, 
@@ -150,11 +154,18 @@
     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 UNS MIN] UNI 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
+    apply (cases \<open>s\<in>S\<close>)
+    subgoal
+      apply unfold_locales
+      using maintain_S_precise_and_connected[OF UNS MIN] UNI S_precise
+      apply (auto simp: maintain_upper_bound upper_bound relax_precise_id)
+      apply (simp add: relax_outgoing_def)  
+      by (meson S_relaxed order.trans relax_mono)
+    subgoal
+      apply unfold_locales
+      using s_in_S UNI distance_direct 
+      by (auto simp: relax_outgoing_def split: if_splits)
+    done
     
 
   text \<open>When the algorithm is finished, i.e., when there are 
@@ -180,21 +191,18 @@
     assumes UNI: "D u < \<infinity>"
     shows "unfinished_dnodes (Set.insert u S) \<subset> unfinished_dnodes S"
   proof -
-    note s_in_S
-      
     text \<open>There is a path to \<open>u\<close>\<close>
     from UNI have "\<delta> s u < \<infinity>" using upper_bound[of u] leD by fastforce
     
-    text \<open>Thus, \<open>u\<close> must have an incoming edge and is among \<open>all_dnodes\<close>\<close>
+    text \<open>Thus, \<open>u\<close> is among \<open>all_dnodes\<close>\<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 
+      with \<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
+        by (auto simp: Dijkstra.all_dnodes_def)
     qed
     text \<open>Which implies the proposition\<close>
     with \<open>u\<notin>S\<close> show ?thesis by (auto simp: unfinished_dnodes_def)
@@ -284,7 +292,9 @@
     assumes UNS: "u\<notin>S"
     assumes UNI: "D u = enat du"
     
-    shows "coupling ((relax_outgoing' u du V Q)(u:=None)) (V(u\<mapsto>du)) (relax_outgoing u D) (Set.insert u S)"
+    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 
   proof (intro ext conjI; elim conjE)
     assume \<alpha>: "D = enat_of_option \<circ> V ++ Q" "S = dom V" 
@@ -319,8 +329,8 @@
   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]"
+  definition "initQ \<equiv> Map.empty(s\<mapsto>0)"
+  definition "initV \<equiv> Map.empty"
     
   lemma coupling_init:
     "coupling initQ initV initD initS"    
@@ -377,37 +387,7 @@
       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
-      
 end
   
 subsection \<open>Implementation using ADT Interfaces\<close>
@@ -452,7 +432,7 @@
 begin  
   lemma finite_all_dnodes[simp, intro!]: "finite all_dnodes"
   proof -  
-    have "all_dnodes \<subseteq> snd ` edges"
+    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 .
@@ -486,32 +466,14 @@
     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"
+    "Q_initQ \<equiv> Q_update s 0 Q_empty"
             
   lemma Q_init_Q[simp]:
-    shows "Q_invar (Q_initQ s)" "Q_lookup (Q_initQ s) = 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 s)" unfolding Q_initQ_def by auto
-      
-    from aux have "Q_lookup (Q_initQ s) = 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 s) = initQ" .
-  qed
-  
+    shows "Q_invar (Q_initQ)" "Q_lookup (Q_initQ) = initQ"
+    by (auto simp: Q_initQ_def initQ_def)
     
   definition (in Dijkstra_Impl_Defs)
-    "M_initV \<equiv> M_update s 0 M_empty"
+    "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
@@ -527,7 +489,7 @@
         V = M_update u du V
       in
         (Q,V)
-    ) (Q_initQ s,M_initV)"
+    ) (Q_initQ,M_initV)"
   
   definition (in Dijkstra_Impl_Defs) "dijkstra \<equiv> snd dijkstra_loop"
   
@@ -582,7 +544,9 @@
       by simp
   qed  
     
-  lemma dijkstra_correct: "M_invar dijkstra" "M_lookup dijkstra u = Some d \<longleftrightarrow> \<delta> s u = enat d"
+  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 -
@@ -664,7 +628,7 @@
   unfolding dijkstra_list_def
   by (auto simp: dijkstra_correct G.from_list_correct)
 
-export_code dijkstra_list in SML
+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"