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.

INDUCTION    make a rule that suggests a certain induction

     Example:
     (:induction :corollary t  ; the theorem proved is irrelevant!
                 :pattern (* 1/2 i)
                 :condition (and (integerp i) (>= i 0))
                 :scheme (recursion-by-sub2 i))

In ACL2, as in Nqthm, the functions in a conjecture "suggest" the
inductions considered by the system.  Because every recursive function
must be admitted with a justification in terms of a measure that
decreases in a well-founded way on a given set of "controlling"
arguments, every recursive function suggests a dual induction scheme
that "unwinds" the function from a given application.

For example, since append (actually binary-append, but we'll ignore the
distinction here) decomposes its first argument by successive cdrs as
long as it is a non-nil true list, the induction scheme suggested by
(append x y) has a base case supposing x to be either not a true list
or to be nil and then has an induction step in which the induction
hypothesis is obtained by replacing x by (cdr x).  This substitution
decreases the same measure used to justify the definition of append.
Observe that an induction scheme is suggested by a recursive function
application only if the controlling actuals are distinct variables, a
condition that is sufficient to ensure that the "substitution" used to
create the induction hypothesis is indeed a substitution and that it
drives down a certain measure.  In particular, (append (foo x) y) does
not suggest an induction unwinding append because the induction scheme
suggested by (append x y) requires that we substitute (cdr x) for x and
we cannot do that if x is not a variable symbol.

Once ACL2 has collected together all the suggested induction schemes it
massages them in various ways, combining some to simultaneously unwind
certain cliques of functions and vetoing others because they "flaw"
others.  We do not further discuss the induction heuristics here; the
interested reader should see Chapter XIV of A Computational Logic
(Boyer and Moore, Academic Press, 1979) which represents a fairly
complete description of the induction heuristics of ACL2.

However, unlike Nqthm, ACL2 provides a means by which the user can
elaborate the rules under which function applications suggest induction
schemes.  Such rules are called :induction rules.  The definitional
principle automatically creates an :induction rule, named (:induction
fn), for each admitted recursive function, fn.  It is this rule that
links applications of fn to the induction scheme it suggests.
Disabling (:induction fn) will prevent fn from suggesting the induction
scheme derived from its recursive definition.  It is possible for the
user to create additional :induction rules by using the :induction rule
class in defthm.

Technically we are "overloading" defthm by using it in the creation of
:induction rules because no theorem need be proved to set up the
heuristic link represented by an :induction rule.  However, since
defthm is generally used to create rules and rule-class objects are
generally used to specify the exact form of each rule, we maintain that
convention and introduce the notion of an :induction rule.  An
:induction rule can be created from any lemma whatsoever.

     General Form of an :induction Lemma or Corollary:
     T

     General Form of an :induction rule-class:
     (:induction :pattern pat-term
                 :condition cond-term
                 :scheme scheme-term)

where pat-term, cond-term, and scheme-term are all terms, pat-term is
the application of a function symbol, fn, scheme-term is the
application of a function symbol, rec-fn, that suggests an induction,
and, finally, every free variable of cond-term and scheme-term is a
free variable of pat-term.  We actually check that rec-fn is either
recursively defined -- so that it suggests the induction that is
intrinsic to its recursion -- or else that another :induction rule has
been proved linking a call of rec-fn as the :pattern to some scheme.

The induction rule created is used as follows.  When an instance of the
:pattern term occurs in a conjecture to be proved by induction and the
corresponding instance of the :condition term is known to be non-nil
(by type reasoning alone), the corresponding instance of the :scheme
term is created and the rule "suggests" the induction, if any,
suggested by that term.  If rec-fn is recursive, then the suggestion is
the one that unwinds that recursion.

Consider, for example, the example given above,

     (:induction :pattern (* 1/2 i)
                 :condition (and (integerp i) (>= i 0))
                 :scheme (recursion-by-sub2 i)).

In this example, we imagine that recursion-by-sub2 is the function:

     (defun recursion-by-sub2 (i)
       (if (and (integerp i)
                (< 1 i))
           (recursion-by-sub2 (- i 2))
           t))

Observe that this function recursively decomposes its integer argument
by subtracting 2 from it repeatedly and stops when the argument is 1 or
less.  The value of the function is irrelevant; it is its induction
scheme that concerns us.  The induction scheme suggested by
(recursion-by-sub2 i) is

     (and (implies (not (and (integerp i) (< 1 i)))   ; base case
                   (:p i))
          (implies (and (and (integerp i) (< 1 i))    ; induction step
                        (:p (- i 2)))
                   (:p i)))

We can think of the base case as covering two situations.  The first is
when i is not an integer.  The second is when the integer i is 0 or 1.
In the base case we must prove (:p i) without further help.  The
induction step deals with those integer i greater than 1, and
inductively assumes the conjecture for i-2 while proving it for i.  Let
us call this scheme "induction on i by twos."

