Package list-map: The list map function

Information

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

Files

Defined Constant

Theorems

map id = id

f. map f [] = []

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

l f. length (map f l) = length l

f l. toSet (map f l) = image f (toSet l)

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

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

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

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. (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 T

¬T F

length [] = 0

toSet [] =

t. t t

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

t. ¬¬t t

t. (T t) t

t. F t F

t. T t t

t. t T t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

t. t T T

l. [] @ l = l

f. image f =

t. (F t) ¬t

t. t F ¬t

() = λp q. p q p

t. (t T) (t F)

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

x y. x = y y = x

t1 t2. t1 t2 t2 t1

h t. length (h :: t) = suc (length 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

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

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

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

() = λ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

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

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

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

f x s. image f (insert x s) = insert (f x) (image f s)

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)