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 ― ‹anonymous context› corollary contradiction: "False" using Q_hit_exists contradiction' by blast end ― ‹locale @{locale ProofStepInduct_y_neq_new_last}› end