Added comment on starting with empty S draft
authorlammich <lammich@in.tum.de>
Thu, 12 Jul 2018 23:38:18 +0200
changeset 69950 dc55e8f7a9bd
parent 69949 217d8ffe0fde
child 69951 2c739672fa5d
Added comment on starting with empty S
Thys/Dijkstra.thy
--- a/Thys/Dijkstra.thy	Thu Jul 12 23:32:12 2018 +0200
+++ b/Thys/Dijkstra.thy	Thu Jul 12 23:38:18 2018 +0200
@@ -62,7 +62,16 @@
   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 *)
+  (* 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_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>