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