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 = {[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

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