Package list-set-thm: Properties of list to set conversions

Information

namelist-set-thm
version1.29
descriptionProperties of list to set conversions
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-02-07
requiresbool
natural
set
list-def
list-thm
list-length
list-set-def
showData.Bool
Data.List
Number.Natural
Set

Files

Theorems

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

Input Type Operators

Input Constants

Assumptions

finite

¬

size = 0

toSet [] =

n. 0 n

n. n n

p. p

n. n suc n

(¬) = λp. p

() = λp. p = λx.

t. ( t) t

t. t t

t. t t

t. ( t) ¬t

() = λp q. p q p

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

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

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

m n. suc m suc n m n

m n p. m n n p m p

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

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)