# Theory TemporalOrderOnPath

(*  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

lemma between_chain: "[a;b;c] ⟹ ch {a,b,c}"
proof -
assume "[a;b;c]"
hence "∃f. local_ordering f betw {a,b,c}"
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
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
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

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"
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"
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"

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
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"
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≠{}"
hence "card P ≠ 0"
moreover have "¬(card P ≥ 1)"
using path_card_nil
ultimately show False
by simp
qed

end (* contex MinkowskiSpacetime *)

section "3.5 Second collinearity theorem"

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