# Theory Menger

```section ‹Menger's Theorem›

theory Menger imports Y_eq_new_last Y_neq_new_last begin

text ‹In this section, we combine the cases and finally prove Menger's Theorem.›

locale ProofStepInductOptimalPaths = ProofStepInduct +
assumes optimal_paths:
"⋀paths' P_new'. ProofStepInduct G v0 v1 paths' P_new' sep_size
⟹ Digraph.distance (remove_vertex v0) (last P_new) v1
≤ Digraph.distance (remove_vertex v0) (last P_new') v1"
begin

lemma one_more_paths_exists_trivial:
"new_last = v1 ⟹ ∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
using P_new_solves_if_disjoint paths_sep_size by blast

lemma one_more_paths_exists_nontrivial:
assumes "new_last ≠ v1"
shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
proof-
interpret ProofStepInduct_NonTrivial G v0 v1 paths P_new sep_size
using assms new_last_def by unfold_locales simp
obtain P_k_pre y P_k_post where
"ProofStepInduct_NonTrivial_P_k_pre G v0 v1 paths P_new sep_size P_k_pre y P_k_post"
using ProofStepInduct_NonTrivial_P_k_pre_exists by blast
then interpret ProofStepInduct_NonTrivial_P_k_pre G v0 v1 paths P_new sep_size P_k_pre y P_k_post .
{
assume "y ≠ v1" "y = new_last"
then interpret ProofStepInduct_y_eq_new_last G v0 v1 paths P_new sep_size P_k_pre y P_k_post
using optimal_paths[folded H_def] by unfold_locales
have ?thesis using with_optimal_paths_solves by blast
} moreover {
assume "y ≠ v1" "y ≠ new_last"
then interpret ProofStepInduct_y_neq_new_last G v0 v1 paths P_new sep_size P_k_pre y P_k_post
by unfold_locales
have ?thesis using contradiction by blast
}
ultimately show ?thesis using y_eq_v1_solves by blast
qed

corollary one_more_paths_exists:
shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
using one_more_paths_exists_trivial one_more_paths_exists_nontrivial by blast

end

lemma (in ProofStepInduct) one_more_paths_exists:
"∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
proof-
define paths_weight where "paths_weight ≡
λ(paths' :: 'a Walk set, P_new'). Digraph.distance (remove_vertex v0) (last P_new') v1"
define paths_good where "paths_good ≡
λ(paths', P_new'). ProofStepInduct G v0 v1 paths' P_new' sep_size"
have "∃paths' P_new'. paths_good (paths', P_new')"
unfolding paths_good_def using ProofStepInduct_axioms by auto
then obtain P' where
P': "paths_good P'" "⋀P''. paths_good P'' ⟹ paths_weight P' ≤ paths_weight P''"
using arg_min_ex[of paths_good paths_weight] by blast

then obtain paths' P_new' where P'_decomp: "P' = (paths', P_new')" by (meson surj_pair)

have optimal_paths_good: "ProofStepInduct G v0 v1 paths' P_new' sep_size"
using P'(1) P'_decomp unfolding paths_good_def by auto

have "⋀paths'' P_new''. paths_good (paths'', P_new'')
⟹ paths_weight P' ≤ paths_weight (paths'', P_new'')" by (simp add: P'(2))
then have optimal_paths_min: "⋀paths'' P_new''. ProofStepInduct G v0 v1 paths'' P_new'' sep_size
⟹ Digraph.distance (remove_vertex v0) (last P_new') v1
≤ Digraph.distance (remove_vertex v0) (last P_new'') v1"
unfolding paths_good_def paths_weight_def by (simp add: P'_decomp)

interpret G: ProofStepInductOptimalPaths G v0 v1 paths' P_new' sep_size
using optimal_paths_good optimal_paths_min
show ?thesis using G.one_more_paths_exists by blast
qed

subsection ‹Menger's Theorem›

theorem (in v0_v1_Digraph) menger:
assumes "⋀S. Separation G v0 v1 S ⟹ card S ≥ n"
shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = n"
using assms v0_v1_Digraph_axioms proof (induct n arbitrary: G)
case (0 G)
then show ?case using v0_v1_Digraph.DisjointPaths_empty[of G] card.empty by blast
next
case (Suc n G)
interpret G: v0_v1_Digraph G v0 v1 using Suc(3) .
have "⋀S. Separation G v0 v1 S ⟹ n ≤ card S" using Suc.prems Suc_leD by blast
then obtain paths where P: "DisjointPaths G v0 v1 paths" "card paths = n" using Suc(1,3) by blast
interpret G: DisjointPaths G v0 v1 paths using P(1) .

obtain P_new where
P_new: "v0 ↝P_new↝⇘G⇙ v1" "set P_new ∩ G.second_vertices = {}"
using G.disjoint_paths_new_path P(2) Suc.prems(1) by blast
have P_new_new: "P_new ∉ paths"
by (metis G.paths_tl_notnil G.second_vertex_def G.second_vertices_def G.path_from_toE IntI
P_new empty_iff image_eqI list.set_sel(1) list.set_sel(2))

have "G.hitting_paths v1" unfolding G.hitting_paths_def using v0_neq_v1 by blast
then have "∃x ∈ set P_new. G.hitting_paths x" using P_new(1) by fastforce
then obtain new_pre x new_post where
P_new_decomp: "P_new = new_pre @ x # new_post"
and x: "G.hitting_paths x"
"⋀y. y ∈ set new_pre ⟹ ¬G.hitting_paths y"
by (metis split_list_first_prop)

have 1: "DisjointPathsPlusOne G v0 v1 paths (new_pre @ [x])" proof
show "v0 ↝(new_pre @ [x])↝⇘G⇙ last (new_pre @ [x])" using P_new(1)
by (metis G.path_decomp' P_new_decomp append_is_Nil_conv hd_append2 list.distinct(1)
list.sel(1) path_from_to_def self_append_conv2)
then show "tl (new_pre @ [x]) ≠ []"
by (metis DisjointPaths.hitting_paths_def G.DisjointPaths_axioms G.path_from_toE
butlast.simps(1) butlast_snoc list.distinct(1) list.sel(1) self_append_conv2
tl_append2 x(1))
have "new_pre ≠ Nil" using G.hitting_paths_def P_new(1) P_new_decomp x(1) by auto
then have "hd (tl (new_pre @ [x])) = hd (tl P_new)" by (simp add: P_new_decomp hd_append)
then show "hd (tl (new_pre @ [x])) ∉ G.second_vertices"
by (metis P_new(2) P_new_decomp ‹new_pre ≠ []› append_is_Nil_conv disjoint_iff_not_equal
list.distinct(1) list.set_sel(1) list.set_sel(2) tl_append2)
show "G.hitting_paths (last (new_pre @ [x]))" using x(1) by auto
show "⋀v. v ∈ set (butlast (new_pre @ [x])) ⟹ ¬G.hitting_paths v" by (simp add: x(2))
qed

have 2: "NoSmallSeparationsInduct G v0 v1 n"
NoSmallSeparationsInduct_axioms_def Suc.hyps Suc.prems(1))

show ?case proof (rule ccontr)
assume not_case: "¬?case"
have "x ≠ v1" proof
assume "x = v1"
define paths' where "paths' = insert P_new paths"
{
fix xs v
assume *: "xs ∈ paths" "v ∈ set xs" "v ∈ set P_new" "v ≠ v0" "v ≠ v1"
have "v ∈ set new_pre"
by (metis *(3,5) G.path_from_to_ends G.path_from_toE P_new(1) P_new_decomp
‹x = v1› butlast_snoc set_butlast)
then have False using *(1,2,4) G.hitting_paths_def x(2) by auto
}
then have "DisjointPaths G v0 v1 paths'" unfolding paths'_def
using G.DisjointPaths_extend P_new(1) by blast
moreover have "card paths' = Suc n"
using P_new_new by (simp add: G.finite_paths P(2) paths'_def)
ultimately show False using not_case by blast
qed
have "ProofStepInduct_axioms paths n" proof
show "n ≠ 0"
using G.DisjointPaths_extend G.finite_paths P(2) P_new(1) not_case card_insert_disjoint
by fastforce
qed (insert P(2))
then have "ProofStepInduct G v0 v1 paths (new_pre @ [x]) n"
using 1 2 by (simp add: ProofStepInduct.intro)
then show False using ProofStepInduct.one_more_paths_exists not_case by metis
qed
qed

text ‹
The previous theorem was the difficult direction of Menger's Theorem.  Let us now prove the other
direction: If we have @{term n} disjoint paths, than every separator must contain at least
@{term n} vertices.  This direction is rather trivial because every separator needs to separate
at least the @{term n} paths, so we do not need induction or an elaborate setup to prove this.
›

theorem (in v0_v1_Digraph) menger_trivial:
assumes "DisjointPaths G v0 v1 paths" "card paths = n"
shows "⋀S. Separation G v0 v1 S ⟹ card S ≥ n"
proof-
interpret DisjointPaths G v0 v1 paths using assms(1) .
fix S assume "Separation G v0 v1 S"
then interpret S: Separation G v0 v1 S .

text ‹
Our plan is to show @{term "card S ≥ n"} by defining an injective function from @{term paths}
into @{term S}.  Because we have @{term "card paths = n"}, the result follows.

For the injective function, we simply use the observation stated above: Every path needs to
be separated by @{term S} at some vertex, so we can choose such a vertex.
›
define f where "f ≡ λxs. SOME v. v ∈ S ∧ v ∈ set xs"

have f_good: "⋀xs. xs ∈ paths ⟹ f xs ∈ S ∧ f xs ∈ set xs" proof-
fix xs assume "xs ∈ paths"
then obtain v where "v ∈ set xs ∩ S" using S.S_separates paths by fastforce
then show "f xs ∈ S ∧ f xs ∈ set xs" unfolding f_def
using someI[of "λv. v ∈ S ∧ v ∈ set xs" v] by blast
qed

text ‹This @{term f} is injective because no two paths intersect in the same vertex.›
have "inj_on f paths" proof
fix xs ys
assume *: "xs ∈ paths" "ys ∈ paths" "f xs = f ys"
then obtain v where "v ∈ S" "v ∈ set xs" "v ∈ set ys"
using f_good by fastforce
then show "xs = ys" using *(1,2) paths_disjoint S.v0_notin_S S.v1_notin_S by fastforce
qed

then show "card S ≥ n" using assms(2) f_good
by (metis S.finite_S finite_paths image_subsetI inj_on_iff_card_le)
qed

subsection ‹Self-contained Statement of the Main Theorem›

text ‹
Let us state both directions of Menger's Theorem again in a more self-contained way in the
@{locale Digraph} locale. Stating the theorems in a self-contained way helps avoiding mistakes
due to wrong definitions hidden in one of the numerous locales we used and also significantly
reduces the work needed to review this formalization.

With the statements below, all you need to do in order to verify that this formalization
actually expresses Menger's Theorem (and not something else), is to look into the assumptions
and definitions of the @{locale Digraph} locale.
›

theorem (in Digraph) menger:
fixes v0 v1 :: 'a and n :: nat
assumes v0_V: "v0 ∈ V"
and v1_V: "v1 ∈ V"
and v0_neq_v1: "v0 ≠ v1"
and no_small_separators: "⋀S.
⟦ S ⊆ V; v0 ∉ S; v1 ∉ S; ⋀xs. v0 ↝xs↝ v1 ⟹ set xs ∩ S ≠ {} ⟧ ⟹ card S ≥ n"
shows "∃paths. card paths = n ∧ (∀xs ∈ paths.
v0 ↝xs↝ v1 ∧ (∀ys ∈ paths - {xs}. (∀v ∈ set xs ∩ set ys. v = v0 ∨ v = v1)))"
proof-
interpret v0_v1_Digraph G v0 v1 using v0_V v1_V v0_nonadj_v1 v0_neq_v1 by unfold_locales
have "⋀S. Separation G v0 v1 S ⟹ n ≤ card S" using no_small_separators
by (simp add: Separation.S_V Separation.S_separates Separation.v0_notin_S Separation.v1_notin_S)
then obtain paths where
paths: "DisjointPaths G v0 v1 paths" "card paths = n" using no_small_separators menger by blast
then show ?thesis
by (metis DiffD1 DiffD2 DisjointPaths.paths DisjointPaths.paths_disjoint IntD1 IntD2 singletonI)
qed

theorem (in Digraph) menger_trivial:
fixes v0 v1 :: 'a and n :: nat
assumes v0_V: "v0 ∈ V"
and v1_V: "v1 ∈ V"
and v0_neq_v1: "v0 ≠ v1"
and n_paths: "card paths = n"
and paths_disjoint: "∀xs ∈ paths.
v0 ↝xs↝ v1 ∧ (∀ys ∈ paths - {xs}. (∀v ∈ set xs ∩ set ys. v = v0 ∨ v = v1))"
shows "⋀S. ⟦ S ⊆ V; v0 ∉ S; v1 ∉ S; ⋀xs. v0 ↝xs↝ v1 ⟹ set xs ∩ S ≠ {} ⟧ ⟹ card S ≥ n"
proof-
interpret v0_v1_Digraph G v0 v1 using v0_V v1_V v0_nonadj_v1 v0_neq_v1 by unfold_locales
interpret DisjointPaths G v0 v1 paths proof
show "⋀xs. xs ∈ paths ⟹ v0 ↝xs↝ v1" using paths_disjoint by simp
next
fix xs ys v assume "xs ∈ paths" "ys ∈ paths" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
then have "xs ∈ paths" "ys ∈ paths - {xs}" "v ∈ set xs ∩ set ys" by blast+
then show "v = v0 ∨ v = v1" using paths_disjoint by blast
qed
fix S assume "S ⊆ V" "v0 ∉ S" "v1 ∉ S" "⋀xs. v0 ↝xs↝ v1 ⟹ set xs ∩ S ≠ {}"
then interpret Separation G v0 v1 S by unfold_locales
show "card S ≥ n" using menger_trivial DisjointPaths_axioms Separation_axioms n_paths by blast
qed

end
```