Theory Derangements_Enum

```section"Derangements"
theory Derangements_Enum
imports
"HOL-Combinatorics.Multiset_Permutations"
"Common_Lemmas"
(* "Derangements.Derangements" *)
begin

subsection"Definition"

fun no_overlap :: "'a list ⇒ 'a list ⇒ bool" where
"no_overlap _ [] = True"
| "no_overlap [] _ = True"
| "no_overlap (x#xs) (y#ys) = (x ≠ y ∧ no_overlap xs ys)"

lemma no_overlap_nth: "length xs = length ys ⟹ i < length xs ⟹ no_overlap xs ys ⟹ xs ! i ≠ ys ! i"
by(induct xs ys arbitrary: i rule: list_induct2) (auto simp: less_Suc_eq_0_disj)

lemma nth_no_overlap: "length xs = length ys ⟹ ∀ i < length xs. xs ! i ≠ ys ! i ⟹ no_overlap xs ys"
proof (induct xs ys rule: list_induct2)
case (Cons x xs y ys)
then show ?case using Suc_less_eq nth_Cons_Suc by fastforce
qed simp

definition derangements :: "'a list ⇒ 'a list set" where
"derangements xs = {ys. distinct ys ∧ length xs = length ys ∧ set xs = set ys ∧ no_overlap xs ys }"
text "A derangement of a list is a permutation where every element changes its position,
assuming all elements are distinguishable."
text ‹An alternative definition exists in ‹Derangements.Derangements› \cite{AFPderan}.›
text "Cardinality: ‹count_derangements (length xs)› (from ‹Derangements.Derangements›)"
text "Example: ‹derangements [0,1,2] = {[1,2,0], [2,0,1]}›"

subsection"Algorithm"
fun derangement_enum_aux :: "'a list ⇒ 'a list ⇒ 'a list list" where
"derangement_enum_aux [] ys = [[]]"
| "derangement_enum_aux (x#xs) ys = [y#r . y ← ys, r ← derangement_enum_aux xs (remove1 y ys), y ≠ x]"

fun derangement_enum :: "'a list  ⇒ 'a list list" where
"derangement_enum xs = derangement_enum_aux xs xs"

subsection"Verification"

subsubsection"Correctness"

lemma derangement_enum_aux_elem_length: "zs ∈ set (derangement_enum_aux xs ys) ⟹ length xs = length zs"
by(induct xs arbitrary: ys zs) auto

lemma derangement_enum_aux_not_in: "y ∉ set ys ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ y ∉ set zs"
proof(induct xs arbitrary: ys zs)
case Nil
then show ?case by simp
next
case (Cons x xs)
then obtain z zs2 where ob: "zs = z#zs2"
by auto
have "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys)) ⟹ y ∉ set zs2"
using Cons notin_set_remove1 by fast
then show ?case using Cons ob
by auto
qed

lemma derangement_enum_aux_in: "y ∈ set zs ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ y ∈ set ys"
using derangement_enum_aux_not_in by fast

lemma derangement_enum_aux_distinct_elem: "distinct ys ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ distinct zs"
proof(induct xs arbitrary: ys zs)
case Nil
then show ?case by simp
next
case (Cons x xs)
obtain z zs2 where ob: "zs = z#zs2"
using Cons by auto
then have ev: "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys))"
using Cons ob by auto

have "distinct zs2"
using ev Cons distinct_remove1 by fast
moreover have "z ∉ set zs2"
using ev Cons(2) derangement_enum_aux_in by fastforce
ultimately show ?case using ob by simp
qed

lemma derangement_enum_aux_no_overlap: "zs ∈ set (derangement_enum_aux xs ys) ⟹ no_overlap xs zs"
by(induct xs arbitrary: zs ys) auto

lemma derangement_enum_aux_set:
"length xs = length ys ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ set zs = set ys"
proof(induct xs ys arbitrary: zs rule: derangement_enum_aux.induct)
case (1 ys)
then show ?case by simp
next
case (2 x xs ys)
obtain z zs2 where ob: "zs = z#zs2"
using 2 by auto
have ev1: "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys))"
using 2 ob  by simp
have ev2:"z ∈ set ys"
using 2 ob by simp

have "length xs = length (remove1 z ys)"
using ev2 Suc_length_remove1 "2.prems"(1) by force
then have "set zs2 = set (remove1 z ys)"
using "2.hyps"[of z zs2] ev1 ev2  by simp

then show ?case
using ob notin_set_remove1 ev2 in_set_remove1 by fastforce
qed

lemma derangement_enum_correct_aux1:
"⟦distinct zs;length ys = length zs; length ys = length xs; set ys = set zs; no_overlap xs zs⟧
⟹ zs ∈ set (derangement_enum_aux xs ys)"
proof(induct xs arbitrary: zs ys)
case Nil
then show ?case by simp
next
case (Cons x xs)
obtain z zs2 where ob: "zs = z#zs2"
using Cons length_0_conv neq_Nil_conv by metis

have e1: "z ≠ x"
using Cons.prems(5) ob  by auto

have "distinct zs2"
using Cons.prems(1) ob by auto
moreover have "length (remove1 z ys) = length zs2" using Cons.prems ob
moreover have "length (remove1 z ys) = length xs"
by (simp add: Cons.prems(3) Cons.prems(4) length_remove1 ob)
moreover have "set (remove1 z ys) = set zs2"
using Cons ob by (metis distinct_card distinct_remdups length_remdups_eq remove1.simps(2) set_remdups set_remove1_eq)
moreover have "no_overlap xs zs2"
using Cons.prems(5) ob by fastforce

ultimately have "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys))"
using Cons.hyps[of zs2 "(remove1 z ys)"] by simp
then show ?case
using ob e1 Cons by simp
qed

theorem derangement_enum_correct: "distinct xs ⟹ derangements xs = set (derangement_enum xs)"
proof(standard)
show "distinct xs ⟹ derangements xs ⊆ set (derangement_enum xs)"
unfolding derangements_def using derangement_enum_correct_aux1 by auto
next
show "distinct xs ⟹ set (derangement_enum xs) ⊆ derangements xs"
unfolding derangements_def
using derangement_enum_aux_set derangement_enum_aux_distinct_elem derangement_enum_aux_elem_length derangement_enum_aux_no_overlap
by auto
qed

subsubsection"Distinctness"

lemma derangement_enum_aux_distinct: "distinct ys ⟹ distinct (derangement_enum_aux xs ys)"
proof(induct xs arbitrary: ys)
case Nil
then show ?case by simp
next
case (Cons x xs)
show ?case
using inj2_distinct_concat_map_function_filter[of
"Cons"
ys
"λy. derangement_enum_aux xs (remove1 y ys)"
"λy. y ≠ x"
]
using Cons Cons_inj2
by (simp)
qed

theorem derangement_enum_distinct: "distinct xs ⟹ distinct (derangement_enum xs)"
using derangement_enum_aux_distinct by auto

(*
subsubsection"Cardinality"
should be provable with Derangements.Derangements
*)

end
```