Filter
Top Products
98 CHAPTER 12. MATHEMATICAL THEORIES
12.7 Sets
Sets in HOL Light are just predicates, but the usual set operations are defined:
EMPTY = |- EMPTY = (\x. F)
UNIV = |- UNIV = (\x. T)
UNION = |- !s t. s UNION t = {x | x IN s \/ x IN t}
UNIONS = |- !s. UNIONS s = {x | ?u. u IN s /\ x IN u}
INTER = |- !s t. s INTER t = {x | x IN s /\ x IN t}
INTERS = |- !s. INTERS s = {x | !u. u IN s ==> x IN u}
DIFF = |- !s t. s DIFF t = {x | x IN s /\ ~(x IN t)}
INSERT = |- x INSERT s = {y | y IN s \/ (y = x)}
DELETE = |- !s x. s DELETE x = {y | y IN s /\ ~(y = x)}
SUBSET = |- !s t. s SUBSET t = (!x. x IN s ==> x IN t)
PSUBSET = |- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t)
DISJOINT = |- !s t. DISJOINT s t = s INTER t = EMPTY
The parser and printer support set enumerations and set abstractions. Triv-
ial facts of set theory, which are just liftings of first order facts, can be proved
automatically in a tactic framework using SET TAC, e.g.
#prove
(‘x INSERT (s UNION t) = (x INSERT s) UNION (x INSERT t)‘,SET_TAC[]);;
it : thm = |- x INSERT (s UNION t) = x INSERT s UNION x INSERT t
There are quite a lot of such theorems pre-proved. Some more interesting pre-
proved theorems concern the finiteness and cardinality of sets, and in general the
definition of function over finite sets by recursion:
CARD_CLAUSES =
|- (CARD EMPTY = 0) /\
(!x s.
FINITE s
==> (CARD (x INSERT s) =
if x IN s then CARD s else SUC (CARD s)))
HAS_SIZE = |- !s n. s HAS_SIZE n = FINITE s /\ (CARD s = n)
CARD_SUBSET_LE =
|- !a b. FINITE b /\ a SUBSET b /\ CARD b <= CARD a ==> (a = b)
FINITE_RECURSION =
|- !f b.
(!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))