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

Information

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

Files

Theorems

l. ¬null l nth l (length l - 1) = last l

p l. all p l i. i < length l p (nth l i)

p l. exists p l i. i < length l p (nth l i)

l x. member x l i. i < length l x = nth l i

l. toSet l = image (nth l) { i. i | i < length l }

f l i. i < length l nth (map f l) i = f (nth l i)

l1 l2.
    length l1 = length l2 (i. i < length l1 nth l1 i = nth l2 i)
    l1 = l2

l1 l2 k.
    k < length l1 + length l2
    nth (l1 @ l2) k =
    if k < length l1 then nth l1 k else nth l2 (k - length l1)

Input Type Operators

Input Constants

Assumptions

null []

¬

¬

length [] = 0

toSet [] =

t. t t

p. p

fromPredicate (λx. ) =

n. ¬(n < n)

n. 0 < suc n

n. n < suc n

(¬) = λp. p

t. (x. t) t

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

n. ¬(suc n = 0)

m. m < 0

m. m - 0 = m

l. [] @ l = l

f. image f =

l. null l l = []

h t. ¬null (h :: t)

() = λp q. p q p

n. suc n - 1 = n

l. length l = 0 null l

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

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

l. length l = 0 l = []

x y. x = y y = x

x y. x = y y = x

h t. nth (h :: t) 0 = h

t1 t2. t1 t2 t2 t1

f l. length (map f l) = length l

p x. x fromPredicate p p x

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

m n. ¬(m < n) n m

m. m = 0 n. m = suc n

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)

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

m n. suc m = suc n m = n

m n. suc m < suc n m < n

l1 l2. length (l1 @ l2) = length l1 + length l2

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

p. (x y. p x y) y x. p x y

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

s t. (x. x s x t) s = t

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

p l. exists p l x. x toSet l p x

m n. n m suc m - suc n = m - n

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 0 (n. P n P (suc n)) n. P n

p x. x { y. y | p y } p x

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

h t n. n < length t nth (h :: t) (suc n) = nth t n

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 c x y. p (if c then x else y) (c p x) (¬c p y)

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

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

n. { m. m | m < suc n } = insert 0 { m. suc m | m < n }