pred_set/Manual/description.tex

5 elements of type \ml{'a}, and the standard operations on sets such as union,
6 intersection, and set difference are appropriately defined for this
11 names for constants and theorems and the same form of definitions for
16 `\ml{pred\_set}'. This document explains the logical basis of this theory and
18 conversions for expanding set specifications and for evaluating various
20 library also provides parser and pretty-printer support for terms that denote
23 \section{Membership and the axioms of set theory}
39 all operators and predicates on sets are ultimately defined in terms of this
47 value.  Since sets and predicates are identical in the \ml{pred\_sets} library,
66 \ml{IN} and the extensionality functions in higher order logic.
68 Once the theorems \ml{EXTENSION} and \ml{SPECIFICATION} have been proved, they
69 provide a complete basis for all further reasoning about sets and membership.
79 set specification: an expression \ml{E[x]} and a predicate \ml{P[x]}. For any
80 such expression and predicate, there is a corresponding set
95 and constructs the set (i.e. predicate of type {\small\verb!'a->bool!}) of all
129 \subsection{Parser and pretty-printer support}\label{abst}
132 \ml{pred\_sets}\linebreak[3] library provides parser and pretty-printer support
149 the expression $E$ and the proposition $P$ (i.e.\ the set $\{x_1,\dots,x_n\}$
150 is the intersection of the set of free variables of $E$ and the set of free
151 variables of $P$).  If there are {\it no\/} variables free in both $E$ and $P$,
223 variables $x_1$, \dots, $x_n$ occur free in both $E$ and $P$.}
244 variables \ml{n} and \ml{m} are bound in the underlying generalized set
294 $E$ and $P$. The expression $E$ cannot in general be eliminated in this case,
315 \noindent The right-hand sides of \ml{th1} and \ml{th2} could, in principle, be
317 function of the values of \ml{n} and \ml{m}, and so by eliminating the
335 \section{The empty and universal sets}
338 {\small\verb!EMPTY:'a->bool!}, which denotes the empty set; and
353 \ml{EMPTY\_DEF} and \ml{UNIV\_DEF} shown above are named according
361 abstractions {\small\verb!"{x | T}"!} and {\small\verb!"{x | F}"!} cannot be
365 about \ml{EMPTY} and \ml{UNIV} are also made available in the theory
376 \noindent That is, nothing is an element of \ml{EMPTY} and everything is an
377 element of \ml{UNIV}. These properties follow directly from the definitions and
378 the theorem \ml{SPECIFICATION}.  Other pre-proved theorems about the empty and
384 The infix functions \ml{SUBSET} and \ml{PSUBSET} denote the binary relations of
385 set inclusion and proper set inclusion, respectively.  These are defined
399 also an element of \ml{t}; and \ml{s} is a proper subset of \ml{t} if it is a
402 Various pre-proved theorems about the subset and proper subset relations are
418 set inclusion and other constants or operations on sets.  For example, there
419 are the following facts about set inclusion and the empty and universal sets:
439 \section{Union, intersection, and set difference}
441 The binary operations of union, intersection and set difference are all defined
461 that occur in both {\small $E$} and {\small $P$}, and the variables \ml{s} and
466 conditions for \ml{UNION}, \ml{INTER} and \ml{DIFF} from the definitions given
485 intersection and set difference; users should almost never have to appeal
487 \ml{UNION}, \ml{INTER} and \ml{DIFF} may be found in chapter~\ref{theorems}.
507 \section{Insertion and deletion of an element}
510 sets) the library contains definitions of two constants \ml{INSERT} and
512 value and removing a value from a set, respectively.  The formal definitions of
531 {\samepage The membership conditions for sets constructed using \ml{INSERT} and
543 theorems about the relationship between the operations \ml{INSERT} and
544 \ml{DELETE} and other relations and operations on sets.  Chapter~\ref{theorems}
547 \subsection{Parser and pretty-printer support}\label{finite}
549 The \ml{pred\_sets} library provides special parser and pretty-printer support
591 with four elements (each a number), two elements (each of which is a pair), and
597 computing the results of operations and predicates on finite sets specified by
681 and \ml{num\_EQ\_CONV} therefore cannot determine if it is equal to any of the
694 fails; but the call to \ml{IN\_CONV} nonetheless succeeds and returns the
718 {\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!} and another set {\small$s$}. The
761 \ml{UNION\_CONV} also checks for and eliminates alpha-equivalent elements.
776 and only the elements of the first set {\small\verb!{1,2,3}!} that are
812 {\small$t$} and {\small$t_i$} are provably equal.\pagebreak[3]
816 the terms {\small$t$} and  {\small$t_i$} are alpha-equivalent, of if
864 Like \ml{IN\_CONV} and \ml{INSERT\_CONV}, the function \ml{DELETE\_CONV} takes
883 {\tt |- ($t_k$ = $t$) = F}, and where for all {\small$t_k$} in
943 \section{The {\tt CHOICE} and {\tt REST} functions}
976 and \ml{REST}; for a full list of these theorems, see chapter~\ref{theorems}.
1005 union and intersection.  For a full list of theorems about \ml{IMAGE}, see
1076 image set containing both {\small\verb!SUC 1!} and {\small\verb!SUC(SUC 0)!}.
1078 and therefore to simplify the resulting set by eliminating one of them from it.
1085 The \ml{pred\_sets} library contains a few basic definitions and theorems
1118 to \ml{t} if it is both injective and surjective:
1128 and \ml{BIJ} available in the library; see chapter~\ref{theorems} for a full
1132 and \ml{RINV}, which yield left and right inverses to injective and surjective
1146 two functions. Furthermore, the definitions of \ml{LINV} and \ml{RINV} shown
1150 \section{Finite and infinite sets}
1153 \ml{FINITE}, which is true of finite sets and false of infinite ones.  The
1167 class of sets that contains the empty set and is closed under the \ml{INSERT}
1184 \noindent These state that the empty set is indeed finite and insertion
1189 logic, and it therefore also determines the form of definition for the
1241 {\small\verb!\!$s$\verb!.!$P$} holds of the empty set and is preserved by the
1277 theorems \ml{FINITE\_EMPTY} and \ml{FINITE\_INSERT} shown in the previous
1342 \ml{pred\_sets}; and the \HOL\ help search path is updated with a pathname to
1352 into \HOL\, and all the theorems in the library (including definitions) are set
1353 up to be autoloaded on demand.  The parser and pretty-printer for the notation
1354 described above in sections~\ref{abst} and~\ref{finite} are then activated, and
1379 could have been achieved (in a fresh session) by first loading the library and
1398 Now, suppose that \ml{foo} has been created as shown above, and the user does
1399 some work in this theory, quits \HOL, and in a later session wishes to load the
1401 \ml{pred\_sets} library and {\it then\/} loading the theory \ml{foo}.
1427 and the current theory is not an ancestor of the theory \ml{pred\_sets}.  In
1428 this case, loading the library can (and will) update the search paths.  But the
1431 can not at this stage be activated; and the \ML\ code in the library can not be
1435 In the situation described above---when the system is not in draft mode and the
1442 functions of the \ml{pred\_sets} library into \HOL\ and activates autoloading
1443 from its theory files.  It also activates the parser and pretty-printer support
1444 for set abstractions and finite sets.  The function \ml{load\_pred\_sets} fails