# Theory n_Permutations

section "N-Permutations"

theory n_Permutations
imports

Common_Lemmas

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

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