# Theory Integer_Partitions

```section "Integer Paritions"

theory Integer_Partitions
imports
"HOL-Library.Multiset"
Common_Lemmas
Card_Number_Partitions.Card_Number_Partitions
begin

subsection"Definition"

definition integer_partitions :: "nat ⇒ nat multiset set" where
"integer_partitions i = {A. sum_mset A = i ∧ 0 ∉# A}"
text ‹Cardinality: ‹Partition i› (from ‹Card_Number_Partitions.Card_Number_Partitions› \cite{AFPnumpat})›
text "Example: ‹integer_partitions 4 = {{4}, {3,1}, {2,2} {2,1,1}, {1,1,1,1}}›"

subsection"Algorithm"

fun integer_partitions_enum_aux :: "nat ⇒ nat ⇒ nat list list" where
"integer_partitions_enum_aux 0 m = [[]]"
| "integer_partitions_enum_aux n m =
[h#r . h ← [1..< Suc (min n m)], r ← integer_partitions_enum_aux (n-h) h]"

fun integer_partitions_enum :: "nat ⇒ nat list list" where
"integer_partitions_enum n = integer_partitions_enum_aux n n"

subsection"Verification"

subsubsection"Correctness"

lemma integer_partitions_empty: "[] ∈ set (integer_partitions_enum_aux n m) ⟹ n = 0"
by(induct n) auto

lemma integer_partitions_enum_aux_first:
"x # xs ∈ set (integer_partitions_enum_aux n m)
⟹ xs ∈ set (integer_partitions_enum_aux (n-x) x)"
by(induct n) auto

lemma integer_partitions_enum_aux_max_n:
"x#xs ∈ set (integer_partitions_enum_aux n m) ⟹ x ≤ n"
by (induct n) auto

"x#xs ∈ set (integer_partitions_enum_aux n m) ⟹ x ≤ m"
by (induct n) auto

(*not used, but nice to have nonetheless*)
lemma integer_partitions_enum_aux_max:
"xs ∈ set (integer_partitions_enum_aux n m) ⟹ x ∈ set xs ⟹ x ≤ m"
proof(induct xs arbitrary: n m x)
case Nil
then show ?case using integer_partitions_enum_aux_max_head by simp
next
case (Cons y xs)
then show ?case
by fastforce
qed

lemma integer_partitions_enum_aux_sum:
"xs ∈ set (integer_partitions_enum_aux n m) ⟹ sum_list xs = n"
proof(induct xs arbitrary: n m)
case Nil
then show ?case using integer_partitions_empty by simp
next
case (Cons x xs)
then have "⟦xs ∈ set (integer_partitions_enum_aux (n-x) x)⟧ ⟹ sum_list xs = (n-x)"
by simp
moreover have "xs ∈ set (integer_partitions_enum_aux (n-x) x)"
using Cons integer_partitions_enum_aux_first by simp
moreover have "x ≤ n"
using Cons integer_partitions_enum_aux_max_n by simp
ultimately show ?case
by simp
qed

lemma integer_partitions_enum_aux_not_null_aux:
"x#xs ∈ set (integer_partitions_enum_aux n m) ⟹ x ≠ 0"
by (induct n) auto

lemma integer_partitions_enum_aux_not_null:
"xs ∈ set (integer_partitions_enum_aux n m) ⟹ x ∈ set xs ⟹ x ≠ 0"
proof(induct xs arbitrary: x n m)
case Nil
then show ?case by simp
next
case (Cons y xs)
show ?case proof(cases "y = x")
case True
then show ?thesis
using Cons integer_partitions_enum_aux_not_null_aux by simp
next
case False
then show ?thesis
using Cons integer_partitions_enum_aux_not_null_aux integer_partitions_enum_aux_first
by fastforce
qed
qed

"h ≤ m ⟹ h > 0 ⟹ n ≥ h ⟹
ys ∈ set (integer_partitions_enum_aux (n-h) h)⟹ h#ys ∈ set (integer_partitions_enum_aux n m)"
proof(induct n)
case 0
then show ?case by simp
next
case (Suc n)
then have 1: "1 ≤ m" by simp

have 2: "(∃x. (x = min (Suc n) m ∨ Suc 0 ≤ x ∧ x < Suc n ∧ x < m) ∧ h # ys
∈ (#) x ` set (integer_partitions_enum_aux (Suc n - x) x))"
unfolding image_def using Suc by auto

