theory Filter_Bool_List imports "HOL.List" begin text "A simple algorithm to filter a list by a boolean list. A different approach would be to filter by a set of indices, but this approach is faster, because lookups are slow in ML." fun filter_bool_list :: "bool list ⇒ 'a list ⇒ 'a list" where "filter_bool_list [] _ = []" | "filter_bool_list _ [] = []" | "filter_bool_list (b#bs) (x#xs) = (if b then x#(filter_bool_list bs xs) else (filter_bool_list bs xs))" text"The following could be an alternative definition, but the version above provides a nice computational induction rule." lemma "filter_bool_list bs xs = map snd (filter fst (zip bs xs))" by(induct bs xs rule: filter_bool_list.induct) auto lemma filter_bool_list_in: "n < length xs ⟹ n < length bs ⟹ bs!n ⟹ xs!n ∈ set (filter_bool_list bs xs)" proof (induct bs xs arbitrary: n rule: filter_bool_list.induct) case (3 b bs x xs) then show ?case by(cases n) auto qed auto lemma filter_bool_list_not_elem: "x ∉ set xs ⟹ x ∉ set (filter_bool_list bs xs)" by(induct bs xs rule: filter_bool_list.induct) auto lemma filter_bool_list_elem: "x ∈ set (filter_bool_list bs xs) ⟹ x ∈ set xs" using filter_bool_list_not_elem by fast lemma filter_bool_list_not_in: "distinct xs ⟹ n < length xs⟹ n < length bs ⟹ bs!n = False ⟹ xs!n ∉ set (filter_bool_list bs xs)" proof (induct bs xs arbitrary: n rule: filter_bool_list.induct) case (3 b bs x xs) then show ?case proof(induct n) case 0 then show ?case using filter_bool_list_not_elem by force qed auto qed auto lemma filter_bool_list_elem_nth: "ys ∈ set (filter_bool_list bs xs) ⟹ ∃n. ys = xs ! n ∧ bs ! n ∧ n < length bs ∧ n < length xs" proof(induct bs xs arbitrary: ys rule: filter_bool_list.induct) case (1 xs) then show ?case by simp next case (2 b bs) then show ?case by simp next case (3 b bs y ys) then show ?case by(cases b) (force)+ qed text"May be a useful conversion, since the algorithm could also be implemented with a list of indices." lemma filter_bool_list_set_nth: "set (filter_bool_list bs xs) = {xs ! n |n. bs ! n ∧ n < length bs ∧ n < length xs}" by (auto simp: filter_bool_list_in filter_bool_list_elem_nth) lemma filter_bool_list_exist_length: "A ⊆ set xs ⟹ ∃bs. length bs = length xs ∧ A = set (filter_bool_list bs xs)" proof(induct xs arbitrary: A) case Nil then show ?case by auto next case (Cons x xs) from Cons have "A - {x} ⊆ set xs" by auto from this Cons have 1: "∃bs. length bs = length xs ∧ A - {x} = set (filter_bool_list bs xs)" by simp then have "∃bs. length bs = length (x # xs) ∧ A = set (filter_bool_list bs (x # xs))" by (metis Diff_empty Diff_insert0 insert_Diff_single insert_absorb list.simps(15) list.size(4) filter_bool_list.simps(3)) then show ?case . qed lemma filter_bool_list_card: "⟦distinct xs; length xs = length bs⟧ ⟹ card (set (filter_bool_list bs xs)) = count_list bs True" by(induct bs xs rule: filter_bool_list.induct) (auto simp: filter_bool_list_not_elem) lemma filter_bool_list_exist_length_card_True: "⟦distinct xs; A ⊆ set xs; n = card A⟧ ⟹ ∃bs. length bs = length xs ∧ count_list bs True = card A ∧ A = set (filter_bool_list bs xs)" by (metis filter_bool_list_card filter_bool_list_exist_length) lemma filter_bool_list_distinct: "distinct xs ⟹ distinct (filter_bool_list bs xs)" by(induct bs xs rule: filter_bool_list.induct) (auto simp: filter_bool_list_not_elem) lemma filter_bool_list_inj_aux: assumes "length bs1 = length xs" and "length xs = length bs2" and "distinct xs" shows "filter_bool_list bs1 xs = filter_bool_list bs2 xs ⟹ bs1 = bs2" using assms proof(induct rule: list_induct3) case Nil then show ?case by simp next case (Cons b1 bs1 x xs b2 bs2) then show ?case by(cases b1; cases b2, auto) (metis list.set_intros(1) filter_bool_list_not_elem)+ qed lemma filter_bool_list_inj: "distinct xs ⟹ inj_on (λbs. filter_bool_list bs xs) {bs. length bs = length xs}" unfolding inj_on_def using filter_bool_list_inj_aux by fastforce end