--- a/Thys/Dijkstra.thy Mon Jul 09 11:57:12 2018 +0200
+++ b/Thys/Dijkstra.thy Thu Jul 12 23:32:12 2018 +0200
@@ -64,7 +64,6 @@
assumes s_in_S: \<open>s\<in>S\<close> \<comment> \<open>The start node is finished\<close>
(* TODO: CLRS starts with empty S *)
assumes S_precise: "u\<in>S \<Longrightarrow> D u = \<delta> s u" \<comment> \<open>Finished nodes have precise estimate\<close>
- assumes S_connected: \<open>u\<in>S \<Longrightarrow> \<delta> s u < \<infinity>\<close> \<comment> \<open>Finished nodes have finite distance\<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>
begin
@@ -96,16 +95,15 @@
This will allow us to add the node \<open>u\<close> to \<open>S\<close>. \<close>
lemma maintain_S_precise_and_connected:
assumes UNS: "u\<notin>S"
- assumes UNI: "D u < \<infinity>"
assumes MIN: "\<forall>v. v\<notin>S \<longrightarrow> D u \<le> D v"
- shows "D u = \<delta> s u" (*"\<delta> s u < \<infinity>"*)
- proof -
+ 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
+ next
+ assume "\<delta> s u < \<infinity>"
note s_in_S
-
- text \<open>Node \<open>u\<close> has a finite estimate, thus it has a finite distance from \<open>s\<close>\<close>
- from UNI upper_bound have DSUNI: "\<delta> s u < \<infinity>"
- by (clarsimp) (metis enat_ile)
-
+
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)
@@ -144,7 +142,7 @@
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 assms] UNI S_connected S_precise
+ 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
@@ -156,34 +154,14 @@
lemma invar_finish_imp_correct:
assumes F: "\<forall>u. u\<notin>S \<longrightarrow> D u = \<infinity>"
shows "D u = \<delta> s u"
- proof (cases)
+ proof (cases "u\<in>S")
assume "u\<in>S" text \<open>The estimates of finished nodes are accurate\<close>
then show ?thesis using S_precise by simp
next
- assume \<open>u\<notin>S\<close> text \<open>So consider an unfinished node \<open>u\<close>\<close>
- note s_in_S
-
- {
- text \<open>We will show that it is not connected to \<open>s\<close>\<close>
- presume "\<delta> s u = \<infinity>"
- text \<open>Thus, both its estimate and its distance must be \<open>\<infinity>\<close>\<close>
- with upper_bound[of u] show "D u = \<delta> s u" by auto
- }
+ assume \<open>u\<notin>S\<close> text \<open>\<open>D u\<close> is minimal, and minimal estimates are precise\<close>
+ then show ?thesis
+ using F maintain_S_precise_and_connected[of u] by auto
- text \<open>It remains to show that \<open>\<delta> s u = \<infinity>\<close>. For this, we obtain a shortest path 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>And find an edge where it leaves \<open>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 \<open>x\<in>S\<close>, it has a finite distance, and the edge \<open>(x,y)\<close> got relaxed
- with a precise estimate for \<open>x\<close>. However, as we terminated and \<open>y\<notin>S\<close>,
- the estimate for \<open>y\<close> is \<open>\<infinity>\<close>. Thus, the edge has infinite weight.\<close>
- have "w (x,y) = \<infinity>"
- using S_connected[OF \<open>x\<in>S\<close>] S_relaxed[OF \<open>x\<in>S\<close>, of y] F \<open>y\<notin>S\<close>
- by (cases "w (x,y)") auto
- text \<open>And so has the path on which this edge lays\<close>
- then show "\<delta> s u = \<infinity>" by (auto simp: DSU)
qed
--- a/Thys/Weighted_Graph_Specs.thy Mon Jul 09 11:57:12 2018 +0200
+++ b/Thys/Weighted_Graph_Specs.thy Thu Jul 12 23:32:12 2018 +0200
@@ -122,8 +122,9 @@
finally show ?thesis unfolding \<delta>_def .
qed
- text \<open>Any prefix of a shortest path is a shortest path itself.\<close>
- (* TODO: Do we need the < \<infinity> ? *)
+ text \<open>Any prefix of a shortest path is a shortest path itself.
+ Note: The \<open>< \<infinity>\<close> conditions are required to avoid saturation in adding to \<open>\<infinity>\<close>!
+ \<close>
lemma shortest_path_prefix:
assumes "path s p\<^sub>1 x" "path x p\<^sub>2 u"
and DSU: "\<delta> s u = sum_list p\<^sub>1 + sum_list p\<^sub>2" "\<delta> s u < \<infinity>"