Theory 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). XA // R. x  X  y  X} = R"
proof
  show "{(x, y). XA // R. x  X  y  X}  R"
  proof
    fix xy
    assume "xy  {(x, y). XA // 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). XA // 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). XA // R. x  X  y  X}"
      by auto
    from this show "xy  {(x, y). XA // 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). XP. x  X  y  X}"])
  show "R{R. equiv A R}. {(x, y). XA // R. x  X  y  X} = R"
    by (simp add: equiv_relation_of_partition_of)
  show "P{P. partition_on A P}. A // {(x, y). XP. 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). XP. 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). XP. x  X  y  X}"])
  show "R{R. equiv A R  card (A // R) = k}. {(x, y). XA // 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). XP. 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). XP. 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