Theory Card_Equiv_Relations.Card_Equiv_Relations

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Cardinality of Equivalence Relations›

theory Card_Equiv_Relations
imports
  Card_Partitions.Card_Partitions
  Bell_Numbers_Spivey.Bell_Numbers
begin

subsection ‹Bijection between Equivalence Relations and Set Partitions›

subsubsection ‹Possibly Interesting Theorem for @{theory HOL.Equiv_Relations}›

text ‹This theorem was historically useful in this theory, but
is now after some proof refactoring not needed here anymore.
Possibly it is an interesting fact about equivalence relations, though.
›

lemma equiv_quotient_eq_quotient_on_UNIV:
  assumes "equiv A R"
  shows "A // R = (UNIV // R) - {{}}"
proof
  show "UNIV // R - {{}} ⊆ A // R"
  proof
    fix X
    assume "X ∈ UNIV // R - {{}}"
    from this obtain x where "X = R `` {x}" and "X ≠ {}"
      by (auto elim!: quotientE)
    from this have "x ∈ A"
      using ‹equiv A R› equiv_class_eq_iff by fastforce
    from this ‹X = R `` {x}› show "X ∈ A // R"
      by (auto intro!: quotientI)
  qed
next
  show "A // R ⊆ UNIV // R - {{}}"
  proof
    fix X
    assume "X ∈ A // R"
    from this have "X ≠ {}"
      using ‹equiv A R› in_quotient_imp_non_empty by auto
    moreover from ‹X ∈ A // R› have "X ∈ UNIV // R"
      by (metis UNIV_I assms proj_Eps proj_preserves)
    ultimately show "X ∈ UNIV // R - {{}}" by simp
  qed
qed

subsubsection ‹Dedicated Facts for Bijection Proof›

