# Theory n_Sequences

```section "N-Sequences"

theory n_Sequences
imports
"HOL.List"
Common_Lemmas
begin

subsection"Definition"

definition n_sequences :: "'a set ⇒ nat ⇒ 'a list set" where
"n_sequences A n = {xs. set xs ⊆ A ∧ length xs = n}"

text"Cardinality: ‹card A ^ n›"
text"Example: ‹n_sequences {0, 1} 2 = {[0,0], [0,1], [1,0], [1,1]}›"

subsection"Algorithm"

fun n_sequence_enum :: "'a list ⇒ nat ⇒ 'a list list" where
"n_sequence_enum xs 0 = [[]]"
| "n_sequence_enum xs (Suc n) = [x#r . x ← xs, r ← n_sequence_enum xs n]"

text "An enumeration of n-sequences already exists: ‹n_lists›. This part of this AFP entry is mostly
to establish the patterns used in the more complex combinatorial objects."

lemma "set (n_sequence_enum xs n) = set (List.n_lists n xs)"
by(induct n) auto

thm set_n_lists

subsection"Verification"

subsubsection"Correctness"

theorem n_sequence_enum_correct:
"set (n_sequence_enum xs n) = n_sequences (set xs) n"
proof standard
show "set (n_sequence_enum xs n) ⊆ n_sequences (set xs) n"
unfolding n_sequences_def by (induct n) auto+
next
show "n_sequences (set xs) n ⊆ set (n_sequence_enum xs n)"
proof(induct n)
case 0
then show ?case
unfolding n_sequences_def by auto
next
case (Suc n)

have "⟦n_sequences (set xs) n ⊆ set (n_sequence_enum xs n); set x ⊆ set xs; length x = Suc n⟧
⟹ ∃xa∈set xs. x ∈ (#) xa ` set (n_sequence_enum xs n)" for x
unfolding n_sequences_def by (cases x) auto

from this Suc show ?case
unfolding n_sequences_def by auto
qed
qed

subsubsection"Distinctness"

theorem n_sequence_enum_distinct:
"distinct xs ⟹ distinct (n_sequence_enum xs n)"
by (induct n) (auto simp: Cons_distinct_concat_map)

subsubsection"Cardinality"

lemma n_sequence_enum_length:
"length (n_sequence_enum xs n) = (length xs) ^ n "
by(induct n arbitrary: xs) (auto simp: length_concat_map)

text"of course ‹card_lists_length_eq› can directly proof it
but we want to derive it from ‹n_sequence_enum_length›"
thm card_lists_length_eq

theorem n_sequences_card:
assumes "finite A"
shows "card (n_sequences A n) = card A ^ n"
proof -
obtain xs where set: "set xs = A" and dis: "distinct xs"
using assms finite_distinct_list by auto
have "length (n_sequence_enum xs n) = (length xs) ^ n"
using n_sequence_enum_distinct n_sequence_enum_length by auto
then have "card (set (n_sequence_enum xs n)) = card (set xs) ^ n"
by (simp add: dis distinct_card n_sequence_enum_distinct)
then have "card (n_sequences (set xs) n) = card (set xs) ^ n"