Session Card_Number_Partitions

Theory Additions_to_Main

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

section ‹Additions to Isabelle's Main Theories›

theory Additions_to_Main
imports "HOL-Library.Multiset"
begin

subsection ‹Addition to Finite-Set Theory›

lemma bound_domain_and_range_impl_finitely_many_functions:
  "finite {f::natnat. (i. f i  n)  (im. 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)  (im. f i = 0)})"
  {
    fix g
    assume "i. g i  n" "iSuc 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)  (iSuc m. f i = 0)} = ?S" by auto
  from this Suc show ?case by simp
qed

subsection ‹Addition to Set-Interval Theory›

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

subsection ‹Additions to Multiset Theory›

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 = (iset_mset M. count M i * i)"
proof (induct M)
  show "sum_mset {#} = (iset_mset {#}. count {#} i * i)" by simp
next
  fix M x
  assume hyp: "sum_mset M = (iset_mset M. count M i * i)"
  show "sum_mset (add_mset x M) = (iset_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) = (iset_mset M. count M i * i) + x"
      using hyp by simp
    also have " = (iset_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 + (iset_mset (add_mset x M) - {x}. count (add_mset x M) i * i)"
      by simp
    also have " = (iset_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 "(iset_mset M. count M i * i) = (iA. count M i * i)"
proof -
  note ‹finite A ‹set_mset M  A
  moreover have "iA - 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
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)  (in. p i * i) = n)"

lemma partitionsI:
  assumes "i. p i  0  1  i  i  n"
  assumes "(in. 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" "(in. 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: "(in. 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}  (in. p i * i)"
    by (auto intro: sum_mono)
  also from assms have n: "(in. 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: "(in. p i * i) = n" and "k  n"
      by (auto elim: partitionsE)
    have "(in. 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: "(in. 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: "(in. 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 "(in. 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 "(in - k. (p(k := p k - 1)) i * i) = (in. (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 "... = (in. 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 "(in - 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 "(in + 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 "... = (in. 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 "(in + k. (p(k := p k + 1)) i * i) = n + k" .
qed

lemma count_remove1:
  assumes "p partitions n"
  assumes "0 < p k"
  shows "(in - k. (p(k := p k - 1)) i) = (in. p i) - 1"
proof -
  have "k  n" using assms by (auto elim: partitionsE)
  have "(in - k. (p(k := p k - 1)) i) = (in. (p(k := p k - 1)) i)"
    using partitions_remove1_bounds assms by (auto intro!: sum.mono_neutral_left)
  also have "(in. (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} = (in. p i) + 1"
proof -
  have "(in + 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 "... = (in. 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: "(im. 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: "(jm. (p(i + 1 := p (i + 1) - 1)) j * j)  (jm. (p(i + 1 := p (i + 1) - 1)) j)"
        using p 0 = 0 not_less by (fastforce intro!: sum_mono)
      have ineq22a: "(jm. (p(i + 1 := p (i + 1) - 1)) j) = (jm. p j) - 1"
        using i + 1  m neq by (simp add: sum.remove[where x="i + 1"])
      have ineq22: "(jm. (p(i + 1 := p (i + 1) - 1)) j)  k - 1"
        using sum neq ineq22a by auto
      have ineq2: "(jm. (p(i + 1 := p (i + 1) - 1)) j * j)  k - 1"
        using ineq21 ineq22 by auto
      have "(im. 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) + (jm. (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 "(im. p i * i) = i + 1 + (jm. (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 "(im. 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 "(im - k. p (i + 1) * i) = (im. p (i + 1) * i)"
      using bounds by (auto intro: sum.mono_neutral_left)
    also have "... = (iSuc ` {..m}. p i * (i - 1))"
      by (auto simp add: sum.reindex)
    also have "... = (iSuc m. p i * (i - 1))"
      using p 0 = 0
      by (simp add: atMost_Suc_eq_insert_0)
    also have "... = (im. p i * (i - 1))"
      using p by (auto elim!: partitionsE)
    also have "... = (im. p i * i - p i)"
      by (simp add: diff_mult_distrib2)
    also have "... = (im. p i * i) - (im. p i)"
      using geq by (simp only: sum_subtractf_nat)
    also have "... = m - k" using sum p by (auto elim!: partitionsE)
    finally show "(im - 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: "(im - k. p i * i) = m - k" by (auto elim!: partitionsE)
  have "(im. p (i - 1) * i) = (iSuc m. p (i - 1) * i)"
    using partitions k by (cases k) (auto elim!: partitionsE)
  also have "(iSuc m. p (i - 1) * i) = (im. p i * (i + 1))"
    by (subst sum.atMost_Suc_shift) simp
  also have "... = (im - k. p i * (i + 1))"
    using eq_0 by (auto intro: sum.mono_neutral_right)
  also have "... = (im - k. p i * i) + (im - 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 "(im. 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 "(im. p (i - 1)) = k"
proof -
  have "p 0 = 0" using partitions by (auto elim!: partitionsE)
  have "(im. 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)) = (im - 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 "(im - 1. p i) = (im. 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 "... = (im - 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)" "(in. 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 "(in. 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: "(in. 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) = (in. 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 "(in. p i * i) = n"
  proof -
    have "(in. 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

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 = (ik. 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 "(im. (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 "(im. 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  (in. 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} = (kn. Partition n k)"
proof -
  have seteq: "{p. p partitions n} = ((λk. {p. p partitions n  (in. 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  (in. p i) = k}) ` {..n}))"
    using finite by (simp add: seteq)
  also have "... = (xn. card {p. p partitions n  sum p {..n} = x})"
    using finite by (subst card_UN_disjoint) auto
  also have "... = (kn. 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_msetx < n have "?N = {}" by auto
  from this show ?thesis by (simp only: card.empty)
qed

end