Theory Card_Partitions

theory Card_Partitions
imports Stirling Set_Partition Injectivity_Solver
(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Cardinality of Set Partitions›

theory Card_Partitions
imports
  "HOL-Library.Stirling"
  Set_Partition
  Injectivity_Solver
begin

lemma set_partition_on_insert_with_fixed_card_eq:
  assumes "finite A"
  assumes "a ∉ A"
  shows "{P. partition_on (insert a A) P ∧ card P = Suc k} = (do {
     P <- {P. partition_on A P ∧ card P = Suc k};
     p <- P;
     {insert (insert a p) (P - {p})}
  })
  ∪ (do {
    P <- {P. partition_on A P ∧ card P = k};
    {insert {a} P}
  })" (is "?S = ?T")
proof
  show "?S ⊆ ?T"
  proof
    fix P
    assume "P ∈ {P. partition_on (insert a A) P ∧ card P = Suc k}"
    from this have "partition_on (insert a A) P" and "card P = Suc k" by auto
    show "P ∈ ?T"
    proof cases
      assume "{a} ∈ P"
      have "partition_on A (P - {{a}})"
        using ‹{a} ∈ P› ‹partition_on (insert a A) P›[THEN partition_on_Diff, of "{{a}}"] ‹a ∉ A›
        by auto
      moreover from ‹{a} ∈ P› ‹card P = Suc k› have "card (P - {{a}}) = k"
        by (subst card_Diff_singleton) (auto intro: card_ge_0_finite)
      moreover from ‹{a} ∈ P› have "P = insert {a} (P - {{a}})" by auto
      ultimately have "P ∈ {P. partition_on A P ∧ card P = k} ⤜ (λP. {insert {a} P})"
        by auto
      from this show ?thesis by auto
    next
      assume "{a} ∉ P"
      let ?p' = "(THE X. a ∈ X ∧ X ∈ P)"
      let ?p = "(THE X. a ∈ X ∧ X ∈ P) - {a}"
      let ?P' = "insert ?p (P - {?p'})"
      from ‹partition_on (insert a A) P› have "a ∈ (THE X. a ∈ X ∧ X ∈ P)"
        using partition_on_in_the_unique_part by fastforce
      from ‹partition_on (insert a A) P› have "(THE X. a ∈ X ∧ X ∈ P) ∈ P"
        using partition_on_the_part_mem by fastforce
      from this ‹partition_on (insert a A) P› have "(THE X. a ∈ X ∧ X ∈ P) - {a} ∉ P"
        using partition_subset_imp_notin ‹a ∈ (THE X. a ∈ X ∧ X ∈ P)› by blast
      have "(THE X. a ∈ X ∧ X ∈ P) ≠ {a}"
        using ‹(THE X. a ∈ X ∧ X ∈ P) ∈ P› ‹{a} ∉ P› by auto
      from ‹partition_on (insert a A) P› have "(THE X. a ∈ X ∧ X ∈ P) ⊆ insert a A"
        using ‹(THE X. a ∈ X ∧ X ∈ P) ∈ P› partition_onD1 by fastforce
      note facts_on_the_part_of = ‹a ∈ (THE X. a ∈ X ∧ X ∈ P)› ‹(THE X. a ∈ X ∧ X ∈ P) ∈ P›
        ‹(THE X. a ∈ X ∧ X ∈ P) - {a} ∉ P› ‹(THE X. a ∈ X ∧ X ∈ P) ≠ {a}›
        ‹(THE X. a ∈ X ∧ X ∈ P) ⊆ insert a A›
      from ‹partition_on (insert a A) P› ‹finite A› have "finite P"
        by (meson finite.insertI finite_elements)
      from ‹partition_on (insert a A) P› ‹a ∉ A› have "partition_on (A - ?p) (P - {?p'})"
        using facts_on_the_part_of by (auto intro: partition_on_remove_singleton)
      from this have "partition_on A ?P'"
        using facts_on_the_part_of by (auto intro: partition_on_insert simp add: disjnt_iff)
      moreover have "card ?P' = Suc k"
      proof -
        from ‹card P = Suc k› have "card (P - {THE X. a ∈ X ∧ X ∈ P}) = k"
          using ‹finite P› ‹(THE X. a ∈ X ∧ X ∈ P) ∈ P› by simp
        from this show ?thesis
          using ‹finite P› ‹(THE X. a ∈ X ∧ X ∈ P) - {a} ∉ P› by (simp add: card_insert_if)
      qed
      moreover have "?p ∈ ?P'" by auto
      moreover have "P = insert (insert a ?p) (?P' - {?p})"
        using facts_on_the_part_of by (auto simp add: insert_absorb)
      ultimately have "P ∈ {P. partition_on A P ∧ card P = Suc k} ⤜ (λP. P ⤜ (λp. {insert (insert a p) (P - {p})}))"
        by auto
      then show ?thesis by auto
    qed
  qed
