# Theory Euler_Partition

```(* Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
Dedicated to Sandra H. for a wonderful relaxing summer
*)

section ‹Euler's Partition Theorem›

theory Euler_Partition
imports
Main
Card_Number_Partitions.Number_Partition
begin

subsection ‹Preliminaries›

lemma power_div_nat:
assumes "c ≤ b"
assumes "a > 0"
shows  "(a :: nat) ^ b div a ^ c = a ^ (b - c)"

lemma sum_div:
assumes "finite A"
assumes "⋀a. a ∈ A ⟹ (b::'b::euclidean_semiring) dvd f a"
shows "(∑a∈A. f a) div b = (∑a∈A. (f a) div b)"
using assms
proof (induct)
case insert from this show ?case by auto (subst div_add; auto intro!: dvd_sum)
qed (auto)

lemma sum_mod:
assumes "finite A"
assumes "⋀a. a ∈ A ⟹ f a mod b = (0::'b::unique_euclidean_semiring)"
shows "(∑a∈A. f a) mod b = 0"

lemma finite_exponents:
"finite {i. 2 ^ i ≤ (n::nat)}"
proof -
have "{i::nat. 2 ^ i ≤ n} ⊆ {0..n}"
using dual_order.trans by fastforce
from finite_subset[OF this] show ?thesis by simp
qed

subsection ‹Binary Encoding of Natural Numbers›

definition bitset :: "nat ⇒ nat set"
where
"bitset n = {i. odd (n div (2 ^ i))}"

lemma in_bitset_bound:
"b ∈ bitset n ⟹ 2 ^ b ≤ n"
unfolding bitset_def using not_less by fastforce

lemma in_bitset_bound_weak:
"b ∈ bitset n ⟹ b ≤ n"
by (meson order.trans in_bitset_bound self_le_ge2_pow[OF order_refl])

lemma finite_bitset:
"finite (bitset n)"
proof -
have "bitset n ⊆ {..n}" by (auto dest: in_bitset_bound_weak)
from this show ?thesis using finite_subset by auto
qed

lemma bitset_0:
"bitset 0 = {}"
unfolding bitset_def by auto

lemma bitset_2n: "bitset (2 * n) = Suc ` (bitset n)"
proof (rule set_eqI)
fix x
show "(x ∈ bitset (2 * n)) = (x ∈ Suc ` bitset n)"
unfolding bitset_def by (cases x) auto
qed

lemma bitset_Suc:
assumes "even n"
shows "bitset (n + 1) = insert 0 (bitset n)"
proof (rule set_eqI)
fix x
from assms show "(x ∈ bitset (n + 1)) = (x ∈ insert 0 (bitset n))"
unfolding bitset_def by (cases x) (auto simp add: Divides.div_mult2_eq)
qed

lemma bitset_2n1:
"bitset (2 * n + 1) = insert 0 (Suc ` (bitset n))"
by (subst bitset_Suc) (auto simp add: bitset_2n)

lemma sum_bitset:
"(∑i∈bitset n. 2 ^ i) = n"
proof (induct rule: nat_bit_induct)
case zero
show ?case by (auto simp add: bitset_0)
next
case (even n)
from this show ?case
by (simp add: bitset_2n sum.reindex sum_distrib_left[symmetric])
next
case (odd n)
have "(∑i∈bitset (2 * n + 1). 2 ^ i) = (∑i∈insert 0 (Suc ` bitset n). 2 ^ i)"
by (simp only: bitset_2n1)
also have "... = 2 ^ 0 + (∑i∈Suc ` bitset n. 2 ^ i)"
by (subst sum.insert) (auto simp add: finite_bitset)
also have "... = 2 * n + 1"
using odd by (simp add: sum.reindex sum_distrib_left[symmetric])
finally show ?case by simp
qed

