Theory Graph_Theory.Shortest_Path

(* 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