Package list: List types

Information

namelist
version1.104
descriptionList types
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksum228bc1b22aa81b4a238aff09a62e39e6062c6bcb
requiresbool
function
natural
pair
set
showData.Bool
Data.List
Data.Pair
Function
Number.Natural
Set

Files

Defined Type Operator

Defined Constants

Theorems

null []

length [] = 0

concat [] = []

nubReverse [] = []

reverse [] = []

toSet [] =

map id = id

l. finite (toSet l)

p. all p []

l. all (λx. ) l

zip [] [] = []

x. ¬member x []

p. ¬any p []

unzip [] = ([], [])

x. replicate x 0 = []

m. interval m 0 = []

l. reverse (reverse l) = l

l. [] @ l = l

l. l @ [] = l

l. drop 0 l = l

l. take 0 l = []

f. map f [] = []

p. filter p [] = []

l. map (λx. x) l = l

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

l. null l l = []

l. length (reverse l) = length l

l. nub (nub l) = nub l

l. nubReverse (nubReverse l) = nubReverse l

l. toSet (nub l) = toSet l

l. toSet (nubReverse l) = toSet l

l. toSet (reverse l) = toSet l

l. length (nub l) length l

l. length (nubReverse l) length l

l. size (toSet l) length l

l. drop (length l) l = []

l. take (length l) l = l

l. case [] (::) l = l

l. foldr (::) [] l = l

f. zipWith f [] [] = []

h t. ¬null (h :: t)

l. all (λx. ) l null l

l. nub l = reverse (nubReverse (reverse l))

l. length l = 0 null l

l. toSet l = null l

l. null (concat l) all null l

x n. length (replicate x n) = n

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

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

h t. tail (h :: t) = t

b f. case b f [] = b

m n. length (interval m n) = n

f b. foldr f b [] = b

f b. foldl f b [] = b

l. length l = 0 l = []

l. toSet l = l = []

l. foldl (flip (::)) [] l = reverse l

s. finite s toSet (fromSet s) = s

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

f l. null (map f l) null l

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

p l. length (filter p l) length l

s. finite s length (fromSet s) = size s

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

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

l x. member x l x toSet l

l x. member x (nub l) member x l

l x. member x (nubReverse l) member x l

l x. member x (reverse l) member x l

l1 l2. foldr (::) l2 l1 = l1 @ l2

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

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

l1 l2. zip l1 l2 = zipWith , l1 l2

l. unzip l = (map fst l, map snd l)

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

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

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

f l. reverse (map f l) = map f (reverse l)

f l. toSet (map f l) = image f (toSet l)

f l. map f l = [] l = []

l. ¬null l head l :: tail l = l

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

h t. take 1 (h :: t) = h :: []

m n. map suc (interval m n) = interval (suc m) n

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

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

l1 l2. reverse (l1 @ l2) = reverse l2 @ reverse l1

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

l1 l2. foldl (flip (::)) l2 l1 = reverse l1 @ l2

f g. map f map g = map (f g)

l. l = [] h t. l = h :: t

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

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

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

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

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

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

m n. interval m (suc n) = m :: interval (suc m) n

n l. n length l length (take n l) = n

l k. foldl (λn x. suc n) k l = length l + k

l k. foldr (λx n. suc n) k l = length l + k

s. finite s x. member x (fromSet s) x s

l. ¬null l length (tail l) = length l - 1

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

p l. (x. member x l p x) all p l

p l. (x. member x l p x) any p l

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

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

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

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

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

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

f g l. map (f g) l = map f (map g l)

p f l. all p (map f l) all (p f) l

p f l. any p (map f l) any (p f) l

f b l. foldr f b (reverse l) = foldl (flip f) b l

f b l. foldl f b l = foldr (flip f) b (reverse l)

f b l. foldl f b (reverse l) = foldr (flip f) b l

x y. zip (x :: []) (y :: []) = (x, y) :: []

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

b f h t. case b f (h :: t) = f h t

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

xs ys. length xs = length ys map fst (zip xs ys) = xs

xs ys. length xs = length ys map snd (zip xs ys) = ys

s. finite s toSet (fromSet s) = s length (fromSet s) = size s

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

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

p h t. any p (h :: t) p h any p t

