(* Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *) section ‹Cardinality of Number Partitions› theory Card_Number_Partitions imports Number_Partition begin subsection ‹The Partition Function› fun Partition :: "nat ⇒ nat ⇒ nat" where "Partition 0 0 = 1" | "Partition 0 (Suc k) = 0" | "Partition (Suc m) 0 = 0" | "Partition (Suc m) (Suc k) = Partition m k + Partition (m - k) (Suc k)" lemma Partition_less: assumes "m < k" shows "Partition m k = 0" using assms by (induct m k rule: Partition.induct) auto lemma Partition_sum_Partition_diff: assumes "k ≤ m" shows "Partition m k = (∑i≤k. Partition (m - k) i)" using assms by (induct m k rule: Partition.induct) auto lemma Partition_parts1: "Partition (Suc m) (Suc 0) = 1" by (induct m) auto lemma Partition_diag: "Partition (Suc m) (Suc m) = 1" by (induct m) auto lemma Partition_diag1: "Partition (Suc (Suc m)) (Suc m) = 1" by (induct m) auto lemma Partition_parts2: shows "Partition m 2 = m div 2" proof (induct m rule: nat_less_induct) fix m assume hypothesis: "∀n<m. Partition n 2 = n div 2" have "(m = 0 ∨ m = 1) ∨ m ≥ 2" by auto from this show "Partition m 2 = m div 2" proof assume "m = 0 ∨ m = 1" from this show ?thesis by (auto simp add: numerals(2)) next assume "2 ≤ m" from this obtain m' where m': "m = Suc (Suc m')" by (metis add_2_eq_Suc le_Suc_ex) from hypothesis this have "Partition m' 2 = m' div 2" by simp from this m' show ?thesis using Partition_parts1 Partition.simps(4)[of "Suc m'" "Suc 0"] div2_Suc_Suc by (simp add: numerals(2) del: Partition.simps) qed qed subsection ‹Cardinality of Number Partitions› lemma set_rewrite1: "{p. p partitions Suc m ∧ sum p {..Suc m} = Suc k ∧ p 1 ≠ 0} = (λp. p(1 := p 1 + 1)) ` {p. p partitions m ∧ sum p {..m} = k}" (is "?S = ?T") proof { fix p assume assms: "p partitions Suc m" "sum p {..Suc m} = Suc k" "0 < p 1" have "p(1 := p 1 - 1) partitions m" using assms by (metis partitions_remove1 diff_Suc_1) moreover have "(∑i≤m. (p(1 := p 1 - 1)) i) = k" using assms by (metis count_remove1 diff_Suc_1) ultimately have "p(1 := p 1 - 1) ∈ {p. p partitions m ∧ sum p {..m} = k}" by simp moreover have "p = p(1 := p 1 - 1, 1 := (p(1 := p 1 - 1)) 1 + 1)" using ‹0 < p 1› by auto ultimately have "p ∈ (λp. p(1 := p 1 + 1)) ` {p. p partitions m ∧ sum p {..m} = k}" by blast } from this show "?S ⊆ ?T" by blast next { fix p assume assms: "p partitions m" "sum p {..m} = k" have "(p(1 := p 1 + 1)) partitions Suc m" (is ?g1) using assms by (metis partitions_insert1 Suc_eq_plus1 zero_less_one) moreover have "sum (p(1 := p 1 + 1)) {..Suc m} = Suc k" (is ?g2) using assms by (metis count_insert1 Suc_eq_plus1) moreover have "(p(1 := p 1 + 1)) 1 ≠ 0" (is ?g3) by auto ultimately have "?g1 ∧ ?g2 ∧ ?g3" by simp } from this show "?T ⊆ ?S" by auto qed lemma set_rewrite2: "{p. p partitions m ∧ sum p {..m} = k ∧ p 1 = 0} = (λp. (λi. p (i - 1))) ` {p. p partitions (m - k) ∧ sum p {..m - k} = k}" (is "?S = ?T") proof { fix p assume assms: "p partitions m" "sum p {..m} = k" "p 1 = 0" have "(λi. p (i + 1)) partitions m - k" using assms partitions_decrease1 by blast moreover from assms have "sum (λi. p (i + 1)) {..m - k} = k" using assms count_decrease1 by blast ultimately have "(λi. p (i + 1)) ∈ {p. p partitions m - k ∧ sum p {..m - k} = k}" by simp moreover have "p = (λi. p ((i - 1) + 1))" proof (rule ext) fix i show "p i = p (i - 1 + 1)" using assms by (cases i) (auto elim!: partitionsE) qed ultimately have "p ∈ (λp. (λi. p (i - 1))) ` {p. p partitions m - k ∧ sum p {..m - k} = k}" by auto } from this show "?S ⊆ ?T" by auto next { fix p assume assms: "p partitions m - k" "sum p {..m - k} = k" from assms have "(λi. p (i - 1)) partitions m" (is ?g1) using partitions_increase1 by blast moreover from assms have "(∑i≤m. p (i - 1)) = k" (is ?g2) using count_increase1 by blast moreover from assms have "p 0 = 0" (is ?g3) by (auto elim!: partitionsE) ultimately have "?g1 ∧ ?g2 ∧ ?g3" by simp } from this show "?T ⊆ ?S" by auto qed theorem card_partitions_k_parts: "card {p. p partitions n ∧ (∑i≤n. p i) = k} = Partition n k" proof (induct n k rule: Partition.induct) case 1 have eq: "{p. p = (λx. 0) ∧ p 0 = 0} = {(λx. 0)}" by auto show "card {p. p partitions 0 ∧ sum p {..0} = 0} = Partition 0 0" by (simp add: partitions_zero eq) next case (2 k) have eq: "{p. p = (λx. 0) ∧ p 0 = Suc k} = {}" by auto show "card {p. p partitions 0 ∧ sum p {..0} = Suc k} = Partition 0 (Suc k)" by (simp add: partitions_zero eq) next case (3 m) have eq: "{p. p partitions Suc m ∧ sum p {..Suc m} = 0} = {}" by (fastforce elim!: partitionsE simp add: le_Suc_eq) from this show "card {p. p partitions Suc m ∧ sum p {..Suc m} = 0} = Partition (Suc m) 0" by (simp only: Partition.simps card.empty) next case (4 m k) let ?set1 = "{p. p partitions Suc m ∧ sum p {..Suc m} = Suc k ∧ p 1 ≠ 0}" let ?set2 = "{p. p partitions Suc m ∧ sum p {..Suc m} = Suc k ∧ p 1 = 0}" have "finite {p. p partitions Suc m}" by (simp add: finite_partitions) from this have finite_sets: "finite ?set1" "finite ?set2" by simp+ have set_eq: "{p. p partitions Suc m ∧ sum p {..Suc m} = Suc k} = ?set1 ∪ ?set2" by auto have disjoint: "?set1 ∩ ?set2 = {}" by auto have inj1: "inj_on (λp. p(1 := p 1 + 1)) {p. p partitions m ∧ sum p {..m} = k}" by (auto intro!: inj_onI) (metis diff_Suc_1 fun_upd_idem_iff fun_upd_upd) have inj2: "inj_on (λp i. p (i - 1)) {p. p partitions m - k ∧ sum p {..m - k} = Suc k}" by (auto intro!: inj_onI simp add: fun_eq_iff) (metis add_diff_cancel_right') have card1: "card ?set1 = Partition m k" using inj1 4(1) by (simp only: set_rewrite1 card_image) have card2: "card ?set2 = Partition (m - k) (Suc k)" using inj2 4(2) by (simp only: set_rewrite2 card_image diff_Suc_Suc) have "card {p. p partitions Suc m ∧ sum p {..Suc m} = Suc k} = Partition m k + Partition (m - k) (Suc k)" using finite_sets disjoint by (simp only: set_eq card_Un_disjoint card1 card2) from this show "card {p. p partitions Suc m ∧ sum p {..Suc m} = Suc k} = Partition (Suc m) (Suc k)" by auto qed theorem card_partitions: "card {p. p partitions n} = (∑k≤n. Partition n k)" proof - have seteq: "{p. p partitions n} = ⋃((λk. {p. p partitions n ∧ (∑i≤n. p i) = k}) ` {..n})" by (auto intro: partitions_parts_bounded) have finite: "⋀k. finite {p. p partitions n ∧ sum p {..n} = k}" by (simp add: finite_partitions) have "card {p. p partitions n} = card (⋃((λk. {p. p partitions n ∧ (∑i≤n. p i) = k}) ` {..n}))" using finite by (simp add: seteq) also have "... = (∑x≤n. card {p. p partitions n ∧ sum p {..n} = x})" using finite by (subst card_UN_disjoint) auto also have "... = (∑k≤n. Partition n k)" by (simp add: card_partitions_k_parts) finally show ?thesis . qed lemma card_partitions_atmost_k_parts: "card {p. p partitions n ∧ sum p {..n} ≤ k} = Partition (n + k) k" proof - have "card {p. p partitions n ∧ sum p {..n} ≤ k} = card (⋃((λk'. {p. p partitions n ∧ sum p {..n} = k'}) ` {..k}))" proof - have "{p. p partitions n ∧ sum p {..n} ≤ k} = (⋃k'≤k. {p. p partitions n ∧ sum p {..n} = k'})" by auto from this show ?thesis by simp qed also have "card (⋃((λk'. {p. p partitions n ∧ sum p {..n} = k'}) ` {..k})) = sum (λk'. card {p. p partitions n ∧ sum p {..n} = k'}) {..k}" using finite_partitions_k_parts by (subst card_UN_disjoint) auto also have "… = sum (λk'. Partition n k') {..k}" using card_partitions_k_parts by simp also have "… = Partition (n + k) k" using Partition_sum_Partition_diff by simp finally show ?thesis . qed subsection ‹Cardinality of Number Partitions as Multisets of Natural Numbers› lemma bij_betw_multiset_number_partition_with_size: "bij_betw count {N. number_partition n N ∧ size N = k} {p. p partitions n ∧ sum p {..n} = k}" proof (rule bij_betw_byWitness[where f'="Abs_multiset"]) show "∀N∈{N. number_partition n N ∧ size N = k}. Abs_multiset (count N) = N" using count_inverse by blast show "∀p∈{p. p partitions n ∧ sum p {..n} = k}. count (Abs_multiset p) = p" by (auto simp add: partitions_imp_finite_elements) show "count ` {N. number_partition n N ∧ size N = k} ⊆ {p. p partitions n ∧ sum p {..n} = k}" by (auto simp add: count_partitions_iff size_nat_multiset_eq) show "Abs_multiset ` {p. p partitions n ∧ sum p {..n} = k} ⊆ {N. number_partition n N ∧ size N = k}" using partitions_iff_Abs_multiset size_nat_multiset_eq by fastforce qed lemma bij_betw_multiset_number_partition_with_atmost_size: "bij_betw count {N. number_partition n N ∧ size N ≤ k} {p. p partitions n ∧ sum p {..n} ≤ k}" proof (rule bij_betw_byWitness[where f'="Abs_multiset"]) show "∀N∈{N. number_partition n N ∧ size N ≤ k}. Abs_multiset (count N) = N" using count_inverse by blast show "∀p∈{p. p partitions n ∧ sum p {..n} ≤ k}. count (Abs_multiset p) = p" by (auto simp add: partitions_imp_finite_elements) show "count ` {N. number_partition n N ∧ size N ≤ k} ⊆ {p. p partitions n ∧ sum p {..n} ≤ k}" by (auto simp add: count_partitions_iff size_nat_multiset_eq) show "Abs_multiset ` {p. p partitions n ∧ sum p {..n} ≤ k} ⊆ {N. number_partition n N∧ size N ≤ k}" using partitions_iff_Abs_multiset size_nat_multiset_eq by fastforce qed theorem card_number_partitions_with_atmost_k_parts: shows "card {N. number_partition n N ∧ size N ≤ x} = Partition (n + x) x" proof - have "bij_betw count {N. number_partition n N ∧ size N ≤ x} {p. p partitions n ∧ sum p {..n} ≤ x}" by (rule bij_betw_multiset_number_partition_with_atmost_size) from this have "card {N. number_partition n N ∧ size N ≤ x} = card {p. p partitions n ∧ sum p {..n} ≤ x}" by (rule bij_betw_same_card) also have "card {p. p partitions n ∧ sum p {..n} ≤ x} = Partition (n + x) x" by (rule card_partitions_atmost_k_parts) finally show ?thesis . qed theorem card_partitions_with_k_parts: "card {N. number_partition n N ∧ size N = k} = Partition n k" proof - have "bij_betw count {N. number_partition n N ∧ size N = k} {p. p partitions n ∧ sum p {..n} = k}" by (rule bij_betw_multiset_number_partition_with_size) from this have "card {N. number_partition n N ∧ size N = k} = card {p. p partitions n ∧ sum p {..n} = k}" by (rule bij_betw_same_card) also have "… = Partition n k" by (rule card_partitions_k_parts) finally show ?thesis . qed subsection ‹Cardinality of Number Partitions with only 1-parts› lemma number_partition1_eq_replicate_mset: "{N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition n N} = {replicate_mset n 1}" proof show "{N. (∀n. n ∈# N ⟶ n = 1) ∧ number_partition n N} ⊆ {replicate_mset n 1}" proof fix N assume N: "N ∈ {N. (∀n. n ∈# N ⟶ n = 1) ∧ number_partition n N}" have "N = replicate_mset n 1" proof (rule multiset_eqI) fix i have "count N 1 = sum_mset N" proof cases assume "N = {#}" from this show ?thesis by auto next assume "N ≠ {#}" from this N have "1 ∈# N" by blast from this N show ?thesis by (auto simp add: sum_mset_sum_count sum.remove[where x="1"] simp del: One_nat_def) qed from N this show "count N i = count (replicate_mset n 1) i" unfolding number_partition_def by (auto intro: count_inI) qed from this show "N ∈ {replicate_mset n 1}" by simp qed next show "{replicate_mset n 1} ⊆ {N. (∀n. n ∈# N ⟶ n = 1) ∧ number_partition n N}" unfolding number_partition_def by auto qed lemma card_number_partitions_with_only_parts_1_eq_1: assumes "n ≤ x" shows "card {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition n N ∧ size N ≤ x} = 1" (is "card ?N = _") proof - have "∀N ∈ {N. (∀n. n ∈# N ⟶ n = 1) ∧ number_partition n N}. size N = n" unfolding number_partition1_eq_replicate_mset by simp from this number_partition1_eq_replicate_mset ‹n ≤ x› have "?N = {replicate_mset n 1}" by auto from this show ?thesis by simp qed lemma card_number_partitions_with_only_parts_1_eq_0: assumes "x < n" shows "card {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition n N ∧ size N ≤ x} = 0" (is "card ?N = _") proof - have "∀N ∈ {N. (∀n. n ∈# N ⟶ n = 1) ∧ number_partition n N}. size N = n" unfolding number_partition1_eq_replicate_mset by simp from this number_partition1_eq_replicate_mset‹x < n› have "?N = {}" by auto from this show ?thesis by (simp only: card.empty) qed end