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

text ‹Helpful proofs on sets.›

lemma set_le_two [simp]: "card {a, b}  2"
  by (simp add: card_insert_if)

lemma set_le_three [simp]: "card {a, b, c}  3"
  by (simp add: card_insert_if)

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"
  by (simp add: eval_nat_numeral card_insert_if)

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"
    apply (simp add: eval_nat_numeral)
    by (auto simp add: card_le_Suc_iff)
  thus "?card3 X"
    using Finite_Set.card_subset_eq card X = 3
    apply (simp add: eval_nat_numeral)
    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"
    apply (simp add: eval_nat_numeral)
    by (auto simp add: card_le_Suc_iff)
  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
    apply (simp add: eval_nat_numeral)
    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