next
  show "?T ⊆ ?S"
  proof
    fix P
    assume "P ∈ ?T" (is "_ ∈ ?subexpr1 ∪ ?subexpr2")
    from this show "P ∈ ?S"
    proof
      assume "P ∈ ?subexpr1"
      from this obtain p P' where "P = insert (insert a p) (P' - {p})"
        and "partition_on A P'" and "card P' = Suc k" and "p ∈ P'"  by auto
      from ‹p ∈ P'› ‹partition_on A P'› have "partition_on (A - p) (P' - {p})"
        by (simp add: partition_on_remove_singleton)
      from ‹partition_on A P'› ‹finite A› have "finite P"
        using ‹P = _› finite_elements by auto
      from ‹partition_on A P'› ‹a ∉ A› have "insert a p ∉ P' - {p}"
        using partition_onD1 by fastforce
      from ‹P = _› this ‹card P' = Suc k› ‹finite P› ‹p ∈ P'›
      have "card P = Suc k" by auto
      moreover have "partition_on (insert a A) P"
        using ‹partition_on (A - p) (P' - {p})› ‹a ∉ A› ‹p ∈ P'› ‹partition_on A P'› ‹P = _›
        by (auto intro!: partition_on_insert dest: partition_onD1 simp add: disjnt_iff)
      ultimately show "P ∈ ?S" by auto
    next
      assume "P ∈ ?subexpr2"
      from this obtain P' where "P = insert {a} P'" and "partition_on A P'" and "card P' = k" by auto
      from ‹partition_on A P'› ‹finite A› have "finite P"
        using ‹P = insert {a} P'› finite_elements by auto
      from ‹partition_on A P'› ‹a ∉ A› have "{a} ∉ P'"
        using partition_onD1 by fastforce
      from ‹P = insert {a} P'› ‹card P' = k› this ‹finite P› have "card P = Suc k" by auto
      moreover from ‹partition_on A P'› ‹a ∉ A› have "partition_on (insert a A) P"
        using ‹P = insert {a} P'› by (simp add: partition_on_insert_singleton)
      ultimately show "P ∈ ?S" by auto
    qed
  qed
qed

lemma injectivity_subexpr1:
  assumes "a ∉ A"
  assumes "X ∈ P ∧ X' ∈ P'"
  assumes "insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})"
  assumes "(partition_on A P ∧ card P = Suc k') ∧ (partition_on A P' ∧ card P' = Suc k')"
  shows "P = P'" and "X = X'"
proof -
  from assms(1, 2, 4) have "a ∉ X" "a ∉ X'"
    using partition_onD1 by auto
  from assms(1, 4) have "insert a X ∉ P" "insert a X' ∉ P'"
    using partition_onD1 by auto
  from assms(1, 3, 4) have "insert a X = insert a X'"
    by (metis Diff_iff insertE insertI1 mem_simps(9) partition_onD1)
  from this ‹a ∉ X'› ‹a ∉ X› show "X = X'"
    by (meson insert_ident)
  from assms(2, 3) show "P = P'"
    using ‹insert a X = insert a X'› ‹insert a X ∉ P› ‹insert a X' ∉ P'›
    by (metis insert_Diff insert_absorb insert_commute insert_ident)
qed

lemma injectivity_subexpr2:
  assumes "a ∉ A"
  assumes "insert {a} P = insert {a} P'"
  assumes "(partition_on A P ∧ card P = k') ∧ partition_on A P' ∧ card P' = k'"
  shows "P = P'"
proof -
  from assms(1, 3) have "{a} ∉ P" and "{a} ∉ P'"
    using partition_onD1 by auto
  from ‹{a} ∉ P› have "P = insert {a} P - {{a}}" by simp
  also from ‹insert {a} P = insert {a} P'› have "… = insert {a} P' - {{a}}" by simp
  also from ‹{a} ∉ P'› have "… = P'" by simp
  finally show ?thesis .
qed

theorem card_partition_on:
  assumes "finite A"
  shows "card {P. partition_on A P ∧ card P = k} = Stirling (card A) k"
using assms
proof (induct A arbitrary: k)
  case empty
    have eq: "{P. P = {} ∧ card P = 0} = {{}}" by auto
    show ?case by (cases k) (auto simp add: partition_on_empty eq)
next
  case (insert a A)
  from this show ?case
  proof (cases k)
    case 0
    from insert(1) have empty: "{P. partition_on (insert a A) P ∧ card P = 0} = {}"
      unfolding partition_on_def by (auto simp add: card_eq_0_iff finite_UnionD)
    from 0 insert show ?thesis by (auto simp add: empty)
  next
    case (Suc k')
    let ?subexpr1 = "do {
      P <- {P. partition_on A P ∧ card P = Suc k'};
      p <- P;
      {insert (insert a p) (P - {p})}
    }"
    let ?subexpr2 = "do {
      P <- {P. partition_on A P ∧ card P = k'};
      {insert {a} P}
    }"
    let ?expr = "?subexpr1 ∪ ?subexpr2"
    have "card {P. partition_on (insert a A) P ∧ card P = k} = card ?expr"
      using ‹finite A› ‹a ∉ A› ‹k = Suc k'› by (simp add: set_partition_on_insert_with_fixed_card_eq)
    also have "card ?expr = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'"
    proof -
      have "finite ?subexpr1 ∧ card ?subexpr1 = Stirling (card A) (Suc k') * Suc k'"
      proof -
        from ‹finite A› have "finite {P. partition_on A P ∧ card P = Suc k'}"
          by (simp add: finitely_many_partition_on)
        moreover have "∀X∈{P. partition_on A P ∧ card P = Suc k'}. finite (X ⤜ (λp. {insert (insert a p) (X - {p})}))"
          using finite_elements ‹finite A› finite_bind
          by (metis (no_types, lifting) finite.emptyI finite_insert mem_Collect_eq)
        moreover have "disjoint_family_on (λP. P ⤜ (λp. {insert (insert a p) (P - {p})})) {P. partition_on A P ∧ card P = Suc k'}"
          by (injectivity_solver rule: injectivity_subexpr1(1)[OF ‹a ∉ A›])
        moreover have "card (P ⤜ (λp. {insert (insert a p) (P - {p})})) = Suc k'"
          if "P ∈ {P. partition_on A P ∧ card P = Suc k'}" for P
        proof -
          from that ‹finite A› have "finite P"
            using finite_elements by blast
          moreover have "inj_on (λp. insert (insert a p) (P - {p})) P"
            using that injectivity_subexpr1(2)[OF ‹a ∉ A›] by (simp add: inj_onI)
          moreover from that have "card P = Suc k'" by simp
          ultimately show ?thesis by (simp add: card_bind_singleton)
        qed
        ultimately have "card ?subexpr1 = card {P. partition_on A P ∧ card P = Suc k'} * Suc k'"
          by (subst card_bind_constant) simp+
        from this have "card ?subexpr1 = Stirling (card A) (Suc k') * Suc k'"
          using insert.hyps(3) by simp
        moreover have "finite ?subexpr1"
          using ‹finite {P. partition_on A P ∧ card P = Suc k'}›
          ‹∀X∈{P. partition_on A P ∧ card P = Suc k'}. finite (X ⤜ (λp. {insert (insert a p) (X - {p})}))›
          by (auto intro: finite_bind)
        ultimately show ?thesis by blast
      qed
      moreover have "finite ?subexpr2 ∧ card ?subexpr2 = Stirling (card A) k'"
      proof -
        from ‹finite A› have "finite {P. partition_on A P ∧ card P = k'}"
          by (simp add: finitely_many_partition_on)
        moreover have " inj_on (insert {a}) {P. partition_on A P ∧ card P = k'}"
          using injectivity_subexpr2[OF ‹a ∉ A›] by (simp add: inj_on_def)
        ultimately have "card ?subexpr2 = card {P. partition_on A P ∧ card P = k'}"
          by (simp add: card_bind_singleton)
        also have "… = Stirling (card A) k'"
          using insert.hyps(3) .
        finally have "card ?subexpr2 = Stirling (card A) k'" .
        moreover have "finite ?subexpr2"
          by (simp add: ‹finite {P. partition_on A P ∧ card P = k'}› finite_bind)
        ultimately show ?thesis by blast
      qed
      moreover have "?subexpr1 ∩ ?subexpr2 = {}"
      proof -
        have "∀P∈?subexpr1. {a} ∉ P"
          using insert.hyps(2) by (force elim!: partition_onE)
        moreover have "∀P∈?subexpr2. {a} ∈ P" by auto
        ultimately show "?subexpr1 ∩ ?subexpr2 = {}" by blast
      qed
      ultimately show ?thesis
        by (simp add: card_Un_disjoint)
    qed
    also have "… = Stirling (card (insert a A)) k"
      using insert(1, 2) ‹k = Suc k'› by simp
    finally show ?thesis .
  qed
qed

theorem card_partition_on_at_most_size:
  assumes "finite A"
  shows "card {P. partition_on A P ∧ card P ≤ k} = (∑j≤k. Stirling (card A) j)"
proof -
  have "card {P. partition_on A P ∧ card P ≤ k} = card (⋃j≤k. {P. partition_on A P ∧ card P = j})"
    by (rule arg_cong[where f="card"]) auto
  also have "… = (∑j≤k. card {P. partition_on A P ∧ card P = j})"
    by (subst card_UN_disjoint) (auto simp add: ‹finite A› finitely_many_partition_on)
  also have "(∑j≤k. card {P. partition_on A P ∧ card P = j}) = (∑j≤k. Stirling (card A) j)"
    using ‹finite A› by (simp add: card_partition_on)
  finally show ?thesis .
qed

theorem partition_on_size1:
  assumes "finite A"
  shows "{P. partition_on A P ∧ (∀X∈P. card X = 1)} = {(λa. {a}) ` A}"
proof
  show "{P. partition_on A P ∧ (∀X∈P. card X = 1)} ⊆ {(λa. {a}) ` A}"
  proof
    fix P
    assume P: "P ∈ {P. partition_on A P ∧ (∀X∈P. card X = 1)}"
    have "P = (λa. {a}) ` A"
    proof
      show "P ⊆ (λa. {a}) ` A"
      proof
        fix X
        assume "X ∈ P"
        from P this obtain x where "X = {x}"
           by (auto simp add: card_Suc_eq)
        from this ‹X ∈ P› have "x ∈ A"
          using P unfolding partition_on_def by blast
        from this ‹X = {x}› show "X ∈(λa. {a}) ` A" by auto
      qed
    next
      show "(λa. {a}) ` A ⊆ P"
      proof
        fix X
        assume "X ∈ (λa. {a}) ` A"
        from this obtain x where X: "X = {x}" "x ∈ A" by auto
        have "⋃P = A"
          using P unfolding partition_on_def by blast
        from this ‹x ∈ A› obtain X' where "x ∈ X'" and "X' ∈ P"
          using UnionE by blast
        from ‹X' ∈ P› have "card X' = 1"
          using P unfolding partition_on_def by auto
        from this ‹x ∈ X'› have "X' = {x}"
          using card_1_singletonE by blast
        from this X(1) ‹X' ∈ P› show "X ∈ P" by auto
      qed
    qed
    from this show "P ∈ {(λa. {a}) ` A}" by auto
  qed
next
  show "{(λa. {a}) ` A} ⊆ {P. partition_on A P ∧ (∀X∈P. card X = 1)}"
  proof
    fix P
    assume "P ∈ {(λa. {a}) ` A}"
    from this have P: "P = (λa. {a}) ` A" by auto
    from this have "partition_on A P" by (auto intro: partition_onI)
    from P this show "P ∈ {P. partition_on A P ∧ (∀X∈P. card X = 1)}" by auto
  qed
qed

theorem card_partition_on_size1:
  assumes "finite A"
  shows "card {P. partition_on A P ∧ (∀X∈P. card X = 1)} = 1"
using assms partition_on_size1 by fastforce

lemma card_partition_on_size1_eq_1:
  assumes "finite A"
  assumes "card A ≤ k"
  shows "card {P. partition_on A P ∧ card P ≤ k ∧ (∀X∈P. card X = 1)} = 1"
proof -
  {
    fix P
    assume "partition_on A P" "∀X∈P. card X = 1"
    from this have "P ∈ {P. partition_on A P ∧ (∀X∈P. card X = 1)}" by simp
    from this have "P ∈ {(λa. {a}) ` A}"
      using partition_on_size1 ‹finite A› by auto
    from this have "P = (λa. {a}) ` A" by auto
    moreover from this have "card P = card A"
      by (auto intro: card_image)
  }
  from this have "{P. partition_on A P ∧ card P ≤ k ∧ (∀X∈P. card X = 1)} = {P. partition_on A P ∧ (∀X∈P. card X = 1)}"
    using ‹card A ≤ k› by auto
  from this show ?thesis
    using ‹finite A› by (simp only: card_partition_on_size1)
qed

lemma card_partition_on_size1_eq_0:
  assumes "finite A"
  assumes "k < card A"
  shows "card {P. partition_on A P ∧ card P ≤ k ∧ (∀X∈P. card X = 1)} = 0"
proof -
  {
    fix P
    assume "partition_on A P" "∀X∈P. card X = 1"
    from this have "P ∈ {P. partition_on A P ∧ (∀X∈P. card X = 1)}" by simp
    from this have "P ∈ {(λa. {a}) ` A}"
      using partition_on_size1 ‹finite A› by auto
    from this have "P = (λa. {a}) ` A" by auto
    from this have "card P = card A"
      by (auto intro: card_image)
  }
  from this assms(2) have "{P. partition_on A P ∧ card P ≤ k ∧ (∀X∈P. card X = 1)} = {}"
    using Collect_empty_eq leD by fastforce
  from this show ?thesis by (simp only: card_empty)
qed

end