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

Information

namelist-replicate-thm
version1.57
descriptionProperties of the list replicate function
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2013-09-08
requiresbool
list-append
list-def
list-length
list-map
list-nth
list-replicate-def
list-set
list-thm
natural
set
showData.Bool
Data.List
Number.Natural
Set

Files

Theorems

x n. length (replicate x n) = n

x n. null (replicate x n) n = 0

f x n. map f (replicate x n) = replicate (f x) n

x n i. i < n nth (replicate x n) i = x

x n. toSet (replicate x n) = if n = 0 then else insert x

x m n. replicate x (m + n) = replicate x m @ replicate x n

x n y. member y (replicate x n) y = x ¬(n = 0)

x n l1 l2.
    l1 @ l2 = replicate x n
    replicate x (length l1) = l1 replicate x (length l2) = l2
    length l1 + length l2 = n

External Type Operators

External Constants

Assumptions

¬

¬

length [] = 0

toSet [] =

t. t t

p. p

x. ¬(x )

m. ¬(m < 0)

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

x. replicate x 0 = []

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

n. 0 + n = n

l. [] @ l = l

f. map f [] = []

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

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

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

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

x y. x insert y x = y

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

x s. insert x (insert x s) = insert x s

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

m n. suc m = suc n m = n

m n. suc m < suc n m < n

x n. replicate x (suc n) = x :: replicate x n

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

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

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

m n. m + n = 0 m = 0 n = 0

l1 l2. l1 @ l2 = [] l1 = [] l2 = []

f h t. map f (h :: t) = f h :: map f t

p. p 0 (n. p n p (suc n)) n. p n

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

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)