		Search-engine friendly clone of the ACL2 documentation.

Rule-classes

Built-in-clause

To build a clause into the simplifier

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.

Example:
(defthm acl2-count-abl
  (and (implies (and (true-listp x)
                     (not (equal x nil)))
                (< (acl2-count (abl x))
                   (acl2-count x)))
       (implies (and (true-listp x)
                     (not (equal nil x)))
                (< (acl2-count (abl x))
                   (acl2-count x))))
  :rule-classes :built-in-clause)

A :built-in-clause rule can be built from any formula other than propositional tautologies. Roughly speaking, the system uses the list of built-in clauses as the first method of proof when attacking a new goal. Any goal that is subsumed by a built in clause is proved ``silently.''

ACL2 maintains a set of ``built-in'' clauses that are used to short-circuit certain theorem proving tasks. We discuss this at length below. When a theorem is given the rule class :built-in-clause ACL2 flattens the implies and and structure of the :corollary formula so as to obtain a set of formulas whose conjunction is equivalent to the given corollary. It then converts each of these to clausal form and adds each clause to the set of built-in clauses.

The example above (regardless of the definition of abl) will build in two clauses,

{(not (true-listp x))
 (equal x nil)
 (< (acl2-count (abl x)) (acl2-count x))}

and

{(not (true-listp x))
 (equal nil x)
 (< (acl2-count (abl x)) (acl2-count x))}.

We now give more background.

Recall that a clause is a set of terms, implicitly representing the disjunction of the terms. Clause c1 is ``subsumed'' by clause c2 if some instance of c2 is a subset c1.

For example, let c1 be

{(not (consp l))
 (equal a (car l))
 (< (acl2-count (cdr l)) (acl2-count l))}.

Then c1 is subsumed by c2, shown below,

{(not (consp x))
 ; second term omitted here
 (< (acl2-count (cdr x)) (acl2-count x))}

because we can instantiate x in c2 with l to obtain a subset of c1.

Observe that c1 is the clausal form of

(implies (and (consp l)
              (not (equal a (car l))))
         (< (acl2-count (cdr l)) (acl2-count l))),

c2 is the clausal form of

(implies (consp l)
         (< (acl2-count (cdr l)) (acl2-count l)))

and the subsumption property just means that c1 follows trivially from c2 by instantiation.

The set of built-in clauses is just a set of known theorems in clausal form. Any formula that is subsumed by a built-in clause is thus a theorem. If the set of built-in theorems is reasonably small, this little theorem prover is fast. ACL2 uses the ``built-in clause check'' in four places: (1) at the top of the iteration in the prover — thus if a built-in clause is generated as a subgoal it will be recognized when that goal is considered, (2) within the simplifier so that no built-in clause is ever generated by simplification, (3) as a filter on the clauses generated to prove the termination of recursively defun'd functions and (4) as a filter on the clauses generated to verify the guards of a function.

The latter two uses are the ones that most often motivate an extension to the set of built-in clauses. Frequently a given formalization problem requires the definition of many functions which require virtually identical termination and/or guard proofs. These proofs can be short-circuited by extending the set of built-in clauses to contain the most general forms of the clauses generated by the definitional schemes in use.

The attentive user might have noticed that there are some recursive schemes, e.g., recursion by cdr after testing consp, that ACL2 just seems to ``know'' are ok, while for others it generates measure clauses to prove. Actually, it always generates measure clauses but then filters out any that pass the built-in clause check. When ACL2 is initialized, the clause justifying cdr recursion after a consp test is added to the set of built-in clauses. (That clause is c2 above.)

Note that only a subsumption check is made; no rewriting or simplification is done. Thus, if we want the system to ``know'' that cdr recursion is ok after a negative atom test (which, by the definition of atom, is the same as a consp test), we have to build in a second clause. The subsumption algorithm does not ``know'' about commutative functions. Thus, for predictability, we have built in commuted versions of each clause involving commutative functions. For example, we build in both

{(not (integerp x))
 (< 0 x)
 (= x 0)
 (< (acl2-count (+ -1 x)) (acl2-count x))}

and the commuted version

{(not (integerp x))
 (< 0 x)
 (= 0 x)
 (< (acl2-count (+ -1 x)) (acl2-count x))}

so that the user need not worry whether to write (= x 0) or (= 0 x) in definitions.

:built-in-clause rules added by the user can be enabled and disabled.