Theory ShortestPathNeg

theory ShortestPathNeg

(*
  This theory uses the graph library and  
  several lemmas that were proven in the 
  shortest path theory
*)
imports ShortestPath

begin
section ‹Shortest Path (with general edge costs)›
(* 
  In this locale we assume we are given a 
  wellformed directed graph $G = (V,E)$ with 
  finite $V$ and $E$ (this is the assumption 
  $graphG$). Moreover, a source vertex $s$ in 
  $V$ . In addition, a cost function c, a function
 $num:V\to \Nat$, $parent\dash edge:V\to E \cup $*)
locale shortest_paths_locale_step1 = 
  fixes G :: "('a, 'b) pre_digraph" (structure)
  fixes s :: "'a"
  fixes c :: "'b ⇒ real"
  fixes num :: "'a ⇒ nat"
  fixes parent_edge :: "'a ⇒ 'b option"
  fixes dist :: "'a  ⇒ ereal"
  assumes graphG: "fin_digraph G"
  assumes s_assms: 
    "s ∈ verts G" 
    "dist s ≠ ∞" 
    "parent_edge s = None" 
    "num s = 0"
  assumes  parent_num_assms: 
    "⋀v.  ⟦v ∈ verts G; v ≠ s; dist v ≠ ∞⟧ ⟹
    (∃e ∈ arcs G. parent_edge v = Some e ∧ 
    head G e = v ∧ dist (tail G e) ≠ ∞ ∧
    num v  = num (tail G e) + 1)"
  assumes noPedge: "⋀e. e∈arcs G ⟹ 
    dist (tail G e) ≠ ∞ ⟹ dist (head G e) ≠ ∞"

sublocale shortest_paths_locale_step1 ⊆ fin_digraph G
  using graphG by auto

definition (in shortest_paths_locale_step1) enum :: "'a ⇒ enat" where
  "enum v = (if (dist v = ∞ ∨ dist v = - ∞) then ∞ else num v)"

locale shortest_paths_locale_step2 = 
  shortest_paths_locale_step1 +
  basic_just_sp G dist c s enum +
  assumes source_val: "(∃v ∈ verts G. enum v ≠ ∞) ⟹ dist s = 0"
  assumes no_edge_Vm_Vf: 
    "⋀e. e ∈ arcs G ⟹ dist (tail G e) = - ∞ ⟹ ∀ r. dist (head G e) ≠ ereal r"

function (in shortest_paths_locale_step1) pwalk :: "'a ⇒ 'b list" 
where
  "pwalk v = 
    (if (v = s ∨ dist v = ∞ ∨ v ∉ verts G)
      then [] 
      else pwalk (tail G (the (parent_edge v))) @ [the (parent_edge v)]
    )"
by auto 
termination (in shortest_paths_locale_step1) 
  using parent_num_assms
  by (relation "measure num", auto, fastforce)


lemma (in shortest_paths_locale_step1) pwalk_simps:
  "v = s ∨ dist v = ∞ ∨ v ∉ verts G ⟹ pwalk v = []"
  "v ≠ s ⟹ dist v ≠ ∞ ⟹ v ∈ verts G ⟹ 
    pwalk v = pwalk (tail G (the (parent_edge v))) @ [the (parent_edge v)]"
by auto

definition (in shortest_paths_locale_step1) pwalk_verts :: "'a  ⇒ 'a set" where 
  "pwalk_verts v = {u. u ∈ set (awalk_verts s (pwalk v))}" 

