author lammich 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 file | annotate | diff | comparison | revisions
```--- 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>```