Suppose the above :induction rule has been added.  Then an occurrence
of, say, (* 1/2 k) in a conjecture to be proved by induction would
suggest, via this rule, an induction on k by twos, provided k was known
to be a nonnegative integer.  This is because the induction rule's
:pattern is matched in the conjecture, its :condition is satisfied, and
the :scheme suggested by the rule is that derived from
(recursion-by-sub2 k), which is induction on k by twos.  Similarly, the
term (* 1/2 (length l)) would suggest no induction via this rule, even
though the rule "fires" because it creates the :scheme
(recursion-by-sub2 (length l)) which suggests no inductions unwinding
recursion-by-sub2 (since the controlling argument of recursion-by-sub2
in this :scheme is not a variable symbol).

Continuing this example one step further illustrates the utility of
:induction rules.  We could define the function recursion-by-cddr that
suggests the induction scheme decomposing its consp argument two cdrs
at a time.  We could then add the :induction rule linking (* 1/2
(length x)) to (recursion-by-cddr x) and arrange for (* 1/2 (length l))
to suggest induction on l by cddr.

Observe that :induction rules require no proofs to be done.  Such a
rule is merely a heuristic link between the :pattern term, which may
occur in conjectures to be proved by induction, and the :scheme term,
from which an induction scheme may be derived.  Hence, when an
:induction rule-class is specified in a defthm event, the theorem
proved is irrelevant.  The easiest theorem to prove is, of course, t.
Thus, we suggest that when an :induction rule is to be created, the
following form be used:

     (defthm name T
       :rule-classes ((:induction :pattern pat-term
                                  :condition cond-term
                                  :scheme scheme-term)))

The name of the rule created is (:induction name).  When that rune is
disabled the heuristic link between pat-term and scheme-term is broken.

LINEAR    make some arithmetic inequality rules

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

     Example:
     (implies (and (eqlablep e)           if inequality reasoning begins to
                   (true-listp x))        consider how (length (member a b))
              (<= (length (member e x))   compares to any other term, add to
                  (length x)))            set of known inequalities the fact
                                          that it is no larger than (length b),
                                          provided (eqlablep a) and (true-listp b)
                                          rewrite to t

     General Form:
     (and ...
          (implies (and ...hi...)
                   (implies (and ...hk...)
                            (and ...
                                 (rel lhs rhs)
                                 ...)))
          ...)

Note: One :linear rule class object might create many linear arithmetic
rules from the :corollary formula.  To create the rules, we first
flatten the and and implies structure of the formula, transforming it
into a conjunction of formulas, each of the form

     (implies (and h1 ... hn) (rel lhs rhs))

where no hypothesis is a conjunction and rel is one of the inequality
relations <, <=, =, >, or >=.  If necessary, the hypothesis of such a
conjunct may be vacuous.  We create a :linear rule for each such
conjunct, if possible, and otherwise cause an error.

Each rule has one or more "trigger terms" which may be specified by the
user using the :trigger-terms field of the rule class or which may be
defaulted to values chosen by the system.  We discuss the determination
of trigger terms after discussing how linear rules are used.

:linear rules are used by an arithmetic decision procedure during
rewriting.  See LINEAR-ARITHMETIC and see
NON-LINEAR-ARITHMETIC.  Here we assume that the reader is familiar
with the material described in linear-arithmetic.

Recall that we eliminate the unknowns of an inequality in term-order,
largest unknowns first.  (See TERM-ORDER.)  In order to
facilitate this strategy, we store the inequalities in "linear pots".
For purposes of the present discussion, let us say that an inequality is
"about" its largest unknown.  Then, all of the inequalities about a
particular unknown are stored in the same linear pot, and the pot is
said to be "labeled" with that unknown.  This storage layout groups all
of the inequalities which are potential candidates for cancellation
with each other into one place.  It is also key to the efficient
operation of :linear rules.

If the arithmetic decision procedure has stabilized and not yielded a
contradiction, we scan through the list of linear pots examining each
label as we go.  If the trigger term of some :linear rule can be
instantiated to match the label, we so instantiate that rule and
attempt to relieve the hypotheses with general-purpose rewriting.  If
we are successful, we add the rule's instantiated conclusion to our set
of inequalities.  This may let cancellation continue.

Note: Problems may arise if you explicitly store a linear lemma under a
trigger term that, when instantiated, is not the largest unknown in the
instantiated concluding inequality.  Suppose for example you store the
linear rule (<= (fn i j) (/ i (* j j))) under the trigger term (fn i
j).  Then when the system "needs" an inequality about (fn a b), (i.e.,
because (fn a b) is the label of some linear pot, and hence the largest
unknown in some inequality), it will appeal to the rule and deduce (<=
(fn a b) (/ a (* b b))).  However, the largest unknown in this
inequality is (/ a (* b b)) and hence it will be stored in a linear pot
labeled with (/ a (* b b)).  The original, triggering inequality which
is in a pot about (fn a b) will therefore not be cancelled against the
new one.  It is generally best to specify as a trigger term one of the
"maximal" terms of the polynomial, as described below.

We now describe how the trigger terms are determined.  Most of the
time, the trigger terms are not specified by the user and are instead
selected by the system.  However, the user may specify the terms by
including an explicit :trigger-terms field in the rule class, e.g.,

     General Form of a Linear Rule Class:
     (:LINEAR :COROLLARY formula
              :TRIGGER-TERMS (term1 ... termk))