lemma binarysum_div:
assumes "finite B"
shows "(∑i∈B. (2::nat) ^ i) div 2 ^ j = (∑i∈B. if i < j then 0 else 2 ^ (i - j))"
(is "_ = (∑i∈_. ?f i)")
proof -
have split_B: "B = {i∈B. i < j} ∪ {i∈B. j ≤ i}" by auto
have bound: "(∑i | i ∈ B ∧ i < j. (2::nat) ^ i) < 2 ^ j"
proof (rule order.strict_trans1)
show "(∑i | i ∈ B ∧ i < j. (2::nat) ^ i) ≤ (∑i<j. 2 ^ i)" by (auto intro: sum_mono2)
show "... < 2 ^ j" using sum_power2 by (simp add: atLeast0LessThan)
qed
from this have zero: "(∑i | i ∈ B ∧ i < j. (2::nat) ^ i) div (2 ^ j) = 0" by (elim div_less)
from assms have mod0: "(∑i | i ∈ B ∧ j ≤ i. (2::nat) ^ i) mod 2 ^ j = 0"
by (auto intro!: sum_mod simp add: le_imp_power_dvd)
from assms have "(∑i∈B. (2::nat) ^ i) div (2 ^ j) = ((∑i | i ∈ B ∧ i < j. 2 ^ i) + (∑i | i ∈ B ∧ j ≤ i. 2 ^ i)) div 2 ^ j"
by (subst sum.union_disjoint[symmetric]) (auto simp add: split_B[symmetric])
also have "... = (∑i | i ∈ B ∧ j ≤ i. 2 ^ i) div 2 ^ j"
also have "... = (∑i | i ∈ B ∧ j ≤ i. 2 ^ i div 2 ^ j)"
using assms by (subst sum_div) (auto simp add: sum_div le_imp_power_dvd)
also have "... = (∑i | i ∈ B ∧ j ≤ i. 2 ^ (i - j))"
by (rule sum.cong[OF refl]) (auto simp add: power_div_nat)
also have "... = (∑i∈B. ?f i)"
using assms by (subst split_B; subst sum.union_disjoint) auto
finally show ?thesis .
qed

lemma odd_iff:
assumes "finite B"
shows "odd (∑i∈B. if i < x then (0::nat) else 2 ^ (i - x)) = (x ∈ B)" (is "odd (∑i∈_. ?s i) = _")
proof -
from assms have even: "even (∑i∈B - {x}. ?s i)"
by (subst dvd_sum) auto
show ?thesis
proof
assume "odd (∑i∈B. ?s i)"
from this even show "x ∈ B" by (cases "x ∈ B") auto
next
assume "x ∈ B"
from assms this have "(∑i∈B. ?s i) = 1 + (∑i∈B-{x}. ?s i)"
from assms this even show "odd (∑i∈B. ?s i)" by auto
qed
qed

lemma bitset_sum:
assumes "finite B"
shows "bitset (∑i∈B. 2 ^ i) = B"
using assms unfolding bitset_def by (simp add: binarysum_div odd_iff)

subsection ‹Decomposition of a Number into a Power of Two and an Odd Number›

function (sequential) index :: "nat ⇒ nat"
where
"index 0 = 0"
| "index n = (if odd n then 0 else Suc (index (n div 2)))"
by (pat_completeness) auto

termination
proof
show "wf {(x::nat, y). x < y}" by (simp add: wf)
next
fix n show "(Suc n div 2, Suc n) ∈ {(x, y). x < y}" by simp
qed

function (sequential) oddpart :: "nat ⇒ nat"
where
"oddpart 0 = 0"
| "oddpart n = (if odd n then n else oddpart (n div 2))"
by pat_completeness auto

termination
proof
show "wf {(x::nat, y). x < y}" by (simp add: wf)
next
fix n show "(Suc n div 2, Suc n) ∈ {(x, y). x < y}" by simp
qed

lemma odd_oddpart:
"odd (oddpart n) ⟷ n ≠ 0"
by (induct n rule: index.induct) auto

lemma index_oddpart_decomposition:
"n = 2 ^ (index n) * oddpart n"
proof (induct n rule: index.induct)
case (2 n)
from this show "Suc n = 2 ^ index (Suc n) * oddpart (Suc n)"
qed (simp)