from 1 2 have "Suc 0 ≤ m ∧(∃x. (x = min (Suc n) m ∨ Suc 0 ≤ x ∧ x < Suc n ∧ x < m)
∧ h # ys ∈ (#) x ` set (integer_partitions_enum_aux (Suc n - x) x))"
by simp

then show ?case by auto
qed

"h ≤ m ⟹ h > 0 ⟹ ys ∈ set (integer_partitions_enum_aux n h)
⟹ h#ys ∈ set (integer_partitions_enum_aux (h + n) m)"

lemma integer_partitions_enum_correct_aux1:
assumes "0 ∉# A "
and "∀x ∈# A. x ≤ m"
shows" ∃xs∈set (integer_partitions_enum_aux (∑⇩# A) m). A = mset xs"
using assms proof(induct A arbitrary: m rule: multiset_induct_max)
case empty
then show ?case by simp
next
have hc1: "h ≤ m"

have hc2: "h > 0"

obtain ys where o1: "ys ∈ set (integer_partitions_enum_aux (∑⇩# A) h)" and o2: " A = mset ys"

have "h#ys ∈ set (integer_partitions_enum_aux (h + ∑⇩# A) m)"
using integer_partitions_enum_aux_head_plus hc1 o1 hc2 by blast

then show ?case
using o2 by force
qed

theorem integer_partitions_enum_correct:
"set (map mset (integer_partitions_enum n)) = integer_partitions n"
proof(standard)
have "⟦xs ∈ set (integer_partitions_enum_aux n n)⟧ ⟹ ∑⇩# (mset xs) = n" for xs
moreover have "xs ∈ set (integer_partitions_enum_aux n n) ⟹ 0 ∉# mset xs" for xs
using integer_partitions_enum_aux_not_null by auto
ultimately show "set (map mset (integer_partitions_enum n)) ⊆ integer_partitions n"
unfolding integer_partitions_def by auto
next
have "0 ∉# A ⟹ A ∈ mset ` set (integer_partitions_enum_aux (∑⇩# A) (∑⇩# A))" for A
unfolding image_def
using integer_partitions_enum_correct_aux1 by (simp add: sum_mset.remove)
then show "integer_partitions n ⊆ set (map mset (integer_partitions_enum n))"
unfolding integer_partitions_def by auto
qed

subsubsection"Distinctness"

lemma integer_partitions_enum_aux_distinct:
"distinct (integer_partitions_enum_aux n m)"
proof(induct n m rule:integer_partitions_enum_aux.induct)
case (1 m)
then show ?case by simp
next
case (2 n m)
have "distinct [h#r . h ← [1..< Suc (min (Suc n) m)], r ← integer_partitions_enum_aux ((Suc n)-h) h]"
apply(subst Cons_distinct_concat_map_function)
using 2 by auto
then show ?case by simp
qed

theorem integer_partitions_enum_distinct:
"distinct (integer_partitions_enum n)"
using integer_partitions_enum_aux_distinct by simp

subsubsection"Cardinality"

lemma partitions_bij_betw_count:
"bij_betw count {N. count N partitions n} {p. p partitions n}"
by (rule bij_betw_byWitness[where f'="Abs_multiset"]) (auto simp: partitions_imp_finite_elements)

lemma card_partitions_count_partitions:
"card {p. p partitions n} = card {N. count N partitions n}"
using bij_betw_same_card partitions_bij_betw_count by metis

text"this sadly is not proven in ‹Card_Number_Partitions.Card_Number_Partitions›"
lemma card_partitions_number_partition:
"card {p. p partitions n} = card {N. number_partition n N}"
using card_partitions_count_partitions count_partitions_iff by simp

lemma integer_partitions_number_partition_eq:
"integer_partitions n = {N. number_partition n N}"
using integer_partitions_def number_partition_def by auto

lemma integer_partitions_cardinality_aux:
"card (integer_partitions n) = (∑k≤n. Partition n k)"
using card_partitions_number_partition integer_partitions_number_partition_eq card_partitions
by simp

theorem integer_partitions_cardinality:
"card (integer_partitions n) = Partition (2*n) n"