# Theory Util

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

begin

text ‹Some "utility" proofs -- little proofs that come in handy every now and then.›

text ‹
We need this in order to obtain a natural number which can be passed to the ordering function,
distinct from two others, in the case of a finite set of events with cardinality a least 3.
›

lemma is_free_nat:
assumes "(m::nat) < n"
and "n < c"
and "c  3"
shows "k::nat. k < m  (m < k  k < n)  (n < k  k < c)"
using assms by presburger

lemma set_le_two [simp]: "card {a, b}  2"

lemma set_le_three [simp]: "card {a, b, c}  3"

lemma card_subset: "card Y = n; Y  X  card X  n  infinite X"
using card_mono by blast

lemma card_subset_finite: "finite X; card Y = n; Y  X  card X  n"
using card_subset by auto

lemma three_subset: "x  y; x  z; y  z; {x,y,z}  X  card X  3  infinite X"
apply (case_tac "finite X")
apply (auto simp : card_mono)
apply (erule_tac Y = "{x,y,z}" in card_subset_finite)
by auto

lemma three_in_set3:
assumes "card X  3"
obtains x y z where "xX" and "yX" and "zX" and "xy" and "xz" and "yz"
using assms by (auto simp add: card_le_Suc_iff numeral_3_eq_3)

lemma card_Collect_nat:
assumes "(j::nat)>i"
shows "card {i..j} = j-i+1"
using card_atLeastAtMost
using Suc_diff_le assms le_eq_less_or_eq by presburger

lemma inf_3_elms: assumes "infinite X" shows "(xX. yX. zX. x  y  y  z  x  z)"
proof -
obtain x y where 1: "xX" "yX" "yx"
by (metis assms finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI)
have "infinite (X-{x,y})"
using infinite_remove by (simp add: assms)
then obtain z where 2: "zX" "xz" "zy"
using infinite_imp_nonempty by (metis Diff_eq_empty_iff insertCI subset_eq)
show ?thesis using 1 2 by blast
qed

lemma card_3_dist: "card {x,y,z} = 3  xy  xz  yz"

lemma card_3_eq:
"card X = 3  (x y z. X={x,y,z}  x  y  y  z  x  z)"
(is "card X = 3  ?card3 X")
proof
assume asm: "card X = 3" hence "card X  3" by simp
then obtain x y z where "x  y  y  z  x  z" "{x,y,z}  X"
thus "?card3 X"
using Finite_Set.card_subset_eq card X = 3
by (smt (verit, ccfv_threshold) {x, y, z}  X card.empty card.infinite card_insert_if
card_subset_eq empty_iff finite.emptyI insertE nat.distinct(1))
next
show "?card3 X  card X = 3"
by (smt (z3) card.empty card.insert eval_nat_numeral(2) finite.intros(1) finite_insert insertE
insert_absorb insert_not_empty numeral_3_eq_3 semiring_norm(26,27))
qed

lemma card_3_eq':
"card X = 3; card {a,b,c} = 3; {a,b,c} X  X = {a,b,c}"
"card X = 3; a  X; b  X; c  X; a  b; a  c; b  c  X = {a,b,c}"
proof -
show "card X = 3; card {a,b,c} = 3; {a,b,c} X  X = {a,b,c}"
by (metis card.infinite card_subset_eq zero_neq_numeral)
thus "card X = 3; a  X; b  X; c  X; a  b; a  c; b  c  X = {a,b,c}"
by (meson card_3_dist empty_subsetI insert_subset)
qed

lemma card_4_eq:
"card X = 4  (S1. S2. S3. S4. X = {S1, S2, S3, S4}
S1  S2  S1  S3  S1  S4  S2  S3  S2  S4  S3  S4)"
(is "card X = 4  ?card4 X")
proof
assume "card X = 4"
hence "card X  4" by auto
then obtain S1 S2 S3 S4 where
0: "S1X  S2X  S3X  S4X" and
1: "S1  S2  S1  S3  S1  S4  S2  S3  S2  S4  S3  S4"
then have 2: "{S1, S2, S3, S4}  X" "card {S1, S2, S3, S4} = 4" by auto
have "X = {S1, S2, S3, S4}"
using Finite_Set.card_subset_eq card X = 4
by (smt (z3) card X = 4 2 card.infinite card_subset_eq nat.distinct(1))
thus "?card4 X" using 1 by blast
next
show "?card4 X  card X = 4"
by (smt (z3) card.empty card.insert eval_nat_numeral(2) finite.intros(1) finite_insert insertE
insert_absorb insert_not_empty numeral_3_eq_3 semiring_norm(26,27))
qed

text ‹These lemmas make life easier with some of the ordering proofs.›

lemma less_3_cases: "n < 3  n = 0  n = Suc 0  n = Suc (Suc 0)"
by auto

end