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
  ― ‹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_xv1" 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}