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

The \ml{finite\_sets} library contains a theory of sets based on a defined
logical type \ml{(*)set}, values of which are finite collections or `sets' of
elements of type \ml{*}.  The library was originally written in May 1989 by P.\
J.\ Windley and Philippe Leveilley.  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{finite\_sets} library closely parallel to the \HOL\ \ml{sets} and
\ml{pred\_sets} libraries, with the same names for constants and theorems and,
as far as possible, the same form of definitions for operations on sets.  This
consistency across the three set theory libraries allows proofs done in one
library to be easily adapted to the others.  It is also helpful to users who,
for example, have to switch between set theory libraries for different
projects.

There is only one theory in the \ml{finite\_sets} library, namely the theory
`\ml{finite\_sets}'. This contains all the definitions and theorems in the
library.  This document, adapted from the manual for the \ml{sets}
library~\cite{melham}, explains the logical basis of this theory. The theory
itself closely follows the finite set theory presented in chapter 10 of Manna
and Waldinger's book~\cite{manna}.  This document also explains the
theorem-proving support provided by the \ml{finite\_sets} library, which
includes conversions evaluating various operations on finite sets described by
enumeration of their elements.  The library also provides parser and
pretty-printer support for certain terms that denote finite sets.

\section{The type definition}\index{definition!of (*)set@of {\ptt (*)set}|(} 

The \ml{finite\_sets} library is based on a polymorphic type of sets
\ml{(*)set}, values of which unordered finite collections of values of the base
type \ml{*}.  The representing type for the definition of \ml{(*)set} is the
type of predicates {\small\verb!*->bool!}; the values of type \ml{(*)set}
correspond to precisely those predicates that are true of a finite number of
values of type \ml{*}.

The set of all such predicates is defined inductively in terms of
representations of the empty set and the operation of inserting an element into
an already existing set.  The empty set is represented by the constant false
predicate {\small\verb!\x.F!}. The insertion operation is represented by the
function that maps a value \ml{x:*} and a predicate \ml{s} representing a set
to the predicate {\small\verb!\e. (e = x) \/ s e!}, which represents of the set
obtained by adding {\small\verb!x!} to the set represented by {\small\verb!s!}.
A predicate {\small\verb!s:*->bool!} then represents a finite set iff it is in
the intersection of all classes of predicates that contain the representation
of empty and are closed under the representation of the insertion operation.
Hence {\small\verb!s:*->bool!} represents a finite set if and only if it can be
obtained by applying a finite sequence of insert operations to the empty set.

This characterization of the finite sets is expressed formally in the
\ml{finite\_sets} theory by the constant \ml{IS\_SET\_REP}, which is defined
the following constant specification:

\begin{hol}
\index{definition!of IS\_SET\_REP@of {\ptt IS\_SET\_REP}}
\index{IS\_SET\_REP@{\ptt IS\_SET\_REP}}
\begin{verbatim}
   IS_SET_REP
   |- IS_SET_REP(\x. F) /\
      (!s. IS_SET_REP s ==> (!x. IS_SET_REP(\y. (y = x) \/ s y))) /\
      (!P.
        P(\x. F) /\ (!t. P t ==> (!x. P(\y. (y = x) \/ t y))) ==>
        (!s. IS_SET_REP s ==> P s))
\end{verbatim}\end{hol}

\noindent The specification has three conjuncts, which constitute an {\it
inductive definition\/} (see~\cite{ind-defs}) of the class of all finite set
representations.  The first conjunct states that the constant false predicate
{\small\verb!\x.F!} is included in the class of predicates that represent
finite sets.  The second states that the class of predicates that represent
finite sets is closed under the element insertion operation. And the third
states that \ml{IS\_SET\_REP} is true of precisely the smallest such class of
predicates.

Using this definition of the class of finite sets, 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 IS_SET_REP rep
\end{verbatim}\end{hol}

\noindent This definitional axiom asserts the existence of a bijection \ml{rep}
between the type {\small\verb!(*)set!} and the class of all predicates on
\ml{*} that represent finite sets.  The\index{naming conventions!for
definitions|(} theorem \ml{set\_TY\_DEF} is named according to the general
convention that definitions in the \ml{finite\_sets} library are given names
ending in `{\small\verb!_DEF!}'.\index{naming conventions!for definitions|)}%
\index{definition!of (*)set@of {\ptt (*)set}|)}

\section{Abstract characterization of the type
{\tt (*)set}}\index{axioms for (*)set@axioms for {\ptt (*)set}|(}

The \ml{finite\_sets} library contains an abstract characterization of finite
sets derived by formal proof from the type definition for
{\small\verb!(*)set!}.  This characterizes finite sets in terms of three
constants: \ml{EMPTY}, which denotes the empty set; \ml{INSERT}, which is the
insertion operation by which non-empty sets are constructed; and the membership
relation \ml{IN}.  These basic constants are introduced simultaneously by the
following constant specification:

\begin{hol}
\index{definition!of IN@of {\ptt IN}}
\index{definition!of EMPTY@of {\ptt EMPTY}}
\index{definition!of INSERT@of {\ptt INSERT}}
\index{FINITE\_SET\_DEF@{\ptt FINITE\_SET\_DEF}}
\begin{verbatim}
   FINITE_SET_DEF
   |- (!x. ~x IN EMPTY) /\
      (!x y s. x IN (y INSERT s) = (x = y) \/ x IN s) /\
      (!x s. x INSERT (x INSERT s) = x INSERT s) /\
      (!x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)) /\
      (!P. P EMPTY /\ (!s. P s ==> (!e. P(e INSERT s))) ==> (!s. P s))
\end{verbatim}\end{hol}

\noindent The five conjuncts of this theorem constitute a derived
`axiomatization' for finite sets; once this theorem has been proved, it
provides a complete basis for all further reasoning about sets.  In particular,
users of the library should never have to appeal to the type definition for
{\small\verb!(*)set!}. The library theory \ml{finite\_sets} itself is developed
entirely on the basis of these `axioms' of set theory.

The first two conjuncts of \ml{FINITE\_SET\_DEF} specify the membership
relation \ml{IN} for empty and non-empty sets.  The next two conjuncts state
that sets do not contain multiple instances of the same element and that the
elements of a set are not ordered.  The final conjunct is an
induction\index{induction} theorem for finite sets.  It states that if a
property is true of the empty set and is preserved by the insertion operation,
then it holds of all sets.  It follows from this theorem that every finite set
is either empty or can be built up from the empty set by a finite number of
insertion operations.

For consistency with the other set libraries, the first four conjuncts of
\ml{FINITE\_SET\_DEF} are stored as separate theorems in the \ml{finite\_sets}
library.  They are given the names shown below.

\begin{hol} 
\index{NOT\_IN\_EMPTY@{\ptt NOT\_IN\_EMPTY}}
\index{IN\_INSERT@{\ptt IN\_INSERT}}
\index{INSERT\_INSERT@{\ptt INSERT\_INSERT}}
\index{INSERT\_COMM@{\ptt INSERT\_COMM}}
\begin{verbatim}
   NOT_IN_EMPTY  = |- !x. ~x IN {}
   IN_INSERT     = |- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s
   INSERT_INSERT = |- !x s. x INSERT (x INSERT s) = x INSERT s
   INSERT_COMM   = |- !x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)
\end{verbatim}\end{hol}

\noindent The\index{induction|(} induction property is also saved as a separate
theorem, but in a slightly stronger form than that in which it appears as part
of \ml{FINITE\_SET\_DEF}.  This theorem is:

\begin{hol} 
\index{SET\_INDUCT@{\ptt SET\_INDUCT}}
\begin{verbatim}
   SET_INDUCT 
   |- !P. P EMPTY /\ (!s. P s ==> (!e. ~e IN s ==> P(e INSERT s))) ==> !s. P s
\end{verbatim}\end{hol}

\noindent The `step' case of this stronger induction theorem requires one to
show only that the property \ml{P} is preserved by the operation of inserting
an element not already in a set \ml{s} for which \ml{P s} is assumed to
hold.\index{induction|)}

The \ml{finite\_sets} library contains many pre-proved theorems the constants
about \ml{IN}, \ml{EMPTY}, and \ml{INSERT}. These include the fundamental set
equality 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, which corresponds to what is usually called the {\it axiom
of extension\/}\index{axiom of extension} for sets.  For a complete list of the
other built-in theorems about \ml{IN}, \ml{EMPTY}, and \ml{INSERT}, see
chapter~\ref{theorems}.\index{axioms for (*)set@axioms for {\ptt (*)set}|)}

