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

Information

namelist-reverse-thm
version1.10
descriptionProperties of the list reverse function
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-15
requiresbool
natural
set
list-def
list-length
list-set
list-append
list-reverse-def
showData.Bool
Data.List
Number.Natural
Set

Files

Theorems

l. reverse (reverse l) = l

l. length (reverse l) = length l

l. toSet (reverse l) = toSet l

l m. reverse (l @ m) = reverse m @ reverse l

Input Type Operators

Input Constants

Assumptions

T

length [] = 0

reverse [] = []

toSet [] =

t. (x. t) t

() = λp. p = λx. T

m. m + 0 = m

l. [] @ l = l

l. l @ [] = l

() = λp q. p q p

s t. s t = t s

h t. length (h :: t) = suc (length t)

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

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

x s. insert x s = insert x s

m n. m + suc n = suc (m + n)

l m. length (l @ m) = length l + length m

l1 l2. toSet (l1 @ l2) = toSet l1 toSet l2

x l. reverse (x :: l) = reverse l @ x :: []

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

l m n. l @ m @ n = (l @ m) @ n

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