GEN_REWRITE_CONV : (conv -> conv) -> thm list -> conv
SYNOPSIS
Rewrites a term, selecting terms according to a user-specified strategy.
DESCRIPTION
Rewriting in HOL is based on the use of equational theorems as left-to-right
replacements on the subterms of an object theorem. This replacement is
mediated by the use of REWR_CONV, which finds matches between left-hand sides
of given equations in a term and applies the substitution.
Equations used in rewriting are obtained from the theorem lists given as
arguments to the function. These are at first transformed into a form suitable
for rewriting. Conjunctions are separated into individual rewrites. Theorems
with conclusions of the form `~t` are transformed into the corresponding
equations `t = F`. Theorems `t` which are not equations are cast as
equations of form `t = T`.
If a theorem is used to rewrite a term, its assumptions are added to the
assumptions of the returned theorem. The matching involved uses variable
instantiation. Thus, all free variables are generalized, and terms are
instantiated before substitution. Theorems may have universally quantified
variables.
The theorems with which rewriting is done are divided into two groups, to
facilitate implementing other rewriting tools. However, they are considered in
an order-independent fashion. (That is, the ordering is an implementation
detail which is not specified.)
The search strategy for finding matching subterms is the first argument to the
rule. Matching and substitution may occur at any level of the term, according
to the specified search strategy: the whole term, or starting from any subterm.
The search strategy also specifies the depth of the search: recursively up to
an arbitrary depth until no matches occur, once over the selected subterm, or
any more complex scheme.
FAILURE CONDITIONS
GEN_REWRITE_CONV fails if the search strategy fails. It may also cause a
non-terminating sequence of rewrites, depending on the search strategy used.
USES
This conversion is used in the system to implement all other rewritings
conversions, and may provide a user with a method to fine-tune rewriting of
terms.
EXAMPLE
Suppose we have a term of the form:
`(1 + 2) + 3 = (3 + 1) + 2`
and we would like to rewrite the left-hand side with the
theorem ADD_SYM without changing the right hand side. This can be
done by using:
GEN_REWRITE_CONV (RATOR_CONV o ONCE_DEPTH_CONV) [ADD_SYM] mythm
Other rules, such as ONCE_REWRITE_CONV, would match and
substitute on both sides, which would not be the desirable result.