Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

In the following paragraphs we give some links to advanced topics, marked with ``''. If you are reading this topic as part of the tutorial on the theorem prover, do not follow these links upon your first reading. Just take note of the existence of the facilities and ideas mentioned.

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

, we recommend that you do

(include-book "arithmetic/top-with-meta" :dir :system)which loads into ACL2 all the rules in one of the so-called ACL2 ``community books''. (

**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

**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 `corollary`

. Also, see the discussion of
`corollary`

in `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 and see congruence .

**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 ) meaning that the rule is to be applied even if that
hypothesis is not relieved -- but if the proof is successful the system will
turn its attention to all forced subgoals. You may similarly mark a
hypothesis so as to cause a case split, allowing the relief of the
hypothesis on one branch and spawning another branch explicitly denying the
hypothesis; see case-split . You may add a bogus hypothesis that looks at
the intended application of the rule and decides whether to apply the rule
or not, performing an arbitrary computation on the syntactic context of the
application; see syntaxp . By providing a `:match-free`

modifier to the
`:rewrite`

rule declaration in your rule-classes, you may tell ACL2 to try all
or only the first free variable value it guesses (see rule-classes
). You may provide a bogus hypothesis that computes from the
syntactic environment the values to guess for the free variables in a rule;
see bind-free . You may mark a term so that the rewriter does not
dive into it; see hide .

**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*`)`

, rules are applied to the *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
`(len (rev x))`

to `(len x)`

and suppose you wish to prove a theorem
about `(LEN (REV (CONS A B)))`

. Suppose `rev`

is defined in terms of
`append`

, as shown in programming-knowledge-taken-for-granted. Then
you might see a checkpoint in which the `(LEN (REV ...))`

above has been
simplified to `(LEN (APPEND (REV B) (LIST A)))`

instead of to
`(LEN (CONS A B))`

. Why wasn't your rule about `(len (rev x))`

applied?
The reason is that `(REV (CONS A B))`

rewrote to `(APPEND (REV B) (LIST A))`

before rules were applied to `(LEN (REV ...))`

. You need a rule about
`(len (append x y))`

, as you will see from the checkpoint.

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

, `g`

, and `h`

are functions defined so that the following two theorems are provable and
suppose you executed the following two events in the order shown:

(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

`(F (G A))`

, the result
will be `(H 2 A)`

, because the latter rule, `rule2`

, is applied
first. It is generally best not to have conflicting rules or, at least,
to understand how such conflicts are resolved. The system will warn you
when you propose a rule that conflicts with an existing one.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.