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)
                      (xX. (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: "xX. 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) 
      (xX. 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