Theory DisjointPaths
section ‹Internally Vertex-Disjoint Paths›
theory DisjointPaths imports Separations begin
text ‹
Menger's Theorem talks about internally vertex-disjoint @{term v0}-@{term v1}-paths. Let us
define this concept.
›
locale DisjointPaths = v0_v1_Digraph +
fixes paths :: "'a Walk set"
assumes paths:
"⋀xs. xs ∈ paths ⟹ v0↝xs↝v1"
and paths_disjoint: "⋀xs ys v.
⟦ xs ∈ paths; ys ∈ paths; xs ≠ ys; v ∈ set xs; v ∈ set ys ⟧ ⟹ v = v0 ∨ v = v1"
subsection ‹Basic Properties›
text ‹The empty set of paths trivially satisfies the conditions.›
lemma (in v0_v1_Digraph) DisjointPaths_empty: "DisjointPaths G v0 v1 {}"
by (simp add: DisjointPaths.intro DisjointPaths_axioms_def v0_v1_Digraph_axioms)
text ‹Re-adding a deleted vertex is fine.›
lemma (in v0_v1_Digraph) DisjointPaths_supergraph:
assumes "DisjointPaths (remove_vertex v) v0 v1 paths"
shows "DisjointPaths G v0 v1 paths"
proof
interpret H: DisjointPaths "remove_vertex v" v0 v1 paths using assms .
show "⋀xs. xs ∈ paths ⟹ v0 ↝xs↝ v1" using remove_vertex_path_from_to_add H.paths by blast
show "⋀xs ys v. ⟦ xs ∈ paths; ys ∈ paths; xs ≠ ys; v ∈ set xs; v ∈ set ys ⟧ ⟹ v = v0 ∨ v = v1"
by (meson DisjointPaths.paths_disjoint H.DisjointPaths_axioms)
qed
context DisjointPaths begin
lemma paths_in_all_paths: "paths ⊆ all_paths" unfolding all_paths_def using paths by blast
lemma finite_paths: "finite paths"
using finitely_many_paths infinite_super paths_in_all_paths by blast
lemma paths_edge_finite: "finite (⋃(edges_of_walk ` paths))" proof-
have "⋃(edges_of_walk ` paths) ⊆ E" using edges_of_walk_in_E paths by fastforce
then show ?thesis by (meson finite_edge_set finite_subset)
qed
lemma paths_tl_notnil: "xs ∈ paths ⟹ tl xs ≠ Nil"
by (metis path_from_toE hd_Cons_tl last_ConsL paths v0_neq_v1)
lemma paths_second_in_V: "xs ∈ paths ⟹ hd (tl xs) ∈ V"
by (metis paths edges_are_in_V(2) list.exhaust_sel path_from_toE paths_tl_notnil walk_first_edge')
lemma paths_second_not_v0: "xs ∈ paths ⟹ hd (tl xs) ≠ v0"
by (metis distinct.simps(2) hd_in_set list.exhaust_sel path_from_to_def paths paths_tl_notnil)
lemma paths_second_not_v1: "xs ∈ paths ⟹ hd (tl xs) ≠ v1"
using paths paths_tl_notnil v0_nonadj_v1 walk_first_edge' by fastforce
lemma paths_second_disjoint: "⟦ xs ∈ paths; ys ∈ paths; xs ≠ ys ⟧ ⟹ hd (tl xs) ≠ hd (tl ys)"
by (metis paths_disjoint Nil_tl hd_in_set list.set_sel(2)
paths_second_not_v0 paths_second_not_v1 paths_tl_notnil)
lemma paths_edge_disjoint:
assumes "xs ∈ paths" "ys ∈ paths" "xs ≠ ys"
shows "edges_of_walk xs ∩ edges_of_walk ys = {}"
proof (rule ccontr)
assume "edges_of_walk xs ∩ edges_of_walk ys ≠ {}"
then obtain v w where v_w: "(v,w) ∈ edges_of_walk xs" "(v,w) ∈ edges_of_walk ys" by auto
then have "v ∈ set xs" "w ∈ set xs" "v ∈ set ys" "w ∈ set ys" by (meson walk_edges_vertices)+
then have "v = v0 ∨ v = v1" "w = v0 ∨ w = v1" using assms paths_disjoint by blast+
then show False using v_w(1) assms(1) v0_nonadj_v1 edges_of_walk_edge path_edges
by (metis distinct_length_2_or_more path_decomp(2) path_from_to_def path_from_to_ends paths)
qed
text ‹Specify the conditions for adding a new disjoint path to the set of disjoint paths.›
lemma DisjointPaths_extend:
assumes P_path: "v0↝P↝v1"
and P_disjoint: "⋀xs v. ⟦ xs ∈ paths; xs ≠ P; v ∈ set xs; v ∈ set P ⟧ ⟹ v = v0 ∨ v = v1"
shows "DisjointPaths G v0 v1 (insert P paths)"
proof
fix xs ys v
assume "xs ∈ insert P paths" "ys ∈ insert P paths" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
then show "v = v0 ∨ v = v1"
by (metis DisjointPaths.paths_disjoint DisjointPaths_axioms P_disjoint insert_iff)
next
show "⋀xs. xs ∈ insert P paths ⟹ v0 ↝xs↝ v1"
using P_path paths by blast
qed
lemma DisjointPaths_reduce:
assumes "paths' ⊆ paths"
shows "DisjointPaths G v0 v1 paths'"
proof
fix xs assume "xs ∈ paths'" then show "v0 ↝xs↝ v1" using assms paths by blast
next
fix xs ys v assume "xs ∈ paths'" "ys ∈ paths'" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
then show "v = v0 ∨ v = v1" by (meson assms paths_disjoint subsetCE)
qed
subsection ‹Second Vertices›
text ‹
Let us now define the set of second vertices of the paths. We are going to need this in order
to find a path avoiding the old paths on its first edge.
›
definition second_vertex where "second_vertex ≡ λxs :: 'a Walk. hd (tl xs)"
definition second_vertices where "second_vertices ≡ second_vertex ` paths"
lemma second_vertex_inj: "inj_on second_vertex paths"
unfolding second_vertex_def using paths_second_disjoint by (meson inj_onI)
lemma second_vertices_card: "card second_vertices = card paths"
unfolding second_vertices_def using finite_paths card_image second_vertex_inj by blast
lemma second_vertices_in_V: "second_vertices ⊆ V"
unfolding second_vertex_def second_vertices_def using paths_second_in_V by blast
lemma v0_v1_notin_second_vertices: "v0 ∉ second_vertices" "v1 ∉ second_vertices"
unfolding second_vertices_def second_vertex_def
using paths_second_not_v0 paths_second_not_v1 by blast+
lemma second_vertices_new_path: "hd (tl xs) ∉ second_vertices ⟹ xs ∉ paths"
by (metis image_iff second_vertex_def second_vertices_def)
lemma second_vertices_first_edge:
"⟦ xs ∈ paths; first_edge_of_walk xs = (v,w) ⟧ ⟹ w ∈ second_vertices"
unfolding second_vertices_def second_vertex_def
using first_edge_hd_tl paths paths_tl_notnil by fastforce
text ‹
If we have no small separations, then the set of second vertices is not a separator and we can
find a path avoiding this set.
›
lemma disjoint_paths_new_path:
assumes no_small_separations: "⋀S. Separation G v0 v1 S ⟹ card S ≥ Suc (card paths)"
shows "∃P_new. v0↝P_new↝v1 ∧ set P_new ∩ second_vertices = {}"
proof-
have "¬Separation G v0 v1 second_vertices"
using no_small_separations second_vertices_card by force
then show ?thesis
by (simp add: path_exists_if_no_separation second_vertices_in_V v0_v1_notin_second_vertices)
qed
text ‹
We need the following predicate to find the first vertex on a new path that hits one of the
other paths. We add the condition @{term "x = v1"} to cover the case @{term "paths = {}"}.
›
definition hitting_paths where
"hitting_paths ≡ λx. x ≠ v0 ∧ ((∃xs ∈ paths. x ∈ set xs) ∨ x = v1)"
end
section ‹One More Path›
text ‹
Let us define a set of disjoint paths with one more path. Except for the first and last vertex,
the new path must be disjoint from all other paths. The first vertex must be @{term v0} and the
last vertex must be on some other path. In the ideal case, the last vertex will be @{term v1},
in which case we are already done because we have found a new disjoint path between @{term v0}
and @{term v1}.
›
locale DisjointPathsPlusOne = DisjointPaths +
fixes P_new :: "'a Walk"
assumes P_new:
"v0 ↝P_new↝ (last P_new)"
and tl_P_new:
"tl P_new ≠ Nil"
"hd (tl P_new) ∉ second_vertices"
and last_P_new:
"hitting_paths (last P_new)"
"⋀v. v ∈ set (butlast P_new) ⟹ ¬hitting_paths v"
begin
subsection ‹Characterizing the New Path›
lemma P_new_hd_disjoint: "⋀xs. xs ∈ paths ⟹ hd (tl P_new) ≠ hd (tl xs)"
using tl_P_new(2) unfolding second_vertices_def second_vertex_def by blast
lemma P_new_new: "P_new ∉ paths" using P_new_hd_disjoint by auto
definition paths_with_new where "paths_with_new ≡ insert P_new paths"
lemma card_paths_with_new: "card paths_with_new = Suc (card paths)"
unfolding paths_with_new_def using P_new_new by (simp add: finite_paths)
lemma paths_with_new_no_Nil: "Nil ∉ paths_with_new"
using P_new paths_tl_notnil paths_with_new_def by fastforce
lemma paths_with_new_path: "xs ∈ paths_with_new ⟹ path xs"
using P_new paths paths_with_new_def by auto
lemma paths_with_new_start_in_v0: "xs ∈ paths_with_new ⟹ hd xs = v0"
using P_new paths paths_with_new_def by auto
subsection ‹The Last Vertex of the New Path›
text ‹
McCuaig in \<^cite>‹"DBLP:journals/jgt/McCuaig84"› calls the last vertex of @{term P_new} by the name
@{term x}. However, this name is somewhat confusing because it is so short and it will be visible
in most places from now on, so let us give this vertex the more descriptive name of
@{term new_last}.
›
definition new_pre where "new_pre ≡ butlast P_new"
definition new_last where "new_last ≡ last P_new"
lemma P_new_decomp: "P_new = new_pre @ [new_last]"
by (metis new_pre_def append_butlast_last_id list.sel(2) tl_P_new(1) new_last_def)
lemma new_pre_not_Nil: "new_pre ≠ Nil" using P_new(1) hitting_paths_def
by (metis P_new_decomp list.sel(3) self_append_conv2 tl_P_new(1))
lemma new_pre_hitting: "x' ∈ set new_pre ⟹ ¬hitting_paths x'"
by (simp add: new_pre_def last_P_new(2))
lemma P_hit: "hitting_paths new_last"
by (simp add: last_P_new(1) new_last_def)
lemma new_last_neq_v0: "new_last ≠ v0" using hitting_paths_def P_hit by force
lemma new_last_in_V: "new_last ∈ V" using P_new new_last_def path_in_V by fastforce
lemma new_last_to_v1: "∃R. new_last ↝R↝⇘remove_vertex v0⇙ v1"
proof (cases)
assume "new_last = v1"
then have "new_last ↝[v1]↝⇘remove_vertex v0⇙ v1"
by (metis last.simps list.sel(1) list.set(1) list.simps(15) list.simps(3) path_from_to_def
path_singleton remove_vertex_path_from_to singletonD v0_V v0_neq_v1 v1_V)
then show ?thesis by blast
next
assume "new_last ≠ v1"
then obtain xs where xs: "xs ∈ paths" "new_last ∈ set xs"
using hitting_paths_def last_P_new(1) new_last_def by auto
then obtain xs_pre xs_post where xs_decomp: "xs = xs_pre @ new_last # xs_post"
by (meson split_list)
then have "new_last ↝(new_last # xs_post)↝ v1" using ‹xs ∈ paths›
by (metis paths last_appendR list.sel(1) list.simps(3) path_decomp(2) path_from_to_def)
then have "new_last ↝(new_last # xs_post)↝⇘remove_vertex v0⇙ v1"
using remove_vertex_path_from_to
by (metis paths Set.set_insert xs_decomp xs(1) disjoint_insert(1) distinct_append hd_append
hitting_paths_def last_P_new(1) list.set_sel(1) path_from_to_def v0_V new_last_def)
then show ?thesis by blast
qed
lemma paths_plus_one_disjoint:
assumes "xs ∈ paths_with_new" "ys ∈ paths_with_new" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
shows "v = v0 ∨ v = v1 ∨ v = new_last"
proof-
have "xs ∈ paths ∨ ys ∈ paths" using assms(1,2,3) paths_with_new_def by auto
then have "hitting_paths v ∨ v = v0" using assms(1,2,4,5) unfolding hitting_paths_def by blast
then show ?thesis using assms last_P_new(2) set_butlast paths_disjoint
by (metis insert_iff paths_with_new_def new_last_def)
qed
text ‹If the new path is disjoint, we are happy.›
lemma P_new_solves_if_disjoint:
"new_last = v1 ⟹ ∃paths'. DisjointPaths G v0 v1 paths' ∧ card paths' = Suc (card paths)"
using DisjointPaths_extend P_new(1) paths_plus_one_disjoint card_paths_with_new
unfolding paths_with_new_def new_last_def by blast
subsection ‹Removing the Last Vertex›
definition H_x where "H_x ≡ remove_vertex new_last"
lemma H_x_Digraph: "Digraph H_x" unfolding H_x_def using remove_vertex_Digraph .
lemma H_x_v0_v1_Digraph: "new_last ≠ v1 ⟹ v0_v1_Digraph H_x v0 v1" unfolding H_x_def
using remove_vertices_v0_v1_Digraph hitting_paths_def P_hit by (simp add: H_x_def)
subsection ‹A New Path Following the Other Paths›
text ‹
The following lemma is one of the most complicated technical lemmas in the proof of Menger's
Theorem.
Suppose we have a non-trivial path whose edges are all in the edge set of @{term path_with_new}
and whose first edge equals the first edge of some @{term "P ∈ path_with_new"}. Also suppose that
the path does not contain @{term v1} or @{term new_last}. Then it follows by induction that this
path is an initial segment of @{term P}.
Note that McCuaig does not mention this statement at all in his proof because it looks so obvious.
›
lemma new_path_follows_old_paths:
assumes xs: "v0 ↝xs↝ w" "tl xs ≠ Nil" "v1 ∉ set xs" "new_last ∉ set xs"
and P: "P ∈ paths_with_new" "hd (tl xs) = hd (tl P)"
and edges_subset: "edges_of_walk xs ⊆ ⋃(edges_of_walk ` paths_with_new)"
shows "edges_of_walk xs ⊆ edges_of_walk P"
using xs P(2) edges_subset proof (induct "length xs" arbitrary: xs w)
case 0
then show ?case using xs(1) by auto
next
case (Suc n xs w)
have "n ≠ 0" using Suc.hyps(2) Suc.prems(1,2)
by (metis path_from_toE Nitpick.size_list_simp(2) Suc_inject length_0_conv)
show ?case proof (cases)
assume "n = Suc 0"
then obtain v w where v_w: "xs = [v,w]"
by (metis (full_types) Suc.hyps(2) length_0_conv length_Suc_conv)
then have "v = v0" using Suc.prems(1) by auto
moreover have "w = hd (tl P)" using Suc.prems(5) v_w by auto
moreover have "edges_of_walk xs = {(v, w)}" using v_w edges_of_walk_2 by simp
moreover have "(v0, hd (tl P)) ∈ edges_of_walk P" using P tl_P_new(1) P_new paths
by (metis first_edge_hd_tl first_edge_in_edges insert_iff paths_tl_notnil paths_with_new_def)
ultimately show ?thesis by auto
next
assume "n ≠ Suc 0"
obtain xs' x where xs': "xs = xs' @ [x]"
by (metis path_from_toE Suc.prems(1) append_butlast_last_id)
then have "n = length xs'" using xs' using Suc.hyps(2) by auto
moreover have xs'_path: "v0 ↝xs'↝ last xs'"
using xs' Suc.prems(1) ‹tl xs ≠ Nil› walk_decomp(1)
by (metis distinct_append hd_append list.sel(3) path_from_to_def self_append_conv2)
moreover have "tl xs' ≠ []" using ‹n ≠ Suc 0›
by (metis path_from_toE Nitpick.size_list_simp(2) calculation(1,2))
moreover have "v1 ∉ set xs'" using xs' Suc.prems(3) by auto
moreover have "new_last ∉ set xs'" using xs' Suc.prems(4) by auto
moreover have "hd (tl xs') = hd (tl P)"
using xs' ‹tl xs' ≠ []› Suc.prems(5) calculation(2) by auto
moreover have "edges_of_walk xs' ⊆ ⋃(edges_of_walk ` paths_with_new)"
using xs' Suc.prems(6) edges_of_comp1 by blast
ultimately have xs'_edges: "edges_of_walk xs' ⊆ edges_of_walk P" using Suc.hyps(1) by blast
moreover have "edges_of_walk xs = edges_of_walk xs' ∪ { (last xs', x) }"
using xs' using walk_edges_decomp'[of "butlast xs'" "last xs'" x Nil] xs'_path
by (metis path_from_toE Un_empty_right append_assoc append_butlast_last_id butlast.simps(2)
edges_of_walk_empty(2) last_ConsL last_ConsR list.distinct(1))
moreover have "(last xs', x) ∈ edges_of_walk P" proof (rule ccontr)
assume contra: "(last xs', x) ∉ edges_of_walk P"
have xs_last_edge: "(last xs', x) ∈ edges_of_walk xs"
using xs' calculation(2) by blast
then obtain P' where
P': "P' ∈ paths_with_new" "(last xs', x) ∈ edges_of_walk P'"
using Suc.prems(6) by auto
then have "P ≠ P'" using contra by blast
moreover have "last xs' ∈ set P" using xs_last_edge xs'_edges ‹tl xs' ≠ []› xs'_path
by (metis path_from_toE last_in_set subsetCE walk_edges_subset)
moreover have "last xs' ∈ set P'" using P'(2) by (meson walk_edges_vertices(1))
ultimately have "last xs' = v0 ∨ last xs' = v1 ∨ last xs' = new_last"
using paths_plus_one_disjoint P'(1) P paths_with_new_def by auto
then show False using Suc.prems(3) ‹new_last ∉ set xs'› ‹tl xs' ≠ []› xs' xs'_path
by (metis path_from_toE butlast_snoc in_set_butlastD last_in_set last_tl path_from_to_first)
qed
ultimately show ?thesis by simp
qed
qed
end
end