Theory Card_Partitions.Card_Partitions
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} = (∑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