(* Title: Shortest_Path.thy Author: Lars Noschinski, TU München *) theory Shortest_Path imports Arc_Walk Weighted_Graph "HOL-Library.Extended_Real" begin section ‹Shortest Paths› context wf_digraph begin (*Rename, as we are outside of any local context?*) definition μ where "μ f u v ≡ INF p∈ {p. awalk u p v}. ereal (awalk_cost f p)" lemma shortest_path_inf: assumes "¬(u →⇧^{*}v)" shows "μ f u v = ∞" proof - have *: "{p. awalk u p v} = {}" using assms by (auto simp: reachable_awalk) show "μ f u v = ∞" unfolding μ_def * by (simp add: top_ereal_def) qed lemma min_cost_le_walk_cost: assumes "awalk u p v" shows "μ c u v ≤ awalk_cost c p" using assms unfolding μ_def by (auto intro: INF_lower2) lemma pos_cost_pos_awalk_cost: assumes "awalk u p v" assumes pos_cost: "⋀e. e ∈ arcs G ⟹ c e ≥ 0" shows "awalk_cost c p ≥ 0" using assms by (induct p arbitrary: u) (auto simp: awalk_Cons_iff) fun mk_cycles_path :: "nat ⇒ 'b awalk ⇒ 'b awalk" where "mk_cycles_path 0 c = []" | "mk_cycles_path (Suc n) c = c @ (mk_cycles_path n c)" lemma mk_cycles_path_awalk: assumes "awalk u c u" shows "awalk u (mk_cycles_path n c) u" using assms by (induct n) (auto simp: awalk_Nil_iff) lemma mk_cycles_awalk_cost: assumes "awalk u p u" shows "awalk_cost c (mk_cycles_path n p) = n * awalk_cost c p" using assms proof (induct rule: mk_cycles_path.induct) case 1 show ?case by simp next case (2 n p) have "awalk_cost c (mk_cycles_path (Suc n) p) = awalk_cost c (p @ (mk_cycles_path n p))" by simp also have "… = awalk_cost c p + real n * awalk_cost c p" proof (cases n) case 0 then show ?thesis by simp next case (Suc n') then show ?thesis using 2 by simp qed also have "… = real (Suc n) * awalk_cost c p" by (simp add: algebra_simps) finally show ?case . qed lemma inf_over_nats: fixes a c :: real assumes "c < 0" shows "(INF (i :: nat). ereal (a + i * c)) = - ∞" proof (rule INF_eqI) fix i :: nat show "- ∞ ≤ a + real i * c" by simp next fix y :: ereal assume "⋀(i :: nat). i ∈ UNIV ⟹ y ≤ a + real i * c" then have l_assm: "⋀i::nat. y ≤ a + real i * c" by simp show "y ≤ - ∞" proof (subst ereal_infty_less_eq, rule ereal_bot) fix B :: real obtain real_x where "a + real_x * c ≤ B" using ‹c < 0› by atomize_elim (rule exI[where x="(- abs B -a)/c"], auto simp: field_simps) obtain x :: nat where "a + x * c ≤ B" proof (atomize_elim, intro exI[where x="nat(ceiling real_x)"] conjI) have "real (nat(ceiling real_x)) * c ≤ real_x * c" using ‹c < 0› by (simp add: real_nat_ceiling_ge) then show "a + nat(ceiling real_x) * c ≤ B" using ‹a + real_x * c ≤ B› by simp qed then show "y ≤ ereal B" proof - have "ereal (a + x * c) ≤ ereal B" using ‹a + x * c ≤ B› by simp with l_assm show ?thesis by (rule order_trans) qed qed qed lemma neg_cycle_imp_inf_μ: assumes walk_p: "awalk u p v" assumes walk_c: "awalk w c w" assumes w_in_p: "w ∈ set (awalk_verts u p)" assumes "awalk_cost f c < 0" shows "μ f u v = -∞" proof - from w_in_p obtain xs ys where pv_decomp: "awalk_verts u p = xs @ w # ys" by (auto simp: in_set_conv_decomp) define q r where "q = take (length xs) p" and "r = drop (length xs) p" define ext_p where "ext_p n = q @ mk_cycles_path n c @ r" for n have ext_p_cost: "⋀n. awalk_cost f (ext_p n) = (awalk_cost f q + awalk_cost f r) + n * awalk_cost f c" using ‹awalk w c w› by (auto simp: ext_p_def intro: mk_cycles_awalk_cost) from q_def r_def have "awlast u q = w" using pv_decomp walk_p by (auto simp: awalk_verts_take_conv elim!: awalkE) moreover from q_def r_def have "awalk u (q @ r) v" using walk_p by simp ultimately have "awalk u q w" "awalk w r v" "⋀n. awalk w (mk_cycles_path n c) w" using walk_c by (auto simp: intro: mk_cycles_path_awalk) then have "⋀n. awalk u (ext_p n) v" unfolding ext_p_def by (blast intro: awalk_appendI) then have "{ext_p i|i. i ∈ UNIV} ⊆ {p. awalk u p v}" by auto then have "(INF p∈{p. awalk u p v}. ereal (awalk_cost f p)) ≤ (INF p∈ {ext_p i|i. i ∈ UNIV}. ereal (awalk_cost f p))" by (auto intro: INF_superset_mono) also have "… = (INF i∈ UNIV. ereal (awalk_cost f (ext_p i)))" by (rule arg_cong[where f=Inf], auto) also have "… = - ∞" unfolding ext_p_cost by (rule inf_over_nats[OF ‹awalk_cost f c < 0›]) finally show ?thesis unfolding μ_def by simp qed lemma walk_cheaper_path_imp_neg_cyc: assumes p_props: "awalk u p v" assumes less_path_μ: "awalk_cost f p < (INF p∈ {p. apath u p v}. ereal (awalk_cost f p))" shows "∃w c. awalk w c w ∧ w ∈ set (awalk_verts u p) ∧ awalk_cost f c < 0" proof - define path_μ where "path_μ = (INF p∈ {p. apath u p v}. ereal (awalk_cost f p))" then have "awalk u p v" and "awalk_cost f p < path_μ" using p_props less_path_μ by simp_all then show ?thesis proof (induct rule: awalk_to_apath_induct) case (path p) then have "apath u p v" by (auto simp: apath_def) then show ?case using path.prems by (auto simp: path_μ_def dest: not_mem_less_INF) next case (decomp p q r s) then obtain w where p_props: "p = q @ r @ s" "awalk u q w" "awalk w r w" "awalk w s v" by (auto elim: awalk_cyc_decompE) then have "awalk u (q @ s) v" using ‹awalk u p v› by (auto simp: awalk_appendI) then have verts_ss: "set (awalk_verts u (q @ s)) ⊆ set (awalk_verts u p)" using ‹awalk u p v› ‹p = q @ r @ s› by (auto simp: set_awalk_verts) show ?case proof (cases "ereal (awalk_cost f (q @ s)) < path_μ") case True then have "∃w c. awalk w c w ∧ w ∈ set (awalk_verts u (q @ s)) ∧ awalk_cost f c < 0" by (rule decomp) then show ?thesis using verts_ss by auto next case False note ‹awalk_cost f p < path_μ› also have "path_μ ≤ awalk_cost f (q @ s)" using False by simp finally have "awalk_cost f r < 0" using ‹p = q @ r @ s› by simp moreover have "w ∈ set (awalk_verts u q)" using ‹awalk u q w› by auto then have "w ∈ set (awalk_verts u p)" using ‹awalk u p v› ‹awalk u q w› ‹p = q @ r @ s› by (auto simp: set_awalk_verts) ultimately show ?thesis using ‹awalk w r w› by auto qed qed qed lemma (in fin_digraph) neg_inf_imp_neg_cyc: assumes inf_mu: "μ f u v = - ∞" shows "∃p. awalk u p v ∧ (∃w c. awalk w c w ∧ w ∈ set (awalk_verts u p) ∧ awalk_cost f c < 0)" proof - define path_μ where "path_μ = (INF s∈{p. apath u p v}. ereal (awalk_cost f s))" have awalks_ne: "{p. awalk u p v} ≠ {}" using inf_mu unfolding μ_def by safe (simp add: top_ereal_def) then have paths_ne: "{p. apath u p v} ~= {}" by (auto intro: apath_awalk_to_apath) obtain p where "apath u p v" "awalk_cost f p = path_μ" proof - obtain p where "p ∈ {p. apath u p v}" "awalk_cost f p = path_μ" using finite_INF_in[OF apaths_finite paths_ne, of "awalk_cost f"] by (auto simp: path_μ_def) then show ?thesis using that by auto qed then have "path_μ ≠ -∞" by auto then have "μ f u v < path_μ" using inf_mu by simp then obtain pw where p_def: "awalk u pw v" "awalk_cost f pw < path_μ" by atomize_elim (auto simp: μ_def INF_less_iff) then have "∃w c. awalk w c w ∧ w ∈ set (awalk_verts u pw) ∧ awalk_cost f c < 0" by (intro walk_cheaper_path_imp_neg_cyc) (auto simp: path_μ_def) with ‹awalk u pw v› show ?thesis by auto qed lemma (in fin_digraph) no_neg_cyc_imp_no_neg_inf: assumes no_neg_cyc: "⋀p. awalk u p v ⟹ ¬(∃w c. awalk w c w ∧ w ∈ set (awalk_verts u p) ∧ awalk_cost f c < 0)" shows "- ∞ < μ f u v" proof (intro ereal_MInfty_lessI notI) assume "μ f u v = - ∞" then obtain p where p_props: "awalk u p v" and ex_cyc: "∃w c. awalk w c w ∧ w ∈ set (awalk_verts u p) ∧ awalk_cost f c < 0" by atomize_elim (rule neg_inf_imp_neg_cyc) then show False using no_neg_cyc by blast qed lemma μ_reach_conv: "μ f u v < ∞ ⟷ u →⇧^{*}v" proof assume "μ f u v < ∞" then have "{p. awalk u p v} ≠ {}" unfolding μ_def by safe (simp add: top_ereal_def) then show "u →⇧^{*}v" by (simp add: reachable_awalk) next assume "u →⇧^{*}v" then obtain p where p_props: "apath u p v" by (metis reachable_awalk apath_awalk_to_apath) then have "{p} ⊆ {p. apath u p v}" by simp then have "μ f u v ≤ (INF p∈ {p}. ereal (awalk_cost f p))" unfolding μ_def by (intro INF_superset_mono) (auto simp: apath_def) also have "… < ∞" by (simp add: min_def) finally show "μ f u v < ∞" . qed lemma awalk_to_path_no_neg_cyc_cost: assumes p_props:"awalk u p v" assumes no_neg_cyc: "¬ (∃w c. awalk w c w ∧ w ∈ set (awalk_verts u p) ∧ awalk_cost f c < 0)" shows "awalk_cost f (awalk_to_apath p) ≤ awalk_cost f p" using assms proof (induct rule: awalk_to_apath_induct) case path then show ?case by (auto simp: awalk_to_apath.simps) next case (decomp p q r s) from decomp(2,3) have "is_awalk_cyc_decomp p (q,r,s)" using awalk_cyc_decomp_has_prop[OF decomp(1)] by auto then have decomp_props: "p = q @ r @ s" "∃w. awalk w r w" by auto have "awalk_cost f (awalk_to_apath p) = awalk_cost f (awalk_to_apath (q @ s))" using decomp by (auto simp: step_awalk_to_apath[of _ p _ q r s]) also have "… ≤ awalk_cost f (q @ s)" proof - have "awalk u (q @ s) v" using ‹awalk u p v› decomp_props by (auto dest!: awalk_ends_eqD) then have "set (awalk_verts u (q @ s)) ⊆ set (awalk_verts u p)" using ‹awalk u p v› ‹p = q @ r @ s› by (auto simp add: set_awalk_verts) then show ?thesis using decomp.prems by (intro decomp.hyps) auto qed also have "… ≤ awalk_cost f p" proof - obtain w where "awalk u q w" "awalk w r w" "awalk w s v" using decomp by (auto elim: awalk_cyc_decompE) then have "w ∈ set (awalk_verts u q)" by auto then have "w ∈ set (awalk_verts u p)" using ‹p = q @ r @ s› ‹awalk u p v› ‹awalk u q w› by (auto simp add: set_awalk_verts) then have "0 ≤ awalk_cost f r" using ‹awalk w r w› using decomp.prems by (auto simp: not_less) then show ?thesis using ‹p = q @ r @ s› by simp qed finally show ?case . qed lemma (in fin_digraph) no_neg_cyc_reach_imp_path: assumes reach: "u →⇧^{*}v" assumes no_neg_cyc: "⋀p. awalk u p v ⟹ ¬(∃w c. awalk w c w ∧ w ∈ set (awalk_verts u p) ∧ awalk_cost f c < 0)" shows "∃p. apath u p v ∧ μ f u v = awalk_cost f p" proof - define set_walks where "set_walks = {p. awalk u p v}" define set_paths where "set_paths = {p. apath u p v}" have "set_paths ≠ {}" proof - obtain p where "apath u p v" using reach by (metis apath_awalk_to_apath reachable_awalk) then show ?thesis unfolding set_paths_def by blast qed have "μ f u v = (INF p∈ set_walks. ereal (awalk_cost f p))" unfolding μ_def set_walks_def by simp also have "… = (INF p∈ set_paths. ereal (awalk_cost f p))" proof (rule antisym) have "awalk_to_apath ` set_walks ⊆ set_paths" unfolding set_walks_def set_paths_def by (intro subsetI) (auto elim: apath_awalk_to_apath) then have "(INF p∈ set_paths. ereal (awalk_cost f p)) ≤ (INF p∈ awalk_to_apath ` set_walks. ereal (awalk_cost f p))" by (rule INF_superset_mono) simp also have "… = (INF p∈ set_walks. ereal (awalk_cost f (awalk_to_apath p)))" by (simp add: image_comp) also have "… ≤ (INF p∈ set_walks. ereal (awalk_cost f p))" proof - { fix p assume "p ∈ set_walks" then have "awalk u p v" by (auto simp: set_walks_def) then have "awalk_cost f (awalk_to_apath p) ≤ awalk_cost f p" using no_neg_cyc using no_neg_cyc and awalk_to_path_no_neg_cyc_cost by auto } then show ?thesis by (intro INF_mono) auto qed finally show "(INF p∈ set_paths. ereal (awalk_cost f p)) ≤ (INF p∈ set_walks. ereal (awalk_cost f p))" by simp have "set_paths ⊆ set_walks" unfolding set_paths_def set_walks_def by (auto simp: apath_def) then show "(INF p∈ set_walks. ereal (awalk_cost f p)) ≤ (INF p∈ set_paths. ereal (awalk_cost f p))" by (rule INF_superset_mono) simp qed also have "… ∈ (λp. ereal (awalk_cost f p)) ` set_paths" using apaths_finite ‹set_paths ≠ {}› by (intro finite_INF_in) (auto simp: set_paths_def) finally show ?thesis by (simp add: set_paths_def image_def) qed lemma (in fin_digraph) min_cost_awalk: assumes reach: "u →⇧^{*}v" assumes pos_cost: "⋀e. e ∈ arcs G ⟹ c e ≥ 0" shows "∃p. apath u p v ∧ μ c u v = awalk_cost c p" proof - have pc: "⋀u p v. awalk u p v ⟹ 0 ≤ awalk_cost c p" using pos_cost_pos_awalk_cost pos_cost by auto from reach show ?thesis by (rule no_neg_cyc_reach_imp_path) (auto simp: not_less intro: pc) qed lemma (in fin_digraph) pos_cost_mu_triangle: assumes pos_cost: "⋀e. e ∈ arcs G ⟹ c e ≥ 0" (* introduce predicate? *) assumes e_props: "arc_to_ends G e = (u,v)" "e ∈ arcs G" shows "μ c s v ≤ μ c s u + c e" proof cases assume "μ c s u = ∞" then show ?thesis by simp next assume "μ c s u ≠ ∞" then have "{p. awalk s p u} ≠ {}" unfolding μ_def by safe (simp add: top_ereal_def) then have "s →⇧^{*}u" by (simp add: reachable_awalk) with pos_cost obtain p where p_props: "apath s p u" and p_cost: "μ c s u = awalk_cost c p" by (metis min_cost_awalk) have "awalk u [e] v" using e_props by (auto simp: arc_to_ends_def awalk_simps) with ‹apath s p u› have "awalk s (p @ [e]) v" by (auto simp: apath_def awalk_appendI) then have "μ c s v ≤ awalk_cost c (p @ [e])" by (rule min_cost_le_walk_cost) also have "… ≤ awalk_cost c p + c e" by simp also have "… ≤ μ c s u + c e" using p_cost by simp finally show ?thesis . qed lemma (in fin_digraph) mu_exact_triangle: assumes "v ≠ s" assumes "s →⇧^{*}v" assumes nonneg_arcs: "⋀e. e ∈ arcs G ⟹ 0 ≤ c e" obtains u e where "μ c s v = μ c s u + c e" and "arc e (u,v)" proof - obtain p where p_path: "apath s p v" and p_cost: "μ c s v = awalk_cost c p" using assms by (metis min_cost_awalk) then obtain e p' where p'_props: "p = p' @ [e]" using ‹v ≠ s› by (cases p rule: rev_cases) (auto simp: apath_def) then obtain u where "awalk s p' u" "awalk u [e] v" using ‹apath s p v› by (auto simp: apath_def) then have mu_le: "μ c s v ≤ μ c s u + c e" and arc: "arc e (u,v)" using nonneg_arcs by (auto intro!: pos_cost_mu_triangle simp: arc_to_ends_def arc_def) have "μ c s u + c e ≤ ereal (awalk_cost c p') + ereal (c e)" using ‹awalk s p' u› by (fast intro: add_right_mono min_cost_le_walk_cost) also have "… = awalk_cost c p" using p'_props by simp also have "… = μ c s v" using p_cost by simp finally have "μ c s v = μ c s u + c e" using mu_le by auto then show ?thesis using arc .. qed lemma (in fin_digraph) mu_exact_triangle_Ex: assumes "v ≠ s" assumes "s →⇧^{*}v" assumes "⋀e. e ∈ arcs G ⟹ 0 ≤ c e" shows "∃u e. μ c s v = μ c s u + c e ∧ arc e (u,v)" using assms by (metis mu_exact_triangle) lemma (in fin_digraph) mu_Inf_triangle: assumes "v ≠ s" assumes "⋀e. e ∈ arcs G ⟹ 0 ≤ c e" shows "μ c s v = Inf {μ c s u + c e | u e. arc e (u, v)}" (is "_ = Inf ?S") proof cases assume "s →⇧^{*}v" then obtain u e where "μ c s v = μ c s u + c e" "arc e (u,v)" using assms by (metis mu_exact_triangle) then have "Inf ?S ≤ μ c s v" by (auto intro: Complete_Lattices.Inf_lower) also have "… ≤ Inf ?S" using assms(2) by (auto intro!: Complete_Lattices.Inf_greatest pos_cost_mu_triangle simp: arc_def arc_to_ends_def) finally show ?thesis by simp next assume "¬s →⇧^{*}v" then have "μ c s v = ∞" by (metis shortest_path_inf) define S where "S = ?S" show "μ c s v = Inf S" proof cases assume "S = {}" then show ?thesis unfolding ‹μ c s v = ∞› by (simp add: top_ereal_def) next assume "S ≠ {}" { fix x assume "x ∈ S" then obtain u e where "arc e (u,v)" and x_val: "x = μ c s u + c e" unfolding S_def by auto then have "¬s →⇧^{*}u" using ‹¬ s →⇧^{*}v› by (metis reachable_arc_trans) then have "μ c s u + c e= ∞" by (simp add: shortest_path_inf) then have "x = ∞" using x_val by simp } then have "S = {∞}" using ‹S ≠ {}› by auto then show ?thesis using ‹μ c s v = ∞› by (simp add: min_def) qed qed end end