ACL2-pc::rewrite
(primitive)
apply a rewrite rule
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'' y
(rewrite foo ((x 2) (y 3)) t)
-- apply the rewrite rule foo by substituting 2 and 3 for free
variables x and y, respectively, and also binding all other
free variables possible by using the current context
(hypotheses and governors)
General Form:
(rewrite &optional rule-id substitution instantiate-free)
Replace the current subterm with a new term by applying a rewrite or
definition rule. The replacement will be done according to the
information provided by the show-rewrites (sr) command.
If rule-id is a positive integer n, then the nth 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 symbol or else a :rewrite or
:definition rune. If a symbol is supplied, then any
(:rewrite or :definition) rule of that name may be used. We say
more about this, and describe the other optional arguments, 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) causes the current
subterm to be replaced by y and creates 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.
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. Except:
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 or definition rule is selected according to
the arguments of the rewrite instruction. The selection is made as
explained under ``General Form'' above.
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 match fails, then the instruction fails.
Next, an attempt is made to relieve (discharge) the hypotheses, much as the
theorem prover relieves hypotheses except that there is no call to the
rewriter. First, the substitution unify-subst is extended with the
substitution argument, which may bind free variables (see free-variables). Each hypothesis of the rule is then considered in turn,
from first to last. For each hypothesis, first the current substitution is
applied, and then the system checks whether the hypothesis is ``clearly'' true
in the current context. If there are variables in the hypotheses of the rule
that are not bound by the current substitution, then a weak attempt is made to
extend that substitution so that the hypothesis is present in the current
context (see ACL2-pc::hyps), much as would be done by the theorem
prover's rewriter.
If in the process above there are free variables (see free-variables), but the interactive proof-builder can see how to bind them
to relieve all hypotheses, then it will do so in both the
show-rewrites (sr) and rewrite commands. But normally, if even
one hypothesis remains unrelieved, then no automatic extension of the
substitution is made. Except, if instantiate-free is not nil, then
that extension to the substitution is kept. (Technical note: in the case of
an unrelieved hypothesis and a non-nil value of instantiate-free, if
a bind-free hypothesis produces a list of binding alists, then the
last of those alists is the one that is used to extend the substitution.)
Finally, the instruction is applied as follows. The current subterm is
replaced by applying the final substitution described above to the right-hand
side of the selected 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.
Remark: The substitution argument should be a list whose elements
have the form (variable term), where term may contain
abbreviations.
