summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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