Theory n_Subsets

section "N-Subsets"

theory n_Subsets
  imports
    Common_Lemmas
    "HOL-Combinatorics.Multiset_Permutations"
    Filter_Bool_List
begin

subsection"Definition"

definition n_subsets :: "'a set ⇒ nat ⇒ 'a set set" where
  "n_subsets A n = {B. B ⊆ A ∧ card B = n}"

text "Cardinality: ‹binomial (card A) n›"
text "Example: ‹n_subsets {0,1,2} 2 = {{0,1}, {0,2}, {1,2}}›"

subsection"Algorithm"

fun n_bool_lists :: "nat ⇒ nat ⇒ bool list list" where
  "n_bool_lists n 0 = (if n > 0 then [] else [[]])"
| "n_bool_lists n (Suc x) = (if n = 0 then [replicate (Suc x) False]
    else if n = Suc x then [replicate (Suc x) True]
    else if n > x then []
    else [False#xs . xs ← n_bool_lists n x] @ [True#xs . xs ← n_bool_lists (n-1) x])"

fun n_subset_enum :: "'a list ⇒ nat ⇒ 'a list list" where
  "n_subset_enum xs n = [(filter_bool_list bs xs) . bs ← (n_bool_lists n (length xs))]"

subsection"Verification"
                        
subsubsection"n-bool-lists"

lemma n_bool_lists_True_count: "xs ∈ set (n_bool_lists n x) ⟹ count_list xs True = n"
 by (induct x arbitrary: xs n) (auto split: if_splits simp: count_list_replicate)

lemma n_bool_lists_length: "xs ∈ set (n_bool_lists n x) ⟹ length xs = x"
  by (induct x arbitrary: xs n) (auto split: if_splits)

lemma n_bool_lists_distinct: "distinct (n_bool_lists n x)"
proof(induct x arbitrary: n)
  case 0
  then show ?case by simp
next
  case (Suc x)
  then show ?case
    using distinct_map by fastforce
qed

lemma replicate_True_not_False: "count_list ys True = 0 ⟷ ys = replicate (length ys) False"
  using count_list_zero_not_elem count_list_full_elem count_list_length_replicate by fastforce

lemma n_bool_lists_correct_aux:
  "length xs = x ⟹ count_list xs True = n ⟹ xs ∈ set (n_bool_lists n x)"
proof(induct x arbitrary: n xs)
  case 0
  then show ?case by auto
next
  case (Suc x)
   show ?case proof(cases "n = 0")
    case True
    then show ?thesis
      using Suc True replicate_True_not_False by auto
  next
    case c1: False
    then show ?thesis proof(cases "n = Suc x")
      case True
      then have "xs = True # replicate x True "
        using Suc.prems count_list_length_replicate replicate_Suc by metis
      then show ?thesis
        using True by simp
    next
      case c2: False
      then show ?thesis proof(cases "n > x")
        case True
        then have "xs = []"
          using Suc.prems c2 count_le_length by (metis Suc_lessI linorder_not_less)
        then show ?thesis
          using Suc by auto
      next
        case c3: False
        then show ?thesis proof (cases xs)
          case Nil
          then show ?thesis
            using Suc.prems(1) by auto 
        next
          case (Cons y ys)
          then show ?thesis proof (cases y)
            case True
            then show ?thesis using Suc c1 c2 c3 Cons
              by simp 
          next
            case False 
            then show ?thesis using Suc c1 c2 c3 Cons
              by simp
          qed 
        qed
      qed
    qed
  qed
qed

lemma n_bool_lists_correct: "set (n_bool_lists n x) = {xs. length xs = x ∧ count_list xs True = n}"
proof(standard)
  show "set (n_bool_lists n x) ⊆ {xs. length xs = x ∧ count_list xs True = n}"
  proof(cases x)
    case 0
    then show ?thesis by simp
  next
    case (Suc x)
    then show ?thesis using n_bool_lists_True_count n_bool_lists_length
      by blast
  qed
next
  show "{xs. length xs = x ∧ count_list xs True = n} ⊆ set (n_bool_lists n x)"
    using n_bool_lists_correct_aux by auto
qed


subsubsection"Correctness"

lemma n_subset_enum_correct_aux1:
  "⟦distinct xs; length ys = length xs⟧
    ⟹ set (filter_bool_list ys xs) ∈ n_subsets (set xs) (count_list ys True)"
  unfolding n_subsets_def
  by (auto simp: filter_bool_list_card filter_bool_list_elem)

lemma n_subset_enum_correct_aux2:
  "distinct xs ⟹ n_subsets (set xs) n ⊆ set (map set (n_subset_enum xs n))"
  unfolding n_subsets_def
  by (auto simp: n_bool_lists_correct image_def filter_bool_list_exist_length_card_True)

theorem n_subset_enum_correct:
  "distinct xs ⟹ set (map set (n_subset_enum xs n)) = n_subsets (set xs) n"
proof(standard)
  show "distinct xs ⟹ set (map set (n_subset_enum xs n)) ⊆ n_subsets (set xs) n"
    using n_subset_enum_correct_aux1 n_bool_lists_correct by auto
next
  show "distinct xs ⟹ n_subsets (set xs) n ⊆ set (map set (n_subset_enum xs n))"
    using n_subset_enum_correct_aux2 by auto
qed

subsubsection"Distinctness"

theorem n_subset_enum_distinct_elem:
  "distinct xs ⟹ ys ∈ set (n_subset_enum xs n) ⟹ distinct ys"
  by(cases "length xs < n") (auto simp: filter_bool_list_distinct)

theorem n_subset_enum_distinct: "distinct xs ⟹ distinct (n_subset_enum xs n)"
  by(auto simp: distinct_map n_bool_lists_distinct inj_on_def filter_bool_list_inj_aux n_bool_lists_length)

subsubsection"Cardinality"

text ‹Cardinality of @{term "n_subsets"} is already shown in @{thm [source] "Binomial.n_subsets"}.›

subsection "Alternative using Multiset permutations"

text "It would be possible to define ‹n_bool_lists› using ‹permutations_of_multiset› with the
following definition:"

fun n_bool_lists2 :: "nat ⇒ nat ⇒ bool list set" where
  "n_bool_lists2 n x = (if n > x then {}
    else permutations_of_multiset (mset (replicate n True @ replicate (x-n) False)))"

