IT/Description/conv.tex

\chapter{Conversions}
\label{avra_conv}

A {\it conversion\/} in \HOL\ is a rule that maps a term to a theorem
expressing the equality of that term to some other term.  An example is the
rule for $\beta$-conversion:

\[\ml{(}\verb%\%x\ml{.}t_1\ml{)}t_2\quad\mapsto\quad
\ml{|- (}\verb%\%x\ml{.}t_1\ml{)}t_2\;\; \ml{=}  \;\;t_1[t_2/x] \]

\noindent Theorems\index{equational theorems, in HOL logic@equational theorems, in \HOL\ logic!produced by conversions}\index{conversions!purpose of} of this sort are used in
\HOL\ in a variety of contexts, to justify the replacement of particular terms
by semantically equivalent terms.

The \ML\ type of conversions is \ml{conv}:

\begin{hol}\begin{verbatim}
type conv = term -> thm
\end{verbatim}\end{hol}

\noindent For example, \ml{BETA\_CONV}\index{BETA_CONV@\ml{BETA\_CONV}}
is an \ML\ function of type \ml{conv} (\ie\ a conversion) that
expresses $\beta$-conversion in \HOL.  It produces the appropriate
equational theorem on $\beta$-redexes and fails elsewhere.

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- BETA_CONV;
> val it = fn : term -> thm

- BETA_CONV ``(\x. (\y. (\z. x + y + z)3)2) 1``;
> val it = |- (\x. (\y. (\z. x + (y + z))3)2)1 = (\y. (\z. 1 + (y + z))3)2 :
  thm

- BETA_CONV ``(\y. (\z. 1 + (y + z))3) 2``;
> val it = |- (\y. (\z. 1 + (y + z))3)2 = (\z. 1 + (2 + z))3 : thm

- BETA_CONV ``(\z. 1 + (2 + z)) 3``;
> val it = |- (\z. 1 + (2 + z))3 = 1 + (2 + 3) : thm

- BETA_CONV ``1 + (2 + 3)``;
! Uncaught exception:
! HOL_ERR
\end{verbatim}
\end{session}

The basic conversions, as well as a number of those commonly used, are
provided in \HOL.  There are also groups of
application-specific\index{conversions!application specific}
conversions to be found in some of the libraries.  (Of those provided,
some are derived and some, like \ml{BETA\_CONV} are taken as
axiomatic\footnote{A list of the axiomatic rules was supplied in
  Section~\ref{avra_standard}.}.)  In addition, \HOL\ provides a
collection of \ML\ functions enabling users to define new conversions
(as well as new rules and tactics) as functions of existing ones.
Some of these are described in Sections~\ref{avra1} and~\ref{avra2}.
The notion of conversions is inherited from Cambridge
\LCF;\index{LCF@\LCF!Cambridge} the underlying principles are
described in \cite{lcp-rewrite,new-LCF-man}.

Conversions such as \ml{BETA\_CONV}\index{beta-conversion, in HOL
  logic@beta-conversion, in \HOL\ logic!not expressible as a
  theorem}\index{theorems, in HOL logic@theorems, in \HOL\ logic!rules
  inexpressible as}\index{conversions!as families of equations}
represent infinite families of equations\footnote{This was also
  mentioned in Section~\ref{avra_standard}.}. They are particularly
useful in cases in which it is impossible to state, within the logic,
a single axiom or theorem instantiable to every equation in a
family\index{families of inferences, in HOL logic@families of
  inferences, in \HOL\ logic}.\footnote{In the case of
  $\beta$-conversion specifically, it is the substitution of one term
  for another in a context that is inexpressible; but in general,
  there is a variety of reasons that arise.} Instead, an \ML\
procedure returns the instance of the desired theorem for any given
term. This is also the reason that quite a few of the other rules in
\HOL\ are not stated instead as axioms or theorems. As rules,
conversions are distinguished with an \ML\ type abbreviation simply
because there are relatively many of them with the same type, and
because they return equational\index{theorems, in HOL logic@theorems,
  in \HOL\ logic!equational}\index{equational theorems, in HOL
  logic@equational theorems, in \HOL\ logic!produced by conversions}
theorems that lend themselves directly to term rewriting.\footnote{In
  fact, some ML functions have names with the suffix `{\tt \_CONV}'
  but do not have the type {\tt conv}; {\tt SUBST\_CONV}, for example,
  has type {\tt (thm \# term) list -> term -> conv}. Those that
  eventually produce conversion are thought of as `conversion
  schemas'.} In many \HOL\ applications, the main use of conversions
is to produce these equational theorems.  A few examples of
conversions are illustrated below.

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- NOT_FORALL_CONV ``~!x. (f:'a->'a) x = g x``;
> val it = |- ~(!x. f x = g x) = (?x. ~(f x = g x)) : thm

- CONTRAPOS_CONV ``(!x. f x = g x) ==> ((f:'a->'a) = g)``;
> val it = |- (!x. f x = g x) ==> (f = g) = ~(f = g) ==> ~!x. f x = g x : thm

- SELECT_CONV ``(@f:'a->'a. f x = g x)x = g x``;
> val it = |- ((@f. f x = g x)x = g x) = ?f. f x = g x

- EXISTS_UNIQUE_CONV ``?!z. (f:'a->'a) z = g z``;
> val it =
    |- (?!z. f z = g z) =
       (?z. f z = g z) /\ !z z'. (f z = g z) /\ (f z' = g z') ==> (z = z') :
  thm
\end{verbatim}
\end{session}

\noindent An example of an application specific conversion is
\ml{numLib}'s \ml{num\_CONV}:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- numLib.num_CONV ``2``;
> val it = |- 2 = SUC 1 : thm

- numLib.num_CONV ``1``;
> val it = |- 1 = SUC 0 : thm

- numLib.num_CONV ``0`` handle e => Raise e;

Exception raised at Num_conv.num_CONV:
Term either not a numeral or zero
! Uncaught exception:
! HOL_ERR
\end{verbatim}
\end{session}

Another application of conversions, related to the first, is in the
implementation of the existing rewriting tools, \ml{REWRITE\_CONV}
(Section~\ref{avra3}), \ml{REWRITE\_RULE} (Section~\ref{avra_rewrite})
and \ml{REWRITE\_TAC} (Chapter~\ref{tactics-and-tacticals}), which are
central to theorem proving in \HOL.  This use is explained in
Section~\ref{avra3}, both as an example and because users may have
occasion to construct rewriting tools of their own design, by similar
methods.  The next section introduces the conversion-building tools in
general.

\section{Indicating unchangedness}

