Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
`:`

`corollary`

formula from which a `:compound-recognizer`

rule might be
built is:

Example: (implies (alistp x) When (alistp x) is assumed true, (true-listp x)) add the additional hypothesis that x is of primitive type true-listp.

Before presenting the General Forms, we start with a motivating example. The
following provides a nice example of a `:compound-recognizer`

rule that is
built into ACL2.

(defthm natp-compound-recognizer (equal (natp x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)To see how this rule might be useful, consider the following (admittedly very simple) events.

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

`:compound-recognizer`

rule is disabled, then the following
trivial theorem fails as shown; we explain below.
(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
`(integerp (triple x))`

using the `:`

`rewrite`

rule
`triple-preserves-integerp`

, it needs to rewrite the hypothesis
`(integerp x) to c[t`

, but instead what is known is `(natp x)`

. If we
remove the hint, then the proof succeeds because the above
`:compound-recognizer`

rule tells ACL2 that when assuming `(natp x)`

to
be true, it should actually assume both `(integerp x)`

and `(<= 0 x)`

to
be true.

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

`fn`

is a Boolean valued function of one argument, `x`

is a
variable symbol, and the system can deduce some restriction on the primitive
type of `x`

from the assumption that `concl`

holds. The last restriction
is vague but one way to understand it is to weaken it a little to ``and
`concl`

is a non-tautological conjunction or disjunction of the primitive
type recognizers listed below.''The primitive ACL2 types and a suitable primitive recognizing expression for each are listed below.

type suitable primitive recognizer zero (equal x 0) negative integers (and (integerp x) (< x 0)) positive integers (and (integerp x) (> x 0)) 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, a suitable `concl`

to recognize the naturals would be
`(or (equal x 0) (and (integerp x) (> x 0)))`

but it turns out that we also
permit `(and (integerp x) (>= x 0))`

. Similarly, the true-lists could be
specified by

(or (equal x nil) (and (consp x) (true-listp x)))but we in fact allow

`(true-listp x)`

. When time permits we will document
more fully what is allowed or implement a macro that permits direct
specification of the desired type in terms of the primitives.There are essentially four forms of `:compound-recognizer`

rules, as the
forms labeled (3) and (4) above are equivalent, as are those labeled (5)
and (6). We explain how such rules are used by considering the individual
forms.

Consider form (1), `(implies (fn x) concl)`

. The effect of such a rule is
that when the rewriter assumes `(fn x)`

true, as it would while diving
through `(if (fn x) xxx ...)`

to rewrite `xxx`

, it restricts the type of
`x`

as specified by `concl`

. For example, if `concl`

is the term
`(integerp x)`

, then when rewriting `xxx`

, `x`

will be assumed to be an
integer. However, when assuming `(fn x)`

false, as necessary in
`(if (fn x) ... xxx)`

, the rule permits no additional assumptions about the
type of `x`

. For example, if `fn`

is `primep`

, i.e., the predicate
that recognizes prime numbers, then
`(implies (primep x) (and (integerp x) (>= x 0)))`

is a compound recognizer
rule of the first form. When `(primep x)`

is assumed true, the rewriter
gains the additional information that `x`

is a natural number. When
`(primep x)`

is assumed false, no additional information is gained --
since `x`

may be a non-prime natural or may not even be a natural.

Form (2) is the symmetric case, when assuming `(fn x)`

false permits type
restrictions on `x`

but assuming `(fn x)`

true permits no such
restrictions. For example, if we defined `exprp`

to be the recognizer for
well-formed expressions for some language in which all symbols, numbers,
character objects and strings were well-formed -- e.g., the well-formedness
rules only put restrictions on expressions represented by `consp`

s --
then the theorem `(implies (not (exprp x)) (consp x))`

is a rule of the
second form. Assuming `(exprp x)`

true tells us nothing about the type of
`x`

; assuming it false tells us `x`

is a `consp`

.

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

and a generally unrelated
type may be deduced from its negation. If we modified the expression
recognizer above so that character objects are illegal, then rules of the
forms (3) and (4) are

(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 `fn`

recognizes
all and only the objects whose type is described. In these cases, `fn`

is
really just a new name for some ``compound recognizers.'' The classic
example is `(booleanp x)`

, which is just a handy combination of two
primitive types:

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

Often it is best to disable `fn`

after proving that it is a compound
recognizer, since otherwise the term `(fn x)`

will be expanded and thus
disappear.

Every time you prove a new compound recognizer rule about `fn`

it overrides
all previously proved compound recognizer rules about `fn`

. Thus, if you
want to establish the type implied by `(fn x)`

and you want to establish
the type implied by `(not (fn x))`

, you must prove a compound recognizer
rule of the third, fourth, fifth, or sixth forms. Proving a rule of the
first form followed by one of the second only leaves the second fact in the
database.

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

, if any, are exposed.

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 `:compound-recognizer`

rules.