Quelle  MengerInduction.thy

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"
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 ― ‹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"
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])↝ 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 ― ‹locale @{locale ProofStepInduct_NonTrivial_P_k_pre}›

end