Theory Graph
section ‹Graphs›
theory Graph
imports Main begin
text ‹@{typ 'a} is the vertex type.›
type_synonym 'a Edge = "'a × 'a"
type_synonym 'a Walk = "'a list"
record 'a Graph =
verts :: "'a set" ("Vı")
arcs :: "'a Edge set" ("Eı")
abbreviation is_arc :: "('a, 'b) Graph_scheme ⇒ 'a ⇒ 'a ⇒ bool" (infixl "→ı" 60) where
"v →⇘G⇙ w ≡ (v,w) ∈ E⇘G⇙"
text ‹
We only consider undirected finite simple graphs, that is, graphs without multi-edges and without
loops.
›
locale Graph =
fixes G :: "('a, 'b) Graph_scheme" (structure)
assumes finite_vertex_set: "finite V"
and valid_edge_set: "E ⊆ V × V"
and undirected: "v→w = w→v"
and no_loops: "¬v→v"
begin
lemma finite_edge_set [simp]: "finite E" using finite_vertex_set valid_edge_set
by (simp add: finite_subset)
lemma edges_are_in_V: assumes "v→w" shows "v ∈ V" "w ∈ V"
using assms valid_edge_set by blast+
subsection ‹Walks›
text ‹A walk is sequence of vertices connected by edges.›
inductive walk :: "'a Walk ⇒ bool" where
Nil [simp]: "walk []"
| Singleton [simp]: "v ∈ V ⟹ walk [v]"
| Cons: "v→w ⟹ walk (w # vs) ⟹ walk (v # w # vs)"
text ‹
Show a few composition/decomposition lemmas for walks. These will greatly simplify the proofs
that follow.›
lemma walk_2 [simp]: "v→w ⟹ walk [v,w]" by (simp add: edges_are_in_V(2) walk.intros(3))
lemma walk_comp: "⟦ walk xs; walk ys; xs = Nil ∨ ys = Nil ∨ last xs→hd ys ⟧ ⟹ walk (xs @ ys)"
by (induct rule: walk.induct, simp_all add: walk.intros(3))
(metis list.exhaust_sel walk.intros(2) walk.intros(3))
lemma walk_tl: "walk xs ⟹ walk (tl xs)" by (induct rule: walk.induct) simp_all
lemma walk_drop: "walk xs ⟹ walk (drop n xs)" by (induct n, simp) (metis drop_Suc tl_drop walk_tl)
lemma walk_take: "walk xs ⟹ walk (take n xs)"
by (induct arbitrary: n rule: walk.induct)
(simp, metis Graph.walk.simps Graph_axioms take_Cons' take_eq_Nil,
metis Graph.walk.simps Graph_axioms edges_are_in_V(1) take_Cons')
lemma walk_rev: "walk xs ⟹ walk (rev xs)"
by (induct rule: walk.induct, simp, simp)
(metis Singleton edges_are_in_V(1) last_ConsL last_appendR list.sel(1)
not_Cons_self2 rev.simps(2) undirected walk_comp)
lemma walk_decomp: assumes "walk (xs @ ys)" shows "walk xs" "walk ys"
using assms append_eq_conv_conj[of xs ys "xs @ ys"] walk_take walk_drop by metis+
lemma walk_dropWhile: "walk xs ⟹ walk (dropWhile f xs)" by (simp add: walk_drop dropWhile_eq_drop)
lemma walk_takeWhile: "walk xs ⟹ walk (takeWhile f xs)" using walk_take takeWhile_eq_take by metis
lemma walk_in_V: "walk xs ⟹ set xs ⊆ V" by (induct rule: walk.induct; simp add: edges_are_in_V)
lemma walk_first_edge: "walk (v # w # xs) ⟹ v→w" using walk.cases by fastforce
lemma walk_first_edge': "⟦ walk (v # xs); xs ≠ Nil ⟧ ⟹ v→hd xs"
using walk_first_edge by (metis list.exhaust_sel)
lemma walk_middle_edge: "walk (xs @ v # w # ys) ⟹ v→w"
by (induct "xs @ v # w # ys" arbitrary: xs rule: walk.induct, simp, simp)
(metis list.sel(1,3) self_append_conv2 tl_append2)
lemma walk_last_edge: "⟦ walk (xs @ ys); xs ≠ Nil; ys ≠ Nil ⟧ ⟹ last xs→hd ys"
using walk_middle_edge[of "butlast xs" "last xs" "hd ys" "tl ys"]
by (metis Cons_eq_appendI append_butlast_last_id append_eq_append_conv2 list.exhaust_sel self_append_conv)
lemma walk_takeWhile_edge:
assumes "walk (xs @ [v])" "xs ≠ Nil" "hd xs ≠ v"
shows "last (takeWhile (λx. x ≠ v) xs)→v" (is "last ?xs→v")
proof-
obtain xs' where xs': "xs = ?xs @ xs'" by (metis takeWhile_dropWhile_id)
thus ?thesis proof (cases)
assume "xs' = Nil" thus ?thesis using xs' assms(1,2) walk_last_edge by force
next
assume "xs' ≠ Nil"
hence "hd xs' = v" by (metis (full_types) hd_dropWhile same_append_eq takeWhile_dropWhile_id xs')
thus ?thesis by (metis ‹xs' ≠ []› append_Nil assms(1,3) walk_decomp(1) walk_last_edge xs')
qed
qed
subsection ‹Connectivity›
definition connected :: "'a ⇒ 'a ⇒ bool" (infixl "→⇧*" 60) where
"connected v w ≡ ∃xs. walk xs ∧ xs ≠ Nil ∧ hd xs = v ∧ last xs = w"
lemma connectedI [intro]: "⟦ walk xs; xs ≠ Nil; hd xs = v; last xs = w ⟧ ⟹ v →⇧* w"
unfolding connected_def by blast
lemma connectedE:
assumes "v →⇧* w"
obtains xs where "walk xs" "xs ≠ Nil" "hd xs = v" "last xs = w"
using assms that unfolding connected_def by blast
lemma connected_in_V: assumes "v →⇧* w" shows "v ∈ V" "w ∈ V"
using assms unfolding connected_def by (meson hd_in_set last_in_set subsetCE walk_in_V)+
lemma connected_refl: "v ∈ V ⟹ v →⇧* v" by (rule connectedI[of "[v]"]) simp_all
lemma connected_edge: "v→w ⟹ v →⇧* w" by (rule connectedI[of "[v,w]"]) simp_all
lemma connected_trans:
assumes u_v: "u →⇧* v" and v_w: "v →⇧* w"
shows "u →⇧* w"
proof-
obtain xs where xs: "walk xs" "xs ≠ Nil" "hd xs = u" "last xs = v" using u_v connectedE by blast
obtain ys where ys: "walk ys" "ys ≠ Nil" "hd ys = v" "last ys = w" using v_w connectedE by blast
let ?R = "xs @ tl ys"
show ?thesis proof
show "walk ?R" using walk_comp[OF xs(1)] by (metis xs(4) ys(1,2,3) list.sel(1,3) walk.simps)
show "?R ≠ Nil" by (simp add: xs(2))
show "hd ?R = u" by (simp add: xs(2,3))
show "last ?R = w" using xs(2,4) ys(2,3,4)
by (metis append_butlast_last_id last_append last_tl list.exhaust_sel)
qed
qed
subsection ‹Paths›
text ‹A path is a walk without repeated vertices. This is simple enough, so most of the above
lemmas transfer directly to paths.›
abbreviation path :: "'a Walk ⇒ bool" where "path xs ≡ walk xs ∧ distinct xs"
lemma path_singleton [simp]: "v ∈ V ⟹ path [v]" by simp
lemma path_2 [simp]: "⟦ v→w; v ≠ w ⟧ ⟹ path [v,w]" by simp
lemma path_cons: "⟦ path xs; xs ≠ Nil; v→hd xs; v ∉ set xs ⟧ ⟹ path (v # xs)"
by (metis distinct.simps(2) list.exhaust_sel walk.Cons)
lemma path_comp: "⟦ walk xs; walk ys; xs = Nil ∨ ys = Nil ∨ last xs→hd ys; distinct (xs @ ys) ⟧
⟹ path (xs @ ys)" using walk_comp by blast
lemma path_tl: "path xs ⟹ path (tl xs)" by (simp add: distinct_tl walk_tl)
lemma path_drop: "path xs ⟹ path (drop n xs)" by (simp add: walk_drop)
lemma path_take: "path xs ⟹ path (take n xs)" by (simp add: walk_take)
lemma path_rev: "path xs ⟹ path (rev xs)" by (simp add: walk_rev)
lemma path_decomp: assumes "path (xs @ ys)" shows "path xs" "path ys"
using walk_decomp assms distinct_append by blast+
lemma path_dropWhile: "path xs ⟹ path (dropWhile f xs)" by (simp add: walk_dropWhile)
lemma path_takeWhile: "path xs ⟹ path (takeWhile f xs)" by (simp add: walk_takeWhile)
lemma path_in_V: "path xs ⟹ set xs ⊆ V" by (simp add: walk_in_V)
lemma path_first_edge: "path (v # w # xs) ⟹ v→w" using walk_first_edge by blast
lemma path_first_edge': "⟦ path (v # xs); xs ≠ Nil ⟧ ⟹ v→hd xs" using walk_first_edge' by blast
lemma path_middle_edge: "path (xs @ v # w # ys) ⟹ v → w" using walk_middle_edge by blast
lemma path_takeWhile_edge: "⟦ path (xs @ [v]); xs ≠ Nil; hd xs ≠ v ⟧
⟹ last (takeWhile (λx. x ≠ v) xs)→v" using walk_takeWhile_edge by blast
end
text ‹We introduce shorthand notation for a path connecting two vertices.›
definition path_from_to :: "('a, 'b) Graph_scheme ⇒ 'a ⇒ 'a Walk ⇒ 'a ⇒ bool"
("_ ↝_↝ı _" [71, 71, 71] 70) where
"path_from_to G v xs w ≡ Graph.path G xs ∧ xs ≠ Nil ∧ hd xs = v ∧ last xs = w"
context Graph begin
lemma path_from_toI [intro]: "⟦ path xs; xs ≠ Nil; hd xs = v; last xs = w ⟧ ⟹ v ↝xs↝ w"
and path_from_toE [dest]: "v ↝xs↝ w ⟹ path xs ∧ xs ≠ Nil ∧ hd xs = v ∧ last xs = w"
unfolding path_from_to_def by blast+
text ‹Every walk contains a path connecting the same vertices.›
lemma walk_to_path:
assumes "walk xs" "xs ≠ Nil" "hd xs = v" "last xs = w"
shows "∃ys. v ↝ys↝ w ∧ set ys ⊆ set xs"
proof-
text ‹We prove this by removing loops from @{term xs} until @{term xs} is a path.
We want to perform induction over @{term "length xs"}, but @{term xs} in
@{term "set ys ⊆ set xs"} should not be part of the induction hypothesis. To accomplish this,
we hide @{term "set xs"} behind a definition for this specific part of the goal.›
define target_set where "target_set = set xs"
hence "set xs ⊆ target_set" by simp
thus "∃ys. v ↝ys↝ w ∧ set ys ⊆ target_set"
using assms
proof (induct "length xs" arbitrary: xs rule: infinite_descent0)
case (smaller n)
then obtain xs where
xs: "n = length xs" "walk xs" "xs ≠ Nil" "hd xs = v" "last xs = w" "set xs ⊆ target_set" and
hyp: "¬(∃ys. v ↝ys↝ w ∧ set ys ⊆ target_set)" by blast
text ‹If @{term xs} is not a path, then @{term xs} is not distinct and we can decompose it.›
then obtain ys zs u
where xs_decomp: "u ∈ set ys" "distinct ys" "xs = ys @ u # zs"
using not_distinct_conv_prefix by (metis path_from_toI)
text ‹@{term u} appears in @{term xs}, so we have a loop in @{term xs} starting from an
occurrence of @{term u} in @{term xs} ending in the vertex @{term u} in @{term "u # ys"}.
We define @{term zs} as @{term xs} without this loop.›
obtain ys' ys_suffix where
ys_decomp: "ys = ys' @ u # ys_suffix" by (meson split_list xs_decomp(1))
define zs' where "zs' = ys' @ u # zs"
have "walk zs'" unfolding zs'_def using xs(2) xs_decomp(3) ys_decomp
by (metis walk_decomp list.sel(1) list.simps(3) walk_comp walk_last_edge)
moreover have "length zs' < n" unfolding zs'_def by (simp add: xs(1) xs_decomp(3) ys_decomp)
moreover have "hd zs' = v" unfolding zs'_def
by (metis append_is_Nil_conv hd_append list.sel(1) xs(4) xs_decomp(3) ys_decomp)
moreover have "last zs' = w" unfolding zs'_def using xs(5) xs_decomp(3) by auto
moreover have "set zs' ⊆ target_set" unfolding zs'_def using xs(6) xs_decomp(3) ys_decomp by auto
ultimately show ?case using zs'_def hyp by blast
qed simp
qed
corollary connected_by_path:
assumes "v →⇧* w"
obtains xs where "v ↝xs↝ w"
using assms connected_def walk_to_path by blast
subsection ‹Cycles›
text ‹A cycle in an undirected graph is a closed path with at least 3 different vertices.
Closed paths with 0 or 1 vertex do not exist (graphs are loop-free), and paths with 2 vertices
are not considered loops in undirected graphs.›
definition cycle :: "'a Walk ⇒ bool" where
"cycle xs ≡ path xs ∧ length xs > 2 ∧ last xs → hd xs"
lemma cycleI [intro]: "⟦ path xs; length xs > 2; last xs→hd xs ⟧ ⟹ cycle xs"
unfolding cycle_def by blast
lemma cycleE: "cycle xs ⟹ path xs ∧ xs ≠ Nil ∧ length xs > 2 ∧ last xs→hd xs"
unfolding cycle_def by auto
text ‹We can now show a lemma that explains how to construct cycles from certain paths.
If two paths both starting from @{term v} diverge immediately and meet again on their
last vertices, then the graph contains a cycle with @{term v} on it.
Note that if two paths do not diverge immediately but only eventually, then
@{prop maximal_common_prefix} can be used to remove the common prefix.›
lemma meeting_paths_produce_cycle:
assumes xs: "path (v # xs)" "xs ≠ Nil"
and ys: "path (v # ys)" "ys ≠ Nil"
and meet: "last xs = last ys"
and diverge: "hd xs ≠ hd ys"
shows "∃zs. cycle zs ∧ hd zs = v"
proof-
have "set xs ∩ set ys ≠ {}" using meet xs(2) ys(2) last_in_set by fastforce
then obtain xs' x xs'' where xs': "xs = xs' @ x # xs''" "set xs' ∩ set ys = {}" "x ∈ set ys"
using split_list_first_prop[of xs "λx. x ∈ set ys"] by (metis disjoint_iff_not_equal)
then obtain ys' ys'' where ys': "ys = ys' @ x # ys''" "x ∉ set ys'"
using split_list_first_prop[of ys "λy. y = x"] by blast
let ?zs = "v # xs' @ x # (rev ys')"
have "last ?zs→hd ?zs"
using undirected walk_first_edge walk_first_edge' ys'(1) ys(1) by (fastforce simp: last_rev)
moreover have "path ?zs" proof
have "walk (x # rev ys')" proof(cases)
assume "ys' = Nil" thus ?thesis using ‹last ?zs→hd ?zs› edges_are_in_V(1) by auto
next
assume "ys' ≠ Nil"
moreover hence "last ys'→x" using walk_last_edge walk_tl ys'(1) ys(1) by fastforce
moreover have "hd (rev ys') = last ys'" by (simp add: ‹ys' ≠ []› hd_rev)
moreover have "walk (rev ys')" by (metis list.sel(3) walk_decomp(1) walk_rev walk_tl ys'(1) ys(1))
ultimately show "walk (x # rev ys')" using path_cons undirected ys'(1) ys(1) by auto
qed
thus "walk (v # xs' @ x # rev ys')" using xs'(1) xs(1)
by (metis append_Cons list.sel(1) list.simps(3) walk_comp walk_decomp(1) walk_last_edge)
next
show "distinct (v # xs' @ x # rev ys')" unfolding distinct_append distinct.simps(2) set_append
using xs'(1,2) xs(1) ys'(1) ys(1) by auto
qed
moreover have "length ?zs ≠ 2" using diverge xs'(1) ys'(1) by auto
ultimately show ?thesis using cycleI[of ?zs] by auto
qed
text ‹A graph with unique paths between every pair of connected vertices has no cycles.›
lemma unique_paths_implies_no_cycles:
assumes unique_paths: "⋀v w. v →⇧* w ⟹ ∃!xs. v ↝xs↝ w"
shows "⋀xs. ¬cycle xs"
proof
fix xs assume "cycle xs"
let ?v = "hd xs"
let ?w = "last xs"
let ?ys = "[?v,?w]"
define good where "good xs ⟷ ?v ↝xs↝ ?w" for xs
have "path ?ys" using ‹cycle xs› cycle_def no_loops undirected by auto
hence "good ?ys" unfolding good_def by (simp add: path_from_toI)
moreover have "good xs" unfolding good_def by (simp add: path_from_toI ‹cycle xs› cycleE)
moreover have "?ys ≠ xs" using ‹cycle xs›
by (metis One_nat_def Suc_1 cycleE length_Cons less_not_refl list.size(3))
ultimately have "¬(∃!xs. good xs)" by blast
moreover have "connected ?v ?w" using ‹cycle xs› cycleE by blast
ultimately show False unfolding good_def using unique_paths by blast
qed
text ‹
A graph without cycles (also called a forest) has a unique path between every pair of connected
vertices.
›
lemma no_cycles_implies_unique_paths:
assumes no_cycles: "⋀xs. ¬cycle xs" and connected: "v →⇧* w"
shows "∃!xs. v ↝xs↝ w"
proof (rule ex_ex1I)
show "∃xs. v ↝xs↝ w" using connected connected_by_path by blast
next
fix xs ys
assume "v ↝xs↝ w" "v ↝ys↝ w"
hence xs_valid: "path xs" "xs ≠ Nil" "hd xs = v" "last xs = w"
and ys_valid: "path ys" "ys ≠ Nil" "hd ys = v" "last ys = w" by blast+
show "xs = ys" proof (rule ccontr)
assume "xs ≠ ys"
hence "∃ps xs' ys'. xs = ps @ xs' ∧ ys = ps @ ys' ∧ (xs' = Nil ∨ ys' = Nil ∨ hd xs' ≠ hd ys')"
by (induct xs ys rule: list_induct2', blast, blast, blast)
(metis (no_types, opaque_lifting) append_Cons append_Nil list.sel(1))
then obtain ps xs' ys' where
ps: "xs = ps @ xs'" "ys = ps @ ys'" "xs' = Nil ∨ ys' = Nil ∨ hd xs' ≠ hd ys'" by blast
have "last xs ∈ set ps" if "xs' = Nil" using xs_valid(2) ps(1) by (simp add: that)
hence xs_not_nil: "xs' ≠ Nil" using ‹xs ≠ ys› ys_valid(1,4) ps(1,2) xs_valid(4) by auto
have "last ys ∈ set ps" if "ys' = Nil" using ys_valid(2) ps(2) by (simp add: that)
hence ys_not_nil: "ys' ≠ Nil" using ‹xs ≠ ys› xs_valid(1,4) ps(1,2) ys_valid(4) by auto
have "∃zs. cycle zs" proof-
let ?v = "last ps"
have *: "ps ≠ Nil" using xs_valid(2,3) ys_valid(2,3) ps(1,2,3) by auto
have "path (?v # xs')" using xs_valid(1) ps(1) * walk_decomp(2)
by (metis append_Cons append_assoc append_butlast_last_id distinct_append self_append_conv2)
moreover have "path (?v # ys')" using ys_valid(1) ps(2) * walk_decomp(2)
by (metis append_Cons append_assoc append_butlast_last_id distinct_append self_append_conv2)
moreover have "last xs' = last ys'"
using xs_valid(4) ys_valid(4) xs_not_nil ys_not_nil ps(1,2) by auto
ultimately show ?thesis using ps(3) meeting_paths_produce_cycle xs_not_nil ys_not_nil by blast
qed
thus False using no_cycles by blast
qed
qed
end
end