Quelle  DisjointPaths.thy

section ‹Internally Vertex-Disjoint Paths›

theory DisjointPaths imports Separations begin

text ‹
 Menger's Theorem talks about internally vertex-disjoint @{term v0}-@{term v1}-paths. Let us
 define this concept.
 ›

locale DisjointPaths = v0_v1_Digraph +
  fixes paths :: "'a Walk set"
  assumes paths:
    "∧xs. xs ∈ paths ==> v0↝xs↝v1"
  and paths_disjoint: "∧xs ys v.
    [ xs ∈ paths; ys ∈ paths; xs ≠ ys; v ∈ set xs; v ∈ set ys ] ==> v = v0 ∨ v = v1"

subsection ‹Basic Properties›

text ‹The empty set of paths trivially satisfies the conditions.›
lemma (in v0_v1_Digraph) DisjointPaths_empty: "DisjointPaths G v0 v1 {}"
  by (simp add: DisjointPaths.intro DisjointPaths_axioms_def v0_v1_Digraph_axioms)

text ‹Re-adding a deleted vertex is fine.›
lemma (in v0_v1_Digraph) DisjointPaths_supergraph:
  assumes "DisjointPaths (remove_vertex v) v0 v1 paths"
  shows "DisjointPaths G v0 v1 paths"
proof
  interpret H: DisjointPaths "remove_vertex v" v0 v1 paths using assms .
  show "∧xs. xs ∈ paths ==> v0 ↝xs↝ v1" using remove_vertex_path_from_to_add H.paths by blast
  show "∧xs ys v. [ xs ∈ paths; ys ∈ paths; xs ≠ ys; v ∈ set xs; v ∈ set ys ] ==> v = v0 ∨ v = v1"
    by (meson DisjointPaths.paths_disjoint H.DisjointPaths_axioms)
qed

context DisjointPaths begin

lemma paths_in_all_paths: "paths ⊆ all_paths" unfolding all_paths_def using paths by blast
lemma finite_paths: "finite paths"
  using finitely_many_paths infinite_super paths_in_all_paths by blast

lemma paths_edge_finite: "finite (∪(edges_of_walk ` paths))" proof-
  have "∪(edges_of_walk ` paths) ⊆ E" using edges_of_walk_in_E paths by fastforce
  then show ?thesis by (meson finite_edge_set finite_subset)
qed

lemma paths_tl_notnil: "xs ∈ paths ==> tl xs ≠ Nil"
  by (metis path_from_toE hd_Cons_tl last_ConsL paths v0_neq_v1)

