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
      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