:rewrite rules (possibly conditional ones)
Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.
This doc topic discusses the rule-class :rewrite. If you want a general
discussion of how rewriting works in ACL2 and some guidance on how to
construct effective rewrite rules, see introduction-to-rewrite-rules-part-1
and then see introduction-to-rewrite-rules-part-2.
Examples:
(defthm plus-commutes ; Replace (+ a b) by (+ b a) provided
(equal (+ x y) (+ y x))) ; certain heuristics approve the
; permutation.
(defthm plus-commutes ; equivalent to the above
(equal (+ x y) (+ y x))
:rule-classes ((:rewrite :corollary (equal (+ x y) (+ y x))
:loop-stopper ((x y binary-+))
:match-free :all)))
(defthm append-nil ; Replace (append a nil) by a, if
(implies (true-listp x) ; (true-listp a) rewrites to t.
(equal (append x nil) x)))
(defthm append-nil ; as above, but with defaults and
(implies (true-listp x) ; a backchain limit
(equal (append x nil) x))
:rule-classes ((:rewrite :corollary (implies (true-listp x)
(equal (append x nil) x))
:backchain-limit-lst (3) ; or equivalently, 3
:match-free :all)))
(defthm member-append ; Replace (member e (append b c)) by
(implies ; (or (member e b) (member e c) in
(and ; contexts in which propositional
(true-listp x) ; equivalence is sufficient, provided
(true-listp y)) ; b and c are true-lists.
(iff (member e (append x y))
(or (member e x) (member e y)))))
Some Related Topics
:rewrite rule class object might create many rewrite rules from
the :corollary formula. To create the rules, we first translate
the formula, expanding all macros (see trans) and also expanding away calls
of all so-called ``guard holders,'' mv-list and return-last (the
latter resulting for example from calls of prog2$, mbe, or
ec-call), as well as expansions of the macro `the'. Next, we
eliminate all lambdas; one may think of this step as simply substituting
away every let, let*, and mv-let in the formula. We then
flatten the AND and IMPLIES structure of the formula; for
example, if the hypothesis or conclusion is of the form
(and (and term1 term2) term3), then we replace that by the ``flat'' term
(and term1 term2 term3). (The latter is actually an abbreviation for the
right-associated term (and term1 (and term2 term3)).) The result is a
conjunction of formulas, each of the form
(implies (and h1 ... hn) concl)where no hypothesis is a conjunction and
concl is neither a conjunction
nor an implication. If necessary, the hypothesis of such a conjunct may be
vacuous. We then further coerce each concl into the form
(equiv lhs rhs), where equiv is a known equivalence relation, by
replacing any concl not of that form by (iff concl t). A concl
of the form (not term) is considered to be of the form
(iff term nil). By these steps we reduce the given :corollary
to a sequence of conjuncts, each of which is of the form
(implies (and h1 ... hn)
(equiv lhs rhs))
where equiv is a known equivalence relation. See equivalence for a
general discussion of the introduction of new equivalence relations.
At this point, we check whether lhs and rhs are the same term; if so,
we cause an error, since this rule will loop. (But this is just a basic
check; the rule could loop in other cases, for example if rhs is an
instance of lhs; see loop-stopper.)We create a :rewrite rule for each such conjunct, if possible, and
otherwise cause an error. It is possible to create a rewrite rule from such
a conjunct provided lhs is not a variable, a quoted constant, a
let-expression, a lambda application, or an if-expression.
A :rewrite rule is used when any instance of the lhs occurs in a
context in which the equivalence relation is an admissible congruence
relation. First, we find a substitution that makes lhs equal to the
target term. Then we attempt to relieve the instantiated hypotheses of the
rule. Hypotheses that are fully instantiated are relieved by recursive
rewriting. Hypotheses that contain ``free variables'' (variables not
assigned by the unifying substitution) are relieved by attempting to guess a
suitable instance so as to make the hypothesis equal to some known assumption
in the context of the target. If the hypotheses are relieved, and certain
restrictions that prevent some forms of infinite regress are
met (see loop-stopper), the target is replaced by the instantiated rhs,
which is then recursively rewritten.
ACL2's rewriting process has undergone some optimization. In particular,
when a term t1 is rewritten to a new term t2, the rewriter is then
immediately applied to t2. On rare occasions you may find that you do
not want this behavior, in which case you may wish to use a trick involving
hide; see meta, near the end of that documentation.
In another optimization, when the hypotheses and right-hand side are rewritten, ACL2 does not really first apply the substitution and then rewrite; instead, it as it rewrites those terms it looks up the already rewritten values of the bound variables. Sometimes you may want those bindings rewritten again, e.g., because the variables occur in slots that admit additional equivalence relations. See double-rewrite.
See introduction-to-rewrite-rules-part-1 and see introduction-to-rewrite-rules-part-2 for an extended discussion of how to create effective rewrite rules.
