Package list-filter: The list filter function

Information

namelist-filter
version1.34
descriptionThe list filter function
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
list-append
list-def
list-length
list-map
list-set
natural
set
showData.Bool
Data.List
Function
Number.Natural
Set

Files

Defined Constant

Theorems

p. filter p [] = []

p l. length (filter p l) length l

p l x. member x (filter p l) member x l p x

p l1 l2. filter p (l1 @ l2) = filter p l1 @ filter p l2

p f l. filter p (map f l) = map f (filter (p f) l)

p q l. all p (filter q l) all (λx. q x p x) l

p q l. exists p (filter q l) exists (λx. q x p x) l

p l. toSet (filter p l) = toSet l \ { x. x | ¬p x }

p h t. filter p (h :: t) = if p h then h :: filter p t else filter p t

Input Type Operators

Input Constants

Assumptions

¬

¬

toSet [] =

n. n n

p. p

n. n suc n

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

t. ¬¬t t

l. [] @ l = l

s. \ s =

f. map f [] = []

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

h t. length (h :: t) = suc (length t)

l x. member x l x toSet l

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

h t. toSet (h :: t) = insert h (toSet t)

m n. suc m suc n m n

f g x. (f g) x = f (g x)

() = λp q. r. (p r) (q r) r

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m n n p m p

l h t. (h :: t) @ l = h :: t @ l

p l. all p l x. x toSet l p x

p l. exists p l x. x toSet l p x

p. (x. y. p x y) y. x. p x (y x)

f h t. map f (h :: t) = f h :: map f t

p x. x { y. y | p y } p x

b f x y. f (if b then x else y) = if b then f x else f y

s t x. x s \ t x s ¬(x t)

p. p [] (h t. p t p (h :: t)) l. p l

p c x y. p (if c then x else y) (c p x) (¬c p y)

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)

s t x. insert x s \ t = if x t then s \ t else insert x (s \ t)