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

Information

namelist-set-thm
version1.23
descriptionProperties of list to set conversions
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-27
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

T

finite

¬F T

size = 0

toSet [] =

n. 0 n

n. n n

F p. p

n. n suc n

(¬) = λp. p F

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

t. (T t) t

t. t T t

t. T t t

t. (F 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 T T

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