pred_set/Manual/description.tex

1 \chapter{The pred{\und}sets Library}
3 The \ml{pred\_sets} library contains a theory of predicates regarded as sets.
7 representation.  The library was originally written in 1989 by Ton Kalker.  It
9 1992.  The aim of this revision was to make the \ml{pred\_sets} library closely
12 operations on sets.  The present document is itself also adapted from the
17 the theorem-proving support provided by library.  The latter includes
19 operations on finite sets described by enumeration of their elements.  The
37 \noindent The infix function constant \ml{IN} defined here constitutes the
42 The definition of \ml{IN} shown above loosely corresponds to what is usually
51 The definition of \ml{IN} is one of two fundamental theorems in the
52 \ml{pred\_sets} library, from which all others are derived.  The second of
70 The library theory \ml{pred\_sets} is developed entirely on the basis of these
84 The \ml{pred\_sets} library supports generalized set specifications by means of
94 \noindent The function \ml{GSPEC} takes a function \ml{f :\ 'b -> ('a \# bool)}
97 type \ml{'b}. The formal definition of the constant \ml{GSPEC} is given by the
126 \ml{E[x]}.  The constructed set therefore contains all values \ml{E[x]} for
134 {\small\verb!"{!$E$\verb! | !$P$\verb!}"!}.  The built-in \ML\ function
139 The call made to this function extends the \HOL\ parser so that a quotation of
175 \noindent The term {\small\verb!{n | n > N}!} in the definition of \ml{gtr}
178 on only one side of the bar `{\small\verb!|!}'.  The set abstraction
251 The \ml{pred\_sets} library provides proof support for the set abstraction
271 be a variable. The following session illustrates this use of
283 The conversion \ml{SET\_SPEC\_CONV} behaves differently when applied to terms
294 $E$ and $P$. The expression $E$ cannot in general be eliminated in this case,
299 The following session illustrates the form of the theorem proved by
315 \noindent The right-hand sides of \ml{th1} and \ml{th2} could, in principle, be
316 further simplified.  The value of the expression `\ml{(n,m)}' is an injective
329 its free variables, as for example is the case in theorem \ml{th3}.  The
335 \section{The empty and universal sets}
337 The following two constants are defined in the \ml{pred\_sets} library:
352 \noindent The\index{naming conventions!for definitions|(} theorems
384 The infix functions \ml{SUBSET} and \ml{PSUBSET} denote the binary relations of
441 The binary operations of union, intersection and set difference are all defined
442 using the set abstraction notation introduced above in section~\ref{abst}.  The
512 value and removing a value from a set, respectively.  The formal definitions of
525 \noindent The elements of the set denoted by {\small\verb!x INSERT s!} are all
527 not be an element of \ml{s} itself.  The set denoted by
531 {\samepage The membership conditions for sets constructed using \ml{INSERT} and
549 The \ml{pred\_sets} library provides special parser and pretty-printer support
596 The \ml{pred\_sets} library provides a collection of optimized conversions for
601 The sections that follow describe most of these conversions; the remainder are
606 The\index{IN\_CONV@{\ptt IN\_CONV}|(}%
611 set.  The function
653 The following session shows how \ml{IN\_CONV} can be used in practice.
665 \noindent The built-in conversion \ml{num\_EQ\_CONV} is used here to decide
700 The\index{UNION\_CONV@{\ptt UNION\_CONV}|(}%
709 \noindent that can be used to compute the union of two finite sets.  The first
718 {\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!} and another set {\small$s$}. The
760 sequence of elements in the resulting finite set.  The function
775 \noindent The supplied equality conversion in these examples is \ml{NO\_CONV},
795 The\index{INSERT\_CONV@{\ptt INSERT\_CONV}|(}%
858 The\index{DELETE\_CONV@{\ptt DELETE\_CONV}|(}%
891 The following session shows \ml{DELETE\_CONV} in use:
916 \noindent The library contains several built-in theorems about singleton sets.
943 \section{The {\tt CHOICE} and {\tt REST} functions}
945 The \ml{pred\_sets} library contains the definition of a functions \ml{CHOICE}
946 which can be used to select an arbitrary element from a non-empty set. The
962 The library also contains a function \ml{REST}, which is defined in terms of
975 The library contains various built-in theorems about the functions \ml{CHOICE}
980 The {\it image\/} of a function {\small\verb!f:'a->'b!} on a set
1002 \noindent The \ml{pred\_sets} library contains various theorems about
1010 The\index{IMAGE\_CONV@{\ptt IMAGE\_CONV}|(}%
1014 set {\small\verb!{!\tt$t_1$,\dots,$t_n$\verb!}!}.  The function
1021 \noindent is parameterized by two conversions.  The first conversion is
1023 each element {\small$t_1$}, \dots, {\small $t_n$}.  The second parameter is an
1027 The following session shows a simple example of the use of \ml{IMAGE\_CONV} on
1062 The following session illustrates the use of the second parameter to
1085 The \ml{pred\_sets} library contains a few basic definitions and theorems
1131 The library also contains constant specifications for two functions \ml{LINV}
1152 The \ml{pred\_sets} library includes the definition of a predicate called
1153 \ml{FINITE}, which is true of finite sets and false of infinite ones.  The
1172 The \ml{pred\_sets} library contains various built-in theorems that follow from
1188 The above definition of \ml{FINITE} formalizes the notion of a finite set in
1201 \ml{pred\_sets} library.  The following theorem, for example, states that the
1219 The\index{FINITE\_CONV@{\ptt FINITE\_CONV}|(}
1234 The\index{SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|(}
1246 The following session illustrates the use of the tactic \ml{SET\_INDUCT\_TAC}
1276 \noindent The resulting subgoals are easy to prove, given the two basic
1285 The {\it cardinality\/} of a finite set is the number of elements it contains.
1305 The built-in theorems about cardinality are all restricted to finite sets only,
1337 The \ml{pred\_sets} library is loaded into a user's \HOL\ session using the
1339 library loading).  The first action in the load sequence is to update the
1353 up to be autoloaded on demand.  The parser and pretty-printer for the notation
1356 The \ml{pred\_sets} library is then fully loaded into the user's \HOL\ session.
1360 The following session shows how the \ml{pred\_sets} library may be loaded using
1378 library theory \ml{pred\_sets} into a parent of \ml{foo}.  The same effect
1394 \noindent The theory \ml{pred\_sets} is first made the current theory of the
1420 \subsection{The {\tt load\_pred\_sets} function}%
1423 The \ml{pred\_sets} library may in many cases simply be loaded into the system
1444 for set abstractions and finite sets.  The function \ml{load\_pred\_sets} fails