subsection"‹mset_count›"

text"Correspondence between ‹count_list› and ‹count (mset xs)› and transfer of a few results
for multisets to lists."

lemma count_list_count_mset: "count_list ys T = n ⟹ count (mset ys) T = n"
  by(induct ys arbitrary: n) auto

lemma count_mset_count_list: "count (mset ys) T = n ⟹ count_list ys T = n"
  by(induct ys arbitrary: n) auto

lemma count_mset_replicate_aux1:
  "⟦¬ x < n; mset ys = mset (replicate n True) + mset (replicate (x - n) False)⟧
    ⟹ count (mset ys) True = n"
  by (auto simp: count_list_count_mset count_mset)

lemma  count_mset_replicate_aux2: 
  assumes "¬ length xs < count_list xs True"
  shows "mset xs = mset (replicate (count_list xs True) True) + mset (replicate (length xs - count_list xs True) False)"
proof -
  have "count_list xs B =
         count_list (replicate (count_list xs True) True) B + count_list (replicate (length xs - count_list xs True) False) B"
    for B
  proof(cases B)
    case True
    then show ?thesis
      by (simp add: count_list_replicate)
  next
    case False

    have "count_list xs False = count_list (replicate (length xs - count_list xs True) False) False"
      by (metis count_list_True_False count_list_replicate diff_add_inverse)
      
    from this False show ?thesis
      using assms by auto 
  qed

  then have "count (mset xs) B =
         count (mset (replicate (count_list xs True) True) + mset (replicate (length xs - count_list xs True) False)) B"
    for B
    by (metis count_mset_count_list count_union)
  
  then show "mset xs = mset (replicate (count_list xs True) True) + mset (replicate (length xs - count_list xs True) False)"
    using multiset_eqI by blast
qed

lemma n_bool_lists2_correct: "set (n_bool_lists n x) = n_bool_lists2 n x"
proof(standard)
  have "⟦¬ length ys < count_list ys True; x = length ys; n = count_list ys True⟧
          ⟹ ys ∈ permutations_of_multiset
                     (mset (replicate (count_list ys True) True) + mset (replicate (length ys - count_list ys True) False))"
          for ys
    using count_mset_replicate_aux2 permutations_of_multisetI by blast
  
  then show "set (n_bool_lists n x) ⊆ n_bool_lists2 n x"
    unfolding n_bool_lists_correct
    by (auto simp: count_le_length leD)
next
  have "⟦¬ x < n; ys ∈ permutations_of_multiset (mset (replicate n True) + mset (replicate (x - n) False))⟧
          ⟹ count (mset ys) True = n " for ys
    using count_mset_replicate_aux1 permutations_of_multisetD by blast
  then have "⟦¬ x < n; ys ∈ permutations_of_multiset (mset (replicate n True) + mset (replicate (x - n) False))⟧
          ⟹  count_list ys True = n " for ys
    by (simp add: count_list_count_mset) 
  then show "n_bool_lists2 n x ⊆ set (n_bool_lists n x)" unfolding n_bool_lists_correct 
    by (auto simp: length_finite_permutations_of_multiset)
qed

end