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 "x∈X" and "y∈X" and "z∈X" and "x≠y" and "x≠z" and "y≠z"
  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 "(∃x∈X. ∃y∈X. ∃z∈X. x ≠ y ∧ y ≠ z ∧ x ≠ z)"
proof -
  obtain x y where 1: "x∈X" "y∈X" "y≠x"
    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: "z∈X" "x≠z" "z≠y"
    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 ⟷ x≠y ∧ x≠z ∧ y≠z"
  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: "S1∈X ∧ S2∈X ∧ S3∈X ∧ S4∈X" 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