section ‹Powerset› theory Powerset imports Main n_Sequences Common_Lemmas Filter_Bool_List begin subsection"Definition" text "Pow A" text "Cardinality: ‹2 ^ card A›" text "Example: ‹Pow {0,1} = {{}, {1}, {0}, {0, 1}}›" subsection"Algorithm" fun all_bool_lists :: "nat ⇒ bool list list" where "all_bool_lists 0 = [[]]" | "all_bool_lists (Suc x) = concat [[False#xs, True#xs] . xs ← all_bool_lists x]" fun powerset_enum where "powerset_enum xs = [(filter_bool_list x xs) . x ← all_bool_lists (length xs)]" subsection"Verification" text "First we show the relevant theorems for ‹all_bool_lists›, then we'll transfer the results to the enumeration algorithm for powersets." lemma distinct_concat_aux: "distinct xs ⟹ distinct (concat (map (λxs. [False # xs, True # xs]) xs))" by (induct xs) auto lemma distinct_all_bool_lists : "distinct (all_bool_lists x)" by (induct x) (auto simp add: distinct_concat_aux) lemma all_bool_lists_correct: "set (all_bool_lists x) = {xs. length xs = x}" proof(standard) show "set (all_bool_lists x) ⊆ {xs. length xs = x}" by (induct x) auto next show "{xs. length xs = x} ⊆ set (all_bool_lists x)" proof(induct x) case 0 then show ?case by simp next case (Suc x) have "length ys = Suc x ⟹ ∃xs. ys = False # xs ∨ ys = True # xs" for ys by (metis (full_types) Suc_length_conv) then show ?case using Suc by fastforce qed qed subsubsection"Correctness" theorem powerset_enum_correct: "set (map set (powerset_enum xs)) = Pow (set xs)" proof(standard) show "set (map set (powerset_enum xs)) ⊆ Pow (set xs)" using filter_bool_list_not_elem by fastforce next have "⋀x. x ⊆ set xs ⟹ x ∈ (λx. set (filter_bool_list x xs)) ` {zs. length zs = length xs}" unfolding image_def using filter_bool_list_exist_length image_def by auto then show "Pow (set xs) ⊆ set (map set (powerset_enum xs))" using all_bool_lists_correct by auto qed subsubsection"Distinctness" theorem powerset_enum_distinct_elem: "distinct xs ⟹ ys ∈ set (powerset_enum xs) ⟹ distinct ys" using filter_bool_list_distinct by auto theorem powerset_enum_distinct: "distinct xs ⟹ distinct (powerset_enum xs)" proof - assume dis: "distinct xs" then have " distinct (map (λx. filter_bool_list x xs) (all_bool_lists (length xs)))" using distinct_map filter_bool_list_inj distinct_all_bool_lists by (metis all_bool_lists_correct) then show ?thesis using dis by simp qed subsubsection"Cardinality" text "Cardinality for powersets is already shown in @{thm [source] card_Pow}." subsection"Alternative algorithm with ‹n_sequence_enum›" fun all_bool_lists2 :: "nat ⇒ bool list list" where "all_bool_lists2 n = n_sequence_enum [True, False] n" lemma all_bool_lists2_distinct: "distinct (all_bool_lists2 n)" by (auto simp add: n_sequence_enum_distinct) lemma all_bool_lists2_correct: "set (all_bool_lists n) = set (all_bool_lists2 n)" by (auto simp: all_bool_lists_correct n_sequence_enum_correct n_sequences_def) end