This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

CLAUSE-PROCESSOR    make or apply a :clause-processor rule (goal-level simplifier)

Also see DEFINE-TRUSTED-CLAUSE-PROCESSOR for documentation of
an analogous utility that does not require the clause-processor to be
proved correct.  But please read the present documentation before
reading about that utility.  Both utilities designate functions
"clause-processors".  Such functions must be executable -- hence not
constrained by virtue of being introduced in the signature of an
encapsulate -- and must respect stobj and output arity restrictions.
For example, something like (car (mv ...)) is illegal; also see
SIGNATURE.

We begin this documentation with an introduction, focusing on an
example, and then conclude with details.  You might find it most useful
simply to look at the examples in distributed directory
books/clause-processors/; see file Readme.lsp in that directory.

A :clause-processor rule installs a simplifier at the level of goals,
where a goal is represented as a _clause_: a list of terms that is
implicitly viewed as a disjunction (the application of OR).  For
example, if ACL2 prints a goal in the form (implies (and p q) r), then
the clause might be the one-element list containing the internal
representation of this term -- (implies (if p q 'nil) r) -- but more
likely, the corresponding clause is ((not p) (not q) r).  Note that the
members of a clause are _translated_ terms; see TERM.  For
example, they do not contains calls of the macro AND, and constants are
quoted.

Note that clause-processor simplifiers are similar to metafunctions, and
similar efficiency considerations apply.  See META, in
particular the discussion on how to "make a metafunction maximally
efficient."

Unlike rules of class :meta, rules of class :clause-processor must be
applied by explicit :clause-processor hints; they are not applied
automatically (unless by way of computed hints; see
COMPUTED-HINTS).  But :clause-processor rules can be useful in
situations for which it is more convenient to code a simplifier that
manipulates the entire goal clause rather than individual subterms of
terms in the clause.

We begin with a simple illustrative example: a clause-processor that
assumes an alleged fact and creates a separate goal to prove that fact.
We can extend the hypotheses of the current goal with a term by adding
the negation of that term to the clause (disjunctive) representation of
that goal.  So the following returns two clauses: the result of adding
term as a hypothesis to the input clause, as just described, and a
second clause consisting only of that term.

     (defun note-fact-clause-processor (cl term)
       (declare (xargs :guard t)) ; optional, for better efficiency
       (list (cons (list 'not term)
                   cl)
             (list term)))

As with :meta rules, we need to introduce a suitable evaluator; see
DEFEVALUATOR if you want details.  Since we expect to reason
about the function NOT, because of its role in
note-fact-clause-processor as defined above, we include NOT in the set
of functions known to this evaluator.  We also include IF, as is often
a good idea.

     (defevaluator evl0 evl0-list
       ((not x) (if x y z)))

ACL2 can now prove the following theorem automatically.  (Of course,
:clause-processor rules about clause-processor functions less trivial
than note-fact-clause-processor may require lemmas to be proved first!)
The function disjoin takes a clause and returns its disjunction (the
result of applying OR to its members), and conjoin-clauses applies
disjoin to every element of a given list of clauses and then conjoins
(applies AND) to the corresponding list of resulting terms.

     (defthm correctness-of-note-fact-clause-processor
       (implies (and (pseudo-term-listp cl)
                     (alistp a)
                     (evl0 (conjoin-clauses
                            (note-fact-clause-processor cl term))
                           a))
                (evl0 (disjoin cl) a))
       :rule-classes :clause-processor)

Now let us submit a silly but illustrative example theorem to ACL2, to
show how a corresponding :clause-processor hint is applied.  The hint
says to apply the clause-processor function,
note-fact-clause-processor, to the current goal clause and a "user
hint" as the second argument of that function, in this case (equal a
a).  Thus, a specific variable, clause, is always bound to the current
goal clause for the evaluation of the :clause-processor hint, to
produce a list of clauses.  Since two subgoals are created below, we
know that this list contained two clauses.  Indeed, these are the
clauses returned when note-fact-clause-processor is applied to two
arguments:  the current clause, which is the one-element list ((equal
(car (cons x y)) x)), and the user hint, (equal a a).

     ACL2 !>(thm (equal (car (cons x y))
                        x)
                 :hints
                 (("Goal"
                   :clause-processor
                   (note-fact-clause-processor clause '(equal a a)))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     We now apply the verified :CLAUSE-PROCESSOR function NOTE-FACT-CLAUSE-
     PROCESSOR to produce two new subgoals.

     Subgoal 2
     (IMPLIES (EQUAL A A)
              (EQUAL (CAR (CONS X Y)) X)).

     But we reduce the conjecture to T, by the :executable-counterpart of
     IF and the simple :rewrite rule CAR-CONS.

     Subgoal 1
     (EQUAL A A).

     But we reduce the conjecture to T, by primitive type reasoning.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:EXECUTABLE-COUNTERPART IF)
             (:EXECUTABLE-COUNTERPART NOT)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:REWRITE CAR-CONS))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Proof succeeded.
     ACL2 !>

That concludes our introduction to clause-processor rules and hints.
We turn now to detailed documentation.

The signature of a clause-processor function, CL-PROC, must have one of
the following forms.  Here, each st_i is a stobj (possibly state) while
the other parameters and results are not stobjs (see DEFSTOBJ).
Note that there need not be input stobjs in [3] -- i.e., k can be 0 --
and even if there are, there need not be output stobjs.

     [1]  ((CL-PROC cl) => cl-list)

     [2]  ((CL-PROC cl hint) => cl-list)

     [3]  ((CL-PROC cl hint st_1 ... st_k) => (erp cl-list st_i1 ... st_in))

In [3], we think of the first component of the result as an error flag.
Indeed, a proof will instantly abort if that error flag is not nil.

We next discuss the legal forms of :clause-processor rules, followed
below by a discussion of :clause-processor hints.  In the discussion
below, we use lower-case names to represent specific symbols, for
example implies, and we use upper-case names to represent more
arbitrary pieces of syntax (which we will describe), for example, CL.

If a :rule-classes specification includes :clause-processor, then the
corresponding term must have the form

     (implies (and (pseudo-term-listp CL)
                   (alistp A)
                   (EVL (conjoin-clauses <CL-LIST>)
                         B))
              (EVL (disjoin CL) A))

where: EVL is a known evaluator; CL and A are distinct non-stobj
variables; and <CL-LIST> is an expression representing the clauses
returned by the clause-processor function CL-PROC, whose form depends on
the signature of that function, as follows.  Typically B is A, but it
can be any term (useful when generalization is occurring; see the
example "Test generalizing alist" in
books/clause-processors/basic-examples.lisp).  For cases [1] and [2]
above, <CL-LIST> is of the form (CL-PROC CL) or (CL-PROC CL HINT),
respectively, where in the latter case HINT is a non-stobj variable
distinct from the variables CL and A.  For case [3], <CL-LIST> is of
the form

     (clauses-result (CL-PROC CL HINT st_1 ... st_k))

where the st_i are the specific stobj names mentioned in [3].
Logically, clauses-result returns the cadr if the car is NIL, and
otherwise (for the error case) returns a list containing the empty
(false) clause.  So in the non-error case, clauses-result picks out the
second result, denoted cl-list in [3] above, and in the error case the
implication above trivially holds.

The clause-processor function, CL, must have a guard that ACL2 can
trivially prove from the hypotheses that the first argument of CL is
known to be a pseudo-term-listp and any stobj arguments are assumed to
satisfy their stobj predicates.

Next we specify the legal forms for :clause-processor hints.  These
depend on the signature as described in [1] through [3] above.  Below,
as above, CL-PROC is the clause-processor function, and references to
"clause" refer to that exact variable (not, for example, to cl).  In
each of the three cases, the forms shown for that case are equivalent;
in particular, the :function syntax is simply a convenience for the
final form in each case.

Signature [1], ((cl-proc cl) => cl-list):

     :clause-processor CL-PROC
     :clause-processor (:function CL-PROC)
     :clause-processor (CL-PROC clause)

or any term macroexpanding to (CL-PROC clause).

Signature [2], ((cl-proc cl hint) => cl-list):

     :clause-processor (:function CL-PROC :hint HINT)
     :clause-processor (CL-PROC clause HINT)

or any term macroexpanding to (CL-PROC clause HINT), where HINT is any
term with at most CLAUSE free.

Signature [3], ((CL-PROC cl hint ...) => (erp cl-list ...))

     :clause-processor (:function CL-PROC :hint HINT)
     :clause-processor (CL-PROC clause HINT st_1 ... st_k)

or any term macroexpanding to (CL-PROC clause HINT st_1 ... st_k), where
HINT is any term with at most CLAUSE free.

A :clause-processor hint causes the proof to abort if the result
returned by evaluating the suitable CL-PROC call, as above, is not a
list of clauses, i.e., a list of (translated) term lists.  The proof
also aborts if in case [3] the first (erp) value returned is not nil,
in which case erp is used for printing an error message as follows: if
it is a string, then that string is printed; but if it is a non-empty
true list whose first element is a string, then it is printed as though
by (fmt ~@0 (list (cons #\0 erp)) ...) (see FMT).  Otherwise, a
non-nil erp value causes a generic error message to be printed.

If there is no error as above, but the CL-PROC call returns clause list
whose single element is equal to the input clause, then the hint is
ignored since we are left with the goal with which we started.  In that
case, the other prover processes are then applied as usual.

You can see all current :clause-processor rules by issuing the following
command: (print-clause-processor-rules).

The following paper discusses ACL2 clause-processors at a high level
suitable for a non-ACL2 audience:

     M. Kaufmann, J S. Moore, S. Ray, and E. Reeber, "Integrating
     External Deduction Tools with ACL2."  Proceedings of the 6th
     International Workshop on the Implementation of Logics (IWIL 2006)
     (C. Benzmueller, B. Fischer, and G. Sutcliffe, editors), CEUR
     Workshop Proceedings Vol. 212, Phnom Penh, Cambodia, pp. 7-26,
     November 2006, http://ceur-ws.org/Vol-212/.  Expanded version to
     appear in the Journal of Applied Logic.

COMPOUND-RECOGNIZER    make a rule used by the typing mechanism

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)               ; (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 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, as the
third and fourth forms are equivalent, as are the fifth and sixth.  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 and fourth general forms, 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 third and fourth forms 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 the fifth and sixth classes 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 (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, 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 data base.

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

CONGRUENCE    the relations to maintain while simplifying arguments

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 :congruence rule might be built is:

     Example:
     (implies (set-equal x y)
              (iff (memb e x) (memb e y))).

Also see DEFCONG and see EQUIVALENCE.

     General Form:
     (implies (equiv1 xk xk-equiv)
              (equiv2 (fn x1... xk       ...xn)
                      (fn x1... xk-equiv ...xn)))

where equiv1 and equiv2 are known equivalence relations, fn is an n-ary
function symbol and the xi and xk-equiv are all distinct variables.
The effect of such a rule is to record that the equiv2-equivalence of
fn-expressions can be maintained if, while rewriting the kth argument
position, equiv1-equivalence is maintained.  See EQUIVALENCE
for a general discussion of the issues.  We say that equiv2, above, is
the "outside equivalence" in the rule and equiv1 is the "inside
equivalence for the kth argument"

The macro form (defcong equiv1 equiv2 (fn x1 ... x1) k) is an
abbreviation for a defthm of rule-class :congruence that attempts to
establish that equiv2 is maintained by maintaining equiv1 in fn's kth
argument.  The defcong macro automatically generates the general
formula shown above.  See DEFCONG.

The memb example above tells us that (memb e x) is propositionally
equivalent to (memb e y), provided x and y are set-equal.  The outside
equivalence is iff and the inside equivalence for the second argument
is set-equal.  If we see a memb expression in a propositional context,
e.g., as a literal of a clause or test of an if (but not, for example,
as an argument to cons), we can rewrite its second argument maintaining
set-equality.  For example, a rule stating the commutativity of append
(modulo set-equality) could be applied in this context.  Since equality
is a refinement of all equivalence relations, all equality rules are
always available.  See REFINEMENT.

All known :congruence rules about a given outside equivalence and fn
can be used independently.  That is, consider two :congruence rules
with the same outside equivalence, equiv, and about the same function
fn.  Suppose one says that equiv1 is the inside equivalence for the
first argument and the other says equiv2 is the inside equivalence for
the second argument.  Then (fn a b) is equiv (fn a' b') provided a is
equiv1 to a' and b is equiv2 to b'.  This is an easy consequence of the
transitivity of equiv.  It permits you to think independently about the
inside equivalences.

Furthermore, it is possible that more than one inside equivalence for a
given argument slot will maintain a given outside equivalence.  For
example, (length a) is equal to (length a') if a and a' are related
either by list-equal or by string-equal.  You may prove two (or more)
:congruence rules for the same slot of a function.  The result is that
the system uses a new, "generated" equivalence relation for that slot
with the result that rules of both (or all) kinds are available while
rewriting.

:Congruence rules can be disabled.  For example, if you have two
different inside equivalences for a given argument position and you
find that the :rewrite rules for one are unexpectedly preventing the
application of the desired rule, you can disable the rule that
introduced the unwanted inside equivalence.

_Remark on Replacing IFF by EQUAL._ You may encounter a warning
suggesting that a congruence rule "can be strengthened by replacing the
second equivalence relation, IFF, by EQUAL."  Suppose for example that
this warning occurs when you submit the following rule:

     (defcong equiv1 iff (fn x y) 2)

which is shorthand for the following:

     (defthm equiv1-implies-iff-fn-2
            (implies (equiv1 y y-equiv)
                     (iff (fn x y) (fn x y-equiv)))
            :rule-classes (:congruence))

The warning is telling you that ACL2 was able to deduce that fn always
returns a Boolean, and hence a trivial but useful consequence is
obtained by replacing iff by equal --

     (defcong equiv1 equal (fn x y) 2)

-- which is shorthand for the following:

     (defthm equiv1-implies-equal-fn-2
            (implies (equiv1 y y-equiv)
                     (equal (fn x y) (fn x y-equiv)))
            :rule-classes (:congruence))

If you have difficulty proving the latter directly, you can derive it
from the former by giving a suitable hint, minimally as follows.

     (defcong equiv1 equal (fn x y) 2
       :hints (("Goal"
                :use equiv1-implies-iff-fn-2
                :in-theory
                (union-theories '((:type-prescription fn))
                                (theory 'minimal-theory)))))

By heeding this warning, you may avoid unnecessary double-rewrite
warnings later.  We now explain why, but see DOUBLE-REWRITE for
relevant background material.

For example, suppose you have proved the "iff" version of the
congruence rule above, and later you submit the following rewrite rule.

     (defthm equal-list-perm
       (implies (equiv1 x y)
                (fn x y)))

Since fn is known to return a Boolean, ACL2 performs an optimization
that stores this rule as though it were the following.

     (defthm equal-list-perm
       (implies (equiv1 x y)
                (equal (fn x y) t)))

Thus, if ACL2's rewriter sees a term (fn a b) in a context where the
equivalence relation iff is not being maintained, then it cannot use
rule equiv1-implies-iff-fn-2, so it rewrites argument a without the
benefit of knowing that it suffices to maintain equiv1; and then it
caches the result.  When ACL2 subsequently attempts to relieve the
hypothesis (equiv1 x y), it will rewrite x simply by returning the
rewritten value of a from the result cache.  This is unfortunate if a
could have been rewritten more completely under maintainance of the
equivalence relation equiv1 -- which is legal in the hypothesis since a
is an argument of equiv1, which is an equivalence relation.  The user
who observes the warning from rule equiv1-implies-iff-fn-2, and
replaces it with equiv1-implies-equal-fn-2, will avoid this unfortunate
case.

DEFINITION    make a rule that acts like a function definition

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 :definition rule might be built is:

     Example:
     (implies (true-listp x)
              (equal (len x)
                     (if (null x)
                         0
                         (if (null (cdr x))
                             1
                             (+ 2 (len (cddr x)))))))

     General Form:
     (implies hyp (equiv (fn a1 ... an) body))

where equiv is an equivalence relation and fn is a function symbol
other than if, hide, force or case-split.  Such rules allow
"alternative" definitions of fn to be proved as theorems but used as
definitions.  These rules are not true "definitions" in the sense that
they (a) cannot introduce new function symbols and (b) do not have to
be terminating recursion schemes.  They are just conditional rewrite
rules that are controlled the same way we control recursive
definitions.  We call these "definition rules" or "generalized
definitions".

Consider the general form above.  Generalized definitions are stored
among the :rewrite rules for the function "defined," fn above, but the
procedure for applying them is a little different.  During rewriting,
instances of (fn a1 ... an) are replaced by corresponding instances of
body provided the hyps can be established as for a :rewrite rule and
the result of rewriting body satisfies the criteria for function
expansion.  There are two primary criteria, either of which permits
expansion.  The first is that the "recursive" calls of fn in the
rewritten body have arguments that already occur in the goal
conjecture.  The second is that the "controlling" arguments to fn are
simpler in the rewritten body.

The notions of "recursive call" and "controllers" are complicated by
the provisions for mutually recursive definitions.  Consider a "clique"
of mutually recursive definitions.  Then a "recursive call" is a call
to any function defined in the clique and an argument is a "controller"
if it is involved in the measure that decreases in all recursive calls.
These notions are precisely defined by the definitional principle and
do not necessarily make sense in the context of generalized
definitional equations as implemented here.

But because the heuristics governing the use of generalized definitions
require these notions, it is generally up to the user to specify which
calls in body are to be considered recursive and what the controlling
arguments are.  This information is specified in the :clique and
:controller-alist fields of the :definition rule class.

The :clique field is the list of function symbols to be considered
recursive calls of fn.  In the case of a non-recursive definition, the
:clique field is empty; in a singly recursive definition, it should
consist of the singleton list containing fn; otherwise it should be a
list of all of the functions in the mutually recursive clique with this
definition of fn.

If the :clique field is not provided it defaults to nil if fn does not
occur as a function symbol in body and it defaults to the singleton
list containing fn otherwise.  Thus, :clique must be supplied by the
user only when the generalized definition rule is to be treated as one
of several in a mutually recursive clique.

The :controller-alist is an alist that maps each function symbol in the
:clique to a mask specifying which arguments are considered
controllers.  The mask for a given member of the clique, fn, must be a
list of t's and nil's of length equal to the arity of fn.  A t should
be in each argument position that is considered a "controller" of the
recursion.  For a function admitted under the principle of definition,
an argument controls the recursion if it is one of the arguments
measured in the termination argument for the function.  But in
generalized definition rules, the user is free to designate any subset
of the arguments as controllers.  Failure to choose wisely may result
in the "infinite expansion" of definitional rules but cannot render
ACL2 unsound since the rule being misused is a theorem.

If the :controller-alist is omitted it can sometimes be defaulted
automatically by the system.  If the :clique is nil, the
:controller-alist defaults to nil.  If the :clique is a singleton
containing fn, the :controller-alist defaults to the controller alist
computed by (defun fn args body).  If the :clique contains more than
one function, the user must supply the :controller-alist specifying the
controllers for each function in the clique.  This is necessary since
the system cannot determine and thus cannot analyze the other
definitional equations to be included in the clique.

For example, suppose fn1 and fn2 have been defined one way and it is
desired to make "alternative" mutually recursive definitions available
to the rewriter.  Then one would prove two theorems and store each as a
:definition rule.  These two theorems would exhibit equations
"defining" fn1 and fn2 in terms of each other.  No provision is here
made for exhibiting these two equations as a system of equations.  One
is proved and then the other.  It just so happens that the user intends
them to be treated as mutually recursive definitions.  To achieve this
end, both :definition rules should specify the :clique (fn1 fn2) and
should specify a suitable :controller-alist.  If, for example, the new
definition of fn1 is controlled by its first argument and the new
definition of fn2 is controlled by its second and third (and they each
take three arguments) then a suitable :controller-alist would be ((fn1
t nil nil) (fn2 nil t t)).  The order of the pairs in the alist is
unimportant, but there must be a pair for each function in the clique.

Inappropriate heuristic advice via :clique and :controller-alist can
cause "infinite expansion" of generalized definitions, but cannot
render ACL2 unsound.

Note that the actual definition of fn1 has the runic name (:definition
fn1).  The runic name of the alternative definition is (:definition
lemma), where lemma is the name given to the event that created the
generalized :definition rule.  This allows theories to switch between
various "definitions" of the functions.

By default, a :definition rule establishes the so-called "body" of a
function.  The body is used by :expand hints, and it is also used
heuristically by the theorem prover's preprocessing (the initial
simplification using "simple" rules that is controlled by the
preprocess symbol in :do-not hints), induction analysis, and the
determination for when to warn about non-recursive functions in rules.
The body is also used by some heuristics involving whether a function is
recursively defined, and by the expand, x, and x-dumb commands of the
proof-checker.

See RULE-CLASSES for a discussion of the optional field
:install-body of :definition rules, which controls whether a
:definition rule is used as described in the paragraph above.  Note
that even if :install-body nil is supplied, the rewriter will still
rewrite with the :definition rule; in that case, ACL2 just won't
install a new body for the top function symbol of the left-hand side of
the rule, which for example affects the application :expand hints as
described in the preceding paragraph.  Also see SET-BODY and
see SHOW-BODIES for how to change the body of a function symbol.

Note only that if you prove a definition rule for function foo, say,
foo-new-def, you will need to refer to that definition as foo-new-def
or as (:DEFINITION foo-new-def).  That is because a :definition rule
does not change the meaning of the symbol foo for :use hints, nor does
it change the meaning of the symbol foo in theory expressions; see
THEORIES, in particular the discussion there of runic
designators.  Similarly :pe foo and :pf foo will still show the
original definition of foo.

The definitional principle, defun, actually adds :definition rules.
Thus the handling of generalized definitions is exactly the same as for
"real" definitions because no distinction is made in the
implementation.  Suppose (fn x y) is defun'd to be body.  Note that
defun (or defuns or mutual-recursion) can compute the clique for fn
from the syntactic presentation and it can compute the controllers from
the termination analysis.  Provided the definition is admissible, defun
adds the :definition rule (equal (fn x y) body).

ELIM    make a destructor elimination rule

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Here we describe the
class of :elim rules, which is fundamentally quite different from the
more common class of :rewrite rules.  Briefly put, a :rewrite rule
replaces instances of its left-hand side with corresponding instances
of its right-hand side.  But an :elim rule, on the other hand, has the
effect of generalizing so-called "destructor" function applications to
variables.  In essence, applicability of a :rewrite rule is based on
matching its left-hand side, while applicability of an :elim rule is
based on the presence of at least one destructor term.

For example, a conjecture about (car x) and (cdr x) can be replaced by
a conjecture about new variables x1 and x2, as shown in the following
example.  (Run the command :mini-proveall and search for CAR-CDR-ELIM
to see the full proof containing this excerpt.)

     Subgoal *1/1'
     (IMPLIES (AND (CONSP X)
                   (TRUE-LISTP (REV (CDR X))))
              (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))).

     The destructor terms (CAR X) and (CDR X) can be eliminated by using
     CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X)
     by X2.  This produces the following goal.

     Subgoal *1/1''
     (IMPLIES (AND (CONSP (CONS X1 X2))
                   (TRUE-LISTP (REV X2)))
              (TRUE-LISTP (APP (REV X2) (LIST X1)))).

     This simplifies, using primitive type reasoning, to

     Subgoal *1/1'''
     (IMPLIES (TRUE-LISTP (REV X2))
              (TRUE-LISTP (APP (REV X2) (LIST X1)))).

The resulting conjecture is often simpler and hence more amenable to
proof.

The application of an :elim rule thus replaces a variable by a term that
contains applications of so-called "destructor" functions to that
variable.  The example above is typical: the variable x is replaced by
the term (cons (car x) (cdr x)), which applies a so-called "constructor"
function, cons, to applications (car x) and (cdr x) of destructor
functions car and cdr to that same variable, x.  But that is only part
of the story.  ACL2 then generalizes the destructor applications (car
x) and (cdr x) to new variables x1 and x2, respectively, and ultimately
the result is a simpler conjecture.

More generally, the application of an :elim rule replaces a variable by
a term containing applications of destructors; there need not be a
clear-cut notion of "constructor."  But the situation described above
is typical, and we will focus on it, giving full details when we
introduce the "General Form" below.

The example above employs the following built-in :elim rule named
car-cdr-elim.

     Example:
     (implies (consp x)                      when (car v) or (cdr v) appears
              (equal (cons (car x) (cdr x))  in a conjecture, and v is a
                     x))                     variable, consider replacing v by
                                             (cons a b), for two new variables
                                             a and b.

     Notice that the situation is complicated a bit by the fact that this
     replacement is only valid if the variable being replaced a cons structure.
     Thus, when ACL2 applies car-cdr-elim to replace a variable v, it will
     split into two cases: one case in which (consp v) is true, in which v
     is replaced by (cons (car v) (cdr v)) and then (car v) and
     (cdr v) are generalized to new variables; and one case in which
     (consp v) is false.  In practice, (consp v) is often provable,
     perhaps even literally present as a hypotheses; then of course there is no
     need to introduce the second case.  That is why there is no such second case
     in the example above.

     You might find :elim rules to be useful whenever you have in mind a data
     type that can be built up from its fields with a ``constructor'' function and
     whose fields can be accessed by corresponding ``destructor'' functions.  So
     for example, if you have a ``house'' data structure that represents a house
     in terms of its address, price, and color, you might have a rule like the
     following.
          Example:
          (implies (house-p x)
                   (equal (make-house (address x)
                                      (price x)
                                      (color x))
                          x))

     The application of such a rule is entirely analogous to the application of
     the rule car-cdr-elim discussed above.  We discuss such rules and their
     application more carefully below.

     General Form:
     (implies hyp (equiv lhs x))

where equiv is a known equivalence relation (see DEFEQUIV); x
is a variable symbol; and lhs contains one or more terms (called
"destructor terms") of the form (fn v1 ... vn), where fn is a function
symbol and the vi are distinct variable symbols, v1, ..., vn include
all the variable symbols in the formula, no fn occurs in lhs in more
than one destructor term, and all occurrences of x in lhs are inside
destructor terms.

To use an :elim rule, the theorem prover waits until a conjecture has
been maximally simplified.  It then searches for an instance of some
destructor term (fn v1 ... vn) in the conjecture, where the instance for
x is some variable symbol, vi, and every occurrence of vi outside the
destructor terms is in an equiv-hittable position.  If such an instance
is found, then the theorem prover instantiates the :elim formula as
indicated by the destructor term matched; splits the conjecture into two
goals, according to whether the instantiated hypothesis, hyp, holds; and
in the case that it does hold, generalizes all the instantiated
destructor terms in the conjecture to new variables and then replaces
vi in the conjecture by the generalized instantiated lhs.  An
occurrence of vi is "equiv-hittable" if sufficient congruence rules
(see DEFCONG) have been proved to establish that the
propositional value of the clause is not altered by replacing that
occurrence of vi by some equiv-equivalent term.

If an :elim rule is not applied when you think it should have been, and
the rule uses an equivalence relation, equiv, other than equal, it is
most likely that there is an occurrence of the variable that is not
equiv-hittable.  Easy occurrences to overlook are those in the
governing hypotheses.  If you see an unjustified occurrence of the
variable, you must prove the appropriate congruence rule to allow the
:elim to fire.

Further examples of how ACL2 :elim rules are used may be found in the
corresponding discussion of "Elimation of Destructors" for Nqthm, in
Section 10.4 of A Computational Logic Handbook.