# Theory n_Permutations

```section "N-Permutations"

theory n_Permutations
imports
"HOL-Combinatorics.Multiset_Permutations"
Common_Lemmas
"Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics"
begin
subsection"Definition"

definition n_permutations :: "'a set ⇒ nat ⇒ 'a list set" where
"n_permutations A n = {xs. set xs ⊆ A ∧ distinct xs ∧ length xs = n}"
text "Permutations with a maximum length. They are different from ‹HOL-Combinatorics.Multiset_Permutations›
because the entries must all be distinct."
text "Cardinality: ‹'falling factorial' (card A) n›"
text "Example: ‹n_permutations {0,1,2} 2 = {[0,1], [0,2], [1,0], [1,2], [2,0], [2,1]}›"

lemma "permutations_of_set A ⊆ n_permutations A (card A)"
by (simp add: length_finite_permutations_of_set n_permutations_def permutations_of_setD subsetI)

subsection"Algorithm"
(*algorithm for permutations with arbitrary length exists in HOL-Combinatorics.Multiset_Permutations*)
fun n_permutation_enum :: "'a list ⇒ nat ⇒ 'a list list" where
"n_permutation_enum xs 0 = [[]]"
| "n_permutation_enum xs (Suc n) = [x#r . x ← xs, r ← n_permutation_enum (remove1 x xs) n]"

subsection"Verification"

subsubsection"Correctness"

lemma n_permutation_enum_subset: "ys ∈ set (n_permutation_enum xs n) ⟹ set ys ⊆ set xs "
proof(induct n arbitrary: ys xs)
case 0
then show ?case by simp
next
case (Suc n)
obtain x where o1: "x∈set xs" and o2: " ys ∈ (#) x ` set (n_permutation_enum (remove1 x xs) n)"
using Suc by auto

have "y ∈ set (n_permutation_enum (remove1 x xs) n) ⟹ set y ⊆ set xs" for y
using Suc set_remove1_subset by fast

then show ?case using o1 o2
by fastforce
qed

lemma n_permutation_enum_length: "ys ∈ set (n_permutation_enum xs n) ⟹ length ys = n"
by (induct n arbitrary: ys xs) auto

lemma n_permutation_enum_elem_distinct: "distinct xs ⟹ ys ∈ set (n_permutation_enum xs n) ⟹ distinct ys"
proof (induct n arbitrary: ys xs)
case 0
then show ?case
by simp
next
case (Suc n)
then obtain z zs where o: "ys = z # zs"
by auto
from this Suc have t: "zs ∈ set (n_permutation_enum (remove1 z xs) n)"
by auto

then have "distinct zs"
using Suc distinct_remove1 by fast

also have "z ∉ set zs"
using o t n_permutation_enum_subset Suc by fastforce

ultimately show ?case
using o by simp
qed

lemma n_permutation_enum_correct1: "distinct xs ⟹ set (n_permutation_enum xs n) ⊆ n_permutations (set xs) n"
unfolding n_permutations_def
using n_permutation_enum_subset n_permutation_enum_elem_distinct n_permutation_enum_length
by fast

lemma n_permutation_enum_correct2: "ys ∈ n_permutations (set xs) n ⟹ ys ∈ set (n_permutation_enum xs n)"
proof(induct n arbitrary: xs ys)
case 0
then show ?case unfolding n_permutations_def by simp
next
case (Suc n)
show ?case proof(cases ys)
case Nil
then show ?thesis using Suc
next
case (Cons z zs)

have z_in: "z ∈ set xs"
using Suc Cons unfolding n_permutations_def by simp

have 1: "set zs ⊆ set xs"
using Suc Cons unfolding n_permutations_def by simp

have 2: "length zs = n"
using Suc Cons unfolding n_permutations_def by simp

have 3: "distinct zs"
using Suc Cons unfolding n_permutations_def by simp

show ?thesis proof(cases "z ∈ set zs")
case True
then have "zs ∈ set (n_permutation_enum (remove1 z xs) n)"
using Suc Cons unfolding n_permutations_def by auto
then show ?thesis
using True Cons z_in by auto
next
case False
then have "x ∈ set zs ⟹ x ∈ set (remove1 z xs)" for x
using 1 by(cases "x = z") auto

then have "zs ∈ n_permutations (set (remove1 z xs)) n"
unfolding n_permutations_def using 2 3 by auto
then have "zs ∈ set (n_permutation_enum (remove1 z xs) n)"
using Suc by simp
then have "∃x∈set xs. z # zs ∈ (#) x ` set (n_permutation_enum (remove1 x xs) n)"
unfolding image_def using z_in by simp
then show ?thesis
using False Cons by simp
qed
qed
qed

theorem n_permutation_enum_correct: "distinct xs ⟹ set (n_permutation_enum xs n) = n_permutations (set xs) n"
proof standard
show "distinct xs ⟹ set (n_permutation_enum xs n) ⊆ n_permutations (set xs) n"
next
show "distinct xs ⟹ n_permutations (set xs) n ⊆ set (n_permutation_enum xs n)"
qed

subsubsection"Distinctness"

theorem n_permutation_distinct: "distinct xs ⟹ distinct (n_permutation_enum xs n)"
proof(induct n arbitrary: xs)
case 0
then show ?case by simp
next
case (Suc n)
let ?f = "λx. (n_permutation_enum (remove1 x xs) n)"
from Suc have "distinct (?f x)" for x
by simp

from this Suc show ?case
by (auto simp: Cons_distinct_concat_map_function_distinct_on_all [of ?f xs])
qed

subsubsection"Cardinality"
thm card_lists_distinct_length_eq
theorem "finite A ⟹ card (n_permutations A n) = ffact n (card A)"
unfolding n_permutations_def using card_lists_distinct_length_eq
by (metis (no_types, lifting) Collect_cong)

subsection"‹n_multiset› extension (with remdups)"

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

fun n_multiset_permutation_enum :: "'a list ⇒ nat ⇒ 'a list list" where
"n_multiset_permutation_enum xs n = remdups (n_permutation_enum xs n)"

lemma "distinct (n_multiset_permutation_enum xs n)"
by auto

lemma n_multiset_permutation_enum_correct1:
"mset ys ⊆# mset xs ⟹ ys ∈ set (n_permutation_enum xs (length ys))"
proof(induct "ys" arbitrary: xs)
case Nil
then show ?case
by simp
next
case (Cons y ys)
then have "y ∈ set xs"
moreover have "ys ∈ set (n_permutation_enum (remove1 y xs) (length ys))"
using Cons by (simp add: insert_subset_eq_iff)
ultimately show ?case
using Cons by auto
qed

lemma n_multiset_permutation_enum_correct2:
"ys ∈ set (n_permutation_enum xs n) ⟹ mset ys ⊆# mset xs"
proof(induct "n" arbitrary: xs ys)
case 0
then show ?case
by simp
next
case (Suc n)
then show ?case
using insert_subset_eq_iff mset_remove1 by fastforce
qed

lemma n_multiset_permutation_enum_correct:
"set (n_multiset_permutation_enum xs n) = n_multiset_permutations (mset xs) n"
unfolding n_multiset_permutations_def
proof(standard)
show "set (n_multiset_permutation_enum xs n) ⊆ {xsa. mset xsa ⊆# mset xs ∧ length xsa = n}"
by (simp add: n_multiset_permutation_enum_correct2 n_permutation_enum_length subsetI)
next
show "{xsa. mset xsa ⊆# mset xs ∧ length xsa = n} ⊆ set (n_multiset_permutation_enum xs n)"
using n_multiset_permutation_enum_correct1 by auto
qed

end
```