Theory Flow_Networks.Graph

section ‹Directed Graphs›
theory Graph
imports Main
begin
text ‹
  We define a specialized graph library for graphs that are induced by 
  capacity matrices.
›

lemma finite_Image: fixes R shows " finite R   finite (R `` A)"
  by (meson Image_iff finite_Range Range.intros finite_subset subsetI)

lemma map_eq_appendE: 
  assumes "map f ls = fl@fl'"
  obtains l l' where "ls=l@l'" and "map f l=fl" and  "map f l' = fl'"
using that[of "take (length fl) ls" "drop (length fl) ls"] assms 
by(simp add: take_map[symmetric] drop_map[symmetric])

subsection ‹Definitions›

subsubsection ‹Basic Definitions›
text ‹
  We fix the nodes to be natural numbers.
›  
  type_synonym node = nat 
  type_synonym edge = "node × node"

text ‹
  The capacities are left polymorphic, however, they
  are restricted to linearly ordered domains.
›
type_synonym 'capacity graph = "edge  'capacity"
  
locale Graph = fixes c :: "'capacity::linordered_idom graph"
begin
definition E :: "edge set" ― ‹Edges of the graph›
where "E  {(u, v). c (u, v)  0}"

definition V :: "node set" ― ‹Nodes of the graph. Exactly the nodes 
  that have adjacent edges.›
where "V  {u. v. (u, v)  E  (v, u)  E}"

definition incoming :: "node  edge set" ― ‹Incoming edges into a node›
where "incoming v  {(u, v) | u. (u, v)  E}"

definition outgoing :: "node  edge set" ― ‹Outgoing edges from a node›
where "outgoing v  {(v, u) | u. (v, u)  E}"
  
definition adjacent :: "node  edge set" ― ‹Adjacent edges of a node›
where "adjacent v  incoming v  outgoing v"

definition incoming' :: "node set  edge set" ― ‹Incoming edges into 
  a set of nodes›
where "incoming' k  {(u, v) | u v. u  k  v  k  (u, v)  E}"
  
definition outgoing' :: "node set  edge set" ― ‹Outgoing edges from 
  a set of nodes›
where "outgoing' k  {(v, u) | u v. u  k  v  k  (v, u)  E}"
  
definition adjacent' :: "node set  edge set" ― ‹Edges adjacent to a 
  set of nodes›
where "adjacent' k  incoming' k  outgoing' k"

definition is_adj_map :: "(node  node list)  bool" where
  "is_adj_map ps  (u. distinct (ps u)  set (ps u) = E``{u}  E¯``{u})"

definition "adjacent_nodes u  E``{u}  E¯``{u}"
  
  
end ― ‹Graph›

subsubsection ‹Finite Graphs›
locale Finite_Graph = Graph +
  assumes finite_V[simp, intro!]: "finite V"

subsubsection ‹Paths›
type_synonym path = "edge list"