All conversions may raise the special exception \ml{Conv.UNCHANGED} on
an input term \ml{t}, as a ``short-hand'' instead of returning the
reflexive theorem \ml{|-~t~=~t}.  This is done for efficiency reasons.
All of the connectives described below in Section~\ref{avra1} handle
this exception appropriately.  The standard function \ml{QCONV} is
provided to automatically handle this exception in contexts where it
would be inappropriate (typically where a conversion is being called
to provide a theorem directly).  \ml{QCONV}'s implementation is
\begin{alltt}
   fun QCONV c t = c t handle UNCHANGED => REFL t
\end{alltt}


\section{Conversion combining operators}
\label{avra1}

A term $u$ is said to {\it reduce\/}\index{reduction, by conversions}\index{conversions!reduction by} to a term $v$ by a conversion $c$ if
there exists a
finite sequence\index{sequencing!of conversions} of terms $t_1$, $t_2$, $\ldots$, $t_n$ such that:
\begin{myenumerate}
\item $u = t_1$ and $v = t_n$;
\item $c\ t_i$ evaluates to the theorem
$\ml{|- }t_i\;\ml{=}\;t_{i+1}$ for $1\leq i < n$;
\item The evaluation of $c\ t_n$ fails.
\end{myenumerate}

\noindent The first session of this chapter illustrates the reduction of
the term

\begin{hol}
\begin{verbatim}
   (\x. (\y. (\z. x + y + z)3)2)1
\end{verbatim}
\end{hol}

\noindent to \ml{1 + (2 + 3)} by the
conversion \ml{BETA\_CONV}, in a reduction sequence of length four:

\begin{hol}
\begin{verbatim}
   (\x. (\y. (\z. x + (y + z))3)2)1
   (\y. (\z. 1 + (y + z))3)2
   (\z. 1 + (2 + z))3
   1 + (2 + 3)
\end{verbatim}
\end{hol}

\noindent That is, \ml{BETA\_CONV} applies to each term of the sequence,
except the fourth and last, to give a theorem equating that term to
the next term. Therefore, each term of the sequence, from the second
on, can be extracted from the theorem for the previous term; namely,
it is the right hand side of the conclusion.  The whole reduction can
therefore be accomplished by repeated application of \ml{BETA\_CONV}
to the terms of the sequence as they are generated.

