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

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
next
  case (Cons y xs)
  then show ?case 
    using integer_partitions_enum_aux_max_head integer_partitions_enum_aux_first  
    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

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

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" ∃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
  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
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
    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
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"
  using integer_partitions_cardinality_aux Partition_sum_Partition_diff add_implies_diff le_add1 mult_2
  by simp  

end