(* Title: Schutz_Spacetime/TemporalOrderOnPath.thy Authors: Richard Schmoetten, Jake Palmer and Jacques D. Fleuriot University of Edinburgh, 2021 *) theory TemporalOrderOnPath imports Minkowski "HOL-Library.Disjoint_Sets" begin text ‹ In Schutz \<^cite>‹‹pp.~18-30› in "schutz1997"›, this is ``Chapter 3: Temporal order on a path''. All theorems are from Schutz, all lemmas are either parts of the Schutz proofs extracted, or additional lemmas which needed to be added, with the exception of the three transitivity lemmas leading to Theorem 9, which are given by Schutz as well. Much of what we'd like to prove about chains with respect to injectivity, surjectivity, bijectivity, is proved in ‹TernaryOrdering.thy›. Some more things are proved in interlude sections. › section "Preliminary Results for Primitives" text ‹ First some proofs that belong in this section but aren't proved in the book or are covered but in a different form or off-handed remark. › context MinkowskiPrimitive begin lemma cross_once_notin: assumes "Q ∈ 𝒫" and "R ∈ 𝒫" and "a ∈ Q" and "b ∈ Q" and "b ∈ R" and "a ≠ b" and "Q ≠ R" shows "a ∉ R" using assms paths_cross_once eq_paths by meson lemma paths_cross_at: assumes path_Q: "Q ∈ 𝒫" and path_R: "R ∈ 𝒫" and Q_neq_R: "Q ≠ R" and QR_nonempty: "Q ∩ R ≠ {}" and x_inQ: "x ∈ Q" and x_inR: "x ∈ R" shows "Q ∩ R = {x}" proof (rule equalityI) show "Q ∩ R ⊆ {x}" proof (rule subsetI, rule ccontr) fix y assume y_in_QR: "y ∈ Q ∩ R" and y_not_in_just_x: "y ∉ {x}" then have y_neq_x: "y ≠ x" by simp then have "¬ (∃z. Q ∩ R = {z})" by (meson Q_neq_R path_Q path_R x_inQ x_inR y_in_QR cross_once_notin IntD1 IntD2) thus False using paths_cross_once by (meson QR_nonempty Q_neq_R path_Q path_R) qed show "{x} ⊆ Q ∩ R" using x_inQ x_inR by simp qed lemma events_distinct_paths: assumes a_event: "a ∈ ℰ" and b_event: "b ∈ ℰ" and a_neq_b: "a ≠ b" shows "∃R∈𝒫. ∃S∈𝒫. a ∈ R ∧ b ∈ S ∧ (R ≠ S ⟶ (∃!c∈ℰ. R ∩ S = {c}))" by (metis events_paths assms paths_cross_once) end (* context MinkowskiPrimitive *) context MinkowskiBetweenness begin lemma assumes "[a;b;c]" shows "∃f. local_long_ch_by_ord f {a,b,c}" using abc_abc_neq[OF assms] unfolding chain_defs by (simp add: assms ord_ordered_loc) lemma between_chain: "[a;b;c] ⟹ ch {a,b,c}" proof - assume "[a;b;c]" hence "∃f. local_ordering f betw {a,b,c}" by (simp add: abc_abc_neq ord_ordered_loc) hence "∃f. local_long_ch_by_ord f {a,b,c}" using ‹[a;b;c]› abc_abc_neq local_long_ch_by_ord_def by auto thus ?thesis by (simp add: chain_defs) qed end (* context MinkowskiBetweenness *) section "3.1 Order on a finite chain" context MinkowskiBetweenness begin subsection ‹Theorem 1› text ‹ See ‹Minkowski.abc_only_cba›. Proving it again here to show it can be done following the prose in Schutz. › theorem theorem1 [no_atp]: assumes abc: "[a;b;c]" shows "[c;b;a] ∧ ¬ [b;c;a] ∧ ¬ [c;a;b]" proof - (* (i) *) have part_i: "[c;b;a]" using abc abc_sym by simp (* (ii) *) have part_ii: "¬ [b;c;a]" proof (rule notI) assume "[b;c;a]" then have "[a;b;a]" using abc abc_bcd_abd by blast thus False using abc_ac_neq by blast qed (* (iii) *) have part_iii: "¬ [c;a;b]" proof (rule notI) assume "[c;a;b]" then have "[c;a;c]" using abc abc_bcd_abd by blast thus False using abc_ac_neq by blast qed thus ?thesis using part_i part_ii part_iii by auto qed subsection ‹Theorem 2› text ‹ The lemma ‹abc_bcd_acd›, equal to the start of Schutz's proof, is given in ‹Minkowski› in order to prove some equivalences. We're splitting up Theorem 2 into two named results: \begin{itemize} \item[‹order_finite_chain›] there is a betweenness relation for each triple of adjacent events, and \item[‹index_injective›] all events of a chain are distinct. \end{itemize} We will be following Schutz' proof for both. Distinctness of chain events is interpreted as injectivity of the indexing function (see ‹index_injective›): we assume that this corresponds to what Schutz means by distinctness of elements in a sequence. › text ‹ For the case of two-element chains: the elements are distinct by definition, and the statement on \<^term>‹local_ordering› is void (respectively, \<^term>‹False ⟹ P› for any \<^term>‹P›). We exclude this case from our proof of ‹order_finite_chain›. Two helper lemmas are provided, each capturing one of the proofs by induction in Schutz' writing. › lemma thm2_ind1: assumes chX: "local_long_ch_by_ord f X" and finiteX: "finite X" shows "∀j i. ((i::nat) < j ∧ j < card X - 1) ⟶ [f i; f j; f (j + 1)]" proof (rule allI)+ let ?P = "λ i j. [f i; f j; f (j+1)]" fix i j show "(i<j ∧ j<card X -1) ⟶ ?P i j" proof (induct j) case 0 (* this assumption is False, so easy *) show ?case by blast next case (Suc j) show ?case proof (clarify) assume asm: "i<Suc j" "Suc j<card X -1" have pj: "?P j (Suc j)" using asm(2) chX less_diff_conv local_long_ch_by_ord_def local_ordering_def by (metis Suc_eq_plus1) have "i<j ∨ i=j" using asm(1) by linarith thus "?P i (Suc j)" proof assume "i=j" hence "Suc i = Suc j ∧ Suc (Suc j) = Suc (Suc j)" by simp thus "?P i (Suc j)" using pj by auto next assume "i<j" have "j < card X - 1" using asm(2) by linarith thus "?P i (Suc j)" using ‹i<j› Suc.hyps asm(1) asm(2) chX finiteX Suc_eq_plus1 abc_bcd_acd pj by presburger qed qed qed qed lemma thm2_ind2: assumes chX: "local_long_ch_by_ord f X" and finiteX: "finite X" shows "∀m l. (0<(l-m) ∧ (l-m) < l ∧ l < card X) ⟶ [f (l-m-1); f (l-m); (f l)]" proof (rule allI)+ fix l m let ?P = "λ k l. [f (k-1); f k; f l]" let ?n = "card X" let ?k = "(l::nat)-m" show "0 < ?k ∧ ?k < l ∧ l < ?n ⟶ ?P ?k l" proof (induct m) case 0 (* yet again, this assumption is False, so easy *) show ?case by simp next case (Suc m) show ?case proof (clarify) assume asm: "0 < l - Suc m" "l - Suc m < l" "l < ?n" have "Suc m = 1 ∨ Suc m > 1" by linarith thus "[f (l - Suc m - 1); f (l - Suc m); f l]" (is ?goal) proof assume "Suc m = 1" show ?goal proof - have "l - Suc m < card X" using asm(2) asm(3) less_trans by blast then show ?thesis using ‹Suc m = 1› asm finiteX thm2_ind1 chX using Suc_eq_plus1 add_diff_inverse_nat diff_Suc_less gr_implies_not_zero less_one plus_1_eq_Suc by (smt local_long_ch_by_ord_def ordering_ord_ijk_loc) qed next assume "Suc m > 1" show ?goal apply (rule_tac a="f l" and c="f(l - Suc m - 1)" in abc_sym) apply (rule_tac a="f l" and c="f(l-Suc m)" and d="f(l-Suc m-1)" and b="f(l-m)" in abc_bcd_acd) proof - have "[f(l-m-1); f(l-m); f l]" using Suc.hyps ‹1 < Suc m› asm(1,3) by force thus "[f l; f(l - m); f(l - Suc m)]" using abc_sym One_nat_def diff_zero minus_nat.simps(2) by metis have "Suc(l - Suc m - 1) = l - Suc m" "Suc(l - Suc m) = l-m" using Suc_pred asm(1) by presburger+ hence "[f(l - Suc m - 1); f(l - Suc m); f(l - m)]" using chX unfolding local_long_ch_by_ord_def local_ordering_def by (metis asm(2,3) less_trans_Suc) thus "[f(l - m); f(l - Suc m); f(l - Suc m - 1)]" using abc_sym by blast qed qed qed qed qed lemma thm2_ind2b: assumes chX: "local_long_ch_by_ord f X" and finiteX: "finite X" and ordered_nats: "0<k ∧ k<l ∧ l < card X" shows "[f (k-1); f k; f l]" using thm2_ind2 finiteX chX ordered_nats by (metis diff_diff_cancel less_imp_le) text ‹ This is Theorem 2 properly speaking, except for the "chain elements are distinct" part (which is proved as injectivity of the index later). Follows Schutz fairly well! The statement Schutz proves under (i) is given in ‹MinkowskiBetweenness.abc_bcd_acd› instead. › theorem (*2*) order_finite_chain: assumes chX: "local_long_ch_by_ord f X" and finiteX: "finite X" and ordered_nats: "0 ≤ (i::nat) ∧ i < j ∧ j < l ∧ l < card X" shows "[f i; f j; f l]" proof - let ?n = "card X - 1" have ord1: "0≤i ∧ i<j ∧ j<?n" using ordered_nats by linarith have e2: "[f i; f j; f (j+1)]" using thm2_ind1 using Suc_eq_plus1 chX finiteX ord1 by presburger have e3: "∀k. 0<k ∧ k<l ⟶ [f (k-1); f k; f l]" using thm2_ind2b chX finiteX ordered_nats by blast have "j<l-1 ∨ j=l-1" using ordered_nats by linarith thus ?thesis proof assume "j<l-1" have "[f j; f (j+1); f l]" using e3 abc_abc_neq ordered_nats using ‹j < l - 1› less_diff_conv by auto thus ?thesis using e2 abc_bcd_abd by blast next assume "j=l-1" thus ?thesis using e2 using ordered_nats by auto qed qed corollary (*2*) order_finite_chain2: assumes chX: "[f↝X]" and finiteX: "finite X" and ordered_nats: "0 ≤ (i::nat) ∧ i < j ∧ j < l ∧ l < card X" shows "[f i; f j; f l]" proof - have "card X > 2" using ordered_nats by (simp add: eval_nat_numeral) thus ?thesis using order_finite_chain chain_defs short_ch_card(1) by (metis assms nat_neq_iff) qed theorem (*2ii*) index_injective: fixes i::nat and j::nat assumes chX: "local_long_ch_by_ord f X" and finiteX: "finite X" and indices: "i<j" "j<card X" shows "f i ≠ f j" proof (cases) assume "Suc i < j" then have "[f i; f (Suc(i)); f j]" using order_finite_chain chX finiteX indices(2) by blast then show ?thesis using abc_abc_neq by blast next assume "¬Suc i < j" hence "Suc i = j" using Suc_lessI indices(1) by blast show ?thesis proof (cases) assume "Suc j = card X" then have "0<i" proof - have "card X ≥ 3" using assms(1) finiteX long_chain_card_geq by blast thus ?thesis using ‹Suc i = j› ‹Suc j = card X› by linarith qed then have "[f 0; f i; f j]" using assms order_finite_chain by blast thus ?thesis using abc_abc_neq by blast next assume "¬Suc j = card X" then have "Suc j < card X" using Suc_lessI indices(2) by blast then have "[f i; f j; f(Suc j)]" using chX finiteX indices(1) order_finite_chain by blast thus ?thesis using abc_abc_neq by blast qed qed theorem (*2ii*) index_injective2: fixes i::nat and j::nat assumes chX: "[f↝X]" and finiteX: "finite X" and indices: "i<j" "j<card X" shows "f i ≠ f j" using assms(1) unfolding ch_by_ord_def proof (rule disjE) assume asm: "short_ch_by_ord f X" hence "card X = 2" using short_ch_card(1) by simp hence "j=1" "i=0" using indices plus_1_eq_Suc by auto thus ?thesis using asm unfolding chain_defs by force next assume "local_long_ch_by_ord f X" thus ?thesis using index_injective assms by presburger qed text ‹ Surjectivity of the index function is easily derived from the definition of ‹local_ordering›, so we obtain bijectivity as an easy corollary to the second part of Theorem 2. › corollary index_bij_betw: assumes chX: "local_long_ch_by_ord f X" and finiteX: "finite X" shows "bij_betw f {0..<card X} X" proof (unfold bij_betw_def, (rule conjI)) show "inj_on f {0..<card X}" using index_injective[OF assms] by (metis (mono_tags) atLeastLessThan_iff inj_onI nat_neq_iff) { fix n assume "n ∈ {0..<card X}" then have "f n ∈ X" using assms unfolding chain_defs local_ordering_def by auto } moreover { fix x assume "x ∈ X" then have "∃n ∈ {0..<card X}. f n = x" using assms unfolding chain_defs local_ordering_def using atLeastLessThan_iff bot_nat_0.extremum by blast } ultimately show "f ` {0..<card X} = X" by blast qed corollary index_bij_betw2: assumes chX: "[f↝X]" and finiteX: "finite X" shows "bij_betw f {0..<card X} X" using assms(1) unfolding ch_by_ord_def proof (rule disjE) assume "local_long_ch_by_ord f X" thus "bij_betw f {0..<card X} X" using index_bij_betw assms by presburger next assume asm: "short_ch_by_ord f X" show "bij_betw f {0..<card X} X" proof (unfold bij_betw_def, (rule conjI)) show "inj_on f {0..<card X}" using index_injective2[OF assms] by (metis (mono_tags) atLeastLessThan_iff inj_onI nat_neq_iff) { fix n assume asm2: "n ∈ {0..<card X}" have "f n ∈ X" using asm asm2 short_ch_card(1) apply (simp add: eval_nat_numeral) by (metis One_nat_def less_Suc0 less_antisym short_ch_ord_in) } moreover { fix x assume asm2: "x ∈ X" have "∃n ∈ {0..<card X}. f n = x" using short_ch_card(1) short_ch_by_ord_def asm asm2 atLeast0_lessThan_Suc by (auto simp: eval_nat_numeral)[1] } ultimately show "f ` {0..<card X} = X" by blast qed qed subsection "Additional lemmas about chains" lemma first_neq_last: assumes "[f↝Q|x..z]" shows "x≠z" apply (cases rule: finite_chain_with_cases[OF assms]) using chain_defs apply (metis Suc_1 card_2_iff diff_Suc_1) using index_injective[of f Q 0 "card Q - 1"] by (metis card.infinite diff_is_0_eq diff_less gr0I le_trans less_imp_le_nat less_numeral_extra(1) numeral_le_one_iff semiring_norm(70)) lemma index_middle_element: assumes "[f↝X|a..b..c]" shows "∃n. 0<n ∧ n<(card X - 1) ∧ f n = b" proof - obtain n where n_def: "n < card X" "f n = b" using local_ordering_def assms chain_defs by (metis two_ordered_loc) have "0<n ∧ n<(card X - 1) ∧ f n = b" using assms chain_defs n_def by (metis (no_types, lifting) Suc_pred' gr_implies_not0 less_SucE not_gr_zero) thus ?thesis by blast qed text ‹ Another corollary to Theorem 2, without mentioning indices. › corollary fin_ch_betw: "[f↝X|a..b..c] ⟹ [a;b;c]" using order_finite_chain2 index_middle_element using finite_chain_def finite_chain_with_def finite_long_chain_with_def by (metis (no_types, lifting) card_gt_0_iff diff_less empty_iff le_eq_less_or_eq less_one) lemma long_chain_2_imp_3: "⟦[f↝X|a..c]; card X > 2⟧ ⟹ ∃b. [f↝X|a..b..c]" using points_in_chain first_neq_last finite_long_chain_with_def by (metis card_2_iff' numeral_less_iff semiring_norm(75,78)) lemma finite_chain2_betw: "⟦[f↝X|a..c]; card X > 2⟧ ⟹ ∃b. [a;b;c]" using fin_ch_betw long_chain_2_imp_3 by metis lemma finite_long_chain_with_alt [chain_alts]: "[f↝Q|x..y..z] ⟷ [f↝Q|x..z] ∧ [x;y;z] ∧ y∈Q" proof { assume "[f↝Q|x .. z] ∧ [x;y;z] ∧ y∈Q" thus "[f↝Q|x..y..z]" using abc_abc_neq finite_long_chain_with_def by blast } { assume asm: "[f↝Q|x..y..z]" show "[f↝Q|x .. z] ∧ [x;y;z] ∧ y∈Q" using asm fin_ch_betw finite_long_chain_with_def by blast } qed lemma finite_long_chain_with_card: "[f↝Q|x..y..z] ⟹ card Q ≥ 3" unfolding chain_defs numeral_3_eq_3 by fastforce lemma finite_long_chain_with_alt2: assumes "finite Q" "local_long_ch_by_ord f Q" "f 0 = x" "f (card Q - 1) = z" "[x;y;z] ∧ y∈Q" shows "[f↝Q|x..y..z]" using assms finite_chain_alt finite_chain_with_def finite_long_chain_with_alt by blast lemma finite_long_chain_with_alt3: assumes "finite Q" "local_long_ch_by_ord f Q" "f 0 = x" "f (card Q - 1) = z" "y≠x ∧ y≠z ∧ y∈Q" shows "[f↝Q|x..y..z]" using assms finite_chain_alt finite_chain_with_def finite_long_chain_with_def by auto lemma chain_sym_obtain: assumes "[f↝X|a..b..c]" obtains g where "[g↝X|c..b..a]" and "g=(λn. f (card X - 1 - n))" using ordering_sym_loc[of betw X f] abc_sym assms unfolding chain_defs using first_neq_last points_in_long_chain(3) by (metis assms diff_self_eq_0 empty_iff finite_long_chain_with_def insert_iff minus_nat.diff_0) lemma chain_sym: assumes "[f↝X|a..b..c]" shows "[λn. f (card X - 1 - n)↝X|c..b..a]" using chain_sym_obtain [where f=f and a=a and b=b and c=c and X=X] using assms(1) by blast lemma chain_sym2: assumes "[f↝X|a..c]" shows "[λn. f (card X - 1 - n)↝X|c..a]" proof - { assume asm: "a = f 0" "c = f (card X - 1)" and asm_short: "short_ch_by_ord f X" hence cardX: "card X = 2" using short_ch_card(1) by auto hence ac: "f 0 = a" "f 1 = c" by (simp add: asm)+ have "n=1 ∨ n=0" if "n<card X" for n using cardX that by linarith hence fn_eq: "(λn. if n = 0 then f 1 else f 0) = (λn. f (card X - Suc n))" if "n<card X" for n by (metis One_nat_def Zero_not_Suc ac(2) asm(2) not_gr_zero old.nat.inject zero_less_diff) have "c = f (card X - 1 - 0)" and "a = f (card X - 1 - (card X - 1))" and "short_ch_by_ord (λn. f (card X - 1 - n)) X" apply (simp add: asm)+ using short_ch_sym[OF asm_short] fn_eq ‹f 1 = c› asm(2) short_ch_by_ord_def by fastforce } consider "short_ch_by_ord f X"|"∃b. [f↝X|a..b..c]" using assms long_chain_2_imp_3 finite_chain_with_alt by fastforce thus ?thesis apply cases using ‹⟦a=f 0; c=f (card X-1); short_ch_by_ord f X⟧ ⟹ short_ch_by_ord (λn. f (card X -1-n)) X› assms finite_chain_alt finite_chain_with_def apply auto[1] using chain_sym finite_long_chain_with_alt by blast qed lemma chain_sym_obtain2: assumes "[f↝X|a..c]" obtains g where "[g↝X|c..a]" and "g=(λn. f (card X - 1 - n))" using assms chain_sym2 by auto end (* context MinkowskiBetweenness *) section "Preliminary Results for Kinematic Triangles and Paths/Betweenness" text ‹ Theorem 3 (collinearity) First we prove some lemmas that will be very helpful. › context MinkowskiPrimitive begin lemma triangle_permutes [no_atp]: assumes "△ a b c" shows "△ a c b" "△ b a c" "△ b c a" "△ c a b" "△ c b a" using assms by (auto simp add: kinematic_triangle_def)+ lemma triangle_paths [no_atp]: assumes tri_abc: "△ a b c" shows "path_ex a b" "path_ex a c" "path_ex b c" using tri_abc by (auto simp add: kinematic_triangle_def)+ lemma triangle_paths_unique: assumes tri_abc: "△ a b c" shows "∃!ab. path ab a b" using path_unique tri_abc triangle_paths(1) by auto text ‹ The definition of the kinematic triangle says that there exist paths that $a$ and $b$ pass through, and $a$ and $c$ pass through etc that are not equal. But we can show there is a \emph{unique} $ab$ that $a$ and $b$ pass through, and assuming there is a path $abc$ that $a, b, c$ pass through, it must be unique. Therefore ‹ab = abc› and ‹ac = abc›, but ‹ab ≠ ac›, therefore ‹False›. Lemma ‹tri_three_paths› is not in the books but might simplify some path obtaining. › lemma triangle_diff_paths: assumes tri_abc: "△ a b c" shows "¬ (∃Q∈𝒫. a ∈ Q ∧ b ∈ Q ∧ c ∈ Q)" proof (rule notI) assume not_thesis: "∃Q∈𝒫. a ∈ Q ∧ b ∈ Q ∧ c ∈ Q" (* First show [abc] or similar so I can show the path through abc is unique. *) then obtain abc where path_abc: "abc ∈ 𝒫 ∧ a ∈ abc ∧ b ∈ abc ∧ c ∈ abc" by auto have abc_neq: "a ≠ b ∧ a ≠ c ∧ b ≠ c" using tri_abc kinematic_triangle_def by simp (* Now extract some information from △ a b c. *) have "∃ab∈𝒫. ∃ac∈𝒫. ab ≠ ac ∧ a ∈ ab ∧ b ∈ ab ∧ a ∈ ac ∧ c ∈ ac" using tri_abc kinematic_triangle_def by metis then obtain ab ac where ab_ac_relate: "ab ∈ 𝒫 ∧ ac ∈ 𝒫 ∧ ab ≠ ac ∧ {a,b} ⊆ ab ∧ {a,c} ⊆ ac" by blast have "∃!ab∈𝒫. a ∈ ab ∧ b ∈ ab" using tri_abc triangle_paths_unique by blast then have ab_eq_abc: "ab = abc" using path_abc ab_ac_relate by auto have "∃!ac∈𝒫. a ∈ ac ∧ b ∈ ac" using tri_abc triangle_paths_unique by blast then have ac_eq_abc: "ac = abc" using path_abc ab_ac_relate eq_paths abc_neq by auto have "ab = ac" using ab_eq_abc ac_eq_abc by simp thus False using ab_ac_relate by simp qed lemma tri_three_paths [elim]: assumes tri_abc: "△ a b c" shows "∃ab bc ca. path ab a b ∧ path bc b c ∧ path ca c a ∧ ab ≠ bc ∧ ab ≠ ca ∧ bc ≠ ca" using tri_abc triangle_diff_paths triangle_paths(2,3) triangle_paths_unique by fastforce lemma triangle_paths_neq: assumes tri_abc: "△ a b c" and path_ab: "path ab a b" and path_ac: "path ac a c" shows "ab ≠ ac" using assms triangle_diff_paths by blast end (*context MinkowskiPrimitive*) context MinkowskiBetweenness begin lemma abc_ex_path_unique: assumes abc: "[a;b;c]" shows "∃!Q∈𝒫. a ∈ Q ∧ b ∈ Q ∧ c ∈ Q" proof - have a_neq_c: "a ≠ c" using abc_ac_neq abc by simp have "∃Q∈𝒫. a ∈ Q ∧ b ∈ Q ∧ c ∈ Q" using abc_ex_path abc by simp then obtain P Q where path_P: "P ∈ 𝒫" and abc_inP: "a ∈ P ∧ b ∈ P ∧ c ∈ P" and path_Q: "Q ∈ 𝒫" and abc_in_Q: "a ∈ Q ∧ b ∈ Q ∧ c ∈ Q" by auto then have "P = Q" using a_neq_c eq_paths by blast thus ?thesis using eq_paths a_neq_c using abc_inP path_P by auto qed lemma betw_c_in_path: assumes abc: "[a;b;c]" and path_ab: "path ab a b" shows "c ∈ ab" (* By abc_ex_path, there is a path through a b c. By eq_paths there can be only one, which must be ab. *) using eq_paths abc_ex_path assms by blast lemma betw_b_in_path: assumes abc: "[a;b;c]" and path_ab: "path ac a c" shows "b ∈ ac" using assms abc_ex_path_unique path_unique by blast lemma betw_a_in_path: assumes abc: "[a;b;c]" and path_ab: "path bc b c" shows "a ∈ bc" using assms abc_ex_path_unique path_unique by blast lemma triangle_not_betw_abc: assumes tri_abc: "△ a b c" shows "¬ [a;b;c]" using tri_abc abc_ex_path triangle_diff_paths by blast lemma triangle_not_betw_acb: assumes tri_abc: "△ a b c" shows "¬ [a;c;b]" by (simp add: tri_abc triangle_not_betw_abc triangle_permutes(1)) lemma triangle_not_betw_bac: assumes tri_abc: "△ a b c" shows "¬ [b;a;c]" by (simp add: tri_abc triangle_not_betw_abc triangle_permutes(2)) lemma triangle_not_betw_any: assumes tri_abc: "△ a b c" shows "¬ (∃d∈{a,b,c}. ∃e∈{a,b,c}. ∃f∈{a,b,c}. [d;e;f])" by (metis abc_ex_path abc_abc_neq empty_iff insertE tri_abc triangle_diff_paths) end (*context MinkowskiBetweenness*) section "3.2 First collinearity theorem" theorem (*3*) (in MinkowskiChain) collinearity_alt2: assumes tri_abc: "△ a b c" and path_de: "path de d e" (* This follows immediately from tri_abc without it as an assumption, but we need ab in scope to refer to it in the conclusion. *) and path_ab: "path ab a b" and bcd: "[b;c;d]" and cea: "[c;e;a]" shows "∃f∈de∩ab. [a;f;b]" proof - have "∃f∈ab ∩ de. ∃X ord. [ord↝X|a..f..b]" proof - have "path_ex a c" using tri_abc triangle_paths(2) by auto then obtain ac where path_ac: "path ac a c" by auto have "path_ex b c" using tri_abc triangle_paths(3) by auto then obtain bc where path_bc: "path bc b c" by auto have ab_neq_ac: "ab ≠ ac" using triangle_paths_neq path_ab path_ac tri_abc by fastforce have ab_neq_bc: "ab ≠ bc" using eq_paths ab_neq_ac path_ab path_ac path_bc by blast have ac_neq_bc: "ac ≠ bc" using eq_paths ab_neq_bc path_ab path_ac path_bc by blast have d_in_bc: "d ∈ bc" using bcd betw_c_in_path path_bc by blast have e_in_ac: "e ∈ ac" using betw_b_in_path cea path_ac by blast show ?thesis using O6_old [where Q = ab and R = ac and S = bc and T = de and a = a and b = b and c = c] ab_neq_ac ab_neq_bc ac_neq_bc path_ab path_bc path_ac path_de bcd cea d_in_bc e_in_ac by auto qed thus ?thesis using fin_ch_betw by blast qed theorem (*3*) (in MinkowskiChain) collinearity_alt: assumes tri_abc: "△ a b c" and path_de: "path de d e" and bcd: "[b;c;d]" and cea: "[c;e;a]" shows "∃ab. path ab a b ∧ (∃f∈de∩ab. [a;f;b])" proof - have ex_path_ab: "path_ex a b" using tri_abc triangle_paths_unique by blast then obtain ab where path_ab: "path ab a b" by blast have "∃f∈ab ∩ de. ∃X g. [g↝X|a..f..b]" proof - have "path_ex a c" using tri_abc triangle_paths(2) by auto then obtain ac where path_ac: "path ac a c" by auto have "path_ex b c" using tri_abc triangle_paths(3) by auto then obtain bc where path_bc: "path bc b c" by auto have ab_neq_ac: "ab ≠ ac" using triangle_paths_neq path_ab path_ac tri_abc by fastforce have ab_neq_bc: "ab ≠ bc" using eq_paths ab_neq_ac path_ab path_ac path_bc by blast have ac_neq_bc: "ac ≠ bc" using eq_paths ab_neq_bc path_ab path_ac path_bc by blast have d_in_bc: "d ∈ bc" using bcd betw_c_in_path path_bc by blast have e_in_ac: "e ∈ ac" using betw_b_in_path cea path_ac by blast show ?thesis using O6_old [where Q = ab and R = ac and S = bc and T = de and a = a and b = b and c = c] ab_neq_ac ab_neq_bc ac_neq_bc path_ab path_bc path_ac path_de bcd cea d_in_bc e_in_ac by auto qed thus ?thesis using fin_ch_betw path_ab by fastforce qed theorem (*3*) (in MinkowskiChain) collinearity: assumes tri_abc: "△ a b c" and path_de: "path de d e" and bcd: "[b;c;d]" and cea: "[c;e;a]" shows "(∃f∈de∩(path_of a b). [a;f;b])" proof - let ?ab = "path_of a b" have path_ab: "path ?ab a b" using tri_abc theI' [OF triangle_paths_unique] by blast have "∃f∈?ab ∩ de. ∃X ord. [ord↝X|a..f..b]" proof - have "path_ex a c" using tri_abc triangle_paths(2) by auto then obtain ac where path_ac: "path ac a c" by auto have "path_ex b c" using tri_abc triangle_paths(3) by auto then obtain bc where path_bc: "path bc b c" by auto have ab_neq_ac: "?ab ≠ ac" using triangle_paths_neq path_ab path_ac tri_abc by fastforce have ab_neq_bc: "?ab ≠ bc" using eq_paths ab_neq_ac path_ab path_ac path_bc by blast have ac_neq_bc: "ac ≠ bc" using eq_paths ab_neq_bc path_ab path_ac path_bc by blast have d_in_bc: "d ∈ bc" using bcd betw_c_in_path path_bc by blast have e_in_ac: "e ∈ ac" using betw_b_in_path cea path_ac by blast show ?thesis using O6_old [where Q = ?ab and R = ac and S = bc and T = de and a = a and b = b and c = c] ab_neq_ac ab_neq_bc ac_neq_bc path_ab path_bc path_ac path_de bcd cea d_in_bc e_in_ac IntI Int_commute by (metis (no_types, lifting)) qed thus ?thesis using fin_ch_betw by blast qed section "Additional results for Paths and Unreachables" context MinkowskiPrimitive begin text ‹The degenerate case.› lemma big_bang: assumes no_paths: "𝒫 = {}" shows "∃a. ℰ = {a}" proof - have "∃a. a ∈ ℰ" using nonempty_events by blast then obtain a where a_event: "a ∈ ℰ" by auto have "¬ (∃b∈ℰ. b ≠ a)" proof (rule notI) assume "∃b∈ℰ. b ≠ a" then have "∃Q. Q ∈ 𝒫" using events_paths a_event by auto thus False using no_paths by simp qed then have "∀b∈ℰ. b = a" by simp thus ?thesis using a_event by auto qed lemma two_events_then_path: assumes two_events: "∃a∈ℰ. ∃b∈ℰ. a ≠ b" shows "∃Q. Q ∈ 𝒫" proof - have "(∀a. ℰ ≠ {a}) ⟶ 𝒫 ≠ {}" using big_bang by blast then have "𝒫 ≠ {}" using two_events by blast thus ?thesis by blast qed lemma paths_are_events: "∀Q∈𝒫. ∀a∈Q. a ∈ ℰ" by simp lemma same_empty_unreach: "⟦Q ∈ 𝒫; a ∈ Q⟧ ⟹ unreach-on Q from a = {}" apply (unfold unreachable_subset_def) by simp lemma same_path_reachable: "⟦Q ∈ 𝒫; a ∈ Q; b ∈ Q⟧ ⟹ a ∈ Q - unreach-on Q from b" by (simp add: same_empty_unreach) text ‹ If we have two paths crossing and $a$ is on the crossing point, and $b$ is on one of the paths, then $a$ is in the reachable part of the path $b$ is on. › lemma same_path_reachable2: "⟦Q ∈ 𝒫; R ∈ 𝒫; a ∈ Q; a ∈ R; b ∈ Q⟧ ⟹ a ∈ R - unreach-on R from b" unfolding unreachable_subset_def by blast (* This will never be used without R ∈ 𝒫 but we might as well leave it off as the proof doesn't need it. *) lemma cross_in_reachable: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" and b_inQ: "b ∈ Q" and b_inR: "b ∈ R" shows "b ∈ R - unreach-on R from a" unfolding unreachable_subset_def using a_inQ b_inQ b_inR path_Q by auto lemma reachable_path: assumes path_Q: "Q ∈ 𝒫" and b_event: "b ∈ ℰ" and a_reachable: "a ∈ Q - unreach-on Q from b" shows "∃R∈𝒫. a ∈ R ∧ b ∈ R" proof - have a_inQ: "a ∈ Q" using a_reachable by simp have "Q ∉ 𝒫 ∨ b ∉ ℰ ∨ b ∈ Q ∨ (∃R∈𝒫. b ∈ R ∧ a ∈ R)" using a_reachable unreachable_subset_def by auto then have "b ∈ Q ∨ (∃R∈𝒫. b ∈ R ∧ a ∈ R)" using path_Q b_event by simp thus ?thesis proof (rule disjE) assume "b ∈ Q" thus ?thesis using a_inQ path_Q by auto next assume "∃R∈𝒫. b ∈ R ∧ a ∈ R" thus ?thesis using conj_commute by simp qed qed end (* context MinkowskiPrimitive *) context MinkowskiBetweenness begin lemma ord_path_of: assumes "[a;b;c]" shows "a ∈ path_of b c" "b ∈ path_of a c" "c ∈ path_of a b" and "path_of a b = path_of a c" "path_of a b = path_of b c" proof - show "a ∈ path_of b c" using betw_a_in_path[of a b c "path_of b c"] path_of_ex abc_ex_path_unique abc_abc_neq assms by (smt (z3) betw_a_in_path the1_equality) show "b ∈ path_of a c" using betw_b_in_path[of a b c "path_of a c"] path_of_ex abc_ex_path_unique abc_abc_neq assms by (smt (z3) betw_b_in_path the1_equality) show "c ∈ path_of a b" using betw_c_in_path[of a b c "path_of a b"] path_of_ex abc_ex_path_unique abc_abc_neq assms by (smt (z3) betw_c_in_path the1_equality) show "path_of a b = path_of a c" by (metis (mono_tags) abc_ac_neq assms betw_b_in_path betw_c_in_path ends_notin_segment seg_betw) show "path_of a b = path_of b c" by (metis (mono_tags) assms betw_a_in_path betw_c_in_path ends_notin_segment seg_betw) qed text ‹ Schutz defines chains as subsets of paths. The result below proves that even though we do not include this fact in our definition, it still holds, at least for finite chains. › text ‹ Notice that this whole proof would be unnecessary if including path-belongingness in the definition, as Schutz does. This would also keep path-belongingness independent of axiom O1 and O4, thus enabling an independent statement of axiom O6, which perhaps we now lose. In exchange, our definition is slightly weaker (for ‹card X ≥ 3› and ‹infinite X›). › lemma obtain_index_fin_chain: assumes "[f↝X]" "x∈X" "finite X" obtains i where "f i = x" "i<card X" proof - have "∃i<card X. f i = x" using assms(1) unfolding ch_by_ord_def proof (rule disjE) assume asm: "short_ch_by_ord f X" hence "card X = 2" using short_ch_card(1) by auto thus "∃i<card X. f i = x" using asm assms(2) unfolding chain_defs by force next assume asm: "local_long_ch_by_ord f X" thus "∃i<card X. f i = x" using asm assms(2,3) unfolding chain_defs local_ordering_def by blast qed thus ?thesis using that by blast qed lemma obtain_index_inf_chain: assumes "[f↝X]" "x∈X" "infinite X" obtains i where "f i = x" using assms unfolding chain_defs local_ordering_def by blast lemma fin_chain_on_path2: assumes "[f↝X]" "finite X" shows "∃P∈𝒫. X⊆P" using assms(1) unfolding ch_by_ord_def proof (rule disjE) assume "short_ch_by_ord f X" thus ?thesis using short_ch_by_ord_def by auto next assume asm: "local_long_ch_by_ord f X" have "[f 0;f 1;f 2]" using order_finite_chain asm assms(2) local_long_ch_by_ord_def by auto then obtain P where "P∈𝒫" "{f 0,f 1,f 2} ⊆ P" by (meson abc_ex_path empty_subsetI insert_subset) then have "path P (f 0) (f 1)" using ‹[f 0;f 1;f 2]› by (simp add: abc_abc_neq) { fix x assume "x∈X" then obtain i where i: "f i = x" "i<card X" using obtain_index_fin_chain assms by blast consider "i=0∨i=1"|"i>1" by linarith hence "x∈P" proof (cases) case 1 thus ?thesis using i(1) ‹{f 0, f 1, f 2} ⊆ P› by auto next case 2 hence "[f 0;f 1;f i]" using assms i(2) order_finite_chain2 by auto hence "{f 0,f 1,f i}⊆P" using ‹path P (f 0) (f 1)› betw_c_in_path by blast thus ?thesis by (simp add: i(1)) qed } thus ?thesis using ‹P∈𝒫› by auto qed lemma fin_chain_on_path: assumes "[f↝X]" "finite X" shows "∃!P∈𝒫. X⊆P" proof - obtain P where P: "P∈𝒫" "X⊆P" using fin_chain_on_path2[OF assms] by auto obtain a b where ab: "a∈X" "b∈X" "a≠b" using assms(1) unfolding chain_defs by (metis assms(2) insertCI three_in_set3) thus ?thesis using P ab by (meson eq_paths in_mono) qed lemma fin_chain_on_path3: assumes "[f↝X]" "finite X" "a∈X" "b∈X" "a≠b" shows "X ⊆ path_of a b" proof - let ?ab = "path_of a b" obtain P where P: "P∈𝒫" "X⊆P" using fin_chain_on_path2[OF assms(1,2)] by auto have "path P a b" using P assms(3-5) by auto then have "path ?ab a b" using path_of_ex by blast hence "?ab = P" using eq_paths ‹path P a b› by auto thus "X ⊆ path_of a b" using P by simp qed end (* context MinkowskiBetweenness *) context MinkowskiUnreachable begin text ‹ First some basic facts about the primitive notions, which seem to belong here. I don't think any/all of these are explicitly proved in Schutz. › lemma no_empty_paths [simp]: assumes "Q∈𝒫" shows "Q≠{}" (*using assms nonempty_events two_in_unreach unreachable_subset_def by blast*) proof - obtain a where "a∈ℰ" using nonempty_events by blast have "a∈Q ∨ a∉Q" by auto thus ?thesis proof assume "a∈Q" thus ?thesis by blast next assume "a∉Q" then obtain b where "b∈unreach-on Q from a" using two_in_unreach ‹a ∈ ℰ› assms by blast thus ?thesis using unreachable_subset_def by auto qed qed lemma events_ex_path: assumes ge1_path: "𝒫 ≠ {}" shows "∀x∈ℰ. ∃Q∈𝒫. x ∈ Q" (*using ex_in_conv no_empty_paths in_path_event assms events_paths by metis*) proof fix x assume x_event: "x ∈ ℰ" have "∃Q. Q ∈ 𝒫" using ge1_path using ex_in_conv by blast then obtain Q where path_Q: "Q ∈ 𝒫" by auto then have "∃y. y ∈ Q" using no_empty_paths by blast then obtain y where y_inQ: "y ∈ Q" by auto then have y_event: "y ∈ ℰ" using in_path_event path_Q by simp have "∃P∈𝒫. x ∈ P" proof cases assume "x = y" thus ?thesis using y_inQ path_Q by auto next assume "x ≠ y" thus ?thesis using events_paths x_event y_event by auto qed thus "∃Q∈𝒫. x ∈ Q" by simp qed lemma unreach_ge2_then_ge2: assumes "∃x∈unreach-on Q from b. ∃y∈unreach-on Q from b. x ≠ y" shows "∃x∈Q. ∃y∈Q. x ≠ y" using assms unreachable_subset_def by auto text ‹ This lemma just proves that the chain obtained to bound the unreachable set of a path is indeed on that path. Extends I6; requires Theorem 2; used in Theorem 13. Seems to be assumed in Schutz' chain notation in I6. › lemma chain_on_path_I6: assumes path_Q: "Q∈𝒫" and event_b: "b∉Q" "b∈ℰ" and unreach: "Q⇩_{x}∈ unreach-on Q from b" "Q⇩_{z}∈ unreach-on Q from b" "Q⇩_{x}≠ Q⇩_{z}" and X_def: "[f↝X|Q⇩_{x}..Q⇩_{z}]" "(∀i∈{1 .. card X - 1}. (f i) ∈ unreach-on Q from b ∧ (∀Q⇩_{y}∈ℰ. [(f(i-1)); Q⇩_{y}; f i] ⟶ Q⇩_{y}∈ unreach-on Q from b))" shows "X⊆Q" proof - have 1: "path Q Q⇩_{x}Q⇩_{z}" using unreachable_subset_def unreach path_Q by simp then have 2: "Q = path_of Q⇩_{x}Q⇩_{z}" using path_of_ex[of Q⇩_{x}Q⇩_{z}] by (meson eq_paths) have "X⊆path_of Q⇩_{x}Q⇩_{z}" proof (rule fin_chain_on_path3[of f]) from unreach(3) show "Q⇩_{x}≠ Q⇩_{z}" by simp from X_def chain_defs show "[f↝X]" "finite X" by metis+ from assms(7) points_in_chain show "Q⇩_{x}∈ X" "Q⇩_{z}∈ X" by auto qed thus ?thesis using 2 by simp qed end (* context MinkowskiUnreachable *) section "Results about Paths as Sets" text ‹ Note several of the following don't need MinkowskiPrimitive, they are just Set lemmas; nevertheless I'm naming them and writing them this way for clarity. › context MinkowskiPrimitive begin lemma distinct_paths: assumes "Q ∈ 𝒫" and "R ∈ 𝒫" and "d ∉ Q" and "d ∈ R" shows "R ≠ Q" using assms by auto lemma distinct_paths2: assumes "Q ∈ 𝒫" and "R ∈ 𝒫" and "∃d. d ∉ Q ∧ d ∈ R" shows "R ≠ Q" using assms by auto lemma external_events_neq: "⟦Q ∈ 𝒫; a ∈ Q; b ∈ ℰ; b ∉ Q⟧ ⟹ a ≠ b" by auto lemma notin_cross_events_neq: "⟦Q ∈ 𝒫; R ∈ 𝒫; Q ≠ R; a ∈ Q; b ∈ R; a ∉ R∩Q⟧ ⟹ a ≠ b" by blast lemma nocross_events_neq: "⟦Q ∈ 𝒫; R ∈ 𝒫; a ∈ Q; b ∈ R; R∩Q = {}⟧ ⟹ a ≠ b" by auto text ‹ Given a nonempty path $Q$, and an external point $d$, we can find another path $R$ passing through $d$ (by I2 aka ‹events_paths›). This path is distinct from $Q$, as it passes through a point external to it. › lemma external_path: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" and d_notinQ: "d ∉ Q" and d_event: "d ∈ ℰ" shows "∃R∈𝒫. d ∈ R" proof - have a_neq_d: "a ≠ d" using a_inQ d_notinQ by auto thus "∃R∈𝒫. d ∈ R" using events_paths by (meson a_inQ d_event in_path_event path_Q) qed lemma distinct_path: assumes "Q ∈ 𝒫" and "a ∈ Q" and "d ∉ Q" and "d ∈ ℰ" shows "∃R∈𝒫. R ≠ Q" using assms external_path by metis lemma external_distinct_path: assumes "Q ∈ 𝒫" and "a ∈ Q" and "d ∉ Q" and "d ∈ ℰ" shows "∃R∈𝒫. R ≠ Q ∧ d ∈ R" using assms external_path by fastforce end (* context MinkowskiPrimitive *) section "3.3 Boundedness of the unreachable set" subsection ‹Theorem 4 (boundedness of the unreachable set)› text ‹ The same assumptions as I7, different conclusion. This doesn't just give us boundedness, it gives us another event outside of the unreachable set, as long as we have one already. I7 conclusion: ‹∃g X Qn. [g↝X|Qx..Qy..Qn] ∧ Qn ∈ Q - unreach-on Q from b› › theorem (*4*) (in MinkowskiUnreachable) unreachable_set_bounded: assumes path_Q: "Q ∈ 𝒫" and b_nin_Q: "b ∉ Q" and b_event: "b ∈ ℰ" and Qx_reachable: "Qx ∈ Q - unreach-on Q from b" and Qy_unreachable: "Qy ∈ unreach-on Q from b" shows "∃Qz∈Q - unreach-on Q from b. [Qx;Qy;Qz] ∧ Qx ≠ Qz" using assms I7_old finite_long_chain_with_def fin_ch_betw by (metis first_neq_last) subsection ‹Theorem 5 (first existence theorem)› text ‹ The lemma below is used in the contradiction in ‹external_event›, which is the essential part to Theorem 5(i). › lemma (in MinkowskiUnreachable) only_one_path: assumes path_Q: "Q ∈ 𝒫" and all_inQ: "∀a∈ℰ. a ∈ Q" and path_R: "R ∈ 𝒫" shows "R = Q" proof (rule ccontr) assume "¬ R = Q" then have R_neq_Q: "R ≠ Q" by simp have "ℰ = Q" by (simp add: all_inQ antisym path_Q path_sub_events subsetI) hence "R⊂Q" using R_neq_Q path_R path_sub_events by auto obtain c where "c∉R" "c∈Q" using ‹R ⊂ Q› by blast then obtain a b where "path R a b" using ‹ℰ = Q› path_R two_in_unreach unreach_ge2_then_ge2 by blast have "a∈Q" "b∈Q" using ‹ℰ = Q› ‹path R a b› in_path_event by blast+ thus False using eq_paths using R_neq_Q ‹path R a b› path_Q by blast qed context MinkowskiSpacetime begin text ‹Unfortunately, we cannot assume that a path exists without the axiom of dimension.› lemma external_event: assumes path_Q: "Q ∈ 𝒫" shows "∃d∈ℰ. d ∉ Q" proof (rule ccontr) assume "¬ (∃d∈ℰ. d ∉ Q)" then have all_inQ: "∀d∈ℰ. d ∈ Q" by simp then have only_one_path: "∀P∈𝒫. P = Q" by (simp add: only_one_path path_Q) thus False using ex_3SPRAY three_SPRAY_ge4 four_paths by auto qed text ‹ Now we can prove the first part of the theorem's conjunction. This follows pretty much exactly the same pattern as the book, except it relies on more intermediate lemmas. › theorem (*5i*) ge2_events: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" shows "∃b∈Q. b ≠ a" proof - have d_notinQ: "∃d∈ℰ. d ∉ Q" using path_Q external_event by blast then obtain d where "d ∈ ℰ" and "d ∉ Q" by auto thus ?thesis using two_in_unreach [where Q = Q and b = d] path_Q unreach_ge2_then_ge2 by metis qed text ‹ Simple corollary which is easier to use when we don't have one event on a path yet. Anything which uses this implicitly used ‹no_empty_paths› on top of ‹ge2_events›. › lemma ge2_events_lax: assumes path_Q: "Q ∈ 𝒫" shows "∃a∈Q. ∃b∈Q. a ≠ b" proof - have "∃a∈ℰ. a ∈ Q" using path_Q no_empty_paths by (meson ex_in_conv in_path_event) thus ?thesis using path_Q ge2_events by blast qed lemma ex_crossing_path: assumes path_Q: "Q ∈ 𝒫" shows "∃R∈𝒫. R ≠ Q ∧ (∃c. c ∈ R ∧ c ∈ Q)" proof - obtain a where a_inQ: "a ∈ Q" using ge2_events_lax path_Q by blast obtain d where d_event: "d ∈ ℰ" and d_notinQ: "d ∉ Q" using external_event path_Q by auto then have "a ≠ d" using a_inQ by auto then have ex_through_d: "∃R∈𝒫. ∃S∈𝒫. a ∈ R ∧ d ∈ S ∧ R ∩ S ≠ {}" using events_paths [where a = a and b = d] path_Q a_inQ in_path_event d_event by simp then obtain R S where path_R: "R ∈ 𝒫" and path_S: "S ∈ 𝒫" and a_inR: "a ∈ R" and d_inS: "d ∈ S" and R_crosses_S: "R ∩ S ≠ {}" by auto have S_neq_Q: "S ≠ Q" using d_notinQ d_inS by auto show ?thesis proof cases assume "R = Q" then have "Q ∩ S ≠ {}" using R_crosses_S by simp thus ?thesis using S_neq_Q path_S by blast next assume "R ≠ Q" thus ?thesis using a_inQ a_inR path_R by blast qed qed text ‹ If we have two paths $Q$ and $R$ with $a$ on $Q$ and $b$ at the intersection of $Q$ and $R$, then by ‹two_in_unreach› (I5) and Theorem 4 (boundedness of the unreachable set), there is an unreachable set from $a$ on one side of $b$ on $R$, and on the other side of that there is an event which is reachable from $a$ by some path, which is the path we want. › lemma path_past_unreach: assumes path_Q: "Q ∈ 𝒫" and path_R: "R ∈ 𝒫" and a_inQ: "a ∈ Q" and b_inQ: "b ∈ Q" and b_inR: "b ∈ R" and Q_neq_R: "Q ≠ R" and a_neq_b: "a ≠ b" shows "∃S∈𝒫. S ≠ Q ∧ a ∈ S ∧ (∃c. c ∈ S ∧ c ∈ R)" proof - obtain d where d_event: "d ∈ ℰ" and d_notinR: "d ∉ R" using external_event path_R by blast have b_reachable: "b ∈ R - unreach-on R from a" using cross_in_reachable path_R a_inQ b_inQ b_inR path_Q by simp have a_notinR: "a ∉ R" using cross_once_notin Q_neq_R a_inQ a_neq_b b_inQ b_inR path_Q path_R by blast then obtain u where "u ∈ unreach-on R from a" using two_in_unreach a_inQ in_path_event path_Q path_R by blast then obtain c where c_reachable: "c ∈ R - unreach-on R from a" and c_neq_b: "b ≠ c" using unreachable_set_bounded [where Q = R and Qx = b and b = a and Qy = u] path_R d_event d_notinR using a_inQ a_notinR b_reachable in_path_event path_Q by blast then obtain S where S_facts: "S ∈ 𝒫 ∧ a ∈ S ∧ (c ∈ S ∧ c ∈ R)" using reachable_path by (metis Diff_iff a_inQ in_path_event path_Q path_R) then have "S ≠ Q" using Q_neq_R b_inQ b_inR c_neq_b eq_paths path_R by blast thus ?thesis using S_facts by auto qed theorem (*5ii*) ex_crossing_at: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" shows "∃ac∈𝒫. ac ≠ Q ∧ (∃c. c ∉ Q ∧ a ∈ ac ∧ c ∈ ac)" proof - obtain b where b_inQ: "b ∈ Q" and a_neq_b: "a ≠ b" using a_inQ ge2_events path_Q by blast have "∃R∈𝒫. R ≠ Q ∧ (∃e. e ∈ R ∧ e ∈ Q)" by (simp add: ex_crossing_path path_Q) then obtain R e where path_R: "R ∈ 𝒫" and R_neq_Q: "R ≠ Q" and e_inR: "e ∈ R" and e_inQ: "e ∈ Q" by auto thus ?thesis proof cases assume e_eq_a: "e = a" then have "∃c. c ∈ unreach-on R from b" using R_neq_Q a_inQ a_neq_b b_inQ e_inR path_Q path_R two_in_unreach path_unique in_path_event by metis thus ?thesis using R_neq_Q e_eq_a e_inR path_Q path_R eq_paths ge2_events_lax by metis next assume e_neq_a: "e ≠ a" (* We know the whole of R isn't unreachable from a because e is on R and both a and e are on Q. We also know there is some point after e, and after the unreachable set, which is reachable from a (because there are at least two events in the unreachable set, and it is bounded). *) (* This does follow Schutz, if you unfold the proof for path_past_unreach here, though it's a little trickier than Schutz made it seem. *) then have "∃S∈𝒫. S ≠ Q ∧ a ∈ S ∧ (∃c. c ∈ S ∧ c ∈ R)" using path_past_unreach R_neq_Q a_inQ e_inQ e_inR path_Q path_R by auto thus ?thesis by (metis R_neq_Q e_inR e_neq_a eq_paths path_Q path_R) qed qed (* Alternative formulation using the path function *) lemma (*5ii_alt*) ex_crossing_at_alt: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" shows "∃ac. ∃c. path ac a c ∧ ac ≠ Q ∧ c ∉ Q" using ex_crossing_at assms by fastforce end (* context MinkowskiSpacetime *) section "3.4 Prolongation" context MinkowskiSpacetime begin lemma (in MinkowskiPrimitive) unreach_on_path: "a ∈ unreach-on Q from b ⟹ a ∈ Q" using unreachable_subset_def by simp lemma (in MinkowskiUnreachable) unreach_equiv: "⟦Q ∈ 𝒫; R ∈ 𝒫; a ∈ Q; b ∈ R; a ∈ unreach-on Q from b⟧ ⟹ b ∈ unreach-on R from a" unfolding unreachable_subset_def by auto theorem (*6i*) prolong_betw: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" and b_inQ: "b ∈ Q" and ab_neq: "a ≠ b" shows "∃c∈ℰ. [a;b;c]" proof - obtain e ae where e_event: "e ∈ ℰ" and e_notinQ: "e ∉ Q" and path_ae: "path ae a e" using ex_crossing_at a_inQ path_Q in_path_event by blast have "b ∉ ae" using a_inQ ab_neq b_inQ e_notinQ eq_paths path_Q path_ae by blast then obtain f where f_unreachable: "f ∈ unreach-on ae from b" using two_in_unreach b_inQ in_path_event path_Q path_ae by blast then have b_unreachable: "b ∈ unreach-on Q from f" using unreach_equiv by (metis (mono_tags, lifting) CollectD b_inQ path_Q unreachable_subset_def) have a_reachable: "a ∈ Q - unreach-on Q from f" using same_path_reachable2 [where Q = ae and R = Q and a = a and b = f] path_ae a_inQ path_Q f_unreachable unreach_on_path by blast thus ?thesis using unreachable_set_bounded [where Qy = b and Q = Q and b = f and Qx = a] b_unreachable unreachable_subset_def by auto qed lemma (in MinkowskiSpacetime) prolong_betw2: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" and b_inQ: "b ∈ Q" and ab_neq: "a ≠ b" shows "∃c∈Q. [a;b;c]" by (metis assms betw_c_in_path prolong_betw) lemma (in MinkowskiSpacetime) prolong_betw3: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" and b_inQ: "b ∈ Q" and ab_neq: "a ≠ b" shows "∃c∈Q. ∃d∈Q. [a;b;c] ∧ [a;b;d] ∧ c≠d" by (metis (full_types) abc_abc_neq abc_bcd_abd a_inQ ab_neq b_inQ path_Q prolong_betw2) lemma finite_path_has_ends: assumes "Q ∈ 𝒫" and "X ⊆ Q" and "finite X" and "card X ≥ 3" shows "∃a∈X. ∃b∈X. a ≠ b ∧ (∀c∈X. a ≠ c ∧ b ≠ c ⟶ [a;c;b])" using assms proof (induct "card X - 3" arbitrary: X) case 0 then have "card X = 3" by linarith then obtain a b c where X_eq: "X = {a, b, c}" by (metis card_Suc_eq numeral_3_eq_3) then have abc_neq: "a ≠ b" "a ≠ c" "b ≠ c" by (metis ‹card X = 3› empty_iff insert_iff order_refl three_in_set3)+ then consider "[a;b;c]" | "[b;c;a]" | "[c;a;b]" using some_betw [of Q a b c] "0.prems"(1) "0.prems"(2) X_eq by auto thus ?case proof (cases) assume "[a;b;c]" thus ?thesis ― ‹All d not equal to a or c is just d = b, so it immediately follows.› using X_eq abc_neq(2) by blast next assume "[b;c;a]" thus ?thesis by (simp add: X_eq abc_neq(1)) next assume "[c;a;b]" thus ?thesis using X_eq abc_neq(3) by blast qed next case IH: (Suc n) obtain Y x where X_eq: "X = insert x Y" and "x ∉ Y" by (meson IH.prems(4) Set.set_insert three_in_set3) then have "card Y - 3 = n" "card Y ≥ 3" using IH.hyps(2) IH.prems(3) X_eq ‹x ∉ Y› by auto then obtain a b where ab_Y: "a ∈ Y" "b ∈ Y" "a ≠ b" and Y_ends: "∀c∈Y. (a ≠ c ∧ b ≠ c) ⟶ [a;c;b]" using IH(1) [of Y] IH.prems(1-3) X_eq by auto consider "[a;x;b]" | "[x;b;a]" | "[b;a;x]" using some_betw [of Q a x b] ab_Y IH.prems(1,2) X_eq ‹x ∉ Y› by auto thus ?case proof (cases) assume "[a;x;b]" thus ?thesis using Y_ends X_eq ab_Y by auto next assume "[x;b;a]" { fix c assume "c ∈ X" "x ≠ c" "a ≠ c" then have "[x;c;a]" by (smt IH.prems(2) X_eq Y_ends ‹[x;b;a]› ab_Y(1) abc_abc_neq abc_bcd_abd abc_only_cba(3) abc_sym ‹Q ∈ 𝒫› betw_b_in_path insert_iff some_betw subsetD) } thus ?thesis using X_eq ‹[x;b;a]› ab_Y(1) abc_abc_neq insert_iff by force next assume "[b;a;x]" { fix c assume "c ∈ X" "b ≠ c" "x ≠ c" then have "[b;c;x]" by (smt IH.prems(2) X_eq Y_ends ‹[b;a;x]› ab_Y(1) abc_abc_neq abc_bcd_acd abc_only_cba(1) abc_sym ‹Q ∈ 𝒫› betw_a_in_path insert_iff some_betw subsetD) } thus ?thesis using X_eq ‹x ∉ Y› ab_Y(2) by fastforce qed qed lemma obtain_fin_path_ends: assumes path_X: "X∈𝒫" and fin_Q: "finite Q" and card_Q: "card Q ≥ 3" and events_Q: "Q⊆X" obtains a b where "a≠b" and "a∈Q" and "b∈Q" and "∀c∈Q. (a≠c ∧ b≠c) ⟶ [a;c;b]" proof - obtain n where "n≥0" and "card Q = n+3" using card_Q nat_le_iff_add by auto then obtain a b where "a≠b" and "a∈Q" and "b∈Q" and "∀c∈Q. (a≠c ∧ b≠c) ⟶ [a;c;b]" using finite_path_has_ends assms ‹n≥0› by metis thus ?thesis using that by auto qed lemma path_card_nil: assumes "Q∈𝒫" shows "card Q = 0" proof (rule ccontr) assume "card Q ≠ 0" obtain n where "n = card Q" by auto hence "n≥1" using ‹card Q ≠ 0› by linarith then consider (n1) "n=1" | (n2) "n=2" | (n3) "n≥3" by linarith thus False proof (cases) case n1 thus ?thesis using One_nat_def card_Suc_eq ge2_events_lax singletonD assms(1) by (metis ‹n = card Q›) next case n2 then obtain a b where "a≠b" and "a∈Q" and "b∈Q" using ge2_events_lax assms(1) by blast then obtain c where "c∈Q" and "c≠a" and "c≠b" using prolong_betw2 by (metis abc_abc_neq assms(1)) hence "card Q ≠ 2" by (metis ‹a ∈ Q› ‹a ≠ b› ‹b ∈ Q› card_2_iff') thus False using ‹n = card Q› ‹n = 2› by blast next case n3 have fin_Q: "finite Q" proof - have "(0::nat) ≠ 1" by simp then show ?thesis by (meson ‹card Q ≠ 0› card.infinite) qed have card_Q: "card Q ≥ 3" using ‹n = card Q› n3 by blast have "Q⊆Q" by simp then obtain a b where "a∈Q" and "b∈Q" and "a≠b" and acb: "∀c∈Q. (c≠a ∧ c≠b) ⟶ [a;c;b]" using obtain_fin_path_ends card_Q fin_Q assms(1) by metis then obtain x where "[a;b;x]" and "x∈Q" using prolong_betw2 assms(1) by blast thus False by (metis acb abc_abc_neq abc_only_cba(2)) qed qed theorem (*6ii*) infinite_paths: assumes "P∈𝒫" shows "infinite P" proof assume fin_P: "finite P" have "P≠{}" by (simp add: assms) hence "card P ≠ 0" by (simp add: fin_P) moreover have "¬(card P ≥ 1)" using path_card_nil by (simp add: assms) ultimately show False by simp qed end (* contex MinkowskiSpacetime *) section "3.5 Second collinearity theorem" text ‹We start with a useful betweenness lemma.› lemma (in MinkowskiBetweenness) some_betw2: assumes path_Q: "Q ∈ 𝒫" and a_inQ: "a ∈ Q" and b_inQ: "b ∈ Q" and c_inQ: "c ∈ Q" shows "a = b ∨ a = c ∨ b = c ∨ [a;b;c] ∨ [b;c;a] ∨ [c;a;b]" using a_inQ b_inQ c_inQ path_Q some_betw by blast lemma (in MinkowskiPrimitive) paths_tri: assumes path_ab: "path ab a b" and path_bc: "path bc b c" and path_ca: "path ca c a" and a_notin_bc: "a ∉ bc" shows "△ a b c" proof - have abc_events: "a ∈ ℰ ∧ b ∈ ℰ ∧ c ∈ ℰ" using path_ab path_bc path_ca in_path_event by auto have abc_neq: "a ≠ b ∧ a ≠ c ∧ b ≠ c" using path_ab path_bc path_ca by auto have paths_neq: "ab ≠ bc ∧ ab ≠ ca ∧ bc ≠ ca" using a_notin_bc cross_once_notin path_ab path_bc path_ca by blast show ?thesis unfolding kinematic_triangle_def using abc_events abc_neq paths_neq path_ab path_bc path_ca by auto qed lemma (in MinkowskiPrimitive) paths_tri2: assumes path_ab: "path ab a b" and path_bc: "path bc b c" and path_ca: "path ca c a" and ab_neq_bc: "ab ≠ bc" shows "△ a b c" by (meson ab_neq_bc cross_once_notin path_ab path_bc path_ca paths_tri) text ‹ Schutz states it more like ‹⟦tri_abc; bcd; cea⟧ ⟹ (path de d e ⟶ ∃f∈de. [a;f;b]∧[d;e;f])›. Equivalent up to usage of ‹impI›. › theorem (*7*) (in MinkowskiChain) collinearity2: assumes tri_abc: "△ a b c" and bcd: "[b;c;d]" and cea: "[c;e;a]" and path_de: "path de d e" shows "∃f. [a;f;b] ∧ [d;e;f]" proof - obtain ab where path_ab: "path ab a b" using tri_abc triangle_paths_unique by blast then obtain f where afb: "[a;f;b]" and f_in_de: "f ∈ de" using collinearity tri_abc path_de path_ab bcd cea by blast (* af will be used a few times, so obtain it here. *) obtain af where path_af: "path af a f" using abc_abc_neq afb betw_b_in_path path_ab by blast have "[d;e;f]" proof - have def_in_de: "d ∈ de ∧ e ∈ de ∧ f ∈ de" using path_de f_in_de by simp then have five_poss:"f = d ∨ f = e ∨ [e;f;d] ∨ [f;d;e] ∨ [d;e;f]" using path_de some_betw2 by blast have "f = d ∨ f = e ⟶ (∃Q∈𝒫. a ∈ Q ∧ b ∈ Q ∧ c ∈ Q)" by (metis abc_abc_neq afb bcd betw_a_in_path betw_b_in_path cea path_ab) then have f_neq_d_e: "f ≠ d ∧ f ≠ e" using tri_abc using triangle_diff_paths by simp then consider "[e;f;d]" | "[f;d;e]" | "[d;e;f]" using five_poss by linarith thus ?thesis proof (cases) assume efd: "[e;f;d]" obtain dc where path_dc: "path dc d c" using abc_abc_neq abc_ex_path bcd by blast obtain ce where path_ce: "path ce c e" using abc_abc_neq abc_ex_path cea by blast have "dc≠ce" using bcd betw_a_in_path betw_c_in_path cea path_ce path_dc tri_abc triangle_diff_paths by blast hence "△ d c e" using paths_tri2 path_ce path_dc path_de by blast then obtain x where x_in_af: "x ∈ af" and dxc: "[d;x;c]" using collinearity [where a = d and b = c and c = e and d = a and e = f and de = af] cea efd path_dc path_af by blast then have x_in_dc: "x ∈ dc" using betw_b_in_path path_dc by blast then have "x = b" using eq_paths by (metis path_af path_dc afb bcd tri_abc x_in_af betw_a_in_path betw_c_in_path triangle_diff_paths) then have "[d;b;c]" using dxc by simp then have "False" using bcd abc_only_cba [where a = b and b = c and c = d] by simp thus ?thesis by simp next assume fde: "[f;d;e]" obtain bd where path_bd: "path bd b d" using abc_abc_neq abc_ex_path bcd by blast obtain ea where path_ea: "path ea e a" using abc_abc_neq abc_ex_path_unique cea by blast obtain fe where path_fe: "path fe f e" using f_in_de f_neq_d_e path_de by blast have "fe≠ea" using tri_abc afb cea path_ea path_fe by (metis abc_abc_neq betw_a_in_path betw_c_in_path triangle_paths_neq) hence "△ e a f" by (metis path_unique path_af path_ea path_fe paths_tri2) then obtain y where y_in_bd: "y ∈ bd" and eya: "[e;y;a]" thm collinearity using collinearity [where a = e and b = a and c = f and d = b and e = d and de = bd] afb fde path_bd path_ea by blast then have "y = c" by (metis (mono_tags, lifting) afb bcd cea path_bd tri_abc abc_ac_neq betw_b_in_path path_unique triangle_paths(2) triangle_paths_neq) then have "[e;c;a]" using eya by simp then have "False" using cea abc_only_cba [where a = c and b = e and c = a] by simp thus ?thesis by simp next assume "[d;e;f]" thus ?thesis by assumption qed qed thus ?thesis using afb f_in_de by blast qed section "3.6 Order on a path - Theorems 8 and 9" context MinkowskiSpacetime begin subsection ‹Theorem 8 (as in Veblen (1911) Theorem 6)› text ‹ Note ‹a'b'c'› don't necessarily form a triangle, as there still needs to be paths between them. › theorem (*8*) (in MinkowskiChain) tri_betw_no_path: assumes tri_abc: "△ a b c" and ab'c: "[a; b'; c]" and bc'a: "[b; c'; a]" and ca'b: "[c; a'; b]" shows "¬ (∃Q∈𝒫. a' ∈ Q ∧ b' ∈ Q ∧ c' ∈ Q)" proof - have abc_a'b'c'_neq: "a ≠ a' ∧ a ≠ b' ∧ a ≠ c' ∧ b ≠ a' ∧ b ≠ b' ∧ b ≠ c' ∧ c ≠ a' ∧ c ≠ b' ∧ c ≠ c'" using abc_ac_neq by (metis ab'c abc_abc_neq bc'a ca'b tri_abc triangle_not_betw_abc triangle_permutes(4)) have tri_betw_no_path_single_case: False if a'b'c': "[a'; b'; c']" and tri_abc: "△ a b c" and ab'c: "[a; b'; c]" and bc'a: "[b; c'; a]" and ca'b: "[c; a'; b]" for a b c a' b' c' proof - have abc_a'b'c'_neq: "a ≠ a' ∧ a ≠ b' ∧ a ≠ c' ∧ b ≠ a' ∧ b ≠ b' ∧ b ≠ c' ∧ c ≠ a' ∧ c ≠ b' ∧ c ≠ c'" using abc_abc_neq that by (metis triangle_not_betw_abc triangle_permutes(4)) have c'b'a': "[c'; b'; a']" using abc_sym a'b'c' by simp have nopath_a'c'b: "¬ (∃Q∈𝒫. a' ∈ Q ∧ c' ∈ Q ∧ b ∈ Q)" proof (rule notI) assume "∃Q∈𝒫. a' ∈ Q ∧ c' ∈ Q ∧ b ∈ Q" then obtain Q where path_Q: "Q ∈ 𝒫" and a'_inQ: "a' ∈ Q" and c'_inQ: "c' ∈ Q" and b_inQ: "b ∈ Q" by blast then have ac_inQ: "a ∈ Q ∧ c ∈ Q" using eq_paths by (metis abc_a'b'c'_neq ca'b bc'a betw_a_in_path betw_c_in_path) thus False using b_inQ path_Q tri_abc triangle_diff_paths by blast qed then have tri_a'bc': "△ a' b c'" by (smt bc'a ca'b a'b'c' paths_tri abc_ex_path_unique) obtain ab' where path_ab': "path ab' a b'" using ab'c abc_a'b'c'_neq abc_ex_path by blast obtain a'b where path_a'b: "path a'b a' b" using tri_a'bc' triangle_paths(1) by blast then have "∃x∈a'b. [a'; x; b] ∧ [a; b'; x]" using collinearity2 [where a = a' and b = b and c = c' and e = b' and d = a and de = ab'] bc'a betw_b_in_path c'b'a' path_ab' tri_a'bc' by blast then obtain x where x_in_a'b: "x ∈ a'b" and a'xb: "[a'; x; b]" and ab'x: "[a; b'; x]" by blast (* ab' ∩ a'b = {c} doesn't follow as immediately as in Schutz. *) have c_in_ab': "c ∈ ab'" using ab'c betw_c_in_path path_ab' by auto have c_in_a'b: "c ∈ a'b" using ca'b betw_a_in_path path_a'b by auto have ab'_a'b_distinct: "ab' ≠ a'b" using c_in_a'b path_a'b path_ab' tri_abc triangle_diff_paths by blast have "ab' ∩ a'b = {c}" using paths_cross_at ab'_a'b_distinct c_in_a'b c_in_ab' path_a'b path_ab' by auto then have "x = c" using ab'x path_ab' x_in_a'b betw_c_in_path by auto then have "[a'; c; b]" using a'xb by auto thus ?thesis using ca'b abc_only_cba by blast qed show ?thesis proof (rule notI) assume path_a'b'c': "∃Q∈𝒫. a' ∈ Q ∧ b' ∈ Q ∧ c' ∈ Q" consider "[a'; b'; c']" | "[b'; c'; a']" | "[c'; a'; b']" using some_betw by (smt abc_a'b'c'_neq path_a'b'c' bc'a ca'b ab'c tri_abc abc_ex_path cross_once_notin triangle_diff_paths) thus False apply (cases) using tri_betw_no_path_single_case[of a' b' c'] ab'c bc'a ca'b tri_abc apply blast using tri_betw_no_path_single_case ab'c bc'a ca'b tri_abc triangle_permutes abc_sym by blast+ qed qed subsection ‹Theorem 9› text ‹ We now begin working on the transitivity lemmas needed to prove Theorem 9. Multiple lemmas below obtain primed variables (e.g. ‹d'›). These are starred in Schutz (e.g. ‹d*›), but that notation is already reserved in Isabelle. › lemma unreachable_bounded_path_only: assumes d'_def: "d'∉ unreach-on ab from e" "d'∈ab" "d'≠e" and e_event: "e ∈ ℰ" and path_ab: "ab ∈ 𝒫" and e_notin_S: "e ∉ ab" shows "∃d'e. path d'e d' e" proof (rule ccontr) assume "¬(∃d'e. path d'e d' e)" hence "¬(∃R∈𝒫. d'∈R ∧ e∈R ∧ d'≠e)" by blast hence "¬(∃R∈𝒫. e∈R ∧ d'∈R)" using d'_def(3) by blast moreover have "ab∈𝒫 ∧ e∈ℰ ∧ e∉ab" by (simp add: e_event e_notin_S path_ab) ultimately have "d'∈ unreach-on ab from e" unfolding unreachable_subset_def using d'_def(2) by blast thus False using d'_def(1) by auto qed lemma unreachable_bounded_path: assumes S_neq_ab: "S ≠ ab" and a_inS: "a ∈ S" and e_inS: "e ∈ S" and e_neq_a: "e ≠ a" and path_S: "S ∈ 𝒫" and path_ab: "path ab a b" and path_be: "path be b e" and no_de: "¬(∃de. path de d e)" and abd:"[a;b;d]" obtains d' d'e where "d'∈ab ∧ path d'e d' e ∧ [b; d; d']" proof - have e_event: "e∈ℰ" using e_inS path_S by auto have "e∉ab" using S_neq_ab a_inS e_inS e_neq_a eq_paths path_S path_ab by auto have "ab∈𝒫 ∧ e∉ab" using S_neq_ab a_inS e_inS e_neq_a eq_paths path_S path_ab by auto have "b ∈ ab - unreach-on ab from e" using cross_in_reachable path_ab path_be by blast have "d ∈ unreach-on ab from e" using no_de abd path_ab e_event ‹e∉ab› betw_c_in_path unreachable_bounded_path_only by blast have "∃d' d'e. d'∈ab ∧ path d'e d' e ∧ [b; d; d']" proof - obtain d' where "[b; d; d']" "d'∈ab" "d'∉ unreach-on ab from e" "b≠d'" "e≠d'" using unreachable_set_bounded ‹b ∈ ab - unreach-on ab from e› ‹d ∈ unreach-on ab from e› e_event ‹e∉ab› path_ab by (metis DiffE) then obtain d'e where "path d'e d' e" using unreachable_bounded_path_only e_event ‹e∉ab› p