# Theory Integer_Compositions

section "Integer Compositions"

theory Integer_Compositions
imports
Common_Lemmas
begin

subsection"Definition"

definition integer_compositions ::  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 = {[3], [2,1], [1,2], [1,1,1]}›"

subsection"Algorithm"

fun integer_composition_enum ::  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:
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

lemma integer_composition_enum_head_set:
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))"
by(induct xs) (auto simp: integer_composition_enum_head_set)

theorem integer_composition_enum_correct:

proof standard
show
unfolding integer_compositions_def
using integer_composition_enum_not_null integer_composition_enum_sum by auto
next
show
unfolding integer_compositions_def
using integer_composition_enum_correct_aux by auto
qed

subsubsection"Distinctness"

theorem integer_composition_enum_distinct:

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

have h1:  for x
using "2" by simp

have h2:
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
by (simp add: Suc_diff_le)
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