p l x. member x (filter p l) member x l p x

p l. (x. all (p x) l) all (λy. x. p x y) l

p l. (x. any (p x) l) any (λy. x. p x y) l

n l. n length l length (drop n l) = length l - n

n l. n length l n + length (drop n l) = length l

n l. n length l take n l @ drop n l = l

l xs. unzip l = (xs, []) l = [] xs = []

l ys. unzip l = ([], ys) l = [] ys = []

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

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

m n x. m n take m (replicate x n) = replicate x m

m n i. i < n nth (interval m n) i = m + i

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

f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2

f. (ys. xs. map f xs = ys) y. x. f x = y

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

p l1 l2. filter p (l1 @ l2) = filter p l1 @ filter p l2

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

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

p f l. filter p (map f l) = map f (filter (p f) l)

h t.
    nubReverse (h :: t) =
    if member h t then nubReverse t else h :: nubReverse t

p q l. all p (filter q l) all (λx. q x p x) l

p q l. any p (filter q l) any (λx. q x p x) l

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

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 x y. zipWith f (x :: []) (y :: []) = f x y :: []

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

f b h t. foldr f b (h :: t) = f h (foldr f b t)

f b h t. foldl f b (h :: t) = foldl f (f b h) t

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

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

m n x. m n drop m (replicate x n) = replicate x (n - m)

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

f l y. member y (map f l) x. y = f x member x l

f g l. all (λx. f x = g x) l map f l = map g l

p q l. all (λx. p x q x) l all p l all q l

p q l. all (λx. p x q x) l all p l all q l

f b l1 l2. foldr f b (l1 @ l2) = foldr f (foldr f b l2) l1

f b l1 l2. foldl f b (l1 @ l2) = foldl f (foldl f b l1) l2

l1 l2 n. length l1 = n length l2 = n length (zip l1 l2) = n

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

p l. toSet (filter p l) = toSet l \ { x. x | ¬p x }

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

p h t. filter p (h :: t) = if p h then h :: filter p t else filter p t

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

l n. length l = suc n h t. l = h :: t length t = n

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

m n l. m + n length l drop (m + n) l = drop m (drop n l)

n l i. n + i < length l nth (drop n l) i = nth l (n + i)

n l i. n length l i < n nth (take n l) i = nth l i

l xs ys. unzip l = (xs, ys) length xs = length ys l = zip xs ys

l1 l1' l2 l2'. length l1 = length l1' l1 @ l2 = l1' @ l2' l1 = l1'

l1 l1' l2 l2'. length l2 = length l2' l1 @ l2 = l1' @ l2' l2 = l2'

p q l. (x. member x l p x q x) all p l all q l

p q l. (x. member x l p x q x) any p l any q l

f l1 l2 n. length l1 = n length l2 = n length (zipWith f l1 l2) = n

m n l. m + n length l take (m + n) l = take m l @ take n (drop m l)

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

x y xs ys.
    length xs = length ys zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

f. (l1 l2. map f l1 = map f l2 l1 = l2) x y. f x = f y x = y

f h1 h2 t1 t2.
    length t1 = length t2
    zipWith f (h1 :: t1) (h2 :: t2) = f h1 h2 :: zipWith f t1 t2

unzip = foldr (λ(x, y) (xs, ys). (x :: xs, y :: ys)) ([], [])

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)

x1 x2 y1 y2.
    length x1 = length y1 length x2 = length y2
    zip (x1 @ x2) (y1 @ y2) = zip x1 y1 @ zip x2 y2

l1 l2 n i.
    length l1 = n length l2 = n i < n
    nth (zip l1 l2) i = (nth l1 i, nth l2 i)

h x y t xs ys.
    unzip (h :: t) = (x :: xs, y :: ys) h = (x, y) unzip t = (xs, ys)

n l i.
    n length l i < length l
    nth l i = if i < n then nth (take n l) i else nth (drop n l) (i - n)

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

f l1 l2 n i.
    length l1 = n length l2 = n i < n
    nth (zipWith f l1 l2) i = f (nth l1 i) (nth l2 i)

f x1 x2 y1 y2.
    length x1 = length y1 length x2 = length y2
    zipWith f (x1 @ x2) (y1 @ y2) = zipWith f x1 y1 @ zipWith f x2 y2

