# Session Card_Number_Partitions

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

section ‹Additions to Isabelle's Main Theories›

imports "HOL-Library.Multiset"
begin

lemma bound_domain_and_range_impl_finitely_many_functions:
"finite {f::nat⇒nat. (∀i. f i ≤ n) ∧ (∀i≥m. f i = 0)}"
proof (induct m)
case 0
have eq: "{f. (∀i. f i ≤ n) ∧ (∀i. f i = 0)} = {(λ_. 0)}" by auto
from this show ?case by auto (subst eq; auto)
next
case (Suc m)
let ?S = "(λ(y, f). f(m := y))  ({0..n} × {f. (∀i. f i ≤ n) ∧ (∀i≥m. f i = 0)})"
{
fix g
assume "∀i. g i ≤ n" "∀i≥Suc m. g i = 0"
from this have "g ∈ ?S"
by (auto intro: image_eqI[where x="(g m, g(m:=0))"])
}
from this have "{f. (∀i. f i ≤ n) ∧ (∀i≥Suc m. f i = 0)} = ?S" by auto
from this Suc show ?case by simp
qed

lemma sum_atMost_remove_nat:
assumes "k ≤ (n :: nat)"
shows "(∑i≤n. f i) = f k + (∑i∈{..n}-{k}. f i)"
using assms by (auto simp add: sum.remove[where x=k])

lemma set_mset_Abs_multiset:
assumes "finite {x. f x > 0}"
shows "set_mset (Abs_multiset f) = {x. f x > 0}"
using assms unfolding set_mset_def by simp

lemma sum_mset_sum_count:
"sum_mset M = (∑i∈set_mset M. count M i * i)"
proof (induct M)
show "sum_mset {#} = (∑i∈set_mset {#}. count {#} i * i)" by simp
next
fix M x
assume hyp: "sum_mset M = (∑i∈set_mset M. count M i * i)"
show "sum_mset (add_mset x M) = (∑i∈set_mset (add_mset x M). count (add_mset x M) i * i)"
proof (cases "x ∈# M")
assume a: "¬ x ∈# M"
from this have "count M x = 0" by (meson count_inI)
from ‹¬ x ∈# M› this hyp show ?thesis
by (auto intro!: sum.cong)
next
assume "x ∈# M"
have "sum_mset (add_mset x M) = (∑i∈set_mset M. count M i * i) + x"
using hyp by simp
also have "… = (∑i∈set_mset M - {x}. count M i * i) + count M x * x + x"
using ‹x ∈# M› by (simp add: sum.remove[of _ x])
also have "… = count (add_mset x M) x * x + (∑i∈set_mset (add_mset x M) - {x}. count (add_mset x M) i * i)"
by simp
also have "… = (∑i∈set_mset (add_mset x M). count (add_mset x M) i * i)"
using ‹x ∈# M› by (simp add: sum.remove[of _ x])
finally show ?thesis .
qed
qed

lemma sum_mset_eq_sum_on_supersets:
assumes "finite A" "set_mset M ⊆ A"
shows "(∑i∈set_mset M. count M i * i) = (∑i∈A. count M i * i)"
proof -
note ‹finite A› ‹set_mset M ⊆ A›
moreover have "∀i∈A - set_mset M. count M i * i = 0"
using count_inI by fastforce
ultimately show ?thesis
by (auto intro: sum.mono_neutral_cong_left)
qed

end


# Theory Number_Partition

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

section ‹Number Partitions›

theory Number_Partition
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
qed

lemma finite_partitions_k_parts:
"finite {p. p partitions n ∧ sum p {..n} = k}"

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"
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"
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"
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"])
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))"
also have "... = (∑i≤Suc m. p i * (i - 1))"
using ‹p 0 = 0›
also have "... = (∑i≤m. p i * (i - 1))"
using p by (auto elim!: partitionsE)
also have "... = (∑i≤m. p i * i - p i)"
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}"
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"
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›
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"
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)"
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


# Theory Card_Number_Partitions

(*  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"
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)"
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}"
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}"
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}"
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)"
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"
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"
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
`