--- 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>