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"
where "E ≡ {(u, v). c (u, v) ≠ 0}"
definition V :: "node set"
where "V ≡ {u. ∃v. (u, v) ∈ E ∨ (v, u) ∈ E}"
definition incoming :: "node ⇒ edge set"
where "incoming v ≡ {(u, v) | u. (u, v) ∈ E}"
definition outgoing :: "node ⇒ edge set"
where "outgoing v ≡ {(v, u) | u. (v, u) ∈ E}"
definition adjacent :: "node ⇒ edge set"
where "adjacent v ≡ incoming v ∪ outgoing v"
definition incoming' :: "node set ⇒ edge set"
where "incoming' k ≡ {(u, v) | u v. u ∉ k ∧ v ∈ k ∧ (u, v) ∈ E}"
definition outgoing' :: "node set ⇒ edge set"
where "outgoing' k ≡ {(v, u) | u v. u ∉ k ∧ v ∈ k ∧ (v, u) ∈ E}"
definition adjacent' :: "node set ⇒ edge set"
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
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)"
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"
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"
where "dist v d v' ≡ ∃p. isPath v p v' ∧ length p = d"
definition min_dist :: "node ⇒ node ⇒ nat"
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: "(∑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¯``{u}. g (v,u))"
proof -
have "(∑e∈incoming u. g e) = (∑e∈(λv. (v,u))`(E¯``{u}). g e)"
by (rule sum.cong) (auto simp: incoming_def)
also have "… = (∑v∈E¯``{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.›
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:
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)
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"
"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_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
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)¯ = {}"
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'"
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 @{text "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 @{text "min_dist"}, i.e.,
the shortest path between two nodes has length @{text "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 @{text "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 @{text "d"},
then, for any @{text "d'<d"}, there is also a node with a shortest path
of length @{text "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 @{text "min_dist_less"} can be weakened to @{text "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
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 -
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
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
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
end