Package list-set-def: Definition of list to set conversions

Information

namelist-set-def
version1.27
descriptionDefinition of list to set conversions
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-12-18
requiresbool
set
list-def
list-length
showData.Bool
Data.List
Number.Natural
Set

Files

Defined Constants

Theorems

toSet [] =

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

length [] = 0

size = 0

F p. p

(¬) = λp. p F

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

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

t. T t t

t. T t t

() = λp q. p q p

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

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

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

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

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