## REWRITE

make some `:rewrite` rules (possibly conditional ones)
```Major Section:  RULE-CLASSES
```

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.

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. Example `:``corollary` formulas from which `:rewrite` rules might be built are:

```Example:
(equal (+ x y) (+ y x))            replace (+ a b) by (+ b a) provided
certain heuristics approve the
permutation.

(implies (true-listp x)            replace (append a nil) by a, if
(equal (append x nil) x)) (true-listp a) rewrites to t

(implies                           replace (member a (append b c)) by
(and (eqlablep e)              (member a (append c b)) in contexts
(true-listp x)            in which propositional equivalence
(true-listp y))           is sufficient, provided (eqlablep a)
(iff (member e (append x y))   (true-listp b) and (true-listp c)
(member e (append y x)))) rewrite to t and the permutative
heuristics approve

Some Related Topics

BIND-FREE -- to bind free variables of a rewrite or linear rule

CASE-SPLIT -- like force but immediately splits the top-level goal on the hypothesis

DOUBLE-REWRITE -- cause a term to be rewritten twice

FORCE -- identity function used to force a hypothesis

FREE-VARIABLES -- free variables in rules

SYNTAXP -- attach a heuristic filter on a `:``rewrite`, `:``meta`, or `:``linear` rule

General Form:
(and ...
(implies (and ...hi...)
(implies (and ...hk...)
(and ...
(equiv lhs rhs)
...)))
...)
```
Note: One `: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; also see trans). Next, we eliminate all `lambda`s; 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.

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.