Theory MengerInduction

theory MengerInduction
imports DisjointPaths
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
  ― ‹The size of a minimum separator.›
  assumes no_small_separations: "⋀S. Separation G v0 v1 S ⟹ card S ≥ Suc sep_size"
  ― ‹The induction hypothesis.›
  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"

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"
  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)

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'"
  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)

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)
  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
  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

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 ― ‹locale @{locale ProofStepInduct_NonTrivial}›

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"
  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

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

  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"
    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)
    ultimately show ?thesis by blast
end ― ‹locale @{locale ProofStepInduct_NonTrivial_P_k_pre}›