pred_set/Manual/description.tex

\chapter{The pred{\und}sets Library}

The \ml{pred\_sets} library contains a theory of predicates regarded as sets.
A predicate {\small\verb!s:'a->bool!} is considered as a collection or `set' of
elements of type \ml{'a}, and the standard operations on sets such as union,
intersection, and set difference are appropriately defined for this
representation.  The library was originally written in 1989 by Ton Kalker.  It
was completely rewritten by the present author for \HOL\ version 2.01 in early
1992.  The aim of this revision was to make the \ml{pred\_sets} library closely
parallel to the much more developed \HOL\ \ml{sets} library, with the same
names for constants and theorems and the same form of definitions for
operations on sets.  The present document is itself also adapted from the
manual for the \ml{sets} library~\cite{melham}.

There is only one theory in the \ml{pred\_sets} library, namely the theory
`\ml{pred\_set}'. This document explains the logical basis of this theory and
the theorem-proving support provided by library.  The latter includes
conversions for expanding set specifications and for evaluating various
operations on finite sets described by enumeration of their elements.  The
library also provides parser and pretty-printer support for terms that denote
sets.

\section{Membership and the axioms of set theory}

A value \ml{x} is defined to be an element of a set exactly when the
characteristic predicate of the set is true of \ml{x}. Since sets in the
\ml{pred\_sets} library are just represented by their characteristic
predicates, this membership relation is straightforward to define as follows:

\begin{hol}
\index{definition!of IN@of {\ptt IN}}
\index{SPECIFICATION@{\ptt SPECIFICATION}}
\begin{verbatim}
   SPECIFICATION   |- !P x. x IN P = P x
\end{verbatim}\end{hol}

\noindent The infix function constant \ml{IN} defined here constitutes the
basic language for the entire theory of sets in the \ml{pred\_sets} library;
all operators and predicates on sets are ultimately defined in terms of this
one function.

The definition of \ml{IN} shown above loosely corresponds to what is usually
called the {\it axiom of specification\/}\index{axiom of specification} for
sets (hence the name \ml{SPECIFICATION}). This axiom states that sets can be
constructed from predicates that describe or `specify' their elements. A value
is an element of the constructed set exactly when the predicate is true of that
value.  Since sets and predicates are identical in the \ml{pred\_sets} library,
we can simply say that \ml{x} is in the `set' \ml{P} exactly when
{\small\verb!P x!} holds.

The definition of \ml{IN} is one of two fundamental theorems in the
\ml{pred\_sets} library, from which all others are derived.  The second of
these fundamental theorems states what is usually called the {\it axiom of
extension\/}\index{axiom of extension} for sets.  This is not, of course,
literally an {\it axiom\/} of the \ml{pred\_sets} theory, but rather a theorem
derived by proof:

\begin{hol}
\index{EXTENSION@{\ptt EXTENSION}}
\begin{verbatim}
   EXTENSION   |- !s t. (s = t) <=> (!x. x IN s = x IN t)
\end{verbatim}\end{hol}

\noindent \ml{EXTENSION} states that two sets are equal exactly when they have
the same elements.  This follows directly from the definition of the constant
\ml{IN} and the extensionality functions in higher order logic.

Once the theorems \ml{EXTENSION} and \ml{SPECIFICATION} have been proved, they
provide a complete basis for all further reasoning about sets and membership.
The library theory \ml{pred\_sets} is developed entirely on the basis of these
two `axioms' of set theory.

\section{Generalized set specifications}

In addition to the basic constant \ml{IN}, which allows one to regard a
predicate as the set of all values that satisfy it, the \ml{pred\_sets} library
also provides a general way of constructing sets by describing or specifying
their elements.  Roughly speaking, there are two components to a generalized
set specification: an expression \ml{E[x]} and a predicate \ml{P[x]}. For any
such expression and predicate, there is a corresponding set
{\small\verb!{E[x] | P[x]}!}, the set of all values {\small\verb!E[x]!} for
which {\small\verb!P[x]!} holds.

The \ml{pred\_sets} library supports generalized set specifications by means of
the constant:

\begin{hol}
\index{GSPEC@{\ptt GSPEC}}
\begin{verbatim}
   GSPEC : ('b -> ('a # bool)) -> 'a -> bool
\end{verbatim}
\end{hol}

\noindent The function \ml{GSPEC} takes a function \ml{f :\ 'b -> ('a \# bool)}
and constructs the set (i.e. predicate of type {\small\verb!'a->bool!}) of all
values \ml{FST(f x)} for which \ml{SND(f x)} holds, for some value \ml{x} of
type \ml{'b}. The formal definition of the constant \ml{GSPEC} is given by the
following constant specification:

\begin{hol}
\index{definition!of GSPEC@of {\ptt GSPEC}}
\index{GSPECIFICATION@{\ptt GSPECIFICATION}}
\begin{verbatim}
   GSPECIFICATION   |- !f v. v IN (GSPEC f) = (?x. v,T = f x)
\end{verbatim}
\end{hol}

\noindent This theorem is analogous to the axiom of specification\index{axiom
of specification!for generalized set specifications} for \ml{IN}.
This states that a value \ml{v} is an element of the set specified by
\ml{f} exactly when \ml{v} is one of the values of \ml{FST(f x)} for which
\ml{SND(f x)} is true.

To see how this supports the notion of generalized set specification described
above, let \ml{f} in this definition be the function
{\small\verb!\x.E[x],P[x]!}.  With a little simplification, we would then have:

\begin{hol}
\begin{verbatim}
   |- !v. v IN (GSPEC \x.E[x],P[x]) = ?x. (v = E[x]) /\ P[x]
\end{verbatim}
\end{hol}

\noindent That is, a value \ml{v} is in the set constructed by \ml{GSPEC}
exactly when for some \ml{x} for which \ml{P[x]}, the value \ml{v} is equal to
\ml{E[x]}.  The constructed set therefore contains all values \ml{E[x]} for
which \ml{P[x]} holds.

\subsection{Parser and pretty-printer support}\label{abst}

To facilitate the use of sets constructed by generalized set specification, the
\ml{pred\_sets}\linebreak[3] library provides parser and pretty-printer support
for set abstractions expressed by the notation
{\small\verb!"{!$E$\verb! | !$P$\verb!}"!}.  The built-in \ML\ function
\ml{define\_set\_abstraction\_syntax}%
\index{define\_set\_abstraction\_syntax@{\ptt
define\_set\_abstraction\_syntax}} (see the manual~\cite{description} for
details) is used to introduce this \mbox{notation} when the library is loaded.
The call made to this function extends the \HOL\ parser so that a quotation of
the form {\small\verb!"{!$E$\verb! | !$P$\verb!}"!} {\samepage parses to:

\begin{hol}
\begin{alltt}
   GSPEC (\bk(\m{x\sb{1}},\(\dots\),\m{x\sb{n}}).(\(E\),\(P\)))
\end{alltt}
\end{hol}

\noindent where $x_1$, \dots, $x_n$ are} the variables that occur free in both
the expression $E$ and the proposition $P$ (i.e.\ the set $\{x_1,\dots,x_n\}$
is the intersection of the set of free variables of $E$ and the set of free
variables of $P$).  If there are {\it no\/} variables free in both $E$ and $P$,
then a parser error is generated.  When the
\ml{print\_set}\index{print\_set@{\ptt print\_set} (flag)} flag is \ml{true},
the quotation pretty-printer inverts this transformation.

A simple example of this set abstraction notation is shown in the following
\HOL\ session, in which it is assumed that the \ml{pred\_sets} library has
already been loaded. (See section~\ref{using} for a description of how
\ml{pred\_sets} is loaded.)

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#let gtr = new_definition (`gtr`, "gtr N = {n | n > N}");;
gtr = |- !N. gtr N = {n | n > N}

#set_flag (`print_set`,false);;
true : bool

#"{n | n > N}";;
"GSPEC(\n. (n,n > N))" : term
\end{verbatim}\end{session}


\noindent The term {\small\verb!{n | n > N}!} in the definition of \ml{gtr}
denotes the set of all natural numbers greater than \ml{N}.  It is important to
note that the variable \ml{N} is a free variable in this term, since it occurs
on only one side of the bar `{\small\verb!|!}'.  The set abstraction
{\small\verb!{n | n > N}!} therefore parses to the generalized set
specification

\begin{hol}
\begin{verbatim}
   GSPEC(\n. (n,n > N))
\end{verbatim}\end{hol}

\noindent This is what gives this set abstraction the (presumably intended)
interpretation `the set of all \ml{n} greater than \ml{N}'.  By contrast, the
term

\begin{hol}
\begin{verbatim}
   GSPEC(\(n,N). (n,n > N))
\end{verbatim}\end{hol}

\noindent denotes the set of all numbers \ml{n} greater than some number
\ml{N}---i.e., the set $\{\ml{1},\ml{2},\ml{3},\dots\}$.  This is {\it not\/}
the default interpretation of the parser, which constructs a generalized set
specification that binds the variable \ml{n} only. Note that only
default\pagebreak[3] interpretations are pretty-printed using the {\samepage
set abstraction notation:

\begin{session}
\begin{verbatim}
#set_flag(`print_set`,true);;
false : bool

#"GSPEC (\n. (n,n>N))";;
"{n | n > N}" : term

#"GSPEC (\(n,N). (n,n>N))";;
"GSPEC(\(n,N). (n,n > N))" : term
\end{verbatim}\end{session}

\noindent That is, a term of the form:

\begin{hol}
\begin{alltt}
   GSPEC (\bk(\m{x\sb{1}},\(\dots\),\m{x\sb{n}}).(\(E\),\(P\)))
\end{alltt}\end{hol}

\noindent prints as {\small\verb!"{!$E$\verb! | !$P$\verb!}"!} only if the
variables $x_1$, \dots, $x_n$ occur free in both $E$ and $P$.}


In general, the expression $E$ in a set abstraction
{\small\verb!"{!$E$\verb! | !$P$\verb!}"!} need not be just a variable.
Consider, for example, the following \HOL\ session:

\begin{session}
\begin{verbatim}
#let S = "{(n,m) | n < m}";;
S = "{(n,m) | n < m}" : term

#set_flag(`print_set`,false);;
true : bool

#"{(n,m) | n < m}";;
"GSPEC(\(n,m). ((n,m),n < m))" : term
\end{verbatim}\end{session}

\noindent Here, a set abstraction is used to construct the set of all pairs of
numbers \ml{(n,m)} for which \ml{n} is less than \ml{m}.  Note that both
variables \ml{n} and \ml{m} are bound in the underlying generalized set
specification.

\subsection{Theorem-proving support}

\index{SET\_SPEC\_CONV@{\ptt SET\_SPEC\_CONV}|(}
\index{conversions!SET\_SPEC\_CONV@{\ptt SET\_SPEC\_CONV}|(}
The \ml{pred\_sets} library provides proof support for the set abstraction
notation in the form of a conversion called \ml{SET\_SPEC\_CONV}.  This
conversion implements the axiom of specification for set abstractions.%
\index{axiom of specification!for set abstractions}
When $v$ is a variable, evaluating:

\begin{hol}\def\m#1{\mbox{\small$#1$}}
\begin{alltt}
   SET_SPEC_CONV "\m{t} IN \lb\m{v} \vb \m{P}\rb";;
\end{alltt}\end{hol}

\noindent returns the theorem:

\begin{hol}\def\m#1{\mbox{\small$#1$}}
\begin{alltt}
   {\vb}- \m{t} IN \lb\m{v} \vb \m{P}\rb = \m{P[t/v]}
\end{alltt}\end{hol}

\noindent This states that $t$ is an element of the set of all $v$ such that
$P$ exactly when $P[t/v]$ holds. Note that, in general, the term $t$ need not
be a variable. The following session illustrates this use of
\ml{SET\_SPEC\_CONV} for membership {\samepage in a particular set abstraction:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#SET_SPEC_CONV ``12 IN {n | n > N}``;
|- 12 IN {n | n > N} = 12 > N
\end{verbatim}\end{session}}

\pagebreak[3]

The conversion \ml{SET\_SPEC\_CONV} behaves differently when applied to terms
of the form {\small\verb!"!$t$\verb! IN {!$E$\verb! | !$P$\verb!}"!} where
{\small $E$} is not a variable.  Applying the conversion to a term of this kind
yields the theorem:

\begin{hol}\def\m#1{\mbox{\small$#1$}}
\begin{alltt}
   {\vb}- \m{t} IN \lb\m{E} \vb \m{P}\rb = ?\m{x\sb{1}\dots x\sb{n}}. (\m{t} = \m{E}) /\bk \m{P}
\end{alltt}\end{hol}

\noindent where $x_1$, \dots, $x_n$ are the variables that occur free in both
$E$ and $P$. The expression $E$ cannot in general be eliminated in this case,
as it can by the substitution $P[t/v]$ when $E$ is just a variable $v$.

\pagebreak[3]

The following session illustrates the form of the theorem proved by
\ml{SET\_SPEC\_CONV} for the second type of input term discussed above:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#let th1 = SET_SPEC_CONV "p IN {(n,m) | n < m}";;
th1 = |- p IN {(n,m) | n < m} = (?n m. (p = n,m) /\ n < m)

#let th2 = SET_SPEC_CONV "(a,b) IN {(n,m) | n < m}";;
th2 = |- (a,b) IN {(n,m) | n < m} = (?n m. (a,b = n,m) /\ n < m)

#let th3 = SET_SPEC_CONV "a IN {n + m | n < m}";;
th3 = |- a IN {n + m | n < m} = (?n m. (a = n + m) /\ n < m)
\end{verbatim}\end{session}

\noindent The right-hand sides of \ml{th1} and \ml{th2} could, in principle, be
further simplified.  The value of the expression `\ml{(n,m)}' is an injective
function of the values of \ml{n} and \ml{m}, and so by eliminating the
existential quantifiers these two theorems could be simplified to:

\begin{hol}
\begin{verbatim}
   th1    |- p IN {(n,m) | n < m} = (FST p < SND p)

   th2    |- (a,b) IN {(n,m) | n < m} = (a < b)
\end{verbatim}\end{hol}

\noindent But in general the value of {\small $E$} in a set abstraction
{\small\verb!"{!$E$\verb! | !$P$\verb!}"!} will not be an injective function of
its free variables, as for example is the case in theorem \ml{th3}.  The
conversion \ml{SET\_SPEC\_CONV} therefore attempts no further simplification of
its result than is described above for the general
case.\index{SET\_SPEC\_CONV@{\ptt SET\_SPEC\_CONV}|)}%
\index{conversions!SET\_SPEC\_CONV@{\ptt SET\_SPEC\_CONV}|)}

\section{The empty and universal sets}

The following two constants are defined in the \ml{pred\_sets} library:
{\small\verb!EMPTY:'a->bool!}, which denotes the empty set; and
{\small\verb!UNIV:'a->bool!}, which denotes the universe, or set of all values
of type \ml{'a}.{\samepage  These constants are defined formally as follows:

\begin{hol}
\index{definition!of EMPTY@of {\ptt EMPTY}}
\index{EMPTY\_DEF@{\ptt EMPTY\_DEF}}
\index{definition!of UNIV@of {\ptt UNIV}}
\index{UNIV\_DEF@{\ptt UNIV\_DEF}}
\begin{verbatim}
  EMPTY_DEF  |- EMPTY = \x. F
  UNIV_DEF   |- UNIV  = \x. T
\end{verbatim}\end{hol}

\noindent The\index{naming conventions!for definitions|(} theorems
\ml{EMPTY\_DEF} and \ml{UNIV\_DEF} shown above are named according
to the general convention that all definitions in the \ml{pred\_sets} library
are given names ending
in `{\small\verb!_DEF!}'.\index{naming conventions!for definitions|)}}

\pagebreak[3]

Note that because of the restriction on free variables discussed above, the set
abstractions {\small\verb!"{x | T}"!} and {\small\verb!"{x | F}"!} cannot be
used in these definitions; the more primitive form of set construction given by
the above lambda-abstractions must be used instead.  But users of the library
will never need to appeal to these definitions, since the following theorems
about \ml{EMPTY} and \ml{UNIV} are also made available in the theory
\ml{pred\_sets}:

\begin{hol}
\index{NOT\_IN\_EMPTY@{\ptt NOT\_IN\_EMPTY}}
\index{IN\_UNIV@{\ptt IN\_UNIV}}
\begin{verbatim}
   NOT_IN_EMPTY  |- !x. ~x IN EMPTY
   IN_UNIV       |- !x. x IN UNIV
\end{verbatim}\end{hol}

\noindent That is, nothing is an element of \ml{EMPTY} and everything is an
element of \ml{UNIV}. These properties follow directly from the definitions and
the theorem \ml{SPECIFICATION}.  Other pre-proved theorems about the empty and
universal sets are also available in the library; see chapter~\ref{theorems}
for a complete list.

\section{Set inclusion}

The infix functions \ml{SUBSET} and \ml{PSUBSET} denote the binary relations of
set inclusion and proper set inclusion, respectively.  These are defined
formally in the obvious way:

\begin{hol}
\index{definition!of SUBSET@of {\ptt SUBSET}}
\index{SUBSET\_DEF@{\ptt SUBSET\_DEF}}
\index{definition!of PSUBSET@of {\ptt PSUBSET}}
\index{PSUBSET\_DEF@{\ptt PSUBSET\_DEF}}
\begin{verbatim}
  SUBSET_DEF   |- !s t. s SUBSET t = (!x. x IN s ==> x IN t)
  PSUBSET_DEF  |- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t)
\end{verbatim}\end{hol}

\noindent That is, \ml{s} is a subset of \ml{t} if every element of \ml{s} is
also an element of \ml{t}; and \ml{s} is a proper subset of \ml{t} if it is a
subset of \ml{t} but not equal to \ml{t}.

Various pre-proved theorems about the subset and proper subset relations are
supplied by the \ml{pred\_sets} library.  For example, the fact that
\ml{SUBSET} is a partial order is stated by the three built-in theorems shown
below.

\begin{hol}
\index{SUBSET\_TRANS@{\ptt SUBSET\_TRANS}}
\index{SUBSET\_REFL@{\ptt SUBSET\_REFL}}
\index{SUBSET\_ANTISYM@{\ptt SUBSET\_ANTISYM}}
\begin{verbatim}
  SUBSET_REFL     |- !s. s SUBSET s
  SUBSET_TRANS    |- !s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u
  SUBSET_ANTISYM  |- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)
\end{verbatim}\end{hol}

\noindent Also provided are built-in theorems about the relationship between
set inclusion and other constants or operations on sets.  For example, there
are the following facts about set inclusion and the empty and universal sets:

\begin{hol}
\index{EMPTY\_SUBSET@{\ptt EMPTY\_SUBSET}}
\index{SUBSET\_UNIV@{\ptt SUBSET\_UNIV}}
\index{NOT\_PSUBSET\_EMPTY@{\ptt NOT\_PSUBSET\_EMPTY}}
\index{NOT\_UNIV\_PSUBSET@{\ptt NOT\_UNIV\_PSUBSET}}
\begin{verbatim}
  EMPTY_SUBSET       |- !s. {} SUBSET s
  SUBSET_UNIV        |- !s. s SUBSET UNIV
  NOT_PSUBSET_EMPTY  |- !s. ~s PSUBSET {}
  NOT_UNIV_PSUBSET   |- !s. ~UNIV PSUBSET s
\end{verbatim}\end{hol}

\noindent As\index{naming conventions!for theorems generally|(} these examples
illustrate, the names of theorems in the \ml{pred\_sets} library are generally
constructed from the names of the constants they contain.  Furthermore, the
ordering of elements in the name of a theorem attempts to reflect the content
of the theorem itself.\index{naming conventions!for theorems generally|)}

\section{Union, intersection, and set difference}

The binary operations of union, intersection and set difference are all defined
using the set abstraction notation introduced above in section~\ref{abst}.  The
formal definitions are:

\begin{hol}
\index{definition!of UNION@of {\ptt UNION}}
\index{UNION\_DEF@{\ptt UNION\_DEF}}
\index{definition!of INTER@of {\ptt INTER}}
\index{INTER\_DEF@{\ptt INTER\_DEF}}
\index{definition!of DIFF@of {\ptt DIFF}}
\index{DIFF\_DEF@{\ptt DIFF\_DEF}}
\begin{verbatim}
  UNION_DEF    |- !s t. s UNION t = {x | x IN s \/ x IN t}
  INTER_DEF    |- !s t. s INTER t = {x | x IN s /\ x IN t}
  DIFF_DEF     |- !s t. s DIFF t = {x | x IN s /\ ~x IN t}
\end{verbatim}\end{hol}

\noindent These definitions illustrate the practical utility of the scheme for
variable binding in set abstractions discussed above in section~\ref{abst}.  An
abstraction {\small\verb!"{!$E$\verb! | !$P$\verb!}"!} binds only the variables
that occur in both {\small $E$} and {\small $P$}, and the variables \ml{s} and
\ml{t} in the set abstractions shown above may therefore be made parameters to
the sets\pagebreak[3] constructed by them.

Using \ml{SET\_EQ\_CONV}, it is trivial to derive the following membership
conditions for \ml{UNION}, \ml{INTER} and \ml{DIFF} from the definitions given
above. As\index{naming conventions!for membership conditions|(} a general rule,
theorems stating membership conditions of the kind illustrated by these
examples are given names of the form {\small\verb!IN_!$\langle\hbox{\it
constant\/}\rangle$} ending in the name of the operation used to construct the
set in question.\index{naming conventions!for membership conditions|)}

\begin{hol}
\index{IN\_UNION@{\ptt IN\_UNION}}
\index{IN\_INTER@{\ptt IN\_INTER}}
\index{IN\_DIFF@{\ptt IN\_DIFF}}
\begin{verbatim}
   IN_UNION  |- !s t x. x IN (s UNION t) = x IN s \/ x IN t
   IN_INTER  |- !s t x. x IN (s INTER t) = x IN s /\ x IN t
   IN_DIFF   |- !s t x. x IN (s DIFF t) = x IN s /\ ~x IN t
\end{verbatim}\end{hol}

\noindent These theorems, which are saved in the library under the names
indicated above, may in practice be used as the defining properties of union,
intersection and set difference; users should almost never have to appeal
directly to the definitions of these operations.  Other built-in theorems about
\ml{UNION}, \ml{INTER} and \ml{DIFF} may be found in chapter~\ref{theorems}.

\section{Disjoint sets}

Two sets are {\it disjoint\/} if they have no elements in common. This concept
is formalized in the \ml{pred\_sets} library by the constant \ml{DISJOINT}, the
definition of which is:

\begin{hol}
\index{definition!of DISJOINT@of {\ptt DISJOINT}}
\index{DISJOINT\_DEF@{\ptt DISJOINT\_DEF}}
\begin{verbatim}
   DISJOINT_DEF  |- !s t. DISJOINT s t = (s INTER t = {})
\end{verbatim}\end{hol}

\noindent At present, there are relatively few pre-proved theorems about the
\ml{DISJOINT} relation in the library. But see chapter~\ref{theorems} for the
few theorems about \ml{DISJOINT} that are in fact available in the
\ml{pred\_sets} library.

\section{Insertion and deletion of an element}

To aid in the construction of particular sets of values (especially finite
sets) the library contains definitions of two constants \ml{INSERT} and
\ml{DELETE}.  These denote the operations of augmenting a set with a given
value and removing a value from a set, respectively.  The formal definitions of
these operations are:

\begin{hol}
\index{definition!of INSERT@of {\ptt INSERT}}
\index{INSERT\_DEF@{\ptt INSERT\_DEF}}
\index{definition!of DELETE@of {\ptt DELETE}}
\index{DELETE\_DEF@{\ptt DELETE\_DEF}}
\begin{verbatim}
   INSERT_DEF  |- !x s. x INSERT s = {y | (y = x) \/ y IN s}
   DELETE_DEF  |- !s x. s DELETE x = s DIFF (INSERT x EMPTY)
\end{verbatim}\end{hol}

\noindent The elements of the set denoted by {\small\verb!x INSERT s!} are all
the elements of the set \ml{s} together with the value \ml{x}, which may or may
not be an element of \ml{s} itself.  The set denoted by
{\small\verb!s DELETE x!} contains all the elements of \ml{s}
except the value \ml{x}.

{\samepage The membership conditions for sets constructed using \ml{INSERT} and
\ml{DELETE} are given by the following pre-proved theorems:

\begin{hol}
\index{IN\_INSERT@{\ptt IN\_INSERT}}
\index{IN\_DELETE@{\ptt IN\_DELETE}}
\begin{verbatim}
   IN_INSERT  |- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s
   IN_DELETE  |- !s x y. x IN (s DELETE y) = x IN s /\ ~(x = y)
\end{verbatim}\end{hol}

\noindent In addition, the library} contains a substantial collection of
theorems about the relationship between the operations \ml{INSERT} and
\ml{DELETE} and other relations and operations on sets.  Chapter~\ref{theorems}
gives a complete list of these theorems.

\subsection{Parser and pretty-printer support}\label{finite}

The \ml{pred\_sets} library provides special parser and pretty-printer support
for finite sets that are constructed by enumeration of their elements. This
notation is introduced by a call made when the library is loaded to the
built-in \ML\ function \ml{define\_finite\_set\_syntax}%
\index{define\_finite\_set\_syntax@{\ptt define\_finite\_set\_syntax}}
(see~\cite{description} for details of this function).  This has the effect of
extending the \HOL\ parser so that a quotation of the form
{\small\verb!"{!\tt$t_1$,$t_2$,\dots,$t_n$\verb!}"!} parses to the following
set built up from \ml{EMPTY} by repeatedly using the function \ml{INSERT}:

\begin{hol}
\begin{alltt}
   INSERT \m{t\sb{1}} (INSERT \m{t\sb{2}} \dots (INSERT \m{t\sb{n}} EMPTY)\dots)
\end{alltt}\end{hol}

\noindent Note that the quotation {\small\verb!"{}"!} just parses to the
constant \ml{EMPTY}. When the
\ml{print\_set}\index{print\_set@{\ptt print\_set} (flag)}
flag is \ml{true}, the \HOL\ pretty-printer for terms inverts this
transformation.

Users should note that care must be taken with regard to the precedence of
comma in a context {\small\verb!"{!\dots\verb!}"!}, as the following session
illustrates:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#set_flag(`print_set`,false);;
true : bool

#"{1,2,3,4}";;
"1 INSERT (2 INSERT (3 INSERT (4 INSERT EMPTY)))" : term

#"{(1,2),(3,4)}";;
"(1,2) INSERT ((3,4) INSERT EMPTY)" : term

#"{((1,2),(3,4))}";;
"((1,2),3,4) INSERT EMPTY" : term
\end{verbatim}\end{session}

\noindent Different grouping by means of enclosing parentheses has given sets
with four elements (each a number), two elements (each of which is a pair), and
one element (a pair of pairs) respectively.

\subsection{Conversions for enumerated finite sets}

The \ml{pred\_sets} library provides a collection of optimized conversions for
computing the results of operations and predicates on finite sets specified by
enumeration of their elements.  All these conversions, the current
implementations of which are somewhat experimental, are designed to work only
for finite sets of the form {\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!}.
The sections that follow describe most of these conversions; the remainder are
discussed in later sections of this manual.

\subsubsection{Membership}\label{inconv}

The\index{IN\_CONV@{\ptt IN\_CONV}|(}%
\index{conversions!IN\_CONV@{\ptt IN\_CONV}|(} most basic
conversion for finite sets is a decision procedure for membership called
\ml{IN\_CONV}.  In general, a way of deciding equality of elements is needed in
order to determine whether a given value is an element of a particular finite
set.  The function

\begin{hol}
\begin{verbatim}
   IN_CONV : conv -> conv
\end{verbatim}\end{hol}

\noindent must therefore be supplied with a conversion that implements a
decision procedure for equality of set elements.  It is assumed that this
conversion will map equations {\small\tt"$e_1$ = $e_2$"} between elements of a
base type \ml{ty} to the theorem {\small\tt |- ($e_1$ = $e_2$) = T} or to the
theorem {\small\tt |- ($e_1$ = $e_2$) = F}, as appropriate.

If \ml{conv} is an equality conversion of the kind described above, then the
function returned by \ml{IN\_CONV conv} is a conversion that decides membership
in finite sets of values of the base type \ml{ty}.  In particular, a call:

\begin{hol}
\begin{alltt}
   IN\_CONV conv "\m{t} IN \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb"
\end{alltt}\end{hol}

\noindent returns the theorem

\begin{hol}
\begin{alltt}
   |- \m{t} IN \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb = T
\end{alltt}\end{hol}

\noindent if the term $t$ is alpha-equivalent to some term $t_i$ or if the
supplied conversion \ml{conv} proves {\tt |- ($t$ = $t_i$) = T} for some $i$
where $1 \leq i \leq n$.  If, on the other hand \ml{conv} proves the theorem
{\tt |- ($t$ = $t_i$) = F} for all $i$ where $1 \leq i \leq n$, then the result
is the theorem

\begin{hol}
\begin{alltt}
   |- \m{t} IN \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb = F
\end{alltt}\end{hol}

\noindent In all other cases, the call to \ml{IN\_CONV} shown above will fail.

The following session shows how \ml{IN\_CONV} can be used in practice.

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#IN_CONV num_EQ_CONV "1 IN {2,1,3}";;
|- 1 IN {2,1,3} = T

#IN_CONV num_EQ_CONV "4 IN {2,1,3}";;
|- 4 IN {2,1,3} = F
\end{verbatim}\end{session}

\noindent The built-in conversion \ml{num\_EQ\_CONV} is used here to decide
equality of the natural numbers involved in the membership
assertions\pagebreak[3] being proved.

An example in which \ml{IN\_CONV} fails is the following:

\begin{session}
\begin{verbatim}
#IN_CONV num_EQ_CONV "x IN {1,2,3}";;
evaluation failed     IN_CONV

#num_EQ_CONV "x = 1";;
evaluation failed     num_EQ_CONV
\end{verbatim}\end{session}

\noindent Failure occurs in this case because the term \ml{x} is a variable,
and \ml{num\_EQ\_CONV} therefore cannot determine if it is equal to any of the
set elements \ml{1}, \ml{2} or \ml{3}.  Note, however, that the supplied
conversion is not required to prove anything if the value being tested for
membership happens to be syntactically identical to an element of the given
set:

\begin{session}
\begin{verbatim}
#IN_CONV NO_CONV "x IN {1,x,3}";;
|- x IN {1,x,3} = T
\end{verbatim}\end{session}

\noindent In this case, the supplied conversion, namely \ml{NO\_CONV}, always
fails; but the call to \ml{IN\_CONV} nonetheless succeeds and returns the
appropriate result.\index{IN\_CONV@{\ptt IN\_CONV}|)}%
\index{conversions!IN\_CONV@{\ptt IN\_CONV}|)}

\subsubsection{Union}

The\index{UNION\_CONV@{\ptt UNION\_CONV}|(}%
\index{conversions!UNION\_CONV@{\ptt UNION\_CONV}|(}
\ml{pred\_sets} library contains a conversion

\begin{hol}
\begin{verbatim}
   UNION_CONV : conv -> conv
\end{verbatim}\end{hol}

\noindent that can be used to compute the union of two finite sets.  The first
argument to \ml{UNION\_CONV} (i.e.\ the conversion argument) is expected to be
an equality conversion of the same kind required as an argument by
\ml{IN\_CONV} (see section~\ref{inconv}).  As will be seen below, this
conversion is used by \ml{UNION\_CONV} to simplify the set that it computes as
the result of taking the union of two finite sets.

Given an equality conversion \ml{conv}, the function \ml{UNION\_CONV} returns a
conversion that computes the union of a finite set
{\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!} and another set {\small$s$}. The
second set {\small$s$} in fact need not be finite.  Ignoring, for the moment,
the possible simplification done using the supplied conversion \ml{conv}, a
call:

\begin{hol}\begin{alltt}
   UNION\_CONV conv "\lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb UNION \m{s}"
\end{alltt}\end{hol}

\noindent just returns the theorem

\begin{hol}\begin{alltt}
   |- \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb UNION \m{s} = \m{t\sb{1}} INSERT (\m{\dots} (\m{t\sb{n}} INSERT \m{s})\m{\dots})
\end{alltt}\end{hol}

\noindent That is, \ml{UNION\_CONV} computes the required union as a repeated
insertion of values into the set {\small$s$}.\pagebreak[3] When {\small$s$} is
a finite set of the form {\small\verb!"{!\tt$u_1$,\dots,$u_m$\verb!}"!}, the
{\samepage resulting theorem will have the form shown below.

\begin{hol}
\begin{alltt}
   |- \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb UNION \lb\m{u\sb{1}},\dots,\m{u\sb{m}}\rb = \lb\m{t\sb{1}},\m{\dots},\m{t\sb{n}},\m{u\sb{1}},\m{\dots},\m{u\sb{m}}\rb
\end{alltt}\end{hol}

\noindent When computing} theorems of this form (i.e.\ when the second set of
the union is a finite set {\small\verb!"{!\tt$u_1$,\dots,$u_m$\verb!}"!}) the
function \ml{UNION\_CONV} attempts to remove redundant elements in the
resulting set using the supplied equality conversion \ml{conv}.  In particular,
if \ml{conv} is able to prove that some element {\small$t_i$} of
{\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!} is equal to any element
{\small$u_j$} of {\small\verb!"{!\tt$u_1$,\dots,$u_m$\verb!}"!}, that is if the
conversion \ml{conv} maps the term {\small\verb!"!$t_i$\verb! = !$u_j$\verb!"!}
to the theorem {\small\verb!|- (!$t_i$\verb! = !$u_j$\verb!) = T!}, then the
resulting theorem will be

\begin{hol}
\begin{alltt}
   |- \lb\m{t\sb{1}},\dots\m{t\sb{i}},\dots,\m{t\sb{n}}\rb UNION \lb\m{u\sb{1}},\dots,\m{u\sb{j}},\dots,\m{u\sb{m}}\rb = \lb\m{t\sb{1}},\m{\dots},\m{t\sb{n}},\m{u\sb{1}},\dots,\m{u\sb{j}},\dots,\m{u\sb{m}}\rb
\end{alltt}\end{hol}

\noindent That is, the redundant term \m{t_i} will be removed from the initial
sequence of elements in the resulting finite set.  The function
\ml{UNION\_CONV} also checks for and eliminates alpha-equivalent elements.

Some examples of \ml{UNION\_CONV} in use are shown in the following \HOL\
session:

\begin{session}
\begin{verbatim}
#UNION_CONV NO_CONV "{1,2,3} UNION {4,5,6}";;
|- {1,2,3} UNION {4,5,6} = {1,2,3,4,5,6}

#UNION_CONV NO_CONV "{1,2,3} UNION {3,2,SUC 0}";;
|- {1,2,3} UNION {3,2,SUC 0} = {1,3,2,SUC 0}
\end{verbatim}\end{session}

\noindent The supplied equality conversion in these examples is \ml{NO\_CONV},
and only the elements of the first set {\small\verb!{1,2,3}!} that are
redundant by virtue of being alpha-equivalent to elements of the second set
are eliminated from the resulting set.  An example in which the equality
conversion is actually used is:

\begin{session}
\begin{verbatim}
#UNION_CONV num_EQ_CONV "{1,2,3} UNION {3,2,SUC 0}";;
|- {1,2,3} UNION {3,2,SUC 0} = {3,2,SUC 0}
\end{verbatim}\end{session}

\noindent In this case, \ml{num\_EQ\_CONV} is used to prove that
{\small\verb!1!} is equal to {\small\verb!SUC 0!}, so that the resulting union
is the set {\small\verb!"{3,2,SUC 0}"!}, rather than
{\small\verb!"{1,3,2,SUC 0}!"}.\index{UNION\_CONV@{\ptt UNION\_CONV}|)}%
\index{conversions!UNION\_CONV@{\ptt UNION\_CONV}|)}

\subsubsection{Insertion}

The\index{INSERT\_CONV@{\ptt INSERT\_CONV}|(}%
\index{conversions!INSERT\_CONV@{\ptt INSERT\_CONV}|(}
conversion \ml{INSERT\_CONV} performs the following reduction
on finite sets:

\begin{hol}
\begin{alltt}
   {\normalsize\rm reduce}\quad"\m{t} INSERT \lb\m{t\sb{1}},\dots,\m{t\sb{i}},\dots,\m{t\sb{n}}\rb"\quad\m{\normalsize\rm to}\quad"\lb\m{t\sb{1}},\dots,\m{t\sb{i}},\dots,\m{t\sb{n}}\rb"
\end{alltt}\end{hol}

\noindent if a supplied equality conversion can prove
{\small\verb!|- (!$t$\verb! = !$t_i$\verb!) = T!}.  Since the
enumerated set notation
{\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!} is just a parser-supported
abbreviation (see section~\ref{finite}), this is equivalent to reducing the set
{\small\verb!"{!\tt$t$,$t_1$,\dots,$t_i$,\dots,$t_n$\verb!}"!} to
{\small\verb!"{!\tt$t_1$,\dots,$t_i$,\dots,$t_n$\verb!}"!} when the terms
{\small$t$} and {\small$t_i$} are provably equal.\pagebreak[3]

More specifically, if for some {\small$t_i$} in
{\small\verb!{!$t_1$\verb!,!\dots\verb!,!$t_n$\verb!}!},
the terms {\small$t$} and  {\small$t_i$} are alpha-equivalent, of if
the conversion \ml{conv} maps {\small\verb!"!$t$\verb! = !$t_i$\verb!"!} to
the theorem {\small\verb!|- (!$t$\verb! = !$t_i$\verb!) = T!}, then the call:

\begin{hol}
\begin{alltt}
   INSERT\_CONV conv "\m{t} INSERT \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb";;
\end{alltt}\end{hol}

\noindent will return the theorem:

\begin{hol}
\begin{alltt}
   |- \m{t} INSERT \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb = \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb
\end{alltt}\end{hol}

Here is an example of \ml{INSERT\_CONV} in use:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#INSERT_CONV num_EQ_CONV "(SUC 2) INSERT {0,1,2,3}";;
|- {SUC 2,0,1,2,3} = {0,1,2,3}
\end{verbatim}\end{session}

When applied repeatedly, \ml{INSERT\_CONV} can be used to reduce finite sets by
eliminating as many redundant occurrences of elements as possible.  An easy to
program, but slow-running, way of doing this is to use \ml{DEPTH\_CONV}:

\begin{session}
\begin{verbatim}
#DEPTH_CONV (INSERT_CONV num_EQ_CONV) "{1,3,x,SUC 1,SUC(SUC 1),2,1,3,x}";;
|- {1,3,x,SUC 1,SUC(SUC 1),2,1,3,x} = {2,1,3,x}
\end{verbatim}\end{session}

\noindent For a faster alternative to this method, see the reference entry for
\ml{INSERT\_CONV} in
chapter~\ref{entries}.\index{INSERT\_CONV@{\ptt INSERT\_CONV}|)}%
\index{conversions!INSERT\_CONV@{\ptt INSERT\_CONV}|)}

\subsubsection{Deletion}

The\index{DELETE\_CONV@{\ptt DELETE\_CONV}|(}%
\index{conversions!DELETE\_CONV@{\ptt DELETE\_CONV}|(}
conversion \ml{DELETE\_CONV} reduces terms of the form
{\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!} DELETE !$t$\verb!"!}
by deleting all elements provably equal to {\small$t$} from the set
{\small\verb!{!\tt$t_1$,\dots,$t_n$\verb!}!}.
Like \ml{IN\_CONV} and \ml{INSERT\_CONV}, the function \ml{DELETE\_CONV} takes
a conversion for deciding equality of set elements as an argument.
If \ml{conv}
is such a conversion, the call:

\begin{hol}\begin{alltt}
   DELETE\_CONV conv "\lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb DELETE \m{t}";;
\end{alltt}\end{hol}

\noindent will return the theorem:

\begin{hol}\begin{alltt}
   |- \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb DELETE \m{t} = \lb\m{t\sb{i}},\dots,\m{t\sb{j}}\rb
\end{alltt}\end{hol}

\noindent where the resulting set
 {\small\verb!{!\tt$t_i$,\dots,$t_j$\verb!}!} is the set of all
values {\small$t_k$} in the original set
 {\small\verb!{!\tt$t_1$,\dots,$t_n$\verb!}!} for which \ml{conv} proves
{\tt |- ($t_k$ = $t$) = F}, and where for all {\small$t_k$} in
{\small\verb!{!\tt$t_1$,\dots,$t_n$\verb!}!} but not in
 {\small\verb!{!\tt$t_i$,\dots,$t_j$\verb!}!}, either  {\small$t_k$}
is alpha-equivalent to  {\small$t$} or \ml{conv} proves
{\tt |- ($t_k$ = $t$) = T}.  Note that the conversion \ml{conv} must
prove either equality or inequality for every element of the original set that
is not simply alpha-equivalent to the deleted value.

The following session shows \ml{DELETE\_CONV} in use:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#DELETE_CONV num_EQ_CONV "{0,1,2,3} DELETE (SUC 1)";;
|- {0,1,2,3} DELETE (SUC 1) = {0,1,3}
\end{verbatim}\end{session}%
\index{DELETE\_CONV@{\ptt DELETE\_CONV}|)}%
\index{conversions!DELETE\_CONV@{\ptt DELETE\_CONV}|)}


\section{Singleton sets}

A {\it singleton\/} set is a set that contains precisely one element.  In the
\ml{pred\_sets} library, the property of being a singleton set is expressed by
the definition:

\begin{hol}
\index{definition!of SING@of {\ptt SING}}
\index{SING\_DEF@{\ptt SING\_DEF}}
\begin{verbatim}
   SING_DEF   |- !s. SING s = (?x. s = {x})
\end{verbatim}\end{hol}

\noindent The library contains several built-in theorems about singleton sets.
These are sometimes expressed in terms of the predicate \ml{SING}, as for
example in the theorem

\begin{hol}
\index{SING@{\ptt SING}}
\begin{verbatim}
   SING   |- !x. SING{x}
\end{verbatim}\end{hol}

\noindent But properties of singleton sets are more usually formulated as
theorems about sets of the form `{\small\verb"{x}"}'. For example, the built-in
theorems about singleton sets include:

\begin{hol}
\index{SING@{\ptt SING}}
\begin{verbatim}
   NOT_SING_EMPTY  |- !x. ~({x} = {})
   IN_SING         |- !x y. x IN {y} = (x = y)
   EQUAL_SING      |- !x y. ({x} = {y}) = (x = y)
\end{verbatim}\end{hol}

\noindent A\index{naming conventions!for theorems about singletons|(} general
convention is that theorems about singleton sets are given names that contain
the element `\ml{SING}', regardless of whether or not they actually contain the
predicate \ml{SING}.\index{naming conventions!for theorems about singletons|)}

\section{The {\tt CHOICE} and {\tt REST} functions}

The \ml{pred\_sets} library contains the definition of a functions \ml{CHOICE}
which can be used to select an arbitrary element from a non-empty set. The
function \ml{CHOICE} is defined formally by the following constant
specification:

\begin{hol}
\index{definition!of CHOICE@of {\ptt CHOICE}}
\index{CHOICE\_DEF@{\ptt CHOICE\_DEF}}
\begin{verbatim}
   CHOICE_DEF   |- !s. ~(s = {}) ==> (CHOICE s) IN s
\end{verbatim}\end{hol}

\noindent This theorem alone is the defining property for the constant
\ml{CHOICE}, which is therefore an only partially specified function from sets
to values.  Note, in particular, that there is no information given by this
definition about the result of applying \ml{CHOICE} to an empty set.

The library also contains a function \ml{REST}, which is defined in terms of
the \ml{CHOICE} function as follows

\begin{hol}
\index{definition!of REST@of {\ptt REST}}
\index{REST\_DEF@{\ptt REST\_DEF}}
\begin{verbatim}
   REST_DEF   |- !s. REST s = s DELETE (CHOICE s)
\end{verbatim}\end{hol}

\noindent For any non-empty set \ml{s}, the set \ml{REST s} comprises all those
elements of \ml{s} except the value selected from \ml{s} by \ml{CHOICE}.

The library contains various built-in theorems about the functions \ml{CHOICE}
and \ml{REST}; for a full list of these theorems, see chapter~\ref{theorems}.

\section{Image of a function on a set}

The {\it image\/} of a function {\small\verb!f:'a->'b!} on a set
{\small\verb!s:'a->bool!} is the set of values {\small\verb!f(x)!} for all
\ml{x} in \ml{s}.  In the \ml{pred\_sets} library, the image of a function on a
set is defined in terms of the obvious set abstraction:

\begin{hol}
\index{definition!of IMAGE@of {\ptt IMAGE}}
\index{IMAGE\_DEF@{\ptt IMAGE\_DEF}}
\begin{verbatim}
   IMAGE_DEF   |- !f s. IMAGE f s = {f x | x IN s}
\end{verbatim}\end{hol}

\noindent Using \ml{SET\_SPEC\_CONV}, is trivial to prove from this
definition the following membership condition for sets constructed using
\ml{IMAGE}:

\begin{hol}
\index{IN\_IMAGE@{\ptt IN\_IMAGE}}
\begin{verbatim}
   IN_IMAGE   |- !y s f. y IN (IMAGE f s) = (?x. (y = f x) /\ x IN s)
\end{verbatim}\end{hol}

\noindent The \ml{pred\_sets} library contains various theorems about
\ml{IMAGE} in addition to this membership theorem.  These include, for example,
theorems about the image of a function on sets constructed by the operations of
union and intersection.  For a full list of theorems about \ml{IMAGE}, see
chapter~\ref{theorems}.

\subsection{Theorem-proving support}

The\index{IMAGE\_CONV@{\ptt IMAGE\_CONV}|(}%
\index{conversions!IMAGE\_CONV@{\ptt IMAGE\_CONV}|(}
\ml{pred\_sets} library contains
a conversion for computing the image of a function {\small\verb!f!} on a finite
set {\small\verb!{!\tt$t_1$,\dots,$t_n$\verb!}!}.  The function

\begin{hol}
\begin{verbatim}
   IMAGE_CONV : conv -> conv -> conv
\end{verbatim}\end{hol}

\noindent is parameterized by two conversions.  The first conversion is
expected to compute the result of applying the function {\small\verb!f!} to
each element {\small$t_1$}, \dots, {\small $t_n$}.  The second parameter is an
equality conversion which is used to simplify the resulting image set by
removing redundant occurrences of its elements.

The following session shows a simple example of the use of \ml{IMAGE\_CONV} on
terms of the form
{\small\tt\verb!"IMAGE (\x.x+2) {!$t_1$,\dots,$t_n$\verb!}"!}.
We first define a conversion that evaluates the
result of applying the function {\small\verb!(\x.x+2)!} to a term {\small$t$}.

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- val AP_CONV = BETA_CONV THENC (TRY_CONV ADD_CONV);;
AP_CONV = - : conv

- AP_CONV ``(\n.n+2) 7``;
|- (\n. n + 2)7 = 9
\end{verbatim}\end{session}

\noindent This conversion, together with the function \ml{IMAGE\_CONV}, gives a
conversion for computing the image of {\small\verb!(\x.x+2)!} on a finite set
of numerical values.

\begin{session}
\begin{verbatim}
- IMAGE_CONV AP_CONV NO_CONV ``IMAGE (\x.x+2) {1;2;3;4}``;
val it = |- IMAGE(\x. x + 2){1;2;3;4} = {3;4;5;6} : thm

- IMAGE_CONV AP_CONV NO_CONV ``IMAGE (\x.x+2) {n;1;n}``;
val it = |- IMAGE(\x. x + 2){n;1;n} = {3;n + 2} : thm
\end{verbatim}\end{session}

\noindent In this case, the second parameter supplied to \ml{IMAGE\_CONV} is
the conversion \ml{NO\_CONV}. This means that no reduction of the resulting
image set is done, beyond the elimination of elements that are provably
redundant by virtue of being alpha-equivalent to some other element (as in the
second example above).

The following session illustrates the use of the second parameter to
\ml{IMAGE\_CONV}.

\begin{session}
\begin{verbatim}
#IMAGE_CONV BETA_CONV NO_CONV "IMAGE (\x. SUC x) {1,SUC 0,2,0}";;
|- IMAGE(\x. SUC x){1,SUC 0,2,0} = {SUC 1,SUC(SUC 0),SUC 2,SUC 0}

#IMAGE_CONV BETA_CONV num_EQ_CONV "IMAGE (\x. SUC x) {1,SUC 0,2,0}";;
|- IMAGE(\x. SUC x){1,SUC 0,2,0} = {SUC(SUC 0),SUC 2,SUC 0}
\end{verbatim}\end{session}

\noindent In the first evaluation, just applying \ml{BETA\_CONV} to the
application of {\small\verb!(\x. SUC x)!} to each element has resulted in an
image set containing both {\small\verb!SUC 1!} and {\small\verb!SUC(SUC 0)!}.
In the second example, \ml{num\_EQ\_CONV} is used to prove these values equal,
and therefore to simplify the resulting set by eliminating one of them from it.
For more detail about \ml{IMAGE\_CONV}, see the reference entry for this
conversion in chapter~\ref{entries}.\index{IMAGE\_CONV@{\ptt IMAGE\_CONV}|)}%
\index{conversions!IMAGE\_CONV@{\ptt IMAGE\_CONV}|)}

\section{Mappings between sets}

The \ml{pred\_sets} library contains a few basic definitions and theorems
having to do with mappings between sets.  A function \ml{f:'a->'b} is an {\it
injective\/} (one-to-one) mapping from a set {\small\verb!s:'a->bool!} to a set
{\small\verb!t:'b->bool!} if it takes distinct elements of the set \ml{s} to
distinct element of the set \ml{t}:

\begin{hol}
\index{definition!of INJ@of {\ptt INJ}}
\index{INJ\_DEF@{\ptt INJ\_DEF}}
\begin{verbatim}
   INJ_DEF =
   |- !f s t.
       INJ f s t =
       (!x. x IN s ==> (f x) IN t) /\
       (!x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y))
\end{verbatim}\end{hol}

\noindent Likewise, a function \ml{f:'a->'b} is a {\it surjective\/} (onto)
mapping from \ml{s} to \ml{t} if for every element \ml{x} of \ml{t} there is
some element \ml{y} of \ml{s} for which {\small\verb!f y = x!}:

\begin{hol}
\index{definition!of SURJ@of {\ptt SURJ}}
\index{SURJ\_DEF@{\ptt SURJ\_DEF}}
\begin{verbatim}
   SURJ_DEF =
   |- !f s t.
       SURJ f s t =
       (!x. x IN s ==> (f x) IN t) /\
       (!x. x IN t ==> (?y. y IN s /\ (f y = x)))
\end{verbatim}\end{hol}

\noindent Finally, a function \ml{f:'a->'b} is a {\it bijection\/} from \ml{s}
to \ml{t} if it is both injective and surjective:

\begin{hol}
\index{definition!of BIJ@of {\ptt BIJ}}
\index{BIJ\_DEF@{\ptt BIJ\_DEF}}
\begin{verbatim}
   BIJ_DEF = |- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t
\end{verbatim}\end{hol}

There are a few pre-proved theorems about the predicates \ml{INJ}, \ml{SURJ},
and \ml{BIJ} available in the library; see chapter~\ref{theorems} for a full
list of these theorems.

The library also contains constant specifications for two functions \ml{LINV}
and \ml{RINV}, which yield left and right inverses to injective and surjective
mappings respectively.  These functions are defined by:

\begin{hol}
\index{definition!of LINV@of {\ptt LINV}}
\index{LINV\_DEF@{\ptt LINV\_DEF}}
\index{definition!of RINV@of {\ptt RINV}}
\index{RINV\_DEF@{\ptt RINV\_DEF}}
\begin{verbatim}
   LINV_DEF = |- !f s t. INJ f s t ==> (!x. x IN s ==> (LINV f s(f x) = x))
   RINV_DEF = |- !f s t. SURJ f s t ==> (!x. x IN t ==> (f(RINV f s x) = x))
\end{verbatim}\end{hol}

\noindent There are, at present, no additional built-in theorems about these
two functions. Furthermore, the definitions of \ml{LINV} and \ml{RINV} shown
above should be regarded as only provisional; they may be changed in future
versions.

\section{Finite and infinite sets}

The \ml{pred\_sets} library includes the definition of a predicate called
\ml{FINITE}, which is true of finite sets and false of infinite ones.  The
definition of this constant is shown below.

\begin{hol}
\index{definition!of FINITE@of {\ptt FINITE}}
\index{FINITE\_DEF@{\ptt FINITE\_DEF}}
\begin{verbatim}
   FINITE_DEF
     |- !s.
         FINITE s =
         (!P. P{} /\ (!s'. P s' ==> (!e. P(e INSERT s'))) ==> P s)
\end{verbatim}\end{hol}

\noindent That is, a set \ml{s} is finite precisely when it is in the smallest
class of sets that contains the empty set and is closed under the \ml{INSERT}
operation.  This inductive definition makes \ml{FINITE} true of just those sets
that can be constructed from the empty set by a finite sequence of applications
of the \ml{INSERT} operation.

The \ml{pred\_sets} library contains various built-in theorems that follow from
the definition of \ml{FINITE} given above.  Among these are the two fundamental
theorems shown below:

\begin{hol}
\index{FINITE\_EMPTY@{\ptt FINITE\_EMPTY}}
\index{FINITE\_INSERT@{\ptt FINITE\_INSERT}}
\begin{verbatim}
   FINITE_EMPTY   |- FINITE{}
   FINITE_INSERT  |- !x s. FINITE(x INSERT s) = FINITE s
\end{verbatim}\end{hol}

\noindent These state that the empty set is indeed finite and insertion
constructs finite sets only from other finite sets. See chapter~\ref{theorems}
for other built-in theorems about finite sets.

The above definition of \ml{FINITE} formalizes the notion of a finite set in
logic, and it therefore also determines the form of definition for the
complementary notion of an infinite set. In the \ml{pred\_sets} library, the
predicate \ml{INFINITE} is defined as follows:

\begin{hol}
\index{definition!of INFINITE@of {\ptt INFINITE}}
\index{INFINITE\_DEF@{\ptt INFINITE\_DEF}}
\begin{verbatim}
   INFINITE_DEF   |- !s. INFINITE s = ~FINITE s
\end{verbatim}\end{hol}

\noindent There are a few consequences of this definition stored in the
\ml{pred\_sets} library.  The following theorem, for example, states that the
image of an injective function on an infinite set is infinite:

\begin{hol}
\index{IMAGE\_11\_INFINITE@{\ptt IMAGE\_11\_INFINITE}}
\begin{verbatim}
   IMAGE_11_INFINITE
      |- !f. (!x y. (f x = f y) ==> (x = y)) ==>
             (!s. INFINITE s ==> INFINITE(IMAGE f s))
\end{verbatim}\end{hol}

\noindent Other built-in theorems about \ml{INFINITE} can be found in
chapter~\ref{theorems}.

\subsection{Theorem-proving support}

There are two \ML\ functions in the \ml{pred\_sets} library for reasoning about
propositions that involve the finiteness predicate \ml{FINITE}.
The\index{FINITE\_CONV@{\ptt FINITE\_CONV}|(}
\index{conversions!FINITE\_CONV@{\ptt FINITE\_CONV}|(} first of these is a
conversion \ml{FINITE\_CONV} which automatically proves that sets of the form
{\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!} are finite.  Evaluating

\begin{hol}
\begin{alltt}
   FINITE\_CONV "FINITE \lb\m{t\sb{1}},\dots,\m{t\sb{n}}\rb";;
\end{alltt}\end{hol}

\noindent yields the theorem
{\small\verb!|- FINITE {!\tt$t_1$,\dots,$t_n$\verb!} = T!}.%
\index{FINITE\_CONV@{\ptt FINITE\_CONV}|)}%
\index{conversions!FINITE\_CONV@{\ptt FINITE\_CONV}|)}

The\index{SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|(}
\index{tactics!SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|(}
second \ML\ function for
reasoning about the predicate \ml{FINITE} is an induction tactic called
\ml{SET\_INDUCT\_TAC}.  When applied to a goal of the form
{\small\verb!"!!$s$\verb!. FINITE !$s$\verb! ==> !$P$\verb!"!}, this tactic
reduces it to proving that the property of sets expressed by
{\small\verb!\!$s$\verb!.!$P$} holds of the empty set and is preserved by the
insertion of an element into an arbitrary finite set.  Since every finite set
can be built up from the empty set by repeated insertion of values, these
subgoals imply that this property holds of all finite sets.

The following session illustrates the use of the tactic \ml{SET\_INDUCT\_TAC}
for proving that the intersection of an arbitrary set \ml{t} with a finite set
\ml{s} is finite.  We first set up an appropriate goal:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
#g "!s:'a->bool. FINITE s ==> !t. FINITE(s INTER t)";;
"!s. FINITE s ==> (!t. FINITE(s INTER t))"

() : void
\end{verbatim}\end{session}

\noindent Expanding with \ml{SET\_INDUCT\_TAC} yields:

\begin{session}
\begin{verbatim}
#expand SET_INDUCT_TAC;;
OK..
2 subgoals
"!t. FINITE((e INSERT s) INTER t)"
    [ "FINITE s" ]
    [ "!t. FINITE(s INTER t)" ]
    [ "~e IN s" ]

"!t. FINITE({} INTER t)"

() : void
\end{verbatim}\end{session}

\noindent The resulting subgoals are easy to prove, given the two basic
theorems \ml{FINITE\_EMPTY} and \ml{FINITE\_INSERT} shown in the previous
section. Note that it may be assumed in the step case that the value \ml{e}
being inserted into the set \ml{s} is not already an element of
\ml{s}.\index{SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|)}%
\index{tactics!SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|)}

\section{Cardinality of finite sets}

The {\it cardinality\/} of a finite set is the number of elements it contains.
In the \ml{pred\_sets} library, this is formalized by a constant \ml{CARD}
defined by means of the following constant specification:

\begin{hol}
\index{definition!of CARD@of {\ptt CARD}}
\index{CARD\_DEF@{\ptt CARD\_DEF}}
\begin{verbatim}
  CARD_DEF
    |- (CARD{} = 0) /\
       (!s.
         FINITE s ==>
         (!x. CARD(x INSERT s) = (x IN s => CARD s | SUC(CARD s))))
\end{verbatim}\end{hol}

\noindent This theorem is the sole defining property of \ml{CARD}.  Because the
equation in the second clause holds only under the assumption that \ml{s} is
finite, this form of definition allows nothing significant to be deduced about
the cardinality `\ml{CARD s}' of an {\it infinite\/} set \ml{s}.

The built-in theorems about cardinality are all restricted to finite sets only,
either implicitly as in the theorem:

\begin{hol}
\index{CARD\_SING@{\ptt CARD\_SING}}
\begin{verbatim}
   CARD_SING  |- !x. CARD{x} = 1
\end{verbatim}\end{hol}

\noindent or explicitly, as in:

\begin{hol}
\index{FINITE\_ISO\_NUM@{\ptt FINITE\_ISO\_NUM}}
\begin{verbatim}
   FINITE_ISO_NUM
     |- !s:'a->bool.
         FINITE s ==>
         (?f:num->'a.
           (!n m.
             n < (CARD s) /\ m < (CARD s) ==> (f n = f m) ==> (n = m)) /\
           (s = {f n | n < (CARD s)}))
\end{verbatim}\end{hol}

\noindent This second theorem states that the elements of a finite set can
always be put into a one-to-one correspondence with the natural numbers less
than the set's cardinality---i.e. the elements of a finite set \ml{s} can be
numbered \ml{0}, \ml{1}, \dots, {\small\verb!(CARD s)-1!}.  Other theorems
involving the cardinality function \ml{CARD} can be found in
chapter~\ref{theorems}.

\section{Using the library}\label{using}

The \ml{pred\_sets} library is loaded into a user's \HOL\ session using the
function \ml{load\_library} (see the \HOL\ manual for a general description of
library loading).  The first action in the load sequence is to update the
internal \HOL\ search paths.  A pathname to the library is added to the search
path so that theorems may be autoloaded from the library theory
\ml{pred\_sets}; and the \HOL\ help search path is updated with a pathname to
online help files for the \ML\ functions in the library.

After the search paths are updated, the actions taken by the load sequence for
\ml{pred\_sets} depend on the current state of the \HOL\ session. If the system
is in draft mode, the library theory \ml{pred\_sets} is added as a new parent
to the current theory.  If the system is not in draft mode, but the current
theory is an ancestor of the \ml{pred\_sets} theory in the library (e.g.\ the
user is in a fresh \HOL\ session) then \ml{pred\_sets} is made the current
theory.  In both cases, the \ML\ functions provided by the library are loaded
into \HOL\, and all the theorems in the library (including definitions) are set
up to be autoloaded on demand.  The parser and pretty-printer for the notation
described above in sections~\ref{abst} and~\ref{finite} are then activated, and
the \ML\ functions provided by the library for reasoning about sets are loaded.
The \ml{pred\_sets} library is then fully loaded into the user's \HOL\ session.

\subsection{Example session}

The following session shows how the \ml{pred\_sets} library may be loaded using
\ml{load\_library}. Suppose, beginning in a fresh \HOL\ session, the user
wishes to create a theory \ml{foo} whose parents include the theory
\ml{pred\_sets} in the library. This may be done as follows:

\setcounter{sessioncount}{1}
\begin{session}
\begin{alltt}
#new_theory `foo`;;
() : void

#load_library `pred_sets`;;
  \(\vdots\)
Library pred_sets loaded.
() : void
\end{alltt}\end{session}

\noindent Loading the library while drafting the theory \ml{foo} makes the
library theory \ml{pred\_sets} into a parent of \ml{foo}.  The same effect
could have been achieved (in a fresh session) by first loading the library and
then creating \ml{foo}:

\setcounter{sessioncount}{1}
\begin{session}
\begin{alltt}
#load_library `pred_sets`;;
  \(\vdots\)
Library pred_sets loaded.
() : void

#new_theory `foo`;;
() : void
\end{alltt}\end{session}

\noindent The theory \ml{pred\_sets} is first made the current theory of the
new session.  It then automatically becomes a parent of \ml{foo} when this
theory is created by \ml{new\_theory}.

Now, suppose that \ml{foo} has been created as shown above, and the user does
some work in this theory, quits \HOL, and in a later session wishes to load the
theory \ml{foo}.  This must be done by {\it first\/} loading the
\ml{pred\_sets} library and {\it then\/} loading the theory \ml{foo}.

\setcounter{sessioncount}{1}
\begin{session}
\begin{alltt}
#load_library `pred_sets`;;
  \(\vdots\)
Library pred_sets loaded.
() : void

#load_theory `foo`;;
Theory foo loaded
() : void
\end{alltt}\end{session}

\noindent This sequence of actions ensures that the system can find the parent
theory \ml{pred\_sets} when it comes to load \ml{foo}, since loading the
library updates the search path.

\subsection{The {\tt load\_pred\_sets} function}%
\index{load\_pred\_sets@{\ptt load\_pred\_sets}|(}

The \ml{pred\_sets} library may in many cases simply be loaded into the system
as illustrated by the examples given above.  There are, however, certain
situations in which the library cannot be fully loaded at the time when the
\ml{load\_library} is used.  This occurs when the system is not in draft mode
and the current theory is not an ancestor of the theory \ml{pred\_sets}.  In
this case, loading the library can (and will) update the search paths.  But the
theory \ml{pred\_sets} can neither be made into a parent of the current theory
nor be made the current theory.  This means that autoloading from the library
can not at this stage be activated; and the \ML\ code in the library can not be
loaded into \HOL, since it requires access to some of the theorems in the
library.

In the situation described above---when the system is not in draft mode and the
current theory is not an ancestor of the theory \ml{pred\_sets}---the library
load sequence defines an \ML\ function called \ml{load\_pred\_sets} in the
current \HOL\ session.  If at a future point in the session the \ml{pred\_sets}
theory (now accessible via the search path) becomes an ancestor of the current
theory, this function can then be used to complete loading of the library.
Evaluating {\small\verb!load_pred_sets()!} in such a context loads the \ML\
functions of the \ml{pred\_sets} library into \HOL\ and activates autoloading
from its theory files.  It also activates the parser and pretty-printer support
for set abstractions and finite sets.  The function \ml{load\_pred\_sets} fails
if the theory \ml{pred\_sets} is not an ancestor of the current \HOL\ theory.

Note that the function \ml{load\_pred\_sets} becomes available upon loading the
\ml{pred\_sets} library only if the library theory \ml{pred\_sets} at the point
of loading the library can neither be made into a new parent (i.e.\ the system
is not in draft mode) nor be made the current
theory.\index{load\_pred\_sets@{\ptt load\_pred\_sets}|)}