Theory Shortest_Path
theory Shortest_Path imports
Arc_Walk
Weighted_Graph
"HOL-Library.Extended_Real"
begin
section ‹Shortest Paths›
context wf_digraph begin
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"
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