# Theory Filter_Bool_List

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