# Theory TernaryOrdering

(*  Title:      Schutz_Spacetime/TernaryOrdering.thy
Authors:    Richard Schmoetten, Jake Palmer and Jacques D. Fleuriot
University of Edinburgh, 2021
*)
theory TernaryOrdering
imports Util

begin

text ‹
Definition of chains using an ordering on sets of events
based on natural numbers, plus some proofs.
›

section ‹Totally ordered chains›

text ‹
Based on page 110 of Phil Scott's thesis and the following HOL Light definition:
\begin{verbatim}
let ORDERING = new_definition
ORDERING f X <=> (!n. (FINITE X ==> n < CARD X) ==> f n IN X)
/\ (!x. x IN X ==> ?n. (FINITE X ==> n < CARD X)
/\ f n = x)
/\ !n n' n''. (FINITE X ==> n'' < CARD X)
/\ n < n' /\ n' < n''
==> between (f n) (f n') (f n'');;
\end{verbatim}
I've made it strict for simplicity, and because that's how Schutz's ordering is. It could be
made more generic by taking in the function corresponding to $<$ as a paramater.
Main difference to Schutz: he has local order, not total (cf Theorem 2 and ‹local_ordering›).
›

definition ordering :: "(nat ⇒ 'a) ⇒ ('a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"ordering f ord X ≡ (∀n. (finite X ⟶ n < card X) ⟶ f n ∈ X)
∧ (∀x∈X. (∃n. (finite X ⟶ n < card X) ∧ f n = x))
∧ (∀n n' n''. (finite X ⟶ n'' < card X) ∧ n < n' ∧ n' < n''
⟶ ord (f n) (f n') (f n''))"

lemma finite_ordering_intro:
assumes "finite X"
and "∀n < card X. f n ∈ X"
and "∀x ∈ X. ∃n < card X. f n = x"
and "∀n n' n''. n < n' ∧ n' < n'' ∧ n'' < card X ⟶ ord (f n) (f n') (f n'')"
shows "ordering f ord X"
unfolding ordering_def by (simp add: assms)

lemma infinite_ordering_intro:
assumes "infinite X"
and "∀n::nat. f n ∈ X"
and "∀x ∈ X. ∃n::nat. f n = x"
and "∀n n' n''. n < n' ∧ n' < n'' ⟶ ord (f n) (f n') (f n'')"
shows "ordering f ord X"
unfolding ordering_def by (simp add: assms)

lemma ordering_ord_ijk:
assumes "ordering f ord X"
and "i < j ∧ j < k ∧ (finite X ⟶ k < card X)"
shows "ord (f i) (f j) (f k)"
by (metis ordering_def assms)

lemma empty_ordering [simp]: "∃f. ordering f ord {}"

lemma singleton_ordering [simp]: "∃f. ordering f ord {a}"
apply (rule_tac x = "λn. a" in exI)

lemma two_ordering [simp]: "∃f. ordering f ord {a, b}"
proof cases
assume "a = b"
thus ?thesis using singleton_ordering by simp
next
assume a_neq_b: "a ≠ b"
let ?f = "λn. if n = 0 then a else b"
have ordering1: "(∀n. (finite {a,b} ⟶ n < card {a,b}) ⟶ ?f n ∈ {a,b})" by simp
have local_ordering: "(∀x∈{a,b}. ∃n. (finite {a,b} ⟶ n < card {a,b}) ∧ ?f n = x)"
using a_neq_b all_not_in_conv card_Suc_eq card_0_eq card_gt_0_iff insert_iff lessI by auto
have ordering3: "(∀n n' n''. (finite {a,b} ⟶ n'' < card {a,b}) ∧ n < n' ∧ n' < n''
⟶ ord (?f n) (?f n') (?f n''))" using a_neq_b by auto
have "ordering ?f ord {a, b}" using ordering_def ordering1 local_ordering ordering3 by blast
thus ?thesis by auto
qed

lemma card_le2_ordering:
assumes finiteX: "finite X"
and card_le2: "card X ≤ 2"
shows "∃f. ordering f ord X"
proof -
have card012: "card X = 0 ∨ card X = 1 ∨ card X = 2" using card_le2 by auto
have card0: "card X = 0 ⟶ ?thesis" using finiteX by simp
have card1: "card X = 1 ⟶ ?thesis" using card_eq_SucD by fastforce
have card2: "card X = 2 ⟶ ?thesis" by (metis two_ordering card_eq_SucD numeral_2_eq_2)
thus ?thesis using card012 card0 card1 card2 by auto
qed

lemma ord_ordered:
assumes abc: "ord a b c"
and abc_neq: "a ≠ b ∧ a ≠ c ∧ b ≠ c"
shows "∃f. ordering f ord {a,b,c}"
apply (rule_tac x = "λn. if n = 0 then a else if n = 1 then b else c" in exI)
apply (unfold ordering_def)
using abc abc_neq by auto

lemma overlap_ordering:
assumes abc: "ord a b c"
and bcd: "ord b c d"
and abd: "ord a b d"
and acd: "ord a c d"
and abc_neq: "a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d"
shows "∃f. ordering f ord {a,b,c,d}"
proof -
let ?X = "{a,b,c,d}"
let ?f = "λn. if n = 0 then a else if n = 1 then b else if n = 2 then c else d"
have card4: "card ?X = 4" using abc bcd abd abc_neq by simp
have ordering1: "∀n. (finite ?X ⟶ n < card ?X) ⟶ ?f n ∈ ?X" by simp
have local_ordering: "∀x∈?X. ∃n. (finite ?X ⟶ n < card ?X) ∧ ?f n = x"
by (metis card4 One_nat_def Suc_1 Suc_lessI empty_iff insertE numeral_3_eq_3 numeral_eq_iff
numeral_eq_one_iff rel_simps(51) semiring_norm(85) semiring_norm(86) semiring_norm(87)
semiring_norm(89) zero_neq_numeral)
have ordering3: "(∀n n' n''. (finite ?X ⟶ n'' < card ?X) ∧ n < n' ∧ n' < n''
⟶ ord (?f n) (?f n') (?f n''))"
using card4 abc bcd abd acd card_0_eq card_insert_if finite.emptyI finite_insert less_antisym
less_one less_trans_Suc not_less_eq not_one_less_zero numeral_2_eq_2 by auto
have "ordering ?f ord ?X" using ordering1 local_ordering ordering3 ordering_def by blast
thus ?thesis by auto
qed

lemma overlap_ordering_alt1:
assumes abc: "ord a b c"
and bcd: "ord b c d"
and abc_bcd_abd: "∀ a b c d. ord a b c ∧ ord b c d ⟶ ord a b d"
and abc_bcd_acd: "∀ a b c d. ord a b c ∧ ord b c d ⟶ ord a c d"
and ord_distinct: "∀a b c. (ord a b c ⟶ a ≠ b ∧ a ≠ c ∧ b ≠ c)"
shows "∃f. ordering f ord {a,b,c,d}"
by (metis (full_types) assms overlap_ordering)

lemma overlap_ordering_alt2:
assumes abc: "ord a b c"
and bcd: "ord b c d"
and abd: "ord a b d"
and acd: "ord a c d"
and ord_distinct: "∀a b c. (ord a b c ⟶ a ≠ b ∧ a ≠ c ∧ b ≠ c)"
shows "∃f. ordering f ord {a,b,c,d}"
by (metis assms overlap_ordering)

lemma overlap_ordering_alt:
assumes abc: "ord a b c"
and bcd: "ord b c d"
and abc_bcd_abd: "∀ a b c d. ord a b c ∧ ord b c d ⟶ ord a b d"
and abc_bcd_acd: "∀ a b c d. ord a b c ∧ ord b c d ⟶ ord a c d"
and abc_neq: "a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d"
shows "∃f. ordering f ord {a,b,c,d}"
by (meson assms overlap_ordering)

text ‹
The lemmas below are easy to prove for ‹X = {}›, and if I included that case then I would have
to write a conditional definition in place of ‹{0..|X| - 1}›.
›

lemma finite_ordering_img: "⟦X ≠ {}; finite X; ordering f ord X⟧ ⟹ f  {0..card X - 1} = X"
by (force simp add: ordering_def image_def)

lemma inf_ordering_img: "⟦infinite X; ordering f ord X⟧ ⟹ f  {0..} = X"
by (auto simp add: ordering_def image_def)

lemma inf_ordering_inv_img: "⟦infinite X; ordering f ord X⟧ ⟹ f - X = {0..}"
by (auto simp add: ordering_def image_def)

lemma inf_ordering_img_inv_img: "⟦infinite X; ordering f ord X⟧ ⟹ f  f - X = X"
using inf_ordering_img by auto

lemma finite_ordering_inj_on: "⟦finite X; ordering f ord X⟧ ⟹ inj_on f {0..card X - 1}"
by (metis finite_ordering_img Suc_diff_1 atLeastAtMost_iff card_atLeastAtMost card_eq_0_iff
diff_0_eq_0 diff_zero eq_card_imp_inj_on gr0I inj_onI le_0_eq)

lemma finite_ordering_bij:
assumes orderingX: "ordering f ord X"
and finiteX: "finite X"
and non_empty: "X ≠ {}"
shows "bij_betw f {0..card X - 1} X"
proof -
have f_image: "f  {0..card X - 1} = X" by (metis orderingX finiteX finite_ordering_img non_empty)
thus ?thesis by (metis inj_on_imp_bij_betw orderingX finiteX finite_ordering_inj_on)
qed

lemma inf_ordering_inj':
assumes infX: "infinite X"
and f_ord: "ordering f ord X"
and ord_distinct: "∀a b c. (ord a b c ⟶ a ≠ b ∧ a ≠ c ∧ b ≠ c)"
and f_eq: "f m = f n"
shows "m = n"
proof (rule ccontr)
assume m_not_n: "m ≠ n"
have betw_3n: "∀n n' n''. n < n' ∧ n' < n'' ⟶ ord (f n) (f n') (f n'')"
using f_ord by (simp add: ordering_def infX)
thus False
proof cases
assume m_less_n: "m < n"
then obtain k where "n < k" by auto
then have "ord (f m) (f n) (f k)" using m_less_n betw_3n by simp
then have "f m ≠ f n" using ord_distinct by simp
thus ?thesis using f_eq by simp
next
assume "¬ m < n"
then have n_less_m: "n < m" using m_not_n by simp
then obtain k where "m < k" by auto
then have "ord (f n) (f m) (f k)" using n_less_m betw_3n by simp
then have "f n ≠ f m" using ord_distinct by simp
thus ?thesis using f_eq by simp
qed
qed

lemma inf_ordering_inj:
assumes "infinite X"
and "ordering f ord X"
and "∀a b c. (ord a b c ⟶ a ≠ b ∧ a ≠ c ∧ b ≠ c)"
shows "inj f"
using inf_ordering_inj' assms by (metis injI)

text ‹
The finite case is a little more difficult as I can't just choose some other natural number
to form the third part of the betweenness relation and the initial simplification isn't as nice.
Note that I cannot prove ‹inj f› (over the whole type that ‹f› is defined on, i.e. natural numbers),
because I need to capture the ‹m› and ‹n› that obey specific requirements for the finite case.
In order to prove ‹inj f›, I would have to extend the definition for ordering to include ‹m› and ‹n›
beyond ‹card X›, such that it is still injective. That would probably not be very useful.
›

lemma finite_ordering_inj:
assumes finiteX: "finite X"
and f_ord: "ordering f ord X"
and ord_distinct: "∀a b c. (ord a b c ⟶ a ≠ b ∧ a ≠ c ∧ b ≠ c)"
and m_less_card: "m < card X"
and n_less_card: "n < card X"
and f_eq: "f m = f n"
shows "m = n"
proof (rule ccontr)
assume m_not_n: "m ≠ n"
have surj_f: "∀x∈X. ∃n<card X. f n = x"
using f_ord by (simp add: ordering_def finiteX)
have betw_3n: "∀n n' n''. n'' < card X ∧ n < n' ∧ n' < n'' ⟶ ord (f n) (f n') (f n'')"
using f_ord by (simp add: ordering_def)
show False
proof cases
assume card_le2: "card X ≤ 2"
have card0: "card X = 0 ⟶ False" using m_less_card by simp
have card1: "card X = 1 ⟶ False" using m_less_card n_less_card m_not_n by simp
have card2: "card X = 2 ⟶ False"
proof (rule impI)
assume card_is_2: "card X = 2"
then have mn01: "m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1" using m_less_card n_less_card m_not_n by auto
then have "f m ≠ f n" using card_is_2 surj_f One_nat_def card_eq_SucD insertCI
less_2_cases numeral_2_eq_2 by (metis (no_types, lifting))
thus False using f_eq by simp
qed
show False using card0 card1 card2 card_le2 by simp
next
assume "¬ card X ≤ 2"
then have card_ge3: "card X ≥ 3" by simp
thus False
proof cases
assume m_less_n: "m < n"
then obtain k where k_pos: "k < m ∨ (m < k ∧ k < n) ∨ (n < k ∧ k < card X)"
using is_free_nat m_less_n n_less_card card_ge3 by blast
have k1: "k < m ⟶ord (f k) (f m) (f n)" using m_less_n n_less_card betw_3n by simp
have k2: "m < k ∧ k < n ⟶ ord (f m) (f k) (f n)" using m_less_n n_less_card betw_3n by simp
have k3: "n < k ∧ k < card X ⟶ ord (f m) (f n) (f k)" using m_less_n betw_3n by simp
have "f m ≠ f n" using k1 k2 k3 k_pos ord_distinct by auto
thus False using f_eq by simp
next
assume "¬ m < n"
then have n_less_m: "n < m" using m_not_n by simp
then obtain k where k_pos: "k < n ∨ (n < k ∧ k < m) ∨ (m < k ∧ k < card X)"
using is_free_nat n_less_m m_less_card card_ge3 by blast
have k1: "k < n ⟶ord (f k) (f n) (f m)" using n_less_m m_less_card betw_3n by simp
have k2: "n < k ∧ k < m ⟶ ord (f n) (f k) (f m)" using n_less_m m_less_card betw_3n by simp
have k3: "m < k ∧ k < card X ⟶ ord (f n) (f m) (f k)" using n_less_m betw_3n by simp
have "f n ≠ f m" using k1 k2 k3 k_pos ord_distinct by auto
thus False using f_eq by simp
qed
qed
qed

lemma ordering_inj:
assumes "ordering f ord X"
and "∀a b c. (ord a b c ⟶ a ≠ b ∧ a ≠ c ∧ b ≠ c)"
and "finite X ⟶ m < card X"
and "finite X ⟶ n < card X"
and "f m = f n"
shows "m = n"
using inf_ordering_inj' finite_ordering_inj assms by blast

lemma ordering_sym:
assumes ord_sym: "⋀a b c. ord a b c ⟹ ord c b a"
and "finite X"
and "ordering f ord X"
shows "ordering (λn. f (card X - 1 - n)) ord X"
unfolding ordering_def using assms(2)
apply auto
apply (metis ordering_def assms(3) card_0_eq card_gt_0_iff diff_Suc_less gr_implies_not0)
proof -
fix x
assume "finite X"
assume "x ∈ X"
obtain n where "finite X ⟶ n < card X" and "f n = x"
by (metis ordering_def ‹x ∈ X› assms(3))
have "f (card X - ((card X - 1 - n) + 1)) = x"
by (simp add: Suc_leI ‹f n = x› ‹finite X ⟶ n < card X› assms(2))
thus "∃n<card X. f (card X - Suc n) = x"
by (metis ‹x ∈ X› add.commute assms(2) card_Diff_singleton card_Suc_Diff1 diff_less_Suc plus_1_eq_Suc)
next
fix n n' n''
assume "finite X"
assume "n'' < card X" "n < n'" "n' < n''"
have "ord (f (card X - Suc n'')) (f (card X - Suc n')) (f (card X - Suc n))"
using assms(3) unfolding ordering_def
using ‹n < n'› ‹n' < n''› ‹n'' < card X› diff_less_mono2 by auto
thus " ord (f (card X - Suc n)) (f (card X - Suc n')) (f (card X - Suc n''))"
using ord_sym by blast
qed

lemma  zero_into_ordering:
assumes "ordering f betw X"
and "X ≠ {}"
shows "(f 0) ∈ X"
using ordering_def
by (metis assms card_eq_0_iff gr_implies_not0 linorder_neqE_nat)

section "Locally ordered chains"
text ‹Definitions for Schutz-like chains, with local order only.›

definition local_ordering :: "(nat ⇒ 'a) ⇒ ('a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where "local_ordering f ord X
≡ (∀n. (finite X ⟶ n < card X) ⟶ f n ∈ X) ∧
(∀x∈X. ∃n. (finite X ⟶ n < card X) ∧ f n = x) ∧
(∀n. (finite X ⟶ Suc (Suc n) < card X) ⟶ ord (f n) (f (Suc n)) (f (Suc (Suc n))))"

lemma finite_local_ordering_intro:
assumes "finite X"
and "∀n < card X. f n ∈ X"
and "∀x ∈ X. ∃n < card X. f n = x"
and "∀n n' n''. Suc n = n' ∧ Suc n' = n'' ∧ n'' < card X ⟶ ord (f n) (f n') (f n'')"
shows "local_ordering f ord X"
unfolding local_ordering_def by (simp add: assms)

lemma infinite_local_ordering_intro:
assumes "infinite X"
and "∀n::nat. f n ∈ X"
and "∀x ∈ X. ∃n::nat. f n = x"
and "∀n n' n''. Suc n = n' ∧ Suc n' = n'' ⟶ ord (f n) (f n') (f n'')"
shows "local_ordering f ord X"
using assms unfolding local_ordering_def by metis

lemma total_implies_local:
"ordering f ord X ⟹ local_ordering f ord X"
unfolding ordering_def local_ordering_def
using lessI by presburger

lemma ordering_ord_ijk_loc:
assumes "local_ordering f ord X"
and "finite X ⟶ Suc (Suc i) < card X"
shows "ord (f i) (f (Suc i)) (f (Suc (Suc i)))"
by (metis local_ordering_def assms)

lemma empty_ordering_loc [simp]:
"∃f. local_ordering f ord {}"

lemma singleton_ordered_loc [simp]:
"local_ordering f ord {f 0}"
unfolding local_ordering_def by simp

lemma singleton_ordering_loc [simp]:
"∃f. local_ordering f ord {a}"
using singleton_ordered_loc by fast

lemma two_ordered_loc:
assumes "a = f 0" and "b = f 1"
shows "local_ordering f ord {a, b}"
proof cases
assume "a = b"
thus ?thesis using assms singleton_ordered_loc by (metis insert_absorb2)
next
assume a_neq_b: "a ≠ b"
hence "(∀n. (finite {a,b} ⟶ n < card {a,b}) ⟶ f n ∈ {a,b})"
using assms by (metis One_nat_def card.infinite card_2_iff fact_0 fact_2 insert_iff less_2_cases_iff)
moreover have "(∀x∈{a,b}. ∃n. (finite {a,b} ⟶ n < card {a,b}) ∧ f n = x)"
using assms a_neq_b all_not_in_conv card_Suc_eq card_0_eq card_gt_0_iff insert_iff lessI by auto
moreover have "(∀n. (finite {a,b} ⟶ Suc (Suc n) < card {a,b})
⟶ ord (f n) (f (Suc n)) (f (Suc (Suc n))))"
using a_neq_b by auto
ultimately have "local_ordering f ord {a, b}"
using local_ordering_def by blast
thus ?thesis by auto
qed

lemma two_ordering_loc [simp]:
"∃f. local_ordering f ord {a, b}"
using total_implies_local two_ordering by fastforce

lemma card_le2_ordering_loc:
assumes finiteX: "finite X"
and card_le2: "card X ≤ 2"
shows "∃f. local_ordering f ord X"
using assms total_implies_local card_le2_ordering by metis

lemma ord_ordered_loc:
assumes abc: "ord a b c"
and abc_neq: "a ≠ b ∧ a ≠ c ∧ b ≠ c"
shows "∃f. local_ordering f ord {a,b,c}"
using assms total_implies_local ord_ordered by metis

lemma overlap_ordering_loc:
assumes abc: "ord a b c"
and bcd: "ord b c d"
and abd: "ord a b d"
and acd: "ord a c d"
and abc_neq: "a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d"
shows "∃f. local_ordering f ord {a,b,c,d}"
using overlap_ordering[OF assms] total_implies_local by blast

lemma ordering_sym_loc:
assumes ord_sym: "⋀a b c. ord a b c ⟹ ord c b a"
and "finite X"
and "local_ordering f ord X"
shows "local_ordering (λn. f (card X - 1 - n)) ord X"
unfolding local_ordering_def using assms(2) apply auto
apply (metis local_ordering_def assms(3) card_0_eq card_gt_0_iff diff_Suc_less gr_implies_not0)
proof -
fix x
assume "finite X"
assume "x ∈ X"
obtain n where "finite X ⟶ n < card X" and "f n = x"
by (metis local_ordering_def ‹x ∈ X› assms(3))
have "f (card X - ((card X - 1 - n) + 1)) = x"
by (simp add: Suc_leI ‹f n = x› ‹finite X ⟶ n < card X› assms(2))
thus "∃n<card X. f (card X - Suc n) = x"
by (metis ‹x ∈ X› add.commute assms(2) card_Diff_singleton card_Suc_Diff1 diff_less_Suc plus_1_eq_Suc)
next
fix n
let ?n1 = "Suc n"
let ?n2 = "Suc ?n1"
assume "finite X"
assume "Suc (Suc n) < card X"
have "ord (f (card X - Suc ?n2)) (f (card X - Suc ?n1)) (f (card X - Suc n))"
using assms(3) unfolding local_ordering_def
using ‹Suc (Suc n) < card X› by (metis
Suc_diff_Suc Suc_lessD card_eq_0_iff card_gt_0_iff diff_less gr_implies_not0 zero_less_Suc)
thus " ord (f (card X - Suc n)) (f (card X - Suc ?n1)) (f (card X - Suc ?n2))"
using ord_sym by blast
qed

lemma  zero_into_ordering_loc:
assumes "local_ordering f betw X"
and "X ≠ {}"
shows "(f 0) ∈ X"
using local_ordering_def by (metis assms card_eq_0_iff gr_implies_not0 linorder_neqE_nat)

end