\chapter{The sets Library}

The \HOL\ \ml{sets} library contains a theory of sets based on a defined
logical type \ml{(*)set}, values of which are collections or `sets' of elements
of type \ml{*}. The library was originally written in June 1989 by Philippe
Leveilley.  Since then, it has been completely revised and extended with new
theorems by the present author.  There is only one theory in the library,
namely the theory `\ml{sets}', which contains all the definitions and theorems
in the \ml{sets} library.

This document explains the logical basis of the \ml{sets} library and describes
the theorem-proving support it provides.  This 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{The type definition}\index{definition!of (*)set@of {\ptt (*)set}|(} 

The basis of the library is the polymorphic type of sets \ml{(*)set}, which is
defined in the library theory \ml{sets}.  Values of this type are not true
sets, but just unordered collections of values of the base type \ml{*}.  The
type \ml{(*)set} is, in fact, just an object-language abbreviation for the type
\ml{*->bool}, values of which are predicates on \ml{*}. The elements of a set
\ml{S:(*)set} are just those values of type \ml{*} for which the corresponding
predicate is true.

The type \ml{(*)set} is defined formally in the library by the type definition:

\begin{hol}
\index{set\_TY\_DEF@{\ptt set\_TY\_DEF}}
\begin{verbatim}
   set_TY_DEF   |- ?rep:(*)set -> (* -> bool). TYPE_DEFINITION(\p. T)rep
\end{verbatim}\end{hol}

\noindent This definitional axiom asserts the existence of a bijection \ml{rep}
between sets with elements of type \ml{*} and the set of all predicates on
\ml{*}.  In the library theory \ml{sets}, a pair of constant functions is
introduced using the built-in function
\ml{define\_new\_type\_bijections}\index{define\_new\_type\_bijections@{\ptt
define\_new\_type\_bijections}} to denote this bijection and its inverse:

\begin{hol}
\index{SPEC@{\ptt SPEC}}
\index{CHF@{\ptt CHF}}
\begin{alltt}
   CHF : (*)set -> (* -> bool)   {\normalsize\rm and}   SPEC : (* -> bool) -> (*)set
\end{alltt}\end{hol}

\noindent {\samepage The defining property of these constants is the constant
specification \ml{set\_ISO\_DEF}\index{set\_ISO\_DEF@{\ptt set\_ISO\_DEF}}:

\begin{hol}
\index{definition!of CHF@of {\ptt CHF}}
\index{definition!of SPEC@of {\ptt SPEC}}
\begin{verbatim}
   |- (!a. SPEC(CHF a) = a) /\ (!r. (\p. T)r = (CHF(SPEC r) = r))
\end{verbatim}\end{hol}

\noindent which states that \ml{CHF} and \ml{SPEC} are} the inverses of one
another.  These two functions can be used to move freely between sets and the
predicates to which they correspond; the function \ml{CHF} maps a set to its
characteristic predicate, and \ml{SPEC} maps a predicate to the set of values
for which it holds.  

The\index{naming conventions!for definitions|(} theorems \ml{set\_TY\_DEF} and
\ml{set\_ISO\_DEF} shown above are named according to the general convention
that all definitions in the \ml{sets} library are given names ending in
`{\small\verb!_DEF!}'.\index{naming conventions!for definitions|)}%
\index{definition!of (*)set@of {\ptt (*)set}|)}

\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}. The bijection \ml{CHF}
just maps sets to their characteristic predicates, so this membership relation
for sets is straightforward to define\index{definition!of IN@of {\ptt IN}} as
follows:

\begin{hol}
\index{IN\_DEF@{\ptt IN\_DEF}}
\begin{verbatim}
   IN_DEF   |- !x s. x IN s = CHF s x
\end{verbatim}\end{hol}

\noindent The infix function constant \ml{IN} defined here is essentially just
an abbreviation for \ml{CHF}.  The functions \ml{IN} and \ml{SPEC} (introduced
above) constitute the basic language for the theory of sets in the \ml{sets}
library; all operators and predicates on sets are ultimately defined in terms
of these two functions.

The first significant theorem in the \ml{sets} library states what is usually
called the {\it axiom of extension\/}\index{axiom of extension} for sets.  This
is not, of course, an {\it axiom\/} of the \ml{sets} theory, but rather a
theorem:

\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 \ml{IN} and
the fact that the function \ml{CHF} has a left inverse and is therefore
injective.

The second main theorem in the library concerns the function \ml{SPEC}.  This
function maps an arbitrary predicate \ml{P:(*->bool)} on values of type \ml{*}
to the set of all values \ml{x:*} such that \ml{P x} is true.  The \ml{SPEC}
function can therefore be used to construct sets from predicates that describe
or `specify' their elements. A value is in the constructed set exactly when the
predicate is true of that value:

\begin{hol}
\index{SPECIFICATION@{\ptt SPECIFICATION}}
\begin{verbatim}
   SPECIFICATION   |- !P x. x IN (SPEC P) = P x
\end{verbatim}\end{hol}

\noindent This theorem corresponds to what is usually called the {\it axiom of
specification\/}\index{axiom of specification} for sets.  It follows directly
from the definition of \ml{IN} and the fact that \ml{CHF} is the left inverse
of \ml{SPEC}.

Once the theorems \ml{EXTENSION} and \ml{SPECIFICATION} have been proved, they
provide a complete basis for all further reasoning about sets.  Given these two
theorems, users of the library should never have to appeal to the definition of
\ml{IN} or make use of the theorems in the previous section about the formal
definition of the type \ml{(*)set}.  The library theory \ml{sets} itself is
developed entirely on the basis of these two `axioms' of set theory.

\section{Generalized set specifications}

In addition to the basic function \ml{SPEC}, which allows one to construct a
set from a predicate that specifies its elements, the \ml{sets} library also
provides way of constructing sets from more general forms of set
specifications.  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{sets} library supports generalized set specifications by means of the
constant:

\begin{hol}
\index{GSPEC@{\ptt GSPEC}}
\begin{verbatim}
   GSPEC : (** -> (* # bool)) -> (*)set
\end{verbatim}\end{hol}

\noindent The function \ml{GSPEC} takes a function \ml{f : ** -> (* \# bool)}
and constructs the set of all values \ml{FST(f x)} for which \ml{SND(f x)}
holds, for some value \ml{x} of type \ml{**}. The formal definition of the
constant \ml{GSPEC} is:

\begin{hol}
\index{definition!of GSPEC@of {\ptt GSPEC}}
\index{GSPEC\_DEF@{\ptt GSPEC\_DEF}}
\begin{verbatim}
   GSPEC_DEF   |- !f. GSPEC f = SPEC(\y. ?x. (y,T) = f x)
\end{verbatim}\end{hol}

\noindent The following analogue to the axiom of
specification\index{axiom of specification!for generalized set specifications} 
for \ml{SPEC} follows immediately from this definition:

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

\noindent 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{sets} library provides parser and pretty-printer support for set
abstractions of the form {\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{sets} library has already
been loaded. (See section~\ref{using} for a description of how \ml{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
interpretations are pretty-printed using the 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
\pagebreak[3] 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{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 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}

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 set-valued constants are defined in the \ml{sets} library:
\ml{EMPTY:(*)set}, which denotes the empty set; and \ml{UNIV:(*)set}, which
denotes the universe, or set of all values of type \ml{*}.  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 = SPEC(\x. F)
  UNIV_DEF   |- UNIV  = SPEC(\x. T)
\end{verbatim}\end{hol}

\noindent 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 provided by \ml{SPEC} 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{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{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{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{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{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{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{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{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{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{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:*->**!} on a set
{\small\verb!s:(*)set!} is the set of values {\small\verb!f(x)!} for all \ml{x}
in \ml{s}.  In the \ml{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 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{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{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}
#let 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}";;
|- IMAGE(\x. x + 2){1,2,3,4} = {3,4,5,6}

#IMAGE_CONV AP_CONV NO_CONV "IMAGE (\x.x+2) {n,1,n}";;
|- IMAGE(\x. x + 2){n,1,n} = {3,n + 2}
\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{sets} library contains a few basic definitions and theorems having to
do with mappings between sets.  A function \ml{f:*->**} is an {\it injective\/}
(one-to-one) mapping from a set \ml{s:(*)set} to a set \ml{t:(**)set} if it
takes distinct elements of \ml{s} to distinct element of \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:*->**} 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:*->**} 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{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{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{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{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{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:(*)set. 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{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:(*)set.
         FINITE s ==>
         (?f:num->*.
           (!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{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{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{sets} depend on the current state of the \HOL\ session. If the system is in
draft mode, the library theory \ml{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{sets} theory in the library (e.g.\ the user is in a
fresh \HOL\ session) then \ml{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{sets}
library is then fully loaded into the user's \HOL\ session.

\subsection{Example session}

The following session shows how the \ml{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{sets}
in the library. This may be done as follows:

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

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

\noindent Loading the library while drafting the theory \ml{foo} makes the
library theory \ml{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 `sets`;;
  \(\vdots\)
Library sets loaded.
() : void

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

\noindent The theory \ml{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{sets}
library and {\it then\/} loading the theory \ml{foo}.

\setcounter{sessioncount}{1}
\begin{session}\begin{alltt}
#load_library `sets`;;
  \(\vdots\)
Library 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{sets} when it comes to load \ml{foo}, since loading the library
updates the search path. 

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

The \ml{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{sets}.  In this
case, loading the library can (and will) update the search paths.  But the
theory \ml{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{sets}---the library load
sequence defines an \ML\ function called \ml{load\_sets} in the current \HOL\
session.  If at a future point in the session the \ml{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_sets()!} in such a context loads the \ML\ functions of the
\ml{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\_sets} fails if the theory \ml{sets} is
not an ancestor of the current \HOL\ theory.

Note that the function \ml{load\_sets} becomes available upon loading the
\ml{sets} library only if the library theory \ml{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\_sets@{\ptt
load\_sets}|)}