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

Information

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

Files

Theorems

map id = id

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 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

id = λx. x

¬

¬

length [] = 0

toSet [] =

t. t t

p. p

x. id x = x

t. t ¬t

(¬) = λp. p

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. t

t. t t

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 =

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

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

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 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. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

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