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"
    by (simp add: n_sequence_enum_correct)
  then show "card (n_sequences A n) = card A ^ n"
    using set by simp
qed

end