COMPOUND-RECOGNIZER

make a rule used by the typing mechanism 
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.


General Forms:
(implies (fn x) concl)
(implies (not (fn x)) concl)
(and (implies (fn x) concl1)
     (implies (not (fn x)) concl2))
(iff (fn x) concl)
(equal (fn x) concl)
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 third 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, the last two general forms above being equivalent. We explain how such rules are used by considering the individual forms.

Consider a rule of the first form, (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. 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.

The second general form addresses itself to 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 consps -- 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.

The third general form addresses itself 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 a rule of the third form is 

(and (implies (exprp x) (not (characterp x)))
     (implies (not (exprp x)) (or (consp x) (characterp x)))).
Finally, rules of the fourth class address the case where fn recognizes all and only the objects whose type is described. In this case, 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 (fn x) will not be recognized as a compound recognizer once it has been expanded.

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 or fourth forms. Proving a rule of the first form followed by one of the second only leaves the second fact in the data base.

Compound recognizer rules can be disabled with the effect that older rules about fn, if any, are exposed.

If you prove multiple compound recognizer rules 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 interpretions 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 know and then forget 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.