context Graph
begin
  fun isPath :: "node  path  node  bool" 
  where
    "isPath u [] v  u = v"
  | "isPath u ((x,y)#p) v  u = x  (x, y)  E  isPath y p v"

  fun pathVertices :: "node  path  node list"
  where
    "pathVertices u [] = [u]"
  | "pathVertices u (e # es) = fst e # (pathVertices (snd e) es)"
  
  (* TODO: This characterization is probably nicer to work with! Exchange! *)
  definition (in Graph) pathVertices_fwd :: "node  edge list  node list" 
    where "pathVertices_fwd u p = u#map snd p"

  lemma (in Graph) pathVertices_fwd: 
    assumes "isPath u p v"
    shows "pathVertices u p = pathVertices_fwd u p"
    unfolding pathVertices_fwd_def
    using assms apply (induction p arbitrary: u)
    by auto


  definition connected :: "node  node  bool" 
    where "connected u v  p. isPath u p v" 
  
  abbreviation (input) "isReachable  connected" (* Deprecated *)

  definition reachableNodes :: "node  node set"  
    where "reachableNodes u  {v. connected u v}"
  
  definition isShortestPath :: "node  path  node  bool" 
    where "isShortestPath u p v 
     isPath u p v  (p'. isPath u p' v  length p  length p')"
      
  definition isSimplePath :: "node  path  node  bool" 
    where "isSimplePath u p v  isPath u p v  distinct (pathVertices u p)"

  definition dist :: "node  nat  node  bool" 
    ― ‹There is a path of given length between the nodes›
    where "dist v d v'  p. isPath v p v'  length p = d"

  definition min_dist :: "node  node  nat"
    ― ‹Minimum distance between two connected nodes›
    where "min_dist v v' = (LEAST d. dist v d v')"

end  


subsection ‹Properties›

subsubsection ‹Basic Properties›
context Graph
begin

lemma V_alt: "V = fst`E  snd`E" unfolding V_def by force

lemma E_ss_VxV: "E  V×V" by (auto simp: V_def)

lemma adjacent_nodes_ss_V: "adjacent_nodes u  V"  
  unfolding adjacent_nodes_def using E_ss_VxV by auto
    
lemma Vfin_imp_Efin[simp, intro]: assumes "finite V" shows "finite E"
  using E_ss_VxV assms by (auto intro: finite_subset)

lemma Efin_imp_Vfin: "finite E  finite V"
  unfolding V_alt by auto

lemma zero_cap_simp[simp]: "(u,v)E  c (u,v) = 0"  
  by (auto simp: E_def)

lemma succ_ss_V: "E``{u}  V" by (auto simp: V_def)

lemma pred_ss_V: "E¯``{u}  V" by (auto simp: V_def)


lemma 
  incoming_edges: "incoming u  E" and
  outgoing_edges: "outgoing u  E" and
  incoming'_edges: "incoming' U  E" and
  outgoing'_edges: "outgoing' U  E"
  by (auto simp: incoming_def outgoing_def incoming'_def outgoing'_def)
  
lemma 
  incoming_alt: "incoming u = (λv. (v,u))`(E¯``{u})" and
  outgoing_alt: "outgoing u = Pair u`(E``{u})"
  by (auto simp: incoming_def outgoing_def)

lemma 
  finite_incoming[simp, intro]: "finite V  finite (incoming u)" and
  finite_outgoing[simp, intro]: "finite V  finite (outgoing u)"
  by (auto simp: incoming_alt outgoing_alt intro: finite_Image)

lemma 
  finite_incoming'[simp, intro]: "finite V  finite (incoming' U)" and
  finite_outgoing'[simp, intro]: "finite V  finite (outgoing' U)"
  by (auto 
    intro: finite_subset[OF incoming'_edges] 
    intro: finite_subset[OF outgoing'_edges])
  
subsubsection ‹Summations over Edges and Nodes›  
text ‹We provide useful alternative characterizations for summation over 
    all incoming or outgoing edges.›
lemma sum_outgoing_pointwise: "(eoutgoing u. g e) = (vE``{u}. g (u,v))"  
proof -
  have "(eoutgoing u. g e) = (e(λv. (u,v))`(E``{u}). g e)"  
    by (rule sum.cong) (auto simp: outgoing_def)
  also have " = (vE``{u}. g (u,v))"  
    by (subst sum.reindex)(auto simp add: inj_on_def)
  finally show ?thesis .
qed  

lemma sum_incoming_pointwise: "(eincoming u. g e) = (vE¯``{u}. g (v,u))"  
proof -
  have "(eincoming u. g e) = (e(λv. (v,u))`(E¯``{u}). g e)"  
    by (rule sum.cong) (auto simp: incoming_def)
  also have " = (vE¯``{u}. g (v,u))"  
    by (subst sum.reindex)(auto simp add: inj_on_def)
  finally show ?thesis .
qed  

text ‹Extend summations over incoming/outgoing edges to summations over
  all nodes, provided the summed-up function is zero for non-edges.›
lemma (in Finite_Graph) sum_incoming_extend:  
  assumes "v.  vV; (v,u)E   g (v,u) = 0"
  shows "(eincoming u. g e) = (vV. g (v,u))"
  apply (subst sum_incoming_pointwise)
  apply (rule sum.mono_neutral_left)
  using assms pred_ss_V by auto

lemma (in Finite_Graph) sum_outgoing_extend:  
  assumes "v.  vV; (u,v)E   g (u,v) = 0"
  shows "(eoutgoing u. g e) = (vV. g (u,v))"
  apply (subst sum_outgoing_pointwise)
  apply (rule sum.mono_neutral_left)
  using assms succ_ss_V by auto

text ‹When summation is done over something that satisfies the capacity 
  constraint, e.g., a flow, the summation can be extended to all 
  outgoing/incoming edges, as the additional edges must have zero capacity.›
(* TODO: Historical lemmas. Get rid of ∀ quantifier. *)
lemma (in Finite_Graph) sum_outgoing_alt: "e. 0  g e  g e  c e 
  v  V. (e  outgoing v. g e) = (u  V. g (v, u))"
  apply (rule ballI)
  apply (rule sum_outgoing_extend)
  apply clarsimp
  by (metis antisym zero_cap_simp)
  
lemma (in Finite_Graph) sum_incoming_alt: "e. 0  g e  g e  c e 
  v  V. (e  incoming v. g e) = (u  V. g (u, v))"
  apply (rule ballI)
  apply (rule sum_incoming_extend)
  apply clarsimp
  by (metis antisym zero_cap_simp)


subsubsection ‹Finite Graphs›

lemma (in Finite_Graph) finite_E[simp,intro!]: "finite E" by simp

lemma (in Graph) Finite_Graph_EI: "finite E  Finite_Graph c"
  apply unfold_locales
  by (rule Efin_imp_Vfin)
  
lemma (in Finite_Graph) adjacent_nodes_finite[simp, intro!]: "finite (adjacent_nodes u)"
  unfolding adjacent_nodes_def by (auto intro: finite_Image)
    
subsubsection ‹Paths›

named_theorems split_path_simps ‹Simplification lemmas to split paths›

lemma transfer_path:
  ― ‹Transfer path to another graph›
  assumes "set pE  Graph.E c'"
  assumes "isPath u p v"
  shows "Graph.isPath c' u p v"
  using assms
  apply (induction u p v rule: isPath.induct)
  apply (auto simp: Graph.isPath.simps)
  done

lemma isPath_append[split_path_simps]: 
  "isPath u (p1 @ p2) v  (w. isPath u p1 w  isPath w p2 v)"  
  by (induction p1 arbitrary: u) auto 
  
lemma isPath_head[split_path_simps]: 
  "isPath u (e#p) v  fst e = u  e  E  isPath (snd e) p v"
  by (cases e) auto

lemma isPath_head2: 
  "isPath u (e#p) v  (p = []  (p  []  fst (hd p) = snd e))"
  by (metis Graph.isPath_head list.collapse)
  
lemma isPath_tail: 
  "isPath u (p@[e]) v  isPath u p (fst e)  e  E  snd e = v"
  by (induction p) (auto simp: isPath_append isPath_head)

lemma isPath_tail2: 
  "isPath u (p@[e]) v  (p = []  (p  []  snd (last p) = fst e))"
  by (metis Graph.isPath_tail append_butlast_last_id)
      
(* TODO: Really needed? *)  
lemma isPath_append_edge: 
  "isPath v p v'  (v',v'')E  isPath v (p@[(v',v'')]) v''"  
  by (auto simp: isPath_append)

lemma isPath_edgeset: "isPath u p v; e  set p  e  E"
  using E_def 
  by (metis isPath_head isPath_append in_set_conv_decomp_first)
  
lemma isPath_rtc: "isPath u p v  (u, v)  E*"
proof (induction p arbitrary: u)
  case Nil
  thus ?case by auto
next
  case (Cons e es)
  obtain u1 u2 where "e = (u1, u2)" apply (cases e) by auto
  then have "u = u1  isPath u2 es v  (u1, u2)  E"
    using isPath.simps(2) Cons.prems by auto
  then have "(u, u2)  E" and "(u2, v)  E*" using Cons.IH by auto
  thus ?case by auto 
qed
  
lemma rtc_isPath: "(u, v)  E*  (p. isPath u p v)"
proof (induction rule: rtrancl.induct)
  case (rtrancl_refl a)
  have "isPath a [] a" by simp
  thus ?case by blast
next
  case (rtrancl_into_rtrancl u u' v)
  then obtain p1 where "isPath u p1 u'" by blast
  moreover have "(u', v)  E" using rtrancl_into_rtrancl.hyps(2) by simp
  ultimately have "isPath u (p1 @ [(u', v)]) v" using isPath_tail by simp
  thus ?case by blast
qed
    
lemma rtci_isPath: "(v, u)  (E¯)*  (p. isPath u p v)"
proof -
  assume "(v,u)(E¯)*" 
  hence "(u,v)E*" by (rule rtrancl_converseD)
  thus ?thesis by (rule rtc_isPath)
qed      
  
lemma isPath_ex_edge1: 
  assumes "isPath u p v"
  assumes "(u1, v1)  set p"
  assumes "u1  u"
  shows "u2. (u2, u1)  set p"
proof -
  obtain w1 w2 where obt1: "p = w1 @ [(u1, v1)] @ w2" using assms(2)
    by (metis append_Cons append_Nil in_set_conv_decomp_first)
  then have "isPath u w1 u1" using assms(1) isPath_append by auto
  have "w1  []"
    proof (rule ccontr)
      assume "¬ w1  []"
      then have "u = u1" using isPath u w1 u1 by (metis isPath.simps(1))
      thus "False" using assms(3) by blast
    qed
  then obtain e w1' where obt2:"w1 = w1' @ [e]" by (metis append_butlast_last_id)
  then obtain u2 where "e = (u2, u1)" 
    using isPath u w1 u1 isPath_tail by (metis prod.collapse)
  then have "p = w1' @ (u2, u1) # (u1, v1) # w2" using obt1 obt2 by auto 
  thus ?thesis by auto
qed

lemma isPath_ex_edge2: 
  assumes "isPath u p v"
  assumes "(u1, v1)  set p"
  assumes "v1  v"
  shows "v2. (v1, v2)  set p"
proof -
  obtain w1 w2 where obt1: "p = w1 @ [(u1, v1)] @ w2" using assms(2)
    by (metis append_Cons append_Nil in_set_conv_decomp_first)
  then have "isPath v1 w2 v" using assms(1) isPath_append by auto
  have "w2  []"
    proof (rule ccontr)
      assume "¬ w2  []"
      then have "v = v1" using isPath v1 w2 v by (metis isPath.simps(1))
      thus "False" using assms(3) by blast
    qed
  then obtain e w2' where obt2:"w2 =  e # w2'" by (metis neq_Nil_conv)
  then obtain v2 where "e = (v1, v2)" 
    using isPath v1 w2 v isPath_head by (metis prod.collapse)
  then have "p = w1 @ (u1, v1) # (v1, v2) # w2'" using obt1 obt2 by auto
  thus ?thesis by auto
qed

subsubsection ‹Vertices of Paths›

lemma (in Graph) pathVertices_fwd_simps[simp]: 
  "pathVertices_fwd s ([]) = [s]"  
  "pathVertices_fwd s (e#p) = s#pathVertices_fwd (snd e) p"  
  "pathVertices_fwd s (p@[e]) = pathVertices_fwd s p@[snd e]"
  "pathVertices_fwd s (p1@e#p2) 
    = pathVertices_fwd s p1 @ pathVertices_fwd (snd e) p2"
  "sset (pathVertices_fwd s p)"
  by (auto simp: pathVertices_fwd_def)

lemma pathVertices_alt: "p  [] 
     pathVertices u p = map fst p @ [snd (last p)]"
  by (induction p arbitrary: u) auto

lemma pathVertices_singleton_iff[simp]: "pathVertices s p = [u]  (p=[]  s=u)"
  apply (cases p rule: rev_cases)
  apply (auto simp: pathVertices_alt)
  done

lemma length_pathVertices_eq[simp]: "length (pathVertices u p) = length p + 1"
  apply (cases "p=[]")
  apply (auto simp: pathVertices_alt)
  done

lemma pathVertices_edgeset: "uV; isPath u p v  set (pathVertices u p)  V"
  apply (cases p rule: rev_cases; simp)
  using isPath_edgeset[of u p v]
  apply (fastforce simp: pathVertices_alt V_def)
  done

lemma pathVertices_append: "pathVertices u (p1 @ p2) = 
butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2"
proof (induction p1 arbitrary: u)
  case Nil
    thus ?case by auto
next
  case (Cons e es)
  have "pathVertices u ((e # es) @ p2) =  fst e # pathVertices (snd e) (es @ p2)"
    by (metis Graph.pathVertices.simps(2) append_Cons)
  moreover have "pathVertices (snd e) (es @ p2) 
    = butlast (pathVertices (snd e) es) 
      @ pathVertices (last (pathVertices (snd e) es)) p2" 
    using Cons.IH by auto
  moreover have "fst e # butlast (pathVertices (snd e) es) = 
    butlast (fst e # pathVertices (snd e) es)" 
    by (metis Graph.pathVertices.simps(1)
        Graph.pathVertices_alt Nil_is_append_conv butlast.simps(2) 
        list.distinct(1))
  moreover have "fst e # pathVertices (snd e) es = pathVertices u (e # es)"
    by (metis Graph.pathVertices.simps(2))
  moreover have "last (pathVertices (snd e) es) = last (pathVertices u (e # es))"
    by (metis Graph.pathVertices.simps(1) Graph.pathVertices_alt 
    last.simps last_snoc list.distinct(1))
  ultimately show ?case by (metis append_Cons)
qed

lemma split_path_at_vertex: 
  assumes "uset (pathVertices_fwd s p)"
  assumes "isPath s p t"
  obtains p1 p2 where "p=p1@p2" "isPath s p1 u" "isPath u p2 t"
  using assms
  apply -
  (*unfolding pathVertices_fwd*)
  unfolding pathVertices_fwd_def
  apply (auto simp: in_set_conv_decomp isPath_append) 
  apply force
  by (metis Graph.isPath_append_edge append_Cons append_Nil append_assoc)


lemma split_path_at_vertex_complete: 
  assumes "isPath s p t" "pathVertices_fwd s p = pv1@u#pv2" 
  obtains p1 p2 where 
    "p=p1@p2" 
    "isPath s p1 u" "pathVertices_fwd s p1 = pv1@[u]" 
    "isPath u p2 t" "pathVertices_fwd u p2 = u#pv2" 
proof -
  from assms have PV: "pathVertices s p = pv1@u#pv2" 
    by (simp add: pathVertices_fwd)
  then obtain p1 p2 where 
    "p=p1@p2" 
    "isPath s p1 u" "pathVertices s p1 = pv1@[u]" 
    "isPath u p2 t" "pathVertices u p2 = u#pv2"
  proof -
    show thesis
    using assms(1) PV
    apply (cases p rule: rev_cases; clarsimp simp: pathVertices_alt)
      apply (rule that[of "[]" "[]"]; simp add: Cons_eq_append_conv)

      apply (cases pv2; clarsimp)
      apply (rule that[of p "[]"]; 
        auto simp add: isPath_append pathVertices_alt
      )  
      apply (clarsimp simp: append_eq_append_conv2;
        auto elim!: map_eq_appendE append_eq_Cons_conv[THEN iffD1, elim_format]
            simp: isPath_append)
      subgoal for … l
        apply (erule that) 
        apply auto [4]
        apply (case_tac l rule: rev_cases; 
          auto simp add: pathVertices_alt isPath_append)
        done

      subgoal for … l
        apply (erule that) 
        apply auto [4]
        apply (case_tac l rule: rev_cases; 
          auto simp add: pathVertices_alt isPath_append)
        done

      subgoal for … l u1 u2 u3
        apply (erule that)  
        apply auto [4]
        apply (case_tac l rule: rev_cases; 
          auto simp add: pathVertices_alt isPath_append)
        apply (auto simp: isPath_append) []
        apply (auto simp: pathVertices_alt) []
        done
        
        apply (erule that) apply(auto simp add: Cons_eq_append_conv) [4]
        subgoal for … l
          by (case_tac l rule: rev_cases; 
            auto simp add: pathVertices_alt isPath_append)
      done
  qed
  thus ?thesis apply - unfolding pathVertices_fwd using that .
qed

lemma isPath_fwd_cases: 
  assumes "isPath s p t"
  obtains "p=[]" "t=s"
    | p' u where "p=(s,u)#p'" "(s,u)E" "isPath u p' t"
    using assms by (cases p) (auto)

lemma isPath_bwd_cases: 
  assumes "isPath s p t"
  obtains "p=[]" "t=s"
    | p' u where "p=p'@[(u,t)]" "isPath s p' u" "(u,t)E"
    using assms by (cases p rule: rev_cases) (auto simp: split_path_simps)


lemma pathVertices_edge: "isPath s p t  e  set p  
  vs1 vs2. pathVertices_fwd s p = vs1 @ fst e # snd e # vs2"
  apply (cases e)
  apply (auto simp: in_set_conv_decomp split_path_simps)
  apply (erule isPath_bwd_cases[where s=s]; auto)
  apply (erule isPath_fwd_cases[where t=t]; auto)
  apply (erule isPath_fwd_cases[where t=t]; auto)
  done  


(* TODO: Really needed? *)
lemma pathVertices_edge_old: "isPath u p v  e  set p  
  vs1 vs2. pathVertices u p = vs1 @ fst e # snd e # vs2"
  unfolding pathVertices_fwd
  by (rule pathVertices_edge)

subsubsection ‹Reachability›

lemma connected_refl[simp, intro!]: "connected v v" 
  unfolding connected_def by (force intro: exI[where x="[]"])

lemma connected_append_edge: "connected u v  (v,w)E  connected u w"
  unfolding connected_def by (auto intro: isPath_append_edge)

lemma connected_inV_iff: "connected u v  vV  uV"
  apply (auto simp: connected_def)
  apply (case_tac p; auto simp: V_def) []
  apply (case_tac p rule: rev_cases; auto simp: isPath_append V_def) []
  done

lemma connected_edgeRtc: "connected u v  (u, v)  E*"  
  using isPath_rtc rtc_isPath
  unfolding connected_def by blast

lemma reachable_ss_V: "s  V  reachableNodes s  V"
proof
  assume asm: "s  V"
  fix x
  assume "x  reachableNodes s"
  then obtain p where "x  {v. isPath s p v}"
    unfolding reachableNodes_def connected_def by blast
  thus "x  V" using asm
    by (induction p arbitrary: s) (auto simp: isPath_head V_alt) 
qed

lemma reachableNodes_E_closed: "E``reachableNodes s  reachableNodes s"  
  unfolding reachableNodes_def by (auto intro: connected_append_edge)

corollary reachableNodes_append_edge: 
  "ureachableNodes s  (u,v)E  vreachableNodes s"
  using reachableNodes_E_closed by blast


subsubsection ‹Simple Paths›

lemma isSimplePath_fwd: "isSimplePath s p t 
   isPath s p t  distinct (pathVertices_fwd s p)"  
  by (auto simp: isSimplePath_def pathVertices_fwd)

lemma isSimplePath_singelton[split_path_simps]: 
  "isSimplePath u [e] v  (e=(u,v)  uv  (u,v)E)"
  by (auto simp: isSimplePath_def isPath_head)

lemma (in Graph) isSimplePath_append[split_path_simps]: 
  "isSimplePath s (p1@p2) t 
     (u. 
      isSimplePath s p1 u 
     isSimplePath u p2 t 
     set (pathVertices_fwd s p1)  set (pathVertices_fwd u p2) = {u})"  
  (is "_  ?R")
  unfolding isSimplePath_fwd
  apply (cases p1 rule: rev_cases; simp; cases p2; simp)
  by (auto simp: split_path_simps)
  
lemma (in Graph) isSimplePath_cons[split_path_simps]: 
  "isSimplePath s (e#p) t 
   (u. e=(s,u)  su  (s,u)E 
         isSimplePath u p t  sset (pathVertices_fwd u p))"
  using isSimplePath_append[of s "[e]" p t, simplified]
  by (auto simp: split_path_simps)

lemma (in Finite_Graph) simplePath_length_less_V:
  assumes UIV: "uV"
  assumes P: "isSimplePath u p v" 
  shows "length p < card V"
proof -
  from P have 1: "isPath u p v" and 2: "distinct (pathVertices u p)"
    by (auto simp: isSimplePath_def)
  from pathVertices_edgeset[OF UIV 1] have "set (pathVertices u p)  V" .
  with 2 finite_V have "length (pathVertices u p)  card V"
    using distinct_card card_mono by metis
  hence "length p + 1  card V" by simp
  thus ?thesis by auto
qed      

lemma split_simple_path: "isSimplePath u (p1@p2) v 
   (w. isSimplePath u p1 w  isSimplePath w p2 v)"
  apply (auto simp: isSimplePath_def isPath_append)
  apply (rule exI; intro conjI; assumption?)
  apply (cases p1 rule: rev_cases) []
  apply simp
  apply (cases p2)
  apply simp
  apply (clarsimp simp: pathVertices_alt isPath_append)

  apply (cases p1 rule: rev_cases) []
  apply simp
  apply (cases p2  rule: rev_cases)
  apply simp
  apply (clarsimp simp: pathVertices_alt isPath_append)
  done  
      
lemma simplePath_empty_conv[simp]: "isSimplePath s [] t  s=t"
  by (auto simp: isSimplePath_def)

lemma simplePath_same_conv[simp]: "isSimplePath s p s  p=[]"  
  apply rule
  apply (cases p; simp)
  apply (rename_tac e pp)
  apply (case_tac pp rule: rev_cases; simp)
  apply (auto simp: isSimplePath_def pathVertices_alt isPath_append) [2]
  apply simp
  done

lemma isSPath_pathLE: "isPath s p t  p'. isSimplePath s p' t"
proof (induction p rule: length_induct)
  case (1 p)
  hence IH: "p'. length p' < length p; isPath s p' t 
     p'. isSimplePath s p' t"
    and PATH: "isPath s p t"
    by auto

  show "p. isSimplePath s p t"  
  proof cases
    assume "distinct (pathVertices_fwd s p)"
    thus ?thesis using PATH by (auto simp: isSimplePath_fwd)
  next
    assume "¬(distinct (pathVertices_fwd s p))"  
    then obtain pv1 pv2 pv3 u where "pathVertices_fwd s p = pv1@u#pv2@u#pv3" 
      by (auto dest: not_distinct_decomp)
    then obtain p1 p2 p3 where
      "p = p1@p2@p3" "p2[]" "isPath s p1 u" "isPath u p3 t"
      using PATH
      apply -
      apply (erule (1) split_path_at_vertex_complete[where s=s]; simp)
      apply (erule split_path_at_vertex_complete[of _ _ t "u#pv2" u pv3]; simp)
      apply (auto intro: that)
      done
    hence "length (p1@p3) < length p" "isPath s (p1@p3) t"  
      by (auto simp: split_path_simps)
    thus ?case by (rule IH)
  qed
qed  
      

lemma isSPath_no_selfloop: "isSimplePath u p v  (u1, u1)  set p"
  apply (rule ccontr)
  apply (auto simp: in_set_conv_decomp split_path_simps)
  done

lemma isSPath_sg_outgoing: "isSimplePath u p v; (u1, v1)  set p; v1  v2 
   (u1, v2)  set p"
  by (auto simp: in_set_conv_decomp isSimplePath_def pathVertices_alt 
      append_eq_append_conv2 Cons_eq_append_conv append_eq_Cons_conv)

lemma isSPath_sg_incoming: 
  "isSimplePath u p v; (u1, v1)  set p; u1  u2  (u2, v1)  set p"
  by (auto simp: in_set_conv_decomp isSimplePath_fwd pathVertices_fwd_def
      append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv)

lemma isSPath_nt_parallel:
  assumes SP: "isSimplePath s p t"
  assumes EIP: "eset p"
  shows "prod.swap e  set p"
proof -  
  from SP have P: "isPath s p t" and D: "distinct (pathVertices_fwd s p)"
    by (auto simp: isSimplePath_fwd)

  show "prod.swap e  set p"  
    apply (cases e) using D EIP
    by(auto dest!: pathVertices_edge[OF P] simp add: append_eq_append_conv2 Cons_eq_append_conv append_eq_Cons_conv)

qed

lemma isSPath_nt_parallel_old: 
  "isSimplePath u p v  ((u, v)  set p. (v, u)  set p)"
  using isSPath_nt_parallel[of u p v] by auto

corollary isSPath_nt_parallel_pf: 
  "isSimplePath s p t  set p  (set p)¯ = {}"
  by (auto dest: isSPath_nt_parallel)
      
lemma isSPath_distinct: "isSimplePath u p v  distinct p"
  apply (rule ccontr)
  apply (auto dest!: not_distinct_decomp simp: split_path_simps)
  done

text ‹Edges adjacent to a node that does not lie on a path 
  are not contained in that path:›  
lemma adjacent_edges_not_on_path:
  assumes PATH: "isPath s p t"
  assumes VNV: "vset (pathVertices_fwd s p)"
  shows "adjacent v  set p = {}" 
proof -
  from VNV have "u. (u,v)set p  (v,u)set p"
    by (auto dest: pathVertices_edge[OF PATH])
  thus "adjacent v  set p = {}"
    by (auto simp: incoming_def outgoing_def adjacent_def)
qed    

corollary 
  assumes "isPath s p t"
  assumes "vset (pathVertices_fwd s p)"
  shows incoming_edges_not_on_path: "incoming v  set p = {}" 
    and outgoing_edges_not_on_path: "outgoing v  set p = {}"
  using adjacent_edges_not_on_path[OF assms]
  unfolding adjacent_def by auto

text ‹A simple path over a vertex can be split at this vertex, 
  and there are exactly two edges on the path touching this vertex.›  
lemma adjacent_edges_on_simple_path:
  assumes SPATH: "isSimplePath s p t"
  assumes VNV: "vset (pathVertices_fwd s p)" "vs" "vt"
  obtains p1 u w p2 where 
    "p = p1@(u,v)#(v,w)#p2" 
    "incoming v  set p = {(u,v)}" 
    "outgoing v  set p = {(v,w)}"
proof -
  from SPATH have 
    PATH: "isPath s p t" and 
    DIST: "distinct (pathVertices_fwd s p)" 
    by (auto simp: isSimplePath_def pathVertices_fwd)
  from split_path_at_vertex[OF VNV(1) PATH] obtain p1 p2 where 
    [simp]: "p=p1@p2" and P1: "isPath s p1 v" and P2: "isPath v p2 t" .
  from vs P1 obtain p1' u where 
    [simp]: "p1=p1'@[(u,v)]" and P1': "isPath s p1' u" and UV: "(u,v)E"
    by (cases p1 rule: rev_cases) (auto simp: split_path_simps)
  from vt P2 obtain w p2' where 
    [simp]: "p2=(v,w)#p2'" and VW: "(v,w)E" and P2': "isPath w p2' t"
    by (cases p2) (auto)
  show thesis
    apply (rule that[of p1' u w p2'])
    apply simp
    using 
      isSPath_sg_outgoing[OF SPATH, of v w] 
      isSPath_sg_incoming[OF SPATH, of u v]
      isPath_edgeset[OF PATH]
    apply (fastforce simp: incoming_def outgoing_def)+
    done
qed

subsubsection ‹Distance›

lemma connected_by_dist: "connected v v' = (d. dist v d v')"
  by (auto simp: dist_def connected_def)

lemma isPath_distD: "isPath u p v  dist u (length p) v"
  by (auto simp: dist_def)

lemma
  shows connected_distI[intro]: "dist v d v'  connected v v'"
    (*and connectedI_succ: "connected v v' ⟹ (v',v'') ∈ E ⟹ connected v v''"*)
  by (auto simp: dist_def connected_def intro: isPath_append_edge)
  
  
lemma min_distI2: 
  "connected v v'; d. dist v d v'; d'. dist v d' v'  d  d'  Q d 
     Q (min_dist v v')"
  unfolding min_dist_def
  apply (rule LeastI2_wellorder[where Q=Q and a="SOME d. dist v d v'"])
  apply (auto simp: connected_by_dist intro: someI)
  done

lemma min_distI_eq:
  " dist v d v'; d'. dist v d' v'  d  d'   min_dist v v' = d"
  by (force intro: min_distI2 simp: connected_by_dist)

text ‹Two nodes are connected by a path of length 0›, 
  iff they are equal.›
lemma dist_z_iff[simp]: "dist v 0 v'  v'=v"
  by (auto simp: dist_def)


lemma dist_z[simp, intro!]: "dist v 0 v" by simp
lemma dist_suc: "dist v d v'; (v',v'')E  dist v (Suc d) v''"
  by (auto simp: dist_def intro: isPath_append_edge)

lemma dist_cases[case_names dist_z dist_suc, consumes 1, cases pred]:
  assumes "dist v d v'"
  obtains "v=v'" "d=0"
   | vh dd where "d=Suc dd" "dist v dd vh" "(vh,v')E"
  using assms 
  apply (cases d; clarsimp simp add: dist_def)
  subgoal for … p by(cases p rule: rev_cases)(fastforce simp add: isPath_append)+
  done


text ‹The same holds for min_dist›, i.e., 
  the shortest path between two nodes has length 0›, 
  iff these nodes are equal.›
lemma min_dist_z[simp]: "min_dist v v = 0"
  by (rule min_distI2) auto

lemma min_dist_z_iff[simp]: "connected v v'  min_dist v v' = 0  v'=v" 
  by (rule min_distI2) (auto)
  
lemma min_dist_is_dist: "connected v v'  dist v (min_dist v v') v'"
  by (auto intro: min_distI2)
lemma min_dist_minD: "dist v d v'  min_dist v v'  d"
  by (auto intro: min_distI2)

text ‹We also provide introduction and destruction rules for the
  pattern min_dist v v' = Suc d›.
›

lemma min_dist_succ: 
  " connected v v'; (v',v'')  E   min_dist v v''  Suc (min_dist v v') "
  apply (rule min_distI2[where v'=v'])
  apply (auto intro!: min_dist_minD intro: dist_suc)
  done

lemma min_dist_suc:
  assumes c: "connected v v'" "min_dist v v' = Suc d"
  shows "v''. connected v v''  (v'',v')  E  min_dist v v'' = d"
proof -
  from min_dist_is_dist[OF c(1)]
  have "min_dist v v' = Suc d  ?thesis"
  proof cases
    case (dist_suc v'' d') then show ?thesis
      using min_dist_succ[of v v'' v'] min_dist_minD[of v d v'']
      by (auto simp: connected_distI)
  qed simp
  with c show ?thesis by simp
qed

text ‹
  If there is a node with a shortest path of length d›, 
  then, for any d'<d›, there is also a node with a shortest path
  of length d'›.
›
lemma min_dist_less:
  assumes "connected src v" "min_dist src v = d" and "d' < d"
  shows "v'. connected src v'  min_dist src v' = d'"
  using assms
proof (induct d arbitrary: v)
  case (Suc d) with min_dist_suc[of src v] show ?case
    by (cases "d' = d") auto
qed auto

text ‹
  Lemma min_dist_less› can be weakened to d'≤d›.
›

corollary min_dist_le:
  assumes c: "connected src v" and d': "d'  min_dist src v"
  shows "v'. connected src v'  min_dist src v' = d'"
  using min_dist_less[OF c, of "min_dist src v" d'] d' c
  by (auto simp: le_less)


lemma dist_trans[trans]: "dist u d1 w  dist w d2 v  dist u (d1+d2) v"  
  apply (clarsimp simp: dist_def)
  apply (rename_tac p1 p2)
  apply (rule_tac x="p1@p2" in exI)
  by (auto simp: isPath_append)


lemma min_dist_split:
  assumes D1: "dist u d1 w" and D2: "dist w d2 v" and MIN: "min_dist u v = d1+d2"
  shows "min_dist u w = d1" "min_dist w v = d2"
  apply (metis assms ab_semigroup_add_class.add.commute add_le_cancel_left 
    dist_trans min_distI_eq min_dist_minD)
  by (metis assms add_le_cancel_left dist_trans min_distI_eq min_dist_minD)
  
lemma ― ‹Manual proof›
  assumes D1: "dist u d1 w" and D2: "dist w d2 v" and MIN: "min_dist u v = d1+d2"
  shows "min_dist u w = d1" "min_dist w v = d2"
proof -
  from min_dist_minD[OF dist u d1 w] have "min_dist u w  d1" .
  moreover {
    have "dist u (min_dist u w) w"
      apply (rule min_dist_is_dist)
      using D1 by auto
    also note D2
    finally have "dist u (min_dist u w + d2) v" .
    moreover assume "min_dist u w < d1"
    moreover note MIN
    ultimately have False by (auto dest: min_dist_minD)
  } ultimately show "min_dist u w = d1"
    unfolding not_less[symmetric] using nat_neq_iff by blast

  from min_dist_minD[OF dist w d2 v] have "min_dist w v  d2" .
  moreover {
    note D1
    also have "dist w (min_dist w v) v"
      apply (rule min_dist_is_dist)
      using D2 by auto
    finally have "dist u (d1 + min_dist w v) v" .
    moreover assume "min_dist w v < d2"
    moreover note MIN
    ultimately have False by (auto dest: min_dist_minD)
  } ultimately show "min_dist w v = d2"
    unfolding not_less[symmetric] using nat_neq_iff by blast
qed    

subsubsection ‹Shortest Paths›

text ‹Characterization of shortest path in terms of minimum distance›
lemma isShortestPath_min_dist_def: 
  "isShortestPath u p v  isPath u p v  length p = min_dist u v"  
  unfolding isShortestPath_def min_dist_def dist_def
  apply (rule iffI; clarsimp)
  apply (rule Least_equality[symmetric]; auto; fail)
  apply (rule Least_le; auto; fail)
  done      

lemma obtain_shortest_path: 
  assumes CONN: "connected u v"  
  obtains p where "isShortestPath u p v"
  using min_dist_is_dist[OF CONN]
  unfolding dist_def isShortestPath_min_dist_def
  by blast

lemma shortestPath_is_simple:
  assumes "isShortestPath s p t"
  shows "isSimplePath s p t"
proof (rule ccontr)
  from assms have PATH: "isPath s p t" 
    and SHORTEST: "p'. isPath s p' t  length p  length p'"
    by (auto simp: isShortestPath_def)

  assume "¬isSimplePath s p t"  
  with PATH have "¬distinct (pathVertices_fwd s p)" 
    by (auto simp: isSimplePath_fwd)

  then obtain pv1 u pv2 pv3 where PV: "pathVertices_fwd s p = pv1@u#pv2@u#pv3" 
    by (auto dest: not_distinct_decomp)

  from split_path_at_vertex_complete[OF PATH PV] obtain p1 p23 where
    [simp]: "p=p1@p23" and 
      P1: "isPath s p1 u" "pathVertices_fwd s p1 = pv1@[u]" and
      P23: "isPath u p23 t" "pathVertices_fwd u p23 = (u#pv2)@u#pv3"
      by auto
      
  from split_path_at_vertex_complete[OF P23] obtain p2 p3 where
    [simp]: "p23 = p2@p3" and
    P2: "isPath u p2 u" "pathVertices_fwd u p2 = u#pv2@[u]" and
    P3: "isPath u p3 t" "pathVertices_fwd u p3 = u#pv3"
    by auto

  from P1(1) P3(1) have SHORTER_PATH: "isPath s (p1@p3) t" 
    by (auto simp: isPath_append)
  
  from P2 have "p2[]" by auto
  hence LESS: "length (p1@p3) < length p" by auto
  with SHORTER_PATH SHORTEST show False by auto
qed    

text ‹We provide yet another characterization of shortest paths:›
lemma isShortestPath_alt: 
  "isShortestPath u p v  isSimplePath u p v  length p = min_dist u v"
  using shortestPath_is_simple isShortestPath_min_dist_def
  unfolding isSimplePath_def by auto

lemma shortestPath_is_path: "isShortestPath u p v  isPath u p v"
  by (auto simp: isShortestPath_def)
  
lemma split_shortest_path: "isShortestPath u (p1@p2) v 
   (w. isShortestPath u p1 w  isShortestPath w p2 v)"
  apply (auto simp: isShortestPath_min_dist_def isPath_append)
  apply (rule exI; intro conjI; assumption?)
  apply (drule isPath_distD)+ using min_dist_split apply auto []
  apply (drule isPath_distD)+ using min_dist_split apply auto []
  done

text ‹Edges in a shortest path connect nodes with increasing 
  minimum distance from the source›
lemma isShortestPath_level_edge:  
  assumes SP: "isShortestPath s p t" 
  assumes EIP: "(u,v)set p"
  shows 
    "connected s u" "connected u v" "connected v t" and
    "min_dist s v = min_dist s u + 1" (is ?G1) and
    "min_dist u t = 1 + min_dist v t" (is ?G2) and
    "min_dist s t = min_dist s u + 1 + min_dist v t" (is ?G3) 
proof -  
  ― ‹Split the original path at the edge›
  from EIP obtain p1 p2 where [simp]: "p=p1@(u,v)#p2"
    by (auto simp: in_set_conv_decomp)
  from isShortestPath s p t have 
    MIN: "min_dist s t = length p" and 
      P: "isPath s p t" and 
     DV: "distinct (pathVertices s p)"
    by (auto simp: isShortestPath_alt isSimplePath_def)
  from P have DISTS: "dist s (length p1) u" "dist u 1 v" "dist v (length p2) t"
    by (auto simp: isPath_append dist_def intro: exI[where x="[(u,v)]"])
    
  from DISTS show "connected s u" "connected u v" "connected v t" by auto

  ― ‹Express the minimum distances in terms of the split original path›  
  from MIN have MIN': "min_dist s t = length p1 + 1 + length p2" by auto
  
  from min_dist_split[OF dist_trans[OF DISTS(1,2)] DISTS(3) MIN'] have
      MDSV: "min_dist s v = length p1 + 1" and 
    [simp]: "length p2 = min_dist v t" 
    by simp_all
  from min_dist_split[OF DISTS(1) dist_trans[OF DISTS(2,3)]] MIN' have
      MDUT: "min_dist u t = 1 + length p2" and 
    [simp]: "length p1 = min_dist s u" 
    by simp_all

  from MDSV MDUT MIN' show ?G1 ?G2 ?G3 by auto  
qed  

end ― ‹Graph›

context Finite_Graph begin

text ‹In a finite graph, the length of a shortest path is less 
  than the number of nodes›  
lemma isShortestPath_length_less_V:   
  assumes SV: "sV"
  assumes PATH: "isShortestPath s p t"
  shows "length p < card V"
  using simplePath_length_less_V[OF SV]
  using shortestPath_is_simple[OF PATH] .

corollary min_dist_less_V:
  assumes SV: "sV"
  assumes CONN: "connected s t"
  shows "min_dist s t < card V"
  apply (rule obtain_shortest_path[OF CONN])
  apply (frule isShortestPath_length_less_V[OF SV])
  unfolding isShortestPath_min_dist_def by auto

end ― ‹Finite_Graph›

end ― ‹Theory›