Package list-set: List to set conversions

Information

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

Files

Defined Constants

Theorems

toSet [] =

l. finite (toSet l)

l. size (toSet l) length l

l. toSet l = l = []

s. finite s toSet (fromSet s) = s

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

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

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

Input Type Operators

Input Constants

Assumptions

T

finite

¬F T

length [] = 0

size = 0

n. 0 n

n. n n

F p. p

n. n suc n

(¬) = λp. p F

() = λP. P ((select) P)

() = λp. p = λx. T

t. (T t) t

t. T t t

t. t T t

t. T t t

t. (F t) ¬t

() = λp q. p q p

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

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

x s. ¬(insert x s = )

s x. finite (insert x s) finite s

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

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

() = λP. q. (x. P x q) q

m n. suc m suc n m n

m n p. m n n p m p

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

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)

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

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