Package list-append: The list append function

Information

namelist-append
version1.30
descriptionThe list append function
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
natural
set
list-def
list-thm
list-dest
list-length
list-set
showData.Bool
Data.List
Number.Natural
Set

Files

Defined Constant

Theorems

l. [] @ l = l

l. l @ [] = l

l m. null (l @ m) null l null m

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

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

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

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

l m. head (l @ m) = if l = [] then head m else head l

l m. l @ m = [] l = [] m = []

Input Type Operators

Input Constants

Assumptions

¬

length [] = 0

toSet [] =

p. p

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

t. ( t) t

t. t

t. t t

t. t t t

n. 0 + n = n

s. s = s

t. ( t) ¬t

l. null l l = []

() = λp q. p q p

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

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

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

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

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

x s. insert x s = insert x s

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

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

s t u. s t u = s (t u)

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

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

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)