Theory Y_eq_new_last
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
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
end