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