Package list-set: List to set conversions

Information

namelist-set
version1.48
descriptionList to set conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
list-def
list-dest
list-length
natural
set
showData.Bool
Data.List
Number.Natural
Set

Files

Defined Constants

Theorems

toSet [] =

l. finite (toSet l)

p. all p []

l. all (λx. ) l

x. ¬member x []

p. ¬any p []

l. size (toSet l) length l

l. all (λx. ) l null l

l. toSet l = null l

l. toSet l = l = []

s. finite s toSet (fromSet s) = s

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

l x. member x l x toSet l

h t. toSet (h :: t) = insert h (toSet 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

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

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

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

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

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

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

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. 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

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

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

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

External Type Operators

External Constants

Assumptions

null []

finite

¬

length [] = 0

size = 0

n. 0 n

n. n n

p. p

x. ¬(x )

n. n suc n

(¬) = λp. p

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

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

l. null l l = []

h t. ¬null (h :: t)

() = λp q. p q p

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

x s. ¬(insert x s = )

s x. finite (insert x s) finite s

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

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

t1 t2. ¬(t1 t2) t1 ¬t2

m n. suc m suc n m n

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

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

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

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

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

m n p. m n n p m p

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

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

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

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

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

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

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