A grab bag of advice and information on rewriting

In the following paragraphs we give some links to advanced topics,
marked with ``

Arithmetic: If your goal theorem involves even trivial arithmetic,
such as adding or subtracting

(include-book "arithmetic/top-with-meta" :dir :system)

which loads into ACL2 all the rules in one of the so-called ACL2
``community books''. (*Books* are certified files of definitions,
lemmas, etc., usually prepared by other ACL2 users and explicitly shared with
the community. The ACL2 installation instructions suggest downloading the
community books.) The book "top-with-meta" is the most elementary and most
widely used arithmetic book. Other community books include
"arithmetic-5/top" and various hardware and floating-point arithmetic books;
if including "arithmetic/top-with-meta" isn't sufficient, you could try

**Rules Concluding with Arithmetic Inequalities**: If you are tempted to
create a rewrite rule with an arithmetic inequality as its conclusion or
left-hand side, think again. Inequalities such as

(<= (len (delete e x)) (len x))

make poor left-hand sides for rewrite rules. For example, the inequality above does not match the target

(<= (LEN (DELETE E X)) (+ 1 (LEN X)))

even though it is sufficient to prove the target (given some simple
arithmetic). We recommend that if you have a theorem that establishes an
arithmetic inequality, you make it a *linear* rule. See linear

**Rearranging Formulas Before Making Rules**: It is possible to
rearrange the propositional structure of a proved formula before processing it
as a rule. This allows you to state a theorem one way ``for publication'' and
rearrange it to be stored as a more effective rule. See introduction-to-the-database (a tutorial topic you'll come to later) and its
discussion of the concept of `rule-classes`

**Rewriting with New Equivalence Relations**: You may introduce new
*equivalence* relations, like ``set-equal'' or ``is-a-permutation'' and
cause the rewriter to replace equivalents by equivalents in suitable contexts,
where you use *congruence* rules to inform ACL2 of where these more
relaxed notions of equivalence may be used; see equivalence

**Pragmatic Advice to Control Rules**: You may attach various
*pragmas* to a rule that allow you rather fine heuristic control over
whether and how the rule is applied. For example, you may mark a hypothesis
to be *forced* (see force

**Programming Your Own Rewriter**: If you cannot find a way to use
rewrite rules to make the transformations you desire, you might investigate
the use of *metafunctions*. A metafunction is just a little theorem
prover of your own design. It takes as input a list structure representing a
term and returns a list structure representing a term. If you can prove that
the meaning of the input and output terms are equivalent, you can extend the
ACL2 simplifier to call your metafunction. See meta

**The Order in which Targets are Rewritten**: The rewriter sweeps
through terms ``inside-out'' otherwise known as ``left-most innermost first''.
Thus, before trying to apply rewrite rules to *f a1 ... an**ai*. This has the good effect of normalizing
the *ai*.

This fact might help you understand why sometimes your rules ``don't seem
to fire.'' For example, suppose you have a rule for rewriting

**The Order in which Rules are Tried**: The rewriter tries the most
recently proved rules first. For example, suppose

(defthm rule1 (equal (f (g x)) (h 1 x))) (defthm rule2 (equal (f (g x)) (h 2 X)))

Then if rewrite rules are applied to

If you were reading this topic as part of the tutorial introduction to the
theorem prover, use your browser's **Back Button** now to return to introduction-to-rewrite-rules-part-2.