Package list-filter: Definitions and theorems about the list filter function

Information

namelist-filter
version1.12
descriptionDefinitions and theorems about the list filter function
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List
Function

Files

Defined Constant

Theorems

p l. Number.Natural.≤ (length (filter p l)) (length l)

p l. Set.⊆ (toSet (filter p l)) (toSet l)

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. filter P [] = [])
  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

T

n. Number.Natural.≤ n n

s. Set.⊆ s s

F p. p

n. Number.Natural.≤ n (Number.Natural.suc n)

(¬) = λp. p F

() = λP. P ((select) P)

t. (x. t) t

() = λp. p = λx. T

x. x = x T

() = λp q. p q p

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

() = λP. q. (x. P x q) q

x s. Set.∪ (Set.insert x Set.∅) s = Set.insert x s

m n.
    Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.≤ m n

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

m n p.
    Number.Natural.≤ m n Number.Natural.≤ n p Number.Natural.≤ m p

s t u. Set.⊆ s t Set.⊆ t u Set.⊆ s u

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

length [] = 0 h t. length (h :: t) = Number.Natural.suc (length t)

toSet [] = Set.∅ h t. toSet (h :: t) = Set.insert h (toSet t)

(s t. Set.⊆ s (Set.∪ s t)) s t. Set.⊆ s (Set.∪ t s)

s t u. Set.⊆ (Set.∪ s t) u Set.⊆ s u Set.⊆ t u

P. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

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

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)

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

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

t. (T t t) (t T t) (F t F) (t F F) (t t t)