(* TODO: rename to fit Disjoint_Sets' naming scheme and move to Disjoint_Sets *)
lemma equiv_relation_of_partition_of:
  assumes "equiv A R"
  shows "{(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X} = R"
proof
  show "{(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X} ⊆ R"
  proof
    fix xy
    assume "xy ∈ {(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X}"
    from this obtain x y and X where "xy = (x, y)"
      and "X ∈ A // R" and "x ∈ X" "y ∈ X"
      by auto
    from ‹X ∈ A // R› obtain z where "X = R `` {z}"
      by (auto elim: quotientE)
    show "xy ∈ R"
      using ‹xy = (x, y)› ‹X = R `` {z}› ‹x ∈ X› ‹y ∈ X› ‹equiv A R›
      by (simp add: equiv_class_eq_iff)
  qed
next
  show "R ⊆ {(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X}"
  proof
    fix xy
    assume "xy ∈ R"
    obtain x y where "xy = (x, y)" by fastforce
    from ‹xy ∈ R› have "(x, y) ∈ R"
      using ‹xy = (x, y)› by simp
    have "R `` {x} ∈ A // R"
      using ‹equiv A R› ‹(x, y) ∈ R›
      by (simp add: equiv_class_eq_iff quotientI)
    moreover have "x ∈ R `` {x}"
      using ‹(x, y) ∈ R› ‹equiv A R›
      by (meson equiv_class_eq_iff equiv_class_self)
    moreover have "y ∈ R `` {x}"
      using ‹(x, y) ∈ R› ‹equiv A R› by simp
    ultimately have "(x, y) ∈ {(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X}"
      by auto
    from this show "xy ∈ {(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X}"
      using ‹xy = (x, y)› by simp
  qed
qed

subsubsection ‹Bijection Proof›

lemma bij_betw_partition_of:
  "bij_betw (λR. A // R) {R. equiv A R} {P. partition_on A P}"
proof (rule bij_betw_byWitness[where f'="λP. {(x, y). ∃X∈P. x ∈ X ∧ y ∈ X}"])
  show "∀R∈{R. equiv A R}. {(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X} = R"
    by (simp add: equiv_relation_of_partition_of)
  show "∀P∈{P. partition_on A P}. A // {(x, y). ∃X∈P. x ∈ X ∧ y ∈ X} = P"
    by (simp add: partition_on_eq_quotient)
  show "(λR. A // R) ` {R. equiv A R} ⊆ {P. partition_on A P}"
    using partition_on_quotient by auto
  show "(λP. {(x, y). ∃X∈P. x ∈ X ∧ y ∈ X}) ` {P. partition_on A P} ⊆ {R. equiv A R}"
    using equiv_partition_on by auto
qed

lemma bij_betw_partition_of_equiv_with_k_classes:
  "bij_betw (λR. A // R) {R. equiv A R ∧ card (A // R) = k} {P. partition_on A P ∧ card P = k}"
proof (rule bij_betw_byWitness[where f'="λP. {(x, y). ∃X∈P. x ∈ X ∧ y ∈ X}"])
  show "∀R∈{R. equiv A R ∧ card (A // R) = k}. {(x, y). ∃X∈A // R. x ∈ X ∧ y ∈ X} = R"
    by (auto simp add: equiv_relation_of_partition_of)
  show "∀P∈{P. partition_on A P ∧ card P = k}. A // {(x, y). ∃X∈P. x ∈ X ∧ y ∈ X} = P"
    by (auto simp add: partition_on_eq_quotient)
  show "(λR. A // R) ` {R. equiv A R ∧ card (A // R) = k} ⊆ {P. partition_on A P ∧ card P = k}"
    using partition_on_quotient by auto
  show "(λP. {(x, y). ∃X∈P. x ∈ X ∧ y ∈ X}) ` {P. partition_on A P ∧ card P = k} ⊆ {R. equiv A R ∧ card (A // R) = k}"
    using equiv_partition_on by (auto simp add: partition_on_eq_quotient)
qed

subsection ‹Finiteness of Equivalence Relations›

lemma finite_equiv:
  assumes "finite A"
  shows "finite {R. equiv A R}"
proof -
  have "bij_betw (λR. A // R) {R. equiv A R} {P. partition_on A P}"
    by (rule bij_betw_partition_of)
  from this show "finite {R. equiv A R}"
    using ‹finite A› finitely_many_partition_on by (simp add: bij_betw_finite)
qed

subsection ‹Cardinality of Equivalence Relations›

theorem card_equiv_rel_eq_card_partitions:
  "card {R. equiv A R} = card {P. partition_on A P}"
proof -
  have "bij_betw (λR. A // R) {R. equiv A R} {P. partition_on A P}"
    by (rule bij_betw_partition_of)
  from this show "card {R. equiv A R} = card {P. partition_on A P}"
    by (rule bij_betw_same_card)
qed

corollary card_equiv_rel_eq_Bell:
  assumes "finite A"
  shows "card {R. equiv A R} = Bell (card A)"
using assms Bell_altdef card_equiv_rel_eq_card_partitions by force

corollary card_equiv_rel_eq_sum_Stirling:
  assumes "finite A"
  shows "card {R. equiv A R} = sum (Stirling (card A)) {..card A}"
using assms card_equiv_rel_eq_Bell Bell_Stirling_eq by simp

theorem card_equiv_k_classes_eq_card_partitions_k_parts:
  "card {R. equiv A R ∧ card (A // R) = k} = card {P. partition_on A P ∧ card P = k}"
proof -
  have "bij_betw (λR. A // R) {R. equiv A R ∧ card (A // R) = k} {P. partition_on A P ∧ card P = k}"
    by (rule bij_betw_partition_of_equiv_with_k_classes)
  from this show "card {R. equiv A R ∧ card (A // R) = k} = card {P. partition_on A P ∧ card P = k}"
    by (rule bij_betw_same_card)
qed

corollary
  assumes "finite A"
  shows "card {R. equiv A R ∧ card (A // R) = k} = Stirling (card A) k"
using card_equiv_k_classes_eq_card_partitions_k_parts
  card_partition_on[OF ‹finite A›] by metis

end