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