g f b l1 l2.
    (s. g b s = s) (x s1 s2. g (f x s1) s2 = f x (g s1 s2))
    foldr f b (l1 @ l2) = g (foldr f b l1) (foldr f b l2)

g f b l1 l2.
    (s. g s b = s) (s1 s2 x. g s1 (f s2 x) = f (g s1 s2) x)
    foldl f b (l1 @ l2) = g (foldl f b l1) (foldl f b l2)

External Type Operators

External Constants

Assumptions

finite

id = λx. x

¬

¬

bit0 0 = 0

size = 0

t. t t

n. 0 n

n. n n

p. p

fromPredicate (λx. ) =

x. ¬(x )

t. t ¬t

m. ¬(m < 0)

n. ¬(n < n)

n. 0 < suc n

n. n < suc n

n. n suc n

(¬) = λp. p

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

a. ∃!x. x = a

t. (x. t) t

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 t

t. t

n. ¬(suc n = 0)

n. 0 + n = n

m. m + 0 = m

m. m - 0 = m

n. n - n = 0

s. \ s =

s. s = s

f. image f =

f. flip (flip f) = f

() = λf g x. f (g x)

flip = λf x y. f y x

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. even (2 * n)

n. bit1 n = suc (bit0 n)

m. m 0 = 1

m n. m m + n

m n. n m + n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

n. even (suc n) ¬even n

m. m 0 m = 0

n. suc n - 1 = n

x. (fst x, snd x) = x

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

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

x s. ¬(insert x s = )

p x. p x p ((select) p)

n. bit0 (suc n) = suc (suc (bit0 n))

f y. (let x y in f x) = f y

x. a b. x = (a, b)

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

m n. m + n = n + m

m n. m + n - m = n

s x. finite (insert x s) finite s

s t. s t = t s

p x. x fromPredicate p p x

n. 2 * n = n + n

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. suc m n m < n

m. m = 0 n. m = suc n

s. (x. x s) ¬(s = )

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

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

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

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

x y. x insert y x = y

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

x s. insert x s = insert x s

t1 t2. ¬(t1 t2) t1 ¬t2

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

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

m n. suc m = suc n m = n

m n. suc m < suc n m < n

m n. suc m suc n m n

m n. m + n = n m = 0

f g x. (f g) x = f (g x)

f x y. flip f x y = f y x

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

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

m n. even (m * n) even m even n

m n. even (m + n) even m even n

m n. m suc n = m * m n

f g. (x. f x = g x) f = g

p a. (x. a = x p x) p a

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

m n. m n m < n m = n

m n. m n n m m = n

f. fn. a b. fn (a, b) = f a b

m n. m < n d. n = m + suc d

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

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

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

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

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

p q r. p q r p q r

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

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

p m n. m + p = n + p m = n

m n p. m + n m + p n p

m n p. m < n n p m < p

m n p. m n n p m p

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

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

p x. (y. p y y = x) (select) p = x

r. (x. y. r x y) f. x. r x (f x)

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

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

m n. m * n = 0 m = 0 n = 0

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

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

m n. m n = 0 m = 0 ¬(n = 0)

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

x y s. x insert y s x = y x s

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

s t x. x s t x s x t

(∃!) = λp. () p x y. p x p y x = y

b f x y. f (if b then x else y) = if b then f x else f y

s t x. x s \ t x s ¬(x t)

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

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

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

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

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

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n

m n p. m * n = m * p m = 0 n = p

m n p. m * n m * p m = 0 n p

x s.
    finite s size (insert x s) = if x s then size s else suc (size s)

y s f. y image f s x. y = f x x s

m n p. m * n < m * p ¬(m = 0) n < p

a b a' b'. (a, b) = (a', b') a = a' b = b'

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p. (x. ∃!y. p x y) f. x y. p x y f x = y

p c x y. p (if c then x else y) (c p x) (¬c p y)

s t x. insert x s \ t = if x t then s \ t else insert x (s \ t)

p. (∃!x. p x) (x. p x) x x'. p x p x' x = x'

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 }

p.
    p (x s. p s ¬(x s) finite s p (insert x s))
    s. finite s p s