Theory Integer_Partitions

section "Integer Paritions"

theory Integer_Partitions


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}}›"


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"



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

lemma integer_partitions_enum_aux_max_head:
  "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
  case (Cons y xs)
  then show ?case 
    using integer_partitions_enum_aux_max_head integer_partitions_enum_aux_first  
    by fastforce                                         

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
  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

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
  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 
    case False
    then show ?thesis
       using Cons integer_partitions_enum_aux_not_null_aux integer_partitions_enum_aux_first
       by fastforce

lemma integer_partitions_enum_aux_head_minus:
     "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
  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

lemma integer_partitions_enum_aux_head_plus:
  "h  m  h > 0  ys  set (integer_partitions_enum_aux n h)
     h#ys  set (integer_partitions_enum_aux (h + n) m)"
  using integer_partitions_enum_aux_head_minus by simp 

lemma integer_partitions_enum_correct_aux1:
  assumes "0 ∉# A "
  and "x ∈# A. x  m"
shows" xsset (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
  case (add h A)
  have hc1: "h  m"
    using add by simp

  have hc2: "h > 0"
    using add by simp

  obtain ys where o1: "ys  set (integer_partitions_enum_aux (# A) h)" and o2: " A = mset ys"
    using add by force

  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

theorem integer_partitions_enum_correct:
  "set (map mset (integer_partitions_enum n)) = integer_partitions n"
  have "xs  set (integer_partitions_enum_aux n n)  # (mset xs) = n" for xs
    by (simp add: integer_partitions_enum_aux_sum sum_mset_sum_list)
  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
  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


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
  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

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


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) = (kn. 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"
  using integer_partitions_cardinality_aux Partition_sum_Partition_diff add_implies_diff le_add1 mult_2
  by simp