Theory Directed_Graph

section ‹Weighted Directed Graphs›
theory Directed_Graph
imports Common
begin

text ‹
  A weighted graph is represented by a function from edges to weights.

  For simplicity, we use @{typ enat} as weights, @{term ‹∞›} meaning 
  that there is no edge.
›

type_synonym ('v) wgraph = "('v × 'v) ⇒ enat"

text ‹We encapsulate weighted graphs into a locale that fixes a graph›
locale WGraph = fixes w :: "'v wgraph"
begin
text ‹Set of edges with finite weight›
definition "edges ≡ {(u,v) . w (u,v) ≠ ∞}"

subsection ‹Paths›
text ‹A path between nodes ‹u› and ‹v› is a list of edge weights
  of a sequence of edges from ‹u› to ‹v›.
  
  Note that a path may also contain edges with weight ‹∞›.
›

fun path :: "'v ⇒ enat list ⇒ 'v ⇒ bool" where
  "path u [] v ⟷ u=v"
| "path u (l#ls) v ⟷ (∃uh. l = w (u,uh) ∧ path uh ls v)"

lemma path_append[simp]: 
  "path u (ls1@ls2) v ⟷ (∃w. path u ls1 w ∧ path w ls2 v)"
  by (induction ls1 arbitrary: u) auto

text ‹There is a singleton path between every two nodes 
  (it's weight might be ‹∞›).›  
lemma triv_path: "path u [w (u,v)] v" by auto
  
text ‹Shortcut for the set of all paths between two nodes›    
definition "paths u v ≡ {p . path u p v}"

lemma paths_ne: "paths u v ≠ {}" using triv_path unfolding paths_def by blast

text ‹If there is a path from a node inside a set ‹S›, to a node outside 
  a set ‹S›, this path must contain an edge from inside ‹S› to outside ‹S›.
›
lemma find_leave_edgeE:
  assumes "path u p v"
  assumes "u∈S" "v∉S"
  obtains p1 x y p2 
    where "p = p1@w (x,y)#p2" "x∈S" "y∉S" "path u p1 x" "path y p2 v"
proof -
  have "∃p1 x y p2. p = p1@w (x,y)#p2 ∧ x∈S ∧ y∉S ∧ path u p1 x ∧ path y p2 v"
    using assms
  proof (induction p arbitrary: u)
    case Nil
    then show ?case by auto
  next
    case (Cons a p)
    from Cons.prems obtain x where [simp]: "a=w (u,x)" and PX: "path x p v" 
      by auto
    
    show ?case proof (cases "x∈S")
      case False with PX ‹u∈S› show ?thesis by fastforce
    next
      case True from Cons.IH[OF PX True ‹v∉S›] show ?thesis
        by clarsimp (metis WGraph.path.simps(2) append_Cons)
    qed
  qed
  thus ?thesis by (fast intro: that) 
qed

subsection ‹Distance›

text ‹The (minimum) distance between two nodes ‹u› and ‹v› is called ‹δ u v›.›

definition "δ u v ≡ LEAST w::enat. w∈sum_list`paths u v"

lemma obtain_shortest_path: 
  obtains p where "path s p u" "δ s u = sum_list p"
  unfolding δ_def using paths_ne
  by (smt Collect_empty_eq LeastI_ex WGraph.paths_def imageI image_iff 
          mem_Collect_eq paths_def)

lemma shortest_path_least:  
  "path s p u ⟹ δ s u ≤ sum_list p"
  unfolding δ_def paths_def
  by (simp add: Least_le)

lemma distance_refl[simp]: "δ s s = 0"
  using shortest_path_least[of s "[]" s] by auto
  
lemma distance_direct: "δ s u ≤ w (s, u)"  
  using shortest_path_least[of s "[w (s,u)]" u] by auto

text ‹Triangle inequality: The distance from ‹s› to ‹v› is shorter than 
  the distance from ‹s› to ‹u› and the edge weight from ‹u› to ‹v›. ›  
lemma triangle: "δ s v ≤ δ s u + w (u,v)"
proof -
  have "path s (p@[w (u,v)]) v" if "path s p u" for p using that by auto
  then have "(+) (w (u,v)) ` sum_list ` paths s u ⊆ sum_list ` paths s v"
    by (fastforce simp: paths_def image_iff simp del: path.simps path_append) 
  from least_antimono[OF _ this] paths_ne have 
    "(LEAST y::enat. y ∈ sum_list ` paths s v) 
    ≤ (LEAST x::enat. x ∈ (+) (w (u,v)) ` sum_list ` paths s u)"
    by (auto simp: paths_def)
  also have "… = (LEAST x. x ∈ sum_list ` paths s u) + w (u,v)"
    apply (subst Least_mono[of "(+) (w (u,v))" "sum_list`paths s u"])
    subgoal by (auto simp: mono_def)
    subgoal by simp (metis paths_def mem_Collect_eq 
                          obtain_shortest_path shortest_path_least)
    subgoal by auto
    done
  finally show ?thesis unfolding δ_def .
qed
  
text ‹Any prefix of a shortest path is a shortest path itself.
  Note: The ‹< ∞› conditions are required to avoid saturation in adding to ‹∞›!
›
lemma shortest_path_prefix:
  assumes "path s p⇩1 x" "path x p⇩2 u" 
  and DSU: "δ s u = sum_list p⇩1 + sum_list p⇩2" "δ s u < ∞"
  shows "δ s x = sum_list p⇩1" "δ s x < ∞"
proof -  
  have "δ s x ≤ sum_list p⇩1" using assms shortest_path_least by blast
  moreover have "¬δ s x < sum_list p⇩1" proof
    assume "δ s x < sum_list p⇩1"
    then obtain p⇩1' where "path s p⇩1' x" "sum_list p⇩1' < sum_list p⇩1"
      by (auto intro: obtain_shortest_path[of s x])
    with ‹path x p⇩2 u› shortest_path_least[of s "p⇩1'@p⇩2" u] DSU show False
      by fastforce
  qed
  ultimately show "δ s x = sum_list p⇩1" by auto
  with DSU show "δ s x < ∞" using le_iff_add by fastforce
qed  
  
      
end

end