Each termi must be a term and must not be a variable, quoted constant,
lambda application, let-expression or if-expression.  In addition, each
termi must be such that if all the variables in the term are
instantiated and then the hypotheses of the corollary formula are
relieved (possibly instantiating additional free variables), then all
the variables in the concluding inequality are instantiated.  We
generate a linear rule for each conjuctive branch through the corollary
and store each rule under each of the specified triggers.  Thus, if the
corollary formula contains several conjuncts, the variable restrictions
on the termi must hold for each conjunct.

If :trigger-terms is omitted the system computes a set of trigger
terms.  Each conjunct of the corollary formula may be given a unique
set of triggers depending on the variables that occur in the conjunct
and the addends that occur in the concluding inequality.  In
particular, the trigger terms for a conjunct is the list of all
"maximal addends" in the concluding inequality.

The "addends" of (+ x y) and (- x y) are the union of the addends of x
and y.  The addends of (- x) and (* n x), where n is a rational
constant, is just {x}.  The addends of an inequality are the union of
the addends of the left- and right-hand sides.  The addends of any
other term, x, is {x}.

A term is maximal for a conjunct (implies hyps concl) of the corollary
if (a) the term is a non-variable, non-quote, non-lambda application,
non-let and non-if expression, (b) the term contains enough variables
so that when they are instantiated and the hypotheses are relieved
(which may bind some free variables; see FREE-VARIABLES) then
all the variables in concl are instantiated, and (c) no other addend is
always "bigger" than the term, in the technical sense described below.

The technical notion below depends on the notion of _fn-count_, the
number of function symbols in a term, and _pseudo-fn-count_, which is
the number of function symbols implicit in a constant (see the comment
on pseduo-fn-count in the definition of var-fn-count in the sources for
details).  We say term1 is always bigger than term2 if all instances of
term1 have a larger fn-count (actually lexicographic order of fn-count
and pseudo-fn-count) than the corresponding instances of term2.  This
is equivalent to saying that the fn-count of term1 is larger than that
of term2 (by "fn-count" here we mean the lexicographic order of
fn-count and pseudo-fn-count) and the variable bag for term2 is a
subbag of that for term1.  For example, (/ a (* b b)) is always bigger
than (fn a b) because the first has two function applications and {a b}
is a subbag of a b b, but (/ a (* b b)) is not always bigger than (fn a
x).

META    make a :meta rule (a hand-written simplifier)

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Meta rules extend the
ACL2 simplifier with hand-written code to transform certain terms to
equivalent ones.  To add a meta rule, the :corollary formula must
establish that the hand-written "metafunction" preserves the meaning of
the transformed term.

While our intention is that the set of ACL2 documentation topics is
self-contained, readers might find it useful to see the following paper
for an introduction to meta reasoning in ACL2.

     W. A. Hunt, Jr., R. B. Krug, M. Kaufmann, J S. Moore and E. W.
     Smith, "Meta Reasoning in ACL2."  TPHOLs 2005, ed. J. Hurd and T.
     F. Melham, LNCS 3603, Springer-Verlag, Berlin, 2005, pp. 163-178.

Example :corollary formulas from which :meta rules might be built are:

     Examples:
     (equal (evl x a)                  ; Modify the rewriter to use fn to
            (evl (fn x) a))            ; transform terms.  The :trigger-fns
                                       ; of the :meta rule-class specify
                                       ; the top-most function symbols of
                                       ; those x that are candidates for
                                       ; this transformation.

     (implies (and (pseudo-termp x)    ; As above, but this illustrates
                   (alistp a))         ; that without loss of generality we
              (equal (evl x a)         ; may restrict x to be shaped like a
                     (evl (fn x) a)))  ; term and a to be an alist.

     (implies (and (pseudo-termp x)    ; As above (with or without the
                   (alistp a)          ; hypotheses on x and a) with the
                   (evl (hyp-fn x) a)) ; additional restriction that the
              (equal (evl x a)         ; meaning of (hyp-fn x) is true in
                     (evl (fn x) a)))  ; the current context.  That is, the
                                       ; applicability of the transforma-
                                       ; tion may be dependent upon some
                                       ; computed hypotheses.

A non-nil list of function symbols must be supplied as the value of the
:trigger-fns field in a :meta rule class object.

     General Forms:
     (implies (and (pseudo-termp x)        ; this hyp is optional
                   (alistp a)              ; this hyp is optional
                   (ev (hyp-fn x ...) a))  ; this hyp is optional
              (equiv (ev x a)
                     (ev (fn x ...) a)))

where equiv is a known equivalence relation, x and a are distinct
variable names, and ev is an evaluator function (see below), and fn is
a function symbol, as is hyp-fn when provided.  The arguments to fn and
hyp-fn should be identical.  In the most common case, both take a
single argument, x, which denotes the term to be simplified.  If fn
and/or hyp-fn are guarded, their guards should be (implied by)
pseudo-termp.  See PSEUDO-TERMP.  We say the theorem above is a
"metatheorem" or "metalemma" and fn is a "metafunction", and hyp-fn is
a "hypothesis metafunction".