\section{The set induction tactic}\index{induction|(}

The library contains\index{SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|(}
\index{tactics!SET\_INDUCT\_TAC@{\ptt SET\_INDUCT\_TAC}|(} an induction tactic
called \ml{SET\_INDUCT\_TAC} which made available when the library is loaded.
When applied to a goal of the form {\small\verb!"!$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 the fundamental theorem \ml{EXTENSION}. We first set up a goal for
the `hard' direction of the equivalence stated by this theorem:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#g "!s t. (!x:*. x IN s = x IN t) ==> (s = t)";;
"!s t. (!x. x IN s = x IN t) ==> (s = 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. (!x. x IN (e INSERT s) = x IN t) ==> (e INSERT s = t)"
    [ "!t. (!x. x IN s = x IN t) ==> (s = t)" ]
    [ "~e IN s" ]

"!t. (!x. x IN {} = x IN t) ==> ({} = t)"

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

\noindent The resulting subgoals are reasonably easy to prove, given several
other basic theorems about membership, the empty set and insertion. (The \HOL\
proof closely follows the proof in~\cite{manna}.) Note that
\ml{SET\_INDUCT\_TAC} is based on the stronger induction theorem discussed
above, so 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}|)}%
\index{induction|)}

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

The \ml{finite\_sets} library provides special parser and pretty-printer
support for finite sets described 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.

\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{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}|)}



\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{finite\_sets} library is loaded into a user's \HOL\ session using the
builtin \ML\ 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{finite\_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
depend on the current state of the \HOL\ session. If the system is in draft
mode, the library theory \ml{finite\_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{finite\_sets} theory in the library (e.g.\ the user is
in a fresh \HOL\ session) then \ml{finite\_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{finite\_sets} library is then fully loaded into the user's \HOL\
session.

\subsection{Example session}

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

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

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

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

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

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

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

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

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

Note that the function \ml{load\_finite\_sets} is defined upon loading the
\ml{finite\_sets} library only if the library theory \ml{finite\_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\_finite\_sets@{\ptt load\_finite\_sets}|)}