(* 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