REWR_CONV is one of the basic building blocks for the implementation of
rewriting in the HOL system. In particular, the term replacement or rewriting
done by all the built-in rewriting rules and tactics is ultimately done by
applications of REWR_CONV to appropriate subterms. The description given
here for REWR_CONV may therefore be taken as a specification of the atomic
action of replacing equals by equals that is used in all these higher level
rewriting tools.
The first argument to REWR_CONV is expected to be an equational theorem
which is to be used as a left-to-right rewrite rule. The general form of this
theorem is:
A |- t[x1,...,xn] = u[x1,...,xn]
where x1, ..., xn are all the variables that occur free in the
left-hand side of the conclusion of the theorem but do not occur free in the
assumptions. Any of these variables may also be universally quantified at the
outermost level of the equation, as for example in:
A |- !x1...xn. t[x1,...,xn] = u[x1,...,xn]
Note that REWR_CONV will also work, but will give a generally
undesirable result (see below), if the right-hand side of the equation contains
free variables that do not also occur free on the left-hand side, as for
example in:
A |- t[x1,...,xn] = u[x1,...,xn,y1,...,ym]
where the variables y1, ..., ym do not occur free in
t[x1,...,xn].
If th is an equational theorem of the kind shown above, then
REWR_CONV th returns a conversion that maps terms of the form
t[e1,...,en/x1,...,xn], in which the terms e1, ..., en are free for
x1, ..., xn in t, to theorems of the form:
A |- t[e1,...,en/x1,...,xn] = u[e1,...,en/x1,...,xn]
That is, REWR_CONV th tm attempts to match the left-hand side of
the rewrite rule th to the term tm. If such a match is possible, then
REWR_CONV returns the corresponding substitution instance of th.
If REWR_CONV is given a theorem th:
A |- t[x1,...,xn] = u[x1,...,xn,y1,...,ym]
where the variables y1, ..., ym do not occur free in the
left-hand side, then the result of applying the conversion REWR_CONV th to
a term t[e1,...,en/x1,...,xn] will be:
A |- t[e1,...,en/x1,...,xn] = u[e1,...,en,v1,...,vm/x1,...,xn,y1,...,ym]
where v1, ..., vm are variables chosen so as to be free nowhere
in th or in the input term. The user has no control over the choice of the
variables v1, ..., vm, and the variables actually chosen may well be
inconvenient for other purposes. This situation is, however, relatively rare;
in most equations the free variables on the right-hand side are a subset of the
free variables on the left-hand side.
In addition to doing substitution for free variables in the supplied equational
theorem (or `rewrite rule'), REWR_CONV th tm also does type instantiation,
if this is necessary in order to match the left-hand side of the given rewrite
rule th to the term argument tm. If, for example, th is the theorem:
A |- t[x1,...,xn] = u[x1,...,xn]
and the input term tm is (a substitution instance of) an instance
of t[x1,...,xn] in which the types ty1, ..., tyi are substituted for the
type variables vty1, ..., vtyi, that is if:
tm = t[ty1,...,tyn/vty1,...,vtyn][e1,...,en/x1,...,xn]
then REWR_CONV th tm returns:
A |- (t = u)[ty1,...,tyn/vty1,...,vtyn][e1,...,en/x1,...,xn]
Note that, in this case, the type variables vty1, ..., vtyi must
not occur anywhere in the hypotheses A. Otherwise, the conversion will fail.