Make some

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

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))))) General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...)

Note: One `corollary` formula. To create the rules, we first
translate the formula, expanding all macros (see trans) and also
removing guard-holders. Next, we then flatten the `and` and
`implies` structure of the formula; for example, if the hypothesis or
conclusion is of the form `lambda`s as necessary in order to continue flattening; one may think of this
step as simply substituting to eliminate `let`, `let*`, and `mv-let` in order to expose more calls of

(implies (and h1 ... hn) concl)

where no hypothesis is a conjunction and `corollary` to a
sequence of conjuncts, each of which is of the form

(implies (and h1 ... hn) (equiv lhs rhs))

where

You can experiment by creating some rewrite rules using `defthm` and
then using `pr` to see how the rule was stored.

We create a `let`-expression, or a `if`-expression

A

ACL2's rewriting process has some optimizations, including the following.

- The suggestion, above, that the rewriter looks through the goal clause for
``any instance of the
lhs '' is not quite true.:Rewrite rules are never applied to quoted constants or any term inside a call of`hide`. If you want to rewrite a quoted constant use a: `rewrite-quoted-constant`rule. - The notion of ``a substitution that makes
lhs equal to the target term'' is a bit more generous than the most straightforward such notion. Suppose for example thatlhs is(f (+ 3 x)) and the target term is(f (+ 3 (g y)) . (Aside: ACL2 deals in so-called translated terms, so since+ is a macro,lhs and term would actually be(f (binary-+ '3 x)) and(f (binary-+ '3 (g y))) ; we will ignore this distinction, but if you want more information, see term.) Then of course, that substitution bindsx to(g y) . But now suppose that instead the target term is(f 10) . You may be surprised to learn that the substitution bindingx to7 makes(f (+ 3 x)) equal to(f 10) ; for example, the rewrite rule(equal (f (+ x 3)) (h x))) would rewrite(f 10) to(h 7) . This would also be the case iflhs were instead(f (+ x 3)) . This sort of optimization occurs when the new constant has`ACL2-count`no greater than the old constant. There are similar optimizations for* ,/ ,- , strings, symbols, and conses (for details see ACL2 source functionone-way-unify1-quotep-subproblems ). - When a term
t1 is rewritten to a new termt2 , the rewriter is then immediately applied tot2 . 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. - When the hypotheses and right-hand side are rewritten, ACL2 does not
really first apply the substitution and then rewrite; instead, 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.

- Force
- Identity function used to force a hypothesis
- Hide
- Hide a term from the rewriter
- Syntaxp
- Attach a heuristic filter on a rule
- Free-variables
- Free variables in rules
- Bind-free
- To bind free variables of a rewrite, definition, or linear rule
- Loop-stopper
- Limit application of permutative rewrite rules
- Backchain-limit
- Limiting the effort expended on relieving hypotheses
- Double-rewrite
- Cause a term to be rewritten twice
- Random-remarks-on-rewriting
- Some basic facts about the ACL2 rewriter
- Rewrite-lambda-object
- rewriting lambda objects in :FN slots
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Set-rw-cache-state
- Set the default rw-cache-state
- Simple
: `definition`and: `rewrite`rules used in preprocessing- Rewrite-stack-limit
- Limiting the stack depth of the ACL2 rewriter
- Rewrite-equiv
- Force ACL2 to perform substitution using a stylized equivalence hypothesis
- Set-rw-cache-state!
- Set the default rw-cache-state non-
`local`ly