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

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