pred_set/Manual/description.tex

37 \noindent The infix function constant \ml{IN} defined here constitutes the
40 one function.
94 \noindent The function \ml{GSPEC} takes a function \ml{f :\ 'b -> ('a \# bool)}
115 above, let \ml{f} in this definition be the function
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
317 function of the values of \ml{n} and \ml{m}, and so by eliminating the
328 {\small\verb!"{!$E$\verb! | !$P$\verb!}"!} will not be an injective function of
552 built-in \ML\ function \ml{define\_finite\_set\_syntax}%
554 (see~\cite{description} for details of this function).  This has the effect of
557 set built up from \ml{EMPTY} by repeatedly using the function \ml{INSERT}:
611 set.  The function
625 function returned by \ml{IN\_CONV conv} is a conversion that decides membership
716 Given an equality conversion \ml{conv}, the function \ml{UNION\_CONV} returns a
745 function \ml{UNION\_CONV} attempts to remove redundant elements in the
760 sequence of elements in the resulting finite set.  The function
864 Like \ml{IN\_CONV} and \ml{INSERT\_CONV}, the function \ml{DELETE\_CONV} takes
947 function \ml{CHOICE} is defined formally by the following constant
958 \ml{CHOICE}, which is therefore an only partially specified function from sets
962 The library also contains a function \ml{REST}, which is defined in terms of
963 the \ml{CHOICE} function as follows
978 \section{Image of a function on a set}
980 The {\it image\/} of a function {\small\verb!f:'a->'b!} on a set
982 \ml{x} in \ml{s}.  In the \ml{pred\_sets} library, the image of a function on a
1004 theorems about the image of a function on sets constructed by the operations of
1013 a conversion for computing the image of a function {\small\verb!f!} on a finite
1014 set {\small\verb!{!\tt$t_1$,\dots,$t_n$\verb!}!}.  The function
1022 expected to compute the result of applying the function {\small\verb!f!} to
1031 result of applying the function {\small\verb!(\x.x+2)!} to a term {\small$t$}.
1043 \noindent This conversion, together with the function \ml{IMAGE\_CONV}, gives a
1086 having to do with mappings between sets.  A function \ml{f:'a->'b} is an {\it
1102 \noindent Likewise, a function \ml{f:'a->'b} is a {\it surjective\/} (onto)
1117 \noindent Finally, a function \ml{f:'a->'b} is a {\it bijection\/} from \ml{s}
1202 image of an injective function on an infinite set is infinite:
1236 second \ML\ function for
1332 involving the cardinality function \ml{CARD} can be found in
1338 function \ml{load\_library} (see the \HOL\ manual for a general description of
1420 \subsection{The {\tt load\_pred\_sets} function}%
1437 load sequence defines an \ML\ function called \ml{load\_pred\_sets} in the
1440 theory, this function can then be used to complete loading of the library.
1444 for set abstractions and finite sets.  The function \ml{load\_pred\_sets} fails
1447 Note that the function \ml{load\_pred\_sets} becomes available upon loading the