Theory Card_Partitions

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

section ‹Cardinality of Set Partitions›

theory Card_Partitions
imports
  "HOL-Combinatorics.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} = (jk. Stirling (card A) j)"
proof -
  have "card {P. partition_on A P  card P  k} = card (jk. {P. partition_on A P  card P = j})"
    by (rule arg_cong[where f="card"]) auto
  also have " = (jk. 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 "(jk. card {P. partition_on A P  card P = j}) = (jk. 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  (XP. card X = 1)} = {(λa. {a}) ` A}"
proof
  show "{P. partition_on A P  (XP. card X = 1)}  {(λa. {a}) ` A}"
  proof
    fix P
    assume P: "P  {P. partition_on A P  (XP. 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  (XP. 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  (XP. card X = 1)}" by auto
  qed
qed

theorem card_partition_on_size1:
  assumes "finite A"
  shows "card {P. partition_on A P  (XP. 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  (XP. card X = 1)} = 1"
proof -
  {
    fix P
    assume "partition_on A P" "XP. card X = 1"
    from this have "P  {P. partition_on A P  (XP. 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  (XP. card X = 1)} = {P. partition_on A P  (XP. 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  (XP. card X = 1)} = 0"
proof -
  {
    fix P
    assume "partition_on A P" "XP. card X = 1"
    from this have "P  {P. partition_on A P  (XP. 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  (XP. card X = 1)} = {}"
    using Collect_empty_eq leD by fastforce
  from this show ?thesis by (simp only: card.empty)
qed

end