` `

apply a rewrite rule
Major Section: PROOF-CHECKER-COMMANDS

Examples: (rewrite reverse-reverse) -- apply the rewrite rule `reverse-reverse' (rewrite (:rewrite reverse-reverse)) -- same as above (rewrite 2) -- apply the second rewrite rule, as displayed by show-rewrites rewrite -- apply the first rewrite rule, as displayed by show-rewrites (rewrite transitivity-of-< ((y 7))) -- apply the rewrite rule transitivity-of-< with the substitution that associates 7 to the ``free variable'' yReplace the current subterm with a new term by applying a rewrite rule. IfGeneral Form: (rewrite &optional rule-id substitution)

`rule-id`

is a positive integer `n`

, then the `n`

th rewrite
rule as displayed by `show-rewrites`

is the one that is applied. If
`rule-id`

is `nil`

or is not supplied, then it is treated as the number
1. Otherwise, `rule-id`

should be either a rune of or name of a
rewrite rule. If a name is supplied, then any rule of that name may
be used. More explanation of all of these points follows below.
Consider first the following example. Suppose that the current
subterm is `(reverse (reverse y))`

and that there is a rewrite rule
called `reverse-reverse`

of the form

(implies (true-listp x) (equal (reverse (reverse x)) x)) .Then the instruction

`(rewrite reverse-reverse)`

would cause the
current subterm to be replaced by `y`

and would create a new goal with
conclusion `(true-listp y)`

. An exception is that if the top-level
hypotheses imply `(true-listp y)`

using only ``trivial reasoning''
(more on this below), then no new goal is created.
A rather important point is that if the `rule-id`

argument is a number
or is not supplied, then the system will store an instruction of the
form `(rewrite name ...)`

, where `name`

is the name of a rewrite rule;
this is in order to make it easier to replay instructions when there
have been changes to the history. Actually, instead of the name
(whether the name is supplied or calculated), the system stores the
rune if there is any chance of ambiguity. (Formally, ``ambiguity''
here means that the rune being applied is of the form
`(:rewrite name . index)`

, where index is not `nil`

.)

Speaking in general, then, a `rewrite`

instruction works as follows:

First, a rewrite rule is selected according to the arguments of the
`rewrite`

instruction. The selection is made as explained above under
``General Form'' above. The ``disambiguating rare arguments'' will
rarely be of interest to the user; as explained just above, the
stored instruction always contains the name of the rewrite rule, so
if there is more than one rule of that name then the system creates
and stores these extra arguments in order to make the resulting
instruction unambiguous, i.e., so that only one rewrite rule
applies. For what it's worth, they correspond respectively to the
fields of a rewrite rule record named `lhs`

, `rhs`

, `hyps`

, and `equiv`

.

Next, the left-hand side of the rule is matched with the current
subterm, i.e., a substitution `unify-subst`

is found such that if one
instantiates the left-hand side of the rule with `unify-subst`

, then
one obtains the current subterm. If this matching fails, then the
instruction fails.

Now an attempt is made to relieve the hypotheses, in much the same
sense as the theorem prover relieves hypotheses except that there is
no call to the rewriter. Essentially, this means that the
substitution `unify-subst`

is applied to the hypotheses and the system
then checks whether all hypotheses are ``clearly'' true in the
current context. If there are variables in the hypotheses of the
rewrite rule that do not occur in the left-hand side of the
conclusion even after the user-supplied substitution (default: `nil`

)
is applied, then a weak attempt is made to extend that substitution
so that even those hypotheses can be relieved. However, if even one
hypothesis remains unrelieved, then no automatic extension of the
substitution is made, and in fact hypotheses that contain even one
uninstantiated variable will remain unrelieved.

Finally, the instruction is applied as follows. The current subterm
is replaced by applying the final substitution, i.e., the extension
of `unify-subst`

by the user-supplied substitution which may in turn
be extended by the system (as explained above) in order to relieve
all hypotheses, to the right-hand side of the selected rewrite rule.
And, one new subgoal is created for each unrelieved hypothesis of
the rule, whose top-level hypotheses are the governors and top-level
hypotheses of the current goal and whose conclusion and current
subterm are the instance, by that same final substitution, of that
unrelieved hypothesis.

**Note:** The substitution argument should be a list whose elements
have the form `(variable term)`

, where `term`

may contain
abbreviations.