\index{alternation!of conversions|(} To transform \ml{BETA\_CONV} to
achieve this effect, two operators on
conversions\index{conversions!operators on|(} are introduced.  The
first one, infixed, is \ml{THENC}, which sequences conversions.

\begin{holboxed}
\index{THENC@\ml{THENC}|pin}
\begin{verbatim}
   op THENC : conv -> conv -> conv
\end{verbatim}
\end{holboxed}

\noindent If $c_1\ t_1$ evaluates to $\Gamma_1\ml{ |- }t_1\ml{=}t_2$ and
$c_2\ t_2$ evaluates to $\Gamma_2\ml{ |- }t_2\ml{=}t_3$, then
$\ml{(}c_1\ \ml{THENC}\ c_2\ml{)}\ t_1$ evaluates to $\Gamma_1\cup
\Gamma_2\ml{\ |-\ }t_1\ml{=}t_3$. If the evaluation of $c_1\ t_1$ or
the evaluation of $c_2\ t_2$ fails, then so does the evaluation of
$c_1\ \ml{THENC}\ c_2$. \ml{THENC} is justified by the transitivity of
equality.

The second, also infixed, is \ml{ORELSEC}; this applies a second
conversion if the application of the first one fails.

\begin{holboxed}
\index{ORELSEC@\ml{ORELSEC}|pin}
\begin{verbatim}
   op ORELSEC : conv -> conv -> conv
\end{verbatim}
\end{holboxed}

\noindent $\ml{(}c_1\ \ml{ORELSEC}\ c_2\ml{)}\ t$ evaluates to $c_1\ t$
if that evaluation succeeds, and to $c_2\ t$ otherwise. (The failure
to evaluate is detected via the \ML\ failure construct.)

The functions \ml{THENC} and \ml{ORELSEC} are used to define the
desired operator, \ml{REPEATC}\index{repetition!of conversions}, which
successively\index{successive application!conversion operator for}
applies a conversion until it fails:

\begin{holboxed}
\index{REPEATC@\ml{REPEATC}|pin}
\begin{verbatim}
   REPEATC : conv -> conv
\end{verbatim}
\end{holboxed}

\noindent \ml{REPEATC}\ $c$ is intuitively equivalent to:

\begin{hol}
\begin{alltt}
   (\m{c} THENC \m{c} THENC ... THENC \m{c} THENC ...) ORELSEC ALL_CONV
\end{alltt}
\end{hol}

\noindent It is defined recursively:\footnote{Note that because ML is a
  call-by-value language, the extra argument $t$ is needed in the
  definition of {\tt REPEATC}; without it the definition would loop.
  There is a similar problem with the tactical {\tt REPEAT}; see
  Chapter~\ref{tactics-and-tacticals}.}

\begin{hol}
\begin{verbatim}
   fun REPEATC c t = ((c THENC (REPEATC c)) ORELSEC ALL_CONV) t
\end{verbatim}
\end{hol}

The current example term can thus be completely reduced by use of
\ml{BETA\_CONV} transformed by the \ml{REPEATC} operator:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- REPEATC BETA_CONV;
> val it = fn : term -> thm

- REPEATC BETA_CONV ``(\x. (\y. (\z. x + y + z)3)2)1``;
> val it = |- (\x. (\y. (\z. x + (y + z))3)2)1 = 1 + (2 + 3) : thm
\end{verbatim}
\end{session}
\index{alternation!of conversions|)}

\ml{BETA\_CONV} applies to terms of a certain top level form only,
namely to $\beta$-redexes, and fails on terms of any other form.  In
addition, no number of repetitions of \ml{BETA\_CONV} will
$\beta$-reduce {\it arbitrary\/} $\beta$-redexes embedded in terms.
For example, the term shown below fails even at the top level because
it is not a $\beta$-redex:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- BETA_CONV ``(((\x.(\y.(\z. x + y + z))) 1) 2) 3``;
! Uncaught exception:
! HOL_ERR

- is_abs ``(((\x.(\y.(\z. x + y + z))) 1) 2)``;
> val it = false : bool
\end{verbatim}
\end{session}

\noindent
The $\beta$-redex {\small\verb|(\w.w)3|} is not affected in the third
input of the session shown below, because of its position in the
structure of the whole term.  This is so even though the whole term is
reduced, and the subterm at top level could be reduced:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#BETA_CONV "(\z. x + y + z)3";;
|- (\z. x + (y + z))3 = x + (y + 3)

#BETA_CONV "(\w.w)3";;
|- (\w. w)3 = 3

#REPEATC BETA_CONV "(\z. x + y + z)((\w.w)3)";;
|- (\z. x + (y + z))((\w. w)3) = x + (y + ((\w. w)3))
\end{verbatim}\end{session}

To produce, from a conversion $c$, a conversion that applies $c$ to every
subterm of a term, the function \ml{DEPTH\_CONV} can be applied to $c$:

\begin{holboxed}
\index{DEPTH_CONV@\ml{DEPTH\_CONV}|pin}
\begin{verbatim}
   DEPTH_CONV : conv -> conv
\end{verbatim}\end{holboxed}

\noindent \ml{DEPTH\_CONV}$\ c$ is a conversion

\[t\quad\mapsto\quad \ml{|- }t\ml{ = }t'\]

\noindent where $t'$ is obtained from $t$ by replacing every subterm
$u$ by $v$ if $u$ reduces to $v$ by $c$. (Subterms for which
$c\ u$ fails are left unchanged.) The definition leaves open the search strategy;
in fact,
\ml{DEPTH\_CONV}$\ c$\index{DEPTH_CONV@\ml{DEPTH\_CONV}!search strategy of}
 traverses a term\footnote{That is, it traverses
the abstract parse tree of the term.} `bottom up', once, and left-to-right,
repeatedly applying $c$ to each subterm until no longer applicable.
This helps with the two problems thus far:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#DEPTH_CONV BETA_CONV "(((\x.(\y.(\z. x + y + z))) 1) 2) 3";;
|- (\x y z. x + (y + z))1 2 3 = 1 + (2 + 3)

#DEPTH_CONV BETA_CONV "(\z. x + y + z)((\w.w)3)";;
|- (\z. x + (y + z))((\w. w)3) = x + (y + 3)
\end{verbatim}\end{session}

It may happen, however,
that the result of such a conversion still contains subterms
that could themselves be reduced at top level. For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let t = "(\f.\x.f x)(\n.n+1)";;
t = "(\f x. f x)(\n. n + 1)" : term

#DEPTH_CONV BETA_CONV t;;
|- (\f x. f x)(\n. n + 1) = (\x. (\n. n + 1)x)
\end{verbatim}\end{session}

\noindent The function \ml{TOP\_DEPTH\_CONV}
 does more
searching and reduction than
\ml{DEPTH\_CONV}: it replaces
every subterm
$u$ by $v'$ if $u$ reduces to $v$ by $c$ and $v$ {\it recursively\/} reduces
to $v'$ by {\tt TOP\_DEPTH\_CONV}$\ c$.\footnote{Readers interested
in characterizing the search strategy of {\tt TOP\_DEPTH\_CONV} should
study the \ML\ definitions near the end of this section.}

\begin{holboxed}
\index{TOP_DEPTH_CONV@\ml{TOP\_DEPTH\_CONV}|pin}
\begin{verbatim}
   TOP_DEPTH_CONV : conv -> conv
\end{verbatim}\end{holboxed}

\noindent Thus:

\begin{session}\begin{verbatim}
#TOP_DEPTH_CONV BETA_CONV t;;
|- (\f x. f x)(\n. n + 1) = (\x. x + 1)
\end{verbatim}\end{session}

Finally, the simpler function \ml{ONCE\_DEPTH\_CONV} is provided:

\begin{holboxed}
\index{ONCE_DEPTH_CONV@\ml{ONCE\_DEPTH\_CONV}|pin}
\begin{verbatim}
   ONCE_DEPTH_CONV : conv -> conv
\end{verbatim}\end{holboxed}

\noindent $\ml{ONCE\_DEPTH\_CONV}\ c\ t$ applies $c$ once to the first
term (and only the first term)
on which it succeeds in a top-down traversal:

\begin{session}\begin{verbatim}
#ONCE_DEPTH_CONV BETA_CONV t;;
|- (\f x. f x)(\n. n + 1) = (\x. (\n. n + 1)x)

#ONCE_DEPTH_CONV BETA_CONV "(\x. (\n. n + 1)x)";;
|- (\x. (\n. n + 1)x) = (\x. x + 1)
\end{verbatim}\end{session}

The equational theorems returned by conversions are not always
useful in equational form.  To make the results more useful for theorem
proving,
a conversion can be converted to a rule or a tactic, using the functions
\ml{CONV\_RULE} or \ml{CONV\_TAC}, respectively.


\begin{holboxed}
\index{CONV_RULE@\ml{CONV\_RULE}|pin}
\index{CONV_TAC@\ml{CONV\_TAC}|pin}
\begin{verbatim}
   CONV_RULE : conv -> thm -> thm
   CONV_TAC  : conv -> tactic
\end{verbatim}\end{holboxed}

\noindent $\ml{CONV\_RULE}\ c\ \ml{(|- }t\ml{)}$ returns $\ml{|- }t'$, where
$c\ t$ evaluates to the equation
$\ml{|-}\ t\ml{=}t'$.
$\ml{CONV\_TAC}\ c$ is a tactic that
converts the conclusion of a goal using $c$. \ml{CONV\_RULE} is defined by:

\begin{hol}\begin{verbatim}
   let CONV_RULE c th = EQ_MP (c(concl th)) th
\end{verbatim}\end{hol}

\noindent (The validation of \ml{CONV\_TAC} also
uses \ml{EQ\_MP}\footnote{For \ml{EQ\_MP}, see ~\ref{avra_eq_mp}.}.)
For example, the built-in rule \ml{BETA\_RULE} reduces some
of the $\beta$-redex subterms of a term.

\begin{holboxed}
\index{BETA_RULE@\ml{BETA\_RULE}|pin}
\begin{verbatim}
   BETA_RULE : thm -> thm
\end{verbatim}\end{holboxed}

\noindent It is defined by:

\begin{hol}\begin{verbatim}
   let BETA_RULE = CONV_RULE(DEPTH_CONV BETA_CONV)
\end{verbatim}\end{hol}

\noindent The search invoked by \ml{BETA\_RULE}
is adequate for some purposes but not others; for example,
the first use shown below but not the second:

\begin{session}\begin{verbatim}
#BETA_RULE(ASSUME "(((\x.(\y.(\z. x + y + z))) 1) 2) 3 < 10");;
. |- (1 + (2 + 3)) < 10

#let th = ASSUME "NEXT = ^t";;
th = . |- NEXT = (\f x. f x)(\n. n + 1)

#BETA_RULE th;;
. |- NEXT = (\x. (\n. n + 1)x)

#BETA_RULE(BETA_RULE th);;
. |- NEXT = (\x. x + 1)
\end{verbatim}\end{session}

\noindent A more powerful
$\beta$-reduction rule
that used the second  search strategy could be defined as shown below
(this is not built into \HOL).

\begin{session}\begin{verbatim}
#let TOP_BETA_RULE = CONV_RULE(TOP_DEPTH_CONV BETA_CONV);;
TOP_BETA_RULE = - : (thm -> thm)

#TOP_BETA_RULE th;;
. |- NEXT = (\x. x + 1)
\end{verbatim}\end{session}

\ml{TOP\_DEPTH\_CONV} is the traversal
strategy used by the \HOL\ rewriting tools described in Section~\ref{avra3}.
\index{conversions!operators on|)}

\section{Writing compound conversions}
\label{avra2}

\index{conversions!functions for building|(}
There are several other conversion operators in \HOL, which,
together with \ml{THENC}, \ml{ORELSEC} and \ml{REPEATC} are available
for building more complex conversions, as well as rules, tactics, and so on.
These are described below; several are good illustrations themselves
of how functions are built using conversions. The section culminates
with the explanation of how \ml{DEPTH\_CONV}, \ml{TOP\_DEPTH\_CONV}, and
\ml{ONCE\_DEPTH\_CONV} are built.

The conversion \ml{NO\_CONV} is an identity for
\ml{ORELSEC}\index{ORELSEC@\ml{ORELSEC}}, useful
in building functions.

\begin{holboxed}
\index{NO_CONV@\ml{NO\_CONV}|pin}
\begin{verbatim}
   NO_CONV : conv
\end{verbatim}\end{holboxed}

\noindent $\ml{NO\_CONV}\ t$ always fails.

The function \ml{FIRST\_CONV}
returns $c\ t$ for the first conversion $c$, in a list of conversions,
for which the evaluation of $c\ t$ succeeds.

\begin{holboxed}
\index{FIRST_CONV@\ml{FIRST\_CONV}|pin}
\begin{verbatim}
   FIRST_CONV : conv list -> conv
\end{verbatim}\end{holboxed}

\noindent $\ml{FIRST\_CONV [}c_1\ml{;}\ldots\ml{;}c_n\ml{]}$ is equivalent,
intuitively, to:

\begin{hol}
\index{ORELSEC@\ml{ORELSEC}}
\begin{alltt}
   \m{c\sb{1}} ORELSEC \m{c\sb{2}} ORELSEC \m{\ldots} ORELSEC \m{c\sb{n}}
\end{alltt}\end{hol}

\noindent It is defined by:

\begin{hol}\begin{verbatim}
   let FIRST_CONV cl t =
       itlist $ORELSEC cl NO_CONV t ? failwith `FIRST_CONV`;;
\end{verbatim}\end{hol}

The conversion \ml{ALL\_CONV} is an identity for \ml{THENC},\index{THENC@\ml{THENC}} useful
in building functions.

\begin{holboxed}
\index{ALL_CONV@\ml{ALL\_CONV}|pin}
\begin{verbatim}
   ALL_CONV : conv
\end{verbatim}\end{holboxed}

\noindent \ml{ALL\_CONV\ $t$} evaluates to \ml{|-\ $t$=$t$}. It is
defined as being identical to \ml{REFL}.\index{REFL@\ml{REFL}}

The function \ml{EVERY\_CONV} applies a list of conversions in sequence.

\begin{holboxed}
\index{EVERY_CONV@\ml{EVERY\_CONV}|pin}
\begin{verbatim}
   EVERY_CONV : conv list -> conv
\end{verbatim}\end{holboxed}

\noindent $\ml{EVERY\_CONV [}c_1\ml{;}\ldots\ml{;}c_n\ml{]}$ is equivalent,
intuitively, to:

\begin{hol}
\index{THENC@\ml{THENC}}
\begin{alltt}
   \m{c\sb{1}} THENC \m{c\sb{2}} THENC \m{\ldots} THENC \m{c\sb{n}}
\end{alltt}\end{hol}

\noindent It is defined by:

\begin{hol}\begin{verbatim}
   let EVERY_CONV cl t =
       itlist $THENC cl ALL_CONV t ? failwith `EVERY_CONV`
\end{verbatim}\end{hol}

The operator \ml{CHANGED\_CONV} converts one conversion to another that
fails on arguments that it cannot change.

\begin{holboxed}
\index{CHANGED_CONV@\ml{CHANGED\_CONV}|pin}
\begin{verbatim}
   CHANGED_CONV : conv -> conv
\end{verbatim}\end{holboxed}

\noindent If $c\ t$ evaluates to $\ml{|-}\ t\ml{=}t'$, then
$\ml{CHANGED\_CONV}\ c\ t$  also evaluates to $\ml{|-}\ t\ml{=}t'$,
unless $t$ and $t'$ are the same (up to $\alpha$-conversion),
in which case it fails.

The operator \ml{TRY\_CONV} maps one conversion to another that
always succeeds, by replacing failures with the identity conversion.

\begin{holboxed}
\index{TRY_CONV@\ml{TRY\_CONV}|pin}
\begin{verbatim}
   TRY_CONV : conv
\end{verbatim}\end{holboxed}

\noindent If $c\ t$ evaluates to $\ml{|-}\ t\ml{=}t'$, then
$\ml{TRY\_CONV}\ c\ t$  also evaluates to $\ml{|-}\ t\ml{=}t'$. If
$c\ t$ fails, then $\ml{TRY\_CONV}\ c\ t$ evaluates
to  $\ml{|-}\ t\ml{=}t$. \ml{TRY\_CONV} is implemented by:

\begin{hol}\begin{verbatim}
   let TRY_CONV c = c ORELSEC ALL_CONV
\end{verbatim}\end{hol}

\noindent It is used in the implementation of
\ml{TOP\_DEPTH\_CONV} (given later).

There are a number of operators for applying conversions to the
immediate subterms of a term. These use the \ML\ functions:


\begin{holboxed}
\index{MK_COMB@\ml{MK\_COMB}|pin}
\index{MK_ABS@\ml{MK\_ABS}|pin}
\begin{verbatim}
   MK_COMB : thm # thm -> thm
   MK_ABS  : thm -> thm
\end{verbatim}\end{holboxed}

\noindent \ml{MK\_COMB} and \ml{MK\_ABS} implement the following derived rules:

$${\Gamma_1 \ml{ |- } u_1\ml{=}v_1\qquad
 \Gamma_2\ml{ |- } u_2\ml{=}v_2 \over
\Gamma_1\cup\Gamma_2\ml{ |- } u_1\ u_2 \ml{=} v_1\ v_2}\quad\ml{MK\_COMB}$$

$${\Gamma\ml{ |- !}x\ml{.}u\ml{=}v \over
\Gamma\ml{ |- (}\verb%\%x\ml{.}u\ml)=(\verb%\%x\ml{.}v\ml{)}}\quad\ml{MK\_ABS}$$

\noindent The function \ml{SUB\_CONV}
applies a conversion to the immediate subterms
of a term.

\begin{holboxed}
\index{SUB_CONV@\ml{SUB\_CONV}|pin}
\begin{verbatim}
   SUB_CONV : conv
\end{verbatim}\end{holboxed}

\noindent In particular:

\begin{itemize}
\item \ml{SUB\_CONV}$\;\;c\;\;$\ml{"}$x$\ml{"} $\;=\;$\ \ml{|- }$x$\ml{=}$x$;
\item \ml{SUB\_CONV}$\;\;c\;\;$\ml{"}$u\;v$\ml{"} $\;=\;$ \ml{|- }$u\;v$\ml{=}$u'\;v'$,\ \  if
$c\;\;u$\ $=$\ \ml{|- }$u$\ml{=}$u'$ and
$c\;\;v$\ $=$\ \ml{|- }$v$\ml{=}$v'$;
\item\ml{SUB\_CONV}$\;\;c\;\;$\ml{"}{\small\verb%\%}$x$\ml{.}$u$\ml{"} $\;=\;$
\ml{|- (}{\small\verb%\%}$x$\ml{.}$u$\ml{) = (}{\small\verb%\%}$x$\ml{.}$u'$\ml{)}, \ \ if
$c\;\;u$\ $=$\ \ml{|- }$u$\ml{=}$u'$.
\end{itemize}

\noindent \ml{SUB\_CONV} is implemented\index{conversions!implementation of, in ML@implementation of, in \ML|(} in terms of
\ml{MK\_COMB} and \ml{MK\_ABS}:

\begin{hol}\begin{verbatim}
   let SUB_CONV c t =
       if is_comb t then
          (let rator,rand = dest_comb t in
           MK_COMB (c rator, c rand))
       if is_abs t then
          (let bv,body = dest_abs t in
           let bodyth = c body in
           MK_ABS (GEN bv bodyth))
                   else (ALL_CONV t)
\end{verbatim}\end{hol}

\noindent \ml{SUB\_CONV}, too, is used in the definitions of
\ml{DEPTH\_CONV} and \ml{TOP\_DEPTH\_CONV}.

Three other useful conversion operators, also for applying conversions
to the immediate subterms of a term, are as follows:


\begin{holboxed}
\index{RATOR_CONV@\ml{RATOR\_CONV}|pin}
\index{RAND_CONV@\ml{RAND\_CONV}|pin}
\index{ABS_CONV@\ml{ABS\_CONV}|pin}
\begin{verbatim}
   RATOR_CONV : conv -> conv
   RAND_CONV  : conv -> conv
   ABS_CONV   : conv -> conv
\end{verbatim}\end{holboxed}

\noindent \ml{RATOR\_CONV}$\ c$ converts the operator of an application using
$c$; \ml{RAND\_CONV}$\ c$ converts the operand of an application; and
\ml{ABS\_CONV}$\ c$ converts the body of an abstraction. Combinations
of these are useful for applying conversions to particular subterms.
These are implemented by:

\begin{hol}\begin{verbatim}
   let RATOR_CONV c t =
    (let rator,rand = dest_comb t in
     MK_COMB (c rator, REFL rand)) ? failwith `RATOR_CONV`

   let ABS_CONV c t =
    (let bv,body = dest_abs t in
     let bodyth = c body in
     MK_ABS (GEN bv bodyth)) ? failwith `ABS_CONV`
\end{verbatim}\end{hol}

\noindent The following
is an example session illustrating these immediate subterm conversions
(recalling that the expression $t_1\ml{+}t_2$
actually parses as $\ml{+}\ t_1\ t_2$).

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let t = "(\x.x+1)m + (\x.x+2)n";;
t = "((\x. x + 1)m) + ((\x. x + 2)n)" : term

#RAND_CONV BETA_CONV t;;
|- ((\x. x + 1)m) + ((\x. x + 2)n) = ((\x. x + 1)m) + (n + 2)

#RATOR_CONV (RAND_CONV BETA_CONV) t;;
|- ((\x. x + 1)m) + ((\x. x + 2)n) = (m + 1) + ((\x. x + 2)n)
\end{verbatim}\end{session}

\noindent Finally, the definitions of \ml{DEPTH\_CONV} and
\ml{TOP\_DEPTH\_CONV} are given below.


\begin{hol}
\index{DEPTH_CONV@\ml{DEPTH\_CONV}}
\index{TOP_DEPTH_CONV@\ml{TOP\_DEPTH\_CONV}}
\begin{verbatim}
   letrec DEPTH_CONV c t =
    (SUB_CONV (DEPTH_CONV c) THENC (REPEATC c)) t

   letrec TOP_DEPTH_CONV c t =
    (REPEATC c THENC
     (TRY_CONV
       (CHANGED_CONV (SUB_CONV (TOP_DEPTH_CONV c)) THENC
        TRY_CONV(c THENC TOP_DEPTH_CONV c)))) t

   letrec ONCE_DEPTH_CONV c t =
    (c ORELSEC (SUB_CONV (ONCE_DEPTH_CONV c))) t
\end{verbatim}\end{hol}
\index{conversions!functions for building|)}
\index{conversions!implementation of, in ML@implementation of, in \ML|)}

\noindent Note that the extra argument {\small\verb%t%} is needed to stop
these definitions looping (because \ML\ is a call-by-value language).
Note also that the actual definition of {\small\verb%ONCE_DEPTH_CONV%}
used in the system has been optimised to use failure to avoid
rebuilding unchanged subterms.


\section{Built in conversions}\label{built-in-conv}


Many conversions are predefined in \HOL; only those likely to be of
general interest are listed here.

\subsection{Generalized beta-reduction}\label{genbeta}

The conversion:


\begin{holboxed}\index{PAIRED_BETA_CONV@\ml{PAIRED\_BETA\_CONV}|pin}
\begin{verbatim}
   PAIRED_BETA_CONV : conv
\end{verbatim}\end{holboxed}

\noindent does
generalized beta-conversion of tupled lambda abstractions applied to
tuples.

Given the term:

\begin{hol}\begin{verbatim}
   "(\(x1, ... ,xn).t) (t1, ... ,tn)"
\end{verbatim}\end{hol}

\noindent \ml{PAIRED\_BETA\_CONV} proves that:

\begin{hol}\begin{verbatim}
   |- (\(x1, ... ,xn). t[x1,...,xn]) (t1, ... ,tn)  =  t[t1, ... ,tn]
\end{verbatim}\end{hol}

\noindent The conversion works for arbitrarily nested tuples.  For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#PAIRED_BETA_CONV "(\((a,b),(c,d)). [a;b;c;d]) ((1,2),(3,4))";;
|- (\((a,b),c,d). [a;b;c;d])((1,2),3,4) = [1;2;3;4]
\end{verbatim}\end{session}

\subsection{Arithmetical conversions}

The conversion:

\begin{holboxed}\index{ADD_CONV@\ml{ADD\_CONV}|pin}
\begin{verbatim}
   ADD_CONV : conv
\end{verbatim}\end{holboxed}

\noindent does addition by formal proof.
If $n$ and $m$ are numerals then
{\small\verb%ADD_CONV "%}$n\ $\ml{+}$\ m$\ml{"}
returns the theorem {\small\verb%|- %}$n\ $\ml{+}$\ m\ $\ml{=}$\  s$,
where $s$ is the numeral denoting the sum of $n$ and $m$.  For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#ADD_CONV "1 + 2";;
|- 1 + 2 = 3

#ADD_CONV "0 + 1000";;
|- 0 + 1000 = 1000

#ADD_CONV "101 + 102";;
|- 101 + 102 = 203
\end{verbatim}\end{session}


The next conversion decides the equality of natural number
constants.

\begin{holboxed}\index{num_EQ_CONV@\ml{num\_EQ\_CONV}|pin}
\begin{verbatim}
   num_EQ_CONV : conv
\end{verbatim}\end{holboxed}

\noindent If $n$ and $m$ are terms constructed from numeral constants
and the successor function \ml{SUC}, then:
{\small\verb%num_EQ_CONV "%}$n$\ml{=}$m$\ml{"}
returns:

\begin{hol}\begin{alltt}
   |- (\(n\)=\(m\)) = T   \(\mbox{if \(n\) and \(m\) represent the same number}\)
   |- (\(n\)=\(m\)) = F   \(\mbox{if \(n\) and \(m\) represent different numbers}\)
\end{alltt}\end{hol}

\noindent In addition, {\small\verb%num_EQ_CONV "%}$t\ $\ml{=}$\ t$\ml{"}
returns: {\small\verb%|- (%}$t$\ml{=}$t${\small\verb%) = T%}

\subsection{List processing conversions}

There are two useful built-in conversions for lists:

\begin{holboxed}
\index{LENGTH_CONV@\ml{LENGTH\_CONV}|pin}
\index{list_EQ_CONV@\ml{list\_EQ\_CONV}|pin}
\begin{verbatim}
   LENGTH_CONV : conv
   list_EQ_CONV: conv
\end{verbatim}\end{holboxed}

\ml{LENGTH\_CONV}: computes the length of a list.
A call to:

\begin{hol}\begin{alltt}
   LENGTH_CONV "LENGTH[\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)]"
\end{alltt}\end{hol}

\noindent generates the theorem:

\begin{hol}\begin{alltt}
   |- LENGTH [\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)] = n
\end{alltt}\end{hol}

The other conversion, \ml{list\_EQ\_CONV}, proves or disproves the
equality of two lists, given
a conversion for deciding the equality of elements.
A call to:

\begin{hol}\begin{alltt}
   list_EQ_CONV \(conv\) "[\(u\sb{1}\);\(\ldots\);\(u\sb{n}\)] = [\(v\sb{1}\);\(\ldots\);\(v\sb{m}\)]"
\end{alltt}\end{hol}

\noindent returns: {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ F} if:

\begin{myenumerate}
\item {\small\verb%~%}\ml{($n$=$m$)} or
\item \ml{$conv$} proves {\small\verb%|- (%}$u_i\ $\ml{=}$\ v_i$\ml{)\ =\ F}
for any $1\leq i \leq m$.
\end{myenumerate}

\noindent {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ T} is returned if:

\begin{myenumerate}

\item \ml{($n$=$m$)} and \ml{$u_i$} is syntactically identical to
\ml{$v_i$} for $1\leq i \leq m$, or
\item \ml{($n$=$m$)} and \ml{$conv$} proves
{\small\verb%|- (%}$u_i$\ml{=}$v_i$\ml{)=T} for $1\leq i \leq n$.
\end{myenumerate}

\subsection{Simplifying {\tt let}-terms}\label{let-terms}
\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!simplification of}

A conversion for reducing {\tt let}-terms is now provided.

\begin{holboxed}\index{let_CONV@\ml{let\_CONV}|pin}
\begin{verbatim}
   let_CONV : conv
\end{verbatim}\end{holboxed}

\noindent Given a term:

\begin{hol}\begin{alltt}
   "let \(v\sb{1}\) = \(t\sb{1}\) and \(\cdots\) and \(v\sb{n}\) = \(t\sb{n}\) in \(t[v\sb{1},\ldots,v\sb{n}]\)"
\end{alltt}\end{hol}

\noindent \ml{let\_CONV} proves that:

\begin{hol}\begin{alltt}
   |- let \(v\sb{1}\) = \(t\sb{1}\) and \(\cdots\) and \(v\sb{n}\) = \(t\sb{n}\) in \(t[v\sb{1},\ldots,v\sb{n}]\)  =  \(t[t\sb{1},\ldots,t\sb{n}]\)
\end{alltt}\end{hol}

\noindent The \ml{$v_i$}'s can take any one of the following forms:

\begin{myenumerate}
\item Variables:    \ml{x} etc.
\item Tuples:   \ml{(x,y)}, \ml{(a,b,c)}, \ml{((a,b),(c,d))} etc.
\item Applications: \ml{f (x,y) z}, \ml{f x} etc.
\end{myenumerate}

\noindent Variables are just substituted for. With tuples, the substitution is
done component-wise, and function applications are effectively
rewritten in the body of the {\tt let}-term.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let_CONV "let x = 1 in x+y";;
|- (let x = 1 in x + y) = 1 + y

#let_CONV "let (x,y) = (1,2) in x+y";;
|- (let (x,y) = 1,2 in x + y) = 1 + 2

#let_CONV "let f x = 1 and f y = 2 in (f 10) + (f 20)";;
|- (let f x = 1 and f y = 2 in (f 10) + (f 20)) = 2 + 2

#let_CONV "let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))";;
|- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) =
(((0 + 2) + 1) + 2) + 1

#CONV_RULE(DEPTH_CONV ADD_CONV)it;;
|- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) = 6

#let_CONV "let f x y = x+y in f 1";;  % NB: partial application %
|- (let f x y = x + y in f 1) = (\y. 1 + y)
\end{verbatim}\end{session}

\subsection{Skolemization}\index{Skolemization}

Two conversions are provided for a higher-order version of
Skolemization (using existentially quantified function variables
rather than first-order Skolem constants).

The conversion

\begin{holboxed}\index{X_SKOLEM_CONV@\ml{X\_SKOLEM\_CONV}|pin}
\begin{verbatim}
   X_SKOLEM_CONV : term -> conv
\end{verbatim}\end{holboxed}

\noindent takes a variable parameter, \ml{$f$} say, and
proves:

\begin{hol}\begin{alltt}
   |- (!\(x\sb{1}\) \(\ldots\) \(x\sb{n}\). ?\(y\). \(t[x\sb{1},\ldots,x\sb{n},y]\)  =  (?\(f\). !\(x\sb{1}\) \(\ldots\) \(x\sb{n}\). \(t[x\sb{1},\ldots,x\sb{n},f x\sb{1}\ldots x\sb{n}]\)
\end{alltt}\end{hol}

\noindent for any input term
\ml{!$x_1\ \ldots\ x_n$.\ ?$y$. $t[x_1,\ldots,x_n,y]$}.
Note that when $n=\ml{0}$, this
is equivalent to alpha-conversion:

\begin{hol}\begin{alltt}
  |- (?\(y\). \(t[y]\)) = (?\(f\). \(t[f]\))
\end{alltt}\end{hol}

\noindent and that the conversion fails if there is already a free
variable \ml{$f$} of the appropriate type in the input term. For example:

\begin{hol}\begin{alltt}
  X_SKOLEM_CONV "f:num->*" "!n:num. ?x:*. x = (f n)"
\end{alltt}\end{hol}

\noindent will fail.  The conversion \ml{SKOLEM\_CONV} is
like \ml{X\_SKOLEM\_CONV}, except that it
uses a primed variant of the name of the existentially quantified variable
as the name of the skolem function it introduces.  For example:

\begin{hol}\begin{alltt}
  SKOLEM_CONV "!x. ?y. P x y"
\end{alltt}\end{hol}

\noindent proves that:

\begin{hol}\begin{alltt}
  |- ?y. !x. P x (y x)
\end{alltt}\end{hol}


\subsection{Quantifier movement conversions}
\index{quantifiers!conversions for}
\index{conversions!quantifier movement}

A complete and systematically-named set of conversions for moving quantifiers
inwards and outwards through the logical connectives {\small\verb%~%},
{\small\verb%/\%}, {\small\verb%\/%}, and {\small\verb%==>%} is provided.
The naming scheme is based on the following
atoms:

\begin{hol}\begin{alltt}
   <\(quant\)> := FORALL | EXISTS
   <\(conn\)>  := NOT | AND | OR | IMP
   [\(dir\)]   := LEFT | RIGHT          \({\it (optional)}\)
\end{alltt}\end{hol}


The conversions for moving quantifiers inwards are called:

\begin{hol}\begin{alltt}
   <\(quant\)>_<\(conn\)>_CONV
\end{alltt}\end{hol}

\noindent where the quantifier \ml{<$quant$>} is to be moved inwards
through \ml{<$conn$>}.

The conversions for moving quantifiers outwards are called:

\begin{hol}\begin{alltt}
   [\(dir\)]_<\(conn\)>_<\(quant\)>_CONV
\end{alltt}\end{hol}

\noindent where \ml{<$quant$>} is to be moved outwards
through \ml{<$conn$>}, and the optional
\ml{[$dir$]} identifies which operand (left or right) contains the quantifier.
The complete set is:

\begin{hol}\begin{verbatim}
   NOT_FORALL_CONV    |- ~(!x.P) = ?x.~P
   NOT_EXISTS_CONV    |- ~(?x.P) = !x.~P
   EXISTS_NOT_CONV    |- (?x.~P) = ~!x.P
   FORALL_NOT_CONV    |- (!x.~P) = ~?x.P
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   FORALL_AND_CONV         |- (!x. P /\ Q) = (!x.P) /\ (!x.Q)
   AND_FORALL_CONV         |- (!x.P) /\ (!x.Q) = (!x. P /\ Q)
   LEFT_AND_FORALL_CONV    |- (!x.P) /\ Q = (!x'. P[x'/x] /\ Q)
   RIGHT_AND_FORALL_CONV   |- P /\ (!x.Q) = (!x'. P /\ Q[x'/x])
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   EXISTS_OR_CONV          |- (?x. P \/ Q) = (?x.P) \/ (?x.Q)
   OR_EXISTS_CONV          |- (?x.P) \/ (?x.Q) = (?x. P \/ Q)
   LEFT_OR_EXISTS_CONV     |- (?x.P) \/ Q = (?x'. P[x'/x] \/ Q)
   RIGHT_OR_EXISTS_CONV    |- P \/ (?x.Q) = (?x'. P \/ Q[x'/x])
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   FORALL_OR_CONV
     |- (!x.P \/ Q) = P \/ !x.Q          [x not free in P]
     |- (!x.P \/ Q) = (!x.P) \/ Q        [x not free in Q]
     |- (!x.P \/ Q) = (!x.P) \/ (!x.Q)   [x not free in P or Q]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   OR_FORALL_CONV
     |- (!x.P) \/ (!x.Q) = (!x.P \/ Q)   [x not free in P or Q]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   LEFT_OR_FORALL_CONV    |- (!x.P) \/ Q = !x'. P[x'/x] \/ Q
   RIGHT_OR_FORALL_CONV   |- P \/ (!x.Q)  = !x'. P \/ Q[x'/x]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   EXISTS_AND_CONV
     |- (?x.P /\ Q) = P /\ ?x.Q          [x not free in P]
     |- (?x.P /\ Q) = (?x.P) /\ Q        [x not free in Q]
     |- (?x.P /\ Q) = (?x.P) /\ (?x.Q)   [x not free in P or Q]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   AND_EXISTS_CONV
     |- (?x.P) /\ (?x.Q) = (?x.P /\ Q)   [x not free in P or Q]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   LEFT_AND_EXISTS_CONV    |- (?x.P) /\ Q = ?x'. P[x'/x] /\ Q
   RIGHT_AND_EXISTS_CONV   |- P /\ (?x.Q)  = ?x'. P /\ Q[x'/x]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   FORALL_IMP_CONV
     |- (!x.P ==> Q) = P ==> !x.Q          [x not free in P]
     |- (!x.P ==> Q) = (?x.P) ==> Q        [x not free in Q]
     |- (!x.P ==> Q) = (?x.P) ==> (!x.Q)   [x not free in P or Q]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   LEFT_IMP_FORALL_CONV   |- (!x.P) ==> Q = !x'. P[x/'x] ==> Q
   RIGHT_IMP_FORALL_CONV  |- P ==> (!x.Q) = !x'. P ==> Q[x'/x]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   EXISTS_IMP_CONV
     |- (?x.P ==> Q) = P ==> ?x.Q          [x not free in P]
     |- (?x.P ==> Q) = (!x.P) ==> Q        [x not free in Q]
     |- (?x.P ==> Q) = (!x.P) ==> (?x.Q)   [x not free in P or Q]
\end{verbatim}\end{hol}

\begin{hol}\begin{verbatim}
   LEFT_IMP_EXISTS_CONV   |- (?x.P) ==> Q = !x'. P[x/'x] ==> Q
   RIGHT_IMP_EXISTS_CONV  |- P ==> (?x.Q) = ?x'. P ==> Q[x'/x]
\end{verbatim}\end{hol}


\section{Rewriting tools}
\label{avra3}

The rewriting tool\index{rewriting!as based on conversions|(}
\ml{REWRITE\_RULE} was introduced
in Chapter~\ref{derived-rules}.
There are also rewriting conversion like \ml{REWRITE\_CONV}.
All of the various rewriting tools provided in \HOL\
are implemented by use of conversions.
Certain new tools could also be built in a similar way.

The rewriting primitive in \HOL\ is \ml{REWR\_CONV}:

\begin{holboxed}
\index{REWR_CONV@\ml{REWR\_CONV}|pin}
\begin{verbatim}
   REWR_CONV : thm -> conv
\end{verbatim}\end{holboxed}

\noindent $\ml{REWR\_CONV (}\Gamma\ml{ |- }u \ml{=}v\ml{) }t$ evaluates to a
theorem $\Gamma\ml{ |- }t\ml{=}t'$
if $t$ is an instance (by type and/or variable instantiation)
of $u$ and $t'$ is the corresponding instance of $v$.
The first argument to \ml{REWR\_CONV} can be quantified.
Below is an illustration.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#REWR_CONV ADD1 "SUC 0";;
Theorem ADD1 autoloaded from theory `arithmetic`.
ADD1 = |- !m. SUC m = m + 1

|- SUC 0 = 0 + 1
\end{verbatim}\end{session}

\noindent All subterms of $t$ can be rewritten according to
an equation $th$ using\index{rewriting!use of DEPTH_CONV in@use of \ml{DEPTH\_CONV} in}\index{DEPTH_CONV@\ml{DEPTH\_CONV}!use of, in rewriting tools}

\[ \ml{DEPTH\_CONV(REWR\_CONV}\;\;th\ml{)}  \]

\noindent as shown below. The function \ml{"PRE"} is the usual
predecessor function.

\begin{session}\begin{verbatim}
#DEPTH_CONV (REWR_CONV ADD1) "SUC(SUC 0) = PRE(SUC 2)";;
|- (SUC(SUC 0) = PRE(SUC 2)) = ((0 + 1) + 1 = PRE(2 + 1))
\end{verbatim}\end{session}

In itself, this is not a very useful rewriting tool, but a collection
of others have been developed for use in \HOL.
All of the rewriting tools are, in fact, logically derived, and are
based on conversions similar to \ml{DEPTH\_CONV}.
They have been optimized in various ways, so their
implementation is in some cases rather complex and is not given here.
The conversions, rules and tactics for rewriting all take a list of
theorems\index{theorems, in HOL logic@theorems, in \HOL\ logic!as rewrite rules}
to be used as rewrites.
The theorems in the list need not be in simple equational form
(\eg\ a conjunction of equations is permissible); but are
converted to equational form
automatically (and internally).
(For example, a conjunction of equations is split into
its constituent conjuncts.)  There are also a number
of standard equations (representing common tautologies) held in
the \ML\ variable
\ml{basic\_rewrites},\index{basic-rewrites@\ml{basic-rewrites}} and these
are used by some of the rewriting tools. All the
built-in rewriting tools are listed below, for
reference, beginning with the rules.
(All are fully
described in \REFERENCE.)

The prefix `\ml{PURE\_}' indicates
that the built-in equations in \ml{basic\_rewrites} are not used,
(\ie\ only those
given explicitly are used).  The prefix `\ml{ONCE\_}' indicates that the
tool
makes only one rewriting pass through the expression
(this is useful to avoid divergence). It is based on \ml{ONCE\_DEPTH\_CONV},
while the other tools traverse using \ml{TOP\_DEPTH\_CONV}.

The rewriting converions are:

\begin{hol}\begin{verbatim}
   REWRITE_CONV                : thm list -> conv
   PURE_REWRITE_CONV           : thm list -> conv
   ONCE_REWRITE_CONV           : thm list -> conv
   PURE_ONCE_REWRITE_CONV      : thm list -> conv
\end{verbatim}\end{hol}

The basic rewriting rules are:

\begin{hol}\begin{verbatim}
   REWRITE_RULE                      : thm list -> thm -> thm
   PURE_REWRITE_RULE                 : thm list -> thm -> thm
   ONCE_REWRITE_RULE                 : thm list -> thm -> thm
   PURE_ONCE_REWRITE_RULE            : thm list -> thm -> thm
\end{verbatim}\end{hol}

\noindent The prefix `\ml{ASM\_}'
indicates that the rule rewrites using the assumptions
of the theorem as rewrites.

\begin{hol}\begin{verbatim}
   ASM_REWRITE_RULE                  : thm list -> thm -> thm
   PURE_ASM_REWRITE_RULE             : thm list -> thm -> thm
   ONCE_ASM_REWRITE_RULE             : thm list -> thm -> thm
   PURE_ONCE_ASM_REWRITE_RULE        : thm list -> thm -> thm
\end{verbatim}\end{hol}

\noindent The prefix `\ml{FILTER\_}'
indicates that the rule only rewrites with
those assumptions of the theorem satisfying the predicate supplied.

\begin{hol}\begin{verbatim}
   FILTER_ASM_REWRITE_RULE           : (term -> bool) -> thm list -> thm -> thm
   FILTER_PURE_ASM_REWRITE_RULE      : (term -> bool) -> thm list -> thm -> thm
   FILTER_ONCE_ASM_REWRITE_RULE      : (term -> bool) -> thm list -> thm -> thm
   FILTER_PURE_ONCE_ASM_REWRITE_RULE : (term -> bool) -> thm list -> thm -> thm
\end{verbatim}\end{hol}

\noindent Tactics\index{rewriting!list of tactics for|(} are introduced in Chapter~\ref{tactics-and-tacticals},
but are listed here for reference.
The tactics corresponding to the above rules are the following:

\begin{hol}\begin{verbatim}
   REWRITE_TAC                       : thm list -> tactic
   PURE_REWRITE_TAC                  : thm list -> tactic
   ONCE_REWRITE_TAC                  : thm list -> tactic
   PURE_ONCE_REWRITE_TAC             : thm list -> tactic
\end{verbatim}\end{hol}

\noindent The prefix `\ml{ASM\_}'
indicates that the tactic rewrites using the assumptions
of the goal as rewrites.

\begin{hol}\index{ASM_REWRITE_TAC@\ml{ASM\_REWRITE\_TAC}}
\begin{verbatim}
   ASM_REWRITE_TAC                   : thm list -> tactic
   PURE_ASM_REWRITE_TAC              : thm list -> tactic
   ONCE_ASM_REWRITE_TAC              : thm list -> tactic
   PURE_ONCE_ASM_REWRITE_TAC         : thm list -> tactic
\end{verbatim}\end{hol}

\noindent The prefix `\ml{FILTER\_}'
indicates that the tactic only rewrites with
those assumptions of the goal satisfying the predicate supplied.

\begin{hol}\begin{verbatim}
   FILTER_ASM_REWRITE_TAC            : (term -> bool) -> thm list -> tactic
   FILTER_PURE_ASM_REWRITE_TAC       : (term -> bool) -> thm list -> tactic
   FILTER_ONCE_ASM_REWRITE_TAC       : (term -> bool) -> thm list -> tactic
   FILTER_PURE_ONCE_ASM_REWRITE_TAC  : (term -> bool) -> thm list -> tactic
\end{verbatim}\end{hol}
\index{rewriting!as based on conversions|)}
\index{rewriting!list of tactics for|)}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "description"
%%% End: