Theory MengerInduction
section ‹Induction of Menger's Theorem›
theory MengerInduction imports Separations DisjointPaths begin
subsection ‹No Small Separations›
text ‹
In this section we set up the general structure of the proof of Menger's Theorem.
The proof is based on induction over @{term sep_size} (called @{term n} in McCuaig's proof), the
minimum size of a separator.
›
locale NoSmallSeparationsInduct = v0_v1_Digraph +
fixes sep_size :: nat
assumes no_small_separations: "⋀S. Separation G v0 v1 S ⟹ card S ≥ Suc sep_size"
and no_small_separations_hyp: "⋀G' :: ('a, 'b) Graph_scheme.
(⋀S. Separation G' v0 v1 S ⟹ card S ≥ sep_size)
⟹ v0_v1_Digraph G' v0 v1
⟹ ∃paths. DisjointPaths G' v0 v1 paths ∧ card paths = sep_size"
text ‹
Next, we want to combine this with @{locale DisjointPathsPlusOne}.
If a minimum separator has size at least @{term "Suc sep_size"}, then it follows immediately from
the induction hypothesis that we have @{term sep_size} many disjoint paths. We then observe
that @{term second_vertices} of these paths is not a separator because
@{term "card second_vertices = sep_size"}. So there exists a new path from @{term v0} to
@{term v1} whose second vertex is not in @{term second_vertices}.
If this path is disjoint from the other paths, we have found @{term "Suc sep_size"} many disjoint
paths, so assume it is not disjoint. Then there exist a vertex @{term x} on the new path that is
not @{term v0} or @{term v1} such that @{term new_last} hits one of the other paths. Let
@{term P_new} be the initial segment of the new path up to @{term x}. We call @{term x},
the last vertex of @{term P_new}, now @{term new_last}.
We then assume that @{term paths} and @{term P_new} have been chosen in such a way that
@{term "distance new_last v1"} is minimal.
First, we define a locale that expresses that we have no small separators (with the corresponding
induction hypothesis) as well as @{term sep_size} many internally vertex-disjoint paths (with
@{term "sep_size ≠ (0 :: nat)"} because the other case is trivial) and also one additional path
that starts in @{term v1}, whose second vertex is not among @{term second_vertices} and whose last
vertex is @{term new_last}.
We will add the assumption @{term "new_last ≠ v1"} soon.
›
locale ProofStepInduct =
NoSmallSeparationsInduct G v0 v1 sep_size + DisjointPathsPlusOne G v0 v1 paths P_new
for G (structure) and v0 v1 paths P_new sep_size +
assumes sep_size_not0: "sep_size ≠ 0"
and paths_sep_size: "card paths = sep_size"
lemma (in ProofStepInduct) hitting_paths_v1: "hitting_paths v1"
unfolding hitting_paths_def using paths v0_neq_v1 by force
subsection ‹Choosing Paths Avoiding $new\_last$›
text ‹Let us now consider only the non-trivial case that @{term "new_last ≠ v1"}.›
locale ProofStepInduct_NonTrivial = ProofStepInduct +
assumes new_last_neq_v1: "new_last ≠ v1"
begin
text ‹
The next step is the observation that in the graph @{term "remove_vertex new_last"}, which
we called @{term H_x}, there are also @{term sep_size} many internally vertex-disjoint paths,
again by the induction hypothesis.
›
lemma Q_exists: "∃Q. DisjointPaths H_x v0 v1 Q ∧ card Q = sep_size"
proof-
have "⋀S. Separation H_x v0 v1 S ⟹ card S ≥ sep_size"
using subgraph_separation_min_size paths walk_in_V P_hit new_last_neq_v1 no_small_separations
by (metis H_x_def new_last_in_V new_last_neq_v0)
then show ?thesis using H_x_v0_v1_Digraph new_last_neq_v1 by (meson no_small_separations_hyp)
qed
text ‹
We want to choose these paths in a clever way, too. Our goal is to choose these paths such that
the number of edges in @{term "(⋃(edges_of_walk ` Q) ∩ (E - ⋃(edges_of_walk ` paths_with_new)))"}
is minimal.
›
definition B where "B ≡ E - ⋃(edges_of_walk ` paths_with_new)"
definition Q_weight where "Q_weight ≡ λQ. card (⋃(edges_of_walk ` Q) ∩ B)"
definition Q_good where "Q_good ≡ λQ. DisjointPaths H_x v0 v1 Q ∧ card Q = sep_size ∧
(∀Q'. DisjointPaths H_x v0 v1 Q' ∧ card Q' = sep_size ⟶ Q_weight Q ≤ Q_weight Q')"
definition Q where "Q ≡ SOME Q. Q_good Q"
text ‹It is easy to show that such a @{const Q} exists.›
lemma Q: "DisjointPaths H_x v0 v1 Q" "card Q = sep_size"
and Q_min: "⋀Q'. DisjointPaths H_x v0 v1 Q' ∧ card Q' = sep_size ⟹ Q_weight Q ≤ Q_weight Q'"
proof-
obtain Q' where "DisjointPaths H_x v0 v1 Q'" "card Q' = sep_size"
"⋀Q''. DisjointPaths H_x v0 v1 Q'' ∧ card Q'' = sep_size ⟹ Q_weight Q' ≤ Q_weight Q''"
using arg_min_ex[of "λQ. DisjointPaths H_x v0 v1 Q ∧ card Q = sep_size" Q_weight]
new_last_neq_v1 Q_exists by metis
then have "Q_good Q'" unfolding Q_good_def by blast
then show "DisjointPaths H_x v0 v1 Q" "card Q = sep_size"
"⋀Q'. DisjointPaths H_x v0 v1 Q' ∧ card Q' = sep_size ⟹ Q_weight Q ≤ Q_weight Q'"
using someI[of Q_good] by (simp_all add: Q_def Q_good_def)
qed
sublocale Q: DisjointPaths H_x v0 v1 Q using Q(1) .
subsection ‹Finding a Path Avoiding $Q$›
text ‹
Because @{const Q} contains only @{term sep_size} many paths, we have
@{term "card Q.second_vertices = sep_size"}. So there exists a path @{term P_k} among the
@{term "Suc sep_size"} many paths in @{term paths_with_new} such that the second vertex of
@{term P_k} is not among @{term Q.second_vertices}.
›
definition P_k where
"P_k ≡ SOME P_k. P_k ∈ paths_with_new ∧ hd (tl P_k) ∉ Q.second_vertices"
lemma P_k: "P_k ∈ paths_with_new" "hd (tl P_k) ∉ Q.second_vertices" proof-
obtain y where "y ∈ insert (hd (tl P_new)) second_vertices" "y ∉ Q.second_vertices" proof-
have "hd (tl P_new) ∉ second_vertices" using P_new_decomp tl_P_new(2) by simp
moreover have "card second_vertices = card Q.second_vertices" using Q(2) paths_sep_size
using Q.second_vertices_card second_vertices_card by (simp add: new_last_neq_v1)
ultimately have "card (insert (hd (tl P_new)) second_vertices) = Suc (card Q.second_vertices)"
using finite_paths second_vertices_def by auto
then show ?thesis
using that card_finite_less_ex
by (metis Q.finite_paths Q.second_vertices_def Zero_not_Suc card.infinite finite_imageI lessI)
qed
then have "∃P_k. P_k ∈ paths_with_new ∧ hd (tl P_k) ∉ Q.second_vertices"
by (metis (mono_tags, lifting) image_iff insertCI insertE paths_with_new_def second_vertex_def
second_vertices_def)
then show "P_k ∈ paths_with_new" "hd (tl P_k) ∉ Q.second_vertices"
using someI[of "λP_k. P_k ∈ paths_with_new ∧ hd (tl P_k) ∉ Q.second_vertices"] P_k_def by auto
qed
lemma path_P_k [simp]: "path P_k" by (simp add: P_k(1) paths_with_new_path)
lemma hd_P_k_v0 [simp]: "hd P_k = v0" by (simp add: P_k(1) paths_with_new_start_in_v0)
definition hitting_Q_or_new_last where
"hitting_Q_or_new_last ≡ λy. y ≠ v0 ∧ (y = new_last ∨ (∃Q_hit ∈ Q. y ∈ set Q_hit))"
text ‹
@{term P_k} hits a vertex in @{term Q} or it hits @{term new_last} because it either ends in
@{term v1} or in @{term new_last}.
›
lemma P_k_hits_Q: "∃y ∈ set P_k. hitting_Q_or_new_last y" proof (cases)
assume "P_k ≠ P_new"
then have "v1 ∈ set P_k"
by (metis P_k(1) insertE last_in_set path_from_toE paths paths_with_new_def)
moreover have "∃Q_witness. Q_witness ∈ Q" using Q(2) sep_size_not0 finite.simps by fastforce
ultimately show ?thesis
using Q.paths path_from_toE hitting_Q_or_new_last_def v0_neq_v1 by fastforce
qed (metis P_new new_last_neq_v0 hitting_Q_or_new_last_def last_in_set path_from_toE new_last_def)
end
subsection ‹Decomposing $P_k$›
text ‹
Having established with the previous lemma that @{term P_k} hits @{term Q} or @{term new_last},
let @{term y} be the first such vertex on @{term P_k}. Then we can split @{term P_k} at
this vertex.
›
locale ProofStepInduct_NonTrivial_P_k_pre = ProofStepInduct_NonTrivial +
fixes P_k_pre y P_k_post
assumes P_k_decomp: "P_k = P_k_pre @ y # P_k_post"
and y: "hitting_Q_or_new_last y"
and y_min: "⋀y'. y' ∈ set P_k_pre ⟹ ¬hitting_Q_or_new_last y'"
text ‹
We can always go from @{locale ProofStepInduct_NonTrivial} to @{locale ProofStepInduct_NonTrivial_P_k_pre}.
›
lemma (in ProofStepInduct_NonTrivial) ProofStepInduct_NonTrivial_P_k_pre_exists:
shows "∃P_k_pre y P_k_post.
ProofStepInduct_NonTrivial_P_k_pre G v0 v1 paths P_new sep_size P_k_pre y P_k_post"
proof-
obtain y P_k_pre P_k_post where
"P_k = P_k_pre @ y # P_k_post" "hitting_Q_or_new_last y"
"⋀y'. y' ∈ set P_k_pre ⟹ ¬hitting_Q_or_new_last y'"
using P_k_hits_Q split_list_first_prop[of P_k hitting_Q_or_new_last] by blast
then have "ProofStepInduct_NonTrivial_P_k_pre G v0 v1 paths P_new sep_size P_k_pre y P_k_post"
by unfold_locales
then show ?thesis by blast
qed
context ProofStepInduct_NonTrivial_P_k_pre begin
lemma y_neq_v0: "y ≠ v0" using hitting_Q_or_new_last_def y by auto
lemma P_k_pre_not_Nil: "P_k_pre ≠ Nil"
using P_k_decomp hd_P_k_v0 hitting_Q_or_new_last_def y by auto
lemma second_P_k_pre_not_in_Q: "hd (tl (P_k_pre @ [y])) ∉ Q.second_vertices"
using P_k(2) P_k_decomp P_k_pre_not_Nil
by (metis append_eq_append_conv2 append_self_conv hd_append2 list.sel(1) tl_append2)
definition H where "H ≡ remove_vertex v0"
sublocale H: Digraph H unfolding H_def using remove_vertex_Digraph .
lemma y_eq_v1_implies_P_k_neq_P_new: assumes "y = v1" shows "P_k ≠ P_new" proof
assume contra: "P_k = P_new"
have "v0 ↝(new_pre @ [new_last])↝ new_last"
using P_new(1) P_new_decomp new_last_def by auto
then have "v0 ↝P_k↝ new_last" using P_new_decomp contra by auto
moreover have "P_k = P_k_pre @ v1 # P_k_post" using P_k_decomp assms(1) by blast
ultimately have **: "v0 ↝(P_k_pre @ v1 # P_k_post)↝ new_last" by simp
then have "v1 ∈ set P_new" by (metis assms contra P_k_decomp in_set_conv_decomp)
then have "new_last = v1"
using hitting_paths_v1 assms last_P_new(2) set_butlast new_last_def by fastforce
then show False using new_last_neq_v1 by blast
qed
text ‹If @{term "y = v1"}, then we are done.›
lemma y_eq_v1_solves:
assumes "y = v1"
shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
proof-
have "P_k ≠ P_new" using y_eq_v1_implies_P_k_neq_P_new assms by blast
then have "P_k = P_k_pre @ [y]"
using P_k(1) P_k_decomp paths assms paths_with_new_def by fastforce
then have "v0 ↝(P_k_pre @ [y])↝ v1"
using paths P_k(1) ‹P_k ≠ P_new› by (simp add: paths_with_new_def)
moreover have "new_last ∉ set P_k_pre"
using hitting_Q_or_new_last_def y_min new_last_neq_v0 by auto
ultimately have "v0 ↝(P_k_pre @ [y])↝⇘H_x⇙ v1" using remove_vertex_path_from_to
by (simp add: H_x_def assms new_last_in_V new_last_neq_v1)
moreover {
fix xs v assume "xs ∈ Q" "v ∈ set xs" "v ∈ set (P_k_pre @ [y])" "v ≠ v0" "v ≠ v1"
then have "v ∈ set P_k_pre" using assms by simp
then have "¬hitting_Q_or_new_last v" using y_min by blast
then have "False" using ‹v ∈ set xs› ‹xs ∈ Q› hitting_Q_or_new_last_def ‹v ≠ v0› by auto
}
ultimately have "DisjointPaths H_x v0 v1 (insert (P_k_pre @ [y]) Q)"
using Q.DisjointPaths_extend by blast
then have "DisjointPaths G v0 v1 (insert (P_k_pre @ [y]) Q)"
using DisjointPaths_supergraph H_x_def new_last_in_V new_last_neq_v0 new_last_neq_v1 by auto
moreover have "card (insert (P_k_pre @ [y]) Q) = Suc sep_size" proof-
have "P_k_pre @ [y] ∉ Q"
by (metis P_k(2) Q.second_vertices_def ‹P_k = P_k_pre @ [y]› image_iff second_vertex_def)
then show ?thesis by (simp add: Q(2) Q.finite_paths)
qed
ultimately show ?thesis by blast
qed
end
end