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

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

{(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

For example, let

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

Then

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

because we can instantiate

Observe that

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

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

and the subsumption property just means that

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

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