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 by (simp add: ProofStepInductOptimalPaths.intro ProofStepInductOptimalPaths_axioms.intro) 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" by (simp add: G.v0_v1_Digraph_axioms NoSmallSeparationsInduct.intro 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_nonadj_v1: "¬v0→v1" 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_nonadj_v1: "¬v0→v1" 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