Package list-map-thm: Properties of the list map function

Information

namelist-map-thm
version1.39
descriptionProperties of the list map function
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-03-24
requiresbool
function
list-append
list-def
list-dest
list-length
list-map-def
list-set
list-thm
set
showData.Bool
Data.List
Function
Number.Natural
Set

Files

Theorems

map id = id

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

f l. null (map f l) null l

f l. 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 (f g) l = map f (map g l)

p f l. all p (map f l) all (p f) l

p f l. exists p (map f l) exists (p f) l

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

f. (ys. xs. map f xs = ys) y. x. f x = y

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

f g l. all (λx. f x = g x) l map f l = map g l

f. (l1 l2. map f l1 = map f l2 l1 = l2) x y. f x = f y x = y

Input Type Operators

Input Constants

Assumptions

id = λx. x

¬

length [] = 0

toSet [] =

t. t t

p. p

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

t. t

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

l. [] @ l = l

f. map f [] = []

f. image f =

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

t. t ¬t

l. null l l = []

() = λp q. p q p

t. (t ) (t )

l. length l = 0 null l

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

x y. x = y y = x

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)

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

l. l = [] h t. l = h :: t

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

p l. ¬all (λx. ¬p x) l exists p l

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

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

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

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

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

p h t. all p (h :: t) p h all p t

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

y s f. y image f s x. y = f x x s

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

p f s. (y. y image f s p y) x. x s p (f x)