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

Information

namelist-map
version1.0
description Definitions and theorems about the list map function
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List
Function

Files

Defined Constant

Theorems

map id = id

l. map (λx. x) l = l

f l. map f l = [] l = []

f g l. map (g o f) l = map g (map f l)

f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2

f. (m. l. map f l = m) y. x. f x = y

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

f. (l m. map f l = map f m l = m) x y. f x = f y x = y

Input Type Operators

Input Constants

Assumptions

T

id = λx. x

F p. p

x. id x = x

t. t ¬t

(¬) = λp. p F

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

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

h t. ¬(h :: t = [])

(¬T F) (¬F T)

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

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

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

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

f g. f = g x. f x = g x

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

P Q. P (x. Q x) x. P Q x

P Q. (x. P x) Q x. P x Q

P Q. (x. P x) Q x. P x Q

P. (x. y. P x y) y. x. P x (y x)

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

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

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2

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

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

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

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

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

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

p q r.
    (p q q p) ((p q) r p q r) (p q r q p r)
    (p p p) (p p q p q)