Package list-append: Appending lists

Information

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

Files

Defined Constants

Theorems

concat [] = []

l. [] @ l = l

l. l @ [] = l

l. null (concat l) all null l

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

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

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

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

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

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

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

l l1 l2. l @ l1 = l @ l2 l1 = l2

l l1 l2. l1 @ l = l2 @ l l1 = l2

l l1 l2. l @ l1 = l @ l2 l1 = l2

l l1 l2. l1 @ l = l2 @ l l1 = l2

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

l1 l2 x. member x (l1 @ l2) member x l1 member x l2

p l1 l2. all p (l1 @ l2) all p l1 all p l2

p l1 l2. any p (l1 @ l2) any p l1 any p l2

x l. member x l l1 l2. ¬member x l1 l = l1 @ x :: l2

External Type Operators

External Constants

Assumptions

null []

¬

length [] = 0

toSet [] =

t. t t

p. all p []

p. p

x. ¬member x []

t. t ¬t

(¬) = λ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. t t

t. t

n. ¬(suc n = 0)

n. 0 + n = n

s. s = s

l. null l l = []

() = λp q. p q p

l. length l = 0 null l

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

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)

x s. insert x s = insert x s

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

m n. m + n = n m = 0

t1 t2. ¬(t1 t2) ¬t1 ¬t2

p l. ¬any (λx. ¬p x) l all p l

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

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

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

p l. any p l x. x toSet l p x

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

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

p h t. all p (h :: t) p h all p t

x h t. member x (h :: t) x = h member x t

p q r. (p q) r p r q r

s t x. x s t x s x t

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

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)