Theory Y_neq_new_last
section ‹The case $y \neq new\_last$›
theory Y_neq_new_last imports MengerInduction begin
text ‹
Let us now consider the case that @{term "y ≠ v1 ∧ y ≠ new_last"}. Our goal is to show that
this is inconsistent: The following locale will be unsatisfiable, proving that
@{term "y = v1 ∨ y = new_last"} holds.
›
locale ProofStepInduct_y_neq_new_last = ProofStepInduct_NonTrivial_P_k_pre +
assumes y_neq_v1: "y ≠ v1" and y_neq_new_last: "y ≠ new_last"
begin
lemma Q_hit_exists: obtains Q_hit Q_hit_pre Q_hit_post where
"Q_hit ∈ Q" "y ∈ set Q_hit" "Q_hit = Q_hit_pre @ y # Q_hit_post"
proof-
obtain Q_hit where "Q_hit ∈ Q" "y ∈ set Q_hit"
using hitting_Q_or_new_last_def y y_neq_v1 y_neq_new_last by auto
then show ?thesis using that by (meson split_list)
qed
text ‹
We open an anonymous context because we do not want to export any lemmas except the final lemma
proving the contradiction. This is also an easy way to get the decomposition of @{term Q_hit},
whose existence we have established above.
›
context
fixes Q_hit Q_hit_pre Q_hit_post
assumes Q_hit: "Q_hit ∈ Q" "y ∈ set Q_hit"
and Q_hit_decomp: "Q_hit = Q_hit_pre @ y # Q_hit_post"
begin
private lemma Q_hit_v0_v1: "v0 ↝Q_hit↝⇘H_x⇙ v1" using Q.paths Q_hit(1) by blast
private lemma Q_hit_vertices: "set Q_hit ⊆ V - {new_last}"
using Q.walk_in_V H_x_def path_from_to_def remove_vertex_V Q_hit_v0_v1 by fastforce
private lemma Q_hit_pre_not_Nil: "Q_hit_pre ≠ Nil"
using Q_hit_v0_v1 y_neq_v0 unfolding Q_hit_decomp by auto
private lemma tl_Q_hit_pre: "tl (Q_hit_pre @ [y]) ≠ Nil" using Q_hit_pre_not_Nil by simp
private lemma Q_hit_pre_edges: "edges_of_walk (Q_hit_pre @ [y]) ∩ B ≠ {}" proof
assume "edges_of_walk (Q_hit_pre @ [y]) ∩ B = {}"
moreover have "edges_of_walk (Q_hit_pre @ [y]) ⊆ E"
by (metis Q.paths H_x_def Q_hit(1) Q_hit_decomp edges_of_walk_in_E path_decomp'
path_from_to_def remove_vertex_walk_add)
ultimately have Q_hit_pre_edges:
"edges_of_walk (Q_hit_pre @ [y]) ⊆ ⋃(edges_of_walk ` paths_with_new)"
unfolding B_def by blast
then have *: "first_edge_of_walk (Q_hit_pre @ [y]) ∈ ⋃(edges_of_walk ` paths_with_new)"
using tl_Q_hit_pre first_edge_in_edges by blast
define v' where "v' ≡ hd (tl (Q_hit_pre @ [y]))"
then have v': "(v0, v') = first_edge_of_walk (Q_hit_pre @ [y])"
using first_edge_hd_tl Q_hit_pre_not_Nil tl_Q_hit_pre
by (metis Q.path_from_toE Q_hit_decomp Q_hit_v0_v1 first_edge_of_walk.simps(1)
hd_Cons_tl hd_append snoc_eq_iff_butlast)
then obtain P_i where
P_i: "P_i ∈ paths_with_new" "(v0, v') ∈ edges_of_walk P_i" using * by auto
then have P_i_first: "first_edge_of_walk P_i = (v0, v')"
using first_edge_first paths_with_new_def paths P_new by (metis insert_iff)
moreover have "first_edge_of_walk P_k = (v0, hd (tl P_k))"
by (metis P_k_decomp P_k_pre_not_Nil append_is_Nil_conv first_edge_of_walk.simps(1)
hd_P_k_v0 list.distinct(1) list.exhaust_sel tl_append2)
ultimately have "P_i ≠ P_k"
by (metis Q.first_edge_first P_k(2) Q.second_vertices_first_edge Q_hit(1) Q_hit_decomp
Q_hit_v0_v1 Un_iff v' tl_Q_hit_pre first_edge_in_edges walk_edges_decomp)
text ‹
Then @{term P_k} and @{term P_i} intersect in @{term y}, which is not one of @{term v0},
@{term v1}, or @{term new_last}. So we get a contradiction because these two paths should be
disjoint on all other vertices.
›
moreover have "v1 ∉ set (Q_hit_pre @ [y])"
using Q_hit_v0_v1 Q_hit_decomp y_neq_v1 by (simp add: Q.path_from_to_last')
moreover have "new_last ∉ set (Q_hit_pre @ [y])" proof-
have "new_last ∉ set Q_hit_pre" using Q_hit_decomp Q_hit_vertices by auto
then show ?thesis using y_neq_new_last by auto
qed
moreover have "hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)" proof-
have "hd (tl P_i) = v'" using P_i_first P_i(1) tl_P_new(1)
by (metis Pair_inject first_edge_of_walk.simps(1) insert_iff list.collapse
paths_tl_notnil paths_with_new_def tl_Nil)
then show ?thesis using v'_def by simp
qed
moreover have "v0 ↝(Q_hit_pre @ [y])↝ y"
by (metis Q.path_decomp' H_x_def Q_hit_decomp Q_hit_v0_v1 Q_hit_pre_not_Nil
hd_append2 path_from_to_def remove_vertex_walk_add snoc_eq_iff_butlast)
ultimately have "edges_of_walk (Q_hit_pre @ [y]) ⊆ edges_of_walk P_i"
using new_path_follows_old_paths tl_Q_hit_pre P_i(1) Q_hit_pre_edges by blast
from walk_edges_subset[OF this] have "y ∈ set P_i" by (simp add: tl_Q_hit_pre)
moreover have "y ∈ set P_k" using P_k_decomp by auto
ultimately show False
using y_neq_v0 y_neq_v1 y_neq_new_last ‹P_i ≠ P_k›
paths_plus_one_disjoint[OF P_i(1), of P_k y] P_k(1) P_new_decomp by auto
qed
private lemma P_k_pre_edges: "edges_of_walk (P_k_pre @ [y]) ∩ B = {}" proof-
have "edges_of_walk (P_k_pre @ [y]) ⊆ ⋃(edges_of_walk ` paths_with_new)"
proof (cases)
assume "P_k = P_new"
then have "edges_of_walk (P_k_pre @ [y]) ⊆ edges_of_walk P_new"
using P_k_decomp edges_of_comp1 by force
then show ?thesis unfolding paths_with_new_def by blast
next
assume "P_k ≠ P_new"
then have "P_k ∈ paths" using P_k(1) paths_with_new_def by blast
then have "edges_of_walk (P_k_pre @ [y]) ⊆ ⋃(edges_of_walk ` paths)"
using edges_of_comp1[of "P_k_pre @ [y]"] P_k_decomp by auto
then show ?thesis unfolding paths_with_new_def by blast
qed
then show ?thesis unfolding B_def by blast
qed
private definition Q_hit' where "Q_hit' ≡ P_k_pre @ y # Q_hit_post"
private lemma Q_hit'_v0_v1: "v0 ↝Q_hit'↝ v1" proof-
{
fix v assume "v ∈ set P_k_pre"
then have "¬Q.hitting_paths v" using Q.paths Q_hit(1) y_min
by (metis Q.hitting_paths_def hitting_Q_or_new_last_def last_in_set path_from_to_def)
moreover have "v0 ∉ set Q_hit_post" using Q.path_from_to_first' Q_hit_v0_v1
unfolding Q_hit_decomp by blast
ultimately have "v ∉ set Q_hit_post" unfolding Q.hitting_paths_def
using Q_hit(1) Q_hit_decomp by auto
}
then have "set P_k_pre ∩ set Q_hit_post = {}" by blast
then show ?thesis unfolding Q_hit'_def using path_from_to_combine
by (metis H_x_def P_k_decomp P_k_pre_not_Nil Q_hit_decomp Q_hit_v0_v1 append_is_Nil_conv
hd_P_k_v0 path_P_k path_from_toI remove_vertex_path_from_to_add)
qed
private lemma Q_hit'_v0_v1_H_x: "v0 ↝Q_hit'↝⇘H_x⇙ v1" proof-
have "new_last ∉ set P_k_pre" using new_last_neq_v0 hitting_Q_or_new_last_def y_min by auto
moreover have "new_last ∉ set Q_hit_post" using Q_hit_vertices unfolding Q_hit_decomp by auto
ultimately have "new_last ∉ set Q_hit'" using y_neq_new_last Q_hit'_def by auto
then show ?thesis using remove_vertex_path_from_to[OF Q_hit'_v0_v1] H_x_def new_last_in_V by simp
qed
private definition Q' where "Q' ≡ insert Q_hit' (Q - {Q_hit})"
private lemma Q_hit_edges_disjoint:
"⋃(edges_of_walk ` (Q - {Q_hit})) ∩ edges_of_walk Q_hit = {}"
using DiffD1 Q.paths_edge_disjoint Q_hit(1) by fastforce
private lemma Q_hit'_notin_Q_minus_Q_hit: "Q_hit' ∉ Q - {Q_hit}" proof-
have "hd (tl Q_hit') ∉ Q.second_vertices" using P_k(2) P_k_decomp
by (metis P_k_pre_not_Nil Q_hit'_def append_eq_append_conv2 append_self_conv hd_append2
list.sel(1) tl_append2)
then show ?thesis using Q.second_vertices_new_path[of Q_hit'] by blast
qed
private lemma Q_weight_smaller: "Q_weight Q' < Q_weight Q" proof-
define Q_edges where "Q_edges ≡ ⋃(edges_of_walk ` Q) ∩ B"
define Q'_edges where "Q'_edges ≡ ⋃(edges_of_walk ` Q') ∩ B"
{
fix v w assume *: "(v,w) ∈ Q'_edges" "(v,w) ∉ Q_edges"
then have v_w_in_B: "(v,w) ∈ B" unfolding Q'_edges_def by blast
obtain Q'_v_w_witness where Q'_v_w_witness:
"Q'_v_w_witness ∈ Q'" "(v,w) ∈ edges_of_walk Q'_v_w_witness"
using *(1) unfolding Q'_edges_def by blast
have "Q'_v_w_witness ≠ Q_hit'" proof
assume "Q'_v_w_witness = Q_hit'"
then have "edges_of_walk Q'_v_w_witness =
edges_of_walk (P_k_pre @ [y]) ∪ edges_of_walk (y # Q_hit_post)"
unfolding Q_hit'_def using walk_edges_decomp[of P_k_pre y Q_hit_post] by simp
moreover have "(v,w) ∉ edges_of_walk (P_k_pre @ [y])"
using P_k_pre_edges v_w_in_B by blast
moreover have "(v,w) ∉ edges_of_walk (y # Q_hit_post)" proof
assume "(v,w) ∈ edges_of_walk (y # Q_hit_post)"
then have "(v,w) ∈ edges_of_walk Q_hit"
unfolding Q_hit_decomp by (metis UnCI walk_edges_decomp)
then show False using *(2) v_w_in_B Q_hit(1) unfolding Q_edges_def by blast
qed
ultimately show False using Q'_v_w_witness(2) by blast
qed
then have "Q'_v_w_witness ∈ Q" using Q'_v_w_witness(1) unfolding Q'_def by blast
then have False using *(2) v_w_in_B Q'_v_w_witness(2) unfolding Q_edges_def by blast
}
moreover have "∃e ∈ Q_edges. e ∉ Q'_edges" proof-
obtain v w where v_w: "(v,w) ∈ edges_of_walk (Q_hit_pre @ [y]) ∩ B"
using Q_hit_pre_edges by auto
then have v_w_in_Q_hit: "(v,w) ∈ edges_of_walk Q_hit ∩ B" unfolding Q_hit_decomp
by (metis Int_iff UnCI walk_edges_decomp)
then have "(v,w) ∈ Q_edges" unfolding Q_edges_def using Q_hit(1) by blast
moreover have "(v,w) ∉ Q'_edges" proof
assume "(v,w) ∈ Q'_edges"
then have "(v,w) ∈ edges_of_walk Q_hit'" unfolding Q'_edges_def Q'_def
using IntD1 v_w_in_Q_hit Q_hit_edges_disjoint by auto
then have "(v,w) ∈ edges_of_walk (y # Q_hit_post)" unfolding Q_hit'_def
using v_w P_k_pre_edges
by (metis (no_types, lifting) IntD2 UnE disjoint_iff_not_equal walk_edges_decomp)
then show False using v_w Q_hit(1) Q.paths Q_hit_decomp
by (metis DiffE Q.path_edges_remove_prefix IntD1 path_from_to_def)
qed
ultimately show ?thesis by blast
qed
moreover have "finite Q_edges" unfolding Q_edges_def B_def by simp
moreover have "finite Q'_edges" unfolding Q'_edges_def B_def by simp
ultimately have "card Q'_edges < card Q_edges" by (metis card_seteq not_le subrelI)
then have "card (⋃(edges_of_walk ` Q') ∩ B) < card (⋃(edges_of_walk ` Q) ∩ B)"
unfolding Q_edges_def Q'_edges_def by blast
then show ?thesis unfolding Q_weight_def by blast
qed
private lemma DisjointPaths_Q': "DisjointPaths H_x v0 v1 Q'" proof-
interpret Q_reduced: DisjointPaths H_x v0 v1 "Q - {Q_hit}"
using Q.DisjointPaths_reduce[of "Q - {Q_hit}"] by blast
{
fix xs v
assume xs: "xs ∈ Q - {Q_hit}"
and v: "v ∈ set xs" "v ∈ set Q_hit'" "v ≠ v0" "v ≠ v1"
have "v ∉ set P_k_pre" proof
assume "v ∈ set P_k_pre"
then have "¬hitting_Q_or_new_last v" using y_min by blast
moreover have "v ≠ new_last" using v(2) calculation hitting_Q_or_new_last_def v(3) by auto
ultimately show False unfolding hitting_Q_or_new_last_def using v(1,3) xs by blast
qed
moreover have "v ≠ y"
by (metis DiffE Q.paths_disjoint Q_hit y_neq_v0 y_neq_v1 insert_iff v(1) xs)
moreover have "v ∉ set Q_hit_post" proof
assume "v ∈ set Q_hit_post"
then have "v ∈ set Q_hit" unfolding Q_hit_decomp by simp
then show False using Q.paths_disjoint[of Q_hit xs] xs Q_hit(1) v by blast
qed
ultimately have False using v(2) unfolding Q_hit'_def by simp
}
then show ?thesis using Q_reduced.DisjointPaths_extend Q_hit'_v0_v1_H_x
unfolding Q'_def by blast
qed
private lemma card_Q': "card Q' = sep_size" proof-
have "Suc (card (Q - {Q_hit})) = card Q"
using Q_hit(1) Q.finite_paths by (meson card_Suc_Diff1)
then show ?thesis using Q(2) Q.finite_paths Q_hit'_notin_Q_minus_Q_hit
unfolding Q'_def by simp
qed
lemma contradiction': "False" using Q_weight_smaller DisjointPaths_Q' card_Q' Q_min
using Suc_leI not_less_eq_eq by blast
end
corollary contradiction: "False" using Q_hit_exists contradiction' by blast
end
end