This is documentation for ACL2 Version 4.3
Copyright (C) 2011  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.

FLUSH-COMPRESS    flush the under-the-hood array for the given name

     Example Form:
     (flush-compress 'my-array)

     General Form:
     (flush-compress name)

where name is a symbol.

Recall that (compress1 nm alist) associates an under-the-hood raw Lisp
one-dimensional array of name nm with the given association list,
alist, while (compress2 nm alist) is the analogous function for
two-dimensional arrays; see COMPRESS1 and see
COMPRESS2.  The only purpose of flush-compress, which always returns
nil, is to remove the association of any under-the-hood array with the
given name, thus eliminating slow array accesses (see
SLOW-ARRAY-WARNING).  It is not necessary if the return values of
compress1 and compress2 are always used as the "current" copy of the
named array, and thus flush-compress should rarely, if ever, be needed
in user applications.

Nevertheless, we provide the following contrived example to show how
flush-compress can be used to good effect.  Comments have been added to
this log to provide explanation.

     ACL2 !>(assign a (compress1 'demo
                                 '((:header :dimensions (5)
                                            :maximum-length 15
                                            :default uninitialized
                                            :name demo)
                                   (0 . zero)
                                   (1 . one))))
      ((:HEADER :DIMENSIONS (5)
                :MAXIMUM-LENGTH
                15 :DEFAULT UNINITIALIZED :NAME DEMO)
       (0 . ZERO)
       (1 . ONE))
     ACL2 !>(aref1 'demo (@ a) 0)
     ZERO
     ; As expected, the above evaluation did not cause a slow array warning.  Now
     ; we associate a different under-the-hood array with the name 'demo.
     ACL2 !>(compress1 'demo
                       '((:header :dimensions (5)
                                  :maximum-length 15
                                  :default uninitialized
                                  :name demo)
                         (0 . zero)))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO))
     ; The following array access produces a slow array warning because (@ a) is
     ; no longer associated under-the-hood with the array name 'demo.
     ACL2 !>(aref1 'demo (@ a) 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ; Now we associate under-the-hood, with array name 'demo, an alist equal to
     ; (@ a).
     ACL2 !>(compress1 'demo
                       '((:header :dimensions (5)
                                  :maximum-length 15
                                  :default uninitialized
                                  :name demo)
                         (0 . zero)
                         (1 . one)))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO)
      (1 . ONE))
     ; The following array access is still slow, because the under-the-hood array
     ; is merely associated with a copy of (@ a), not with the actual object
     ; (@ a).
     ACL2 !>(aref1 'demo (@ a) 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ; So we might try to fix the problem by recompressing. But this doesn't
     ; work.  It would work, by the way, if we re-assign a:
     ; (assign a (compress1 'demo (@ a))).  That is why we usually will not need
     ; flush-compress.
     ACL2 !>(compress1 'demo (@ a))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO)
      (1 . ONE))
     ACL2 !>(aref1 'demo (@ a) 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ; Finally, we eliminate the warning by calling flush-compress before we call
     ; compress1.  The call of flush-compress removes any under-the-hood
     ; association of an array with the name 'demo.  Then the subsequent call of
     ; compress1 associates the object (@ a) with that name.  (Technical point:
     ; compress1 always associates the indicated name with the value that it
     ; returns.  in this case, what compress1 returns is (@ a), because (@ a) is
     ; already, logically speaking, a compressed array1p (starts with a :header
     ; and the natural number keys are ordered).
     ACL2 !>(flush-compress 'demo)
     NIL
     ACL2 !>(compress1 'demo (@ a))
     ((:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH
               15 :DEFAULT UNINITIALIZED :NAME DEMO)
      (0 . ZERO)
      (1 . ONE))
     ACL2 !>(aref1 'demo (@ a) 0)
     ZERO
     ACL2 !>

HEADER    return the header of a 1- or 2-dimensional array

     Example Form:
     (header 'delta1 a)

     General Form:
     (header name alist)

where name is arbitrary and alist is a 1- or 2-dimensional array.  This
function returns the header of the array alist.  The function operates
in virtually constant time if alist is the semantic value of name.  See
ARRAYS.

MAXIMUM-LENGTH    return the :maximum-length from the header of an array

     Example Form:
     (maximum-length 'delta1 a)

     General Form:
     (maximum-length name alist)

where name is an arbitrary object and alist is a 1- or 2-dimensional
array.  This function returns the contents of the :maximum-length field
of the header of alist.  Whenever an aset1 or aset2 would cause the
length of the alist to exceed its maximum length, a compress1 or
compress2 is done automatically to remove irrelevant pairs from the
array.  Maximum-length operates in virtually constant time if alist is
the semantic value of name.  See ARRAYS.

SLOW-ARRAY-WARNING    a warning or error issued when arrays are used inefficiently

If you use ACL2 arrays you may sometimes see a *slow array* warning.
We explain below what that warning means and some likely "mistakes" it
may signify.

First, we note that you can control whether or not you get a warning
and, if so, whether or not a break (error from which you can continue;
see BREAK$) ensues:

     (assign slow-array-action :warning) ; warn on slow array access (default)
     (assign slow-array-action :break)   ; warn as above, and then call break$
     (assign slow-array-action nil) ; do not warn or break on slow array access

If you are using ACL2 arrays, then you probably care about performance,
in which case it is probably best to avoid the nil setting.  Below we
assume the default behavior: a warning, but no break.

The discussion in the documentation for arrays defines what we mean by
the semantic value of a name.  As noted there, behind the scenes ACL2
maintains the invariant that with some names there is associated a pair
consisting of an ACL2 array alist, called the semantic value of the
name, and an equivalent raw lisp array.  Access to ACL2 array elements,
as in (aref1 name alist i), is executed in constant time when the array
alist is the semantic value of the name, because we can just use the
corresponding raw lisp array to obtain the answer.  Aset1 and compress1
modify the raw lisp array appropriately to maintain the invariant.

If aref1 is called on a name and alist, and the alist is not the
then-current semantic value of the name, the correct result is computed
but it requires linear time because the alist must be searched.  When
this happens, aref1 prints a *slow array* warning message to the
comment window.  Aset1 behaves similarly because the array it returns
will cause the *slow array* warning every time it is used.

From the purely logical perspective there is nothing "wrong" about such
use of arrays and it may be spurious to print a warning message.  But
because arrays are generally used to achieve efficiency, the *slow
array* warning often means the user's intentions are not being
realized.  Sometimes merely performance expectations are not met; but
the message may mean that the functional behavior of the program is
different than intended.

Here are some "mistakes" that might cause this behavior.  In the
following we suppose the message was printed by aset1 about an array
named name.  Suppose the alist supplied aset1 is alist.

(1) Compress1 was never called on name and alist.  That is, perhaps you
created an alist that is an array1p and then proceeded to access it
with aref1 but never gave ACL2 the chance to create a raw lisp array
for it.  After creating an alist that is intended for use as an array,
you must do (compress1 name alist) and pass the resulting alist' as the
array.

(2) Name is misspelled.  Perhaps the array was compressed under the
name 'delta-1 but accessed under 'delta1?

(3) An aset1 was done to modify alist, producing a new array, alist',
but you subsequently used alist as an array.  Inspect all (aset1 name
...) occurrences and make sure that the alist modified is never used
subsequently (either in that function or any other).  It is good
practice to adopt the following syntactic style.  Suppose the alist you
are manipulating is the value of the local variable alist.  Suppose at
some point in a function definition you wish to modify alist with
aset1.  Then write

     (let ((alist (aset1 name alist i val))) ...)

and make sure that the subsequent function body is entirely within the
scope of the let.  Any uses of alist subsequently will refer to the new
alist and it is impossible to refer to the old alist.  Note that if you
write

      (foo (let ((alist (aset1 name alist i val))) ...)  ; arg 1
           (bar alist))                                  ; arg 2

you have broken the rules, because in arg 1 you have modified alist but
in arg 2 you refer to the old value.  An appropriate rewriting is to
lift the let out:

      (let ((alist (aset1 name alist alist i val)))
        (foo ...                                         ; arg 1
             (bar alist)))                               ; arg 2

Of course, this may not mean the same thing.

(4) A function which takes alist as an argument and modifies it with
aset1 fails to return the modified version.  This is really the same as
(3) above, but focuses on function interfaces.  If a function takes an
array alist as an argument and the function uses aset1 (or a
subfunction uses aset1, etc.), then the function probably "ought" to
return the result produced by aset1.  The reasoning is as follows.  If
the array is passed into the function, then the caller is holding the
array.  After the function modifies it, the caller's version of the
array is obsolete.  If the caller is going to make further use of the
array, it must obtain the latest version, i.e., that produced by the
function.

BACKCHAIN-LIMIT    limiting the effort expended on relieving hypotheses

Before ACL2 can apply a rule with hypotheses, it must establish that the
hypotheses are true.  (We ignore the relaxing of this requirement
afforded by case-splits and forced hypotheses.)  ACL2 typically
establishes each hypothesis by backchaining -- instantiating the
hypothesis and then rewriting it recursively.  Here we describe how
ACL2 allows the user to limit backchaining.  At the end, below, we
describe the function backchain-limit.

Each hypothesis of a rewrite, meta, linear, or type-prescription rule
is assigned a backchain-limit when the rule is stored.  By default,
this limit is nil, denoting infinity (no limit).  However, the value
used for the default may be set to a non-negative integer (or to nil)
by the user; see SET-DEFAULT-BACKCHAIN-LIMIT.  The default is
overridden when a :backchain-limit-lst is supplied explicitly with the
rule; see RULE-CLASSES.  The number of recursive applications of
backchaining starting with the hypothesis of a rule is limited to the
backchain-limit associated with that hypothesis.

Moreover, the user may set global backchain-limits that limit the total
backchaining depth.  See SET-BACKCHAIN-LIMIT.  One limit is for
the use of rewrite, meta, and linear rules, while the other limit is
for so-called "type-set reasoning", which uses rules of class
type-prescription rules.  The two limits operate independently.  Below,
we discuss the first kind of backchain limits, i.e., for other than
type-prescription rules, except as otherwise indicated; but the
mechanism for those rules is similar.

Below we lay out the precise sense in which a global backchain-limit
interacts with the backchain-limits of individual rules in order to
limit backchaining.  But first we note that when further backchaining is
disallowed, ACL2 can still prove a hypothesis in a given context by
using that contextual information.  In fact, type-set reasoning may be
used (except that a weaker version of it is used in the second case
above, i.e., where we are already doing type-set reasoning).  Thus, the
relieving of hypotheses may be limited to the use of contextual
information (without backchaining, i.e., without recursively rewriting
hypotheses) by executing :set-backchain-limit 0.

Recall that there are two sorts of backchain limits: those applied to
hypotheses of individual rules, as assigned by their :rule-classes or
else taken from the default (see SET-DEFAULT-BACKCHAIN-LIMIT);
and the global limit, initially nil (no limit) but settable with
:set-backchain-limit.  Here is how these two types of limits interact
to limit backchaining, i.e., recursive rewriting of hypotheses.  ACL2
maintains a current backchain limit, which is the limit on the depth of
recursive calls to the rewriter, as well as a current backchain depth,
which is initially 0 and is incremented each time ACL2 backchains (and
is decremented when a backchain completes).  When ACL2 begins to
rewrite a literal (crudely, one of the "top-level" terms of the goal
currently being worked on), it sets the current backchain-limit to the
global value, which is initially nil but can be set using
:set-backchain-limit.  When ACL2 is preparing to relieve a hypothesis
by backchaining (hence, after it has already tried type-set reasoning),
it first makes sure that the current backchain limit is greater than
the current backchain depth.  If not, then it refuses to relieve that
hypothesis.  Otherwise, it increments the current backchain depth and
calculates a new current backchain-limit by taking the minimum of two
values: the existing current backchain-limit, and the sum of the
current backchain depth and the the backchain-limit associated with the
hypothesis.  Thus, ACL2 only modifies the current backchain-limit if it
is necessary to decrease that limit in order to respect the backchain
limit associated with the hypothesis.

We illustrate with the following examples.

     ; We stub out some functions so that we can reason about them.

     (defstub p0 (x) t)
     (defstub p1 (x) t)
     (defstub p2 (x) t)
     (defstub p3 (x) t)

     ; Initially, the default-backchain-limit is nil, or infinite.

     (defaxiom p2-implies-p1-limitless
       (implies (p2 x)
                (p1 x)))

     ; The following rule will have a backchain-limit of 0.

     (defaxiom p1-implies-p0-limit-0
       (implies (p1 x)
                (p0 x))
       :rule-classes ((:rewrite :backchain-limit-lst 0)))

     ; We have (p2 x) ==> (p1 x) ==> (p0 x).  We wish to establish that
     ; (p2 x) ==> (p0 x).  Normally, this would be no problem, but here
     ; we fail because ACL2 cannot establish (p0 x) by type-set reasoning
     ; alone.

     (thm
       (implies (p2 x)
                (p0 x)))

     ; We set the default-backchain-limit (for rewriting) to 1.

     :set-default-backchain-limit 1

     ; The following is more powerful than p1-implies-p0-limit-0
     ; because it can use rewrite rules to establish (p1 x).

     (defaxiom p1-implies-p0-limit-1
       (implies (p1 x)
                (p0 x)))

     ; This theorem will succeed:

     (thm
       (implies (p2 x)
                (p0 x)))

     ; We return the default-backchain-limit to its initial value.

     :set-default-backchain-limit nil

     ; Here is our last axiom.

     (defaxiom p3-implies-p2-limitless
       (implies (p3 x)
                (p2 x)))

     ; We now have (p3 x) ==> (p2 x) ==> (p1 x) ==> (p0 x).  However the
     ; rule p1-implies-p0-limit-1 has a backchain-limit of 1; hence we
     ; are not allowed to backchain far enough back to use
     ; p3-implies-p2-limitless.  We therefore lose.

     (defthm will-fail
       (implies (p3 x)
                (p0 x)))

Finally, we remark that to see the current global backchain-limits,
issue the following commands.

     (backchain-limit wrld :ts) ; backchain limit for type-set reasoning
     (backchain-limit wrld :rewrite) ; backchain limit for rewriting

BACKCHAIN-LIMIT-RW    hints keyword :BACKCHAIN-LIMIT-RW

See HINTS.

BACKTRACK    hints keyword :BACKTRACK

See HINTS.

BIBLIOGRAPHY    reports about ACL2

For a list of notes and reports about ACL2, see
`http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html'.

BIND-FREE    to bind free variables of a rewrite or linear rule

     Examples:
     (IMPLIES (AND (RATIONALP LHS)
                   (RATIONALP RHS)
                   (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
              (EQUAL (EQUAL LHS RHS)
                     (EQUAL (+ (- X) LHS) (+ (- X) RHS))))

     (IMPLIES (AND (BIND-FREE
                     (FIND-RATIONAL-MATCH-IN-TIMES-NESTS LHS RHS MFC STATE)
                     (X))
                   (RATIONALP X)
                   (CASE-SPLIT (NOT (EQUAL X 0))))
              (EQUAL (< LHS RHS)
                     (IF (< 0 X)
                         (< (* (/ X) LHS) (* (/ X) RHS))
                        (< (* (/ X) RHS) (* (/ X) LHS)))))

General Forms:

     (BIND-FREE term var-list)
     (BIND-FREE term t)
     (BIND-FREE term)

A rule which uses a bind-free hypothesis has similarities to both a
rule which uses a syntaxp hypothesis and to a :meta rule.  Bind-free is
like syntaxp, in that it logically always returns t but may affect the
application of a :rewrite or :linear rule when it is called at the
top-level of a hypothesis.  It is like a :meta rule, in that it allows
the user to perform transformations of terms under progammatic control.

Note that a bind-free hypothesis does not, in general, deal with the
meaning or semantics or values of the terms, but rather with their
syntactic forms.  Before attempting to write a rule which uses
bind-free, the user should be familiar with syntaxp and the internal
form that ACL2 uses for terms.  This internal form is similar to what
the user sees, but there are subtle and important differences.  Trans
can be used to view this internal form.

Just as for a syntaxp hypothesis, there are two types of bind-free
hypotheses.  The simpler type of bind-free hypothesis may be used as
the nth hypothesis in a :rewrite or :linear rule whose :corollary is
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided term is
a term, term contains at least one variable, and every variable
occuring freely in term occurs freely in lhs or in some hypi, i<n.  In
addition, term must not use any stobjs.  (Later below we will describe
the second type, an _extended_ bind-free hypothesis, which may use
state.)

We begin our description of bind-free by examining the first example
above in some detail.

We wish to write a rule which will cancel "like" addends from both
sides of an equality.  Clearly, one could write a series of rules such
as

     (DEFTHM THE-HARD-WAY-2-1
        (EQUAL (EQUAL (+ A X B)
                      (+ X C))
               (EQUAL (+ A B)
                      (FIX C))))

with one rule for each combination of positions the matching addends
might be found in (if one knew before-hand the maximum number of
addends that would appear in a sum).  But there is a better way.  (In
what follows, we assume the presence of an appropriate set of rules for
simplifying sums.)

Consider the following definitions and theorem:

     (DEFUN INTERSECTION-EQUAL (X Y)
       (COND ((ENDP X)
              NIL)
             ((MEMBER-EQUAL (CAR X) Y)
              (CONS (CAR X) (INTERSECTION-EQUAL (CDR X) Y)))
             (T
              (INTERSECTION-EQUAL (CDR X) Y))))

     (DEFUN PLUS-LEAVES (TERM)
       (IF (EQ (FN-SYMB TERM) 'BINARY-+)
           (CONS (FARGN TERM 1)
                 (PLUS-LEAVES (FARGN TERM 2)))
         (LIST TERM)))

     (DEFUN FIND-MATCH-IN-PLUS-NESTS (LHS RHS)
       (IF (AND (EQ (FN-SYMB LHS) 'BINARY-+)
                (EQ (FN-SYMB RHS) 'BINARY-+))
           (LET ((COMMON-ADDENDS (INTERSECTION-EQUAL (PLUS-LEAVES LHS)
                                                     (PLUS-LEAVES RHS))))
             (IF COMMON-ADDENDS
                 (LIST (CONS 'X (CAR COMMON-ADDENDS)))
               NIL))
         NIL))

     (DEFTHM CANCEL-MATCHING-ADDENDS-EQUAL
       (IMPLIES (AND (RATIONALP LHS)
                     (RATIONALP RHS)
                     (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
                (EQUAL (EQUAL LHS RHS)
                       (EQUAL (+ (- X) LHS) (+ (- X) RHS)))))

How is this rule applied to the following term?

     (equal (+ 3 (expt a n) (foo a c))
            (+ (bar b) (expt a n)))

As mentioned above, the internal form of an ACL2 term is not always
what one sees printed out by ACL2.  In this case, by using :trans one
can see that the term is stored internally as

     (equal (binary-+ '3
                      (binary-+ (expt a n) (foo a c)))
            (binary-+ (bar b) (expt a n))).

When ACL2 attempts to apply cancel-matching-addends-equal to the term
under discussion, it first forms a substitution that instantiates the
left-hand side of the conclusion so that it is identical to the target
term.  This substitution is kept track of by the substitution alist:

     ((LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))).

ACL2 then attempts to relieve the hypotheses in the order they were
given. Ordinarily this means that we instantiate each hypothesis with
our substitution and then attempt to rewrite the resulting instance to
true.  Thus, in order to relieve the first hypothesis, we rewrite:

     (RATIONALP (binary-+ '3
                           (binary-+ (expt a n) (foo a c)))).

Let us assume that the first two hypotheses rewrite to t.  How do we
relieve the bind-free hypothesis?  Just as for a syntaxp hypothesis,
ACL2 evaluates (find-match-in-plus-nests lhs rhs) in an environment
where lhs and rhs are instantiated as determined by the substitution.
In this case we evaluate

     (FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3
                                           (binary-+ (expt a n) (foo a c)))
                               '(binary-+ (bar b) (expt a n))).

Observe that, just as in the case of a syntaxp hypothesis, we
substitute the quotation of the variables bindings into the term to be
evaluated.  See SYNTAXP for the reasons for this.  The result
of this evaluation, ((X . (EXPT A N))), is then used to extend the
substitution alist:

     ((X . (EXPT A N))
      (LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))),

and this extended substitution determines
cancel-matching-addends-equal's result:

     (EQUAL (+ (- X) LHS) (+ (- X) RHS))
     ==>
     (EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C))
            (+ (- (EXPT A N)) (BAR B) (EXPT A N))).

Question: What is the internal form of this result?
Hint: Use :trans.

When this rule fires, it adds the negation of a common term to both
sides of the equality by selecting a binding for the otherwise-free
variable x, under programmatic control.  Note that other mechanisms
such as the binding of free-variables may also extend the substitution
alist.

Just as for a syntaxp test, a bind-free form signals failure by
returning nil.  However, while a syntaxp test signals success by
returning true, a bind-free form signals success by returning an alist
which is used to extend the current substitution alist.  Because of
this use of the alist, there are several restrictions on it -- in
particular the alist must only bind variables, these variables must not
be already bound by the substitution alist, and the variables must be
bound to ACL2 terms.  If term returns an alist and the alist meets
these restrictions, we append the alist to the substitution alist and
use the result as the new current substitution alist.  This new current
substitution alist is then used when we attempt to relieve the next
hypothesis or, if there are no more, instantiate the right hand side of
the rule.

There is also a second, optional, var-list argument to a bind-free
hypothesis.  If provided, it must be either t or a list of variables.
If it is not provided, it defaults to t.  If it is a list of variables,
this second argument is used to place a further restriction on the
possible values of the alist to be returned by term: any variables
bound in the alist must be present in the list of variables.  We
strongly recommend the use of this list of variables, as it allows some
consistency checks to be performed at the time of the rule's admittance
which are not possible otherwise.

An extended bind-free hypothesis is similar to the simple type
described above, but it uses two additional variables, mfc and state,
which must not be bound by the left hand side or an earlier hypothesis
of the rule.  They must be the last two variables mentioned by term:
first mfc, then state.  These two variables give access to the
functions mfc-xxx; see EXTENDED-METAFUNCTIONS.  As described
there, mfc is bound to the so-called metafunction-context and state to
ACL2's state.  See BIND-FREE-EXAMPLES for examples of the use
of these extended bind-free hypotheses.

BIND-FREE-EXAMPLES    examples pertaining to bind-free hypotheses

See BIND-FREE for a basic discussion of the use of bind-free to
control rewriting.

We give examples of the use of bind-free hypotheses from the
perspective of a user interested in reasoning about arithmetic, but it
should be clear that bind-free can be used for many other purposes also.

EXAMPLE 1:  Cancel a common factor.

     (defun bind-divisor (a b)

     ; If a and b are polynomials with a common factor c, we return a
     ; binding for x.  We could imagine writing get-factor to compute the
     ; gcd, or simply to return a single non-invertible factor.

       (let ((c (get-factor a b)))
         (and c (list (cons 'x c)))))

     (defthm cancel-factor
       ;; We use case-split here to ensure that, once we have selected
       ;; a binding for x, the rest of the hypotheses will be relieved.
       (implies (and (acl2-numberp a)
                     (acl2-numberp b)
                     (bind-free (bind-divisor a b) (x))
                     (case-split (not (equal x 0)))
                     (case-split (acl2-numberp x)))
                (iff (equal a b)
                     (equal (/ a x) (/ b x)))))

EXAMPLE 2:  Pull integer summand out of floor.  Note:  This example has
an _extended_ bind-free hypothesis, which uses the term
(find-int-in-sum sum mfc state).

     (defun fl (x)
       ;; This function is defined, and used, in the IHS books.
       (floor x 1))

     (defun int-binding (term mfc state)
       ;; The call to mfc-ts returns the encoded type of term. ;
       ;; Thus, we are asking if term is known by type reasoning to ;
       ;; be an integer. ;
       (declare (xargs :stobjs (state) :mode :program))
       (if (ts-subsetp (mfc-ts term mfc state)
                       *ts-integer*)
           (list (cons 'int term))
         nil))

     (defun find-int-in-sum (sum mfc state)
       (declare (xargs :stobjs (state) :mode :program))
       (if (and (nvariablep sum)
                (not (fquotep sum))
                (eq (ffn-symb sum) 'binary-+))
           (or (int-binding (fargn sum 1) mfc state)
               (find-int-in-sum (fargn sum 2) mfc state))
         (int-binding sum mfc state)))

     ; Some additional work is required to prove the following.  So for
     ; purposes of illustration, we wrap skip-proofs around the defthm.

     (skip-proofs
      (defthm cancel-fl-int
       ;; The use of case-split is probably not needed, since we should
       ;; know that int is an integer by the way we selected it.  But this
       ;; is safer.
        (implies (and (acl2-numberp sum)
                      (bind-free (find-int-in-sum sum mfc state) (int))
                      (case-split (integerp int)))
                 (equal (fl sum)
                        (+ int (fl (- sum int)))))
        :rule-classes ((:rewrite :match-free :all)))
     )

     ; Arithmetic libraries will have this sort of lemma.
     (defthm hack (equal (+ (- x) x y) (fix y)))

     (in-theory (disable fl))

     (thm (implies (and (integerp x) (acl2-numberp y))
                   (equal (fl (+ x y)) (+ x (fl y)))))

EXAMPLE 3:  Simplify terms such as (equal (+ a (* a b)) 0)

     (defun factors (product)
       ;; We return a list of all the factors of product.  We do not
       ;; require that product actually be a product.
       (if (eq (fn-symb product) 'BINARY-*)
           (cons (fargn product 1)
                 (factors (fargn product 2)))
         (list product)))

     (defun make-product (factors)
       ;; Factors is assumed to be a list of ACL2 terms.  We return an
       ;; ACL2 term which is the product of all the ellements of the
       ;; list factors.
       (cond ((atom factors)
              ''1)
             ((null (cdr factors))
              (car factors))
             ((null (cddr factors))
              (list 'BINARY-* (car factors) (cadr factors)))
             (t
              (list 'BINARY-* (car factors) (make-product (cdr factors))))))

     (defun quotient (common-factors sum)
       ;; Common-factors is a list of ACL2 terms.   Sum is an ACL2 term each
       ;; of whose addends have common-factors as factors.  We return
       ;; (/ sum (make-product common-factors)).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((first (make-product (set-difference-equal (factors (fargn sum 1))
                                                            common-factors))))
             (list 'BINARY-+ first (quotient common-factors (fargn sum 2))))
         (make-product (set-difference-equal (factors sum)
                                             common-factors))))

     (defun intersection-equal (x y)
       (cond ((endp x)
              nil)
             ((member-equal (car x) y)
              (cons (car x) (intersection-equal (cdr x) y)))
             (t
              (intersection-equal (cdr x) y))))

     (defun common-factors (factors sum)
       ;; Factors is a list of the factors common to all of the addends
       ;; examined so far.  On entry, factors is a list of the factors in
       ;; the first addend of the original sum, and sum is the rest of the
       ;; addends.  We sweep through sum, trying to find a set of factors
       ;; common to all the addends of sum.
       (declare (xargs :measure (acl2-count sum)))
       (cond ((null factors)
              nil)
             ((eq (fn-symb sum) 'BINARY-+)
              (common-factors (intersection-equal factors (factors (fargn sum 1)))
                              (fargn sum 2)))
             (t
              (intersection-equal factors (factors sum)))))

     (defun simplify-terms-such-as-a+ab-rel-0-fn (sum)
       ;; If we can find a set of factors common to all the addends of sum,
       ;; we return an alist binding common to the product of these common
       ;; factors and binding quotient to (/ sum common).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((common-factors (common-factors (factors (fargn sum 1))
                                                 (fargn sum 2))))
             (if common-factors
                 (let ((common (make-product common-factors))
                       (quotient (quotient common-factors sum)))
                   (list (cons 'common common)
                         (cons 'quotient quotient)))
               nil))
         nil))

     (defthm simplify-terms-such-as-a+ab-=-0
       (implies (and (bind-free
                      (simplify-terms-such-as-a+ab-rel-0-fn sum)
                      (common quotient))
                     (case-split (acl2-numberp common))
                     (case-split (acl2-numberp quotient))
                     (case-split (equal sum
                                        (* common quotient))))
                (equal (equal sum 0)
                       (or (equal common 0)
                           (equal quotient 0)))))

     (thm (equal (equal (+ u (* u v)) 0)
           (or (equal u 0) (equal v -1))))

BREAKS    Common Lisp breaks

     Example:
     Broken at PROVE.  Type :H for Help.
     >>:Q

     ACL2 !>

You may interrupt the system by typing various control character
sequences.  The precise sequences are determined by the host Lisp and
operating system environment.  For example, in GCL and Allegro Common
Lisp, a console interrupt is caused by typing "ctrl-c".  If, however,
the GCL or Allegro is running in an Emacs shell buffer, one must type
"ctrl-c ctrl-c".

If a break occurs, for example because of a bug in ACL2 or a user
interrupt, the break will run a Common Lisp read-eval-print loop, not
an ACL2 read-eval-print loop.  This may not be obvious if the prompts
in the two loops are similar.  Because you are typing to a Common Lisp
evaluator, you must be careful.  It is possible to damage your ACL2
state in irreparable ways by executing non-ACL2 Common Lisp.  It is
even possible to disrupt and render inaccurate the interrupted
evaluation of a simple ACL2 expression.

For ACL2 built on most host Common Lisps, you will see the string [RAW
LISP] in the prompt at a break, to emphasize that one is inside a break
and hence should quit from the break.  For some host Common Lisps, the
top-level prompt also contains the string [RAW LISP].  See
PROMPT for how to control printing of that string.

The most reliable way to return to the ACL2 top level is by executing
the following command: (abort!).  Appropriate cleanup will then be
done, which should leave you in an appropriate state.

However, you may be able to quit from the break in the normal Lisp
manner (as with :q in GCL, :reset in Allegro CL, and q in CMU CL).  If
this attempt to quit is successful, it will return you to the innermost
ACL2 read-eval-print loop, with appropriate cleanup performed first.
Note that if you are within a brr environment when the break occurs,
quitting from the break will only return you to that environment, not
to the top of ACL2's read-eval-print loop.

BY    hints keyword :BY

See HINTS.

CANONICAL-PATHNAME    the true absolute filename, with soft links resolved

For the name fname of a file, the form (Canonical-pathname fname nil
state) evaluates to a Unix-style absolute filename representing the
same file as fname, but generally without any use of soft links in the
name.  (Below, we explain the qualifier "generally".)  If however the
file indicated by fname does not exist, (canonical-pathname fname nil
state) is nil.  Thus, canonical-pathname can be used as one would use
the raw Lisp function probe-file.

The specification of (Canonical-pathname fname dir-p state) when dir-p
is not nil is simlar, except that if the specified file exists but is
not a directory, then the result is nil.

The function canonical-pathname has a guard of t, though the second
argument must be the ACL2 state.  This function is introduced with the
following properties.

     (defthm canonical-pathname-is-idempotent
       (equal (canonical-pathname (canonical-pathname x dir-p state) dir-p state)
              (canonical-pathname x dir-p state)))
     (defthm canonical-pathname-type
       (or (equal (canonical-pathname x dir-p state) nil)
           (stringp (canonical-pathname x dir-p state)))
       :rule-classes :type-prescription)

We use the qualifier "generally", above, because there is no guarantee
that the filename will be canonical without soft links, though we
expect this to be true in practice.  ACL2 attempts to compute the
desired result and then checks that the input and result have the same
Common Lisp "truename".  This check is expected to succeed, but if it
fails then the input string is returned unchanged, and to be
conservative, the value returned is nil in this case if dir-p is true.

CASE-SPLIT    like force but immediately splits the top-level goal on the hypothesis

When a hypothesis of a conditional rule has the form (case-split hyp)
it is logically equivalent to hyp.  However it affects the application
of the rule generated as follows:  if ACL2 attempts to apply the rule
but cannot establish that the required instance of hyp holds in the
current context, it considers the hypothesis true anyhow, but (assuming
all hypotheses are seen to be true and the rule is applied) creates a
subgoal in which that instance of hyp is assumed false.  (There are
exceptions, noted below.)

For example, given the rule

     (defthm p1->p2
       (implies (case-split (p1 x))
                (p2 x)))

then an attempt to prove

     (implies (p3 x) (p2 (car x)))

can give rise to a single subgoal:

     (IMPLIES (AND (NOT (P1 (CAR X))) (P3 X))
              (P2 (CAR X))).

Unlike force, case-split does not delay the "false case" to a forcing
round but tackles it more or less immediately.

The special "split" treatment of case-split can be disabled by
disabling forcing:  see FORCE for a discussion of disabling
forcing, and also see DISABLE-FORCING.  Finally, we should
mention that the rewriter is never willing to split when there is an if
term present in the goal being simplified.  Since and terms and or
terms are merely abbreviations for if terms, they also prevent
splitting.  Note that if terms are ultimately eliminated using the
ordinary flow of the proof (but see
SET-CASE-SPLIT-LIMITATIONS), so case-split will ultimately function
as intended.

When in the proof checker, case-split behaves like force.

CASE-SPLIT-LIMITATIONS    a list of two "numbers" limiting the number of cases produced at once

     Examples:
     ACL2 !>(case-split-limitations (w state))
     (500 100)

With the setting above, clausify will not try subsumption/replacement
if more than 500 clauses are involved.  Furthermore, the simplifier, as
it sweeps over a clause, will inhibit further case splits when it has
accumulated 100 subgoals.  This inhibition is implemented by continuing
to rewrite subsequent literals but not splitting out their cases.  This
can produce literals containing IFs.

See SET-CASE-SPLIT-LIMITATIONS for a more general discussion.

CASES    hints keyword :CASES

See HINTS.

CHECK-SUM    assigning "often unique" integers to files and objects

A "check sum" is an integer in some fixed range computed from the
printed representation of an object, e.g., the sum, modulo 2**32, of
the ascii codes of all the characters in the printed representation.

Ideally, you would like the check sum of an object to be uniquely
associated with that object, like a fingerprint.  It could then be used
as a convenient way to recognize the object in the future: you could
remember the check sum (which is relatively small) and when an object
is presented to you and alleged to be the special one you could compute
its check sum and see if indeed it was.  Alas, there are many more
objects than check sums (after all, each check sum is an object, and
then there's t).  So you try to design a check sum algorithm that maps
similar looking objects far apart, in the hopes that corruptions and
counterfeits -- which appear to be similar to the object -- have
different check sums.  Nevertheless, the best you can do is a
many-to-one map.  If an object with a different check sum is presented,
you can be positive it is not the special object.  But if an object
with the same check sum is presented, you have no grounds for positive
identification.

The basic check sum algorithm in ACL2 is called check-sum-obj, which
computes the check sum of an ACL2 object.  Roughly speaking, we scan
the print representation of the object and, for each character
encountered, we multiply the ascii code of the character times its
position in the stream (modulo a certain prime) and then add (modulo a
certain prime) that into the running sum.  This is inaccurate in many
senses (for example, we don't always use the ascii code and we see
numbers as though they were printed in base 127) but indicates the
basic idea.

ACL2 uses check sums to increase security in the books mechanism; see
CERTIFICATE.

CLAUSE-IDENTIFIER    the internal form of a goal-spec

To each goal-spec, str, there corresponds a clause-identifier produced
by (parse-clause-id str).  For example,

     (parse-clause-id "[2]Subgoal *4.5.6/7.8.9'''")

returns ((2 4 5 6) (7 8 9) . 3).

The function string-for-tilde-@-clause-id-phrase inverts
parse-clause-id in the sense that given a clause identifier it returns
the corresponding goal-spec.

As noted in the documentation for goal-spec, each clause printed in the
theorem prover's proof attempt is identified by a name.  When these
names are represented as strings they are called "goal specs."  Such
strings are used to specify where in the proof attempt a given hint is
to be applied.  The function parse-clause-id converts goal-specs into
clause identifiers, which are cons-trees containing natural numbers.

Examples of goal-specs and their corresponding clause identifiers are
shown below.

                  parse-clause-id
                        -->

     "Goal"                       ((0) NIL . 0)
     "Subgoal 3.2.1'"             ((0) (3 2 1) . 1)
     "[2]Subgoal *4.5.6/7.8.9'''" ((2 4 5 6) (7 8 9) . 3)

                        <--
           string-for-tilde-@-clause-id-phrase

The caar of a clause id specifies the forcing round, the cdar specifies
the goal being proved by induction, the cadr specifies the particular
subgoal, and the cddr is the number of primes in that subgoal.

Internally, the system maintains clause ids, not goal-specs.  The
system prints clause ids in the form shown by goal-specs.  When a
goal-spec is used in a hint, it is parsed (before the proof attempt
begins) into a clause id.  During the proof attempt, the system watches
for the clause id and uses the corresponding hint when the id arises.
(Because of the expense of creating and garbage collecting a lot of
strings, this design is more efficient than the alternative.)

COMMAND    forms you type at the top-level, but...

...the word "command" usually refers to a top-level form whose
evaluation produces a new logical world.

     Typical commands are:
     (defun foo (x) (cons x x))
     (defthm consp-foo (consp (foo x)))
     (defrec pair (hd . tl) nil)

The first two forms are examples of commands that are in fact primitive
events.  See EVENTS.  Defrec, on the other hand, is a macro
that expands into a progn of several primitive events.  In general, a
world extending command generates one or more events.

Both events and commands leave landmarks on the world that enable us to
determine how the given world was created from the previous one.  Most
of your interactions will occur at the command level, i.e., you type
commands, you print previous commands, and you undo back through
commands.  Commands are denoted by command descriptors.  See
COMMAND-DESCRIPTOR.

COMMAND-DESCRIPTOR    an object describing a particular command typed by the user

     Examples:

     :max      ; the command most recently typed by the user
     :x        ; synonymous with :max
     (:x -1)   ; the command before the most recent one
     (:x -2)   ; the command before that
     :x-2      ; synonymous with (:x -2)
     5         ; the fifth command typed by the user
     1         ; the first command typed by the user
     0         ; the last command of the system initialization
     -1        ; the next-to-last initialization command
     :min      ; the first command of the initialization
     :start    ; the last command of the initial ACL2 logical world
     fn        ; the command that introduced the logical name fn
     (:search (defmacro foo-bar))
               ; the first command encountered in a search from :max to
               ; 0 that either contains defmacro and foo-bar in the
               ; command form or contains defmacro and foo-bar in some
               ; event within its block.

The recorded history of your interactions with the top-level ACL2
command loop is marked by the commands you typed that changed the
logical world.  Each such command generated one or more events, since
the only way for you to change the logical world is to execute an event
function.  See COMMAND and see EVENTS.  We divide
history into "command blocks," grouping together each world changing
command and its events.  A "command descriptor" is an object that can
be used to describe a particular command in the history of the ongoing
session.

Each command is assigned a unique integer called its "command number"
which indicates the command's position in the chronological ordering of
all of the commands ever executed in this session (including those
executed to initialize the system).  We assign the number 1 to the
first command you type to ACL2.  We assign 2 to the second and so on.
The non-positive integers are assigned to "prehistoric" commands, i.e.,
the commands used to initialize the ACL2 system: 0 is the last command
of the initialization, -1 is the one before that, etc.

The legal command descriptors are described below.  We use n to denote
any integer, sym to denote any logical name (see LOGICAL-NAME),
and cd to denote, recursively, any command descriptor.

      command                   command
     descriptor                described

     :max   -- the most recently executed command (i.e., the one with
               the largest command number)
     :x     -- synonymous with :max
     :x-k   -- synonymous with (:x -k), if k is an integer and k>0
     :min   -- the earliest command (i.e., the one with the smallest
               command number and hence the first command of the system
               initialization)
     :start -- the last command when ACL2 starts up
     n      -- command number n  (If n is not in the
               range :min<=n<=:max, n is replaced by the nearest of :min
               and :max.)
     sym    -- the command that introduced the logical name sym
     (cd n) -- the command whose number is n plus the command number of
               the command described by cd
     (:search pat cd1 cd2)
               In this command descriptor, pat must be either an atom or
               a true list of atoms and cd1 and cd2 must be command
               descriptors.  We search the interval from cd1 through cd2
               for the first command that matches pat.  Note that if cd1
               occurs chronologically after cd2, the search is
               ``backwards'' through history while if cd1 occurs
               chronologically before cd2, the search is ``forwards''.  A
               backwards search will find the most recent match; a
               forward search will find the chronologically earliest
               match.  A command matches pat if either the command form
               itself or one of the events in the block contains pat (or
               all of the atoms in pat if pat is a list).
     (:search pat)
               the command found by (:search pat :max 0), i.e., the most
               recent command matching pat that was part of the user's
               session, not part of the system initialization.

COMMON-LISP    relation to Common Lisp, including deviations from the spec

ACL2 is a logic, a theorem prover, and a programming language based on
Common Lisp.  A connection with Common Lisp is established with guards
(see GUARD).

However, here we document potential deviations from Common Lisp
semantics even in the presence of verified guards.  Our view is that
these deviations are extremely unlikely to manifest; indeed, as of this
writing we are unaware of any cases in which these issues arise in
practice.  However, we feel obligated to acknowledge their possibility,
which could result in surprises during evaluation or even proof.

The Common Lisp spec allows certain predicates to return what it calls
"generalized Booleans," which are really arbitrary values that are to be
viewed as either nil or non-nil.  However, in ACL2 these functions are
assumed to return nil or t.  For details,see
GENERALIZED-BOOLEANS.

The execution of forms with :program mode functions can result in calls
of functions on arguments that do not satisfy their guards.  In
practice, this simply causes hard Lisp errors.  But in principle one
could imagine a damaged Lisp image that operates incorrectly.  See
DEFUN-MODE-CAVEAT.

The Common Lisp spec, specifically Section 3.2.2.3 of the Common Lisp
HyperSpec, allows for undefined results when a function is "multiply
defined" in a compiled file.  ACL2 allows redundant defuns in a book,
and in general books are compiled by certify-book (but see
CERTIFY-BOOK and see COMPILATION for how to control such
compilation).  Moreover, ACL2 provides a redefinition capability (see
LD-REDEFINITION-ACTION and see REDEF), and the above
section also allows for undefined results when a function is defined in
a compiled file and then redefined, presumably (for example) because of
inlining.

DEFUN-MODE-CAVEAT    potential soundness issue for functions with defun-mode :program

Technically speaking, in the current implementation, the execution of
functions having defun-mode :program may damage the ACL2 system in a
way that renders it unsound.  In practice, we have never seen this
happen; so, the explanations below can be viewed as extremely paranoid.
Nevertheless, here we document this concern, even if it should be taken
with more than a grain of salt.

See DEFUN-MODE for a discussion of defun-modes.  That discussion
describes an imagined implementation that is slightly different from
this one.  This note explains that the current implementation is open to
unsoundness.

For discussion of a different soundness issue that is also related to
function execution, see GENERALIZED-BOOLEANS.

The execution of a function having defun-mode :program may violate
Common Lisp guards on the subroutines used.  (This may be true even for
calls of a function on arguments that satisfy its guard, because ACL2
has not verified that its guard is sufficient to protect its
subroutines.)  When a guard is violated at runtime all bets are off.
That is, no guarantees are made either about the answer being "right"
or about the continued rationality of the ACL2 system itself.

For example, suppose you make the following defun:

     (defun crash (i)
       (declare (xargs :mode :program :guard (integerp i)))
       (car i))

Note that the declared guard does not in fact adequately protect the
subroutines in the body of crash; indeed, satisfying the guard to crash
will guarantee that the car expression is in violation of its guard.
Because this function is admitted in :program-mode, no checks are made
concerning the suitability of the guard.  Furthermore, in the current
ACL2 implementation, crash is executed directly in Common Lisp.  Thus
if you call crash on an argument satisfying its guard you will cause an
erroneous computation to take place.

     ACL2 !>(crash 7)

     Error: Caught fatal error [memory may be damaged]
     ...

There is no telling how much damage is done by this errant computation.
In some lisps your ACL2 job may actually crash back to the operating
system.  In other lisps you may be able to recover from the "hard
error" and resume ACL2 in a damaged but apparently functional image.

THUS, HAVING A FUNCTION WITH DEFUN-MODE :PROGRAM IN YOUR SYSTEM
ABSOLVES US, THE ACL2 IMPLEMENTORS, FROM RESPONSIBILITY FOR THE
SOUNDNESS OF OUR SYSTEM.

Furthermore

ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF
SOUNDNESS AFTER THE INTRODUCTION OF A FUNCTION IN :PROGRAM MODE, EVEN
IF IT IS ULTIMATELY CONVERTED TO :LOGIC MODE (since its execution could
have damaged the system in a way that makes it possible to verify its
termination and guards unsoundly).

Finally,

THE VAST MAJORITY OF ACL2 SYSTEM CODE IS IN :PROGRAM MODE AND SO ALL
BETS ARE OFF FROM BEFORE YOU START!

This hopeless state of current affairs will change, we think.  We think
we have defined our functions "correctly" in the sense that they can be
converted, without "essential" modification, to :logic mode.  We think
it very unlikely that a mis-guarded function in :program mode (whether
ours or yours) will cause unsoundness without some sort of hard lisp
error accompanying it.  We think that ultimately we can make it
possible to execute your functions (interpretively) without risk to the
system, even when some have :program mode.  In that imagined
implementation, code using functions having :program mode would run
more slowly, but safely.  These functions could be introduced into the
logic ex post facto, whereupon the code's execution would speed up
because Common Lisp would be allowed to execute it directly.  We
therefore ask that you simply pretend that this is that imagined
implementation, introduce functions in :program mode, use them as
convenient and perhaps ultimately introduce some of them in :logic mode
and prove their properties.  If you use the system this way we can
develop (or dismiss) this style of formal system development.  BUT BE
ON THE LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE EXECUTION OF
YOUR FUNCTIONS HAVING :PROGRAM MODE!

GENERALIZED-BOOLEANS    potential soundness issues related to ACL2 predicates

The discussion below outlines a potential source of unsoundness in
ACL2.  Although to our knowledge there is no existing Lisp
implementation in which this problem can arise, nevertheless we feel
compelled to explain this situation.

Consider for example the question:  What is the value of (equal 3 3)?
According to the ACL2 axioms, it's t.  And as far as we know, based on
considerable testing, the value is t in every Common Lisp
implementation.  However, according the Common Lisp draft proposed ANSI
standard, any non-nil value could result.  Thus for example, (equal 3
3) is allowed by the standard to be 17.

The Common Lisp standard specifies (or soon will) that a number of
Common Lisp functions that one might expect to return Boolean values
may, in fact, return arbitrary values.  Examples of such functions are
equal, rationalp, and <; a much more complete list is given below.
Indeed, we dare to say that every Common Lisp function that one may
believe returns only Booleans is, nevertheless, not specified by the
standard to have that property, with the exceptions of the functions
not and null.  The standard refers to such arbitrary values as
"generalized Booleans," but in fact this terminology makes no
restriction on those values.  Rather, it merely specifies that they are
to be viewed, in an informal sense, as being either nil or not nil.

This situation is problematic for ACL2, which axiomatizes these
functions to return Booleans.  The problem is that because (for
efficiency and simplicity) ACL2 makes very direct use of compiled
Common Lisp functions to support the execution of its functions, there
is in principle a potential for unsoundness due to these "generalized
Booleans."  For example, ACL2's equal function is defined to be Common
Lisp's equal.  Hence if in Common Lisp the form (equal 3 3) were to
evaluate to 17, then in ACL2 we could prove (using the
:executable-counterpart of equal) (equal (equal 3 3) 17).  However,
ACL2 can also prove (equal (equal x x) t), and these two terms together
are contradictory, since they imply (instantiating x in the second term
by 3) that (equal 3 3) is both equal to 17 and to t.

To make matters worse, the standard allows (equal 3 3) to evaluate to
_different_ non-nil values every time.  That is:  equal need not even
be a function!

Fortunately, no existing Lisp implementation takes advantage of the
flexibility to have (most of) its predicates return generalized
Booleans, as far as we know.  We may implement appropriate safeguards
in future releases of ACL2, in analogy to (indeed, probably extending)
the existing safeguards by way of guards (see GUARD).  For now,
we'll sleep a bit better knowing that we have been up-front about this
potential problem.

The following list of functions contains all those that are defined in
Common Lisp to return generalized Booleans but are assumed by ACL2 to
return Booleans.  In addition, the functions acl2-numberp and
complex-rationalp are directly defined in terms of respective Common
Lisp functions numberp and complexp.

     /=
     <
     =
     alpha-char-p
     atom
     char-equal
     char<
     char<=
     char>
     char>=
     characterp
     consp
     digit-char-p
     endp
     eq
     eql
     equal
     evenp
     integerp
     keywordp
     listp
     logbitp
     logtest
     lower-case-p
     minusp
     oddp
     plusp
     rationalp
     standard-char-p
     string-equal
     string<
     string<=
     string>
     string>=
     stringp
     subsetp
     symbolp
     upper-case-p
     zerop

COMPUTED-HINTS    computing advice to the theorem proving process

     General Form of :hints:
     (hint1 hint2 ... hintk)

Each element, hinti, must be either a common hint or a computed hint.

A common hint is of the form

     (goal-spec :key1 val1 ... :keyn valn)

where goal-spec is as specified in goal-spec and each :keyi and vali is
as specified in hints.  Among the "common hints" we include both the
primitive hints and user-defined custom keyword hints (see
CUSTOM-KEYWORD-HINTS).

A computed hint may be a function symbol, fn, of three, four or seven
arguments.  Otherwise, a computed hint is a term with the following
properties:

(a) the only free variables allowed in the term are ID, CLAUSE, WORLD,
STABLE-UNDER-SIMPLIFICATIONP, HIST, PSPV, CTX, and STATE;

(b) the output signature of the term is either (MV * * STATE), which is
to be treated as an error triple (see below), or is *, denoting a single
non-stobj value; and

(c) in the former case of (b) above, the term is single-threaded in
STATE.

If a computed hint is a function symbol fn, whose arity n is therefore
three, four, or seven, then it is treated as the term resulting from
applying that fn to the first n variables shown in (a) above.  Notice
that it must then return a single non-stobj value, not an error triple,
since state is not one of the first seven variables shown in (a).

Note: Error triples are an ACL2 idiom for implementing "errors."  If a
computation returns (mv erp val state) in a context in which ACL2 is
respecting the error triple convention (see LD-ERROR-TRIPLES and
see LD-ERROR-ACTION), then an error is deemed to have occurred
if erp is non-nil.  The computation is expected to have printed an
appropriate error message to state and further computation is aborted.
On the other hand, if a computation returns an error triple in which
erp is nil, then "value" of the computation is taken to be the second
component, val, of the triple (along with the possibly modified state),
and computation continues.

The function symbol cases are treated as abbreviations of the term (fn
ID CLAUSE WORLD), (fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP), or
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX) as
appropriate for the arity of fn.  (Note that this tells you which
argument of fn is which.)  Moreover, in these cases the value returned
must be a single ordinary (non-stobj) value, not an error triple.  In
the discussion below we assume all computed hints are of the term form.
Indeed, we almost assume all computed hints are of the 3 and 4 argument
forms.  We only comment briefly on the 7 argument form in
using-computed-hints-8.

The semantics of a computed hint term is as follows.  On every subgoal,
the term is evaluated in an environment in which the variables
mentioned in (a) above are bound to context-sensitive values explained
below.  Either the computed hint signals an error, in which the proof
attempt aborts, or else it returns a value, val and a new state, state.
Any changes to those parts of state that affect logical soundness are
undone; more specifically, the values of symbols (sometimes called
"state global variables") in the list *protected-system-state-globals*
in the global table of the state (see STATE) are restored when
changed during evaluation.  The value, val, of a non-erroneous computed
hint calculation is either nil, which means the computed hint did not
apply to the subgoal in question, or it is an alternating list of :keyi
vali pairs as specified in hints.  With one exception, those new hints
are applied to the given subgoal as though the user had typed them
explicitly.

The exception is that the first keyword in the returned val is allowed
to be :COMPUTED-HINT-REPLACEMENT.  Its value should be nil, t, or a
list of terms.  If this keyword is not present, the default value of nil
is provided.  We explain :COMPUTED-HINT-REPLACEMENT below.

The evaluation of a hint term is done with guard checking turned off
(see SET-GUARD-CHECKING); e.g., the form (car 23) in a computed
hint returns nil as per the axioms.

When a non-nil value is returned, the keyword/value pairs (other than
the optional :COMPUTED-HINT-REPLACEMENT) are used as the hint for the
subgoal in question.  Thus, your job as the programmer of computed
hints is either to cause an error, typically by invoking er, or to
return a non-erroneous value triple whose value is the list of keys and
values you would have typed had you supplied a common hint for the
subgoal. (In particular, any theory expressions in it are evaluated
with respect to the global current-theory, not whatever theory is
active at the subgoal in question.)  If the generated list of keywords
and values is illegal, an error will be signaled and the proof attempt
will be aborted.

The purpose of the :COMPUTED-HINT-REPLACEMENT keyword and its value,
chr, is to change the list of hints.  If chr is nil, then the hint
which was applied is removed from the list of hints that is passed down
to the children of the subgoal in question.  This is the default.  If
chr is t, then the hint is left in the list of hints.  This means that
the same hint may act on the children of the subgoal.  Otherwise, chr
must be a list of terms, each of which is treated as a computed hint.
The hint which was applied is deleted from the list of hints and the
hints in chr are added to the list of hints passed to the children of
the subgoal.  The ability to compute new hints and pass them down
allows strange and wonderful behavior.

For these purposes, the goals produced by induction and the top-level
goals of forcing rounds are not considered children; all original hints
are available to them.

Only the first hint applicable to a goal, as specified in the
user-supplied list of :hints followed by the default-hints-table, will
be applied to that goal.  (For an advanced exception, see
OVERRIDE-HINTS.)

It remains only to describe the bindings of the free variables.

Suppose the theorem prover is working on some clause, clause, named by
some goal-spec, e.g., "Subgoal *1/2"'" in some logical world, world.
Corresponding to the printed goal-spec is an internal data structure
called a "clause identifier" id.  See CLAUSE-IDENTIFIER.

In the case of a common hint, the hint applies if the goal-spec of the
hint is the same as the goal-spec of the clause in question.

In the case of a computed hint, the variable ID is bound to the clause
id, the variable CLAUSE is bound to the (translated form of the) clause,
and the variable WORLD is bound to the current ACL2 world.  The variable
STABLE-UNDER-SIMPLIFICATIONP is bound to t or nil.  It is bound to t
only if the clause is known to be stable under simplification.  That
is, the simplifier has been applied to the clause and did not change it.
Such a clause is sometimes known as a "simplification checkpoint."  It
is frequently useful to inject hints (e.g., to enable a rule or provide
a :use hint) only when the goal in question has stabilized.  If a hint
is provided, the processing of the clause starts over with
simplification.

As for CTX and STATE, they are provided so that you can pass them to
the er macro to print error messages.  We recommend not writing
computed hints that otherwise change STATE!

The remaining variables, HIST and PSPV are not documented yet.  Only
users familiar with the internals of ACL2 are likely to need them or
understand their values.

For some instruction about how to use computed hints, see
USING-COMPUTED-HINTS.

CONSTRAINT    restrictions on certain functions introduced in encapsulate events

Suppose that a given theorem, thm, is to be functionally instantiated
using a given functional substitution, alist.  (See
LEMMA-INSTANCE, or for an example, see
FUNCTIONAL-INSTANTIATION-EXAMPLE.)  What is the set of proof
obligations generated?  It is the set obtained by applying alist to all
terms, tm, such that (a) tm mentions some function symbol in the domain
of alist, and (b) either (i) tm arises from the "constraint" on a
function symbol ancestral in thm or in some defaxiom or (ii) tm is the
body of a defaxiom.  Here, a function symbol is "ancestral" in thm if
either it occurs in thm, or it occurs in the definition of some
function symbol that occurs in thm, and so on.

The remainder of this note explains what we mean by "constraint" in the
words above.

In a certain sense, function symbols are introduced in essentially two
ways.  The most common way is to use defun (or when there is mutual
recursion, mutual-recursion or defuns).  There is also a mechanism for
introducing "witness functions"; see DEFCHOOSE.  The
documentation for these events describes the axioms they introduce,
which we will call here their "definitional axioms."  These
definitional axioms are generally the constraints on the function
symbols that these axioms introduce.

However, when a function symbol is introduced in the scope of an
encapsulate event, its constraints may differ from the definitional
axioms introduced for it.  For example, suppose that a function's
definition is local to the encapsulate; that is, suppose the function is
introduced in the signature of the encapsulate.  Then its constraints
include, at the least, those non-local theorems and definitions in the
encapsulate that mention the function symbol.

Actually, it will follow from the discussion below that if the
signature is empty for an encapsulate, then the constraint on each of
its new function symbols is exactly the definitional axiom introduced
for it.  Intuitively, we view such encapsulates just as we view
include-book events.  But the general case, where the signature is not
empty, is more complicated.

In the discussion that follows we describe in detail exactly which
constraints are associated with which function symbols that are
introduced in the scope of an encapsulate event.  In order to simplify
the exposition we make two cuts at it.  In the first cut we present an
over-simplified explanation that nevertheless captures the main ideas.
In the second cut we complete our explanation by explaining how we view
certain events as being "lifted" out of the encapsulate, resulting in a
possibly smaller encapsulate, which becomes the target of the algorithm
described in the first cut.

At the end of this note we present an example showing why a more naive
approach is unsound.

Finally, before we start our "first cut," we note that any information
you want "exported" outside an encapsulate event must be there as an
explicit definition or theorem.  For example, even if a function foo has
output type (mv t t) in its signature, the system will not know
(true-listp (foo x)) merely on account of this information.  Thus, if
you are using functions like foo (constrained mv functions), then you
may find it useful to prove (inside the encapsulate, to be exported) a
:type-prescription rule for the constrained function, for example, the
:type-prescription rule (true-listp (foo x)).

_First cut at constraint-assigning algorithm._  Quite simply, the
formulas introduced in the scope of an encapsulate are conjoined, and
each function symbol introduced by the encapsulate is assigned that
conjunction as its constraint.

Clearly this is a rather severe algorithm.  Let us consider two possible
optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below.  The function before1 does
not refer at all, even indirectly, to the locally-introduced function
sig-fn, so it is unfortunate to saddle it with constraints about sig-fn.

     (encapsulate
      (((sig-fn *) => *))

      (defun before1 (x)
        (if (consp x)
            (before1 (cdr x))
          x))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))
      )

We would like to imagine moving the definition of before1 to just in
front of this encapsulate, as follows.

     (defun before1 (x)
       (if (consp x)
           (before1 (cdr x))
         x))

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))
      )

Thus, we will only assign the constraint (consp (sig-fn x)), from the
theorem sig-fn-prop, to the function sig-fn, not to the function
before1.

More generally, suppose an event in an encapsulate event does not
mention any function symbol in the signature of the encapsulate, nor
any function symbol that mentions any such function symbol, and so on.
(We might say that no function symbol from the signature is an
"ancestor" of any function symbol occurring in the event.)  Then we
imagine moving the event, so that it appears in front of the
encapsulate.  We don't actually move it, but we pretend we do when it
comes time to assign constraints.  Thus, such definitions only
introduce definitional axioms as the constraints on the function
symbols being defined.  In the example above, the event sig-fn-prop
introduces no constraints on function before1.

Once this first optimization is performed, we have in mind a set of
"constrained functions."  These are the functions introduced in the
encapsulate that would remain after moving some of them in front, as
indicated above.  Consider the collection of all formulas introduced by
the encapsulate, except the definitional axioms, that mention these
constrained functions.  So for example, in the event below, no such
formula mentions the function symbol after1.

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))

      (defun after1 (x)
        (sig-fn x))
      )

We can see that there is really no harm in imagining that we move the
definition of after1 out of the encapsulate, to just after the
encapsulate.

Many subtle aspects of this rearrangement process have been omitted.
For example, suppose the function fn uses sig-fn, the latter being a
function in the signature of the encapsulation.  Suppose a formula about
fn is proved in the encapsulation.  Then from the discussion above fn
is among the constrained functions of the encapsulate: it cannot be
moved before the encapsulate and it cannot be moved after the
encapsulation.  But why is fn constrained?  The reason is that the
theorem proved about fn may impose or express constraints on sig-fn.
That is, the theorem proved about fn may depend upon properties of the
witness used for sig-fn.  Here is a simple example:

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (declare (ignore x)) 0))

      (defun fn (lst)
        (if (endp lst)
            t
            (and (integerp (sig-fn (car lst)))
                 (fn (cdr lst)))))

      (defthm fn-always-true
        (fn lst)))

In this example, there are no defthm events that mention sig-fn
explicitly.  One might therefore conclude that it is completely
unconstrained.  But the witness we chose for it always returns an
integer.  The function fn uses sig-fn and we prove that fn always
returns true.  Of course, the proof of this theorem depends upon the
properties of the witness for sig-fn, even though those properties were
not explicitly "called out" in theorems proved about sig-fn.  It would
be unsound to move fn-always-true after the encapsulate.  It would also
be unsound to constrain sig-fn to satisfy just fn-always-true without
including in the constraint the relation between sig-fn and fn.  Hence
both sig-fn and fn are constrained by this encapsulation and the
constraint imposed on each is the same and states the relation between
the two as characterized by the equation defining fn as well as the
property that fn always returns true.  Suppose, later, one proved a
theorem about sig-fn and wished to functionally instantiate it.  Then
one must also functionally instantiate fn, even if it is not involved
in the theorem, because it is only through fn that sig-fn inherits its
constrained properties.

This is a pathological example that illustrate a trap into which one may
easily fall: rather than identify the key properties of the constrained
function the user has foreshadowed its intended application and
constrained those notions.  Clearly, the user wishing to introduce the
sig-fn above would be well-advised to use the following instead:

     (encapsulate
      (((sig-fn *) => *))
      (local (defun sig-fn (x) (declare (ignore x)) 0))
      (defthm integerp-sig-fn
        (integerp (sig-fn x))))

     (defun fn (lst)
       (if (endp lst)
           t
         (and (integerp (sig-fn (car lst)))
              (fn (cdr lst)))))

     (defthm fn-always-true
        (fn lst)))

Note that sig-fn is constrained merely to be an integer.  It is the only
constrained function.  Now fn is introduced after the encapsulation, as
a simple function that uses sig-fn.  We prove that fn always returns
true, but this fact does not constrain sig-fn.  Future uses of sig-fn
do not have to consider fn at all.

Sometimes it is necessary to introduce a function such as fn within the
encapsulate merely to state the key properties of the undefined function
sig-fn.  But that is unusual and the user should understand that both
functions are being constrained.

Another subtle aspect of encapsulation that has been brushed over so
far has to do with exactly how functions defined within the
encapsulation use the signature functions.  For example, above we say
"Consider the collection of all formulas introduced by the encapsulate,
_except the definitional axioms_, that mention these constrained
functions."  We seem to suggest that a definitional axiom which
mentions a constrained function can be moved out of the encapsulation
and considered part of the "post-encapsulation" extension of the
logical world, if the defined function is not used in any
non-definitional formula proved in the encapsulation.  For example, in
the encapsulation above that constrained sig-fn and introduced fn
within the encapsulation, fn was constrained because we proved the
formula fn-always-true within the encapsulation.  Had we not proved
fn-always-true within the encapsulation, fn could have been moved after
the encapsulation.  But this suggests an unsound rule because whether
such a function can be moved after the encapsulate depend on whether
its _admission_ used properties of the witnesses!  In particular, we
say a function is "subversive" if any of its governing tests or the
actuals in any recursive call involve a function in which the signature
functions are ancestral.  See SUBVERSIVE-RECURSIONS.

(Aside: The definition of fn in the first enapsulation above that
defines fn, i.e., the encapsulation with fn-always-true inside, is
subversive because the call of the macro AND expands to a call of IF
that governs a recursive call of fn, in this case:

     (defun fn (lst)
       (if (endp lst)
           t
           (if (integerp (sig-fn (car lst)))
               (fn (cdr lst))
             nil))).

If we switch the order of conjuncts in fn, then the definition of fn is
no longer subversive, but it still "infects" the constraint generated
for the encapsulation, hence for sig-fn, because fn-always-true blocks
the definition of fn from being moved back (to after the
encapsulation).  If we both switch the order of conjuncts and drop
fn-always-true from the encapsulation, then the definition of fn is in
essence moved back to after the encapsulation, and the constraint for
sig-fn no longer includes the definition of fn.  End of aside.)

Another aspect we have not discussed is what happens to nested
encapsulations when each introduces constrained functions.  We say an
encapsulate event is "trivial" if it introduces no constrained
functions, i.e., if its signatures is nil.  Trivial encapsulations are
just a way to wrap up a collection of events into a single event.

From the foregoing discussion we see we are interested in exactly how
we can "rearrange" the events in a non-trivial encapsulation - moving
some "before" the encapsulation and others "after" the encapsulation.
We are also interested in which functions introduced by the
encapsulation are "constrained" and what the "constraints" on each are.
We may summarize the observations above as follows, after which we
conclude with a more elaborate example.

_Second cut at constraint-assigning algorithm._  First, we focus only on
non-trivial encapsulations that neither contain nor are contained in
non-trivial encapsulations.  (Nested non-trivial encapsulations are not
rearranged at all: do not put anything in such a nest unless you mean
for it to become part of the constraints generated.)  Second, in what
follows we only consider the non-local events of such an encapsulate,
assuming that they satisfy the restriction of using no locally defined
function symbols other than the signature functions.  Given such an
encapsulate event, move, to just in front of it and in the same order,
all definitions and theorems for which none of the signature functions
is ancestral.  Now collect up all formulas (theorems) introduced in the
encapsulate other than definitional axioms.  Add to this set any of
those definitional equations that is either subversive or defines a
function used in a formula in the set.  The conjunction of the
resulting set of formulas is called the "constraint" and the set of all
the signature functions of the encapsulate together with all function
symbols defined in the encapsulate and mentioned in the constraint is
called the "constrained functions."  Assign the constraint to each of
the constrained functions.  Move, to just after the encapsulate, the
definitions of all function symbols defined in the encapsulate that
have been omitted from the constraint.

Implementation note.  In the implementation we do not actually move
events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm.  It
builds on the preceding examples.

     (encapsulate
      (((sig-fn *) => *))

      (defun before1 (x)
        (if (consp x)
            (before1 (cdr x))
          x))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))

      (defun during (x)
        (if (consp x)
            x
          (cons (car (sig-fn x))
                17)))

      (defun before2 (x)
        (before1 x))

      (defthm before2-prop
        (atom (before2 x)))

      (defthm during-prop
        (implies (and (atom x)
                      (before2 x))
                 (equal (car (during x))
                        (car (sig-fn x)))))

      (defun after1 (x)
        (sig-fn x))

      (defchoose after2 (x) (u)
        (and (< u x) (during x)))
      )

Only the functions sig-fn and during receive extra constraints.  The
functions before1 and before2 are viewed as moving in front of the
encapsulate, as is the theorem before2-prop.  The functions after1 and
after2 are viewed as being moved past the encapsulate.  The
implementation reports the following.

     In addition to SIG-FN, we export AFTER2, AFTER1, BEFORE2, DURING and
     BEFORE1.

     The following constraint is associated with both of the functions DURING and
     SIG-FN:

     (AND (EQUAL (DURING X)
                 (IF (CONSP X)
                     X (CONS (CAR (SIG-FN X)) 17)))
          (CONSP (SIG-FN X))
          (IMPLIES (AND (ATOM X) (BEFORE2 X))
                   (EQUAL (CAR (DURING X))
                          (CAR (SIG-FN X)))))

Notice that the formula (consp (during x)) is not a conjunct of the
constraint.  During the first pass of the encapsulate, this formula is
stored as a :type-prescription rule deduced during the definition of
the function during.  However, the rule is not exported because of a
rather subtle soundness issue.  (If you are interested in details, see
the comments in source function putprop-type-prescription-lst.)

We conclude by asking (and to a certain extent, answering) the following
question: Isn't there an approach to assigning constraints that avoids
over-constraining more simply than our "second cut" above?  Perhaps it
seems that given an encapsulate, we should simply assign to each
locally defined function the theorems exported about that function.  If
we adopted that simple approach the events below would be admissible.

     (encapsulate
      (((foo *) => *))
      (local (defun foo (x) x))
      (defun bar (x)
        (foo x))
      (defthm bar-prop
        (equal (bar x) x)
        :rule-classes nil))

     (defthm foo-id
       (equal (foo x) x)
       :hints (("Goal" :use bar-prop)))

     ; The following event is not admissible in ACL2.

     (defthm ouch!
       nil
       :rule-classes nil
       :hints
       (("Goal" :use
         ((:functional-instance foo-id
                                (foo (lambda (x) (cons x x))))))))

Under the simple approach we have in mind, bar is constrained to satisfy
both its definition and bar-prop because bar mentions a function
declared in the signature list of the encapsulation.  In fact, bar is
so-constrained in the ACL2 semantics of encapsulation and the first two
events above (the encapsulate and the consequence that foo must be the
identity function) are actually admissible.  But under the simple
approach to assigning constraints, foo is unconstrained because no
theorem about it is exported.  Under that approach, ouch! is provable
because foo can be instantiated in foo-id to a function other than the
identity function.

It's tempting to think we can fix this by including definitions, not
just theorems, in constraints.  But consider the following slightly
more elaborate example.  The problem is that we need to include as a
constraint on foo not only the definition of bar, which mentions foo
explicitly, but also abc, which has foo as an ancestor.

     (encapsulate
      (((foo *) => *))
      (local (defun foo (x) x))
      (local (defthm foo-prop
               (equal (foo x) x)))
      (defun bar (x)
        (foo x))
      (defun abc (x)
        (bar x))
      (defthm abc-prop
        (equal (abc x) x)
        :rule-classes nil))

     (defthm foo-id
       (equal (foo x) x)
       :hints (("Goal" :use abc-prop)))

     ; The following event is not admissible in ACL2.

     (defthm ouch!
       nil
       :rule-classes nil
       :hints
       (("Goal" :use
         ((:functional-instance foo-id
                                (foo (lambda (x) (cons x x)))
                                (bar (lambda (x) (cons x x))))))))

COPYRIGHT    ACL2 copyright, license, sponsorship

ACL2 Version 4.3 - A Computational Logic for Applicative Common Lisp
Copyright (C) 2011  University of Texas at Austin

This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright (C)
1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

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.  See the file LICENSE.  If not, write to the Free
Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann               and J Strother Moore email:
  Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu Department of
Computer Science University of Texas at Austin Austin, TX 78701 U.S.A.

Please also see ACKNOWLEDGMENTS.

COROLLARY    the corollary formula of a rune

This is a low-level system function at the present time.  See
PR and see PR! instead.  Also see RULE-CLASSES for
the use of the symbol :corollary in specifying a rule class.

CURRENT-PACKAGE    the package used for reading and printing

Current-package is an ld special (see LD).  The accessor is
(current-package state) and the updater is (set-current-package val
state), or more conventionally, (in-package val).  The value of
current-package is actually the string that names the package.  (Common
Lisp's "package" objects do not exist in ACL2.)  The current package
must be known to ACL2, i.e., it must be one of the initial packages or
a package defined with defpkg by the user.

When printing symbols, the package prefix is displayed if it is not the
current-package and may be optionally displayed otherwise.  Thus, if
current-package is "ACL2" then the symbol 'ACL2::SYMB may be printed as
SYMB or ACL2::SYMB, while 'MY-PKG::SYMB must be printed as
MY-PKG::SYMB.  But if current-package is "MY-PKG" then the former
symbol must be printed as ACL2::SYMB while the latter may be printed as
SYMB.

In Common Lisp, current-package also affects how objects are read from
character streams.  Roughly speaking, read and print are inverses if
the current-package is fixed, so reading from a stream produced by
printing an object must produce an equal object.

In ACL2, the situation is more complicated because we never read
objects from character streams, we only read them from object "streams"
(channels).  Logically speaking, the objects in such a channel are
fixed regardless of the setting of current-package.  However, our host
file systems do not support the idea of Lisp object files and instead
only support character files.  So when you open an object input channel
to a given (character file) we must somehow convert it to a list of
ACL2 objects.  This is done by a deus ex machina ("a person or thing
that appears or is introduced suddenly and unexpectedly and provides a
contrived solution to an apparently insoluble difficulty," Webster's
Ninth New Collegiate Dictionary).  Roughly speaking, the deus ex
machina determines what sequence of calls to read-object will occur in
the future and what the current-package will be during each of those
calls, and then produces a channel containing the sequence of objects
produced by an analogous sequence of Common Lisp reads with
*current-package* bound appropriately for each.

A simple rule suffices to make sane file io possible:  before you read
an object from an object channel to a file created by printing to a
character channel, make sure the current-package at read-time is the
same as it was at print-time.

CUSTOM-KEYWORD-HINTS    user-defined hints

See ADD-CUSTOM-KEYWORD-HINT for a discussion of how advanced
users can define their own hint keywords.  For examples, see the books
distributed with ACL2 in directory books/hints/, in particular
basic-tests.lisp.

DEFAULT-BACKCHAIN-LIMIT    specifying the backchain limit for a rule

See BACKCHAIN-LIMIT.

The initial value is (nil nil).  To inspect the current value (as
explained elsewhere; see BACKCHAIN-LIMIT):

     (default-backchain-limit wrld :ts) ; for type-set reasoning
     (default-backchain-limit wrld :rewrite) ; for rewriting

DEFAULT-DEFUN-MODE    the default defun-mode of defun'd functions

When a defun is processed and no :mode xarg is supplied, the function
default-defun-mode is used.  To find the default defun-mode of the
current ACL2 world, type (default-defun-mode (w state)).  See
DEFUN-MODE for a discussion of defun-modes.  To change the default
defun-mode of the ACL2 world, type one of the keywords :program or
:logic.

The default ACL2 prompt displays the current default defun-mode by
showing the character p for :program mode, and omitting it for :logic
mode; see DEFAULT-PRINT-PROMPT.  The default defun-mode may be
changed using the keyword commands :program and :logic, which are
equivalent to the commands (program) and (logic).  Each of these names
is documented separately:  see PROGRAM and see LOGIC.
The default defun-mode is stored in the table acl2-defaults-table and
hence may also be changed by a table command.  See TABLE and
also see ACL2-DEFAULTS-TABLE.  Both mode-changing commands are
events.

While events that change the default defun-mode are permitted within an
encapsulate or the text of a book, their effects are local in scope to
the duration of the encapsulation or inclusion.  For example, if the
default defun-mode is :logic and a book is included that contains the
event (program), then subsequent events within the book are processed
with the default defun-mode :program; but when the include-book event
completes, the default defun-mode will still be :logic.  Commands that
change the default defun-mode are not permitted inside local forms.

DEFAULT-HINTS    a list of hints added to every proof attempt

     Examples:
     ACL2 !>(default-hints (w state))
     ((computed-hint-1 clause)
      (computed-hint-2 clause stable-under-simplificationp))

The value returned by this function is added to the right of the :hints
argument of every defthm and thm command, and to hints provided to
defuns as well (:hints, :guard-hints, and (for ACL2(r)) :std-hints).

See SET-DEFAULT-HINTS for a more general discussion.  Advanced
users only: see OVERRIDE-HINTS for an advanced variant of
default hints that are not superseded by :hints arguments.

DEFAULT-PRINT-PROMPT    the default prompt printed by ld

     Example prompt:
     ACL2 p!s>

The prompt printed by ACL2 displays the current package, followed by a
space, followed by zero or more of the three characters as specified
below, followed by the character > printed one or more times,
reflecting the number of recursive calls of ld.  The three characters
in the middle are as follows:

     p     ; when (default-defun-mode (w state)) is :program
     !     ; when guard checking is on
     s     ; when (ld-skip-proofsp state) is t

See DEFAULT-DEFUN-MODE, see SET-GUARD-CHECKING, and see
LD-SKIP-PROOFSP.

Also see LD-PROMPT to see how to install your own prompt.

Here are some examples with ld-skip-proofsp nil.

     ACL2 !>    ; logic mode with guard checking on
     ACL2 >     ; logic mode with guard checking off
     ACL2 p!>   ; program mode with guard checking on
     ACL2 p>    ; program mode with guard checking off

Here are some examples with default-defun-mode of :logic.

     ACL2 >     ; guard checking off, ld-skip-proofsp nil
     ACL2 s>    ; guard checking off, ld-skip-proofsp t
     ACL2 !>    ; guard checking on, ld-skip-proofsp nil
     ACL2 !s>   ; guard checking on, ld-skip-proofsp t

Finally, here is the prompt in raw mode (see SET-RAW-MODE),
regardless of the settings above:

     ACL2 P>

DEFAULT-RULER-EXTENDERS    the default ruler-extenders for defun'd functions

When a defun is processed and no :ruler-extenders xarg is supplied, the
function default-ruler-extenders is used to obtain the current
ruler-extenders; see RULER-EXTENDERS.  To find the default
ruler-extenders of the current ACL2 world, type
(default-ruler-extenders (w state)).

While events that change the default ruler-extenders are permitted
within an encapsulate or the text of a book, their effects are local in
scope to the duration of the encapsulation or inclusion.  See
DEFAULT-DEFUN-MODE for an analogous discussion for defun-modes.

DEFUN-MODE    determines whether a function definition is a logical act

Two "defun-modes" are supported, :program and :logic.  Roughly
speaking, :program mode allows you to prototype a function for
execution without any proof burdens, while :logic mode allows you to
add a new definitional axiom to the logic.  The system comes up in
:logic mode.  Execution of functions whose defun-mode is :program may
render ACL2 unsound!  See DEFUN-MODE-CAVEAT.

Note that calls of local and of many events are skipped in :program
mode; see PROGRAM.

When you define a function in the ACL2 logic, that function can be run
on concrete data.  But it is also possible to reason deductively about
the function because each definition extends the underlying logic with
a definitional axiom.  To ensure that the logic is sound after the
addition of this axiom, certain restrictions have to be met, namely
that the recursion terminates.  This can be quite challenging.

Because ACL2 is a programming language, you often may wish simply to
program in ACL2.  For example, you may wish to define your system and
test it, without any logical burden.  Or, you may wish to define
"utility" functions -- functions that are executed to help manage the
task of building your system but functions whose logical properties are
of no immediate concern.  Such functions might be used to generate test
data or help interpret the results of tests.  They might create files
or explore the ACL2 data base.  The termination arguments for such
functions are an unnecessary burden provided no axioms about the
functions are ever used in deductions.

Thus, ACL2 introduces the idea of the "defun-mode" of a function.  The
:mode keyword of defun's declare xarg allows you to specify the
defun-mode of a given definition.  If no :mode keyword is supplied, the
default defun-mode is used; see DEFAULT-DEFUN-MODE.

There are two defun-modes, each of which is written as a keyword:

:program -- logically undefined but executable outside deductive
contexts.

:logic -- axiomatically defined as per the ACL2 definitional principle.

It is possible to change the defun-mode of a function from :program to
:logic.  We discuss this below.

We think of functions having :program mode as "dangerous" functions,
while functions having :logic mode are "safe."  The only requirement
enforced on :program mode functions is the syntactic one:  each
definition must be well-formed ACL2.  Naively speaking, if a :program
mode function fails to terminate then no harm is done because no axiom
is added (so inconsistency is avoided) and some invocations of the
function may simply never return.  This simplistic justification of
:program mode execution is faulty because it ignores the damage that
might be caused by "mis-guarded" functions.  See
DEFUN-MODE-CAVEAT.

We therefore implicitly describe an imagined implementation of
defun-modes that is safe and, we think, effective.  But please see
DEFUN-MODE-CAVEAT.

The default defun-mode is :logic.  This means that when you defun a
function the system will try to prove termination.  If you wish to
introduce a function of a different defun-mode use the :mode xargs
keyword.  Below we show fact introduced as a function in :program mode.

     (defun fact (n)
       (declare (xargs :mode :program))
       (if (or (not (integerp n)) (= n 0))
           1
         (* n (fact (1- n)))))

No axiom is added to the logic as a result of this definition.  By
introducing fact in :program mode we avoid the burden of a termination
proof, while still having the option of executing the function.  For
example, you can type

     ACL2 !>(fact 3)

and get the answer 6.  If you type (fact -1) you will get a hard lisp
error due to "infinite recursion."

However, the ACL2 theorem prover knows no axioms about fact.  In
particular, if the term (fact 3) arises in a proof, the theorem prover
is unable to deduce that it is 6.  From the perspective of the theorem
prover it is as though fact were an undefined function symbol of arity
1.  Thus, modulo certain important issues (see
DEFUN-MODE-CAVEAT), the introduction of this function in :program
mode does not imperil the soundness of the system -- despite the fact
that the termination argument for fact was omitted -- because nothing
of interest can be proved about fact.  Indeed, we do not allow fact to
be used in logical contexts such as conjectures submitted for proof.

It is possible to convert a function from :program mode to :logic mode
at the cost of proving that it is admissible.  This can be done by
invoking

     (verify-termination fact)

which is equivalent to submitting the defun of fact, again, but in
:logic mode.

     (defun fact (n)
       (declare (xargs :mode :logic))
       (if (or (not (integerp n)) (= n 0))
           1
         (* n (fact (1- n)))))

This particular event will fail because the termination argument
requires that n be nonnegative.  A repaired defun, for example with =
replaced by <=, will succeed, and an axiom about fact will henceforth
be available.

Technically, verify-termination submits a redefinition of the :program
mode function.  This is permitted, even when ld-redefinition-action is
nil, because the new definition is identical to the old (except for its
:mode and, possibly, other non-logical properties).

See GUARD for a discussion of how to restrict the execution of
functions.  Guards may be "verified" for functions in :logic mode; see
VERIFY-GUARDS.

DEFUNS    an alternative to mutual-recursion

     Example:
     (DEFUNS
      (evenlp (x)
        (if (consp x) (oddlp (cdr x)) t))
      (oddlp (x)
        (if (consp x) (evenlp (cdr x)) nil)))

     General Form:
     (DEFUNS defuns-tuple1 ... defuns-tuplen)

is equivalent to

     (MUTUAL-RECURSION
       (DEFUN . defuns-tuple1)
       ...
       (DEFUN . defuns-tuplen))

In fact, defuns is the more primitive of the two and mutual-recursion
is just a macro that expands to a call of defun after stripping off the
defun at the car of each argument to mutual-recursion.  We provide and
use mutual-recursion rather than defuns because by leaving the defuns
in place, mutual-recursion forms can be processed by the Emacs tags
program.  See MUTUAL-RECURSION.

DISABLE-FORCING    to disallow forced case-splits

     General Form:
     ACL2 !>:disable-forcing   ; disallow forced case splits

See FORCE and see CASE-SPLIT for a discussion of forced
case splits, which are inhibited by this command.

Disable-forcing is actually a macro that disables the executable
counterpart of the function symbol force; see FORCE.  When you
want to use hints to turn off forced case splits, use a form such as:

     :in-theory (disable (:executable-counterpart force))

DISABLE-IMMEDIATE-FORCE-MODEP    forced hypotheses are not attacked immediately

     General Form:
     ACL2 !>:disable-immediate-force-modep

This event causes ACL2 to delay forced hypotheses to the next forcing
round, rather than attacking them immediately.  See
IMMEDIATE-FORCE-MODEP.  Or for more basic information, first see
FORCE for a discussion of forced case splits.

Disable-immediate-force-modep is a macro that disables the executable
counterpart of the function symbol immediate-force-modep.  When you
want to disable this mode in hints, use a form such as:

     :in-theory (disable (:executable-counterpart immediate-force-modep))

DISABLEDP    determine whether a given name or rune is disabled

     Examples:

     :disabledp foo   ; returns a list of all disabled runes whose base
                      ; symbol is foo (see RUNE)
     (disabledp 'foo) ; same as above (i.e., :disabledp foo)
     :disabledp (:rewrite bar . 1) ; returns t if the indicated rune is
                                   ; disabled, else nil
     (disabledp (:rewrite bar . 1)); same as immediately above

Also see PR, which gives much more information about the rules
associated with a given event.

Disabledp takes one argument, an event name (see EVENTS) other
than nil or a rune.  In the former case it returns the list of disabled
runes associated with that name, in the sense that the rune's "base
symbol" is that name (see RUNE) or, if the event named is a
defmacro event, then the list of disabled runes associated with the
function corresponding to that macro name, if any (see
MACRO-ALIASES-TABLE).  In the latter case, where the argument is a
rune, disabledp returns t if the rune is disabled, and nil otherwise.

DO-NOT    hints keyword :DO-NOT

See HINTS.

DO-NOT-INDUCT    hints keyword :DO-NOT-INDUCT

See HINTS.

DOUBLE-REWRITE    cause a term to be rewritten twice

Logically, double-rewrite is the identity function: (double-rewrite x)
is equal to x.  However, the ACL2 rewriter treats calls of
double-rewrite in the following special manner.  When it encounters a
term (double-rewrite u), it first rewrites u in the current context,
and then the rewriter rewrites the result.

Such double-rewriting is rarely necessary, but it can be useful when
rewriting under non-trivial equivalence relations (see
EQUIVALENCE).  The following example will illustrate the issue.

     ; Define an equivalence relation.
     (defun my-equiv (x y)
       (equal x y))
     (defequiv my-equiv)

     ; Define a unary function whose argument is preserved by my-equiv.
     (defun foo (x)
       (declare (ignore x))
       t)
     (defcong my-equiv equal (foo x) 1)

     ; Define some other unary functions.
     (defun g (x) x)
     (defun h1 (x) x)
     (defun h2 (x) x)

     ; Prove some lemmas and then disable the functions above.
     (defthm lemma-1
       (my-equiv (h1 x) (h2 x)))
     (defthm lemma-2
       (foo (h2 x)))
     (defthm lemma-3
       (implies (foo x)
                (equal (g x) x)))
     (in-theory (union-theories (theory 'minimal-theory)
                                '(lemma-1 lemma-2 lemma-3
                                  my-equiv-implies-equal-foo-1)))

     ; Attempt to prove a simple theorem that follows ``obviously'' from the
     ; events above.
     (thm (equal (g (h1 a)) (h1 a)))

We might expect the proof of this final thm to succeed by the following
reasoning.  It is immediate from lemma-3 provided we can establish (foo
(h1 a)).  By the defcong event above, we know that (foo (h1 a)) equals
(foo (h2 a)) provided (my-equiv (h1 a) (h2 a)); but this is immediate
from lemma-1.  And finally, (foo (h2 a)) is true by lemma-2.

Unfortunately, the proof fails.  But fortunately, ACL2 gives the
following useful warning when lemma-3 is submitted:

     ACL2 Warning [Double-rewrite] in ( DEFTHM LEMMA-3 ...):  In the :REWRITE
     rule generated from LEMMA-3, equivalence relation MY-EQUIV is maintained
     at one problematic occurrence of variable X in hypothesis (FOO X),
     but not at any binding occurrence of X.  Consider replacing that occurrence
     of X in this hypothesis with (DOUBLE-REWRITE X).  See :doc double-
     rewrite for more information on this issue.

We can follow the warning's advice by changing lemma-3 to the following.

     (defthm lemma-3
       (implies (foo (double-rewrite x))
                (equal (g x) x)))

With this change, the proof succeeds for the final thm above.

In practice, it should suffice for users to follow the advice given in
the "Double-rewrite" warnings, by adding calls of double-rewrite around
certain variable occurrences.  But this can cause inefficiency in large
proof efforts.  For that reason, and for completeness, it seems prudent
to explain more carefully what is going on; and that is what we do for
the remainder of this documentation topic.  Optionally, also see the
paper "Double Rewriting for Equivalential Reasoning in ACL2" by Matt
Kaufmann and J Strother Moore, in the proceedings of the 2006 ACL2
Workshop (paper is published in ACM Digital Library,
`http://portal.acm.org/toc.cfm?id=1217975').

*Suggesting congruence rules.*

Sometimes the best way to respond to a "Double-rewrite" warning may be
to prove a congruence rule.  Consider for example this rule.

     (defthm insert-sort-is-id
       (perm (insert-sort x) x))

Assuming that perm has been identified as an equivalence relation (see
DEFEQUIV), we will get the following warning.

     ACL2 Warning [Double-rewrite] in ( DEFTHM INSERT-SORT-IS-ID ...):
     In a :REWRITE rule generated from INSERT-SORT-IS-ID, equivalence relation
     PERM is maintained at one problematic occurrence of variable X in the
     right-hand side, but not at any binding occurrence of X.  Consider
     replacing that occurrence of X in the right-hand side with
     (DOUBLE-REWRITE X).  See :doc double-rewrite for more information on
     this issue.

The problem is that the second occurrence of x (the right-hand side of
the rule insert-sort-is-id) is in a context where perm is to be
maintained, yet in this example, the argument x of insert-sort on the
left-hand side of that rule is in a context where perm will not be
maintained.  This can lead one to consider the possibility that perm
could be maintained in that left-hand side occurrence of x, and if so,
to prove the following congruence rule.

     (defcong perm perm (insert-sort x) 1)

This will eliminate the above warning for insert-sort-is-id.  More
important, this defcong event would probably be useful, since it would
allow rewrite rules with equivalence relation perm to operate on the
first argument of any call of insert-sort whose context calls for
maintaining perm.

*Details on double-rewrite.*

The reader who wants these details may first wish to see
EQUIVALENCE for relevant review.

The ACL2 rewriter takes a number of contextual arguments, including the
generated equivalence relation being maintained (see
CONGRUENCE) and an association list that maps variables to terms.  We
call the latter alist the unify-subst because it is produced by unifying
(actually matching) a pattern against a current term; let us explain
this point by returning to the example above.  Consider what happens
when the rewriter is given the top-level goal of the thm above.

     (equal (g (h1 a)) (h1 a))

This rewrite is performed with the empty alist (unify-subst), and is
begun by rewriting the first argument (in that same empty unify-subst):

     (g (h1 a))

Note that the only equivalence relation being maintained at this point
is equal.  Now, the rewriter notices that the left-hand side of lemma-3,
which is (g x), matches (g (h1 a)).  The rewriter thus creates a
unify-subst binding x to (h1 a): ((x . (h1 a))).  It now attempts to
rewrite the hypothesis of lemma-3 to t under this unify-subst.

Consider what happens now if the hypothesis of lemma-3 is (foo x).  To
rewrite this hypothesis under a unify-subst of ((x . (h1 a))), it will
first rewrite x under this unify-subst.  The key observation here is
that this rewrite takes place simply by returning the value of x in the
unify-subst, namely (h1 a).  No further rewriting is done!  The
efficiency of the ACL2 rewriter depends on such caching of previous
rewriting results.

But suppose that, instead, the hypothesis of lemma-3 is (foo
(double-rewrite x)).  As before, the rewriter dives to the first
argument of this call of foo.  But this time the rewriter sees the call
(double-rewrite x), which it handles as follows.  First, x is rewritten
as before, yielding (h1 a).  But now, because of the call of
double-rewrite, the rewriter takes (h1 a) and rewrites it under the
empty unify-subst.  What's more, because of the defcong event above,
this rewrite takes place in a context where it suffices to maintain the
equivalence relation my-equiv.  This allows for the application of
lemma-1, hence (h1 a) is rewritten (under unify-subst = nil) to (h2 a).
Popping back up, the rewriter will now rewrite the call of foo to t
using lemma-2.

The example above explains how the rewriter treats calls of
double-rewrite, but it may leave the unfortunate impression that the
user needs to consider each :rewrite or :linear rule carefully, just in
case a call of double-rewrite may be appropriate.  Fortunately, ACL2
provides a "[Double-rewrite]" warning to inform the user of just this
sort of situation.  If you don't see this warning when you submit a
(:rewrite or :linear) rule, then the issue described here shouldn't
come up for that rule.  Such warnings may appear for hypotheses or
right-hand side of a :rewrite rule, and for hypotheses or full
conclusion (as opposed to just the trigger term) of a :linear rule.

If you do see a "[Double-rewrite]" warning, then should you add the
indicated call(s) of double-rewrite?  At the time of writing this
documentation, the answer is not clear.  Early experiments with double
rewriting suggested that it may be too expensive to call double-rewrite
in every instance where a warning indicates that there could be an
advantage to doing so.  And at the time of this writing, the ACL2
regression suite has about 1900 such warnings (but note that books were
developed before double-rewrite or the "[Double-rewrite]" warning were
implemented), which suggests that one can often do fine just ignoring
such warnings.  However, it seems advisable to go ahead and add the
calls of double-rewrite indicated by the warnings unless you run across
efficiency problems caused by doing so.  Of course, if you decide to
ignore all such warnings you can execute the event:
(set-inhibit-warnings "Double-rewrite").

Finally, we note that it is generally not necessary to call
double-rewrite in order to get its effect in the following case, where
the discussion above might have led one to consider a call of
double-rewrite: a hypothesis is a variable, or more generally, we are
considering a variable occurrence that is a branch of the top-level IF
structure of a hypothesis.  The automatic handling of this case, by a
form of double rewriting, was instituted in ACL2 Version_2.9 and
remains in place with the introduction of double-rewrite.  Here is a
simple illustrative example.  Notice that foo-holds applies to prove
the final thm below, even without a call of double-rewrite in the
hypothesis of foo-holds, and that there is no "[Double-rewrite]"
warning when submitting foo-holds.

     (encapsulate
      (((foo *) => *)
       ((bar *) => *))

      (local (defun foo (x) (declare (ignore x)) t))
      (local (defun bar (x) (declare (ignore x)) t))

      (defthm foo-holds
        (implies x
                 (equal (foo x) t)))
      (defthm bar-holds-propositionally
        (iff (bar x) t)))

     (thm (foo (bar y)))

EMBEDDED-EVENT-FORM    forms that may be embedded in other events

     Examples:
     (defun hd (x) (if (consp x) (car x) 0))
     (local (defthm lemma23 ...))
     (progn (defun fn1 ...)
            (local (defun fn2 ...))
            ...)

     General Form:
     An embedded event form is a term, x, such that:

     x is a call of an event function other than DEFPKG (see
     EVENTS for   a listing of the event functions);

     x is of the form (LOCAL x1) where x1 is an embedded   event form;

     x is of the form (SKIP-PROOFS x1) where x1 is an   embedded event
     form;

     x is of the form (MAKE-EVENT &), where & is any term   whose
     expansion is an embedded event (see MAKE-EVENT);

     x is of the form (WITH-OUTPUT ... x1),   (WITH-PROVER-STEP-LIMIT
     ... x1 ...), or   (WITH-PROVER-TIME-LIMIT ... x1), where x1 is an
     embedded   event form;

     x is a call of ENCAPSULATE, PROGN, PROGN!, or   INCLUDE-BOOK;

     x macroexpands to one of the forms above; or

     [intended only for the implementation] x is   (RECORD-EXPANSION x1
     x2), where x1 and x2 are embedded event   forms.

An exception: an embedded event form may not set the
acl2-defaults-table when in the context of local.  Thus for example,
the form

     (local (table acl2-defaults-table :defun-mode :program))

is not an embedded event form, nor is the form (local (program)), since
the latter sets the acl2-defaults-table implicitly.  An example at the
end of the discussion below illustrates why there is this restriction.

Only embedded event forms are allowed in a book after its initial
in-package form.  See BOOKS.  However, you may find that
make-event allows you to get the effect you want for a form that is not
an embedded event form.  For example, you can put the following into a
book, which assigns the value 17 to state global variable x:

     (make-event (er-progn (assign x 17)
                           (value '(value-triple nil)))
                 :check-expansion t)

When an embedded event is executed while ld-skip-proofsp is
'include-book, those parts of it inside local forms are ignored.  Thus,

        (progn (defun f1 () 1)
               (local (defun f2 () 2))
               (defun f3 () 3))

will define f1, f2, and f3 when ld-skip-proofsp is nil but will define
only f1 and f3 when ld-skip-proofsp is 'include-book.

_Discussion:_

Encapsulate, progn, and include-book place restrictions on the kinds of
forms that may be processed.  These restrictions ensure that the
non-local events are indeed admissible provided that the sequence of
local and non-local events is admissible when proofs are done, i.e.,
when ld-skip-proofs is nil.  But progn! places no such restrictions,
hence is potentially dangerous and should be avoided unless you
understand the ramifications; so it is illegal unless there is an active
trust tag (see DEFTTAG).

Local permits the hiding of an event or group of events in the sense
that local events are processed when we are trying to establish the
admissibility of a sequence of events embedded in encapsulate forms or
in books, but are ignored when we are constructing the world produced
by assuming that sequence.  Thus, for example, a particularly ugly and
inefficient :rewrite rule might be made local to an encapsulate that
"exports" a desirable theorem whose proof requires the ugly lemma.

To see why we can't allow just anything in as an embedded event,
consider allowing the form

     (if (ld-skip-proofsp state)
         (defun foo () 2)
         (defun foo () 1))

followed by

     (defthm foo-is-1 (equal (foo) 1)).

When we process the events with ld-skip-proofsp, nil the second defun
is executed and the defthm succeeds.  But when we process the events
with ld-skip-proofsp 'include-book, the second defun is executed, so
that foo no longer has the same definition it did when we proved
foo-is-1.  Thus, an invalid formula is assumed when we process the
defthm while skipping proofs.  Thus, the first form above is not a
legal embedded event form.

If you encounter a situation where these restrictions seem to prevent
you from doing what you want to do, then you may find make-event to be
helpful.  See MAKE-EVENT.

Defpkg is not allowed because it affects how things are read after it
is executed.  But all the forms embedded in an event are read before
any are executed.  That is,

     (encapsulate nil
                  (defpkg "MY-PKG" nil)
                  (defun foo () 'my-pkg::bar))

makes no sense since my-pkg::bar must have been read before the defpkg
for "MY-PKG" was executed.

Finally, let us elaborate on the restriction mentioned earlier related
to the acl2-defaults-table.  Consider the following form.

     (encapsulate
      ()
      (local (program))
      (defun foo (x)
        (if (equal 0 x)
            0
          (1+ (foo (- x))))))

See LOCAL-INCOMPATIBILITY for a discussion of how encapsulate
processes event forms.  Briefly, on the first pass through the events
the definition of foo will be accepted in defun mode :program, and
hence accepted.  But on the second pass the form (local (program)) is
skipped because it is marked as local, and hence foo is accepted in
defun mode :logic.  Yet, no proof has been performed in order to admit
foo, and in fact, it is not hard to prove a contradiction from this
definition!

ENABLE-FORCING    to allow forced splits

     General Form:
     ACL2 !>:enable-forcing    ; allowed forced case splits

See FORCE and see CASE-SPLIT for a discussion of forced
case splits, which are turned back on by this command.  (See
DISABLE-FORCING for how to turn them off.)

Enable-forcing is actually a macro that enables the executable
counterpart of the function symbol force; see FORCE.  When you
want to use hints to turn on forced case splits, use a form such as:

     :in-theory (enable (:executable-counterpart force))

ENABLE-IMMEDIATE-FORCE-MODEP    forced hypotheses are attacked immediately

     General Form:
     ACL2 !>:enable-immediate-force-modep

This event causes ACL2 to attack forced hypotheses immediately instead
of delaying them to the next forcing round.  See
IMMEDIATE-FORCE-MODEP.  Or for more basic information, first see
FORCE for a discussion of forced case splits.

Enable-immediate-force-modep is a macro that enables the executable
counterpart of the function symbol immediate-force-modep.  When you
want to enable this mode in hints, use a form such as:

     :in-theory (enable (:executable-counterpart immediate-force-modep))

ENTER-BOOT-STRAP-MODE    The first millisecond of the Big Bang

ACL2 functions, e.g., if, that show enter-boot-strap-mode as their
defining command are in fact primitives.  It is impossible for the
system to display defining axioms about these symbols.

Enter-boot-strap-mode is a Common Lisp function but not an ACL2
function.  It magically creates from nil an ACL2 property list world
that lets us start the boot-strapping process.  That is, once
enter-boot-strap-mode has created its world, it is possible to process
the defconsts, defuns, and defaxioms, necessary to bring up the rest of
the system.  Before that world is created, the attempt by ACL2 even to
translate a defun form, say, would produce an error because defun is
undefined.

Several ACL2 functions show enter-boot-strap-mode as their defining
command.  Among them are if, cons, car, and cdr.  These functions are
characterized by axioms rather than definitional equations -- axioms
that in most cases are built into our code and hence do not have any
explicit representation among the rules and formulas in the system.

ESCAPE-TO-COMMON-LISP    escaping to Common Lisp

     Example:
     ACL2 !>:Q

There is no Common Lisp escape feature in the lp.  This is part of the
price of purity.  To execute a form in Common Lisp as opposed to ACL2,
exit lp with :q, submit the desired forms to the Common Lisp
read-eval-print loop, and reenter ACL2 with (lp).

EXECUTABLE-COUNTERPART    a rule for computing the value of a function

     Examples:
     (:executable-counterpart length)

which may be abbreviated in theories as

     (length)

Every defun introduces at least two rules used by the theorem prover.
Suppose fn is the name of a defun'd function.  Then (:definition fn) is
the rune (see RUNE) naming the rule that allows the simplifier
to replace calls of fn by its instantiated body.
(:executable-counterpart fn) is the rune for the rule for how to
evaluate the function on known constants.

When typing theories it is convenient to know that (fn) is a runic
designator that denotes (:executable-counterpart fn).  See
THEORIES.

If (:executable-counterpart fn) is enabled, then when applications of
fn to known constants are seen by the simplifier they are computed out
by executing the Common Lisp code for fn (with the appropriate handling
of guards).  Suppose fact is defined as the factorial function.  If the
executable counterpart rune of fact, (:executable-counterpart fact), is
enabled when the simplifier encounters (fact 12), then that term will
be "immediately" expanded to 479001600.  Note that even if subroutines
of fn have disabled executable counterparts, fn will call their Lisp
code nonetheless:  once an executable counterpart function is applied,
no subsidiary enable checks are made.

Such one-step expansions are sometimes counterproductive because they
prevent the anticipated application of certain lemmas about the
subroutines of the expanded function.  Such computed expansions can be
prevented by disabling the executable counterpart rune of the relevant
function.  For example, if (:executable-counterpart fact) is disabled,
(fact 12) will not be expanded by computation.  In this situation,
(fact 12) may be rewritten to (* 12 (fact 11)), using the rule named
(:definition fact), provided the system's heuristics permit the
introduction of the term (fact 11).  Note that lemmas about
multiplication may then be applicable (while such lemmas would be
inapplicable to 479001600).  In many proofs it is desirable to disable
the executable counterpart runes of certain functions to prevent their
expansion by computation.  See EXECUTABLE-COUNTERPART-THEORY.

Finally:  What do we do about functions that are "constrained" rather
than defined, such as the following?  (See ENCAPSULATE.)

     (encapsulate (((foo *) => *))
                  (local (defun foo (x) x)))

Does foo have an executable counterpart?  Yes:  since the vast majority
of functions have sensible executable counterparts, it was decided that
*all* functions, even such "constrained" ones, have executable
counterparts.  We essentially "trap" when such calls are inappropriate.
Thus, consider for example:

     (defun bar (x)
       (if (rationalp x)
           (+ x 1)
         (foo x)))

If the term (bar '3) is encountered by the ACL2 rewriter during a
proof, and if the :executable-counterpart of bar is enabled, then it
will be invoked to reduce this term to '4.  However, if the term (bar
'a) is encountered during a proof, then since 'a is not a rationalp and
since the :executable-counterpart of foo is only a "trap," then this
call of the :executable-counterpart of bar will result in a "trap." In
that case, the rewriter will return the term (hide (bar 'a)) so that it
never has to go through this process again.  See HIDE.

EXIT-BOOT-STRAP-MODE    the end of pre-history

Exit-boot-strap-mode is the last step in creating the ACL2 world in
which the user lives.  It has command number 0.  Commands before it are
part of the system initialization and extend all the way back to :min.
Commands after it are those of the user.

Exit-boot-strap-mode is a Common Lisp function but not an ACL2
function.  It is called when every defconst, defun, etc., in our source
code has been processed under ACL2 and the world is all but complete.
exit-boot-strap-mode has only one job: to signal the completion of the
boot-strapping.

EXPAND    hints keyword :EXPAND

See HINTS.

EXTENDED-METAFUNCTIONS    state and context sensitive metafunctions

     General Form of an Extended :Meta theorem:
     (implies (and (pseudo-termp x)              ; this hyp is optional
                   (alistp a)                    ; this hyp is optional
                   (ev (hyp-fn x mfc state) a))  ; this hyp is optional
              (equiv (ev x a)
                     (ev (fn x mfc state) a)))

where the restrictions are as described in the documentation for meta
and, in addition, mfc and state are distinct variable symbols
(different also from x and a) and state is literally the symbol STATE.
A :meta theorem of the above form installs fn as a metatheoretic
simplifier with hypothesis function hyp-fn, exactly as for vanilla
metafunctions.  The only difference is that when the metafunctions are
applied, some contextual information is passed in via the mfc argument
and the ACL2 state is made available.

See META for a discussion of vanilla flavored metafunctions.
This documentation assumes you are familiar with the simpler situation,
in particular, how to define a vanilla flavored metafunction, fn, and
its associated hypothesis metafunction, hyp-fn, and how to state and
prove metatheorems installing such functions.  Defining extended
metafunctions requires that you also be familiar with many ACL2
implementation details.  This documentation is sketchy on these
details; see the ACL2 source code or email the acl2-help list if you
need more help.

The metafunction context, mfc, is a list containing many different data
structures used by various internal ACL2 functions.  We do not document
the form of mfc.  Your extended metafunction should just take mfc as its
second formal and pass it into the functions mentioned below.  The ACL2
state is well-documented (see STATE).  The following
expressions may be useful in defining extended metafunctions.

(mfc-clause mfc): returns the current goal, in clausal form.  A clause
is a list of ACL2 terms, implicitly denoting the disjunction of the
listed terms.  The clause returned by mfc-clause is the clausal form of
the translation (see TRANS) of the goal or subgoal on which the
rewriter is working.  When a metafunction calls mfc-clause, the term
being rewritten by the metafunction either occurs somewhere in this
clause or, perhaps more commonly, is being rewritten on behalf of some
lemma to which the rewriter has backchained while trying to rewrite a
term in the clause.

(mfc-ancestors mfc): returns an alist whose keys are the negations of
the backchaining hypotheses being pursued.  In particular, (null
(mfc-ancestors mfc)) will be true exactly when rewriting is on part of
the current goal.  Exception: An element of this alist whose key is of
the form (:binding-hyp hyp unify-subst) indicates that hyp has been
encountered as a hypothesis of the form (equal var term) or (equiv var
(double-rewrite-term)), in each case binding variable var to the result
of rewriting term under unify-subst.

(mfc-rdepth mfc): returns the remaining stack depth for calls of the
rewriter (by default, *default-rewrite-stack-limit* at the top level;
see REWRITE-STACK-LIMIT).  When this is 0, no further calls of
the rewriter can be made without error.

(mfc-type-alist mfc): returns the type-alist governing the occurrence of
the term, x, being rewritten by the metafunction.  A type-alist is an
association list, each element of which is of the form (term ts .
ttree).  Such an element means that the term term has the type-set ts.
The ttree component is probably irrelevant here.  All the terms in the
type-alist are in translated form (see TRANS).  The ts are
numbers denoting finite Boolean combinations of ACL2's primitive types
(see TYPE-SET).  The type-alist includes not only information
gleaned from the conditions governing the term being rewritten but also
that gleaned from forward chaining from the (negations of the) other
literals in the clause returned by mfc-clause.

(w state): returns the ACL2 logical world.

(mfc-ts term mfc state): returns the type-set of term in the current
context; see TYPE-SET.

(mfc-rw term obj equiv-info mfc state): returns the result of rewriting
term in the current context, mfc, with objective obj and the
equivalence relation described by equiv-info.  Obj should be t, nil, or
?, and describes your objective: try to show that term is true, false,
or anything.  Equiv-info is either nil, t, a function symbol fn naming
a known equivalence relation, or a list of congruence rules.  Nil means
return a term that is equal to term.  T means return a term that is
propositionally equivalent (i.e., in the iff sense) to term, while fn
means return a term fn-equivalent to term.  The final case, which is
intended only for advanced users, allows the specification of generated
equivalence relations, as supplied to the geneqv argument of rewrite.
Generally, if you wish to establish that term is true in the current
context, use the idiom

     (equal (mfc-rw term t t mfc state) *t*)

The constant *t* is set to the internal form of the constant term t,
i.e., 't.

(mfc-rw+ term alist obj equiv-info mfc state): if alist is nil then
this is equivalent to (mfc-rw term obj equiv-info mfc state).  However,
the former takes an argument, alist, that binds variables to terms, and
returns the result of rewriting term under that alist, where this
rewriting is as described for mfc-rw above.  The function mfc-rw+ can
be more efficient than mfc-rw|, because the terms in the binding alist
have generally already been rewritten, and it can be inefficient to
rewrite them again.  For example, consider a rewrite rule of the
following form.

     (implies (and ...
                   (syntaxp (... (mfc-rw `(bar ,x) ...) ...))
                   ...)
              (equal (... x ...) ...))

Here, x is bound in the conclusion to the result of rewriting some term,
say, tm.  Then the above call of mfc-rw will rewrite tm, which is
probably unnecessary.  So a preferable form of the rule above may be as
follows, so that tm is not further rewritten by mfc-rw+.

     (implies (and ...
                   (syntaxp (... (mfc-rw+ '(bar v) `((v . ,x)) ...) ...))
                   ...)
              (equal (... x ...) ...))

However, you may find that the additional rewriting done by mfc-rw is
useful in some cases.

(mfc-ap term mfc state): returns t or nil according to whether linear
arithmetic can determine that term is false.  To the cognoscenti:
returns the contradiction flag produced by linearizing term and adding
it to the linear-pot-lst.

During the execution of a metafunction by the theorem prover, the
expressions above compute the results specified.  However, there are no
axioms about the mfc- function symbols: they are uninterpreted function
symbols.  Thus, in the proof of the correctness of a metafunction, no
information is available about the results of these functions.  Thus,
_these functions can be used for heuristic purposes only._

For example, your metafunction may use these functions to decide
whether to perform a given transformation, but the transformation must
be sound regardless of the value that your metafunction returns.  We
illustrate this below.  It is sometimes possible to use the hypothesis
metafunction, hyp-fn, to generate a sufficient hypothesis to justify the
transformation.  The generated hypothesis might have already been
"proved" internally by your use of mfc-ts or mfc-rw, but the system
will have to prove it "officially" by relieving it.  We illustrate this
below also.

We conclude with a script that defines, verifies, and uses several
extended metafunctions.  This script is based on one provided by Robert
Krug, who was instrumental in the development of this style of
metafunction and whose help we gratefully acknowledge.

     ; Here is an example.  I will define (foo i j) simply to be (+ i j).
     ; But I will keep its definition disabled so the theorem prover
     ; doesn't know that.  Then I will define an extended metafunction
     ; that reduces (foo i (- i)) to 0 provided i has integer type and the
     ; expression (< 10 i) occurs as a hypothesis in the clause.

     ; Note that (foo i (- i)) is 0 in any case.

     (defun foo (i j) (+ i j))

     (defevaluator eva eva-lst ((foo i j)
                                (unary-- i)

     ; I won't need these two cases until the last example below, but I
     ; include them now.

                                (if x y z)
                                (integerp x)))

     (set-state-ok t)

     (defun metafn (x mfc state)
       (cond
        ((and (consp x)
              (equal (car x) 'foo)
              (equal (caddr x) (list 'unary-- (cadr x))))

     ; So x is of the form (foo i (- i)).  Now I want to check some other
     ; conditions.

         (cond ((and (ts-subsetp (mfc-ts (cadr x) mfc state)
                                 *ts-integer*)
                     (member-equal `(NOT (< '10 ,(cadr x)))
                                   (mfc-clause mfc)))
                (quote (quote 0)))
               (t x)))
        (t x)))

     (defthm metafn-correct
       (equal (eva x a) (eva (metafn x mfc state) a))
       :rule-classes ((:meta :trigger-fns (foo))))

     (in-theory (disable foo))

     ; The following will fail because the metafunction won't fire.
     ; We don't know enough about i.

     (thm (equal (foo i (- i)) 0))

     ; Same here.

     (thm (implies (and (integerp i) (< 0 i)) (equal (foo i (- i)) 0)))

     ; But this will work.

     (thm (implies (and (integerp i) (< 10 i))
                   (equal (foo i (- i)) 0)))

     ; This won't, because the metafunction looks for (< 10 i) literally,
     ; not just something that implies it.

     (thm (implies (and (integerp i) (< 11 i))
                   (equal (foo i (- i)) 0)))

     ; Now I will undo the defun of metafn and repeat the exercise, but
     ; this time check the weaker condition that (< 10 i) is provable
     ; (by rewriting it) rather than explicitly present.

     (ubt 'metafn)

     (defun metafn (x mfc state)
       (cond
        ((and (consp x)
              (equal (car x) 'foo)
              (equal (caddr x) (list 'unary-- (cadr x))))
         (cond ((and (ts-subsetp (mfc-ts (cadr x) mfc state)
                                 *ts-integer*)
                     (equal (mfc-rw `(< '10 ,(cadr x)) t t mfc state)
                            *t*))

     ; The mfc-rw above rewrites (< 10 i) with objective t and iffp t.  The
     ; objective means the theorem prover will try to establish it.  The
     ; iffp means the theorem prover can rewrite maintaining propositional
     ; equivalence instead of strict equality.

                (quote (quote 0)))
               (t x)))
        (t x)))

     (defthm metafn-correct
       (equal (eva x a) (eva (metafn x mfc state) a))
       :rule-classes ((:meta :trigger-fns (foo))))

     (in-theory (disable foo))

     ; Now it will prove both:

     (thm (implies (and (integerp i) (< 10 i))
                   (equal (foo i (- i)) 0)))

     (thm (implies (and (integerp i) (< 11 i))
                   (equal (foo i (- i)) 0)))

     ; Now I undo the defun of metafn and change the problem entirely.
     ; This time I will rewrite (integerp (foo i j)) to t.  Note that
     ; this is true if i and j are integers.  I can check this
     ; internally, but have to generate a hyp-fn to make it official.

     (ubt 'metafn)

     (defun metafn (x mfc state)
       (cond
        ((and (consp x)
              (equal (car x) 'integerp)
              (consp (cadr x))
              (equal (car (cadr x)) 'foo))

     ; So x is (integerp (foo i j)).  Now check that i and j are
     ; ``probably'' integers.

         (cond ((and (ts-subsetp (mfc-ts (cadr (cadr x)) mfc state)
                                 *ts-integer*)
                     (ts-subsetp (mfc-ts (caddr (cadr x)) mfc state)
                                 *ts-integer*))
                *t*)
               (t x)))
        (t x)))

     ; To justify this transformation, I generate the appropriate hyps.

     (defun hyp-fn (x mfc state)

       (declare (ignore mfc state))

     ; The hyp-fn is run only if the metafn produces an answer different
     ; from its input.  Thus, we know at execution time that x is of the
     ; form (integerp (foo i j)) and we know that metafn rewrote
     ; (integerp i) and (integerp j) both to t.  So we just produce their
     ; conjunction.  Note that we must produce a translated term; we
     ; cannot use the macro AND and must quote constants!  Sometimes you
     ; must do tests in the hyp-fn to figure out which case the metafn
     ; produced, but not in this example.

                `(if (integerp ,(cadr (cadr x)))
                     (integerp ,(caddr (cadr x)))
                     'nil))

     (defthm metafn-correct
       (implies (eva (hyp-fn x mfc state) a)
                (equal (eva x a) (eva (metafn x mfc state) a)))
       :rule-classes ((:meta :trigger-fns (integerp))))

     (in-theory (disable foo))

     ; This will not be proved.

     (thm (implies (and (rationalp x) (integerp i)) (integerp (foo i j))))

     ; But this will be.

     (thm (implies (and (rationalp x)
                        (integerp i)
                        (integerp j))
                   (integerp (foo i j))))

FAILED-FORCING    how to deal with a proof failure in a forcing round

See FORCING-ROUND for a background discussion of the notion of
forcing rounds.  When a proof fails during a forcing round it means
that the "gist" of the proof succeeded but some "technical detail"
failed.  The first question you must ask yourself is whether the forced
goals are indeed theorems.  We discuss the possibilities below.

If you believe the forced goals are theorems, you should follow the
usual methodology for "fixing" failed ACL2 proofs, e.g., the
identification of key lemmas and their timely and proper use as rules.
See FAILURE and see PROOF-TREE.

The rules designed for the goals of forcing rounds are often just what
is needed to prove the forced hypothesis at the time it is forced.
Thus, you may find that when the system has been "taught" how to prove
the goals of the forcing round no forcing round is needed.  This is
intended as a feature to help structure the discovery of the necessary
rules.

If a hint must be provided to prove a goal in a forcing round, the
appropriate "goal specifier" (the string used to identify the goal to
which the hint is to be applied) is just the text printed on the line
above the formula, e.g., "[1]Subgoal *1/3"".  See GOAL-SPEC.

If you solve a forcing problem by giving explicit hints for the goals
of forcing rounds, you might consider whether you could avoid forcing
the assumption in the first place by giving those hints in the
appropriate places of the main proof.  This is one reason that we print
out the origins of each forced assumption.  An argument against this
style, however, is that an assumption might be forced in hundreds of
places in the main goal and proved only once in the forcing round, so
that by delaying the proof you actually save time.

We now turn to the possibility that some goal in the forcing round is
not a theorem.

There are two possibilities to consider.  The first is that the
original theorem has insufficient hypotheses to ensure that all the
forced hypotheses are in fact always true.  The "fix" in this case is
to amend the original conjecture so that it has adequate hypotheses.

A more difficult situation can arise and that is when the conjecture
has sufficient hypotheses but they are not present in the forcing round
goal.  This can be caused by what we call "premature" forcing.

Because ACL2 rewrites from the inside out, it is possible that it will
force hypotheses while the context is insufficient to establish them.
Consider trying to prove (p x (foo x)).  We first rewrite the formula
in an empty context, i.e., assuming nothing.  Thus, we rewrite (foo x)
in an empty context.  If rewriting (foo x) forces anything, that forced
assumption will have to be proved in an empty context.  This will
likely be impossible.

On the other hand, suppose we did not attack (foo x) until after we had
expanded p.  We might find that the value of its second argument, (foo
x), is relevant only in some cases and in those cases we might be able
to establish the hypotheses forced by (foo x).  Our premature forcing
is thus seen to be a consequence of our "over eager" rewriting.

Here, just for concreteness, is an example you can try.  In this
example, (foo x) rewrites to x but has a forced hypothesis of
(rationalp x).  P does a case split on that very hypothesis and uses
its second argument only when x is known to be rational.  Thus, the
hypothesis for the (foo x) rewrite is satisfied.  On the false branch
of its case split, p simplies to (p1 x) which can be proved under the
assumption that x is not rational.

     (defun p1 (x) (not (rationalp x)))
     (defun p (x y)(if (rationalp x) (equal x y) (p1 x)))
     (defun foo (x) x)
     (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x)))
     (in-theory (disable foo))

The attempt then to do (thm (p x (foo x))) forces the unprovable goal
(rationalp x).

Since all "formulas" are presented to the theorem prover as single
terms with no hypotheses (e.g., since implies is a function), this
problem would occur routinely were it not for the fact that the theorem
prover expands certain "simple" definitions immediately without doing
anything that can cause a hypothesis to be forced.  See SIMPLE.
This does not solve the problem, since it is possible to hide the
propositional structure arbitrarily deeply.  For example, one could
define p, above, recursively so that the test that x is rational and
the subsequent first "real" use of y occurred arbitrarily deeply.

Therefore, the problem remains: what do you do if an impossible goal is
forced and yet you know that the original conjecture was adequately
protected by hypotheses?

One alternative is to disable forcing entirely.  See
DISABLE-FORCING.  Another is to disable the rule that caused the
force.

A third alternative is to prove that the negation of the main goal
implies the forced hypothesis.  For example,

     (defthm not-p-implies-rationalp
       (implies (not (p x (foo x))) (rationalp x))
       :rule-classes nil)

Observe that we make no rules from this formula.  Instead, we merely
:use it in the subgoal where we must establish (rationalp x).

     (thm (p x (foo x))
          :hints (("Goal" :use not-p-implies-rationalp)))

When we said, above, that (p x (foo x)) is first rewritten in an empty
context we were misrepresenting the situation slightly.  When we
rewrite a literal we know what literal we are rewriting and we
implicitly assume it false.  This assumption is "dangerous" in that it
can lead us to simplify our goal to nil and give up -- we have even
seen people make the mistake of assuming the negation of what they
wished to prove and then via a very complicated series of
transformations convince themselves that the formula is false.  Because
of this "tail biting" we make very weak use of the negation of our
goal.  But the use we make of it is sufficient to establish the forced
hypothesis above.

A fourth alternative is to weaken your desired theorem so as to make
explicit the required hypotheses, e.g., to prove

     (defthm rationalp-implies-main
       (implies (rationalp x) (p x (foo x)))
       :rule-classes nil)

This of course is unsatisfying because it is not what you originally
intended.  But all is not lost.  You can now prove your main theorem
from this one, letting the implies here provide the necessary case
split.

     (thm (p x (foo x))
          :hints (("Goal" :use rationalp-implies-main)))

FAILURE    how to deal with a proof failure

When ACL2 gives up it does not mean that the submitted conjecture is
invalid, even if the last formula ACL2 printed in its proof attempt is
manifestly false.  Since ACL2 sometimes generalizes the goal being
proved, it is possible it adopted an invalid subgoal as a legitimate
(but doomed) strategy for proving a valid goal.  Nevertheless,
conjectures submitted to ACL2 are often invalid and the proof attempt
often leads the careful reader to the realization that a hypothesis has
been omitted or that some special case has been forgotten.  It is good
practice to ask yourself, when you see a proof attempt fail, whether
the conjecture submitted is actually a theorem.

If you think the conjecture is a theorem, then you must figure out from
ACL2's output what you know that ACL2 doesn't about the functions in the
conjecture and how to impart that knowledge to ACL2 in the form of
rules.  The "key checkpoint" information printed at the end of the
summary provides a fine place to start.  See THE-METHOD for a
general discussion of how to prove theorems with ACL2, and see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed tutorial.
Also see SET-GAG-MODE for discussion of key checkpoints and an
abbreviated output mode that focuses attention on them.  You may find
it most useful to start by focusing on key checkpoints that are not
under a proof by induction, if any, both because these are more likely
to suggest useful lemmas and because they are more likely to be
theorems; for example, generalization may have occurred before a proof
by induction has begun.  If you need more information than is provided
by the key checkpoints -- although this should rarely be necessary --
then you can look at the full proof, perhaps with the aid of certain
utilities: see PROOF-TREE, see SET-GAG-MODE, and see
SET-SAVED-OUTPUT.

For information on a tool to help debug failures of encapsulate and
progn events, as well as certify-book failures, see REDO-FLAT.

Again, see THE-METHOD for a general discussion of how to prove
theorems with ACL2, and see INTRODUCTION-TO-THE-THEOREM-PROVER
for a more detailed tutorial.  See also the book "Computer-Aided
Reasoning: An Approach" (Kaufmann, Manolios, Moore), as well as the
discussion of how to read Nqthm proofs and how to use Nqthm rules in "A
Computational Logic Handbook" by Boyer and Moore (Academic Press, 1988).

If the failure occurred during a forcing round, see
FAILED-FORCING.

FIND-RULES-OF-RUNE    find the rules named rune

     General Form:
     (find-rules-of-rune rune wrld)

This function finds all the rules in wrld with :rune rune.  It returns
a list of rules in their internal form (generally as described by the
corresponding defrec).  Decyphering these rules is difficult since one
cannot always look at a rule object and decide what kind of record it
is without exploiting many system invariants (e.g., that :rewrite runes
only name rewrite-rules).

At the moment this function returns nil if the rune in question is a
:refinement rune, because there is no object representing :refinement
rules.  (:refinement rules cause changes in the 'coarsenings
properties.)  In addition, if the rune is an :equivalence rune, then
congruence rules with that rune will be returned -- because
:equivalence lemmas generate some congruence rules -- but the fact that
a certain function is now known to be an equivalence relation is not
represented by any rule object and so no such rule is returned.  (The
fact that the function is an equivalence relation is encoded entirely
in its presence as a 'coarsening of equal.)

FORCE    identity function used to force a hypothesis

When a hypothesis of a conditional rule has the form (force hyp) it is
logically equivalent to hyp but has a pragmatic effect.  In particular,
when the rule is considered, the needed instance of the hypothesis,
hyp', is assumed and a special case is generated, requiring the system
to prove that hyp' is true in the current context.  The proofs of all
such "forced assumptions" are delayed until the successful completion
of the main goal.  See FORCING-ROUND.

Forcing should only be used on hypotheses that are always expected to
be true, such as the guards of functions.  All the power of the theorem
prover is brought to bear on a forced hypothesis and no backtracking is
possible.  If the :executable-counterpart of the function force is
disabled, then no hypothesis is forced.  See ENABLE-FORCING and
see DISABLE-FORCING.  Forced goals can be attacked immediately
(see IMMEDIATE-FORCE-MODEP) or in a subsequent forcing round
(see FORCING-ROUND).  Also see CASE-SPLIT.

It sometimes happens that a conditional rule is not applied because
some hypothesis, hyp, could not be relieved, even though the required
instance of hyp, hyp', can be shown true in the context.  This happens
when insufficient resources are brought to bear on hyp' at the time we
try to relieve it.  A sometimes desirable alternative behavior is for
the system to assume hyp', apply the rule, and to generate explicitly a
special case to show that hyp' is true in the context.  This is called
"forcing" hyp.  It can be arranged by restating the rule so that the
offending hypothesis, hyp, is embedded in a call of force, as in (force
hyp).  By using the :corollary field of the rule-classes entry, a
hypothesis can be forced without changing the statement of the theorem
from which the rule is derived.

Technically, force is just a function of one argument that returns that
argument.  It is generally enabled and hence evaporates during
simplification.  But its presence among the hypotheses of a conditional
rule causes case splitting to occur if the hypothesis cannot be
conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is
otherwise applicable, forcing should be used only on hypotheses that
are expected always to be true.

A particularly common situation in which some hypotheses should be
forced is in "most general" type-prescription lemmas.  If a single
lemma describes the "expected" type of a function, for all "expected"
arguments, then it is probably a good idea to force the hypotheses of
the lemma.  Thus, every time a term involving the function arises, the
term will be given the expected type and its arguments will be required
to be of the expected type.  In applying this advice it might be wise
to avoid forcing those hypotheses that are in fact just type predicates
on the arguments, since the routine that applies type-prescription
lemmas has fairly thorough knowledge of the types of all terms.

Force can have the additional benefit of causing the ACL2 typing
mechanism to interact with the ACL2 rewriter to establish the
hypotheses of type-prescription rules.  To understand this remark,
think of the ACL2 type reasoning system as a rather primitive
rule-based theorem prover for questions about Common Lisp types, e.g.,
"does this expression produce a consp?"  "does this expression produce
some kind of ACL2 number, e.g., an integerp, a rationalp, or a
complex-rationalp?" etc.  It is driven by type-prescription rules.  To
relieve the hypotheses of such rules, the type system recursively
invokes itself.  This can be done for any hypothesis, whether it is
"type-like" or not, since any proposition, p, can be phrased as the
type-like question "does p produce an object of type nil?"  However, as
you might expect, the type system is not very good at establishing
hypotheses that are not type-like, unless they happen to be assumed
explicitly in the context in which the question is posed, e.g., "If p
produces a consp then does p produce nil?"  If type reasoning alone is
insufficient to prove some instance of a hypothesis, then the instance
will not be proved by the type system and a type-prescription rule with
that hypothesis will be inapplicable in that case.  But by embedding
such hypotheses in force expressions you can effectively cause the type
system to "punt" them to the rest of the theorem prover.  Of course, as
already noted, this should only be done on hypotheses that are "always
true."  In particular, if rewriting is required to establish some
hypothesis of a type-prescription rule, then the rule will be found
inapplicable because the hypothesis will not be established by type
reasoning alone.

The ACL2 rewriter uses the type reasoning system as a subsystem.  It is
therefore possible that the type system will force a hypothesis that
the rewriter could establish.  Before a forced hypothesis is reported
out of the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A
type-prescription rule fails to apply because some true hypothesis is
not being relieved.  The user changes the rule so as to *force* the
hypothesis.  The system then applies the rule but reports no forcing.
How can this happen?  The type system "punted" the forced hypothesis to
the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to force
when there is an if term present in the goal being simplified.  Since
and terms and or terms are merely abbreviations for if terms, they also
prevent forcing.  Note that if terms are ultimately eliminated using
the ordinary flow of the proof (but see
SET-CASE-SPLIT-LIMITATIONS), allowing force ultimately to function as
intended.  Moreover, forcing can be disabled, as described above; also
see DISABLE-FORCING.

FORCING-ROUND    a section of a proof dealing with forced assumptions

If ACL2 "forces" some hypothesis of some rule to be true, it is obliged
later to prove the hypothesis.  See FORCE.  ACL2 delays the
consideration of forced hypotheses until the main goal has been proved.
It then undertakes a new round of proofs in which the main goal is
essentially the conjunction of all hypotheses forced in the preceding
proof.  Call this round of proofs the "Forcing Round."  Additional
hypotheses may be forced by the proofs in the Forcing Round.  The
attempt to prove these hypotheses is delayed until the Forcing Round
has been successfully completed.  Then a new Forcing Round is
undertaken to prove the recently forced hypotheses and this continues
until no hypotheses are forced.  Thus, there is a succession of Forcing
Rounds.

The Forcing Rounds are enumerated starting from 1.  The Goals and
Subgoals of a Forcing Round are printed with the round's number
displayed in square brackets.  Thus, "[1]Subgoal 1.3" means that the
goal in question is Subgoal 1.3 of the 1st forcing round.  To supply a
hint for use in the proof of that subgoal, you should use the goal
specifier "[1]Subgoal 1.3".  See GOAL-SPEC.

When a round is successfully completed -- and for these purposes you
may think of the proof of the main goal as being the 0th forcing round
-- the system collects all of the assumptions forced by the
just-completed round.  Here, an assumption should be thought of as an
implication, (implies context hyp), where context describes the context
in which hyp was assumed true.  Before undertaking the proofs of these
assumptions, we try to "clean them up" in an effort to reduce the
amount of work required.  This is often possible because the forced
assumptions are generated by the same rule being applied repeatedly in
a given context.

By delaying and collecting the forced assumptions until the completion
of the "main goal" we gain two advantages.  First, the user gets
confirmation that the "gist" of the proof is complete and that all that
remains are "technical details."  Second, by delaying the proofs of the
forced assumptions ACL2 can undertake the proof of each assumption only
once, no matter how many times it was forced in the main goal.

In order to indicate which proof steps of the previous round were
responsible for which forced assumptions, we print a sentence
explaining the origins of each newly forced goal.  For example,

     [1]Subgoal 1, below, will focus on
     (GOOD-INPUTP (XTRANS I)),
     which was forced in
      Subgoal 14, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I),
      and
      Subgoal 28, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I).

In this entry, "[1]Subgoal 1" is the name of a goal which will be
proved in the next forcing round.  On the next line we display the
forced hypothesis, call it x, which is (good-inputp (xtrans i)) in this
example.  This term will be the conclusion of the new subgoal.  Since
the new subgoal will be printed in its entirety when its proof is
undertaken, we do not here exhibit the context in which x was forced.
The sentence then lists (possibly a succession of) a goal name from the
just-completed round and some step in the proof of that goal that
forced x.  In the example above we see that Subgoals 14 and 28 of the
just-completed proof forced (good-inputp (xtrans i)) by applying
(:rewrite pred-cruncher) to the term (pred (xtrans i) i).

If one were to inspect the theorem prover's description of the proof
steps applied to Subgoals 14 and 28 one would find the word "forced"
(or sometimes "forcibly") occurring in the commentary.  Whenever you
see that word in the output, you know you will get a subsequent forcing
round to deal with the hypotheses forced.  Similarly, if at the
beginning of a forcing round a rune is blamed for causing a force in
some subgoal, inspection of the commentary for that subgoal will reveal
the word "forced" after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier.  When
the simplifier encounters a hypothesis of the form (force hyp) it first
attempts to establish it by rewriting hyp to, say, hyp'.  If the truth
or falsity of hyp' is known, forcing is not required.  Otherwise, the
simplifier actually forces hyp'.  That is, the x mentioned above is
hyp', not hyp, when the forced subgoal was generated by the simplifier.

Once the system has printed out the origins of the newly forced goals,
it proceeds to the next forcing round, where those goals are
individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults to
the global enabled structure.  For example, suppose some rune, rune, is
globally enabled.  Suppose in some event you disable the rune at "Goal"
and successfully prove the goal but force "[1]Goal".  Then during the
proof of "[1]Goal", rune is enabled "again."  The right way to think
about this is that the rune is "still" enabled.  That is, it is enabled
globally and each forcing round resumes with the global enabled
structure.

GAG-MODE    verbosity of proof output

Please see SET-GAG-MODE for an explanation of gag-mode, which
can take any of the following values:

     (gag-mode) ; generally evaluates to t, nil, or :goals

GC$    invoke the garbage collector

This function is provided so that the user can call the garbage
collector of the host Lisp from inside the ACL2 loop.  Specifically, a
call of gc$ is translated into a call of a function below on the same
arguments.

     Allegro CL:            excl:gc
     CCL                    ccl::gc
     CLISP                  ext:gc
     CMU Common Lisp        system::gc
     GCL                    si::gbc
     LispWorks              hcl::gc-generation [default argument list:
                                                (7) for 64-bit OS, else (3)]
     SBCL                   sb-ext:gc

The arguments, if any, are as documented in the underlying Common Lisp.
It is up to the user to pass in the right arguments, although we may do
some rudimentary checks.

This function always returns nil.

GCL    tips on building and using ACL2 based on Gnu Common Lisp

See the installation instructions for basic information about building
ACL2 on top of GCL, including information about where to fetch GCL.
Here, we provide some tips that may be useful.

1. You can place forms to evaluate at start-up into file init.lsp in the
directory where you are starting ACL2 (GCL), or into file acl2-init.lsp
in your home directory.  For example, in order to evaluate both of the
lisp forms mentioned in 2 below, you could put them both into init.lsp
in the current directory or in ~/acl2-init.lsp (either way, without
(lp) or :q):

     (setq si::*optimize-maximum-pages* nil)
     (si::allocate 'cons 75000 t)

Note that if you want to put ACL2 patches in this file, you should
precede them with (in-package "ACL2").

2. Suppose you run out of space, for example with an error like this:

        Error: The storage for CONS is exhausted.
          Currently, 59470 pages are allocated.
          Use ALLOCATE to expand the space.

The following suggestion from Camm Maguire will minimize the heap size,
at the cost of more garbage collection time.

     :q   ; exit the ACL2 loop
     (setq si::*optimize-maximum-pages* nil)
     (lp) ; re-enter the ACL2 loop

A second thing to try, suggested by several people, is to preallocate
more pages before the run, e.g.:

     :q   ; exit the ACL2 loop
     (si::allocate 'cons 75000 t)
     (lp) ; re-enter the ACL2 loop

Also see RESET-KILL-RING for a suggestion on how to free up
space.

3. Windows users have seen this error:

     cc1.exe: unrecognized option `-fno-zero-initialized-in-bss'

Camm Maguire suggests that a solution may be to evaluate the following
in GCL before building ACL2.

     (in-package 'compiler)
     (let* ((x `-fno-zero-initialized-in-bss')
            (i (search x *cc*)))
             (setq *cc* (concatenate 'string
                                     (subseq *cc* 0 i)
                                     (subseq *cc* (+ i (length x))))))

4. It is possible to profile using ACL2 built on GCL.  See file
save-gprof.lsp in the ACL2 source directory.

5. Some versions of GCL may have garbage-collector bugs that, on rare
occasions, cause ACL2 (when built on GCL) to break.  If you run into
this, a solution may be to execute the following:

     :q
     (si::sgc-on nil)
     (lp)

Alternatively, put (si::sgc-on nil) in your ~/acl2-init.lsp file.

A full regression test and found that this decreased performance by
about 10%.  But even with that, GCL may be the fastest Common Lisp for
ACL2 on Linux (performance figures may often be found by following the
"Recent changes" link on the ACL2 home page).

6. GCL operations on numbers can sometimes be sped up, perhaps by up to
two orders of magnitude, by suitable declare forms (also see
TYPE-SPEC).  The following example, developed with Warren Hunt and
Serita Nelesen, illustrates the use of such declarations.

     ; File iplus.lisp:
     ; Operations on naturals together with positive infinity (represented as -1).

     ; After (ld "iplus.lisp"), escape to raw Lisp with :q and then eavluate
     ; (disassemble 'big-test).  You should see lots of arithmetic operations
     ; in C code, but no calls of C functions CMPmake_fixnum or number_plus.

     (in-package "ACL2")

     (defmacro i-max ()
       (expt 2 (1- 28)))

     (defmacro i+ (x y)
       `(the (signed-byte 28)
             (let ((x ,x)
                   (y ,y))
               (declare (type (signed-byte 28) x y))
               (cond ((or (< x 0)
                          (< y 0))
                      -1)
                     (t (let ((result
                               (the (signed-byte 29) (+ x y))))
                          (declare (type (signed-byte 29) result))
                          (cond ((>= result (i-max)) -1)
                                (t (the (signed-byte 28) result)))))))))

     (defmacro imin (x y)
       `(the (signed-byte 28)
             (let ((x ,x)
                   (y ,y))
               (declare (type (signed-byte 28) x y))
               (cond ((< x 0)
                      (cond ((< y 0) -1)
                            (t y)))
                     ((< y 0)
                      x)
                     (t
                      (the (signed-byte 28) (min x y)))))))

     (defun big-test (x y z)
       (declare (type (signed-byte 28) x y z))
       (imin (i+ x y)
             (i+ y (imin x z))))

GET-WORMHOLE-STATUS    make a wormhole's status visible outside the wormhole

General Form: (get-wormhole-status name state)

Name should be the name of a wormhole (see WORMHOLE).  This
function returns an error triple of the form (mv nil s state), where s
is the status of the named wormhole.  The status is obtained by reading
the oracle in the ACL2 state.

This function makes the status of a wormhole visible outside the
wormhole.  But since this function takes state and modifies it, the
function may only be used in contexts in which you may change state.
Otherwise, the wormhole status may stay in the wormhole.  See
wormhole-eval and wormhole.

GOAL-SPEC    to indicate where a hint is to be used

     Examples:
     "Goal"
     "goal"
     "Subgoal *1/3''"
     "subgoal *1/3''"
     "[2]Subgoal *1/3''"

When hints are given to the theorem prover, a goal-spec is provided to
specify the goal to which the hints are to be applied.  The hints
provided are carried along innocuously until the named goal arises.
When it arises, the hints are "activated" for that goal and its
descendents.

A legal goal specification may be extracted from the theorem prover's
output.  Certain lines clearly label formulas, as in

     Subgoal *1/3.2'
     (IMPLIES ... ...)

and these lines all give rise to goal specifications.  In general,
these lines all start either with "Goal" or "Subgoal" or else with
those words preceded by a number in square brackets, as in

     [1]Subgoal *1/3.2'
     (IMPLIES ... ...).

A goal specification may be obtained by deleting any surrounding
whitespace from such a line and embedding the text in string quotation
marks.  Thus

     "[1]Subgoal *1/3.2'"

is the goal specifier for the goal above.

As noted, a hint is applied to a goal when the hint's goal
specification matches the name ACL2 assigns to the goal.  The matching
algorithm is case-insensitive.  Thus, alternative goal specifications
for the goal above are "[1]subgoal *1/3.2'" and "[1]SUBGOAL *1/3.2'".
The matching algorithm does not tolerate non-case discrepancies.  Thus,
"[1]Subgoal*1/3.2'" and " [1]Subgoal *1/3.2'" are unacceptable.

Sometimes a formula is given two names, e.g.,

     Subgoal *1/14.2'
     (IMPLIES ...
              ...)
     Name the formula above *1.1.

It is the first name (the one that starts with "Goal" or "Subgoal") and
not the second which constitutes a legal goal-spec.  Roughly speaking,
when the system prints the line containing the goal specification, it
activates any hints that are attached to that goal-spec.  Consider the
example above.  Suppose Subgoal *1/14.2' could be proved by using a
certain lemma instance.  Then the appropriate entry in the hints would
be:

     ("Subgoal *1/14.2'" :use ...)

This might surprise you because the system appears to do nothing to
*1/14.2' besides push it for a subsequent induction.  But actually
between the time the system printed the goal-spec line and the time it
decides to push the goal, you can think of the system as trying
everything it has.  So a use hint activated when Subgoal *1/14.2'
arises is just what you want.

But what if you want to give an :induct hint?  By the time induction is
tried, the formula has been given the name *1.1.  Well, this is one you
just have to remember:

     ("Subgoal *1/14.2'" :induct ...).

When the above hint is activated the :induct directive short-circuits
the rest of the processing and sends immediately the formula into the
pool of goals to prove by induction.  The induct hint is attached to
the formula in the pool and when the time comes to turn our attention
to that goal, the induct advice is followed.

We conclude by emphasizing a point made above, that a hint is applied
to a goal when the hint's goal specification matches the name ACL2
assigns to the goal.  If there is no such match, then the hint is
ignored.  Consider the following example.

     (thm (equal (append (append x y) z) (append x y z))
          :hints (("Subgoal *1/" :in-theory nil)))

Normally, :in-theory hints are inherited by subgoals (see
HINTS-AND-THE-WATERFALL), so you might expect that the empty theory is
used in Subgoal *1/2 and Subgoal *1/1.  But in fact, since there is no
subgoal printed that is labeled Subgoal *1/, the above :in-theory hint
is ignored.  The above example is in contrast to the following, where
the hint makes the proof fail, because there really is a Subgoal *1/ in
the proof this time.

     (thm (implies (and (not (endp x)) (not (endp (cdr x))))
                   (equal (append (append x y) z) (append x y z)))
          :hints (("Subgoal *1/" :in-theory nil)))

GUARD    restricting the domain of a function

The ACL2 system provides a mechanism for restricting a function to a
particular domain.  Such restrictions are called "guards."  A
definition's guard has no effect on the logical axiom added when that
definition is accepted by ACL2, and novices are often best served by
avoiding guards.  However, guards can be useful as a specification
device or for increasing execution efficiency.  To make such a
restriction, use the :guard keyword; see XARGS.  The general
issue of guards and guard verification is discussed in the topics
listed below.

Related topics other than immediate subtopics:

To begin further discussion of guards, see GUARD-INTRODUCTION.
That section directs the reader to further sections for more details.
To see just a summary of some commands related to guards, see
GUARD-QUICK-REFERENCE.

EXTRA-INFO    generate markers to indicate sources of guard proof obligations

See GUARD-DEBUG for a discussion of this function, which is
useful for debugging failures during guard verification.

GUARD-DEBUG    generate markers to indicate sources of guard proof obligations

ACL2 guard verification (see GUARD) is often best avoided by
beginning users of ACL2.  When guard verification is employed, it can
generate numerous goals, some of which may not be theorems if the
definition being processed has bugs.  It can be difficult to find such
bugs.  This documentation topic explains a capability provided by ACL2
to help find such bugs.

We begin with the following example.  Although it is contrived and a bit
simplistic, it illustrates how the guard-debug utility works.

     (defun length-repeat (x)
       (length (append x x)))
     (verify-guards length-repeat :guard-debug t)

The output produces two top-level key checkpoints, as follows.

     Subgoal 2
     (IMPLIES (EXTRA-INFO '(:GUARD (:BODY LENGTH-REPEAT))
                          '(APPEND X X))
              (TRUE-LISTP X))

     Subgoal 1
     (IMPLIES (AND (EXTRA-INFO '(:GUARD (:BODY LENGTH-REPEAT))
                               '(LENGTH (APPEND X X)))
                   (NOT (TRUE-LISTP (APPEND X X))))
              (STRINGP (APPEND X X)))

The upper subgoal (numbered 2) says that the body of the definition of
length-repeat contains a call (APPEND X X), which is the source of the
goal.  In this case, that makes sense: the guard for a call (append
arg1 arg2) is (true-listp arg1), which in this case is (TRUE-LISTP X).
The lower subgoal (numbered 1) says that the same definition contains
the call (LENGTH (APPEND X X)), which generates the proof obligation
that if (APPEND X X) does not satisfy true-listp, then it must satisfy
stringp.  That proof obligation comes directly from the guard for
length.

Of course, the example above is a bit obvious.  But for large
definitional bodies such information can be very helpful.  Note that
guard-debug can be specified not only in verify-guards events but also
in xargs declare forms of defun events.

We now describe the guard-debug utility in some detail.

(Extra-info x y) always returns t by definition.  However, if guard
verification takes place with a non-nil setting of guard-debug (see
below), then the goals generated for guard verification can include
hypotheses that are calls of extra-info.  Typically, such a hypothesis
is of the following form:

     (extra-info '(:guard (:body F))
                 '(G ARG1 ... ARGk))

The above form indicates that the goal in which it occurs was generated
to verify that the guard of the function F is satisfied by the
arguments ARG1 through ARGk, where the term (G ARG1 ... ARGk) occurs in
the body of the function F whose guard verification is in progress.  If
however the above call of G occurs in the guard of F instead of the
body of F, then :body is replaced by :guard above:

     (extra-info '(:guard (:guard F))
                 '(G ARG1 ... ARGk))

If the same proof obligation (goal clause) arises from more than one
occurrence of the same call, then a single goal will be generated,
which has several extra-info hypotheses added to show the multiple
sources of that proof obligation.

All rules (see RUNE) associated with extra-info are disabled by
default, so that hypotheses of the form described above are not
simplified to t.  These hypotheses are intended to ride along for free:
you can generally expect the proof to have the same structure whether
or not the :guard-debug option is supplied, though on rare occasions
the proofs may diverge.

It remains to explain the notion of a guard-debug setting of t, that
is, to explain how to obtain the additional hypotheses described above.
If guards are being verified during processing of a defun event (whether
or not inside a call of mutual-recursion), then one specifies
:guard-debug t in an xargs declaration of a declare form; see
XARGS.  If however the guard verification is on behalf of a
verify-guards call, whether for a definition or a theorem, then one
specifies the keyword argument :guard-debug t.

Also see PRINT-GV for a utility for debugging guard violations,
in contrast to the above guard-debug mechanism, which is for debugging
failed proofs arising from guard verification.

GUARD-EVALUATION-EXAMPLES-LOG    log showing combinations of defun-modes and guard-checking

See GUARD-EVALUATION-EXAMPLES-SCRIPT for a script that shows
the interaction of defun-modes with the value set by
set-guard-checking.  Here, we present a log resulting from running this
script.

See SET-GUARD-CHECKING for discussion of the interaction between
defun-modes and guard-checking that is illustrated by this script.
Also see GUARD-EVALUATION-TABLE for a succinct table, with
associated discussion, that covers in detail the interactions
illustrated here.

     ACL2 !>(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(trace$ fact)
      ((FACT))
     ACL2 !>:set-guard-checking t

     Guard-checking-on already has value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
     FACT, which is (INTEGERP X), is violated by the arguments in the call
     (FACT T).  See :DOC trace for a useful debugging utility.  See :DOC
     set-guard-checking for information about suppressing this check with
     (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
     FACT, which is (INTEGERP X), is violated by the arguments in the call
     (FACT T).  See :DOC trace for a useful debugging utility.  See :DOC
     set-guard-checking for information about suppressing this check with
     (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u

               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard t
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u

               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     [[output omitted here]]

     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     [[Comment added to the log:
       Normally you would get a message about guard-checking being
       inhibited on recursive calls.  However, when a function is
       traced the guard-checking is done on recursive calls unless
       the guards have been verified (see :DOC verify-guards).
     ]]
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     [[Comment added to the log:
       In spite of the warning above, guards are checked here on
       self-recursive calls, because the function is traced.
     ]]
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
     and the :type-prescription rule FACT.  FACT is compliant with Common
     Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u
      L        1:x(DEFUN FACT (X) ...)
     ACL2 >:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     [[output omitted here]]

     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard t
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     [[output omitted here]]

     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription
     rule FACT.  FACT is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT

     [[Note added to log: No need to trace fact again after verify-guards.]]

     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >

GUARD-EVALUATION-EXAMPLES-SCRIPT    a script to show combinations of defun-modes and guard-checking

Below is a script that illustrates the combination of defun-modes --
:program mode, :logic mode without guards verified, and :logic mode
with guards verified -- with values from set-guard-checking -- t (the
default), :all, :none, and nil.  (It does not illustrate the value
:nowarn, which is the same as t except for inhibiting a warning.)  The
script also illustrates cases where the guard is not, or is, t.

See GUARD-EVALUATION-EXAMPLES-LOG for result of running this
script.  Before presenting the script below, we give some instructions
in case you want to run it yourself.

See SET-GUARD-CHECKING for discussion of the interaction between
defun-modes and guard-checking that is illustrated by this script.
Also see GUARD-EVALUATION-TABLE for a succinct table, with
associated discussion, that covers in detail the interactions
illustrated here.

The script mentions the running of "Tracing Code".  The code is the
following sequence of commands.

     (trace$ fact)
     :set-guard-checking t
     (fact 2)
     (fact t)
     :set-guard-checking :all
     (fact 2)
     (fact t)
     :set-guard-checking :none
     (fact 2)
     (fact t)
     :set-guard-checking nil
     (fact 2)
     (fact t)

If you want to run the script yourself, you may find it handy to use the
following Emacs keyboard macro for running the tracing code in 2-window
mode, with the cursor in the window with the script and ACL2 running in
the other window.

     (fset 'step-guard-script
        [?C-a ?C-  ?C-e ?M-w ?C-a ?C-n
         ?C-x ?o ?M-> ?C-y return ?C-x ?o])

     ; Put it on a key (if you have defined the indicated keymap by using
     ; emacs/emacs-acl2.el):
     (define-key ctl-t-keymap "r" 'step-guard-script)

The script follows.

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Program mode
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It shows execution in raw Lisp in the t and nil
     ; cases of :set-guard-checking, but not in the :all or :none cases.  We get a
     ; guard violation for argument t in the case :set-guard-checking t.

     :u

     (defun fact (x)
              (declare (xargs :guard t
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It should give the same results as above,
     ; except that we no longer get a guard violation in the case
     ; :set-guard-checking t.

     :u

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Logic mode, guard other than t
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It should give guard violations for (fact t)
     ; with guard-checking set to t or :all.  It should never run in raw Lisp,
     ; because we have not verified guards.  In the t case, we can get a warning
     ; about avoiding the guard check on recursive calls, but only if we do not
     ; trace the function, fact.

     (verify-guards fact)

     ; Run the Tracing Code here.  The results should be as described just above,
     ; except that now we go into raw Lisp for (fact 2) with guard-checking other
     ; than :none.

     :u
     :u

     ; The following definition is the same as above, except that guards are
     ; verified.

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  We should get the same traces as in the
     ; immediately preceding case, since guards had been verified in both cases.

     :u

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Logic mode, guard t
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard t
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  We should never go in to raw Lisp, because
     ; guards have not been verified.  We will see the same traces for (fact 2) as
     ; with the (integerp x) guard above with :verify-guards nil specified, except
     ; that even without tracing, there is no warning for :set-guard-checking t
     ; about recursive calls.  And, there are no guard violations for (fact t), of
     ; course, since posp (necessarily, if we are to verify guards) has a guard of
     ; t.

     (verify-guards fact)

     ; Run the Tracing Code here.  You shouldn't see any surprises.  Note however
     ; that if we back up to the start (using :u :u) and then define fact as just
     ; above but without :verify-guards nil, then the :none setting will allow us
     ; to go into raw Lisp: although :none generally avoids execution of raw Lisp
     ; counterparts, it allows this when the guard is T and guards have been
     ; verified.

GUARD-EVALUATION-TABLE    a table that shows combinations of defun-modes and guard-checking

See SET-GUARD-CHECKING for an introduction to the topic
discussed here.  Also see GUARD for a general discussion of
guards, and see GUARD-EVALUATION-EXAMPLES-SCRIPT for a script
that illustrates combinations presented below.

Note: The default setting for guard-checking (that is, the initial
value for (@ guard-checking-on)) is T.

The table below illustrates the interaction of the defun-mode with the
value supplied to set-guard-checking.  The first row considers
functions defined in :program mode; the other two consider functions
defined in :logic mode.  The columns correspond to four values of state
global 'guard-checking-on, as supplied to set-guard-checking.  (A fifth
value, :nowarn, is similar to t but suppresses warnings encountered
with t (as explained in those warning messages), and is not considered
here.)  During proofs, 'guard-checking-on is set to nil regardless of
how this variable has been set in the top-level loop.

Below this table, we make some comments about its entries, ordered by
row and then by column.  For example, when we refer to "b2" we are
discussing the execution of a :logic mode function whose guards have
not been verified, after having executed :set-guard-checking :all.

        guard-checking-on:  (1)t      (2):all   (3):none   (4)nil

      (a) :program             a1        a2        a3        a4
      (b) guards not verified  b1        b2        b3        b4
      (c) guards verified      c1        c2        c3        c4

a1. Check the guard upon entry, then use the raw Lisp code if the guard
checks (else cause an error).  This is a common setting when one wants a
little guard checking but also wants the efficiency of raw Lisp.  But
note that you can get raw Lisp errors.  For example, if you make the
definition (defun foo (x) (car x)) in :program mode and execute
:set-guard-checking t, and then execute (foo 3), you will likely get an
error from the call (car 3) made in raw Lisp.

a2. For built-in (predefined) functions, see a1 instead.  Otherwise:
Check the guard, without exception.  Thus, we never run the raw Lisp
code in this case.  This can be useful when testing :program mode
functions, but you may want to run :comp t or at least :comp :exec in
this case, so that the execution is done using compiled code.

a3. For built-in (predefined) functions, see a4 instead.  Otherwise:
Do not check the guard.  For :program mode functions, we never run the
raw Lisp code in this case; so if you care about efficiency, see the
comment in a2 above about :comp.  This combination is useful if you are
using ACL2 as a programming language and do not want to prove theorems
about your functions or suffer guard violations.  In this case, you can
forget about any connection between ACL2 and Common Lisp.

a4. Run the raw Lisp code without checking guards at all.  Thus, for
:program mode functions, the nil setting is often preferable to the
:none setting because you get the efficiency of raw Lisp execution.
However, with nil you can therefore get hard Lisp errors as in a1 above.

b1. Guards are checked at the top-level, though not at self-recursive
calls.  We never run the raw Lisp code in this case; guards would need
to be verified first.

b2. Unlike the t setting, guards are checked even on self-recursive
calls.  But like the t setting, we do not run the raw Lisp code.  Use
this setting if you want guards checked on each recursive call in spite
of the cost of doing so.

b3, b4. Execution avoids the raw Lisp code and never checks guards.  The
nil and :none settings behave the same in this case (i.e., for :logic
mode functions whose guards have not been verified), except that
recursive calls are never inlined for :none and tracing (see
TRACE) will show recursive calls for :none but not for nil.

c1, c2. Guards are checked.  If the checks pass, evaluation takes place
using the raw Lisp code.  If the checks fail, we get a guard violation.
Either way, we do not execute "in the logic"; we only execute using the
raw Lisp code.  Note that t and :all behave the same in this case,
(i.e. for :logic mode functions whose guards have been verified).

c3, c4. For the :none and nil settings, :logic mode functions whose
guards have been verified will never cause guard violations.  However,
with nil and for built-in functions in :logic mode, guards are still
checked: if the check succeeds, then evaluation is done using the raw
Lisp code, and if not, it is done by the "logic" code, including
self-recursive calls (though unlike the t case, we will not see a
warning about this).  But with :none for user-defined functions, no
guard checking is done, and the only time the raw Lisp code will be
executed is when the guard is t and guards are verified at the time the
executable counterpart of the function is defined (i.e., when the
function is admitted unless it is later defined again and compiled
using :comp).  Thus, if you use :none and you want a function (foo x)
with guard (g x) to execute using raw Lisp code, you can write a
"wrapper"function with a guard of t:

     (defun foo-wrap (x)
       (declare (xargs :guard t))
       (if (g x)
           (foo x)
         'do-not-case))

If you want the speed of executing raw Lisp code and you have
non-trivial guards on functions that you want to call at the top-level,
use nil rather than :none.

GUARD-INTRODUCTION    introduction to guards in ACL2

Most users can probably profit by avoiding dealing with guards most of
the time.  If they seem to get in the way, they can be "turned off"
using the command :set-guard-checking nil; for more about this, see
SET-GUARD-CHECKING.  For more about guards in general, see
GUARD.

The guard on a function symbol is a formula about the formals of the
function.  To see the guard on a function, use the keyword command
:args.  See ARGS.  To specify the guard on a function at
defun-time, use the :guard xarg.  See XARGS.

Guards can be seen as having either of two roles: (a) they are a
specification device allowing you to characterize the kinds of inputs a
function "should" have, or (b) they are an efficiency device allowing
logically defined functions to be executed directly in Common Lisp.
Briefly:  If the guards of a function definition are "verified" (see
VERIFY-GUARDS), then the evaluation of a call of that function
on arguments satisfying its guard will have the following property:

     All subsequent function calls during that evaluation will be on
     arguments satisfying the guard of the called function.

The consequence of this fact for (a) is that your specification
function is well-formed, in the sense that the values returned by this
function on appropriate arguments only depend on the restrictions of
the called functions to their intended domains.  The consequence of
this fact for (b) is that in the ACL2 system, when a function whose
guards have been verified is called on arguments that satisfy its
guard, then the raw lisp function defined by this function's defun
event is used to evaluate the call.  Note however that even when the
user-supplied defun is not used, ACL2 uses a corresponding "executable
counterpart" that generally performs, we expect, nearly as well as the
raw lisp function.  See COMP to see how compilation can speed
up both kinds of execution.

Let us turn next to the issue of the relationship between guards and
evaluation.  See GUARDS-AND-EVALUATION.

GUARD-MISCELLANY    miscellaneous remarks about guards

The discussion of guards concludes here with a few miscellaneous
remarks.  (Presumably you found this documentation by following a link;
see GUARDS-FOR-SPECIFICATION.)  For further information related
to guards other than what you find under "guard," see any of the
following documentation topics:  guard-example,
set-verify-guards-eagerness, set-guard-checking, and verify-guards.

Defun can be made to try to verify the guards on a function.  This is
controlled by the "defun-mode" of the defun; see DEFUN-MODE.
The defun-mode is either as specified with the :mode xarg of the defun
or else defaults to the default defun-mode.  See
DEFAULT-DEFUN-MODE.  If the defun-mode of the defun is :logic and
either a :guard is specified or :verify-guards t is specified in the
xargs, then we attempt to verify the guards of the function.  Otherwise
we do not.

It is sometimes impossible for the system to verify the guards of a
recursive function at definition time.  For example, the guard
conjectures might require the invention and proof of some inductively
derived property of the function (as often happens when the value of a
recursive call is fed to a guarded subroutine).  So sometimes it is
necessary to define the function using :verify-guards nil then to state
and prove key theorems about the function, and only then have the
system attempt guard verification.  Post-defun guard verification is
achieved via the event verify-guards.  See VERIFY-GUARDS.

It should be emphasized that guard verification affects only two
things: how fast ACL2 can evaluate the function and whether the
function is executed correctly by raw Common Lisp, without guard
violations.  Since ACL2 does not use the raw Common Lisp definition of
a function to evaluate its calls unless that function's guards have
been verified, the latter effect is felt only if you run functions in
raw Common Lisp rather than via ACL2's command loop.

Guard verification does not otherwise affect the theorem prover or the
semantics of a definition.  If you are not planning on running your
function on "big" inputs and you don't care if your function runs
correctly in raw Common Lisp (e.g., you have formalized some abstract
mathematical property and just happened to use ACL2 as your language),
there is no need to suffer through guard verification.  Often users
start by not doing guard verification and address that problem later.
Sometimes you are driven to it, even in mathematical projects, because
you find that you want to run your functions particularly fast or in
raw Common Lisp.

If certify-book is used to compile a file, and the file contains
functions with unverified guard conjectures, then you will be warned
that the compiled file cannot be loaded into raw Common Lisp with the
expectation that the functions will run correctly.  This is just the
same point we have been making:  ACL2 and Common Lisp agree only on the
restricted domains specified by our guards.  When guards are violated,
Common Lisp can do anything.  When you call a compiled function on
arguments violating its guards, the chances are only increased that
Common Lisp will go berserk, because compiled functions generally check
fewer things at runtime and tend to be more fragile than interpreted
ones.

Finally, we note that ACL2 collects up guards from declare forms in
order of appearance.  So for example, the declare form

     (declare (xargs :guard (foo x))
              (type string x)

will generate the guard (and (foo x) (stringp x)), while the form

     (declare (type string x)
              (xargs :guard (foo x))

will generate the guard (and (stringp x) (foo x)).  The only exception
to this rule is the case that :guard and :stobjs are specified in the
same xargs form, in which case the :stobjs form will be treated as
through it comes before the :guard form.

GUARD-QUICK-REFERENCE    brief summary of guard checking and guard verification

For a careful introduction to guards, see GUARD.

I. GUARD CHECKING DURING EXECUTION

_Effect_

Guards on definitions are checked at execution time (except for guards
on subsidiary calls of recursive or mutually recursive functions).

_When does it happen_

By default, guards are checked for all forms submitted at the top level.

_To disable_
:set-guard-checking nil   ; skip raw Lisp if there is a guard violation
:set-guard-checking :none ; skip guard checking entirely

_To (re-)enable_
:set-guard-checking t

See SET-GUARD-CHECKING for more options.

II. GUARD VERIFICATION

_Effect_

A proof is attempted of the obligations arising from the guards of
subsidiary functions in a defun, defthm, or defaxiom event.  In the
case of a defun, the guard itself is also verified (under an implicit
guard of t).

_When does it happen_

Only names of defined functions, defthms, and defaxioms are subject to
guard verification.  Guard verification may occur when functions are
defined (using defun), but it requires an explicit call of
verify-guards in order to verify guards for defthms and defaxioms.
Constrained functions (see ENCAPSULATE) may not have their
guards verified.

(verify-guards foo ...)
causes guard verification for the defun, defthm, or defaxiom named by
foo, if it has not already been successfully done.  The default
defun-mode (see DEFAULT-DEFUN-MODE) must be :logic, or else
this event is ignored.

(defun foo ...)
causes guard verification of foo if and only if the following
conditions are both met.  (However, see
SET-VERIFY-GUARDS-EAGERNESS for how to change this behavior.)

     1. Foo is processed in :logic mode (either by setting mode :logic
     globally, or by including :mode :logic in the xargs declaration).

     2. The xargs declaration (see XARGS) either specifies
     :guard or specifies :verify-guards t (or both).

(verify-termination foo ...)
causes guard verification of foo if foo is a function currently defined
in :program mode and the appropriate xargs are supplied, as discussed
for the case of defun above.  The default defun-mode (see
DEFAULT-DEFUN-MODE) must be :logic, or else this event is ignored.

GUARDS-AND-EVALUATION    the relationship between guards and evaluation

The guard has no effect on the logical axiom added by the definition of
a function.  It does, however, have consequences for how calls of that
function are evaluated in ACL2.  We begin by explaining those
consequences, when ACL2 is in its default "mode," i.e., as originally
brought up.  In subsequent discussion we'll consider other ways that
guards can interact with evaluation.

For more about guards in general, see GUARD.  For in-depth
discussion of the interaction between the defun-mode and guard checking,
see SET-GUARD-CHECKING, see GUARD-EVALUATION-TABLE, see
GUARD-EVALUATION-EXAMPLES-SCRIPT, and see
GUARD-EVALUATION-EXAMPLES-LOG.  Also see GENERALIZED-BOOLEANS
for discussion about a subtle issue in the evaluation of certain Common
Lisp functions.

_Guards and evaluation I:  the default_

Consider the following very simple definition.

     (defun foo (x) (cons 1 (cdr x)))

First consider how raw Common Lisp behaves when evaluating calls of
this function.  To evaluate (foo x) for some expression x, first x is
evaluated to some value v, and then (cons 1 (cdr x)) is evaluated with
x bound to v.  For example, if v is (cons 'a 3), then Common Lisp
computes (cons 1 3).  But if (for example) v is a number, e.g., 7, then
there is no way to predict what Common Lisp might do.  Some
implementations would cause "sensible" errors, others might return
nonsense, still others might crash the host machine.  The results tend
toward the catastrophic if the call of foo in question is in compiled
code.

Now by default, ACL2 evaluates calls of foo exactly as Common Lisp
does, except that it uses guards to check the "legality" of each
function call.  So for example, since (cdr x) has a guard of (or (consp
x) (equal x nil)), the call (foo 7) would cause a "guard violation," as
illustrated below.

     ACL2 !>(foo 7)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CDR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CDR 7).

     ACL2 !>

Thus, the relation between evaluation in ACL2 and evaluation in Common
Lisp is that the two produce the very same results, provided there is
no guard violation.

_Guards and evaluation II:_  :set-guard-checking.

The ACL2 logic is a logic of total functions.  That is, every
application of a function defined has a completely specified result.
See the documentation for each individual primitive for the
specification of what it returns when its guard is violated; for
example, see CDR.

The presence of guards thus introduces a choice in the sense of
evaluation.  When you type a form for evaluation do you mean for guards
to be checked or not?  Put another way, do you mean for the form to be
evaluated in Common Lisp (if possible) or in the ACL2 logic?  Note:  If
Common Lisp delivers an answer, it will be the same as in the logic,
but it might be erroneous to execute the form in Common Lisp.  For
example, the ACL2 logic definition of cdr implies that the cdr of an
atom is nil; see CDR.  So: should (cdr 7) cause a guard
violation error or return nil?

The top-level ACL2 loop has a variable which controls which sense of
execution is provided.  By default, "guard checking" is on, by which we
mean that guards are checked at runtime, in the sense already
described.  To allow execution to proceed in the logic when there is a
guard violation, do :set-guard-checking nil; or evaluate
:set-guard-checking :none to skip guard checking entirely.  To turn
"guard checking" back on, execute the top-level form
:set-guard-checking t.  The status of guard checking reflected in the
prompt; guard-checking is "on" when the prompt contains an exclamation
mark (also see DEFAULT-PRINT-PROMPT).  For example,

     ACL2 !>

means guard checking is on and

     ACL2 >

means guard checking is off.  The exclamation mark can be thought of as
"barring" certain computations.  The absence of the mark suggests the
absence of error messages or unbarred access to the logical axioms.
Thus, for example

     ACL2 !>(car 'abc)

will signal an error, while

     ACL2 >(car 'abc)

will return nil.  To return to our previous example:  with guard
checking off, (foo 7) evaluates to (cons 1 nil).  Also see
SET-GUARD-CHECKING.

_Guards and evaluation III:  guard verification_

Consider the defininition of foo given above, but modified so that a
reasonable guard of (consp x) is specified, as shown below.

     (defun foo (x)
       (declare (xargs :guard (consp x)))
       (cons 1 (cdr x)))

We say "reasonable guard" above because if x is such that (consp x)
holds, then the call of cdr in the evaluation of (foo x) will not cause
a guard violation.  Thus, it "should" be legal to evaluate (foo x), for
any such x, simply by evaluating this form in raw Common Lisp.

The verify-guards event has been provided for this purpose.  Details
may be found elsewhere; see VERIFY-GUARDS.  Briefly, for any
defined function fn, the event (verify-guards fn) attempts to check the
condition discussed above, that whenever fn is called on arguments that
satisfy its guard, the evaluation of this call will proceed without any
guard violation.  (Moreover, the guard itself should be evaluable
without any guard violation.)  If this check is successful, then future
calls of this sort will be evaluated in raw Common Lisp.

Returning to our example above, the (verify-guards foo) will succeed
because the guard (consp x) of foo implies the guard generated from the
call (cdr x) in the body of the definition, namely, (or (consp x)
(equal x nil)) (see CDR).  Then the evaluation of (foo (cons 'a
3)) will take place in raw Common Lisp, because (cons 'a 3) satisfies
the guard of foo.

This ability to dive into raw Common Lisp hinges on the proof that the
guards you attach to your own functions are sufficient to ensure that
the guards encountered in the body are satisfied.  This is called
"guard verification." Once a function has had its guards verified, then
ACL2 can evaluate the function somewhat faster (but see "Guards and
evaluation V:  efficiency issues" below).  Perhaps more importantly,
ACL2 can also guarantee that the function will be evaluated correctly
by any implementation of Common Lisp (provided the guard of the
function is satisfied on the input).  That is, if you have verified the
guards of a system of functions and you have determined that they work
as you wish in your host ACL2 (perhaps by proving it, perhaps by
testing), then they will work identically in any Common Lisp.

There is a subtlety to our treatment of evaluation of calls of
functions whose guards have been verified.  If the function's guard is
not satisfied by such a call, then no further attempt is made to
evaluate any call of that function in raw lisp during the course of
evaluation of that call.  This is obvious if guard checking is on,
because an error is signalled the first time its guard is violated; but
in fact it is also true when guard checking is off.  See
GUARD-EXAMPLE for an example.

_Guards and evaluation IV:  functions having :program mode_

Strictly speaking, functions in :program mode (see DEFUN-MODE)
do not have definitions in the ACL2 logic.  So what does it mean to
evaluate calls of such functions in ACL2?  In general we treat :program
functions much as we treat :logic functions whose guards have been
verified, except that when no error occurs then the corresponding raw
Lisp function is always called.  (We say "in general" because there are
exceptions, discussed in the "Aside" just below.)  Note that when the
guard of a function in :logic mode is violated, there is still a value
that the ACL2 logic proves is equal to the given call.  But the same
cannot be said for a function in :program mode.  Nevertheless, for the
sake of convenience we go ahead and evaluate the corresponding raw Lisp
function except in the situation where the guard is violated and
guard-checking is on, aside from the following:

*Aside*.  There are exceptions to the use of raw Lisp, discussed just
above, to evaluate calls of :program mode functions.  The primary one
is that after :set-guard-checking :none, evaluation of user-defined
:program mode function calls is done in the ACL2 logic, not in raw
Lisp.  The more obscure exception is that during expansion of macros
and make-event forms, and during evaluation of defconst forms, ACL2
enters a "safe mode" in which this escape to raw Lisp is prevented.
The following example illustrates how the user can experiment directly
with safe mode, though it is preferred to use :set-guard-checking :none
if you are happy to skip all guard checking and evaluate forms in the
logic.

     ACL2 !>(defun foo (x)
              (declare (xargs :mode :program :guard t))
              (car x))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>(foo 3)
     Error: Attempt to take the car of 3 which is not listp.
       [condition type: SIMPLE-ERROR]

     Restart actions (select using :continue):
      0: Return to Top Level (an "abort" restart).
      1: Abort entirely from this process.
     [1] ACL2(2): :pop
     ACL2 !>(assign safe-mode t)
      T
     ACL2 !>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CAR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CAR 3).  See :DOC trace for a useful debugging utility.  See
     :DOC set-guard-checking for information about suppressing this check
     with (set-guard-checking :none), as recommended for new users.

     ACL2 !>(assign safe-mode nil)
      NIL
     ACL2 !>(foo 3)
     Error: Attempt to take the car of 3 which is not listp.
       [condition type: SIMPLE-ERROR]

     Restart actions (select using :continue):
      0: Return to Top Level (an "abort" restart).
      1: Abort entirely from this process.
     [1] ACL2(2):

The other exception occurs after set-guard-checking can be called with
a value of :all; see SET-GUARD-CHECKING.  *End of aside.*

Thus, as with :logic functions:  when a guard has been satisfied on a
call of a function with :program mode, no subsidiary guard checking
will be done.

Notice that by treating functions in :program mode like functions whose
guards have been verified, we are using raw lisp to compute their
values when their guards are met.  We do not check guards any further
once raw lisp is invoked.  This can lead to hard lisp errors if the
guards are not appropriate, as illustrated below.

     ACL2 >:program
     ACL2 p>(defun foo (x)
             (declare (xargs :guard t))
             (cons 1 (cdr x)))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.02)
      FOO
     ACL2 p>(foo 3)

     Error: 3 is not of type LIST.
     Fast links are on: do (use-fast-links nil) for debugging
     Error signalled by CDR.
     Broken at COND.  Type :H for Help.
     ACL2>>

See DEFUN-MODE-CAVEAT.

However, here is a way to get ACL2 to do run-time guard checking for
user-defined :program mode functions.  With this method, ACL2 will
evaluate calls of user-defined :program mode functions in a manner that
follows their ACL2 definitions.  Simply execute the following in the
ACL2 loop to put ACL2 into a "safe mode."

     (f-put-global 'safe-mode t state)

Let us revisit the example above, using safe mode.  Notice that the
guard of cdr is now being checked, because the executable counterpart
of foo is being called even though the guard is t.

     ACL2 !>(f-put-global 'safe-mode t state)
     <state>
     ACL2 !>:program
     ACL2 p!>(defun foo (x)
               (declare (xargs :guard t))
               (cons 1 (cdr x)))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 p!>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CDR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CDR 3).  See :DOC trace for a useful debugging utility.  See
     :DOC set-guard-checking for information about suppressing this check
     with (set-guard-checking :none), as recommended for new users.

     ACL2 p!>

If we go back into "unsafe" mode, then we once again see a raw Lisp
error, as we now illustrate.

     ACL2 p!>(f-put-global 'safe-mode nil state)
     <state>
     ACL2 p!>(foo 3)

     Error: 3 is not of type LIST.
     Fast links are on: do (si::use-fast-links nil) for debugging
     Error signalled by CDR.
     Broken at COND.  Type :H for Help.
     ACL2>>

_Guards and evaluation V:  efficiency issues_

We have seen that by verifying the guards for a :logic function, we
arrange that raw lisp is used for evaluation of calls of such functions
when the arguments satisfy its guard.

This has several apparent advantages over the checking of guards as we
go.  First, the savings is magnified as your system of functions gets
deeper: the guard is checked upon the top-level entry to your system
and then raw Common Lisp does all the computing.  Second, if the raw
Common Lisp is compiled (see COMPILATION), enormous speed-ups
are possible.  Third, if your Common Lisp or its compiler does such
optimizations as tail-recursion removal, raw Common Lisp may be able to
compute your functions on input much "bigger" than ACL2 can.

The first of these advantages is quite important if you have
complicated guards.  However, the other two advantages are probably not
very important, as we now explain.

When a function is defined in :logic mode, its defun is executed in raw
Common Lisp.  (We might call this the "primary" raw lisp definition of
the function.)  However, a corresponding "logic definition" is also
executed.  The "logic definition" is a defun in raw lisp that checks
guards at runtime and escapes to the primary raw lisp definition if the
guard holds of the arguments and the function has already had its
guards verified.  Otherwise the logic definition executes the body of
the function by calling the logic definitions of each subroutine.  Now
it is true that compilation generally speeds up execution enormously.
However, the :comp command (see COMP) compiles both of the raw
lisp definitions associated with a :logic function.  Also, we have
attempted to arrange that for every tail recursion removal done on the
actual defun, a corresponding tail recursion removal is done on the
"logic definition."

We believe that in most cases, the logic definition executes almost as
fast as the primary raw lisp definition, at least if the evaluation of
the guards is fast.  So, the main advantage of guard verification is
probably that it lets you know that the function may be executed safely
in raw lisp, returning the value predicted by the ACL2 logic, whenever
its arguments satisfy its guard.  We envision the development of
systems of applicative lisp functions that have been developed and
reasoned about using ACL2 but which are intended for evaluation in raw
Common Lisp (perhaps with only a small "core" of ACL2 loaded), so this
advantage of guard verification is important.

Nevertheless, guard verification might be important for optimal
efficiency when the functions make use of type declarations.  For
example, at this writing, the GCL implementation of Common Lisp can
often take great advantage of declare forms that assign small integer
types to formal parameters.

To continue the discussion of guards, see
GUARDS-FOR-SPECIFICATION to read about the use of guards as a
specification device.

GUARDS-FOR-SPECIFICATION    guards as a specification device

A use of guard verification that has nothing to do with efficiency is
as a way to gain confidence in specifications.  This use has the feel
of "types" in many traditional programming languages, though guards
allow much greater expressiveness than most systems of types (and
unfortunately, as a result they are not syntactically checkable).

For more discussion of guards in general, see GUARD.

Suppose you have written a collection of function definitions that are
intended to specify the behavior of some system.  Perhaps certain
functions are only intended to be called on certain sorts of inputs, so
you attach guards to those functions in order to "enforce" that
requirement.  And then, you verify the guards for all those functions.

Then what have you gained, other than somewhat increased efficiency of
execution (as explained above), which quite possibly isn't your main
concern?  You have gained the confidence that when evaluating any call
of a (specification) function whose arguments satisfy that function's
guard, all subsequent function calls during the course of evaluation
will have this same property, that the arguments satisfy the guard of
the calling function.  In logical terms, we can say that the equality
of the original call with the returned value is provable from weakened
versions of the definitions, where each definitional axiom is replaced
by an implication whose antecedent is the requirement that the
arguments satisfy the guard and whose consequent is the original axiom.
For example,

     (defun foo (x)
       (declare (xargs :guard (consp x)))
       (cons 1 (cdr x)))

originally generates the axiom

     (equal (foo x)
            (cons 1 (cdr x)))

but in fact, when evaluation involves no guard violation then the
following weaker axiom suffices in the justification of the evaluation.

     (implies (consp x)
              (equal (foo x)
                     (cons 1 (cdr x))))

If you are following links to read this documentation as a hypertext
style document, then please see GUARD-MISCELLANY.  This
concludes our discussion of guards with miscellaneous remarks, and also
contains pointers to related topics.

GUARD-HINTS    xargs keyword :GUARD-HINTS

See XARGS.

HANDS-OFF    hints keyword :HANDS-OFF

See HINTS.

HIDE    hide a term from the rewriter

Hide is actually the identity function:  (hide x) = x for all x.
However, terms of the form (hide x) are ignored by the ACL2 rewriter,
except when explicit :expand hints are given for such terms (see
HINTS) or when rewrite rules explicitly about hide are available.  An
:expand hint that removes all calls of hide is:

     :expand ((:free (x) (hide x)))

The above hint can be particularly useful when ACL2's equality
heuristics apply hide to an equality after substituting it into the
rest of the goal, if that goal (or a subgoal of it) fails to be proved.

Hide terms are also ignored by the induction heuristics.

Sometimes the ACL2 simplifier inserts hide terms into a proof attempt
out of the blue, as it were.  Why and what can you do about it?
Suppose you have a constrained function, say constrained-fn, and you
define another function, say another-fn, in terms of it, as in:

     (defun another-fn (x y z)
       (if (big-hairy-test x y z)
           (constrained-fn x y z)
           t))

Suppose the term (another-fn 'a 'b 'c) arises in a proof.  Since the
arguments are all constants, ACL2 will try to reduce such a term to a
constant by executing the definition of another-fn.  However, after a
possibly extensive computation (because of big-hairy-test) the
execution fails because of the unevaluable call of constrained-fn.  To
avoid subsequent attempts to evaluate the term, ACL2 embeds it in a
hide expression, i.e., rewrites it to (hide (another-fn 'a 'b 'c)).

You might think this rarely occurs since all the arguments of
another-fn must be constants.  You would be right except for one
special case:  if another-fn takes no arguments, i.e., is a constant
function, then every call of it fits this case.  Thus, if you define a
function of no arguments in terms of a constrained function, you will
often see (another-fn) rewrite to (hide (another-fn)).

We do not hide the term if the executable counterpart of the function
is disabled - because we do not try to evaluate it in the first place.
Thus, to prevent the insertion of a hide term into the proof attempt,
you can globally disable the executable counterpart of the offending
defined function, e.g.,

     (in-theory (disable (:executable-counterpart another-fn))).

It is conceivable that you cannot afford to do this:  perhaps some
calls of the offending function must be computed while others cannot
be.  One way to handle this situation is to leave the executable
counterpart enabled, so that hide terms are introduced on the calls
that cannot be computed, but prove explicit :rewrite rules for each of
those hide terms.  For example, suppose that in the proof of some
theorem, thm, it is necessary to leave the executable counterpart of
another-fn enabled but that the call (another-fn 1 2 3) arises in the
proof and cannot be computed.  Thus the proof attempt will introduce
the term (hide (another-fn 1 2 3)).  Suppose that you can show that
(another-fn 1 2 3) is (contrained-fn 1 2 3) and that such a step is
necessary to the proof.  Unfortunately, proving the rewrite rule

     (defthm thm-helper
       (equal (another-fn 1 2 3) (constrained-fn 1 2 3)))

would not help the proof of thm because the target term is hidden
inside the hide.  However,

     (defthm thm-helper
       (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3)))

would be applied in the proof of thm and is the rule you should prove.

Now to prove thm-helper you need to use the two "tricks" which have
already been discussed.  First, to eliminate the hide term in the proof
of thm-helper you should include the hint :expand (hide (another-fn 1 2
3)).  Second, to prevent the hide term from being reintroduced when the
system tries and fails to evaluate (another-fn 1 2 3) you should
include the hint :in-theory (disable (:executable-counterpart
another-fn)).  Thus, thm-helper will actually be:

     (defthm thm-helper
       (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3))
       :hints
       (("Goal" :expand (hide (another-fn 1 2 3))
                :in-theory (disable (:executable-counterpart another-fn)))))

See EVISCERATE-HIDE-TERMS for how to affect the printing of hide
terms.

HINTS    advice to the theorem proving process

     Examples:
     The following :hints value is nonsensical.  Nevertheless, it
     illustrates all of the available hint keywords except the
     ``custom keywords'' (see CUSTOM-KEYWORD-HINTS) definable
     by the user.

     :hints (("Goal"
              :do-not-induct t
              :do-not '(generalize fertilize)
              :expand ((assoc x a)
                       :lambdas
                       (:free (y) (:with member (member y z))))
              :restrict ((<-trans ((x x) (y (foo x)))))
              :hands-off (length binary-append)
              :in-theory (set-difference-theories
                           (current-theory :here)
                           '(assoc))
              :induct (and (nth n a) (nth n b))
              :use ((:instance assoc-of-append
                               (x a) (y b) (z c))
                    (:functional-instance
                      (:instance p-f (x a) (y b))
                      (p consp)
                      (f assoc)))
              :bdd (:vars (c a0 b0 a1 b1) :prove nil :bdd-constructors (cons))
              :clause-processor (:function cl-proc :hint (my-hint clause))
              :instructions (:x :prove)
              :cases ((true-listp a) (consp a))
              :by (:instance rev-rev (x (cdr z)))
              :nonlinearp t
              :backchain-limit-rw 3
              :reorder (4 7 2)
              :case-split-limitations (20 10)
              :no-op t
              :no-thanks t
              :error ("Bad value ~x0." 123)
              :or (hint-kwd-alist-1 ... hint-kwd-alist-k)
              :rw-cache-state nil
              :backtrack (my-computed-hint clause processor clause-list)))

A very common hint is the :use hint, which in general takes as its
value a list of "lemma instances" (see LEMMA-INSTANCE) but
which allows a single lemma name as a special case:

     :hints (("[1]Subgoal *1/1.2'" :use lemma23))

ACL2 also provides "custom keyword" hints (see
CUSTOM-KEYWORD-HINTS) and even more general "computed hints" for the
advanced user (see COMPUTED-HINTS).

Only the first hint applicable to a goal, as specified in the
user-supplied list of :hints followed by the default hints (see
DEFAULT-HINTS-TABLE), will be applied to that goal.  For an advanced
exception, see OVERRIDE-HINTS.  For a detailed discussion of
how hints fit into the ACL2 waterfall, see
HINTS-AND-THE-WATERFALL.  For examples of the sophisticated use of
hints, primarily for experts, see distributed book
books/hints/basic-tests.lisp.

Background: Hints are allowed in all events that use the theorem
prover.  During defun events there are two different uses of the
theorem prover: one to prove termination and another to verify the
guards.  To pass a hint to the theorem prover during termination proofs,
use the :hints keyword in the defun's xargs declaration.  To pass a
hint to the theorem prover during the guard verification portion of
admitting a defun, use the :guard-hints keyword in the defun's xargs
declaration.  The verify-guards event and the defthm event also use the
theorem prover.  To pass hints to them, use the :hints keyword argument
to the event.

     General Form of Common :hints:
       ((goal-spec :key1 val1 ... :keyn valn)
        ...
        (goal-spec :key1 val1 ... :keyn valn))

where goal-spec is as described elsewhere (see GOAL-SPEC) and
the keys and their respective values are shown below with their
interpretations.  (We also provide "computed hints" but discuss them
separately; see COMPUTED-HINTS.)

:DO-NOT-INDUCT
Value is t, :otf-flg-override, :otf, name or nil, indicating whether
induction is permitted under the specified goal.  If value is t or
:otf-flg-override, then the attempt to apply induction to the indicated
goal or any subgoal under the indicated goal will immediately cause the
theorem prover to report failure, except that if :otf-flg is specified
(see OTF-FLG) and value is t, then the proof will continue
until the time at which the goal pushed for induction is finally
considered.  The latter behavior is also what occurs if value is :otf.
Thus, any non-nil value requires the indicated goal to be proved
entirely by simplification, destructor elimination, and the other
"waterfall" processes.  Induction to prove the indicated goal (or any
subgoal) is not permitted.  See however the :induct hint below.  If
value is a symbol other than t, :otf-flg-override, :otf or nil, the
theorem prover will give a "bye" to any subgoal that would otherwise be
attacked with induction.  This will cause the theorem prover to fail
eventually but will collect the necessary subgoals.  If value is nil,
this hint means induction is permitted.  Since that is the default,
there is no reason to use the value nil.  Note that a :do-not-induct
hint is ignored for any goal on which an :induct hint is supplied.  For
an advanced example of the use of value :otf with override-hints, see
distributed book books/hints/basic-tests.lisp.

:DO-NOT
Value is a term having at most the single free variable world, which
when evaluated (with world bound to the current ACL2 logical world)
produces a list of symbols that is a subset of the list

     (preprocess ;propositional logic, simple rules
      simplify   ;as above plus rewriting, linear arithmetic
      eliminate-destructors
      fertilize  ;use of equalities
      generalize
      eliminate-irrelevance).

The hint indicates that the "processes" named should not be used at or
below the goal in question.  Thus, to prevent generalization and
fertilization, say, include the hint

     :do-not '(generalize fertilize)

If value is a single symbol, as in

     :do-not generalize,

it is taken to be '(value).

:EXPAND
Value is a true list of terms, each of which is of one of the forms
(let ((v1 t1)...) b) or (fn t1 ... tn), where fn is a defined function
symbol with formals v1, ..., vn, and body b.  Such a term is said to be
"expandable:" it can be replaced by the result of substituting the ti's
for the vi's in b.  The terms listed in the :expand hint are expanded
when they are encountered by the simplifier while working on the
specified goal or any of its subgoals.  We permit value to be a single
such term instead of a singleton list.  *Remarks*: (1) Allowed are
"terms" of the form (:free (var1 var2 ...  varn) pattern) where the
indicated variables are distinct and pattern is a term.  Such "terms"
indicate that we consider the indicated variables to be instantiatable,
in the following sense: whenever the simplifier encounters a term that
can be obtained from pattern by instantiating the variables (var1 var2
...  varn), then it expands that term.  (2) Also allowed are "terms" of
the form (:with name term), where name is a function symbol, a macro
name that denotes a function symbol (see MACRO-ALIASES-TABLE),
or a rune.  The corresponding rule of class :rewrite, which is often a
definition rule but need not be, is then used in place of the current
body for the function symbol of term; see SHOW-BODIES and see
SET-BODY.  If the rule is of the form (implies hyp (equiv lhs
rhs)), then after matching lhs to the current term in a context that is
maintaining equivalence relation equiv, ACL2 will replace the current
term with (if hyp rhs (hide term)), or just rhs if the rule is just
(equal lhs rhs).  (3) A combination of both :free and :with, as
described above, is legal.  (4) The term :LAMBDAS is treated specially.
It denotes the list of all lambda applications (i.e., let expressions)
encountered during the proof.  Conceptually, this use of :LAMBDAS tells
ACL2 to treat lambda applications as a notation for substitutions,
rather than as function calls whose opening is subject to the ACL2
rewriter's heuristics (specifically, not allowing lambda applications
to open when they introduce "too many" if terms).

:HANDS-OFF
Value is a true list of function symbols or lambda expressions,
indicating that under the specified goal applications of these
functions are not to be rewritten.  Note however that subterms will
still be rewritten; see HIDE if that is not what is intended.
(The distributed book books/clause-processors/autohide.lisp from Jared
Davis may also be helpful in that case.) Value may also be a single
function symbol or lambda expression instead of a list.

:IN-THEORY
Value is a "theory expression," i.e., a term having at most the single
free variable world which when evaluated (with world bound to the
current ACL2 logical world (see WORLD)) will produce a theory
to use as the current theory for the goal specified.  See
THEORIES.

Note that an :IN-THEORY hint will always be evaluated relative to the
current ACL2 logical world, not relative to the theory of a previous
goal.  Consider the following example.

     (defthm prop
       (p (f (g x)))
       :hints (("Goal"      :in-theory (disable f))
               ("Subgoal 3" :in-theory (enable  g))))

Consider in particular the theory in effect at Subgoal 3.  This call of
the enable macro enables g relative to the current-theory of the
current logical world, _not_ relative to the theory produced by the
hint at Goal.  Thus, the disable of f on behalf of the hint at Goal
will be lost at Subgoal 3, and f will be enabled at Subgoal 3 if was
enabled globally when prop was submitted.

:INDUCT
Value is either t or a term containing at least one recursively defined
function symbol; if t, this hint indicates that the system should
proceed to apply its induction heuristic to the specified goal produced
(without trying simplification, etc.); if value is a term other than t,
then not only should the system apply induction immediately, but it
should analyze value rather than the goal to generate its induction
scheme.  Merging and the other induction heuristics are applied.  Thus,
if value contains several mergeable inductions, the "best" will be
created and chosen.  E.g., the :induct hint

      (and (nth i a) (nth j a))

suggests simultaneous induction on i, j, and a.

If both an :induct and a :do-not-induct hint are supplied for a given
goal then the indicated induction is applied to the goal and the
:do-not-induct hint is inherited by all subgoals generated.

:USE
Value is a lemma-instance or a true list of lemma-instances, indicating
that the propositions denoted by the instances be added as hypotheses
to the specified goal.  See LEMMA-INSTANCE.  Note that :use
makes the given instances available as ordinary hypotheses of the
formula to be proved.  The :instance form of a lemma-instance permits
you to instantiate the free variables of previously proved theorems any
way you wish; but it is up to you to provide the appropriate
instantiations because once the instances are added as hypotheses their
variables are no longer instantiable.  These new hypotheses participate
fully in all subsequent rewriting, etc.  If the goal in question is in
fact an instance of a previously proved theorem, you may wish to use
:by below.  Note that theories may be helpful when employing :use
hints; see MINIMAL-THEORY.

Note that if the value is the name of a function symbol introduced by
defun, then the "normalized" body of that definition is used, for which
ACL2 has propagated IF tests upward.  This behavior differs from that
provided by a :by hint, where the original body of the definition is
used.

:BDD
This hint indicates that ordered binary decision diagrams (BDDs) with
rewriting are to be used to prove or simplify the goal.  See
BDD for an introduction to the ACL2 BDD algorithm.

Value is a list of even length, such that every other element, starting
with the first, is one of the keywords :vars, :bdd-constructors,
:prove, or :literal.  Each keyword that is supplied should be followed
by a value of the appropriate form, as shown below; for others, a
default is used.  Although :vars must always be supplied, we expect
that most users will be content with the defaults used for the other
values.

:vars -- A list of ACL2 variables, which are to be treated as Boolean
variables.  The prover must be able to check, using trivial reasoning
(see TYPE-SET), that each of these variables is Boolean in the
context of the current goal.  Note that the prover will use very simple
heuristics to order any variables that do not occur in :vars (so that
they are "greater than" the variables that do occur in :vars), and
these heuristics are often far from optimal.  In addition, any
variables not listed may fail to be assumed Boolean by the prover,
which is likely to seriously impede the effectiveness of ACL2's BDD
algorithm.  Thus, users are encouraged _not_ to rely on the default
order, but to supply a list of variables instead.  Finally, it is
allowed to use a value of t for vars.  This means the same as a nil
value, except that the BDD algorithm is directed to fail unless it can
guarantee that all variables in the input term are known to be Boolean
(in a sense discussed elsewhere; see BDD-ALGORITHM).

:literal -- An indication of which part of the current goal should
receive BDD processing.  Possible values are:

       :all     treat entire goal as a single literal (the default)
       :conc    process the conclusion
       n        process the hypothesis with index n (1, 2, ...)

:bdd-constructors -- When supplied, this value should be a list of
function symbols in the current ACL2 world; it is (cons) by default,
unless :bdd-constructors has a value in the acl2-defaults-table by
default, in which case that value is the default.  We expect that most
users will be content with the default.  See BDD-ALGORITHM for
information about how this value is used.

:prove -- When supplied, this value should be t or nil; it is t by
default.  When the goal is not proved and this value is t, the entire
proof will abort.  Use the value nil if you are happy to the proof to
go on with the simplified term.

:CLAUSE-PROCESSOR

Value specifies the application of a user-defined simplifier to the
current goal.  See CLAUSE-PROCESSOR, which provides necessary
background and hint syntax.  Also see
DEFINE-TRUSTED-CLAUSE-PROCESSOR for a discussion of "trusted
clause-processors":  goal-level simplifiers that may be external to
ACL2 and do not need to be proved correct in ACL2.

You can see all current :clause-processor rules by issuing the command
(print-clause-processor-rules), and you can see the names of all trusted
clause-processors by issuing the command (table
trusted-clause-processor-table).

:INSTRUCTIONS

Value is a list of proof-checker instructions; see INSTRUCTIONS.
Unlike other hint keywords described here, this one is actually a custom
keyword hint (see CUSTOM-KEYWORD-HINTS) that generates a
suitable :clause-processor hint.

:CASES
Value is a non-empty list of terms.  For each term in the list, a new
goal is created from the current goal by assuming that term; and also,
in essence, one additional new goal is created by assuming all the
terms in the list false.  We say "in essence" because if the
disjunction of the terms supplied is a tautology, then that final goal
will be a tautology and hence will in fact never actually be created.

:BY
Value is a lemma-instance, nil, or a new event name. If the value is a
lemma-instance (see LEMMA-INSTANCE), then it indicates that the
goal (when viewed as a clause) is either equal to the proposition
denoted by the instance, or is subsumed by that proposition when both
are viewed as clauses.  To view a formula as a clause, union together
the negations of the hypotheses and add the conclusion.  For example,

     (IMPLIES (AND (h1 t1) (h2 t2)) (c t1))

may be viewed as the clause

     {~(h1 t1) ~(h2 t2) (c t1)}.

Clause c1 is "subsumed" by clause c2 iff some instance of c2 is a
subset of c1.  For example, the clause above is subsumed by {~(h1 x) (c
x)}, which when viewed as a formula is (implies (h1 x) (c x)).

Note that if the value is the name of a function symbol introduced by
defun, then the original form of the body of that definition is used.
This behavior differs from that provided by a :use hint, where the
so-called "normalized" body, for which ACL2 has propagated IF tests
upward.

If the value is nil or a new name, the prover does not even attempt to
prove the goal to which this hint is attached.  Instead the goal is
given a "bye", i.e., it is skipped and the proof attempt continues as
though the goal had been proved.  If the prover terminates without
error then it reports that the proof would have succeeded had the
indicated goals been proved and it prints an appropriate defthm form to
define each of the :by names.  The "name" nil means "make up a name."
Here is an example (admittedly contrived for illustration purposes).

     ACL2 !>(thm (equal (append (append x y) z)
                        (append x y z))
                 :hints (("Subgoal *1/2'" :by nil)))

     Name the formula above *1.

     [[... output omitted here ...]]

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

     Subgoal *1/2'
     (IMPLIES (AND (CONSP X)
                   (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                          (APPEND (CDR X) Y Z)))
              (EQUAL (APPEND (APPEND X Y) Z)
                     (APPEND X Y Z))).

     But we have been asked to pretend that this goal is subsumed by the
     yet-to-be-proved |THM Subgoal *1/2'|.

     Subgoal *1/1
     [[... proof goes on; further output omitted here ...]]

The system does not attempt to check the uniqueness of the :by names
(supplied or made up), since by the time those goals are proved the
namespace will be cluttered still further.  Therefore, the final list
of "appropriate" defthm forms may be impossible to admit without some
renaming by the user.  If you must invent new names, remember to
substitute the new ones for the old ones in the :by hints themselves.

:RESTRICT
Warning: This is a sophisticated hint, suggested by Bishop Brock, that
is intended for advanced users.  In particular, :restrict hints are
ignored by the preprocessor, so you might find it useful to give the
hint :do-not '(preprocess) when using any :restrict hints, at least if
the rules in question are abbreviations (see SIMPLE).

Value is an association list.  Its members are of the form (x subst1
subst2 ...), where: x is either (1) a rune whose car is :rewrite or
:definition or (2) an event name corresponding to one or more such
runes; and (subst1 subst2 ...) is a non-empty list of substitutions,
i.e., of association lists pairing variables with terms.  First
consider the case that x is a :rewrite or :definition rune.  Recall
that without this hint, the rule named x is used by matching its
left-hand side (call it lhs) against the term currently being
considered by the rewriter, that is, by attempting to find a
substitution s such that the instantiation of lhs using s is equal to
that term.  If however the :restrict hint contains (x subst1 subst2
...), then this behavior will be modified by restricting s so that it
must extend subst1; and if there is no such s, then s is restricted so
that it must extend subst2; and so on, until the list of substitutions
is exhausted.  If no such s is found, then the rewrite or definition
rule named x is not applied to that term.  Finally, if x is an event
name corresponding to one or more :rewrite or :definition runes (that
is, x is the "base symbol" of such runes; see RUNE), say runes
r1, ... rn, then the meaning is the same except that (x subst1 subst2
...) is replaced by (ri subst1 subst2 ...) for each i.  Once this
replacement is complete, the hint may not contain two members whose car
is the same rune.

Note that the substitutions in :restrict hints refer to the variables
actually appearing in the goals, not to the variables appearing in the
rule being restricted.

Here is an example, supplied by Bishop Brock.  Suppose that the
database includes the following rewrite rule, which is probably kept
disabled.  (We ignore the question of how to prove this rule.)

     cancel-<-*$free:
     (implies (and (rationalp x)
                   (rationalp y)
                   (rationalp z))
              (equal (< y z)
                     (if (< x 0)
                         (> (* x y) (* x z))
                       (if (> x 0)
                           (< (* x y) (* x z))
                         (hide (< y z))))))

Then ACL2 can prove the following theorem (unless other rules get in
the way), essentially by multiplying both sides by x.

     (thm
       (implies (and (rationalp x)
                     (< 1 x))
                (< (/ x) 1))
       :hints
       (("Goal"
         :in-theory (enable cancel-<-*$free)
         :restrict ((cancel-<-*$free ((x x) (y (/ x)) (z 1)))))))

The :restrict hint above says that the variables x, y, and z in the
rewrite rule cancel-<-*$free above should be instantiated respectively
by x, (/ x), and 1.  Thus (< y z) becomes (< (/ x) 1), and this
inequality is replaced by the corresponding instance of the
right-hand-side of cancel-<-*$free.  Since the current conjecture
assumes (< 1 x), that instance of the right-hand side simplifies to

     (< (* x (/ x)) (* x 1))

which in turn simplifies to (< 1 x), a hypothesis in the present
theorem.

:NONLINEARP
Value is t or nil, indicating whether non-linear-arithmetic is active.
The default value is nil.  See NON-LINEAR-ARITHMETIC.

:BACKCHAIN-LIMIT-RW
Value is a natural number or nil, indicating the level of backchaining
for rewrite, meta, and linear rules.  This overrides, for the current
goal and (as with :in-theory hints) descendent goals, the default
backchain-limit (see SET-BACKCHAIN-LIMIT).

:REORDER
Value is a list of positive integers without duplicates, corresponding
to the numbering of subgoals generated for the goal-spec, say "G.k"
down to "G.1".  Those subgoals are reordered so that if value is (n1 n2
... nk), then the goal now numbered "G.k" will be the goal originally
numbered "G.n1"; the goal now numbered "G.k-1" will be the goal
formerly numbered "G.n2"; and so on, down the list of ni, after which
the goals not yet printed are printed in their original order.

:CASE-SPLIT-LIMITATIONS
Value is the same as for set-case-split-limitations.  The simplifier
will behave as though the value had instead been supplied to
set-case-split-limitations; see SET-CASE-SPLIT-LIMITATIONS.
This behavior will persist through subgoals unless overridden by another
:CASE-SPLIT-LIMITATIONS hint.

:NO-OP
Value is any object and is irrelevant.  This hint does nothing.  But
empty hints, such as ("Goal"), are illegal and there are occasions,
especially when writing custom keyword hints (see
CUSTOM-KEYWORD-HINTS) and computed hints (see COMPUTED-HINTS)
where it is convenient to be able to generate a non-empty no-op hint.
The standard idiom is ("Goal" :NO-OP T) but the T is completely
ignored.  Unlike other hint keywords, multiple occurrences of the
keyword :NO-OP are tolerated.

:NO-THANKS
Value is any object.  This hint does nothing, except that if value is
non-nil then the usual "[Note:  A hint was supplied... Thanks!]" is not
printed.

:ERROR
Value is typically a "fmt message" to be printed by the fmt
tilde-directive ~@ but may be any object.  The effect of this hint is
to cause an error when the hint is translated.  There is no reason to
include an :ERROR hint in any user-typein, since it will only cause an
error when the form is evaluated.  :ERROR hints are useful in the
definition of functions that generate custom keyword hints
(custom-keyword-hints) and computed hints (computed-hints).  For
example, if you wish to define a custom keyword hint :my-hint val and
you wish the hint to signal an error if there is something
inappropriate about val in the context of the hint, use the following
code to generate the hint

     (list :ERROR (cons "Your specified value, ~x0, is inappropriate"
                        (list (cons #0 val))))

which is equivalent to

     (list :ERROR (msg "Your specified value, ~x0, is inappropriate"
                       val))

which, if val has the value 123, would evaluate to the hint

     (:ERROR ("Your specified value, ~x0, is inappropriate" (#0 . 123))).

Note that any time an :ERROR keyword is produced during hint processing,
including iterations of the expansions of custom keyword hints or of
override-hints, an error will occur.

:OR
Value is a list (kwd-val-listp-1 ... kwd-val-listp-k), where each
kwd-val-listp-i is a list satisfying keyword-value-listp, i.e., an
alternating list of keywords and values.  This hint causes an attempt to
prove the specified goal using hints kwd-val-listp-1 in turn, until the
first of these succeeds.  If none succeeds, then the prover proceeds
after heuristically choosing the "best" result, taking into account the
goals pushed in each case for proof by induction.

The following (contrived but illustrative example illustrates how :or
hints work.

       ACL2 !>(thm (f x)
                   :hints
                   (("Goal"
                     :expand ((nth x 3))
                     :or ((:in-theory (disable car-cons))
                          (:use cdr-cons :in-theory (enable append)))
                     :do-not '(generalize))))

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

       The :OR hint for Goal gives rise to two disjunctive branches.  Proving
       any one of these branches would suffice to prove Goal.  We explore
       them in turn, describing their derivations as we go.

       ---
       Subgoal D2
       ( same formula as Goal ).

       The first disjunctive branch (of 2) for Goal can be created by applying
       the hint:
       ("Subgoal D2" :EXPAND ((NTH X 3))
                     :IN-THEORY (DISABLE CAR-CONS)
                     :DO-NOT '(GENERALIZE)).

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

       Normally we would attempt to prove this formula by induction.  However,
       we prefer in this instance to focus on the original input conjecture
       rather than this simplified special case.  We therefore abandon our
       previous work on this conjecture and reassign the name *1 to the original
       conjecture.  (See :DOC otf-flg.)  [Note:  Thanks again for the hint.]

       ---
       Subgoal D1
       ( same formula as Goal ).

       The second disjunctive branch (of 2) for Goal can be created by applying
       the hint:
       ("Subgoal D1" :EXPAND ((NTH X 3))
                     :USE CDR-CONS
                     :IN-THEORY (ENABLE APPEND)
                     :DO-NOT '(GENERALIZE)).

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

       ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE an enabled
       :REWRITE or :DEFINITION rule, so you may want to consider disabling
       (:REWRITE CDR-CONS).

       We augment the goal with the hypothesis provided by the :USE hint.
       The hypothesis can be obtained from CDR-CONS.  We are left with the
       following subgoal.

       Subgoal D1'
       (IMPLIES (EQUAL (CDR (CONS X Y)) Y)
                (F X)).

       By the simple :rewrite rule CDR-CONS we reduce the conjecture to

       Subgoal D1''
       (F X).

... and so on.  This example illustrates how ACL2 processes :or hints in
general.  For each i from 1 to k, a so-called "disjunctive" subgoal is
created by splicing kwd-val-listp-i into the other hint values (if any)
supplied for the given goal, in order.  A corresponding subgoal is
created for each i, numbered in the usual manner (hence, counting down)
except that the "D" is prefixed to each resulting goal.

:RW-CACHE-STATE
Value is an element of the list constant *legal-rw-cache-states*: :atom
(the default), nil, t, or :disabled.  This hint applies to the
indicated goal and all its descendents, to set the so-called
"rw-cache-state" to the indicated value; see SET-RW-CACHE-STATE.

:BACKTRACK
This is an advanced hint.  You can probably accomplish its effect by
the use of ordinary computed hints; see COMPUTED-HINTS.  But if
you are an expert, read on.  (See HINTS-AND-THE-WATERFALL for
some relevant background.)

Value is a computed hint, which is an expression that evaluates either
to nil -- indicating that the :backtrack hint is to have no effect --
or to a non-empty alternating list of :keyi :vali pairs, as expected
for a hint.  However, unlike ordinary computed hints, :backtrack hints
are evaluated *after* a goal has been processed to yield zero or more
subgoals, not before.  Moreover, variables PROCESSOR and CLAUSE-LIST
are allowed, but variable STABLE-UNDER-SIMPLIFICATIONP is not.  We
explain in more detail below, but first consider the following simple
example.  First we define a standard list reversal function:

     (defun rev (x)
       (if (consp x)
           (append (rev (cdr x)) (cons (car x) nil))
         nil))

Now we prove:

     (thm (true-listp (rev x)))

The successful proof includes the following output.

     Subgoal *1/1'
     (IMPLIES
       (AND (CONSP X)
            (TRUE-LISTP (REV (CDR X))))
       (TRUE-LISTP (APPEND (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 (APPEND (REV X2) (LIST X1)))).

But suppose that we attach a :backtrack hint to the goal above at which
destructor elimination was applied:

     (thm (true-listp (rev x))
          :hints (("Subgoal *1/1'"
                   :backtrack
                   (quote (:do-not '(eliminate-destructors))))))

Then when ACL2 applies destructor elimination as displayed above, this
time the :backtrack hint applies, evaluating to (:do-not
'(eliminate-destructors)).  Since this list is not nil, the prover
decides not to keep the new subgoal, and instead supplies this :do-not
hint before attacking the goal again.  In this example, ACL2 happens to
use a technique later in its "waterfall" arsenal than destructor
elimination, namely, generalization:

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

     [Note:  A hint was supplied for our processing
     of the goal above, because of a :backtrack hint
     that is preventing destructor elimination.
     Thanks!]

     We generalize this conjecture, replacing
     (REV (CDR X)) by RV.  This produces

     Subgoal *1/1''
     (IMPLIES (AND (CONSP X) (TRUE-LISTP RV))
              (TRUE-LISTP (APPEND RV (LIST (CAR X))))).

We now provide a careful explanation of how :backtrack hints work, but
we suggest that you keep the example above in mind.  If ":backtrack
form" is part of the hint that has been selected for a goal, then form
is evaluated when one of ACL2's clause processors successfully applies
to the current goal to produce a list of subgoals.  This evaluation
takes place in an environment just like that for any computed hint (see
COMPUTED-HINTS), with the following exceptions.  First, the
variable STABLE-UNDER-SIMPLIFICATIONP is not allowed to occur free in
form, but instead the following new variables are allowed to occur free
and are bound for this evaluation as follows: PROCESSOR is bound to the
processor in the list *preprocess-clause-ledge* that has applied to the
goal, and CLAUSE-LIST is bound to the list of clauses (each a list of
literals that is implicitly disjoined) returned by that clause
processor.  Second, the variables HIST and PSPV are bound to the
history and pspv returned by the clause processor, *not* the ones that
were passed to the clause processor.  If this evaluation returns an
error, then the proof aborts, as for any computed hint whose evaluation
returns an error.  If this evaluation returns nil, then the :backtrack
hint has no effect, and the goal is replaced by the list of goals (the
value of CLAUSE-LIST described above), as usual.  Otherwise, the clause
processor is deemed to have failed, and the goal clause is tried again
after applying the hint returned by the above evaluation.  That hint
will normally be an alternating list of hint keywords and their values,
but if it is a custom keyword hint (see CUSTOM-KEYWORD-HINTS),
then it will be handled in the usual manner but with the first three
variables above bound to the symbol :OMITTED.  Of course, if the new
hint includes a value for :BACKTRACK then this process can loop; care
should be taken to keep that from happening.

A final note about :BACKTRACK hints: override-hints (if any) are
applied in their processing.  See OVERRIDE-HINTS.

HINTS-AND-THE-WATERFALL    how hints fit into the ACL2 proof waterfall

Below we describe the flow of an ACL2 proof attempt, with special
attention to how hints are applied during a proof.  For most ACL2
users, only one point is important to take away from this documentation
topic: you may specify hints during a proof (see HINTS; perhaps
also see COMPUTED-HINTS and see DEFAULT-HINTS), and
they can be expected to behave intuitively.  See THE-METHOD for
a summary of how to interact with the ACL2 prover; see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed tutorial; and
see HINTS for an introduction to ACL2 hints, including detailed
documentation for specific hint types.

The remainder of this topic serves as a references in case one needs a
deeper understanding of the workings of ACL2's handling of hints.
Also, for examples of the sophisticated use of hints, primarily for
experts, see distributed book books/hints/basic-tests.lisp.

First, we describe the ACL2 "waterfall", which handles each goal either
by replacing it with a list (possibly empty) of child goals, or else by
putting the goal into a "pool" for later proof by induction.  Then, we
describe how hints are handled by the waterfall.

*The Waterfall.*

Each goal considered by the ACL2 prover passes through a series of proof
processes, called the "waterfall processes", as stored in the constant
*preprocess-clause-ledge*.  The top process applies top-level hints,
including :use hints; the next is a lightweight "preprocess" simplifier
for "simple" rules (see SIMPLE); the next is the main ACL2
simplifier; and finally ACL2 attempts (in this order) destructor
elimination, fertilization (heuristic use of equalities),
generalization, and elimination of irrelevance.  Each process may
"hit", creating zero or more child goals that are each then handled at
the top of the waterfall; or it may "miss", in which case the next
process in the above sequence is considered.  If all processes miss,
then a "push" process defers the goal until it is later considered for
proof by induction.  When all goals have been thus handled, the goal
most recently pushed for proof by induction is considered, and the
process repeats.

We next describe the two additional ways in which control can be
returned to the top of the waterfall.

When the simplification process is attempted unsuccessfully for a goal,
the goal is deemed to have "settled down".  In this case, and if no
ancestor of the goal has settled down, then the "settled-down" process
is deemed to have "hit" on the goal, the effect being that the goal
makes a new pass through all the waterfall processes.  (Other processes
can then notice that settling down has occurred and modify their
heuristics accordingly.)  For example, if "Goal" simplifies to "Subgoal
2" (among others), and "Subgoal 2" simplifies to "Subgoal 2.3" (among
others), which in turn is not further simplified, then the the
"settled-down" process hits on "Subgoal 2.3" but not on any of its
children, their children, and so on.

When simplification has missed (and thus the goal has settled down),
the next proof process is normally destructor elimination.  However, if
a computed hint is suitable (in a sense described below; also see
COMPUTED-HINTS, especially the discussion of
stable-under-simplificationp), then that hint is selected as control is
returned to the top of the waterfall.  A subtlety is that in this case,
if the most recent hit had been from settling down, then the prover
"changes its mind" and considers that the goal has not yet settled down
after all as it continues through the waterfall.

Each time a goal is considered at the top of the waterfall, then before
passing through the proof processes as described above, ACL2 searches
for a relevant hint to select unless it has already been provided a
hint in the "stable-under-simplificationp" case mentioned above.  We
turn now to a more thorough discussion of how hints are selected and
applied.

*The handling of hints.*

In the discussion below we will ignore forcing rounds, as each forcing
round is simply treated as a new proof attempt that uses the list of
hints provided at the start of the proof.

When the theorem prover is called by thm or events such as defthm,
defun, and verify-guards, it gathers up the hints that have been
supplied, often provided as a :hints argument, but for example using a
:guard-hints argument for guard verification proofs.  (ACL2(r) users
(see REAL) may also employ :std-hints.)  It then appends these
to the front of the list of default hints (see DEFAULT-HINTS).
The resulting list becomes the initial value of the list of "pending
hints", one of two critical lists maintained by the theorem prover to
manage hints.  The other critical list is a list of "hint settings";
the two lists are maintained as follows.

When a goal is first considered, a hint is selected from the list of
pending hints if any is found to apply, as described below.  If a hint
is selected, then it takes effect and is removed from the pending
hints.  Except: if the selected hint is a computed hint with value t
specified for :computed-hint-replacement, then it is not removed; and
if that value is a list of hints, then that list is appended to the
front of the list of pending hints after the selected hint is removed
(also see COMPUTED-HINTS).  The selected hint is also used to
update the hint settings, as described below.

The list of hint settings associates hint keywords with values.  It is
passed from the current goal to its children (and hence the children's
children, and so on), though modified by hints selected from pending
hints, as described below.  This list is consulted when a goal is
pushed for later proof by induction, at which time the hint settings
are stored so that when the induction proof begins, it begins with
those hint settings.  Note that the list of hint settings is not
re-applied to descendents of a goal; a hint is applied only when it is
selected.  For example, if the hint selected for "Subgoal 3" includes
:in-theory (enable foo), then the hint settings are correspondingly
updated when processing "Subgoal 3", and they persist at subgoals such
as "Subgoal 3.2" and "Subgoal 3.2.1" (unless overriden by hints on
those goals); but the theory specifying foo is not re-installed at
every such subgoal.

When a hint is selected, the list of hint-settings is updated so that
for each keyword :kwd and associated value val from the hint, :kwd is
associated with val in the hint-settings, discarding any previous
association of :kwd with a value in the hint-settings.  Except, certain
"top-level" hints are never saved in the hint-settings: :use, :cases,
:by, :bdd, :or, and :clause-processor.

For example, suppose that we specify the following hints, with no
default hints.

     (("Goal" :expand ((bar x y)))
      ("Subgoal 3" :in-theory (enable foo)))

These hints then become the initial list of pending hints.  When the
proof attempt begins, the prover encounters the top-level goal ("Goal")
and pulls the "Goal" hint from the pending hints, so that the list of
hint settings contains a value only for keyword :expand.  This hint
setting will remain for all children of the top-level goal as well, and
their children, and so on, and will be inherited by induction -- in
other words, it will remain throughout the entire proof.  Now consider
what happens when the proof reaches "Subgoal 3".  At this point there
is only one pending hint, which is in fact attached to that subgoal.
Therefore, this hint is pulled from the pending hints (leaving that
list empty), and the hint settings are extended by associating the
:in-theory keyword with the theory represented by (enable foo).  That
theory is immediately installed until the prover finishes addressing
"Subgoal 3", its children, their children, and so on; and until that
completion is reached, the :in-theory keyword remains associated with
the (enable foo) in the hint settings, although of course there is no
re-installation of the theory at any ensuing child goal.  When finally
"Subgoal 3" and its descendents have been completed and the prover is
about to consider "Subgoal 2", the :in-theory association is removed
from the hint settings and the global theory is re-installed.  However,
the list of pending hints remains empty.

It remains to describe how hints are chosen for a goal.  When a goal is
first considered (hence at the top of the waterfall), the list of
pending hints is scanned, in order, until one of the hints is suitable
for the goal.  An explicit hint (goal-name :kwd1 val1 ... :kwdn valn)
is suitable if goal-name is the name of the current goal and there is
at least one keyword.  A computed hint is suitable if it evaluates to a
non-nil value.  As indicated earlier in this documentation topic, an
exception occurs when a computed hint is selected after simplification
fails (the "stable-under-simplificationp" case): in that case, the goal
returns to the top of the waterfall with that hint is the selected
hint, and no additional search for a hint to select is made at that
time.

The following slightly tricky example illustrates handling of hints.

     ACL2 !>(set-default-hints '(("Goal" :do-not '(preprocess))))
      (("Goal" :DO-NOT '(PREPROCESS)))
     ACL2 !>(thm (equal (append (append x y) z) (append x y z))
                 :hints (("Goal" :in-theory (disable car-cons))))

     ACL2 Warning [Hints] in ( THM ...):  The goal-spec "Goal" is explicitly
     associated with more than one hint.  All but the first of these hints
     may be ignored.  If you intended to give all of these hints, combine
     them into a single hint of the form ("Goal" :kwd1 val1 :kwd2 val2 ...).
     See :DOC hints-and-the-waterfall.

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

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

     Name the formula above *1.

The warning above is printed because "Goal" is associated with two
hints: one given by the set-default-hints call and one supplied by the
:hints keyword of the thm form.  The :in-theory hint is selected
because user-supplied hints are ahead of default hints in the list of
hints to consider; we then get the first "Note" above.  The goal
progresses through the waterfall without any proof process applying to
the goal; in particular, it cannot be further simplified.  After the
simplification process, a "settled-down" process applies, as discussed
above, immediately causing another trip through the waterfall.  At that
point the :in-theory hint had previously been removed when it was
applied, leaving the default (:do-not) hint as the only applicable
hint.  That hint is indeed applied, resulting in the second "Note"
above.

Again, more examples may be found in the distributed book
books/hints/basic-tests.lisp.  A particularly tricky but informative
example in that book is the one related to nonlinearp-default-hint.

Also see OVERRIDE-HINTS for an advanced feature that allows
modification of the hint selected for a goal.

I-AM-HERE    a convenient marker for use with rebuild

     Example Input File for Rebuild:
     (defun fn1 (x y) ...)
     (defthm lemma1 ...)
     (defthm lemma2 ...)
     (i-am-here)
     The following lemma won't go through.  I started
     typing the hint but realized I need to prove a
     lemma first.  See the failed proof attempt in foo.bar.
     I'm going to quit for the night now and resume tomorrow
     from home.

     (defthm lemma3 ...
       :hints (("Goal" :use (:instance ???
     ...

By putting an (i-am-here) form at the "frontier" of an evolving file of
commands, you can use rebuild to load the file up to the (i-am-here).
I-am-here simply returns an ld error triple and any form that "causes
an error" will do the same job.  Note that the text of the file after
the (i-am-here) need not be machine readable.

IMMEDIATE-FORCE-MODEP    when executable counterpart is enabled,
 forced hypotheses are attacked immediately

Also see DISABLE-IMMEDIATE-FORCE-MODEP and see
ENABLE-IMMEDIATE-FORCE-MODEP.

This function symbol is defined simply to provide a rune which can be
enabled and disabled.  Enabling

     (:executable-counterpart immediate-force-modep)

causes ACL2 to attack forced hypotheses immediately instead of delaying
them to the next forcing round.

     Example Hints
     :in-theory (disable (:executable-counterpart immediate-force-modep))
                ; delay forced hyps to forcing round
     :in-theory (enable (:executable-counterpart immediate-force-modep))
                ; split on forced hyps immediately

See FORCE for background information.  When a forced hypothesis
cannot be established a record is made of that fact and the proof
continues.  When the proof succeeds a "forcing round" is undertaken in
which the system attempts to prove each of the forced hypotheses
explicitly.  However, if the rune (:executable-counterpart
immediate-force-modep) is enabled at the time the hypothesis is forced,
then ACL2 does not delay the attempt to prove that hypothesis but
undertakes the attempt more or less immediately.

INDUCT    hints keyword :INDUCT

See HINTS.

KEYWORD    See KEYWORDP.

KEYWORD-COMMANDS    how keyword commands are processed

     Examples:
     user type-in                 form evaluated
     :pc 5                        (ACL2::PC '5)
     :pcs app rev                 (ACL2::PCS 'app 'rev)
     :length (1 2 3)              (ACL2::LENGTH '(1 2 3))
     :quit                        (ACL2::QUIT) ; Note: avoid optional argument

When a keyword, :key, is read as a command, ACL2 determines whether the
symbol with the same name in the "ACL2" package, acl2::key, is a
function or simple macro of n arguments.  If so, ACL2 reads n more
objects, obj1, ..., objn, and then acts as though it had read the
following form (for a given key):

     (ACL2::key 'obj1 ... 'objn)

Thus, by using the keyword command hack you avoid typing the
parentheses, the "ACL2" package name, and the quotation marks.

See LD-KEYWORD-ALIASES for how to customize this behavior.

Note the generality of this hack.  Any function or macro in the "ACL2"
package can be so invoked, not just "commands."  Indeed, there is no
such thing as a distinguished class of commands.  Users may take
advantage of the keyword command hack by defining functions and macros
in the "ACL2" package.

The one caveat is that when the keyword hack is used to invoke a macro,
only the required arguments for that macro are read before calling that
macro: none of the &optional, &rest, &body, or &key arguments are read
for that call.  The macro is thus called with only its required
arguments.  The following log illustrates this caveat.

     ACL2 !>:set-iprint t

     ACL2 Query (:SET-IPRINT):  Action  (T, NIL, RESET, RESET-ENABLE, SAME,
     Q or ?):
     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>

What happened?  First, the command :set-iprint was read.  Since the
macro set-iprint has no required arguments, the ACL2 evaluator was then
called on the form (set-iprint), that is, calling the macro on no
arguments.  Set-iprint is defined to query the ACL2 user when its first
argument is omitted.  The log shows that query, which is set up to read
the next form from the input stream.  That form was available
immediately: the form t that had been supplied by the user.  So the
query returned immediately and the set-iprint call was completed.

LAMBDA    See TERM.