Selecting which kind of rule to create

Successful ACL2 users generally direct many of their proved theorems to be stored as rules, which can be applied automatically in subsequent proof attempts. See rule-classes for a detailed discussion of the kinds of rules that can be created. Here, we give a brief introduction to rule-classes that may suffice for most ACL2 users.

The workhorse for ACL2 proof attempts is generally the application of rewrite rules. When you prove a theorem stated with `defthm`, ACL2
stores it as a rewrite rule unless either the

Most successful ACL2 users make only sparing use of other kinds of rules
besides rewrite rules. When in doubt, the default is probably best: the
absence of any `defthm` event, which
is equivalent to

time egrep -e ':rule-classes .*type-prescription' --include='*.l*sp' -ri .

Below, we sometimes speak of the ``conclusion'' of a formula. For many
rule classes, this is simply the formula itself unless the formula is of the
form

- If the conclusion is a call of a primitive recognizer or a compound
recognizer, or the negation of such — for example,
(true-listp (f x y)) — consider making a type-prescription rule. (For relevant background on recognizers, see compound-recognizer, which also describes how to make a rule that designates a function as a compound-recognizer.) But note that hypotheses of such a rule are proved (``relieved'') by ACL2 only usingtype reasoning. If you want rewriting to be used for relieving the hypotheses, you can wrap them in `force`or`case-split`. - If the conclusion is an inequality or negated inequality, consider making
a linear rule, but generally only if you can identify a reasonable
maximal term, which very roughly is a syntactially largest term that binds all
the variables. For example, the formula
(< (f x y) (g y z)) might not make a good linear rule. For a more careful discussion of maximal terms, see linear. - If the formula is a term in normal form (not simplifiable by your rewrite
rules) that tends to be an explicit hypothesis in some of your theorems,
consider making it a forward-chaining rule. For example, if you are
reasoning about a finite state machine (such as an interpreter) and your
theorems tend to have the hypothesis
(good-state-p st) , and your formula is(good-state-p (foo st)) , then that formula is a good candidate for a forward-chaining rule. - If the rule looks like a recursive definition
(equal (f x1 x2 ..) (... (f ...) ...)) , consider making a definition rule. - When you want to control the simplifier rather than just turning rules (especially rewrite rules) loose on your terms, consider using meta rules or clause-processor rules.

There are other rule classes that can be useful. See rule-classes for a complete list.