ACL2-PC::REWRITE

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'' y

General Form:
(rewrite &optional rule-id substitution)

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)) .

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.