Theory Y_eq_new_last

theory Y_eq_new_last
imports MengerInduction
section ‹The case $y = new\_last$›

theory Y_eq_new_last imports MengerInduction begin

text ‹
  We may assume @{term "y ≠ v1"} now because @{thm ProofStepInduct_NonTrivial_P_k_pre.y_eq_v1_solves}
  shows that @{term "y = v1"} already gives us @{term "Suc sep_size"} many disjoint paths.

  We also assume that we have chosen the previous paths optimally in the sense that the distance
  from @{term new_last} to @{term v1} is minimal.
›

locale ProofStepInduct_y_eq_new_last = ProofStepInduct_NonTrivial_P_k_pre +
  assumes y_neq_v1: "y ≠ v1" and y_eq_new_last: "y = new_last"
      and optimal_paths: "⋀paths' P_new'.
            ProofStepInduct G v0 v1 paths' P_new' sep_size
            ⟹ H.distance (last P_new) v1 ≤ H.distance (last P_new') v1"
begin

text ‹Let @{term R} be a shortest path from @{term new_last} to @{term v1}.›
definition R where "R ≡
  SOME R. new_last ↝R↝H v1 ∧ (∀R'. new_last ↝R'↝H v1 ⟶ length R ≤ length R')"

lemma R: "new_last ↝R↝H v1" "⋀R'. new_last ↝R'↝H v1 ⟹ length R ≤ length R'" proof-
  obtain R' where
    R': "new_last ↝R'↝H v1" "⋀R''. new_last ↝R''↝H v1 ⟹ length R' ≤ length R''"
    using arg_min_ex[OF new_last_to_v1] unfolding H_def by blast
  then show "new_last ↝R↝H v1" "⋀R'. new_last ↝R'↝H v1 ⟹ length R ≤ length R'"
    using someI[of "λR. new_last ↝R↝H v1 ∧ (∀R'. new_last ↝R'↝H v1 ⟶ length R ≤ length R')"]
      R_def by auto
qed

lemma v1_in_Q: "∃Q_hit ∈ Q. v1 ∈ set Q_hit" proof-
  obtain xs where "xs ∈ Q" using Q(2) sep_size_not0 by fastforce
  then show ?thesis using Q.paths last_in_set by blast
qed

lemma R_hits_Q: "∃z ∈ set R. Q.hitting_paths z" proof-
  have "v1 ∈ set R" using R(1) last_in_set by (metis path_from_to_def)
  then show ?thesis unfolding Q.hitting_paths_def using v0_neq_v1 by auto
qed

lemma R_decomp_exists:
  obtains R_pre z R_post
    where "R = R_pre @ z # R_post"
      and "Q.hitting_paths z"
      and "⋀z'. z' ∈ set R_pre ⟹ ¬Q.hitting_paths z'"
  using R_hits_Q split_list_first_prop[of R Q.hitting_paths] by blast

text ‹
  We open an anonymous context in order to hide all but the final lemma.  This also gives us the
  decomposition of @{term R} whose existence we established above.
›

context fixes R_pre z R_post
  assumes R_decomp: "R = R_pre @ z # R_post"
      and z: "Q.hitting_paths z"
      and z_min: "⋀z'. z' ∈ set R_pre ⟹ ¬Q.hitting_paths z'"
begin
  private lemma z_neq_v0: "z ≠ v0" using z Q.hitting_paths_def by auto

  private lemma z_neq_new_last: "z ≠ new_last" proof
    assume "z = new_last"
    then obtain Q_hit where Q_hit: "Q_hit ∈ Q" "new_last ∈ set Q_hit"
      using z Q.hitting_paths_def y_eq_new_last y_neq_v1 by auto
    then have "Q.path Q_hit" by (meson Q.paths path_from_to_def)
    then have "set Q_hit ⊆ V - {new_last}" using Q.walk_in_V H_x_def remove_vertex_V by simp
    then show False using Q_hit(2) by blast
  qed

  private lemma R_pre_neq_Nil: "R_pre ≠ Nil" using z_neq_new_last R_decomp R(1) by auto

  private lemma z_closer_than_new_last: "H.distance z v1 < H.distance new_last v1" proof-
    have "H.distance new_last v1 = length R" using H.distance_witness R by auto
    moreover have "z ↝(z # R_post)↝H v1" using R_decomp R(1)
      by (metis H.walk_decomp(2) distinct_append last_appendR list.sel(1)
          list.simps(3) path_from_to_def)
    moreover have "length R > length (z # R_post)"
      unfolding R_decomp using R_pre_neq_Nil by simp
    ultimately show ?thesis using H.distance_upper_bound by fastforce
  qed

  private definition R'_walk where "R'_walk ≡ P_k_pre @ R_pre @ [z]"

  private lemma R'_walk_not_Nil: "R'_walk ≠ Nil" using R'_walk_def R(1) by simp

  private lemma R'_walk_no_Q: "⟦ v ∈ set R'_walk; v ≠ z ⟧ ⟹ ¬Q.hitting_paths v" proof-
    fix v assume "v ∈ set R'_walk" "v ≠ z"
    moreover have "v ∈ set P_k_pre ⟹ ¬Q.hitting_paths v"
      using Q.hitting_paths_def hitting_Q_or_new_last_def y_min v1_in_Q by auto
    moreover have "v ∈ set R_pre ⟹ ¬Q.hitting_paths v" using z_min by simp
    ultimately show "¬Q.hitting_paths v" unfolding R'_walk_def using R'_walk_def by auto
  qed

  text ‹
    The original proof goes like this:
    ``Let @{term z} be the first vertex of @{term R} on some path in @{term Q}.
    Then the distance in @{term "H"} from @{term z} to @{term v1} is less than the distance
    from @{term new_last} to @{term v1}.  This contradicts the choice of @{term paths} and
    @{term P_new}.''

    It does not say exactly why it contradicts the choice of @{term paths} and @{term P_new}.
    It seems we can choose @{term Q} together with @{term R'_walk} as our new paths plus
    extrapath. But this seems to be wrong because we cannot show that @{term R'_walk} is a path:
    @{term P_k_pre} and @{term R_pre} could intersect.

    So we use @{thm walk_to_path} to transform @{term R'_walk} into a path @{term R'}.
›
  private definition R' where
    "R' ≡ SOME R'. hd (tl R'_walk) ↝R'↝ z ∧ set R' ⊆ set (tl R'_walk)"

  private lemma R': "hd (tl R'_walk) ↝R'↝ z" "set R' ⊆ set (tl R'_walk)" proof-
    have "tl R'_walk ≠ Nil" by (simp add: P_k_pre_not_Nil R'_walk_def)
    moreover have "last R'_walk = z" unfolding R'_walk_def by simp
    moreover have "walk (tl R'_walk)"
      by (metis (no_types, lifting) path_from_toE walk_tl H_def P_k_decomp R'_walk_def R(1)
          R_decomp path_P_k y_eq_new_last hd_append list.sel(1) list.simps(3) path_decomp'
          remove_vertex_path_from_to_add walk_comp walk_decomp(1) walk_last_edge)
    ultimately obtain R'' where "hd (tl R'_walk) ↝R''↝ z" "set R'' ⊆ set (tl R'_walk)"
      using walk_to_path[of "tl R'_walk" "hd (tl R'_walk)" z] last_tl by force
    then show "hd (tl R'_walk) ↝R'↝ z" "set R' ⊆ set (tl R'_walk)" unfolding R'_def
      using someI[of "λR'. hd (tl R'_walk) ↝R'↝ z ∧ set R' ⊆ set (tl R'_walk)"] by auto
  qed

  private lemma hd_R': "hd R' = hd (tl P_k)" proof-
    have "hd (tl R'_walk) = hd (tl P_k)" proof (cases)
      assume "tl P_k_pre = Nil"
      then show ?thesis unfolding R'_walk_def using P_k_decomp R(1) P_k_pre_not_Nil y_eq_new_last
        by (metis H.path_from_toE R_decomp hd_append list.sel(1) tl_append2)
    next
      assume "tl P_k_pre ≠ Nil"
      then show ?thesis unfolding R'_walk_def using P_k_pre_not_Nil by (simp add: P_k_decomp)
    qed
    then show ?thesis using R'(1) by auto
  qed

  private lemma R'_no_Q: "⟦ v ∈ set R'; v ≠ z ⟧ ⟹ ¬Q.hitting_paths v"
    using R'_walk_no_Q by (meson R'(2) R'_walk_not_Nil list.set_sel(2) subsetCE)

  private lemma v0_R'_path: "v0 ↝(v0 # R')↝ z" proof-
    have "v0→hd R'" using hd_R' hd_P_k_v0
      by (metis Nil_is_append_conv P_k_decomp P_k_pre_not_Nil path_P_k list.distinct(1)
          list.exhaust_sel path_first_edge' tl_append2)
    moreover have "v0 ∉ set R'" proof-
      have "v0 ∉ set R" using R(1) H_def H.path_in_V remove_vertex_V
        by (simp add: path_from_to_def subset_Diff_insert)
      then have "v0 ∉ set R_pre" using R_decomp by simp
      moreover have "v0 ∉ set (tl P_k_pre)" using hd_P_k_v0 path_P_k path_first_vertex
        by (metis P_k_decomp P_k_pre_not_Nil hd_append list.exhaust_sel path_decomp(1))
      ultimately show ?thesis using R'(2) unfolding R'_walk_def
        using P_k_pre_not_Nil z_neq_v0 by auto
    qed
    ultimately show ?thesis using path_cons
      by (metis R'(1) last.simps list.sel(1) list.simps(3) path_from_to_def)
  qed

  private corollary z_last_R': "z = last (v0 # R')" using v0_R'_path by auto

  private lemma z_eq_v1_solves:
    assumes "z = v1"
    shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
  proof-
    interpret Q': DisjointPaths G v0 v1 Q
      using DisjointPaths_supergraph H_x_def Q.DisjointPaths_axioms by auto
    have "v0 ↝(v0 # R')↝ v1" using assms v0_R'_path by auto
    moreover {
      fix xs v assume "xs ∈ Q" "xs ≠ v0 # R'" "v ∈ set xs" "v ∈ set (v0 # R')"
      then have "v = v0 ∨ v = v1" using R'_no_Q Q.hitting_paths_def ‹z = v1› by auto
    }
    ultimately have "DisjointPaths G v0 v1 (insert (v0 # R') Q)"
      using Q'.DisjointPaths_extend by blast
    moreover have "card (insert (v0 # R') Q) = Suc sep_size"
      by (simp add: P_k(2) Q(2) Q.finite_paths Q.second_vertices_new_path hd_R')
    ultimately show ?thesis by blast
  qed

  private lemma z_neq_v1_solves:
    assumes "z ≠ v1"
    shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
  proof-
    have "ProofStepInduct G v0 v1 Q (v0 # R') sep_size" proof (rule ProofStepInduct.intro)
      show "DisjointPathsPlusOne G v0 v1 Q (v0 # R')" proof (rule DisjointPathsPlusOne.intro)
        show "DisjointPaths G v0 v1 Q"
          using DisjointPaths_supergraph H_x_def Q.DisjointPaths_axioms by auto
        show "DisjointPathsPlusOne_axioms G v0 v1 Q (v0 # R')" proof
          show "v0 ↝(v0 # R')↝ last (v0 # R')" using v0_R'_path by blast
          show "tl (v0 # R') ≠ []" using R'(1) by auto
          show "hd (tl (v0 # R')) ∉ Q.second_vertices" using hd_R' P_k(2) by auto
          show "Q.hitting_paths (last (v0 # R'))" using z z_last_R' by auto
        next
          fix v assume "v ∈ set (butlast (v0 # R'))"
          then show "¬Q.hitting_paths v" using R'_no_Q path_from_to_last[OF v0_R'_path]
            by (metis Q.hitting_paths_def in_set_butlastD set_ConsD)
        qed
      qed
      show "ProofStepInduct_axioms Q sep_size" using sep_size_not0 Q(2) by unfold_locales
    qed (insert NoSmallSeparationsInduct_axioms)
    then have "H.distance (last P_new) v1 ≤ H.distance (last (v0 # R')) v1"
      using H_def optimal_paths[of Q "v0 # R'"] by blast
    then have False using z_last_R' new_last_def z_closer_than_new_last by simp
    then show ?thesis by blast
  qed

  corollary with_optimal_paths_solves':
    shows "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
    using optimal_paths z_eq_v1_solves z_neq_v1_solves by blast
end ― ‹anonymous context›

corollary with_optimal_paths_solves:
  "∃paths. DisjointPaths G v0 v1 paths ∧ card paths = Suc sep_size"
  using optimal_paths with_optimal_paths_solves' R_decomp_exists by blast

end ― ‹locale @{locale ProofStepInduct_y_eq_new_last}›
end