Make a rule used by the typing mechanism

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.

Examples: (defthm alistp-implies-true-listp-compound-recognizer (implies (alistp x) ; When (alistp x) is assumed true, add (true-listp x)) ; the additional hypothesis that x is :rule-classes :compound-recognizer) ; of primitive type true-listp. (defthm natp-compound-recognizer ; See discussion below. (equal (natp x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)

Before presenting the General Forms, we start with a motivating example:
the second `defthm` form above, which provides a nice example of a

(defun triple (x) (* 3 x)) (defthm triple-preserves-integerp (implies (integerp x) (integerp (triple x)))) (in-theory (disable triple natp))

If the above

(thm (implies (natp x) (integerp (triple x))) :hints (("Goal" :in-theory (disable natp-compound-recognizer))))

The problem is that when ACL2 tries to rewrite the term `rewrite` rule

General Forms: (implies (fn x) concl) ; (1) (implies (not (fn x)) concl) ; (2) (and (implies (fn x) concl1) ; (3) (implies (not (fn x)) concl2)) (if (fn x) concl1 concl2) ; (4) (iff (fn x) concl) ; (5) (equal (fn x) concl) ; (6)

where

The primitive ACL2 types and a suitable primitive recognizing expression for each are listed below.

type suitable primitive recognizer zero (equal x 0) one (equal x 1) negative integers (and (integerp x) (< x 0)) positive integers > 1 (and (integerp x) (> x 1)) negative ratio (and (rationalp x) (not (integerp x)) (< x 0)) positive ratio (and (rationalp x) (not (integerp x)) (> x 0)) complex rational (complex-rationalp x) nil (equal x nil) t (equal x t) other symbols (and (symbolp x) (not (equal x nil)) (not (equal x t))) proper conses (and (consp x) (true-listp x)) improper conses (and (consp x) (not (true-listp x))) strings (stringp x) characters (characterp x)

Thus, since the naturals comprise the types

(or (equal x 0) (equal x 1) (and (integerp x) (> x 1)))

However, it turns out that we also permit

Similarly, the true-lists could be specified by

(or (equal x nil) (and (consp x) (true-listp x)))

but we in fact allow

There are essentially four forms of

Consider form (1),

Form (2) is the symmetric case, when assuming `consp`s — then the theorem `consp`.

Forms (3) and (4), which are really equivalent, address themselves to the
case where one type may be deduced from

(and (implies (exprp x) (not (characterp x))) (implies (not (exprp x)) (or (consp x) (characterp x)))). (if (exprp x) (not (characterp x)) (or (consp x) (characterp x)))

Finally, rules of forms (5) and (6) address the case where

(iff (booleanp x) (or (equal x t) (equal x nil))).

Often it is best to disable

Every time you prove a new compound recognizer rule about

Compound recognizer rules can be disabled with the effect that older rules
about

If you prove more than one compound recognizer rule for a function, you may
see a **warning** message to the effect that the new rule is not as
``restrictive'' as the old. That is, the new rules do not give the rewriter
strictly more type information than it already had. The new rule is stored
anyway, overriding the old, if enabled. You may be playing subtle games with
enabling or rewriting. But two other interpretations are more likely, we
think. One is that you have forgotten about an earlier rule and should merely
print it out to make sure it says what you intend, and then discard your new
rule. The other is that you meant to give the system more information and the
system has simply been unable to extract the intended type information from
the term you placed in the conclusion of the new rule. Given our lack of
specificity in saying how type information is extracted from rules, you can
hardly blame yourself for this problem. Sorry. If you suspect you've been
burned this way, you should rephrase the new rule in terms of the primitive
recognizing expressions above and see if the warning is still given. It would
also be helpful to let us see your example so we can consider it as we
redesign this stuff.

Compound recognizer rules are similar to `forward-chaining`
rules in that the system deduces new information from the act of assuming
something true or false. If a compound recognizer rule were stored as a
forward chaining rule it would have essentially the same effect as described,
when it has any effect at all. The important point is that `forward-chaining` rules, because of their more general and expensive form, are
used ``at the top level'' of the simplification process: we forward chain from
assumptions in the goal being proved. But compound recognizer rules are built
in at the bottom-most level of the simplifier, where type reasoning is
done.

All that said, compound recognizer rules are a rather fancy, specialized
mechanism. It may be more appropriate to create `forward-chaining` rules instead of