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 by (simp add: n_permutations_def) 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" by (simp add: n_permutation_enum_correct1) next show "distinct xs ⟹ n_permutations (set xs) n ⊆ set (n_permutation_enum xs n)" by (simp add: n_permutation_enum_correct2 subsetI) 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" by (simp add: insert_subset_eq_iff) 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