If "..." is empty, i.e., the metafunctions take just one argument, we
say they are "vanilla flavored."  If "..." is non-empty, we say the
metafunctions are "extended."  Extended metafunctions can access state
and context sensitive information to compute their results, within
certain limits.  We discuss vanilla metafunctions here and recommend a
thorough understanding of them before proceeding (at which time see
EXTENDED-METAFUNCTIONS).

Metafunctions and (if supplied) hypothesis metafunctions must be
executable.  That is, they cannot be constrained (i.e., introduced in
the signature of encapsulate events), nor can they be declared
:non-executable.  After all, there is no point in installing a
simplifier that cannot be run!

We defer discussion of the case in which there is a hypothesis
metafunction and for now address the case in which the other two
hypotheses are present.

In the discussion below, we refer to the argument, x, of fn and hyp-fn
as a "term."  When these metafunctions are executed by the simplifier,
they will be applied to (the quotations of) terms.  But during the
proof of the metatheorem itself, x may not be the quotation of a term.
If the pseudo-termp hypothesis is omitted, x may be any object.  Even
with the pseudo-termp hypothesis, x may merely "look like a term" but
use non-function symbols or function symbols of incorrect arity.  In
any case, the metatheorem is stronger than necessary to allow us to
apply the metafunctions to terms, as we do in the discussion below.  We
return later to the question of proving the metatheorem.

