Quellcode-Bibliothek Graph.thy

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<sup>-1</sup>``{u})"

definition "adjacent_nodes u ≡ E``{u} ∪ E<sup>-1</sup>``{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^-1``{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<sup>-1</sup>``{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: "(∑e∈outgoing u. g e) = (∑v∈E``{u}. g (u,v))"  
proof -
  have "(∑e∈outgoing u. g e) = (∑e∈(λv. (u,v))`(E``{u}). g e)"  
    by (rule sum.cong) (auto simp: outgoing_def)
  also have "… = (∑v∈E``{u}. g (u,v))"  
    by (subst sum.reindex)(auto simp add: inj_on_def)
  finally show ?thesis .
qed  

lemma sum_incoming_pointwise: "(∑e∈incoming u. g e) = (∑v∈E^-1``{u}. g (v,u))"  
proof -
  have "(∑e∈incoming u. g e) = (∑e∈(λv. (v,u))`(E<sup>-1</sup>``{u}). g e)"  
    by (rule sum.cong) (auto simp: incoming_def)
  also have "… = (∑v∈E^-1``{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. [ v∈V; (v,u)∉E ] ==> g (v,u) = 0"
  shows "(∑e∈incoming u. g e) = (∑v∈V. 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. [ v∈V; (u,v)∉E ] ==> g (u,v) = 0"
  shows "(∑e∈outgoing u. g e) = (∑v∈V. 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 \<forall> 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 p∩E ⊆ 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^-1)^* ==> (∃p. isPath u p v)"
proof -
  assume "(v,u)∈(E^-1)^*" 
  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"
  "s∈set (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: "[u∈V; 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 "u∈set (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] ==> v∈V ⟷ u∈V"
  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: 
  "u∈reachableNodes s ==> (u,v)∈E ==> v∈reachableNodes 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) ∧ u≠v ∧ (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) ∧ s≠u ∧ (s,u)∈E
        ∧ isSimplePath u p t ∧ s∉set (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: "u∈V"
  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: "e∈set 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)^-1 = {}"
  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: "v∉set (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 "v∉set (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: "v∈set (pathVertices_fwd s p)" "v≠s" "v≠t"
  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 ‹v≠s› 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 ‹v≠t› 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' \<Longrightarrow> (v',v'') \<in> E \<Longrightarrow> 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: "s∈V"
  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: "s∈V"
  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›