lemma oddpart_leq:
"oddpart n ≤ n"
by (induct n rule: index.induct) (simp, metis div_le_dividend le_Suc_eq le_trans oddpart.simps(2))

lemma index_oddpart_unique:
assumes "odd (m :: nat)" "odd m'"
shows "(2 ^ i * m = 2 ^ i' * m') ⟷ (i = i' ∧ m = m')"
proof (induct i arbitrary: i')
case 0
from assms show ?case by auto
next
case (Suc _ i')
from assms this show ?case by (cases i') auto
qed

lemma index_oddpart:
assumes "odd m"
shows "index (2 ^ i * m) = i" "oddpart (2 ^ i * m) = m"
using index_oddpart_unique[where i=i and m=m and m'="oddpart (2 ^ i * m)" and i'="index (2 ^ i * m)"]
assms odd_oddpart index_oddpart_decomposition by force+

subsection ‹Partitions With Only Distinct and Only Odd Parts›

definition odd_of_distinct :: "(nat ⇒ nat) ⇒ nat ⇒ nat"
where
"odd_of_distinct p = (λi. if odd i then (∑j | p (2 ^ j * i) = 1. 2 ^ j) else 0)"

definition distinct_of_odd :: "(nat ⇒ nat) ⇒ nat ⇒ nat"
where
"distinct_of_odd p = (λi. if index i ∈ bitset (p (oddpart i)) then 1 else 0)"

lemma odd:
"odd_of_distinct p i ≠ 0 ⟹ odd i"
unfolding odd_of_distinct_def by auto

lemma distinct_distinct_of_odd:
"distinct_of_odd p i ≤ 1"
unfolding distinct_of_odd_def by auto

lemma odd_of_distinct:
assumes "odd_of_distinct p i ≠ 0"
assumes "⋀i. p i ≠ 0 ⟹ i ≤ n"
shows "1 ≤ i ∧ i ≤ n"
proof
from assms(1) odd have "odd i"
by simp
then show "1 ≤ i"
by (auto elim: oddE)
next
from assms(1) obtain j where "p (2 ^ j * i) > 0"
by (auto simp add: odd_of_distinct_def split: if_splits) fastforce
with assms(2) have "i ≤ 2 ^ j * i" "2 ^ j * i ≤ n"
by simp_all
then show "i ≤ n"
by (rule order_trans)
qed

lemma distinct_of_odd:
assumes "⋀i. p i * i ≤ n" "⋀i. p i ≠ 0 ⟹ odd i"
assumes "distinct_of_odd p i ≠ 0"
shows "1 ≤ i ∧ i ≤ n"
proof
from assms(3) have index: "index i ∈ bitset (p (oddpart i))"
unfolding distinct_of_odd_def by (auto split: if_split_asm)
have "i ≠ 0"
proof
assume zero: "i = 0"
from assms(2) have "p 0 = 0" by auto
from index zero this show "False" by (auto simp add: bitset_0)
qed
from this show "1 ≤ i" by auto
from assms(1) have leq_n: "p (oddpart i) * oddpart i ≤ n" by auto
from index have "2 ^ index i ≤ p (oddpart i)" by (rule in_bitset_bound)
from this leq_n show "i ≤ n"
by (subst index_oddpart_decomposition[of i]) (meson dual_order.trans eq_imp_le mult_le_mono)
qed

lemma odd_distinct:
assumes "⋀i. p i ≠ 0 ⟹ odd i"
shows "odd_of_distinct (distinct_of_odd p) = p"
using assms unfolding odd_of_distinct_def distinct_of_odd_def
by (auto simp add: fun_eq_iff index_oddpart sum_bitset)

lemma distinct_odd:
assumes "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n" "⋀i. p i ≤ 1"
shows "distinct_of_odd (odd_of_distinct p) = p"
proof -
from assms have "{i. p i = 1} ⊆ {..n}" by auto
from this have finite: "finite {i. p i = 1}" by (simp add: finite_subset)
have "⋀x j. x > 0 ⟹ p (2 ^ j * oddpart x) = 1 ⟹
index (2 ^ j * oddpart x) ∈ index ` {i. p i = 1 ∧ oddpart x = oddpart i}"
by (rule imageI) (auto intro: imageI simp add: index_oddpart odd_oddpart)
from this have eq: "⋀x. x > 0 ⟹ {j. p (2 ^ j * oddpart x) = 1} = index ` {i. p i = 1 ∧ oddpart x = oddpart i}"
by (auto simp add: index_oddpart odd_oddpart index_oddpart_decomposition[symmetric])
from finite have all_finite: "⋀x. x > 0 ⟹ finite {j. p (2 ^ j * oddpart x) = 1}"
unfolding eq by auto
show ?thesis
proof
fix x
from assms(1) have p0: "p 0 = 0" by auto
show "distinct_of_odd (odd_of_distinct p) x = p x"
proof (cases "x > 0")
case False
from this p0 show ?thesis
unfolding odd_of_distinct_def distinct_of_odd_def
by (auto simp add: odd_oddpart bitset_0)
next
case True
from p0 assms(2)[of x] all_finite[OF True] show ?thesis
unfolding odd_of_distinct_def distinct_of_odd_def
by (auto simp add: odd_oddpart bitset_0 bitset_sum index_oddpart_decomposition[symmetric])
qed
qed
qed

lemma sum_distinct_of_odd:
assumes "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n"
assumes "⋀i. p i * i ≤ n"
assumes "⋀i. p i ≠ 0 ⟹ odd i"
shows "(∑i≤n. distinct_of_odd p i * i) = (∑i≤n. p i * i)"
proof -
{
fix m
assume odd: "odd (m :: nat)"
have finite: "finite {k. 2 ^ k * m ≤ n ∧ k ∈ bitset (p m)}" by (simp add: finite_bitset)
have "(∑i | ∃k. i = 2 ^ k * m ∧ i ≤ n. distinct_of_odd p i * i) =
(∑i | ∃k. i = 2 ^ k * m ∧ i ≤ n. if index i ∈ bitset (p (oddpart i)) then i else 0)"
unfolding distinct_of_odd_def by (auto intro: sum.cong)
also have "... = (∑i | ∃k. i = 2 ^ k * m ∧ k ∈ bitset (p m) ∧ i ≤ n. i)"
using odd by (intro sum.mono_neutral_cong_right) (auto simp add: index_oddpart)
also have "... = (∑k | 2 ^ k * m ≤ n ∧ k ∈ bitset (p m). 2 ^ k * m)"
using odd by (auto intro!: sum.reindex_cong[OF _ _ refl] inj_onI)
also have "... = (∑k∈bitset (p m). 2 ^ k * m)"
using assms(2)[of m] finite dual_order.trans in_bitset_bound
by (fastforce intro!: sum.mono_neutral_cong_right)
also have "... = (∑k∈bitset (p m). 2 ^ k) * m"
by (subst sum_distrib_right) auto
also have "... = p m * m"
finally have "(∑i | ∃k. i = 2 ^ k * m ∧ i ≤ n. distinct_of_odd p i * i) = p m * m" .
} note inner_eq = this

have set_eq: "{i. 1 ≤ i ∧ i ≤ n} = ⋃((λm. {i. ∃k. i = (2 ^ k) * m ∧ i ≤ n}) ` {m. m ≤ n ∧ odd m})"
proof -
{
fix x
assume "1 ≤ x" "x ≤ n"
from this oddpart_leq[of x] have "oddpart x ≤ n ∧ odd (oddpart x) ∧ (∃k. 2 ^ index x * oddpart x = 2 ^ k * oddpart x)"
from this have "∃m≤n. odd m ∧ (∃k. x = 2 ^ k * m)"
}
from this show ?thesis by (auto simp add: Suc_leI odd_pos)
qed
let ?S = "(λm. {i. ∃k. i = 2 ^ k * m ∧ i ≤ n}) ` {m. m ≤ n ∧ odd m}"
have no_overlap: "∀A∈?S. ∀B∈?S. A ≠ B ⟶ A ∩ B = {}"
have inj: "inj_on (λm. {i. (∃k. i = 2 ^ k * m) ∧ i ≤ n}) {m. m ≤ n ∧ odd m}"
unfolding inj_on_def by auto (force simp add: index_oddpart_unique)
have reindex: "⋀F. (∑i | 1 ≤ i ∧ i ≤ n. F i) = (∑m | m ≤ n ∧ odd m. (∑i | ∃k. i = 2 ^ k * m ∧ i ≤ n. F i))"
unfolding set_eq by (subst sum.Union_disjoint) (auto simp add: no_overlap intro: sum.reindex_cong[OF inj])
have "(∑i≤n. distinct_of_odd p i * i) =  (∑i | 1 ≤ i ∧ i ≤ n. distinct_of_odd p i * i)"
by (auto intro: sum.mono_neutral_right)
also have "... = (∑m | m ≤ n ∧ odd m. ∑i | ∃k. i = 2 ^ k * m ∧ i ≤ n. distinct_of_odd p i * i)"
by (simp only: reindex)
also have "... = (∑i | i ≤ n ∧ odd i. p i * i)"
by (rule sum.cong[OF refl]; subst inner_eq) auto
also have "... = (∑i≤n. p i * i)"
using assms(3) by (auto intro: sum.mono_neutral_left)
finally show ?thesis .
qed

lemma leq_n:
assumes "∀i. 0 < p i ⟶ 1 ≤ i ∧ i ≤ (n::nat)"
assumes "(∑i≤n. p i * i) = n"
shows "p i * i ≤ n"
proof (rule ccontr)
assume "¬ p i * i ≤ n"
from this have gr_n: "p i * i > n" by auto
from this assms(1) have "1 ≤ i ∧ i ≤ n" by force
from this have "(∑j≤n. p j * j) = p i * i + (∑j | j ≤ n ∧ j ≠ i. p j * j)"
by (subst sum.insert[symmetric]) (auto intro: sum.cong simp del: sum.insert)
from this gr_n assms(2) show False by simp
qed

lemma distinct_of_odd_in_distinct_partitions:
assumes "p ∈ {p. p partitions n ∧ (∀i. p i ≠ 0 ⟶ odd i)}"
shows "distinct_of_odd p ∈ {p. p partitions n ∧ (∀i. p i ≤ 1)}"
proof
have "distinct_of_odd p partitions n"
proof (rule partitionsI)
fix i assume "distinct_of_odd p i ≠ 0"
from this assms show "1 ≤ i ∧ i ≤ n"
unfolding partitions_def
by (rule_tac distinct_of_odd) (auto simp add: leq_n)
next
from assms show "(∑i≤n. distinct_of_odd p i * i) = n"
by (subst  sum_distinct_of_odd) (auto simp add: distinct_distinct_of_odd leq_n elim: partitionsE)
qed
moreover have "∀i. distinct_of_odd p i ≤ 1"
by (intro allI distinct_distinct_of_odd)
ultimately show "distinct_of_odd p partitions n ∧ (∀i. distinct_of_odd p i ≤ 1)" by simp
qed

lemma odd_of_distinct_in_odd_partitions:
assumes "p ∈ {p. p partitions n ∧ (∀i. p i ≤ 1)}"
shows "odd_of_distinct p ∈ {p. p partitions n ∧ (∀i. p i ≠ 0 ⟶ odd i)}"
proof
from assms have distinct: "⋀i. p i = 0 ∨ p i = 1"
using le_imp_less_Suc less_Suc_eq_0_disj by fastforce
from assms have set_eq: "{x. p x = 1} = {x ∈ {..n}. p x = 1}"
unfolding partitions_def by auto
from assms have sum: "(∑i≤n. p i * i) = n"
unfolding partitions_def by auto
{
fix i
assume i: "odd (i :: nat)"
have 3: "inj_on index {x. p x = 1 ∧ oddpart x = i}"
unfolding inj_on_def by auto (metis index_oddpart_decomposition)
{
fix j assume "p (2 ^ j * i) = 1"
from this i have "j ∈ index ` {x. p x = 1 ∧ oddpart x = i}"
by (auto simp add: index_oddpart(1, 2) intro!: image_eqI[where x="2 ^ j * i"])
}
from i this have "{j. p (2 ^ j * i) = 1} = index ` {x. p x = 1 ∧ oddpart x = i}"
from 3 this have "(∑j | p (2 ^ j * i) = 1. 2 ^ j) * i = (∑x | p x = 1 ∧ oddpart x = i. 2 ^ index x) * i"
by (auto intro: sum.reindex_cong[where l = "index"])
also have "... = (∑x | p x = 1 ∧ oddpart x = i. 2 ^ index x * oddpart x)"
also have "... = (∑x | p x = 1 ∧ oddpart x = i. x)"
by (simp only: index_oddpart_decomposition[symmetric])
also have "... ≤ (∑x | p x = 1. x)"
using set_eq by (intro sum_mono2) auto
also have "... = (∑x≤n. p x * x)"
using distinct by (subst set_eq) (force intro!: sum.mono_neutral_cong_left)
also have "... = n" using sum .
finally have "(∑j | p (2 ^ j * i) = 1. 2 ^ j) * i ≤ n" .
}
from this have less_n: "⋀i. odd_of_distinct p i * i ≤ n"
unfolding odd_of_distinct_def by auto
have "odd_of_distinct p partitions n"
proof (rule partitionsI)
fix i assume "odd_of_distinct p i ≠ 0"
from this assms show "1 ≤ i ∧ i ≤ n"
by (elim CollectE conjE partitionsE odd_of_distinct) auto
next
have "(∑i≤n. odd_of_distinct p i * i) = (∑i≤n. distinct_of_odd (odd_of_distinct p) i * i)"
using assms less_n by (subst sum_distinct_of_odd) (auto elim!: partitionsE odd_of_distinct simp only: odd)
also have "... = (∑i≤n. p i * i)" using assms
by (auto elim!: partitionsE simp only:) (subst distinct_odd, auto)
also with assms have "... = n" by (auto elim: partitionsE)
finally show "(∑i≤n. odd_of_distinct p i * i) = n" .
qed
moreover have "∀i. odd_of_distinct p i ≠ 0 ⟶ odd i"
by (intro allI impI odd)
ultimately show "odd_of_distinct p partitions n ∧ (∀i. odd_of_distinct p i ≠ 0 ⟶ odd i)" by simp
qed

subsection ‹Euler's Partition Theorem›

theorem Euler_partition_theorem:
"card {p. p partitions n ∧ (∀i. p i ≤ 1)} = card {p. p partitions n ∧ (∀i. p i ≠ 0 ⟶ odd i)}"
(is "card ?distinct_partitions = card ?odd_partitions")
proof (rule card_bij_eq)
from odd_of_distinct_in_odd_partitions show
"odd_of_distinct ` ?distinct_partitions ⊆ ?odd_partitions" by auto
moreover from distinct_of_odd_in_distinct_partitions show
"distinct_of_odd ` ?odd_partitions ⊆ ?distinct_partitions" by auto
moreover have "∀p∈?distinct_partitions. distinct_of_odd (odd_of_distinct p) = p"
by auto (subst distinct_odd; auto simp add: partitions_def)
moreover have "∀p∈?odd_partitions. odd_of_distinct (distinct_of_odd p) = p"
by auto (subst odd_distinct; auto simp add: partitions_def)
ultimately show "inj_on odd_of_distinct ?distinct_partitions"
"inj_on distinct_of_odd ?odd_partitions"
by (intro bij_betw_imp_inj_on bij_betw_byWitness; auto)+
show "finite ?distinct_partitions" "finite ?odd_partitions"