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 {}"
  by (simp add: ordering_def)

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

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 {}"
  by (simp add: local_ordering_def)

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