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

Information

namelist-last-thm
version1.42
descriptionProperties of the last list function
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory exported on 2018-11-26
checksum628ca2e16ad64ea06963ccdbf7a0b4b1e989fe1e
requiresbool
list-append
list-def
list-dest
list-last-def
list-reverse
list-thm
showData.Bool
Data.List

Files

Theorems

x. last (x :: []) = x

l. ¬(l = []) head (reverse l) = last l

l. ¬(l = []) last (reverse l) = head l

l1 l2. last (l1 @ l2) = if null l2 then last l1 else last l2

x1 x2 l. last (x1 :: x2 :: l) = last (x2 :: l)

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

External Type Operators

External Constants

Assumptions

null []

¬

¬

reverse [] = []

p. p

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

t. t

l. reverse (reverse l) = l

l. [] @ l = l

l. l @ [] = l

t. ( t) ¬t

t. t ¬t

h t. ¬null (h :: t)

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

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

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

l. reverse l = [] l = []

t1 t2. t1 t2 t2 t1

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

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

l1 l2. null (l1 @ l2) null l1 null l2

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

h t. last (h :: t) = if null t then h else last t

h t. reverse (h :: t) = reverse t @ h :: []

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

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

p q. (x. p x q x) (x. p x) x. q x

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