Suppose the general form of the metatheorem above is proved with the
pseudo-termp and alistp hypotheses.  Then when the simplifier
encounters a term, (h t1 ... tn), that begins with a function symbol,
h, listed in :trigger-fns, it applies the metafunction, fn, to the
quotation of the term, i.e., it evaluates (fn '(h t1 ... tn)) to obtain
some result, which can be written as 'val.  If 'val is different from
'(h t1 ... tn) and val is a term, then (h t1 ... tn) is replaced by
val, which is then passed along for further rewriting.  Because the
metatheorem establishes the correctness of fn for all terms (even
non-terms!), there is no restriction on which function symbols are
listed in the :trigger-fns.  Generally, of course, they should be the
symbols that head up the terms simplified by the metafunction fn.  See
TERM-TABLE for how one obtains some assistance towards
guaranteeing that val is indeed a term.

The "evaluator" function, ev, is a function that can evaluate a certain
class of expressions, namely, all of those composed of variables,
constants, and applications of a fixed, finite set of function symbols,
g1, ..., gk.  Generally speaking, the set of function symbols handled
by ev is chosen to be exactly the function symbols recognized and
manipulated by the metafunctions being introduced.  For example, if fn
manipulates expressions in which 'equal and 'binary-append occur as
function symbols, then ev is generally specified to handle equal and
binary-append.  The actual requirements on ev become clear when the
metatheorem is proved.  The standard way to introduce an evaluator is to
use the ACL2 macro defevaluator, though this is not strictly necessary.
See DEFEVALUATOR if you want details.

[Aside for the logic-minded.] Why are we justified in using
metafunctions this way?  Suppose (fn 'term1) is 'term2.  What justifies
replacing term1 by term2?  The first step is to assert that term1 is
(ev 'term1 a), where a is an alist that maps 'var to var, for each
variable var in term1.  This step is incorrect, because 'term1 may
contain function symbols other than the ones, g1, ..., gk, that ev
knows how to handle.  But we can grow ev to a "larger" evaluator, ev*,
an evaluator for all of the symbols that occur in term1 or term2.  We
can prove that ev* satisfies the constraints on ev, provided no
defaxiom events are adding constraints to ev (or callers of ev, and
recursively); ACL2 checks this additional property.  Hence, the
metatheorem holds for ev* in place of ev, by functional instantiation.
We can then carry out the proof of the equivalence of term1 and term2
as follows: Fix a to be an alist that maps the quotations of the
variables of term1 and term2 to themselves.  Then,
     ev* and a = (ev* (fn 'term1) a) ; (2) by the metatheorem for ev* = (ev*
     'term2 a) ; (3) by evaluation of fn = term2 ; (4) by construction of ev* and
     a
 Note that in line (2) above, where we appeal to the (functional
instantiation of the) metatheorem, we can relieve its (optional)
pseudo-termp and alistp hypotheses by appealing to the facts that term1
is a term and a is an alist by construction.  [End of Aside for the
logic-minded.]

There are subtleties related to the notion of "growing" ev to a
"larger" evaluator, as mentioned in the paragraph just above.  For
corresponding restrictions on :meta rules, see
EVALUATOR-RESTRICTIONS.

Finally, we turn to the second case, in which there is a hypothesis
metafunction.  In that case, consider as before what happens when the
simplifier encounters a term, (h t1 ... tn), where h is listed in
:trigger-fns.  This time, after it applies fn to '(h t1 ... tn) to
obtain the quotation of some new term, 'val, it then applies the
hypothesis metafunction, hyp-fn.  That is, it evaluates (hyp-fn '(h t1
... tn)) to obtain some result, which can be written as 'hyp-val.  If
hyp-val is not in fact a term, the metafunction is not used.  Provided
hyp-val is a term, the simplifier attempts to establish (by
conventional backchaining) that this term is non-nil in the current
context.  If this attempt fails, then the meta rule is not applied.
Otherwise, (h t1...tn) is replaced by val as in the previous case
(where there was no hypothesis metafunction).

Why is it justified to make this extension to the case of hypothesis
metafunctions?  First, note that the rule

     (implies (and (pseudo-termp x)
                   (alistp a)
                   (ev (hyp-fn x) a))
              (equal (ev x a)
                     (ev (fn x) a)))

is logically equivalent to the rule

     (implies (and (pseudo-termp x)
                   (alistp a))
              (equal (ev x a)
                     (ev (new-fn x) a)))

where (new-fn x) is defined to be (list 'if (hyp-fn x) (fn x) x).  (If
we're careful, we realize that this argument depends on making an
extension of ev to an evaluator ev* that handles if and the functions
manipulated by hyp-fn.)  If we write 'term for the quotation of the
present term, and if (hyp-fn 'term) and (fn 'term) are both terms, say
hyp1 and term1, then by the previous argument we know it is sound to
rewrite term to (if hyp1 term1 term).  But since we have established in
the current context that hyp1 is non-nil, we may simplify (if hyp1
term1 term) to term1, as desired.

We now discuss the role of the pseudo-termp hypothesis.  (Pseudo-termp
x) checks that x has the shape of a term.  Roughly speaking, it ensures
that x is a symbol, a quoted constant, or a true list consisting of a
lambda expression or symbol followed by some pseudo-terms.  Among the
properties of terms not checked by pseudo-termp are that variable
symbols never begin with ampersand, lambda expressions are closed, and
function symbols are applied to the correct number of arguments.  See
PSEUDO-TERMP.

There are two possible roles for pseudo-termp in the development of a
metatheorem: it may be used as the guard of the metafunction and/or
hypothesis metafunction and it may be used as a hypothesis of the
metatheorem.  Generally speaking, the pseudo-termp hypothesis is
included in a metatheorem only if it makes it easier to prove.  The
choice is yours.  (An extreme example of this is when the metatheorem
is invalid without the hypothesis!)  We therefore address ourselves the
question: should a metafunction have a pseudo-termp guard?  A
pseudo-termp guard for a metafunction, in connection with other
considerations described below, improves the efficiency with which the
metafunction is used by the simplifier.

To make a metafunction maximally efficient you should (a) provide it
with a pseudo-termp guard and exploit the guard when possible in coding
the body of the function (see GUARDS-AND-EVALUATION, especially
the section on efficiency issues), (b) verify the guards of the
metafunction (see VERIFY-GUARDS), and (c) compile the
metafunction (see COMP).  When these three steps have been
taken the simplifier can evaluate (fn 'term1) by running the compiled
"primary code" (see GUARDS-AND-EVALUATION) for fn directly in
Common Lisp.  (Note however that explicit compilation may be
suppressed, in which case it is presumably unnecessary anyhow; see
COMPILATION.)

Before discussing efficiency issues further, let us review for a moment
the general case in which we wish to evaluate (fn 'obj) for some :logic
function.  We must first ask whether the guards of fn have been
verified.  If not, we must evaluate fn by executing its logic
definition.  This effectively checks the guards of every subroutine and
so can be slow.  If, on the other hand, the guards of fn have been
verified, then we can run the primary code for fn, provided 'obj
satisfies the guard of fn.  So we must next evaluate the guard of fn on
'obj.  If the guard is met, then we run the primary code for fn,
otherwise we run the logic code.

Now in the case of a metafunction for which the three steps above have
been followed, we know the guard is (implied by) pseudo-termp and that
it has been verified.  Furthermore, we know without checking that the
guard is met (because term1 is a term and hence 'term1 is a
pseudo-termp).  Hence, we can use the compiled primary code directly.

We strongly recommend that you compile your metafunctions, as well as
all their subroutines (unless explicit compilation is suppressed; see
COMPILATION).  Guard verification is also recommended.

Finally, we present a very simple example of the use of :meta rules,
based on one provided by Robert Krug.  This example illustrates a trick
for avoiding undesired rewriting after applying a metafunction or any
other form of rewriting.  To elaborate: in general, the term t2
obtained by applying a metafunction to a term t1 is then handed
immediately to the rewriter, which descends recursively through the
arguments of function calls to rewrite t2 completely.  But if t2 shares
a lot of structure with t1, then it might not be worthwhile to rewrite
t2 immediately.  (A rewrite of t2 will occur anyhow the next time a
goal is generated.)  The trick involves avoiding this rewrite by
wrapping t2 inside a call of hide, which in turn is inside a call of a
user-defined "unhiding" function, unhide.

     (defun unhide (x)
       (declare (xargs :guard t))
       x)

     (defthm unhide-hide
       (equal (unhide (hide x))
              x)
       :hints (("Goal" :expand ((hide x)))))

     (in-theory (disable unhide))

     (defun my-plus (x y)
       (+ x y))

     (in-theory (disable my-plus))

     (defevaluator evl evl-list
       ((my-plus x y)
        (binary-+ x y)
        (unhide x)
        (hide x)))

     (defun meta-fn (term)
       (declare (xargs :guard (pseudo-termp term)))
       (if (and (consp term)
                (equal (length term) 3)
                (equal (car term) 'my-plus))
           `(UNHIDE (HIDE (BINARY-+ ,(cadr term) ,(caddr term))))
         term))

     (defthm my-meta-lemma
       (equal (evl term a)
              (evl (meta-fn term) a))
       :hints (("Goal" :in-theory (enable my-plus)))
       :rule-classes ((:meta :trigger-fns (my-plus))))

Notice that in the following (silly) conjectre, ACL2 initially does
only does the simplification directed by the metafunction; a second
goal is generated before the commuativity of addition can be applied.
If the above calls of UNHIDE and HIDE had been stripped off, then Goal'
would have been the term printed in Goal" below.

     ACL2 !>(thm
             (equal (my-plus b a)
                    ccc))

     This simplifies, using the :meta rule MY-META-LEMMA and the :rewrite
     rule UNHIDE-HIDE, to

     Goal'
     (EQUAL (+ B A) CCC).

     This simplifies, using the :rewrite rule COMMUTATIVITY-OF-+, to

     Goal''
     (EQUAL (+ A B) CCC).

The discussion above probably suffices to make good use of this (UNHIDE
(HIDE ...)) trick.  However, we invite the reader who wishes to
understand the trick in depth to evaluate the following form before
submitting the thm form above.

     (trace$ (rewrite :entry (list (take 2 arglist))
                      :exit (list (car values)))
             (rewrite-with-lemma :entry (list (take 2 arglist))
                                 :exit (take 2 values)))

The following annotated subset of the trace output (which may appear a
bit different depending on the underlying Common Lisp implementation)
explains how the trick works.

         2> (REWRITE ((MY-PLUS B A) NIL))>
           3> (REWRITE-WITH-LEMMA
                   ((MY-PLUS B A)
                    (REWRITE-RULE (:META MY-META-LEMMA)
                                  1822
                                  NIL EQUAL META-FN NIL META NIL NIL)))>

     We apply the meta rule, then recursively rewrite the result, which is the
     (UNHIDE (HIDE ...)) term shown just below.

             4> (REWRITE ((UNHIDE (HIDE (BINARY-+ B A)))
                          ((A . A) (B . B))))>
               5> (REWRITE ((HIDE (BINARY-+ B A))
                            ((A . A) (B . B))))>

     The HIDE protects its argument from being touched by the rewriter.

               <5 (REWRITE (HIDE (BINARY-+ B A)))>
               5> (REWRITE-WITH-LEMMA
                       ((UNHIDE (HIDE (BINARY-+ B A)))
                        (REWRITE-RULE (:REWRITE UNHIDE-HIDE)
                                      1806 NIL EQUAL (UNHIDE (HIDE X))
                                      X ABBREVIATION NIL NIL)))>

     Now we apply UNHIDE-HIDE, then recursively rewrite its right-hand
     side in an environment where X is bound to (BINARY-+ B A).

                 6> (REWRITE (X ((X BINARY-+ B A))))>

     Notice that at this point X is cached, so REWRITE just returns
     (BINARY-+ B A).

                 <6 (REWRITE (BINARY-+ B A))>
               <5 (REWRITE-WITH-LEMMA T (BINARY-+ B A))>
             <4 (REWRITE (BINARY-+ B A))>
           <3 (REWRITE-WITH-LEMMA T (BINARY-+ B A))>
         <2 (REWRITE (BINARY-+ B A))>

EVALUATOR-RESTRICTIONS    some restrictions on the use of evaluators in meta-level rules

Note: This topic, which explains some subtleties for evaluators, can
probably be skipped by most readers.

Rules of class :meta and of class :clause-processor are stated using
so-called "evaluator" functions.  Here we explains some restrictions
related to evaluators.  Below we refer primarily to :meta rules, but
the discussion applies equally to :clause-processor rules.

In a nutshell, we require that a rule's evaluator does not support
other functions in the rule, and we require that the evaluator not be
introduced under a non-trivial encapsulate.  We explain these
restrictions in detail below.

An argument given elsewhere (see META, in particular "Aside for
the logic-minded") explains that the correctness argument for appying
metatheoretic simplifiers requires that one be able to "grow" an
evaluator (see DEFEVALUATOR) to handle all functions in the
current ACL2 world.  Then we may, in essence, functionally instantiate
the original evaluator to the new ("grown") evaluator, provided that
the new evaluator satisfies all of the axioms of the original.  We
therefore require that the evaluator function does not support the
formula of any defaxiom event.  This notion of "support" (sometimes
denoted "is an ancestor of") is defined recursively as follows: a
function symbol supports a formula if either it occurs in that formula,
or else it supports the definition or constraint for some function
symbol that occurs in that formula.  Moreover, we require that neither
the evaluator function nor its list version support the definition or
constraint for any other function symbol occurring in the proposed :meta
theorem.

We also require that the evaluator does not support the formula of a
:meta rule's metafunction (nor, if there is one, hypothesis
metafunction) or of a :clause-processor rule's clause-processor
function.  This requirement, together with the analogous requirement
for defaxiom events stated above, are necessary in order to carry out
the functional instantiation argument alluded to above, as follows
(where the reader may find it useful to have some familiarity with the
paper "Structured Theory Development for a Mechanized Logic" (Journal
of Automated Reasoning 26, no. 2 (2001), pages 161-203).  By the usual
conservativity argument, we know that the rule follows logically from
the axiomatic events for its supporters.  This remains true if we
functionally instantiate the evaluator with one corresponding to all
the functions symbols of the current session, since none of the
definitions of supporters of defaxioms or metafunctions are hit by that
functional substitution.

Notice though that the argument above depends on knowing that the rule
is not itself an axiom about the evaluator!  Therefore, we also
restrict evaluators so that they are not defined in the scope of a
superior encapsulate event with non-empty signature, in order to avoid
an even more subtle problem.  The aforementioned correctness argument
depends on knowing that the rule is provable from the axioms on the
evaluator and metafunction (and hypothesis metafunction, if any).  The
additional restriction avoids unsoundness!  The following events, if
allowed, produce a proof that (f x) equals t even though, as shown
below, that does not follow logically from the axioms introduced.

     ; Introduce our metafunction.
     (defun my-cancel (term)
       (case-match term
         (('f ('g))
          *t*)
         (& term)))

     ; Introduce our evaluator and prove our meta rule, but in the same
     ; encapsulate!
     (encapsulate
      ((f (x) t))

      (local (defun f (x) (declare (ignore x)) t))

      (defevaluator evl evl-list
        ((f x)))

      (defthm correctness-of-my-cancel
        (equal (evl x a)
               (evl (my-cancel x) a))
        :rule-classes ((:meta :trigger-fns (f)))))

     ; Prove that (f x) = t.
     (encapsulate
      ()

      (local (defstub c () t))

      (local (encapsulate
              ()
              (local (defun g () (c)))
              (local (in-theory (disable g (g))))
              (local (defthm f-g
                       (equal (f (g)) t)
                       :rule-classes nil))
              (defthm f-c
                (equal (f (c)) t)
                :hints (("Goal" :use f-g
                         :in-theory (e/d (g) (correctness-of-my-cancel))))
                :rule-classes nil)))

      (defthm f-t
        (equal (f x) t)
        :hints (("Goal" :by (:functional-instance
                             f-c
                             (c (lambda () x)))))
        :rule-classes nil))

To see that the term (equal (f x) t) does not follow logically from the
axiomatic events above, consider following the above definition of
my-cancel with the following events instead.

     ; (defun my-cancel (term) ...) as before, then:

     (defun f (x)
       (not x))

     (defun g ()
       nil)

     (defevaluator evl evl-list
        ((f x) (g)))

These events imply the axiomatic events above, because we still have the
definition of my-cancel, we have a stronger defevaluator event, and we
can now prove correctness-of-my-cancel exactly as it is stated above.
So, the rule f-t is a logical consequence of the chronology of the
current session.  However, in the current session we can also prove the
following rule, which contradicts f-t.

     (defthm f-not-t
       (equal (f t) nil)
       :rule-classes nil)

It follows that the current session logically yields a contradiction!

Erik Reeber has taken the above example and modified it to prove nil in
ACL2 Version_3.1, as follows.

     (in-package "ACL2")

     (defun my-cancel (term)
        (case-match term
          (('f ('g))
           *t*)
          (('f2 ('g2))
           *t*)
          (& term)))

     (defun f2 (x)
        (not x))

     (defun g2 ()
        nil)

     (encapsulate
       ((f (x) t))

       (local (defun f (x) (declare (ignore x)) t))

       (defevaluator evl evl-list
         ((f x)
          (f2 x)
          (g2)))

       (defthm correctness-of-my-cancel
         (equal (evl x a)
                (evl (my-cancel x) a))
         :rule-classes ((:meta :trigger-fns (f)))))

     (encapsulate
       ()

       (local (defstub c () t))

       (local (encapsulate
               ()
               (local (defun g () (c)))
               (local (in-theory (disable g (g))))
               (local (defthm f-g
                        (equal (f (g)) t)
                        :rule-classes nil))
               (defthm f-c
                 (equal (f (c)) t)
                 :hints (("Goal" :use f-g
                          :in-theory (e/d (g) (correctness-of-my-cancel))))
                 :rule-classes nil)))

       (defthm f-t
         (equal (f x) t)
         :hints (("Goal" :by (:functional-instance
                              f-c
                              (c (lambda () x)))))
         :rule-classes nil))

     (defun g ()
        nil)

     ; Below is the expansion of the following defevaluator, changed slightly as
     ; indicated by comments.
     ; (defevaluator evl2 evl2-list ((f x) (f2 x) (g) (g2)))

     (ENCAPSULATE
       (((EVL2 * *) => *)
        ((EVL2-LIST * *) => *))
       (SET-INHIBIT-WARNINGS "theory")
       (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*))
       (LOCAL
        (MUTUAL-RECURSION (DEFUN EVL2 (X A)
                            (DECLARE (XARGS :VERIFY-GUARDS NIL
                                            :MEASURE (ACL2-COUNT X)
                                            :WELL-FOUNDED-RELATION O<
                                            :MODE :LOGIC))
                            (COND ((SYMBOLP X) (CDR (ASSOC-EQ X A)))
                                  ((ATOM X) NIL)
                                  ((EQ (CAR X) 'QUOTE) (CAR (CDR X)))
                                  ((CONSP (CAR X))
                                   (EVL2 (CAR (CDR (CDR (CAR X))))
                                         (PAIRLIS$ (CAR (CDR (CAR X)))
                                                   (EVL2-LIST (CDR X) A))))
                                  ((EQUAL (CAR X) 'F) ; changed f to f2 just below
                                   (F2 (EVL2 (CAR (CDR X)) A)))
                                  ((EQUAL (CAR X) 'F2)
                                   (F2 (EVL2 (CAR (CDR X)) A)))
                                  ((EQUAL (CAR X) 'G) (G))
                                  ((EQUAL (CAR X) 'G2) (G2))
                                  (T NIL)))
                          (DEFUN EVL2-LIST (X-LST A)
                            (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST)
                                            :WELL-FOUNDED-RELATION O<))
                            (COND ((ENDP X-LST) NIL)
                                  (T (CONS (EVL2 (CAR X-LST) A)
                                           (EVL2-LIST (CDR X-LST) A)))))))

       (DEFTHM EVL2-CONSTRAINT-1
         (IMPLIES (SYMBOLP X)
                  (EQUAL (EVL2 X A)
                         (CDR (ASSOC-EQ X A)))))
       (DEFTHM EVL2-CONSTRAINT-2
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'QUOTE))
                  (EQUAL (EVL2 X A) (CADR X))))
       (DEFTHM EVL2-CONSTRAINT-3
         (IMPLIES (AND (CONSP X) (CONSP (CAR X)))
                  (EQUAL (EVL2 X A)
                         (EVL2 (CADDAR X)
                               (PAIRLIS$ (CADAR X)
                                         (EVL2-LIST (CDR X) A))))))
       (DEFTHM EVL2-CONSTRAINT-4
         (IMPLIES (NOT (CONSP X-LST))
                  (EQUAL (EVL2-LIST X-LST A) NIL)))
       (DEFTHM EVL2-CONSTRAINT-5
         (IMPLIES (CONSP X-LST)
                  (EQUAL (EVL2-LIST X-LST A)
                         (CONS (EVL2 (CAR X-LST) A)
                               (EVL2-LIST (CDR X-LST) A)))))
       (DEFTHM EVL2-CONSTRAINT-6
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F))
                  (EQUAL (EVL2 X A) ; changed f to f2 just below
                         (F2 (EVL2 (CADR X) A)))))
       (DEFTHM EVL2-CONSTRAINT-7
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F2))
                  (EQUAL (EVL2 X A)
                         (F2 (EVL2 (CADR X) A)))))
       (DEFTHM EVL2-CONSTRAINT-8
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G))
                  (EQUAL (EVL2 X A) (G))))
       (DEFTHM EVL2-CONSTRAINT-9
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G2))
                  (EQUAL (EVL2 X A) (G2)))))

     (defthm f2-t
        (equal (f2 x) t)
        :hints (("Goal" :by (:functional-instance
                             f-t
                             (f f2)
                             (evl evl2)
                             (evl-list evl2-list)))))

     (defthm bug-implies-nil
        nil
        :hints (("Goal" :use ((:instance f2-t (x t)))))
        :rule-classes nil)

REFINEMENT    record that one equivalence relation refines another

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

     Example:
     (implies (bag-equal x y) (set-equal y x)).

Also see DEFREFINEMENT.

     General Form:
     (implies (equiv1 x y) (equiv2 x y))

Equiv1 and equiv2 must be known equivalence relations.  The effect of
such a rule is to record that equiv1 is a refinement of equiv2.  This
means that equiv1 :rewrite rules may be used while trying to maintain
equiv2.  See EQUIVALENCE for a general discussion of the issues.

The macro form (defrefinement equiv1 equiv2) is an abbreviation for a
defthm of rule-class :refinement that establishes that equiv1 is a
refinement of equiv2.  See DEFREFINEMENT.

Suppose we have the :rewrite rule

     (bag-equal (append a b) (append b a))

which states that append is commutative modulo bag-equality.  Suppose
further we have established that bag-equality refines set-equality.
Then when we are simplifying append expressions while maintaining
set-equality we use append's commutativity property, even though it was
proved for bag-equality.

Equality is known to be a refinement of all equivalence relations.  The
transitive closure of the refinement relation is maintained, so if
set-equality, say, is shown to be a refinement of some third sense of
equivalence, then bag-equality will automatially be known as a
refinement of that third equivalence.

:refinement lemmas cannot be disabled.  That is, once one equivalence
relation has been shown to be a refinement of another, there is no way
to prevent the system from using that information.  Of course,
individual :rewrite rules can be disabled.

More will be written about this as we develop the techniques.