Package list-dest-thm: Properties of list type destructors

Information

namelist-dest-thm
version1.11
descriptionProperties of list type destructors
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-03-24
requiresbool
list-def
list-dest-def
list-thm
showData.Bool
Data.List

Files

Theorems

l. null l l = []

l. case [] (::) l = l

l. ¬null l head l :: tail l = l

Input Type Operators

Input Constants

Assumptions

null []

¬

¬

p. p

(¬) = λp. p

() = λp. p = λx.

t. ( t) t

t. t

t. t t

t. ( t) ¬t

h t. ¬null (h :: t)

() = λp q. p q p

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

h t. head (h :: t) = h

h t. tail (h :: t) = t

b f. case b f [] = b

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

b f h t. case b f (h :: t) = f h t

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