author lammich Thu, 12 Jul 2018 23:32:12 +0200 changeset 69949 217d8ffe0fde parent 69948 7c35ab688cb8 child 69950 dc55e8f7a9bd
Simplification of proofs and invar
 Thys/Dijkstra.thy file | annotate | diff | comparison | revisions Thys/Weighted_Graph_Specs.thy file | annotate | diff | comparison | revisions
```--- 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)
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>"```