(* Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *) section ‹Number Partitions› theory Number_Partition imports Additions_to_Main begin subsection ‹Number Partitions as @{typ "nat => nat"} Functions› definition partitions :: "(nat ⇒ nat) ⇒ nat ⇒ bool" (infix "partitions" 50) where "p partitions n = ((∀i. p i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n) ∧ (∑i≤n. p i * i) = n)" lemma partitionsI: assumes "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n" assumes "(∑i≤n. p i * i) = n" shows "p partitions n" using assms unfolding partitions_def by auto lemma partitionsE: assumes "p partitions n" obtains "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n" "(∑i≤n. p i * i) = n" using assms unfolding partitions_def by auto lemma partitions_zero: "p partitions 0 ⟷ p = (λi. 0)" unfolding partitions_def by auto lemma partitions_one: "p partitions (Suc 0) ⟷ p = (λi. 0)(1 := 1)" unfolding partitions_def by (auto split: if_split_asm) (auto simp add: fun_eq_iff) subsection ‹Bounds and Finiteness of Number Partitions› lemma partitions_imp_finite_elements: assumes "p partitions n" shows "finite {i. 0 < p i}" proof - from assms have "{i. 0 < p i} ⊆ {..n}" by (auto elim: partitionsE) from this show ?thesis using rev_finite_subset by blast qed lemma partitions_bounds: assumes "p partitions n" shows "p i ≤ n" proof - from assms have index_bounds: "(∀i. p i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n)" and sum: "(∑i≤n. p i * i) = n" unfolding partitions_def by auto show ?thesis proof (cases "1 ≤ i ∧ i ≤ n") case True from True have "{..n} = insert i {i'. i' ≤ n ∧ i' ≠ i}" by blast from sum[unfolded this] have "p i * i + (∑i∈{i'. i' ≤ n ∧ i' ≠ i}. p i * i) = n" by auto from this have "p i * i ≤ n" by linarith from this True show ?thesis using dual_order.trans by fastforce next case False from this index_bounds show ?thesis by fastforce qed qed lemma partitions_parts_bounded: assumes "p partitions n" shows "sum p {..n} ≤ n" proof - { fix i assume "i ≤ n" from assms have "p i ≤ p i * i" by (auto elim!: partitionsE) } from this have "sum p {..n} ≤ (∑i≤n. p i * i)" by (auto intro: sum_mono) also from assms have n: "(∑i≤n. p i * i) = n" by (auto elim!: partitionsE) finally show ?thesis . qed lemma finite_partitions: "finite {p. p partitions n}" proof - have "{p. p partitions n} ⊆ {f. (∀i. f i ≤ n) ∧ (∀i. n + 1 ≤ i ⟶ f i = 0)}" by (auto elim: partitions_bounds) (auto simp add: partitions_def) from this bound_domain_and_range_impl_finitely_many_functions[of n "n + 1"] show ?thesis by (simp add: finite_subset) qed lemma finite_partitions_k_parts: "finite {p. p partitions n ∧ sum p {..n} = k}" by (simp add: finite_partitions) lemma partitions_remaining_Max_part: assumes "p partitions n" assumes "0 < p k" shows "∀i. n - k < i ∧ i ≠ k ⟶ p i = 0" proof (clarify) fix i assume "n - k < i" "i ≠ k" show "p i = 0" proof (cases "i ≤ n") assume "i ≤ n" from assms have n: "(∑i≤n. p i * i) = n" and "k ≤ n" by (auto elim: partitionsE) have "(∑i≤n. p i * i) = p k * k + (∑i∈{..n}-{k}. p i * i)" using ‹k ≤ n› sum_atMost_remove_nat by blast also have "... = p i * i + p k * k + (∑i∈{..n}-{i, k}. p i * i)" using ‹i ≤ n› ‹i ≠ k› by (auto simp add: sum.remove[where x="i"]) (metis Diff_insert) finally have eq: "(∑i≤n. p i * i) = p i * i + p k * k + (∑i∈{..n} - {i, k}. p i * i)" . show "p i = 0" proof (rule ccontr) assume "p i ≠ 0" have upper_bound: "p i * i + p k * k ≤ n" using eq n by auto have lower_bound: "p i * i + p k * k > n" using ‹n - k < i› ‹0 < p k› ‹k ≤ n› ‹p i ≠ 0› mult_eq_if not_less by auto from upper_bound lower_bound show False by simp qed next assume "¬ (i ≤ n)" from this show "p i = 0" using assms(1) by (auto elim: partitionsE) qed qed subsection ‹Operations of Number Partitions› lemma partitions_remove1_bounds: assumes partitions: "p partitions n" assumes gr0: "0 < p k" assumes neq: "(p(k := p k - 1)) i ≠ 0" shows "1 ≤ i ∧ i ≤ n - k" proof from partitions neq show "1 ≤ i" by (auto elim!: partitionsE split: if_split_asm) next from partitions gr0 have n: "(∑i≤n. p i * i) = n" and "k ≤ n" by (auto elim: partitionsE) show "i ≤ n - k" proof cases assume "k ≤ n - k" from ‹k ≤ n - k› neq show ?thesis using partitions_remaining_Max_part[OF partitions gr0] not_le by force next assume "¬ k ≤ n - k" from this have "2 * k > n" by auto have "p k = 1" proof (rule ccontr) assume "p k ≠ 1" with gr0 have "p k ≥ 2" by auto from this have "p k * k ≥ 2 * k" by simp with ‹2 * k > n› have "p k * k > n" by linarith from ‹k ≤ n› this have "(∑i≤n. p i * i) > n" by (simp add: sum_atMost_remove_nat[of k]) from this n show "False" by auto qed from neq this show ?thesis using partitions_remaining_Max_part[OF partitions gr0] leI by (auto split: if_split_asm) force qed qed lemma partitions_remove1: assumes partitions: "p partitions n" assumes gr0: "0 < p k" shows "p(k := p k - 1) partitions (n - k)" proof (rule partitionsI) fix i assume "(p(k := p k - 1)) i ≠ 0" from this show "1 ≤ i ∧ i ≤ n - k" using partitions_remove1_bounds partitions gr0 by blast next from partitions gr0 have "k ≤ n" by (auto elim: partitionsE) have "(∑i≤n - k. (p(k := p k - 1)) i * i) = (∑i≤n. (p(k := p k - 1)) i * i)" using partitions_remove1_bounds partitions gr0 by (auto intro!: sum.mono_neutral_left) also have "... = (p k - 1) * k + (∑i∈{..n} - {k}. (p(k := p k - 1)) i * i)" using ‹k ≤ n› by (simp add: sum_atMost_remove_nat[where k="k"]) also have "... = p k * k + (∑i∈{..n} - {k}. p i * i) - k" using gr0 by (simp add: diff_mult_distrib) also have "... = (∑i≤n. p i * i) - k" using ‹k ≤ n› by (simp add: sum_atMost_remove_nat[of k]) also from partitions have "... = n - k" by (auto elim: partitionsE) finally show "(∑i≤n - k. (p(k := p k - 1)) i * i) = n - k" . qed lemma partitions_insert1: assumes p: "p partitions n" assumes "k > 0" shows "(p(k := p k + 1)) partitions (n + k)" proof (rule partitionsI) fix i assume "(p(k := p k + 1)) i ≠ 0" from p this ‹k > 0› show "1 ≤ i ∧ i ≤ n + k" by (auto elim!: partitionsE) next have "(∑i≤n + k. (p(k := p k + 1)) i * i) = p k * k + (∑i∈{..n + k} - {k}. p i * i) + k" by (simp add: sum_atMost_remove_nat[of k]) also have "... = p k * k + (∑i∈{..n} - {k}. p i * i) + k" using p by (auto intro!: sum.mono_neutral_right elim!: partitionsE) also have "... = (∑i≤n. p i * i) + k" using p by (cases "k ≤ n") (auto simp add: sum_atMost_remove_nat[of k] elim: partitionsE) also have "... = n + k" using p by (auto elim: partitionsE) finally show "(∑i≤n + k. (p(k := p k + 1)) i * i) = n + k" . qed lemma count_remove1: assumes "p partitions n" assumes "0 < p k" shows "(∑i≤n - k. (p(k := p k - 1)) i) = (∑i≤n. p i) - 1" proof - have "k ≤ n" using assms by (auto elim: partitionsE) have "(∑i≤n - k. (p(k := p k - 1)) i) = (∑i≤n. (p(k := p k - 1)) i)" using partitions_remove1_bounds assms by (auto intro!: sum.mono_neutral_left) also have "(∑i≤n. (p(k := p k - 1)) i) = p k + (∑i∈{..n} - {k}. p i) - 1" using ‹0 < p k› ‹k ≤ n› by (simp add: sum_atMost_remove_nat[of k]) also have "... = (∑i∈{..n}. p i) - 1" using ‹k ≤ n› by (simp add: sum_atMost_remove_nat[of k]) finally show ?thesis . qed lemma count_insert1: assumes "p partitions n" shows "sum (p(k := p k + 1)) {..n + k} = (∑i≤n. p i) + 1" proof - have "(∑i≤n + k. (p(k := p k + 1)) i) = p k + (∑i∈{..n + k} - {k}. p i) + 1" by (simp add: sum_atMost_remove_nat[of k]) also have "... = p k + (∑i∈{..n} - {k}. p i) + 1" using assms by (auto intro!: sum.mono_neutral_right elim!: partitionsE) also have "... = (∑i≤n. p i) + 1" using assms by (cases "k ≤ n") (auto simp add: sum_atMost_remove_nat[of k] elim: partitionsE) finally show ?thesis . qed lemma partitions_decrease1: assumes p: "p partitions m" assumes sum: "sum p {..m} = k" assumes "p 1 = 0" shows "(λi. p (i + 1)) partitions m - k" proof - from p have "p 0 = 0" by (auto elim!: partitionsE) { fix i assume neq: "p (i + 1) ≠ 0" from p this ‹p 1 = 0› have "1 ≤ i" by (fastforce elim!: partitionsE simp add: le_Suc_eq) moreover have "i ≤ m - k" proof (rule ccontr) assume i_greater: "¬ i ≤ m - k" from p have s: "(∑i≤m. p i * i) = m" by (auto elim!: partitionsE) from p sum have "k ≤ m" using partitions_parts_bounded by fastforce from neq p have "i + 1 ≤ m" by (auto elim!: partitionsE) from i_greater have "i > m - k" by simp have ineq1: "i + 1 > (m - k) + 1" using i_greater by simp have ineq21: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j) ≥ (∑j≤m. (p(i + 1 := p (i + 1) - 1)) j)" using ‹p 0 = 0› not_less by (fastforce intro!: sum_mono) have ineq22a: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j) = (∑j≤m. p j) - 1" using ‹i + 1 ≤ m› neq by (simp add: sum.remove[where x="i + 1"]) have ineq22: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j) ≥ k - 1" using sum neq ineq22a by auto have ineq2: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j) ≥ k - 1" using ineq21 ineq22 by auto have "(∑i≤m. p i * i) = p (i + 1) * (i + 1) + (∑i∈{..m} - {i + 1}. p i * i)" using ‹i + 1 ≤ m› neq by (subst sum.remove[where x="i + 1"]) auto also have "... = (i + 1) + (∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j)" using ‹i + 1 ≤ m› neq by (subst sum.remove[where x="i + 1" and g="λj. (p(i + 1 := p (i + 1) - 1)) j * j"]) (auto simp add: mult_eq_if) finally have "(∑i≤m. p i * i) = i + 1 + (∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j)" . moreover have "... > m" using ineq1 ineq2 ‹k ≤ m› ‹p (i + 1) ≠ 0› by linarith ultimately have "(∑i≤m. p i * i) > m" by simp from s this show False by simp qed ultimately have "1 ≤ i ∧ i ≤ m - k" .. } note bounds = this show "(λi. p (i + 1)) partitions m - k" proof (rule partitionsI) fix i assume "p (i + 1) ≠ 0" from bounds this show "1 ≤ i ∧ i ≤ m - k" . next have geq: "∀i. p i * i ≥ p i" using ‹p 0 = 0› not_less by fastforce have "(∑i≤m - k. p (i + 1) * i) = (∑i≤m. p (i + 1) * i)" using bounds by (auto intro: sum.mono_neutral_left) also have "... = (∑i∈Suc ` {..m}. p i * (i - 1))" by (auto simp add: sum.reindex) also have "... = (∑i≤Suc m. p i * (i - 1))" using ‹p 0 = 0› by (simp add: atMost_Suc_eq_insert_0) also have "... = (∑i≤m. p i * (i - 1))" using p by (auto elim!: partitionsE) also have "... = (∑i≤m. p i * i - p i)" by (simp add: diff_mult_distrib2) also have "... = (∑i≤m. p i * i) - (∑i≤m. p i)" using geq by (simp only: sum_subtractf_nat) also have "... = m - k" using sum p by (auto elim!: partitionsE) finally show "(∑i≤m - k. p (i + 1) * i) = m - k" . qed qed lemma partitions_increase1: assumes partitions: "p partitions m - k" assumes k: "sum p {..m - k} = k" shows "(λi. p (i - 1)) partitions m" proof (rule partitionsI) fix i assume "p (i - 1) ≠ 0" from partitions this k show "1 ≤ i ∧ i ≤ m" by (cases k) (auto elim!: partitionsE) next from k partitions have "k ≤ m" using linear partitions_zero by force have eq_0: "∀i>m - k. p i = 0" using partitions by (auto elim!: partitionsE) from partitions have s: "(∑i≤m - k. p i * i) = m - k" by (auto elim!: partitionsE) have "(∑i≤m. p (i - 1) * i) = (∑i≤Suc m. p (i - 1) * i)" using partitions k by (cases k) (auto elim!: partitionsE) also have "(∑i≤Suc m. p (i - 1) * i) = (∑i≤m. p i * (i + 1))" by (subst sum.atMost_Suc_shift) simp also have "... = (∑i≤m - k. p i * (i + 1))" using eq_0 by (auto intro: sum.mono_neutral_right) also have "... = (∑i≤m - k. p i * i) + (∑i≤m - k. p i)" by (simp add: sum.distrib) also have "... = m - k + k" using s k by simp also have "... = m" using ‹k ≤ m› by simp finally show "(∑i≤m. p (i - 1) * i) = m" . qed lemma count_decrease1: assumes p: "p partitions m" assumes sum: "sum p {..m} = k" assumes "p 1 = 0" shows "sum (λi. p (i + 1)) {..m - k} = k" proof - from p have "p 0 = 0" by (auto elim!: partitionsE) have "sum (λi. p (i + 1)) {..m - k} = sum (λi. p (i + 1)) {..m}" using partitions_decrease1[OF assms] by (auto intro: sum.mono_neutral_left elim!: partitionsE) also have "… = sum (λi. p (i + 1)) {0..m}" by (simp add: atLeast0AtMost) also have "… = sum (λi. p i) {Suc 0.. Suc m}" by (simp only: One_nat_def add_Suc_right add_0_right sum.shift_bounds_cl_Suc_ivl) also have "… = sum (λi. p i) {.. Suc m}" using ‹p 0 = 0› by (simp add: atLeast0AtMost sum_shift_lb_Suc0_0) also have "… = sum (λi. p i) {.. m}" using p by (auto elim!: partitionsE) also have "… = k" using sum by simp finally show ?thesis . qed lemma count_increase1: assumes partitions: "p partitions m - k" assumes k: "sum p {..m - k} = k" shows "(∑i≤m. p (i - 1)) = k" proof - have "p 0 = 0" using partitions by (auto elim!: partitionsE) have "(∑i≤m. p (i - 1)) = (∑i∈{1..m}. p (i - 1))" using ‹p 0 = 0› by (auto intro: sum.mono_neutral_cong_right) also have "(∑i∈{1..m}. p (i - 1)) = (∑i≤m - 1. p i)" proof (cases m) case 0 from this show ?thesis using ‹p 0 = 0› by simp next case (Suc m') { fix x assume "Suc 0 ≤ x" "x ≤ m" from this Suc have "x ∈ Suc ` {..m'}" by (auto intro!: image_eqI[where x="x - 1"]) } from this Suc show ?thesis by (intro sum.reindex_cong[of Suc]) auto qed also have "(∑i≤m - 1. p i) = (∑i≤m. p i)" proof - { fix i assume "0 < p i" "i ≤ m" from assms this have "i ≤ m - 1" using ‹p 0 = 0› partitions_increase1 by (cases k) (auto elim!: partitionsE) } from this show ?thesis by (auto intro: sum.mono_neutral_cong_left) qed also have "... = (∑i≤m - k. p i)" using partitions by (auto intro: sum.mono_neutral_right elim!: partitionsE) also have "... = k" using k by auto finally show ?thesis . qed subsection ‹Number Partitions as Multisets on Natural Numbers› definition number_partition :: "nat ⇒ nat multiset ⇒ bool" where "number_partition n N = (sum_mset N = n ∧ 0 ∉# N)" subsubsection ‹Relationship to Definition on Functions› lemma count_partitions_iff: "count N partitions n ⟷ number_partition n N" proof assume "count N partitions n" from this have "(∀i. count N i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n)" "(∑i≤n. count N i * i) = n" unfolding Number_Partition.partitions_def by auto moreover from this have "set_mset N ⊆ {..n}" by auto moreover have "finite {..n}" by auto ultimately have "sum_mset N = n" using sum_mset_sum_count sum_mset_eq_sum_on_supersets by presburger moreover have "0 ∉# N" using ‹∀i. count N i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n› by auto ultimately show "number_partition n N" unfolding number_partition_def by auto next assume "number_partition n N" from this have "sum_mset N = n" and "0 ∉# N" unfolding number_partition_def by auto { fix i assume "count N i ≠ 0" have "1 ≤ i ∧ i ≤ n" proof from ‹0 ∉# N› ‹count N i ≠ 0› show "1 ≤ i" using Suc_le_eq by auto from ‹sum_mset N = n› ‹count N i ≠ 0› show "i ≤ n" using multi_member_split by fastforce qed } moreover from ‹sum_mset N = n› have "(∑i≤n. count N i * i) = n" by (metis atMost_iff calculation finite_atMost not_in_iff subsetI sum_mset_eq_sum_on_supersets sum_mset_sum_count) ultimately show "count N partitions n" by (rule partitionsI) auto qed lemma partitions_iff_Abs_multiset: "p partitions n ⟷ finite {x. 0 < p x} ∧ number_partition n (Abs_multiset p)" proof assume "p partitions n" from this have bounds: "(∀i. p i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n)" and sum: "(∑i≤n. p i * i) = n" unfolding partitions_def by auto from ‹p partitions n› have "finite {x. 0 < p x}" by (rule partitions_imp_finite_elements) moreover from ‹finite {x. 0 < p x}› bounds have "¬ 0 ∈# Abs_multiset p" using count_eq_zero_iff by force moreover from ‹finite {x. 0 < p x}› this sum have "sum_mset (Abs_multiset p) = n" proof - have "(∑i∈{x. 0 < p x}. p i * i) = (∑i≤n. p i * i)" using bounds by (auto intro: sum.mono_neutral_cong_left) from ‹finite {x. 0 < p x}› this sum show "sum_mset (Abs_multiset p) = n" by (simp add: sum_mset_sum_count set_mset_Abs_multiset) qed ultimately show "finite {x. 0 < p x} ∧ number_partition n (Abs_multiset p)" unfolding number_partition_def by auto next assume "finite {x. 0 < p x} ∧ number_partition n (Abs_multiset p)" from this have "finite {x. 0 < p x}" "0 ∉# Abs_multiset p" "sum_mset (Abs_multiset p) = n" unfolding number_partition_def by auto from ‹finite {x. 0 < p x}› have "(∑i∈{x. 0 < p x}. p i * i) = n" using ‹ sum_mset (Abs_multiset p) = n› by (simp add: sum_mset_sum_count set_mset_Abs_multiset) have bounds: "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n" proof fix i assume "p i ≠ 0" from ‹¬ 0 ∈# Abs_multiset p› ‹finite {x. 0 < p x}› have "p 0 = 0" using count_inI by force from this ‹p i ≠ 0› show "1 ≤ i" by (metis One_nat_def leI less_Suc0) show "i ≤ n" proof (rule ccontr) assume "¬ i ≤ n" from this have "i > n" using le_less_linear by blast from this ‹p i ≠ 0› have "p i * i > n" by (auto simp add: less_le_trans) from ‹p i ≠ 0› have "(∑i∈{x. 0 < p x}. p i * i) = p i * i + (∑i∈{x. 0 < p x} - {i}. p i * i)" using ‹finite {x. 0 < p x}› by (subst sum.insert_remove[symmetric]) (auto simp add: insert_absorb) also from ‹p i * i > n› have "… > n" by auto finally show False using ‹(∑i∈{x. 0 < p x}. p i * i) = n› by blast qed qed moreover have "(∑i≤n. p i * i) = n" proof - have "(∑i≤n. p i * i) = (∑i∈{x. 0 < p x}. p i * i)" using bounds by (auto intro: sum.mono_neutral_cong_right) from this show ?thesis using ‹(∑i∈{x. 0 < p x}. p i * i) = n› by simp qed ultimately show "p partitions n" by (auto intro: partitionsI) qed lemma size_nat_multiset_eq: fixes N :: "nat multiset" assumes "number_partition n N" shows "size N = sum (count N) {..n}" proof - have "set_mset N ⊆ {..sum_mset N}" by (auto dest: multi_member_split) have "size N = sum (count N) (set_mset N)" by (rule size_multiset_overloaded_eq) also have "… = sum (count N) {..sum_mset N}" using ‹set_mset N ⊆ {..sum_mset N}› by (auto intro: sum.mono_neutral_cong_left count_inI) finally show ?thesis using ‹number_partition n N› unfolding number_partition_def by auto qed end