# 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