locale shortest_paths_locale_step3 =
  shortest_paths_locale_step2 +
  fixes C :: "('a ×('b awalk)) set"
  assumes C_se: 
    "C ⊆ {(u, p). dist u ≠ ∞ ∧ awalk u p u ∧ awalk_cost c p < 0}"
  assumes int_neg_cyc: 
    "⋀v. v ∈ verts G ⟹ dist v = -∞ ⟹ 
      (fst ` C) ∩ pwalk_verts v  ≠ {}"

locale shortest_paths_locale_step2_pred = 
  shortest_paths_locale_step1 +
  fixes pred :: "'a ⇒ 'b option" 
  assumes bj: "basic_just_sp_pred G dist c s enum pred" 
  assumes source_val: "(∃v ∈ verts G. enum v ≠ ∞) ⟹ dist s = 0"
  assumes no_edge_Vm_Vf: 
    "⋀e. e ∈ arcs G ⟹ dist (tail G e) = - ∞ ⟹ ∀ r. dist (head G e) ≠ ereal r"
(*
sublocale shortest_paths_locale_step2_pred ⊆ shortest_paths_locale_step2
using shortest_paths_locale_step2_pred_axioms 
unfolding shortest_paths_locale_step2_pred_def 
   shortest_paths_locale_step2_pred_axioms_def 
   shortest_paths_locale_step2_def 
   shortest_paths_locale_step2_axioms_def
try0
*)

lemma (in shortest_paths_locale_step1) num_s_is_min:
  assumes "v ∈ verts G"
  assumes "v ≠ s"
  assumes "dist v ≠ ∞"
  shows "num v > 0"
     using parent_num_assms[OF assms] by fastforce

lemma (in shortest_paths_locale_step1) path_from_root_Vr_ex:
  fixes v :: 'a
  assumes "v ∈ verts G"
  assumes "v ≠ s"
  assumes "dist v ≠ ∞"
  shows  "∃e. s →⇧* tail G e ∧
          e ∈ arcs G ∧ head G e = v ∧ dist (tail G e) ≠ ∞ ∧
          parent_edge v = Some e ∧ num v = num (tail G e) + 1"
using assms
proof(induct "num v - 1" arbitrary : v)
case 0
  obtain e where ee:
    "e ∈ arcs G" "head G e = v" "dist (tail G e) ≠ ∞" 
    "parent_edge v = Some e" "num v = num (tail G e) + 1"
    using parent_num_assms[OF 0(2-4)] by fast
  have "tail G e = s" 
    using num_s_is_min[OF tail_in_verts [OF ee(1)] _ ee(3)] 
    ee(5) 0(1) by auto
  then show ?case using ee by auto
next
case (Suc n')
  obtain e where ee:
    "e ∈ arcs G" "head G e = v" "dist (tail G e) ≠ ∞" 
    "parent_edge v = Some e" "num v = num (tail G e) + 1"
    using parent_num_assms[OF Suc(3-5)] by fast
  then have ss: "tail G e ≠ s"
    using num_s_is_min tail_in_verts
    Suc(2) s_assms(4) by force
  have nst: "n' = num (tail G e) - 1"
    using ee(5) Suc(2) by presburger
  obtain e' where reach: "s →⇧* tail G e'" and
    e': "e' ∈ arcs G" "head G e' = tail G e" "dist (tail G e') ≠ ∞"
    using Suc(1)[OF nst tail_in_verts[OF ee(1)] ss ee(3)] by blast
  then have "s →⇧* tail G e"
    by (metis arc_implies_awalk reachable_awalk reachable_trans)
  then show ?case using e' ee by auto
qed

lemma (in shortest_paths_locale_step1) path_from_root_Vr:
  fixes v :: 'a
  assumes "v ∈ verts G"
  assumes "dist v ≠ ∞"
  shows "s →⇧* v"
proof(cases "v = s")
case True thus ?thesis using assms by simp
next
case False
  obtain e where "s →⇧* tail G e" "e ∈ arcs G" "head G e = v"
      using path_from_root_Vr_ex[OF assms(1) False assms(2)] by blast
  then have "s →⇧* tail G e" "tail G e → v"
    by (auto intro: in_arcs_imp_in_arcs_ends)
  then show ?thesis by (rule reachable_adj_trans)
qed

lemma (in shortest_paths_locale_step1) μ_V_less_inf:
  fixes v :: 'a
  assumes "v ∈ verts G"
  assumes "dist v ≠ ∞"
  shows "μ c s v ≠ ∞"
  using assms path_from_root_Vr μ_reach_conv by force

lemma (in shortest_paths_locale_step2) enum_not0:
  assumes "v ∈ verts G"
  assumes "v ≠ s"
  assumes "enum v ≠ ∞"
  shows "enum v ≠ enat 0"
     using parent_num_assms[OF assms(1,2)] assms unfolding enum_def by auto

lemma (in shortest_paths_locale_step2) dist_Vf_μ:
  fixes v :: 'a
  assumes vG: "v ∈ verts G"
  assumes "∃r. dist v = ereal r"
  shows "dist v = μ c s v"
proof -
  have ds: "dist s =  0" 
    using assms source_val unfolding enum_def by force
  have ews:"awalk s [] s" 
    using s_assms(1) unfolding awalk_def by simp
  have mu: "μ c s s = ereal 0" 
    using min_cost_le_walk_cost[OF ews, where c=c] 
    awalk_cost_Nil ds  dist_le_μ[OF s_assms(1)] zero_ereal_def
    by simp
  thus ?thesis 
    using ds assms dist_le_μ[OF vG] 
    dist_ge_μ[OF vG _ _ mu ds enum_not0]
    unfolding enum_def by fastforce
qed

lemma (in shortest_paths_locale_step1) pwalk_awalk:
  fixes v :: 'a
  assumes "v ∈ verts G"
  assumes "dist v ≠ ∞"
  shows "awalk s (pwalk v) v" 
proof (cases "v=s")
case True
  thus ?thesis 
    using assms pwalk.simps[where v=v] 
    awalk_Nil_iff by presburger 
next
case False
  from assms show ?thesis 
  proof (induct rule: pwalk.induct)
    fix v 
    let ?e = "the (parent_edge v)"
    let ?u = "tail G ?e"
    assume ewu: "¬ (v = s ∨ dist v = ∞ ∨ v ∉ verts G) ⟹ 
                 ?u ∈ verts G ⟹ dist ?u ≠ ∞ ⟹ 
                 awalk s (pwalk ?u) ?u"
    assume vG: "v ∈ verts G" 
    assume dv: "dist v ≠ ∞"
    thus "awalk s (pwalk v) v "
    proof (cases "v = s ∨ dist v = ∞ ∨ v ∉ verts G")
    case True
      thus ?thesis 
        using pwalk.simps vG dv 
        awalk_Nil_iff by fastforce
    next
    case False
      obtain e  where ee:
        "e ∈arcs G" 
        "parent_edge v = Some e" 
        "head G e = v" 
        "dist (tail G e) ≠ ∞" 
        using parent_num_assms False by blast
      hence "awalk s (pwalk ?u) ?u"
        using ewu[OF False] tail_in_verts by simp
      hence "awalk s (pwalk (tail G e) @ [e]) v"
        using ee(1-3) vG
        by (auto simp: awalk_simps simp del: pwalk.simps)
      also have "pwalk (tail G e) @ [e] = pwalk v"
        using False ee(2) unfolding pwalk.simps[where v=v] by auto
      finally show ?thesis .
    qed
  qed
qed

lemma (in shortest_paths_locale_step3) μ_ninf:
  fixes v :: 'a
  assumes "v ∈ verts G"
  assumes "dist v = - ∞"
  shows "μ c s v = - ∞"
proof -
  have "awalk s (pwalk v) v"
    using pwalk_awalk assms by force
moreover
  obtain w where ww: "w ∈ fst ` C ∩ pwalk_verts v"
    using int_neg_cyc[OF assms] by blast
  then obtain q where 
     "awalk w q w" 
     "awalk_cost c q < 0"
     using C_se by auto
moreover 
  have "w ∈ set (awalk_verts s (pwalk v))"
    using ww unfolding pwalk_verts_def by fast
ultimately
  show ?thesis using  neg_cycle_imp_inf_μ by force
qed

lemma (in shortest_paths_locale_step3) correct_shortest_path:
  fixes v :: 'a
  assumes "v ∈ verts G"
  shows "dist v = μ c s v"
proof(cases "dist v")
show " ⋀r. dist v = ereal r ⟹ dist v = μ c s v"
  using dist_Vf_μ[OF assms] by simp 
next
show "dist v = ∞ ⟹ dist v = μ c s v"
  using μ_V_less_inf[OF assms] 
  dist_le_μ[OF assms] by simp
next
show "dist v = -∞ ⟹ dist v = μ c s v"
  using μ_ninf[OF assms] by simp
qed

end