Simplification of proofs and invar draft
authorlammich <lammich@in.tum.de>
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
Thys/Weighted_Graph_Specs.thy
--- 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>"