\chapter{ML Functions in the Library}\label{entries}\input{entries-intro}\DOC{DELETE\_CONV}

\TYPE {\small\verb%DELETE_CONV : conv -> conv%}\egroup

\SYNOPSIS
Reduce {\small\verb%{x1,...,xn} DELETE x%} by deleting {\small\verb%x%} from  {\small\verb%{x1,...,xn}%}.

\DESCRIBE 
The function {\small\verb%DELETE_CONV%} is a parameterized conversion for reducing finite
sets of the form {\small\verb%"{t1,...,tn} DELETE t"%}, where {\small\verb%{t1,...,tn}%} is a set of
type {\small\verb%(ty)set%} and {\small\verb%t%} is a term of type {\small\verb%ty%}.  The first argument to
{\small\verb%DELETE_CONV%} is expected to be a conversion that decides equality between
values of the base type {\small\verb%ty%}.  Given an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and
{\small\verb%e2%} are terms of type {\small\verb%ty%}, this conversion should return the theorem
{\small\verb%|- (e1 = e2) = T%} or the theorem {\small\verb%|- (e1 = e2) = F%}, as appropriate.

Given such a conversion {\small\verb%conv%}, the function {\small\verb%DELETE_CONV%} returns a
conversion that maps a term of the form {\small\verb%"{t1,...,tn} DELETE t"%} to the
theorem 
{\par\samepage\setseps\small
\begin{verbatim}
   |- {t1,...,tn} DELETE t = {ti,...,tj}
\end{verbatim}
}
\noindent where {\small\verb%{ti,...,tj}%} is the subset of {\small\verb%{t1,...,tn}%} for which
the supplied equality conversion {\small\verb%conv%} proves
{\par\samepage\setseps\small
\begin{verbatim}
   |- (ti = t) = F, ..., |- (tj = t) = F
\end{verbatim}
}
\noindent and for all the elements {\small\verb%tk%} in {\small\verb%{t1,...,tn}%} but not in
{\small\verb%{ti,...,tj}%}, either {\small\verb%conv%} proves {\small\verb%|- (tk = t) = T%} or {\small\verb%tk%} is
alpha-equivalent to {\small\verb%t%}.  That is, the reduced set {\small\verb%{ti,...,tj}%} comprises
all those elements of the original set that are provably not equal to the
deleted element {\small\verb%t%}.

\EXAMPLE
In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a
parameter and used to test equality of the deleted value {\small\verb%2%} with the
elements of the set.
{\par\samepage\setseps\small
\begin{verbatim}
   #DELETE_CONV num_EQ_CONV "{2,1,SUC 1,3} DELETE 2";;
   |- {2,1,SUC 1,3} DELETE 2 = {1,3}
\end{verbatim}
}