lemma paths_second_in_V: "xs ∈ paths ==> hd (tl xs) ∈ V"
  by (metis paths edges_are_in_V(2) list.exhaust_sel path_from_toE paths_tl_notnil walk_first_edge')

lemma paths_second_not_v0: "xs ∈ paths ==> hd (tl xs) ≠ v0"
  by (metis distinct.simps(2) hd_in_set list.exhaust_sel path_from_to_def paths paths_tl_notnil)

lemma paths_second_not_v1: "xs ∈ paths ==> hd (tl xs) ≠ v1"
  using paths paths_tl_notnil v0_nonadj_v1 walk_first_edge' by fastforce

lemma paths_second_disjoint: "[ xs ∈ paths; ys ∈ paths; xs ≠ ys ] ==> hd (tl xs) ≠ hd (tl ys)"
  by (metis paths_disjoint Nil_tl hd_in_set list.set_sel(2)
      paths_second_not_v0 paths_second_not_v1 paths_tl_notnil)

lemma paths_edge_disjoint:
  assumes "xs ∈ paths" "ys ∈ paths" "xs ≠ ys"
  shows "edges_of_walk xs ∩ edges_of_walk ys = {}"
proof (rule ccontr)
  assume "edges_of_walk xs ∩ edges_of_walk ys ≠ {}"
  then obtain v w where v_w: "(v,w) ∈ edges_of_walk xs" "(v,w) ∈ edges_of_walk ys" by auto
  then have "v ∈ set xs" "w ∈ set xs" "v ∈ set ys" "w ∈ set ys" by (meson walk_edges_vertices)+
  then have "v = v0 ∨ v = v1" "w = v0 ∨ w = v1" using assms paths_disjoint by blast+
  then show False using v_w(1) assms(1) v0_nonadj_v1 edges_of_walk_edge path_edges
    by (metis distinct_length_2_or_more path_decomp(2) path_from_to_def path_from_to_ends paths)
qed

text ‹Specify the conditions for adding a new disjoint path to the set of disjoint paths.›
lemma DisjointPaths_extend:
  assumes P_path: "v0↝P↝v1"
      and P_disjoint: "∧xs v. [ xs ∈ paths; xs ≠ P; v ∈ set xs; v ∈ set P ] ==> v = v0 ∨ v = v1"
  shows "DisjointPaths G v0 v1 (insert P paths)"
proof
  fix xs ys v
  assume "xs ∈ insert P paths" "ys ∈ insert P paths" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
  then show "v = v0 ∨ v = v1"
    by (metis DisjointPaths.paths_disjoint DisjointPaths_axioms P_disjoint insert_iff)
next
  show "∧xs. xs ∈ insert P paths ==> v0 ↝xs↝ v1"
    using P_path paths by blast
qed

lemma DisjointPaths_reduce:
  assumes "paths' ⊆ paths"
  shows "DisjointPaths G v0 v1 paths'"
proof
  fix xs assume "xs ∈ paths'" then show "v0 ↝xs↝ v1" using assms paths by blast
next
  fix xs ys v assume "xs ∈ paths'" "ys ∈ paths'" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
  then show "v = v0 ∨ v = v1" by (meson assms paths_disjoint subsetCE)
qed

subsection ‹Second Vertices›

text ‹
 Let us now define the set of second vertices of the paths. We are going to need this in order
 to find a path avoiding the old paths on its first edge.
 ›

definition second_vertex where "second_vertex ≡ λxs :: 'a Walk. hd (tl xs)"
definition second_vertices where "second_vertices ≡ second_vertex ` paths"

lemma second_vertex_inj: "inj_on second_vertex paths"
  unfolding second_vertex_def using paths_second_disjoint by (meson inj_onI)

lemma second_vertices_card: "card second_vertices = card paths"
  unfolding second_vertices_def using finite_paths card_image second_vertex_inj by blast

lemma second_vertices_in_V: "second_vertices ⊆ V"
  unfolding second_vertex_def second_vertices_def using paths_second_in_V by blast
lemma v0_v1_notin_second_vertices: "v0 ∉ second_vertices" "v1 ∉ second_vertices"
  unfolding second_vertices_def second_vertex_def
  using paths_second_not_v0 paths_second_not_v1 by blast+

lemma second_vertices_new_path: "hd (tl xs) ∉ second_vertices ==> xs ∉ paths"
  by (metis image_iff second_vertex_def second_vertices_def)

lemma second_vertices_first_edge:
  "[ xs ∈ paths; first_edge_of_walk xs = (v,w) ] ==> w ∈ second_vertices"
  unfolding second_vertices_def second_vertex_def
  using first_edge_hd_tl paths paths_tl_notnil by fastforce

text ‹
 If we have no small separations, then the set of second vertices is not a separator and we can
 find a path avoiding this set.
 ›
lemma disjoint_paths_new_path:
  assumes no_small_separations: "∧S. Separation G v0 v1 S ==> card S ≥ Suc (card paths)"
  shows "∃P_new. v0↝P_new↝v1 ∧ set P_new ∩ second_vertices = {}"
proof-
  have "¬Separation G v0 v1 second_vertices"
    using no_small_separations second_vertices_card by force
  then show ?thesis
      by (simp add: path_exists_if_no_separation second_vertices_in_V v0_v1_notin_second_vertices)
qed

text ‹
 We need the following predicate to find the first vertex on a new path that hits one of the
 other paths. We add the condition @{term "x = v1"} to cover the case @{term "paths = {}"}.
 ›
definition hitting_paths where
  "hitting_paths ≡ λx. x ≠ v0 ∧ ((∃xs ∈ paths. x ∈ set xs) ∨ x = v1)"

end ― ‹DisjointPaths›


section ‹One More Path›

text ‹
 Let us define a set of disjoint paths with one more path. Except for the first and last vertex,
 the new path must be disjoint from all other paths. The first vertex must be @{term v0} and the
 last vertex must be on some other path. In the ideal case, the last vertex will be @{term v1},
 in which case we are already done because we have found a new disjoint path between @{term v0}
 and @{term v1}.
 ›
locale DisjointPathsPlusOne = DisjointPaths +
  fixes P_new :: "'a Walk"
  assumes P_new:
    "v0 ↝P_new↝ (last P_new)"
  and tl_P_new:
    "tl P_new ≠ Nil"
    "hd (tl P_new) ∉ second_vertices"
  and last_P_new:
    "hitting_paths (last P_new)"
    "∧v. v ∈ set (butlast P_new) ==> ¬hitting_paths v"
begin

subsection ‹Characterizing the New Path›

lemma P_new_hd_disjoint: "∧xs. xs ∈ paths ==> hd (tl P_new) ≠ hd (tl xs)"
  using tl_P_new(2) unfolding second_vertices_def second_vertex_def by blast

lemma P_new_new: "P_new ∉ paths" using P_new_hd_disjoint by auto

definition paths_with_new where "paths_with_new ≡ insert P_new paths"

lemma card_paths_with_new: "card paths_with_new = Suc (card paths)"
  unfolding paths_with_new_def using P_new_new by (simp add: finite_paths)

lemma paths_with_new_no_Nil: "Nil ∉ paths_with_new"
  using P_new paths_tl_notnil paths_with_new_def by fastforce

lemma paths_with_new_path: "xs ∈ paths_with_new ==> path xs"
  using P_new paths paths_with_new_def by auto

lemma paths_with_new_start_in_v0: "xs ∈ paths_with_new ==> hd xs = v0"
  using P_new paths paths_with_new_def by auto

subsection ‹The Last Vertex of the New Path›

text ‹
 McCuaig in cite‹"DBLP:journals/jgt/McCuaig84"› calls the last vertex of @{term P_new} by the name
 @{term x}. However, this name is somewhat confusing because it is so short and it will be visible
 in most places from now on, so let us give this vertex the more descriptive name of
 @{term new_last}.
 ›
definition new_pre where "new_pre ≡ butlast P_new"
definition new_last where "new_last ≡ last P_new"

lemma P_new_decomp: "P_new = new_pre @ [new_last]"
  by (metis new_pre_def append_butlast_last_id list.sel(2) tl_P_new(1) new_last_def)

lemma new_pre_not_Nil: "new_pre ≠ Nil" using P_new(1) hitting_paths_def
  by (metis P_new_decomp list.sel(3) self_append_conv2 tl_P_new(1))

lemma new_pre_hitting: "x' ∈ set new_pre ==> ¬hitting_paths x'"
  by (simp add: new_pre_def last_P_new(2))

lemma P_hit: "hitting_paths new_last"
  by (simp add: last_P_new(1) new_last_def)

lemma new_last_neq_v0: "new_last ≠ v0" using hitting_paths_def P_hit by force

lemma new_last_in_V: "new_last ∈ V" using P_new new_last_def path_in_V by fastforce

lemma new_last_to_v1: "∃R. new_last ↝R↝ _v0 v1"
proof (cases)
  assume "new_last = v1"
  then have "new_last ↝[v1]↝ _v0 v1"
    by (metis last.simps list.sel(1) list.set(1) list.simps(15) list.simps(3) path_from_to_def
        path_singleton remove_vertex_path_from_to singletonD v0_V v0_neq_v1 v1_V)
  then show ?thesis by blast
next
  assume "new_last ≠ v1"
  then obtain xs where xs: "xs ∈ paths" "new_last ∈ set xs"
    using hitting_paths_def last_P_new(1) new_last_def by auto
  then obtain xs_pre xs_post where xs_decomp: "xs = xs_pre @ new_last # xs_post"
    by (meson split_list)
  then have "new_last ↝(new_last # xs_post)↝ v1" using ‹xs ∈ paths›
    by (metis paths last_appendR list.sel(1) list.simps(3) path_decomp(2) path_from_to_def)
  then have "new_last ↝(new_last # xs_post)↝ _v0 v1"
    using remove_vertex_path_from_to
    by (metis paths Set.set_insert xs_decomp xs(1) disjoint_insert(1) distinct_append hd_append
        hitting_paths_def last_P_new(1) list.set_sel(1) path_from_to_def v0_V new_last_def)
  then show ?thesis by blast
qed

lemma paths_plus_one_disjoint:
  assumes "xs ∈ paths_with_new" "ys ∈ paths_with_new" "xs ≠ ys" "v ∈ set xs" "v ∈ set ys"
  shows "v = v0 ∨ v = v1 ∨ v = new_last"
proof-
  have "xs ∈ paths ∨ ys ∈ paths" using assms(1,2,3) paths_with_new_def by auto
  then have "hitting_paths v ∨ v = v0" using assms(1,2,4,5) unfolding hitting_paths_def by blast
  then show ?thesis using assms last_P_new(2) set_butlast paths_disjoint
    by (metis insert_iff paths_with_new_def new_last_def)
qed

text ‹If the new path is disjoint, we are happy.›

lemma P_new_solves_if_disjoint:
  "new_last = v1 ==> ∃paths'. DisjointPaths G v0 v1 paths' ∧ card paths' = Suc (card paths)"
  using DisjointPaths_extend P_new(1) paths_plus_one_disjoint card_paths_with_new
  unfolding paths_with_new_def new_last_def by blast

subsection ‹Removing the Last Vertex›

definition H_x where "H_x ≡ remove_vertex new_last"

lemma H_x_Digraph: "Digraph H_x" unfolding H_x_def using remove_vertex_Digraph .

lemma H_x_v0_v1_Digraph: "new_last ≠ v1 ==> v0_v1_Digraph H_x v0 v1" unfolding H_x_def
  using remove_vertices_v0_v1_Digraph hitting_paths_def P_hit by (simp add: H_x_def)

subsection ‹A New Path Following the Other Paths›

text ‹
 The following lemma is one of the most complicated technical lemmas in the proof of Menger's
 Theorem.

 Suppose we have a non-trivial path whose edges are all in the edge set of @{term path_with_new}
 and whose first edge equals the first edge of some @{term "P ∈ path_with_new"}. Also suppose that
 the path does not contain @{term v1} or @{term new_last}. Then it follows by induction that this
 path is an initial segment of @{term P}.

 Note that McCuaig does not mention this statement at all in his proof because it looks so obvious.
 ›

lemma new_path_follows_old_paths:
  assumes xs: "v0 ↝xs↝ w" "tl xs ≠ Nil" "v1 ∉ set xs" "new_last ∉ set xs"
      and P: "P ∈ paths_with_new" "hd (tl xs) = hd (tl P)"
      and edges_subset: "edges_of_walk xs ⊆ ∪(edges_of_walk ` paths_with_new)"
    shows "edges_of_walk xs ⊆ edges_of_walk P"
using xs P(2) edges_subset proof (induct "length xs" arbitrary: xs w)
  case 0
  then show ?case using xs(1) by auto
next
  case (Suc n xs w)
  have "n ≠ 0" using Suc.hyps(2) Suc.prems(1,2)
    by (metis path_from_toE Nitpick.size_list_simp(2) Suc_inject length_0_conv)
  show ?case proof (cases)
    assume "n = Suc 0"
    then obtain v w where v_w: "xs = [v,w]"
      by (metis (full_types) Suc.hyps(2) length_0_conv length_Suc_conv)
    then have "v = v0" using Suc.prems(1) by auto
    moreover have "w = hd (tl P)" using Suc.prems(5) v_w by auto
    moreover have "edges_of_walk xs = {(v, w)}" using v_w edges_of_walk_2 by simp
    moreover have "(v0, hd (tl P)) ∈ edges_of_walk P" using P tl_P_new(1) P_new paths
      by (metis first_edge_hd_tl first_edge_in_edges insert_iff paths_tl_notnil paths_with_new_def)
    ultimately show ?thesis by auto
  next
    assume "n ≠ Suc 0"
    obtain xs' x where xs': "xs = xs' @ [x]"
      by (metis path_from_toE Suc.prems(1) append_butlast_last_id)
    then have "n = length xs'" using xs' using Suc.hyps(2) by auto
    moreover have xs'_path: "v0 ↝xs'↝ last xs'"
      using xs' Suc.prems(1) ‹tl xs ≠ Nil› walk_decomp(1)
      by (metis distinct_append hd_append list.sel(3) path_from_to_def self_append_conv2)
    moreover have "tl xs' ≠ []" using ‹n ≠ Suc 0›
      by (metis path_from_toE Nitpick.size_list_simp(2) calculation(1,2))
    moreover have "v1 ∉ set xs'" using xs' Suc.prems(3) by auto
    moreover have "new_last ∉ set xs'" using xs' Suc.prems(4) by auto
    moreover have "hd (tl xs') = hd (tl P)"
      using xs' ‹tl xs' ≠ []› Suc.prems(5) calculation(2) by auto
    moreover have "edges_of_walk xs' ⊆ ∪(edges_of_walk ` paths_with_new)"
      using xs' Suc.prems(6) edges_of_comp1 by blast
    ultimately have xs'_edges: "edges_of_walk xs' ⊆ edges_of_walk P" using Suc.hyps(1) by blast
    moreover have "edges_of_walk xs = edges_of_walk xs' ∪ { (last xs', x) }"
      using xs' using walk_edges_decomp'[of "butlast xs'" "last xs'" x Nil] xs'_path
      by (metis path_from_toE Un_empty_right append_assoc append_butlast_last_id butlast.simps(2)
          edges_of_walk_empty(2) last_ConsL last_ConsR list.distinct(1))
    moreover have "(last xs', x) ∈ edges_of_walk P" proof (rule ccontr)
      assume contra: "(last xs', x) ∉ edges_of_walk P"
      have xs_last_edge: "(last xs', x) ∈ edges_of_walk xs"
        using xs' calculation(2) by blast
      then obtain P' where
        P': "P' ∈ paths_with_new" "(last xs', x) ∈ edges_of_walk P'"
        using Suc.prems(6) by auto
      then have "P ≠ P'" using contra by blast
      moreover have "last xs' ∈ set P" using xs_last_edge xs'_edges ‹tl xs' ≠ []› xs'_path
        by (metis path_from_toE last_in_set subsetCE walk_edges_subset)
      moreover have "last xs' ∈ set P'" using P'(2) by (meson walk_edges_vertices(1))
      ultimately have "last xs' = v0 ∨ last xs' = v1 ∨ last xs' = new_last"
        using paths_plus_one_disjoint P'(1) P paths_with_new_def by auto
      then show False using Suc.prems(3) ‹new_last ∉ set xs'› ‹tl xs' ≠ []› xs' xs'_path
         by (metis path_from_toE butlast_snoc in_set_butlastD last_in_set last_tl path_from_to_first)
    qed
    ultimately show ?thesis by simp
  qed
qed

end ― ‹locale @{locale DisjointPathsPlusOne}›

end