# Theory Integer_Compositions

```section "Integer Compositions"

theory Integer_Compositions
imports
Common_Lemmas
begin

subsection"Definition"

definition integer_compositions :: "nat ⇒ nat list set" where
"integer_compositions i = {xs. sum_list xs = i ∧ 0 ∉ set xs}"
text "Integer compositions are ‹integer_partitions› where the order matters."
text "Cardinality: ‹sum from n = 1 to i (binomial (i-1) (n-1)) = 2^(i-1)›"
text "Example: ‹integer_compositions 3 = {, [2,1], [1,2], [1,1,1]}›"

subsection"Algorithm"

fun integer_composition_enum :: "nat ⇒ nat list list" where
"integer_composition_enum 0 = [[]]"
| "integer_composition_enum (Suc n) =
[Suc m #xs. m ← [0..< Suc n], xs ← integer_composition_enum (n-m)]"

subsection"Verification"

subsubsection"Correctness"

lemma integer_composition_enum_tail_elem:
"x#xs ∈ set (integer_composition_enum n) ⟹ xs ∈ set (integer_composition_enum (n - x))"
by(induct n) auto

lemma integer_composition_enum_not_null_aux:
"x#xs ∈ set (integer_composition_enum n) ⟹ x ≠ 0"
by(induct n) auto

lemma integer_composition_enum_not_null: "xs ∈ set (integer_composition_enum n) ⟹ 0 ∉ set xs"
proof(induct xs arbitrary: n)
case Nil
then show ?case
by simp
next
case (Cons a xs)
then show ?case
using integer_composition_enum_not_null_aux integer_composition_enum_tail_elem
by fastforce
qed

lemma integer_composition_enum_empty: "[] ∈ set (integer_composition_enum n) ⟹ n = 0"
by(induct n) auto

lemma integer_composition_enum_sum: "xs ∈ set (integer_composition_enum n) ⟹ sum_list xs = n"
proof(induct n arbitrary: xs rule: integer_composition_enum.induct)
case 1
then show ?case by simp
next
case (2 x)
show ?case proof(cases xs)
case Nil
then show ?thesis using 2 by auto
next
case (Cons y ys)
have p1: "sum_list ys = Suc x - y" using 2 Cons
by auto

have "Suc x ≥ y"
using 2 Cons by auto
then have p2: "sum_list ys = Suc x - y ⟹ y + sum_list ys = Suc x"
by simp

show ?thesis
using p1 p2 Cons by simp
qed
qed

assumes"x ≠ 0" and "x ≤ n"
shows" xs ∈ set (integer_composition_enum (n-x)) ⟹ x#xs ∈ set (integer_composition_enum n)"
using assms proof(induct n arbitrary: x xs)
case 0
then show ?case
by simp
next
case c1: (Suc n)
from c1.prems have 1:
"∀y∈{0..<n}. x = Suc y ⟶ xs ∉ set (integer_composition_enum (n - y)) ⟹ x = Suc n"
by(induct x) simp_all

then have 2: "∀y∈{0..<n}. x = Suc y ⟶ xs ∉ set (integer_composition_enum (n - y)) ⟹ xs = []"
using c1.prems(1) by simp
show ?case using 1 2 by auto
qed

lemma integer_composition_enum_correct_aux:
"0 ∉ set xs ⟹ xs ∈ set (integer_composition_enum (sum_list xs))"

theorem integer_composition_enum_correct:
"set (integer_composition_enum n) = integer_compositions n"
proof standard
show "set (integer_composition_enum n) ⊆ integer_compositions n"
unfolding integer_compositions_def
using integer_composition_enum_not_null integer_composition_enum_sum by auto
next
show "integer_compositions n ⊆ set (integer_composition_enum n)"
unfolding integer_compositions_def
using integer_composition_enum_correct_aux by auto
qed

subsubsection"Distinctness"

theorem integer_composition_enum_distinct:
"distinct (integer_composition_enum n)"
proof(induct n rule: integer_composition_enum.induct)
case 1
then show ?case by auto
next
case (2 n)

have h1: "x ∈ set [0..<Suc n] ⟹ distinct (integer_composition_enum (n - x))" for x
using "2" by simp

have h2: "distinct [0..<n]"
by simp

have "distinct [Suc m #xs. m ← [0..< n], xs ← integer_composition_enum (n-m)]"
using h1 h2 Cons_Suc_distinct_concat_map_function by simp
then show ?case by auto
qed

subsubsection"Cardinality"

lemma sum_list_two_pow_aux:
"(∑x←[0..< n]. (2::nat) ^ (n - x)) + 2 ^ (0 - 1) + 2 ^ 0 = 2 ^ (Suc n)"
proof(induct n)
case 0
then show ?case by simp
next
case c1: (Suc n)

have "x ≤ n ⟹ 2 ^ (Suc n - x) = 2 * 2^ (n - x)" for x
also have "x ∈ set [0..<Suc n] ⟹ x ≤ n" for x
by auto
ultimately have "(∑x←[0..<Suc n]. 2 ^ (Suc n - x)) = (∑x←[0..<Suc n]. 2* 2 ^ (n - x))"
by (metis (mono_tags, lifting) map_eq_conv)

also have "... = (∑x←[0..< n]. 2* 2 ^ (n - x)) + 2* 2 ^ (0)"
using sum_list_extract_last by simp

also have "(∑x←[0..< n]. (2::nat)* (2::nat) ^ (n - x)) = 2*(∑x←[0..< n]. 2 ^ (n - x))"
using sum_list_const_mult by fast

ultimately have "(∑x←[0..<Suc n]. (2::nat) ^ (Suc n - x))
= 2*(∑x←[0..< n]. 2 ^ (n - x)) + 2* 2 ^ (0)"
by metis

then show ?case using c1
by simp
qed

lemma sum_list_two_pow:
"Suc (∑x←[0..<n]. 2 ^ (n - Suc x)) = 2 ^ n"
using sum_list_two_pow_aux sum_list_extract_last by(cases n) auto

lemma integer_composition_enum_length:
"length (integer_composition_enum n) = 2^(n-1)"
proof(induct n rule: integer_composition_enum.induct)
case 1
then show ?case by simp
next
case (2 n)
then have "length [Suc m #xs. m ← [0..< n], xs ← integer_composition_enum (n-m)]
= (∑x←[0..<n]. 2 ^ (n - x - 1))"
using length_concat_map_function_sum_list [of
"[0..< n]"
"λ x. integer_composition_enum (n - x)"
"λ x. 2 ^ (n - x - 1)"
"λ m xs. Suc m #xs"]
by auto

then show ?case
using sum_list_two_pow
by simp
qed

theorem integer_compositions_card:
"card (integer_compositions n) = 2^(n-1)"
using integer_composition_enum_correct integer_composition_enum_length
integer_composition_enum_distinct distinct_card by metis

end
```