\FAILURE 
{\small\verb%DELETE_CONV conv%} fails if applied to a term not of the form {\small\verb%"{t1,...,tn}
DELETE t"%}.  A call {\small\verb%DELETE_CONV conv "{t1,...,tn} DELETE t"%} fails unless
for each element {\small\verb%ti%} of the set {\small\verb%{t1,...,tn}%}, the term {\small\verb%t%} is either
alpha-equivalent to {\small\verb%ti%} or {\small\verb%conv "ti = t"%} returns {\small\verb%|- (ti = t) = T%} or 
{\small\verb%|- (ti = t) = F%}.

\SEEALSO
INSERT_CONV.

\ENDDOC

\DOC{IMAGE\_CONV}

\TYPE {\small\verb%IMAGE_CONV : conv -> conv -> conv%}\egroup

\SYNOPSIS
Compute the image of a function on a finite set.

\DESCRIBE 
The function {\small\verb%IMAGE_CONV%} is a parameterized conversion for computing the image
of a function {\small\verb%f:ty1->ty2%} on a finite set {\small\verb%"{t1,...,tn}"%} of type
{\small\verb%(ty1)set%}.  The first argument to {\small\verb%IMAGE_CONV%} is expected to be a conversion
that computes the result of applying the function {\small\verb%f%} to each element of this
set. When applied to a term {\small\verb%"f ti"%}, this conversion should return a theorem
of the form {\small\verb%|- (f ti) = ri%}, where {\small\verb%ri%} is the result of applying the function
{\small\verb%f%} to the element {\small\verb%ti%}.  This conversion is used by {\small\verb%IMAGE_CONV%} to compute a
theorem of the form
{\par\samepage\setseps\small
\begin{verbatim}
   |- IMAGE f {t1,...,tn} = {r1,...,rn}
\end{verbatim}
}
\noindent The second argument to {\small\verb%IMAGE_CONV%} is used (optionally) to simplify
the resulting image set {\small\verb%{r1,...,rn}%} by removing redundant occurrences of
values.  This conversion expected to decide equality of values of the result
type {\small\verb%ty2%}; given an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and {\small\verb%e2%} are terms of
type {\small\verb%ty2%}, the conversion should return either {\small\verb%|- (e1 = e2) = T%} or
{\small\verb%|- (e1 = e2) = F%}, as appropriate.

Given appropriate conversions {\small\verb%conv1%} and {\small\verb%conv2%}, the function {\small\verb%IMAGE_CONV%}
returns a conversion that maps a term of the form {\small\verb%"IMAGE f {t1,...,tn}"%} to
the theorem
{\par\samepage\setseps\small
\begin{verbatim}
   |- IMAGE f {t1,...,tn} = {rj,...,rk}
\end{verbatim}
}
\noindent where {\small\verb%conv1%} proves a theorem of the form {\small\verb%|- (f ti) = ri%} for each
element {\small\verb%ti%} of the set {\small\verb%{t1,...,tn}%}, and where the set {\small\verb%{rj,...,rk}%} is
the smallest subset of {\small\verb%{r1,...,rn}%} such no two elements are
alpha-equivalent and {\small\verb%conv2%} does not map {\small\verb%"rl = rm"%} to the theorem
{\small\verb%|- (rl = rm) = T%} for any pair of values {\small\verb%rl%} and {\small\verb%rm%} in {\small\verb%{rj,...,rk}%}.
That is, {\small\verb%{rj,...,rk}%} is the set obtained by removing multiple occurrences
of values from the set {\small\verb%{r1,...,rn}%}, where the equality conversion {\small\verb%conv2%}
(or alpha-equivalence) is used to determine which pairs of terms in
{\small\verb%{r1,...,rn}%} are equal.

\EXAMPLE
The following is a very simple example in which {\small\verb%REFL%} is used to construct the
result of applying the function {\small\verb%f%} to each element of the set {\small\verb%{1,2,1,4}%},
and {\small\verb%NO_CONV%} is the supplied `equality conversion'.
{\par\samepage\setseps\small
\begin{verbatim}
   #IMAGE_CONV REFL NO_CONV "IMAGE (f:num->num) {1,2,1,4}";;
   |- IMAGE f{1,2,1,4} = {f 2,f 1,f 4}
\end{verbatim}
}
\noindent The result contains only one occurrence of `{\small\verb%f 1%}', even though
{\small\verb%NO_CONV%} always fails, since {\small\verb%IMAGE_CONV%} simplifies the resulting set by
removing elements that are redundant up to alpha-equivalence.

For the next example, we construct a conversion that maps {\small\verb%SUC n%} for any
numeral {\small\verb%n%} to the numeral standing for the successor of {\small\verb%n%}. 
{\par\samepage\setseps\small
\begin{verbatim}
   #let SUC_CONV tm =
        let n = int_of_string(fst(dest_const(rand tm))) in
        let sucn = mk_const(string_of_int(n+1), ":num") in
            SYM (num_CONV sucn);;
   SUC_CONV = - : conv
\end{verbatim}
}
\noindent The result is a conversion that inverts {\small\verb%num_CONV%}:
{\par\samepage\setseps\small
\begin{verbatim}
   #num_CONV "4";;
   |- 4 = SUC 3

   #SUC_CONV "SUC 3";;
   |- SUC 3 = 4
\end{verbatim}
}
\noindent The conversion {\small\verb%SUC_CONV%} can then be used to compute the image
of the successor function on a finite set:
{\par\samepage\setseps\small
\begin{verbatim}
   #IMAGE_CONV SUC_CONV NO_CONV "IMAGE SUC {1,2,1,4}";;
   |- IMAGE SUC{1,2,1,4} = {3,2,5}
\end{verbatim}
}
\noindent Note that {\small\verb%2%} (= {\small\verb%SUC 1%}) appears only once in the resulting set. 

Fianlly, here is an example of using {\small\verb%IMAGE_CONV%} to compute the image of a
paired addition function on a set of pairs of numbers:
{\par\samepage\setseps\small
\begin{verbatim}
   #IMAGE_CONV (PAIRED_BETA_CONV THENC ADD_CONV) num_EQ_CONV
               "IMAGE (\(n,m).n+m) {(1,2), (3,4), (0,3), (1,3)}";;
   |- IMAGE(\(n,m). n + m){(1,2),(3,4),(0,3),(1,3)} = {7,3,4}
\end{verbatim}
}

\FAILURE 
{\small\verb%IMAGE_CONV conv1 conv2%} fails if applied to a term not of the form
{\small\verb%"IMAGE f {t1,...,tn}"%}.  An application of {\small\verb%IMAGE_CONV conv1 conv2%} to
a term {\small\verb%"IMAGE f {t1,...,tn}"%} fails unless for all {\small\verb%ti%} in the set
{\small\verb%{t1,...,tn}%}, evaluating {\small\verb%conv1 "f ti"%} returns {\small\verb%|- (f ti) = ri%}
for some {\small\verb%ri%}.

\ENDDOC

\DOC{IN\_CONV}

\TYPE {\small\verb%IN_CONV : conv -> conv%}\egroup

\SYNOPSIS
Decision procedure for membership in finite sets.

\DESCRIBE 
The function {\small\verb%IN_CONV%} is a parameterized conversion for proving or disproving
membership assertions of the general form:
{\par\samepage\setseps\small
\begin{verbatim}
   "t IN {t1,...,tn}"
\end{verbatim}
}
\noindent where {\small\verb%{t1,...,tn}%} is a set of type {\small\verb%(ty)set%} and {\small\verb%t%} is a value
of the base type {\small\verb%ty%}.  The first argument to {\small\verb%IN_CONV%} is expected to be a
conversion that decides equality between values of the base type {\small\verb%ty%}.  Given
an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and {\small\verb%e2%} are terms of type {\small\verb%ty%}, this
conversion should return the theorem {\small\verb%|- (e1 = e2) = T%} or the theorem
{\small\verb%|- (e1 = e2) = F%}, as appropriate.

Given such a conversion, the function {\small\verb%IN_CONV%} returns a conversion that
maps a term of the form {\small\verb%"t IN {t1,...,tn}"%} to the theorem
{\par\samepage\setseps\small
\begin{verbatim}
   |- t IN {t1,...,tn} = T
\end{verbatim}
}

\noindent if {\small\verb%t%} is alpha-equivalent to any {\small\verb%ti%}, or if the supplied conversion
proves {\small\verb%|- (t = ti) = T%} for any {\small\verb%ti%}. If the supplied conversion proves
{\small\verb%|- (t = ti) = F%} for every {\small\verb%ti%}, then the result is the theorem
{\par\samepage\setseps\small
\begin{verbatim}
   |- t IN {t1,...,tn} = F 
\end{verbatim}
}
\noindent In all other cases, {\small\verb%IN_CONV%} will fail.

\EXAMPLE
In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a
parameter and used to test equality of the candidate element {\small\verb%1%} with the
actual elements of the given set.
{\par\samepage\setseps\small
\begin{verbatim}
   #IN_CONV num_EQ_CONV "2 IN {0,SUC 1,3}";;
   |- 2 IN {0,SUC 1,3} = T
\end{verbatim}
}
\noindent The result is {\small\verb%T%} because {\small\verb%num_EQ_CONV%} is able to prove that {\small\verb%2%} is
equal to {\small\verb%SUC 1%}. An example of a negative result is:
{\par\samepage\setseps\small
\begin{verbatim}
   #IN_CONV num_EQ_CONV "1 IN {0,2,3}";;
   |- 1 IN {0,2,3} = F
\end{verbatim}
}
\noindent Finally the behaviour of the supplied conversion is irrelevant when
the value to be tested for membership is alpha-equivalent to an actual element:
{\par\samepage\setseps\small
\begin{verbatim}
   #IN_CONV NO_CONV "1 IN {3,2,1}";;
   |- 1 IN {3,2,1} = T
\end{verbatim}
}
\noindent The conversion {\small\verb%NO_CONV%} always fails, but {\small\verb%IN_CONV%} is nontheless
able in this case to prove the required result.

\FAILURE
{\small\verb%IN_CONV conv%} fails if applied to a term that is not of the form {\small\verb%"t IN
{t1,...,tn}"%}.  A call {\small\verb%IN_CONV conv "t IN {t1,...,tn}"%} fails unless the
term {\small\verb%t%} is alpha-equivalent to some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
{\small\verb%|- (t = ti) = T%} for some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
{\small\verb%|- (t = ti) = F%} for every {\small\verb%ti%}.

\ENDDOC

\DOC{INSERT\_CONV}

\TYPE {\small\verb%INSERT_CONV : conv -> conv%}\egroup

\SYNOPSIS
Reduce {\small\verb%x INSERT {x1,...,x,...,xn}%} to {\small\verb%{x1,...,x,...,xn}%}.

\DESCRIBE 
The function {\small\verb%INSERT_CONV%} is a parameterized conversion for reducing finite
sets of the form {\small\verb%"t INSERT {t1,...,tn}"%}, where {\small\verb%{t1,...,tn}%} is a set of
type {\small\verb%(ty)set%} and {\small\verb%t%} is equal to some element {\small\verb%ti%} of this set.  The first
argument to {\small\verb%INSERT_CONV%} is expected to be a conversion that decides equality
between values of the base type {\small\verb%ty%}.  Given an equation {\small\verb%"e1 = e2"%}, where
{\small\verb%e1%} and {\small\verb%e2%} are terms of type {\small\verb%ty%}, this conversion should return the theorem
{\small\verb%|- (e1 = e2) = T%} or the theorem {\small\verb%|- (e1 = e2) = F%}, as appropriate.

Given such a conversion, the function {\small\verb%INSERT_CONV%} returns a conversion that
maps a term of the form {\small\verb%"t INSERT {t1,...,tn}"%} to the theorem
{\par\samepage\setseps\small
\begin{verbatim}
   |- t INSERT {t1,...,tn} = {t1,...,tn}
\end{verbatim}
}
\noindent if {\small\verb%t%} is alpha-equivalent to any {\small\verb%ti%} in the set {\small\verb%{t1,...,tn}%}, or
if the supplied conversion proves {\small\verb%|- (t = ti) = T%} for any {\small\verb%ti%}.

\EXAMPLE
In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a
parameter and used to test equality of the inserted value {\small\verb%2%} with the
remaining elements of the set.
{\par\samepage\setseps\small
\begin{verbatim}
   #INSERT_CONV num_EQ_CONV "2 INSERT {1,SUC 1,3}";;
   |- {2,1,SUC 1,3} = {1,SUC 1,3}
\end{verbatim}
}
\noindent In this example, the supplied conversion {\small\verb%num_EQ_CONV%} is able to
prove that {\small\verb%2%} is equal to {\small\verb%SUC 1%} and the set is therefore reduced.  Note
that {\small\verb%"2 INSERT {1,SUC 1,3}"%} is just {\small\verb%"{2,1,SUC 1,3}"%}.

A call to {\small\verb%INSERT_CONV%} fails when the value being inserted is provably not
equal to any of the remaining elements:
{\par\samepage\setseps\small
\begin{verbatim}
   #INSERT_CONV num_EQ_CONV "1 INSERT {2,3}";;
   evaluation failed     INSERT_CONV
\end{verbatim}
}
\noindent But this failure can, if desired, be caught using {\small\verb%TRY_CONV%}.

The behaviour of the supplied conversion is irrelevant when the inserted value
is alpha-equivalent to one of the remaining elements:
{\par\samepage\setseps\small
\begin{verbatim}
   #INSERT_CONV NO_CONV "(y:*) INSERT {x,y,z}";;
   |- {y,x,y,z} = {x,y,z}
\end{verbatim}
}

\noindent The conversion {\small\verb%NO_CONV%} always fails, but {\small\verb%INSERT_CONV%} is
nontheless able in this case to prove the required result.  

Note that {\small\verb%DEPTH_CONV(INSERT_CONV conv)%} can be used to remove duplicate
elements from a finite set, but the following conversion is faster:
{\par\samepage\setseps\small
\begin{verbatim}
   #letrec REDUCE_CONV conv tm =
      (SUB_CONV (REDUCE_CONV conv) THENC (TRY_CONV (INSERT_CONV conv))) tm;;
   REDUCE_CONV = - : (conv -> conv)

   #REDUCE_CONV num_EQ_CONV "{1,2,1,3,2,4,3,5,6}";;
   |- {1,2,1,3,2,4,3,5,6} = {1,2,4,3,5,6}
\end{verbatim}
}

\FAILURE 
{\small\verb%INSERT_CONV conv%} fails if applied to a term not of the form
{\small\verb%"t INSERT {t1,...,tn}"%}.  A call {\small\verb%INSERT_CONV conv "t INSERT {t1,...,tn}"%}
fails unless {\small\verb%t%} is alpha-equivalent to some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
{\small\verb%|- (t = ti) = T%} for some {\small\verb%ti%}.

\SEEALSO
DELETE_CONV.

\ENDDOC

\DOC{SET\_INDUCT\_TAC}

\TYPE {\small\verb%SET_INDUCT_TAC : tactic%}\egroup

\SYNOPSIS
Tactic for induction on finite sets.

\DESCRIBE
{\small\verb%SET_INDUCT_TAC%} is an induction tacic for proving properties of finite
sets.  When applied to a goal of the form
{\par\samepage\setseps\small
\begin{verbatim}
   !s:(*)set. P[s]
\end{verbatim}
}
\noindent {\small\verb%SET_INDUCT_TAC%} reduces this goal to proving that the property
{\small\verb%\s.P[s]%} holds of the empty set and is preserved by insertion of an element
into an arbitrary finite set.  Since every finite set can be built up from the
empty set {\small\verb%"{}"%} by repeated insertion of values, these subgoals imply that
the property {\small\verb%\s.P[s]%} holds of all finite sets.

The tactic specification of {\small\verb%SET_INDUCT_TAC%} is:
{\par\samepage\setseps\small
\begin{verbatim}
                         A ?- !s.P
   ==================================================  SET_INDUCT_TAC
     A |- P[{}/s] 
     A u {P[s'/s], ~e IN s'} ?- P[e INSERT s'/s]
\end{verbatim}
}
\noindent where {\small\verb%e%} is a variable chosen so as not to appear free in the
assumptions {\small\verb%A%}, and {\small\verb%s'%} is a primed variant of {\small\verb%s%} that does not appear free
in {\small\verb%A%} (usually, {\small\verb%s'%} is just {\small\verb%s%}).

\FAILURE
{\small\verb%SET_INDUCT_TAC (A,g)%} fails unless {\small\verb%g%} has the form {\small\verb%!s.P%}, where the variable
{\small\verb%s%} has type {\small\verb%(ty)set%} for some type {\small\verb%ty%}.

\ENDDOC
\DOC{UNION\_CONV}

\TYPE {\small\verb%UNION_CONV : conv -> conv%}\egroup

\SYNOPSIS
Reduce {\small\verb%{t1,...,tn} UNION s%} to {\small\verb%t1 INSERT (... (tn INSERT s))%}.

\DESCRIBE 
The function {\small\verb%UNION_CONV%} is a parameterized conversion for reducing sets of
the form {\small\verb%"{t1,...,tn} UNION s"%}, where {\small\verb%{t1,...,tn}%} and {\small\verb%s%} are sets of
type {\small\verb%(ty)set%}. The first argument to {\small\verb%UNION_CONV%} is expected to be a
conversion that decides equality between values of the base type {\small\verb%ty%}.  Given
an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and {\small\verb%e2%} are terms of type {\small\verb%ty%}, this
conversion should return the theorem {\small\verb%|- (e1 = e2) = T%} or the theorem
{\small\verb%|- (e1 = e2) = F%}, as appropriate.

Given such a conversion, the function {\small\verb%UNION_CONV%} returns a conversion that
maps a term of the form {\small\verb%"{t1,...,tn} UNION s"%} to the theorem
{\par\samepage\setseps\small
\begin{verbatim}
   |- t UNION {t1,...,tn} = ti INSERT ... (tj INSERT s)
\end{verbatim}
}
\noindent where {\small\verb%{ti,...,tj}%} is the set of all terms {\small\verb%t%} that occur as
elements of {\small\verb%{t1,...,tn}%} for which the conversion {\small\verb%IN_CONV conv%} fails to
prove that {\small\verb%|- (t IN s) = T%} (that is, either by proving {\small\verb%|- (t IN s) = F%}
instead, or by failing outright).

\EXAMPLE
In the following example, {\small\verb%num_EQ_CONV%} is supplied as a parameter to
{\small\verb%UNION_CONV%} and used to test for membership of each element of the first
finite set {\small\verb%{1,2,3}%} of the union in the second finite set {\small\verb%{SUC 0,3,4}%}.
{\par\samepage\setseps\small
\begin{verbatim}
   #UNION_CONV num_EQ_CONV "{1,2,3} UNION {SUC 0,3,4}";;
   |- {1,2,3} UNION {SUC 0,3,4} = {2,SUC 0,3,4}
\end{verbatim}
}
\noindent The result is {\small\verb%{2,SUC 0,3,4}%}, rather than {\small\verb%{1,2,SUC 0,3,4}%},
because {\small\verb%UNION_CONV%} is able by means of a call to 
{\par\samepage\setseps\small
\begin{verbatim}
   IN_CONV num_EQ_CONV "1 IN {SUC 0,3,4}"
\end{verbatim}
}
\noindent to prove that {\small\verb%1%} is already an element of the set {\small\verb%{SUC 0,3,4}%}.

The conversion supplied to {\small\verb%UNION_CONV%} need not actually prove equality of
elements, if simplification of the resulting set is not desired.  For example:
{\par\samepage\setseps\small
\begin{verbatim}
   #UNION_CONV NO_CONV "{1,2,3} UNION {SUC 0,3,4}";;
   |- {1,2,3} UNION {SUC 0,3,4} = {1,2,SUC 0,3,4}
\end{verbatim}
}
\noindent In this case, the resulting set is just left unsimplified. Moreover,
the second set argument to {\small\verb%UNION%} need not be a finite set:
{\par\samepage\setseps\small
\begin{verbatim}
   #UNION_CONV NO_CONV "{1,2,3} UNION s";;
   |- {1,2,3} UNION s = 1 INSERT (2 INSERT (3 INSERT s))
\end{verbatim}
}
\noindent And, of course, in this case the conversion argument to {\small\verb%UNION_CONV%}
is irrelevant.

\FAILURE 
{\small\verb%UNION_CONV conv%} fails if applied to a term not of the form
{\small\verb%"{t1,...,tn} UNION s"%}.

\SEEALSO
IN_CONV.

\ENDDOC