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

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 the current list of the negations of the
backchaining hypotheses being pursued.  In particular, (null
(mfc-ancestors mfc)) will be true if and only if the term being
rewritten is part of the current goal; otherwise, that term is part of a
hypothesis from a rule currently being considered for use.  Exception:
An ancestor 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)) that binds 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.  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, see REDO-FLAT.

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 underlying 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
     GCL                    si::gbc
     CLISP                  ext:gc
     CMU Common Lisp        system::gc
     SBCL                   sb-ext:gc
     Macintosh Common Lisp  ccl::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))))

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.

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.

(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))
              :cases ((true-listp a) (consp a))
              :by (:instance rev-rev (x (cdr z)))
              :nonlinearp t
              :reorder (4 7 2)
              :no-op t
              :no-thanks t
              :error ("Bad value ~x0." 123)
              :or (hint-kwd-alist-1 ... hint-kwd-alist-k)
              :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.  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).

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

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.

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

: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-typin, 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.

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

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 turn now to a careful explanation of how :backtrack hints work, but
we suggest that you keep the example above in mind.  When :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 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 above three
variables 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, and see
HINTS for an introduction to ACL2 hints and 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 at 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, before pushing a goal
for later proof by induction if none of these proof processes applies
to the goal.  When all goals have been thus handled, the goal most
recently pushed for proof by induction is considered, and the process
repeats.

When the simplification process is attempted unsuccessfully for a goal,
the goal is deemed to have "settled down".  If no ancestor of the goal
has settled down, then the "settled-down" process is deemed to have
"hit" on the goal, the sole effect being that the goal makes a new pass
through all the waterfall processes.  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.

*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 key lists maintained by the theorem prover to manage
hints.  The other key 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
pending hints after the selected hint is removed; (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.  The primary function of this list is that
when a goal is pushed for later proof by induction, 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 children goals; a hint is applied only when it is
selected.

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 (at the top of the waterfall), the list of pending
hints is scanned, in order, until one of the hints is suitable 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.

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 a bit misplaced in this slightly tricky example.
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 indicated above, immediately causing another trip through
the waterfall.  At that point the :in-theory hint had already been
removed when it applied, leaving the default (:do-not) hint as the only
applicable hint.  That hint is indeed applied, resulting in the second
"Note" above.

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.

LD-ERROR-ACTION    determines ld's response to an error

Ld-error-action is an ld special (see LD).  The accessor is
(ld-error-action state) and the updater is (set-ld-error-action val
state).  Ld-error-action must be :continue, :return, or :error.  The
initial value of ld-error-action is :continue, which means that the
top-level ACL2 command loop will not exit when an error is caused by
user-typein.  But the default value for ld-error-action on calls of ld
is :return.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-action is one of them.  If, while ld-error-triples is t, a
form evaluates to three results, the first of which is non-nil and the
third of which is state, an error is said to have occurred.  If an
error occurs, ld's action depends on ld-error-action.  If it is
:continue, ld just continues processing the forms in standard-oi.  If
it is :return, ld stops and returns as though it had emptied the
channel.  If it is :error, ld stops and returns, signalling an error to
its caller.

LD-ERROR-TRIPLES    determines whether a form caused an error during ld

Ld-error-triples is an ld special (see LD).  The accessor is
(ld-error-triples state) and the updater is (set-ld-error-triples val
state).  Ld-error-triples must be either t or nil.  The initial value
of ld-error-triples is t.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-triples is one of them.  If this variable has the value t then
when a form evaluates to 3 values, the first of which is non-nil and
the third of which is state, an error is deemed to have occurred.  When
an error occurs in evaluating a form, ld rolls back the ACL2 world to
the configuration it had at the conclusion of the last error-free form.
Then ld takes the action determined by ld-error-action.

LD-EVISC-TUPLE    determines whether ld suppresses details when printing

Ld-evisc-tuple is an ld special (see LD).  The accessor is
(ld-evisc-tuple state) and an updater is (set-ld-evisc-tuple val
state), although the use of set-evisc-tuple is preferred for updating.
Ld-evisc-tuple must be either nil, which is its initial value, or a
legal evisc-tuple: see SET-EVISC-TUPLE.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-evisc-tuple is one of them.  Ld may print the forms it is evaluating
and/or the results of evaluation.  Depending on the value of
ld-evisc-tuple ld may "eviscerate" objects before printing them.  See
SET-EVISC-TUPLE for a discussion of evisceration and of how
other evisc-tuples affect the printing of error messages and warnings,
as well as other output not from ld.

LD-KEYWORD-ALIASES    allows the abbreviation of some keyword commands

     Example:
     (set-ld-keyword-aliases '((:q 0 q-fn)
                               (:e 0 exit-acl2-macro))
                             state)

Ld-keyword-aliases is an ld special (see LD).  The accessor is
(ld-keyword-aliases state) and the updater is (set-ld-keyword-aliases
val state).  Ld-keyword-aliases must be an alist, each element of which
is of the form (:keyword n fn), where :keyword is a keyword, n is a
nonnegative integer, and fn is a function symbol of arity n, a macro
symbol, or a lambda expression of arity n.  When keyword is typed as an
ld command, n more forms are read, x1, ..., xn, and the form (fn 'x1
... 'xn) is then evaluated.  The initial value of ld-keyword-aliases is
nil.

In the example above, :q has been redefined to have the effect of
executing (q-fn), so for example if you define

     (defmacro q-fn ()
       '(er soft 'q "You un-bound :q and now we have a soft error."))

then :q will cause an error, and if you define

     (defmacro exit-acl2-macro () '(exit-ld state))

then :e will cause the effect (it so happens) that :q normally has.  If
you prefer :e to :q for exiting the ACL2 loop, you might even want to
put such definitions of q-fn and exit-acl2-macro together with the
set-ld-keyword-aliases form above in your "acl2-customization.lsp"
file; see ACL2-CUSTOMIZATION.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-keyword-aliases is one of them.  Ld-keyword-aliases affects how
keyword commands are parsed.  Generally speaking, ld's command
interpreter reads ":fn x1 ... xn" as "(fn 'x1 ... 'xn)" when :fn is a
keyword and fn is the name of an n-ary function; see
KEYWORD-COMMANDS.  But this parse is overridden, as described above,
for the keywords bound in ld-keyword-aliases.

LD-POST-EVAL-PRINT    determines whether and how ld prints the result of evaluation

Ld-post-eval-print is an ld special (see LD).  The accessor is
(ld-post-eval-print state) and the updater is (set-ld-post-eval-print
val state).  Ld-post-eval-print must be either t, nil, or
:command-conventions.  The initial value of ld-post-eval-print is
:command-conventions.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-post-eval-print is one of them.  If this global variable is t, ld
prints the result.  In the case of a form that produces a multiple
value, ld prints the list containing all the values (which, logically
speaking, is what the form returned).  If ld-post-eval-print is nil, ld
does not print the values.  This is most useful when ld is used to load
a previously processed file.

Finally, if ld-post-eval-print is :command-conventions then ld prints
the result but treats "error triples" specially.  An "error triple" is
a result, (mv erp val state), that consists of three values, the third
of which is state.  Many ACL2 functions use such triples to signal
errors.  The convention is that if erp (the first value) is nil, then
the function is returning val (the second value) as its conventional
single result and possibly side-effecting state (as with some output).
If erp is t, then an error has been caused, val is irrelevant and the
error message has been printed in the returned state.  Example ACL2
functions that follow this convention include defun and in-package.  If
such "error producing" functions are evaluated while ld-post-eval-print
is set to t, then you would see them producing lists of length 3.  This
is disconcerting to users accustomed to Common Lisp (where these
functions produce single results but sometimes cause errors or
side-effect state).

When ld-post-eval-print is :command-conventions and a form produces an
error triple (mv erp val state) as its value, ld prints nothing if erp
is non-nil and otherwise ld prints just val.  Because it is a
misrepresentation to suggest that just one result was returned, ld
prints the value of the global variable 'triple-print-prefix before
printing val.  'triple-print-prefix is initially " ", which means that
when non-erroneous error triples are being abbreviated to val, val
appears one space off the left margin instead of on the margin.

In addition, when ld-post-eval-print is :command-conventions and the
value component of an error triple is the keyword :invisible then ld
prints nothing.  This is the way certain commands (e.g., :pc) appear to
return no value.

By printing nothing when an error has been signalled, ld makes it
appear that the error (whose message has already appeared in state) has
"thrown" the computation back to load without returning a value.  By
printing just val otherwise, we suppress the fact that state has
possibly been changed.

LD-PRE-EVAL-FILTER    determines which forms ld evaluates

Ld-pre-eval-filter is an ld special (see LD).  The accessor is
(ld-pre-eval-filter state) and the updater is (set-ld-pre-eval-filter
val state).  Ld-pre-eval-filter must be either :all, :query, or a new
name that could be defined (e.g., by defun or defconst).  The initial
value of ld-pre-eval-filter is :all.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-pre-eval-filter is one of them.  If the filter is :all, then every
form read is evaluated.  If the filter is :query, then after a form is
read it is printed to standard-co and the user is asked if the form is
to be evaluated or skipped.  If the filter is a new name, then all
forms are evaluated until that name is introduced, at which time ld
terminates normally.

The :all filter is, of course, the normal one.  :Query is useful if you
want to replay selected the commands in some file.  The new name filter
is used if you wish to replay all the commands in a file up through the
introduction of the given one.

LD-PRE-EVAL-PRINT    determines whether ld prints the forms to be eval'd

Ld-pre-eval-print is an ld special (see LD).  The accessor is
(ld-pre-eval-print state) and the updater is (set-ld-pre-eval-print val
state).  Ld-pre-eval-print must be either t, nil, or :never.  The
initial value of ld-pre-eval-print is nil.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-pre-eval-print is one of them.  If this global variable is t, then
before evaluating the form just read from standard-oi, ld prints the
form to standard-co.  If the variable is nil, no such printing occurs.
The t option is useful if you are reading from a file of commands and
wish to assemble a complete script of the session in standard-co.

The value :never of ld-pre-eval-print is rarely used.  During the
evaluation of encapsulate and of certify-book forms, subsidiary events
are normally printed, even if ld-pre-eval-print is nil.  Thus for
example, when the user submits an encapsulate form, all subsidiary
events are generally printed even in the default situation where
ld-pre-eval-print is nil.  But occasionally one may want to suppress
such printing.  In that case, ld-pre-eval-print should be set to
:never.  As described elsewhere (see SET-INHIBIT-OUTPUT-LST),
another way to suppress such printing is to execute
(set-inhibit-output-lst lst) where lst evaluates to a list including
'prove and 'event.

LD-PROMPT    determines the prompt printed by ld

Ld-prompt is an ld special (see LD).  The accessor is
(ld-prompt state) and the updater is (set-ld-prompt val state).
Ld-prompt must be either nil, t, or a function symbol that, when given
an open output character channel and state, prints the desired prompt
to the channel and returns two values: the number of characters printed
and the state.  The initial value of ld-prompt is t.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-prompt is one of them.  Ld-prompt determines whether ld prints a
prompt before reading the next form from standard-oi.  If ld-prompt is
nil, ld prints no prompt.  If ld-prompt is t, the default prompt
printer is used, which displays information that includes the current
package, default defun-mode, guard checking status (on or off), and
ld-skip-proofsp; see DEFAULT-PRINT-PROMPT.

If ld-prompt is neither nil nor t, then it should be a function name,
fn, such that (fn channel state) will print the desired prompt to
channel in state and return (mv col state), where col is the number of
characters output (on the last line output).  You may define your own
prompt printing function.

If you supply an inappropriate prompt function, i.e., one that causes
an error or does not return the correct number and type of results, the
following odd prompt will be printed instead:

     Bad Prompt
     See :DOC ld-prompt>

which will lead you to this message.  You should either call ld
appropriately next time or assign an appropriate value to ld-prompt.

LD-QUERY-CONTROL-ALIST    how to default answers to queries

Ld-query-control-alist is an ld special (see LD).  The accessor
is (ld-query-control-alist state) and the updater is
(set-ld-query-control-alist val state).  Roughly speaking,
ld-query-control-alist is either nil (meaning all queries should be
interactive), t (meaning all should default to the first accepted
response), or an alist that pairs query ids to keyword responses.  The
alist may end in either t or nil, indicating the default value for all
ids not listed explicitly.  Formally, the ld-query-control-alist must
satisfy ld-query-control-alistp.  The initial ld-query-control-alist is
nil, which means all queries are handled interactively.

When an ACL2 query is raised, a unique identifying symbol is printed in
parentheses after the word "Query".  This symbol, called the "query
id," can be used in conjunction with ld-query-control-alist to prevent
the query from being handled interactively.  By "handled interactively"
we mean that the query is printed to *standard-co* and a response is
read from *standard-oi*.  The alist can be used to obtain a "default
value" for each query id.  If this value is nil, then the query is
handled interactively.  In all other cases, the system handles the
query without interaction (although text may be printed to standard-co
to make it appear that an interaction has occurred; see below).  If the
default value is t, the system acts as though the user responded to the
query by typing the first response listed among the acceptable
responses.  If the default value is neither nil nor t, then it must be
a keyword and one of the acceptable responses.  In that case, the
system acts as though the user responded with the given keyword.

Next, we discuss how the ld-query-control-alist assigns a default value
to each query id.  It assigns each id the first value paired with the
id in the alist, or, if no such pair appears in the alist, it assigns
the final cdr of the alist as the value.  Thus, nil assigns all ids
nil.  T assigns all ids t.  '((:filter . nil) (:sysdef . :n) . t)
assigns nil to the :filter query, :n to the :sysdef query, and t to all
others.

It remains only to discuss how the system prints text when the default
value is not nil, i.e., when the query is handled without interaction.
In fact, it is allowed to pair a query id with a singleton list
containing a keyword, rather than a keyword, and this indicates that no
printing is to be done.  Thus for the example above, :sysdef queries
would be handled noninteractively, with printing done to simulate the
interaction.  But if we change the example so that :sysdef is paired
with (:n), i.e., if ld-query-control-alist is '((:filter . nil)
(:sysdef :n) . t), then no such printing would take place for sysdef
queries.  Instead, the default value of :n would be assigned "quietly".

LD-REDEFINITION-ACTION    to allow redefinition without undoing

Ld-redefinition-action is an ld special (see LD).  The accessor
is (ld-redefinition-action state) and the updater is
(set-ld-redefinition-action val state).

*WARNING!*  If ld-redefinition-action is non-nil then ACL2 is liable to
be made unsafe or unsound either by ill-considered definitions, or
because redefining a macro or inlined function called in the body of a
function, g, may not cause the new definition to be called by g.  The
keyword command :redef will set ld-redefinition-action to a convenient
setting allowing unsound redefinition.  See below.

When ld-redefinition-action is nil, redefinition is prohibited.  In
that case, an error message is printed upon any attempt to introduce a
name that is already in use.  There is one exception to this rule.  It
is permitted to redefine a function symbol in :program mode to be a
function symbol in :logic mode provided the formals and body remain the
same.  This is the standard way a function "comes into" logical
existence.

Throughout the rest of this discussion we exclude from our meaning of
"redefinition" the case in which a function in :program mode is
identically redefined in :logic mode.  At one time, ACL2 freely
permitted the signature-preserving redefinition of :program mode
functions but it no longer does.  See REDEFINING-PROGRAMS.

When ld-redefinition-action is non-nil, you are allowed to redefine a
name that is already in use.  *The system may be rendered unsound* by
such an act.  It is important to understand how dangerous redefinition
is.  Suppose fn is a function symbol that is called from within some
other function, say g.  Suppose fn is redefined so that its arity
changes.  Then the definition of g is rendered syntactically ill-formed
by the redefinition.  This can be devastating since the entire ACL2
system assumes that terms in its data base are well-formed.  For
example, if ACL2 executes g by running the corresponding function in
raw Common Lisp the redefinition of fn may cause raw lisp to break in
irreparable ways.  As Lisp programmers we live with this all the time
by following the simple rule: after changing the syntax of a function
don't run any function that calls it via its old syntax.  This rule
also works in the context of the evaluation of ACL2 functions, but it
is harder to follow in the context of ACL2 deductions, since it is hard
to know whether the data base contains a path leading the theorem
prover from facts about one function to facts about another.  Finally,
of course, even if the data base is still syntactically well-formed
there is no assurance that all the rules stored in it are valid.  For
example, theorems proved about g survive the redefinition of fn but may
have crucially depended on the properties of the old fn.  In summary,
we repeat the warning: *all bets are off if you set*
ld-redefinition-action to *non*-nil.

ACL2 provides some enforcement of the concern above, by disabling
certify-book if any world-changing events exist in the certification
world that were executed with a non-nil value of
'ld-redefinition-action.  (This value is checked at the end of each
top-level command, but the value does not change during evaluation of
embedded event forms; see EMBEDDED-EVENT-FORM.)

If at any point in a session you wish to see the list of all names that
have been redefined, see REDEFINED-NAMES.

That said, we'll give you enough rope to hang yourself.  When
ld-redefinition-action is non-nil, it must be a pair, (a .  b).  The
value of a determines how the system interacts with you when a
redefinition is submitted.  The value of b allows you to specify how the
property list of the redefined name is to be "renewed" before the
redefinition.

There are several dimensions to the space of possibilities controlled
by part a: Do you want to be queried each time you redefine a name, so
you can confirm your intention?  (We sometimes make typing mistakes or
simply forget we have used that name already.)  Do you want to see a
warning stating that the name has been redefined?  Do you want ACL2
system functions given special protection from possible redefinition?
Below are the choices for part a:

     :query -- every attempt to redefine a name will produce a query.
     The query will allow you to abort the redefinition or proceed.  It
     will will also allow you to specify the part b for this
     redefinition.  :Query is the recommended setting for users who
     wish to dabble in redefinition.

     :warn -- any user-defined function may be redefined but a
     post-redefinition warning is printed.  The attempt to redefine a
     system name produces a query.  If you are prototyping and testing
     a big system in ACL2 this is probably the desired setting for part
     a.

     :doit -- any user-defined function may be redefined silently
     (without query or warning) but when an attempt is made to redefine
     a system function, a query is made.  This setting is recommended
     when you start making massive changes to your prototyped system
     (and tire of even the warning messages issued by :warn).

In support of our own ACL2 systems programming there are two other
settings.  We suggest ordinary users not use them.

     :warn! -- every attempt to redefine a name produces a warning but
     no query.  Since ACL2 system functions can be redefined this way,
     this setting should be used by the only-slightly-less-than
     supremely confident ACL2 system hacker.

     :doit! -- this setting allows any name to be redefined silently
     (without query or warnings).  ACL2 system functions are fair game.
     This setting is reserved for the supremely confident ACL2 system
     hacker.  (Actually, this setting is used when we are loading
     massively modified versions of the ACL2 source files.)

Part b of ld-redefinition-action tells the system how to "renew" the
property list of the name being redefined.  There are two choices:

     :erase -- erase all properties stored under the name, or

     :overwrite -- preserve existing properties and let the redefining
     overwrite them.

It should be stressed that neither of these b settings is guaranteed to
result in an entirely satisfactory state of affairs after the
redefinition.  Roughly speaking, :erase returns the property list of the
name to the state it was in when the name was first introduced.
Lemmas, type information, etc., stored under that name are lost.  Is
that what you wanted?  Sometimes it is, as when the old definition is
"completely wrong." But other times the old definition was "almost
right" in the sense that some of the work done with it is still
(intended to be) valid.  In that case, :overwrite might be the correct
b setting.  For example if fn was a function and is being re-defun'd
with the same signature, then the properties stored by the new defun
should overwrite those stored by the old defun but the properties
stored by defthms will be preserved.

In addition, neither setting will cause ACL2 to erase properties stored
under other symbols!  Thus, if FOO names a rewrite rule which rewrites
a term beginning with the function symbol BAR and you then redefine FOO
to rewrite a term beginning with the function symbol BAZ, then the old
version of FOO is still available (because the rule itself was added to
the rewrite rules for BAR, whose property list was not cleared by
redefining FOO).

The b setting is only used as the default action when no query is made.
If you choose a setting for part a that produces a query then you will
have the opportunity, for each redefinition, to specify whether the
property list is to be erased or overwritten.

The keyword command :redef sets ld-redefinition-action to the pair
(:query . :overwrite).  Since the resulting query will give you the
chance to specify :erase instead of :overwrite, this setting is quite
convenient.  But when you are engaged in heavy-duty prototyping, you
may wish to use a setting such as :warn or even :doit.  For that you
will have to invoke a form such as:

     (set-ld-redefinition-action '(:doit . :overwrite) state) .

Encapsulate causes somewhat odd interaction with the user if
redefinition occurs within the encapsulation because the encapsulated
event list is processed several times.  For example, if the redefinition
action causes a query and a non-local definition is actually a
redefinition, then the query will be posed twice, once during each
pass.  C'est la vie.

Finally, it should be stressed again that redefinition is dangerous
because not all of the rules about a name are stored on the property
list of the name.  Thus, redefinition can render ill-formed terms
stored elsewhere in the data base or can preserve now-invalid rules.
See REDUNDANT-EVENTS, in particular the section "Note About
Unfortunate Redundancies," for more discussion of potential pitfalls of
redefinition.

LD-SKIP-PROOFSP    how carefully ACL2 processes your commands

     Examples:
     ACL2 !>(set-ld-skip-proofsp t state)
      T
     ACL2 !s>(set-ld-skip-proofsp nil state)
      NIL
     ACL2 !>(set-ld-skip-proofsp 'include-book state)
      INCLUDE-BOOK
     ACL2 !s>

A global variable in the ACL2 state, called 'ld-skip-proofsp,
determines the thoroughness with which ACL2 processes your commands.
This variable may take on one of three values: t, nil or 'include-book.
When ld-skip-proofsp is non-nil, the system assumes that which ought
to be proved and is thus unsound.  The form (set-ld-skip-proofsp flg
state) is the general-purpose way of setting ld-skip-proofsp.  This
global variable is an "ld special," which is to say, you may call ld in
such a way as to "bind" this variable for the dynamic extent of the ld.

When ld-skip-proofsp is non-nil, the default prompt displays the
character s.  Thus, the prompt

     ACL2 !s>

means that the default defun-mode is :logic (otherwise the character p,
for :program, would also be printed; see DEFAULT-PRINT-PROMPT)
but "proofs are being skipped."

Observe that there are two legal non-nil values, t and 'include-book.
When ld-skip-proofsp is t, ACL2 skips all proof obligations but
otherwise performs all other required analysis of input events.  When
ld-skip-proofsp is 'include-book, ACL2 skips not only proof obligations
but all analysis except that required to compute the effect of
successfully executed events.  To explain the distinction, let us
consider one particular event, say a defun.  Very roughly speaking, a
defun event normally involves a check of the syntactic well-formedness
of the submitted definition, the generation and proof of the
termination conditions, and the computation and storage of various
rules such as a :definition rule and some :type-prescription rules.  By
"normally" above we mean when ld-skip-proofsp is nil.  How does a defun
behave when ld-skip-proofsp is non-nil?

If ld-skip-proofsp is t, then defun performs the syntactic
well-formedness checks and computes and stores the various rules, but
it does not actually carry out the termination proofs.  If
ld-skip-proofsp is 'include-book, defun does not do the syntactic
well-formedness check nor does it carry out the termination proof.
Instead, it merely computes and stores the rules under the assumption
that the checks and proofs would all succeed.  Observe that a setting
of 'include-book is "stronger" than a setting of t in the sense that
'include-book causes defun to assume even more about the admissibility
of the event than t does.

As one might infer from the choice of name, the include-book event sets
ld-skip-proofsp to 'include-book when processing the events in a book
being loaded.  Thus, include-book does the miminal work necessary to
carry out the effects of every event in the book.  The syntactic checks
and proof obligations were, presumably, successfully carried out when
the book was certified.

A non-nil value for ld-skip-proofsp also affects the system's output
messages.  Event summaries (the paragraphs that begin "Summary" and
display the event forms, rules used, etc.) are not printed when
ld-skip-proofsp is non-nil.  Warnings and observations are printed when
ld-skip-proofsp is t but are not printed when it is 'include-book.

Intuitively, ld-skip-proofsp t means skip just the proofs and otherwise
do all the work normally required for an event; while ld-skip-proofsp
'include-book is "stronger" and means do as little as possible to
process events.  In accordance with this intuition, local events are
processed when ld-skip-proofsp is t but are skipped when
ld-skip-proofsp is 'include-book.

The ACL2 system itself uses only two settings, nil and 'include-book,
the latter being used only when executing the events inside of a book
being included.  The ld-skip-proofsp setting of t is provided as a
convenience to the user.  For example, suppose one has a file of
events.  By loading it with ld with ld-skip-proofsp set to t, the
events can all be checked for syntactic correctness and assumed without
proof.  This is a convenient way to recover a state lost by a system
crash or to experiment with a modification of an events file.

The foregoing discussion is actually based on a lie.  ld-skip-proofsp
is allowed two other values, 'initialize-acl2 and
'include-book-with-locals.  The first causes behavior similar to t but
skips local events and avoids some error checks that would otherwise
prevent ACL2 from properly booting.  The second is identical to
'include-book but also executes local events.  These additional values
are not intended for use by the user, but no barriers to their use have
been erected.

We close by reminding the user that ACL2 is potentially unsound if
ld-skip-proofsp is ever set by the user.  We provide access to it
simply to allow experimentation and rapid reconstruction of lost or
modified logical worlds.

LD-VERBOSE    determines whether ld prints "ACL2 Loading ..."

Ld-verbose is an ld special (see LD).  The accessor is
(ld-verbose state) and the updater is (set-ld-verbose val state).
Ld-verbose must be t, nil or a string or consp suitable for fmt
printing via the ~@ command.  The initial value of ld-verbose is a fmt
message that prints the ACL2 version number, ld level and connected
book directory.

Before processing the forms in standard-oi, ld may print a header.  The
printing of this header is controlled by ld-verbose.  If ld-verbose is
nil, no header is printed.  If it is t, ld prints the message

        ACL2 loading <file>

where <file> is the input channel supplied to ld.  A similar message is
printed when ld completes.  If ld-verbose is neither t nor nil then it
is presumably a header and is printed with the ~@ fmt directive before
ld begins to read and process forms.  In this case the ~@ fmt directive
is interpreted in an environment in which #\v is the ACL2 version
string, #\l is the level of the current recursion in ld and/or
wormhole, and #\c is the connected book directory (cbd).

LEMMA-INSTANCE    an object denoting an instance of a theorem

Lemma instances are the objects one provides via :use and :by hints
(see HINTS) to bring to the theorem prover's attention some
previously proved or easily provable fact.  A typical use of the :use
hint is given below.  The value specified is a list of five lemma
instances.

     :use (reverse-reverse
           (:type-prescription app)
           (:instance assoc-of-app
                      (x a) (y b) (z c))
           (:functional-instance p-f
                                 (p consp) (f flatten))
           (:instance (:theorem (equal x x))
                      (x (flatten a))))

Observe that an event name can be a lemma instance.  The :use hint
allows a single lemma instance to be provided in lieu of a list, as in:

     :use reverse-reverse

or

     :use (:instance assoc-of-app (x a) (y b) (z c))

A lemma instance denotes a formula which is either known to be a
theorem or which must be proved to be a theorem before it can be used.
To use a lemma instance in a particular subgoal, the theorem prover
adds the formula as a hypothesis to the subgoal before the normal
theorem proving heuristics are applied.

A lemma instance, or lmi, is of one of the following five forms:

(1) name, where name names a previously proved theorem, axiom, or
definition and denotes the formula (theorem) of that name.

(2) rune, where rune is a rune (see RUNE) denoting the
:corollary justifying the rule named by the rune.

(3) (:theorem term), where term is any term alleged to be a theorem.
Such a lemma instance denotes the formula term.  But before using such a
lemma instance the system will undertake to prove term.

(4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively a
lemma instance, the vi's are distinct variables and the ti's are terms.
Such a lemma instance denotes the formula obtained by instantiating
the formula denoted by lmi, replacing each vi by ti.

(5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is
recursively a lemma instance and each fi is an "instantiable" function
symbol of arity ni and gi is a function symbol, a macro alias for a
function symbol gi' (see MACRO-ALIASES-TABLE) in which case we
treat gi as gi', or a pseudo-lambda expression of arity ni.  An
instantiable function symbol is any defined or constrained function
symbol except the primitives not, member, implies, and o<, and a few
others, as listed by the constant *non-instantiable-primitives*.  These
are built-in in such a way that we cannot recover the constraints on
them.  (Special case: a function introduced in the :partial-theory of a
dependent clause-processor is not instantiable; see
DEFINE-TRUSTED-CLAUSE-PROCESSOR.)  A pseudo-lambda expression is an
expression of the form (lambda (v1 ... vn) body) where the vi are
distinct variable symbols and body is any term.  No a priori relation
is imposed between the vi and the variables of body, i.e., body may
ignore some vi's and may contain "free" variables.  However, we do not
permit v to occur freely in body if the functional substitution is to
be applied to any formula (lmi or the constraints to be satisfied) in a
way that inserts v into the scope of a binding of v by let or mv-let
(or, lambda).  If you happen to violate this restriction, an
informative error message will be printed.  That message will list for
you the potentially illegal choices for v in the context in which the
functional substitution is offered.  A :functional-instance lemma
instance denotes the formula obtained by functionally instantiating the
formula denoted by lmi, replacing fi by gi.  However, before such a
lemma instance can be used, the system will generate proof obligations
arising from the replacement of the fi's by the gi's in constraints
that "support" the lemma to be functionally instantiated; see
CONSTRAINT.  One might expect that if the same instantiated
constraint were generated on behalf of several events, then each of
those instances would have to be proved.  However, for the sake of
efficiency, ACL2 stores the fact that such an instantiated constraint
has been proved and avoids it in future events.

Obscure case for definitions.  If the lemma instance refers to a
:definition rune, then it refers to the corollary formula of that rune,
which can be a simplified ("normalized") form of the original formula.
However, if the hint is a :by hint and the lemma instance is based on a
name (i.e., a symbol), rather than a rune, then the formula is the
original formula of the event, as shown by :pe, rather than the
normalized version, as shown by :pf.  This is as one would expect: If
you supply the name of an event, you expect it to refer to the original
event.  For :use hints we use the simplified (normalized) form instead,
which is reasonable since one would expect simplification during the
proof that re-traces the normalization done at the time the rule was
created.

See FUNCTIONAL-INSTANTIATION-EXAMPLE for an example of the use
of :functional-instance (so-called "functional instantiation)."

LINEAR-ARITHMETIC    A description of the linear arithmetic decision procedure

We describe the procedure very roughly here.  Fundamental to the
procedure is the notion of a linear polynomial inequality.  A "linear
polynomial" is a sum of terms, each of which is the product of a
rational constant and an "unknown."  The "unknown" is permitted to be 1
simply to allow a term in the sum to be constant.  Thus, an example
linear polynomial is 3*x + 7*a + 2; here x and a are the (interesting)
unknowns.  However, the unknowns need not be variable symbols.  For
example, (length x) might be used as an unknown in a linear polynomial.
Thus, another linear polynomial is 3*(length x) + 7*a.  A "linear
polynomial inequality" is an inequality (either < or <=) relation
between two linear polynomials.  Note that an equality may be
considered as a pair of inequalities; e.q., 3*x + 7*a + 2 = 0 is the
same as the conjunction of 3*x + 7*a + 2 <= 0 and 0 <= 3*x + 7*a + 2.

Certain linear polynomial inequalities can be combined by
cross-multiplication and addition to permit the deduction of a third
inequality with fewer unknowns.  If this deduced inequality is
manifestly false, a contradiction has been deduced from the assumed
inequalities.

For example, suppose we have two assumptions

     p1:       3*x + 7*a <  4
     p2:               3 <  2*x

and we wish to prove that, given p1 and p2, a < 0.  As suggested above,
we proceed by assuming the negation of our goal

     p3:               0 <= a.

and looking for a contradiction.

By cross-multiplying and adding the first two inequalities, (that is,
multiplying p1 by 2, p2 by 3 and adding the respective sides), we
deduce the intermediate result

     p4:  6*x + 14*a + 9 < 8 + 6*x

which, after cancellation, is:

     p4:        14*a + 1 <  0.

If we then cross-multiply and add p3 to p4, we get

     p5:               1 <= 0,

a contradiction.  Thus, we have proved that p1 and p2 imply the
negation of p3.

All of the unknowns of an inequality must be eliminated by cancellation
in order to produce a constant inequality.  We can choose to eliminate
the unknowns in any order, but we eliminate them in term-order, largest
unknowns first.  (See TERM-ORDER.)  That is, two polys are
cancelled against each other only when they have the same largest
unknown.  For instance, in the above example we see that x is the
largest unknown in each of p1 and p2, and a in p3 and p4.

Now suppose that this procedure does not produce a contradiction but
instead yields a set of nontrivial inequalities.  A contradiction might
still be deduced if we could add to the set some additional
inequalities allowing further cancellations.  That is where :linear
lemmas come in.  When the set of inequalities has stabilized under
cross-multiplication and addition and no contradiction is produced, we
search the data base of :linear rules for rules about the unknowns that
are candidates for cancellation (i.e., are the largest unknowns in
their respective inequalities).  See LINEAR for a description
of how :linear rules are used.

See also non-linear-arithmetic for a description of an extension to the
linear-arithmetic procedure described here.

LOCAL-INCOMPATIBILITY    when non-local events won't replay in isolation

Sometimes a "local incompatibility" is reported while attempting to
embed some events, as in an encapsulate or include-book.  This is
generally due to the use of a locally defined name in a non-local event
or the failure to make a witnessing definition local.

local incompatibilities may be detected while trying to execute the
strictly non-local events of an embedding.  For example, encapsulate
operates by first executing all the events (local and non-local) with
ld-skip-proofsp nil, to confirm that they are all admissible.  Then it
attempts merely to assume the non-local ones to create the desired
theory, by executing the events with ld-skip-proofsp set to
'include-book.  Similarly, include-book assumes the non-local ones,
with the understanding that a previously successful certify-book has
performed the admissiblity check.

How can a sequence of events admitted with ld-skip-proofsp nil fail
when ld-skip-proofsp is 'include-book?  The key observation is that in
the latter case only the non-local events are processed.  The local
ones are skipped and so the non-local ones must not depend upon them.

Two typical mistakes are suggested by the detection of a local
incompatibility: (1) a locally defined function or macro was used in a
non-local event (and, in the case of encapsulate, was not included
among the signatures) and (2) the witnessing definition of a function
that was included among the signatures of an encapsulate was not made
local.

An example of mistake (1) would be to include among your encapsulated
events both (local (defun fn ...)) and (defthm lemma (implies (fn ...)
...)).  Observe that fn is defined locally but a formula involving fn
is defined non-locally.  In this case, either the defthm should be made
local or the defun should be made non-local.

An example of mistake (2) would be to include (fn (x) t) among your
signatures and then to write (defun fn (x) ...) in your events, instead
of (local (defun fn ...)).

One subtle aspect of encapsulate is that if you constrain any member of
a mutually recursive clique you must define the entire clique locally
and then you must constrain those members of it you want axiomatized
non-locally.

Errors due to local incompatibility should never occur in the
assumption of a fully certified book.  Certification ensures against
it.  Therefore, if include-book reports an incompatibility, we assert
that earlier in the processing of the include-book a warning was
printed advising you that some book was uncertified.  If this is not
the case -- if include-book reports an incompatibility and there has
been no prior warning about lack of certification -- please report it
to us.

When a local incompatibility is detected, we roll-back to the world in
which we started the encapsulate or include-book.  That is, we discard
the intermediate world created by trying to process the events skipping
proofs.  This is clean, but we realize it is very frustrating because
the entire sequence of events must be processed from scratch.  Assuming
that the embedded events were, once upon a time, processed as top-level
commands (after all, at some point you managed to create this sequence
of commands so that the local and non-local ones together could survive
a pass in which proofs were done), it stands to reason that we could
define a predicate that would determine then, before you attempted to
embed them, if local incompatibilities exist.  We hope to do that,
eventually.

We conclude with a subtle example of local incompatibility.  The problem
is that in order for foo-type-prescription to be admitted using the
specified :typed-term (foo x), the conclusion (my-natp (foo x)) depends
on my-natp being a compound-recognizer.  This is fine on the first pass
of the encapsulate, during which lemma my-natp-cr is admitted.  But
my-natp-cr is skipped on the second pass because it is marked local,
and this causes foo-type-prescription to fail on the second pass.

     (defun my-natp (x)
       (declare (xargs :guard t))
       (and (integerp x)
            (<= 0 x)))

     (defun foo (x)
       (nfix x))

     (encapsulate
      ()
      (local (defthm my-natp-cr
               (equal (my-natp x)
                      (and (integerp x)
                           (<= 0 x)))
               :rule-classes :compound-recognizer))
      (defthm foo-type-prescription
        (my-natp (foo x))
        :hints (("Goal" :in-theory (enable foo)))
        :rule-classes ((:type-prescription :typed-term (foo x)))))

LOGICAL-NAME    a name created by a logical event

     Examples:
     assoc
     caddr
     +
     "ACL2-USER"
     "arith"
     "project/task-1/arith.lisp"
     :here

A logical name is either a name introduced by some event, such as
defun, defthm, or include-book, or else is the keyword :here, which
refers to the most recent such event.  See EVENTS.  Every
logical name is either a symbol or a string.  For the syntactic rules
on names, see NAME.  The symbols name functions, macros,
constants, axioms, theorems, labels, and theories.  The strings name
packages or books.  We permit the keyword symbol :here to be used as a
logical name denoting the most recently completed event.

The logical name introduced by an include-book is the full book name
string for the book (see FULL-BOOK-NAME).  Thus, under the
appropriate setting for the current book directory (see CBD)
the event (include-book "arith") may introduce the logical name

     "/usr/home/smith/project/task-1/arith.lisp" .

Under a different cbd setting, it may introduce a different logical
name, perhaps

     "/local/src/acl2/library/arith.lisp" .

It is possible that identical include-book events forms in a session
introduce two different logical names because of the current book
directory.

A logical name that is a string is either a package name or a book
name.  If it is not a package name, we support various conventions to
interpret it as a book name.  If it does not end with the string
".lisp" we extend it appropriately.  Then, we search for any book name
that has the given logical name as a terminal substring.  Suppose
(include-book "arith") is the only include-book so far and that
"/usr/home/smith/project/task-1/arith.lisp" is the source file it
processed.  Then "arith", "arith.lisp" and "task-1/arith.lisp" are all
logical names identifying that include-book event (unless they are
package names).  Now suppose a second (include-book "arith") is
executed and processes "/local/src/acl2/library/arith.lisp".  Then
"arith" is no longer a logical name, because it is ambiguous.  However,
"task-1/arith" is a logical name for the first include-book and
"library/arith" is a logical name for the second.  Indeed, the first
can be named by "1/arith" and the second by "y/arith".

Logical names are used primarily in the theory manipulation functions,
e.g., universal-theory and current-theory with which you may obtain
some standard theories as of some point in the historical past.  The
reference points are the introductions of logical names, i.e., the past
is determined by the events it contains.  One might ask, "Why not
discuss the past with the much more flexible language of command
descriptors?" (See COMMAND-DESCRIPTOR.)  The reason is that
inside of such events as encapsulate or macro commands that expand to
progns of events, command descriptors provide too coarse a grain.

When logical names are used as referents in theory expressions used in
books, one must consider the possibility that the defining event within
the book in question becomes redundant by the definition of the name
prior to the assumption of the book.  See REDUNDANT-EVENTS.

LOOP-STOPPER    limit application of permutative rewrite rules

See RULE-CLASSES for a discussion of the syntax of the
:loop-stopper field of :rewrite rule-classes.  Here we describe how
that field is used, and also how that field is created when the user
does not explicitly supply it.

For example, the built-in :rewrite rule commutativity-of-+,

     (implies (and (acl2-numberp x)
                   (acl2-numberp y))
              (equal (+ x y) (+ y x))),

creates a rewrite rule with a loop-stopper of ((x y binary-+)).  This
means, very roughly, that the term corresponding to y must be "smaller"
than the term corresponding to x in order for this rule to apply.
However, the presence of binary-+ in the list means that certain
functions that are "invisible" with respect to binary-+ (by default,
unary- is the only such function) are more or less ignored when making
this "smaller" test.  We are much more precise below.

Our explanation of loop-stopping is in four parts.  First we discuss
ACL2's notion of "term order."  Next, we bring in the notion of
"invisibility", and use it together with term order to define orderings
on terms that are used in the loop-stopping algorithm.  Third, we
describe that algorithm.  These topics all assume that we have in hand
the :loop-stopper field of a given rewrite rule; the fourth and final
topic describes how that field is calculated when it is not supplied by
the user.

ACL2 must sometimes decide which of two terms is syntactically simpler.
It uses a total ordering on terms, called the "term order."  Under
this ordering constants such as '(a b c) are simpler than terms
containing variables such as x and (+ 1 x).  Terms containing variables
are ordered according to how many occurrences of variables there are.
Thus x and (+ 1 x) are both simpler than (cons x x) and (+ x y).  If
variable counts do not decide the order, then the number of function
applications are tried.  Thus (cons x x) is simpler than (+ x (+ 1 y))
because the latter has one more function application.  Finally, if the
number of function applications do not decide the order, a
lexicographic ordering on Lisp objects is used.  See TERM-ORDER
for details.

When the loop-stopping algorithm is controlling the use of permutative
:rewrite rules it allows term1 to be moved leftward over term2 only if
term1 is smaller, in a suitable sense.  Note: The sense used in
loop-stopping is *not* the above explained term order but a more
complicated ordering described below.  The use of a total ordering
stops rules like commutativity from looping indefinitely because it
allows (+ b a) to be permuted to (+ a b) but not vice versa, assuming a
is smaller than b in the ordering.  Given a set of permutative rules
that allows arbitrary permutations of the tips of a tree of function
calls, this will normalize the tree so that the smallest argument is
leftmost and the arguments ascend in the order toward the right.  Thus,
for example, if the same argument appears twice in the tree, as x does
in the binary-+ tree denoted by the term (+ a x b x), then when the
allowed permutations are done, all occurrences of the duplicated
argument in the tree will be adjacent, e.g., the tree above will be
normalized to (+ a b x x).

Suppose the loop-stopping algorithm used term order, as noted above,
and consider the binary-+ tree denoted by (+ x y (- x)).  The arguments
here are in ascending term order already.  Thus, no permutative rules
are applied.  But because we are inside a +-expression it is very
convenient if x and (- x) could be given virtually the same position in
the ordering so that y is not allowed to separate them.  This would
allow such rules as (+ i (- i) j) = j to be applied.  In support of
this, the ordering used in the control of permutative rules allows
certain unary functions, e.g., the unary minus function above, to be
"invisible" with respect to certain "surrounding" functions, e.g., +
function above.

Briefly, a unary function symbol fn1 is invisible with respect to a
function symbol fn2 if fn2 belongs to the value of fn1 in
invisible-fns-table; also see SET-INVISIBLE-FNS-TABLE, which
explains its format and how it can be set by the user.  Roughly
speaking, "invisible" function symbols are ignored for the purposes of
the term-order test.

Consider the example above, (+ x y (- x)).  The translated version of
this term is (binary-+ x (binary-+ y (unary- x))).  The initial
invisible-fns-table makes unary- invisible with repect to binary-+.
The commutativity rule for binary-+ will attempt to swap y and (unary-
x) and the loop-stopping algorithm is called to approve or disapprove.
If term order is used, the swap will be disapproved.  But term order is
not used.  While the loop-stopping algorithm is permuting arguments
inside a binary-+ expression, unary- is invisible.  Thus, insted of
comparing y with (unary- x), the loop-stopping algorithm compares y
with x, approving the swap because x comes before y.

Here is a more precise specification of the total order used for
loop-stopping with respect to a list, fns, of functions that are to be
considered invisible.  Let x and y be distinct terms; we specify when
"x is smaller than y with respect to fns."  If x is the application of
a unary function symbol that belongs to fns, replace x by its argument.
Repeat this process until the result is not the application of such a
function; let us call the result x-guts.  Similarly obtain y-guts from
y.  Now if x-guts is the same term as y-guts, then x is smaller than y
in this order iff x is smaller than y in the standard term order.  On
the other hand, if x-guts is different than y-guts, then x is smaller
than y in this order iff x-guts is smaller than y-guts in the standard
term order.

Now we may describe the loop-stopping algorithm.  Consider a rewrite
rule with conclusion (equiv lhs rhs) that applies to a term x in a
given context; see REWRITE.  Suppose that this rewrite rule has
a loop-stopper field (technically, the :heuristic-info field) of ((x1
y1 . fns-1) ... (xn yn . fns-n)).  (Note that this field can be
observed by using the command :pr with the name of the rule; see
PR.)  We describe when rewriting is permitted.  The simplest case is
when the loop-stopper list is nil (i.e., n is 0); in that case,
rewriting is permitted.  Otherwise, for each i from 1 to n let xi' be
the actual term corresponding to the variable xi when lhs is matched
against the term to be rewritten, and similarly correspond yi' with y.
If xi' and yi' are the same term for all i, then rewriting is not
permitted.  Otherwise, let k be the least i such that xi' and yi' are
distinct.  Let fns be the list of all functions that are invisible with
respect to every function in fns-k, if fns-k is non-empty; otherwise,
let fns be nil.  Then rewriting is permitted if and only if yi' is
smaller than xi' with respect to fns, in the sense defined in the
preceding paragraph.

It remains only to describe how the loop-stopper field is calculated
for a rewrite rule when this field is not supplied by the user.  (On
the other hand, to see how the user may specify the :loop-stopper, see
RULE-CLASSES.)  Suppose the conclusion of the rule is of the
form (equiv lhs rhs).  First of all, if rhs is not an instance of the
left hand side by a substitution whose range is a list of distinct
variables, then the loop-stopper field is nil.  Otherwise, consider all
pairs (u . v) from this substitution with the property that the first
occurrence of v appears in front of the first occurrence of u in the
print representation of rhs.  For each such u and v, form a list fns of
all functions fn in lhs with the property that u or v (or both) appears
as a top-level argument of a subterm of lhs with function symbol fn.
Then the loop-stopper for this rewrite rule is a list of all lists (u v
. fns).

LP    the Common Lisp entry to ACL2

To enter the ACL2 command loop from Common Lisp, call the Common Lisp
program lp (which stands for "loop," as in "read-eval-print loop" or
"command loop.")  The ACL2 command loop is actually coded in ACL2 as
the function ld (which stands for "load").  The command loop is just
what you get by loading from the standard object input channel,
*standard-oi*.  Calling ld directly from Common Lisp is possible but
fragile because hard lisp errors or aborts throw you out of ld and back
to the top-level of Common Lisp.  Lp calls ld in such a way as to
prevent this and is thus the standard way to get into the ACL2 command
loop.  Also see ACL2-CUSTOMIZATION for information on the
loading of an initialization file.

All of the visible functionality of lp is in fact provided by ld, which
is written in ACL2 itself.  Therefore, you should see LD for
detailed documentation of the ACL2 command loop.  We sketch it below,
for novice users.

Every expression typed to the ACL2 top-level must be an ACL2 expression.

Any ACL2 expression may be submitted for evaluation.  Well-formedness
is checked.  Some well-formed expressions cannot be evaluated because
they involve (at some level) undefined constrained functions (see
ENCAPSULATE).  In addition, ACL2 does not allow "global variables" in
expressions to be evaluated.  Thus, (car '(a b c)) is legal and
evaluates to A, but (car x) is not, because there is no "global
context" or binding environment that gives meaning to the variable
symbol x.

There is an exception to the global variable rule outlined above:
single-threaded objects (see STOBJ) may be used as global
variables in top-level expressions.  The most commonly used such object
is the ACL2 "current state," which is the value of the variable symbol
state.  This variable may occur in the top-level form to be evaluated,
but must be passed only to ACL2 functions "expecting" state as
described in the documentation for state and for stobjs in general.  If
the form returns a new state object as one of its values, then that is
considered the new "current" state for the evaluation of the subsequent
form.  See STATE.

ACL2 provides some support for the functionality usually provided by
global variables in a read-eval-print loop, namely the saving of the
result of a computation for subsequent re-use in another expression.
See ASSIGN and see @.

If the form read is a single keyword, e.g., :pe or :ubt, then special
procedures are followed.  See KEYWORD-COMMANDS.

The command loop keeps track of the commands you have typed and allows
you to review them, display them, and roll the logical state back to
that created by any command.  See HISTORY.

ACL2 makes the convention that if a top-level form returns three
values, the last of which is an ACL2 state, then the first is treated
as a flag that means "an error occurred," the second is the value to be
printed if no error occurred, and the third is (of course) the new
state.  When "an error occurs" no value is printed.  Thus, if you
execute a top-level form that happens to return three such values, only
the second will be printed (and that will only happen if the first is
nil!).  See LD for details.

MACRO-ARGS    the formals list of a macro definition

     Examples:
     (x y z)
     (x y z &optional max (base '10 basep))
     (x y &rest rst)
     (x y &key max base)
     (&whole sexpr x y)

The "lambda-list" of a macro definition may include simple formal
parameter names as well as appropriate uses of the following
lambda-list keywords from CLTL (pp. 60 and 145), respecting the order
shown:

       &whole,
       &optional,
       &rest,
       &body,
       &key, and
       &allow-other-keys.

ACL2 does not support &aux and &environment.  In addition, we make the
following restrictions:

     (1) initialization forms in &optional and &key specifiers must be
     quoted values;

     (2) &allow-other-keys may only be used once, as the last
     specifier; and

     (3) destructuring is not allowed.

You are encouraged to experiment with the macro facility.  One way to
do so is to define a macro that does nothing but return the quotation
of its arguments, e.g.,

     (defmacro demo (x y &optional opt &key key1 key2)
       (list 'quote (list x y opt key1 key2)))

You may then execute the macro on some sample forms, e.g.,

       term                         value
     (demo 1 2)                (1 2 NIL NIL NIL)
     (demo 1 2 3)              (1 2 3 NIL NIL)
     (demo 1 2 :key1 3)        error:  non-even key/value arglist
                               (because :key1 is used as opt)
     (demo 1 2 3 :key2 5)      (1 2 3 NIL 5)

In particular, Common Lisp specifies that if you use both &rest and
&key, then both will be bound using the same list of arguments.  The
following example should serve to illustrate how this works.

     ACL2 !>(defmacro foo (&rest args &key k1 k2 k3)
              (list 'quote (list args k1 k2 k3)))

     Summary
     Form:  ( DEFMACRO FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>(foo :k1 3 :k2 4 :k3 5)
     ((:K1 3 :K2 4 :K3 5) 3 4 5)
     ACL2 !>(foo :k1 3 :k2 4)
     ((:K1 3 :K2 4) 3 4 NIL)
     ACL2 !>

Also see TRANS.

MEASURE    xargs keyword :MEASURE

See XARGS.

MODE    xargs keyword :MODE

See XARGS.

NAME    syntactic rules on logical names

     Examples                 Counter-Examples

     PRIMEP               91         (not a symbolp)
     F-AC-23              :CHK-LIST  (in KEYWORD package)
     1AX                  *PACKAGE*  (in the Lisp Package)
     |Prime Number|       1E3        (not a symbolp)

Many different ACL2 entities have names, e.g., functions, macros,
variables, constants, packages, theorems, theories, etc.  Package names
are strings.  All other names are symbols and may not be in the
"KEYWORD" package.  Moreover, names of functions, macros, constrained
functions, and constants, other than those that are predefined, must
not be in the "main Lisp package" (which is ("LISP" or "COMMON-LISP",
according to whether we are following CLTL1 or CLTL2).  An analogous
restriction on variables is given below.

T, nil, and all names above except those that begin with ampersand (&)
are names of variables or constants.  T, nil, and those names beginning
and ending with star (*) are constants.  All other such names are
variables.

Note that names that start with ampersand, such as &rest, may be lambda
list keywords and are reserved for such use whether or not they are in
the CLTL constant lambda-list-keywords.  (See pg 82 of CLTL2.)  That
is, these may not be used as variables.  Unlike constants, variables
may be in the main Lisp package as long as they are in the original
list of imports from that package to ACL2, the list
*common-lisp-symbols-from-main-lisp-package*, and do not belong to a
list of symbols that are potentially "global."  This latter list is the
value of *common-lisp-specials-and-constants*.

Our restrictions pertaining to the main Lisp package take into account
that some symbols, e.g., lambda-list-keywords and boole-c2, are
"special."  Permitting them to be bound could have harmful effects.  In
addition, the Common Lisp language does not allow certain manipulations
with many symbols of that package.  So, we stay away from them, except
for allowing certain variables as indicated above.

NO-THANKS    hints keyword :NO-THANKS

See HINTS.

NON-EXECUTABLE    xargs keyword :NON-EXECUTABLE

See XARGS.

NON-LINEAR-ARITHMETIC    Non-linear Arithmetic

This documentation topic is divided into two parts.  We first discuss
the practical aspect of how to use the non-linear arithmetic extension
to ACL2, and then the theory behind it.  We assume that the reader is
familiar with the material in linear-arithmetic and that on :linear
rules.

We begin our discussion of how to use non-linear arithmetic with a
simple example.  Assume that we wish to prove:

     (thm
      (implies (and (rationalp x)
                    (rationalp y)
                    (rationalp z)
                    (< 0 y)
                    (< x (* y z)))
               (< (floor x y) z)))

Note that (floor x y) <= (/ x y).  Note also that if we divide both
sides of x < (* y z) by y, since 0 < y, we obtain (/ x y) < z.  By
chaining these two inequalities together, we get the inequality we
desired to prove.

We now proceed with our example session:

     (skip-proofs
      (progn

     ; Since the truth of this theorem depends on the linear properties
     ; of floor, we will need the linear lemma:

        (defthm floor-bounds-1
            (implies (and (rationalp x)
                          (rationalp y))
                     (and (< (+ (/ x y) -1)
                             (floor x y))
                          (<= (floor x y)
                              (/ x y))))
            :rule-classes ((:linear :trigger-terms ((floor x y)))))

     ; We now disable floor, so that the linear lemma will be used.

        (in-theory (disable floor))

     ; We create five rewrite rules which we will use during non-linear
     ; arithmetic.  The necessity for these is due to one of the differences in
     ; ACL2's behaviour when non-linear arithmetic is turned on.  Although
     ; the conclusions of linear lemmas have always been rewritten before
     ; they are used, now, when non-linear arithmetic is turned on, the
     ; conclusions are rewritten under a different theory than under ``normal''
     ; rewriting.  This theory is also used in other, similar, circumstances
     ; described below.

        (defthm |arith (* -1 x)|
            (equal (* -1 x)
                   (- x)))

        (defthm |arith (* 1 x)|
            (equal (* 1 x)
                   (fix x)))

        (defthm |arith (* x (/ x) y)|
            (equal (* x (/ x) y)
                   (if (equal (fix x) 0)
                       0
                       (fix y))))

        (defthm |arith (* y x)|
            (equal (* y x)
                   (* x y)))

        (defthm |arith (fix x)|
            (implies (acl2-numberp x)
                     (equal (fix x)
                            x))))
      )  ; End skip-proofs.

     ; We disable the above rewrite rules from normal use.

     (in-theory (disable |arith (* -1 x)|
                         |arith (* 1 x)|
                         |arith (* x (/ x) y)|
                         |arith (* y x)|
                         |arith (fix x)|))

     ; We create an arithmetic-theory.  Note that we must give a quoted
     ; constant for the theory --- none of the normal theory-functions
     ; are applicable to in-arithmetic-theory.

     (in-arithmetic-theory '(|arith (* -1 x)|
                             |arith (* 1 x)|
                             |arith (* x (/ x) y)|
                             |arith (* y x)|
                             |arith (fix x)|))

     ; We turn non-linear arithmetic on.

     (set-non-linearp t)

     ; We can now go ahead and prove our theorem.

     (thm
      (implies (and (rationalp x)
                    (rationalp y)
                    (rationalp z)
                    (< 0 y)
                    (< x (* y z)))
               (< (floor x y) z)))

The above example illustrates the two practical requirements for using
non-linear arithmetic in ACL2.  First, one must set up an
arithmetic-theory.  Usually, one would not set up an arithmetic-theory
on one's own but would instead load a library book or books which do
so.  Second, one must turn the non-linear arithmetic extension on.
This one must do explicitly -- no book can do this for you.

For a brief discussion of why this is so, even though (set-non-linearp
t) is an embeddable event, see ACL2-DEFAULTS-TABLE (in
particular, the final paragraph).  (Note that (set-non-linearp t)
modifies the acl2-defaults-table.)  Also see SET-NON-LINEARP,
see EMBEDDED-EVENT-FORM, and see EVENTS.

You can also enable non-linear arithmetic with the hint :nonlinearp t.
See HINTS.  We, in fact, recommend the use of a hint which will
enable nonlinear arithmetic only when the goal has stabilized under
rewriting.  Using default-hints can make this easier.

     (defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
       (cond (stable-under-simplificationp
              (if (not (access rewrite-constant
                               (access prove-spec-var pspv :rewrite-constant)
                               :nonlinearp))
                  '(:computed-hint-replacement t :nonlinearp t)
                nil))
             ((access rewrite-constant
                      (access prove-spec-var pspv :rewrite-constant)
                      :nonlinearp)
              (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
                  '(:computed-hint-replacement t :nonlinearp nil)
                nil))
             (t nil)))

     (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
                                                   hist pspv)))

This has proven to be a helpful strategy which allows faster proof
times.

We now proceed to briefly describe the theory behind the non-linear
extension to ACL2.  In linear-arithmetic it was stated that, "[L]inear
polynomial inequalities can be combined by cross-multiplication and
addition to permit the deduction of a third inequality...."  That is, if

     0 < poly1,
     0 < poly2,

and c and d are positive rational constants, then

     0 < c*poly1 + d*poly2.

Similarly, given the above,

     0 < poly1*poly2.

In the linear arithmetic case, we are taking advantage of the facts that
multiplication by a positive rational constant does not change the sign
of a polynomial and that the sum of two positive polynomials is itself
positive.  In the non-linear arithmetic case, we are using the fact
that the product of two positive polynomials is itself positive.

For example, suppose we have the three assumptions:

     p1:  3*x*y + 7*a < 4
     p2:            3 < 2*x  or p2': 0 < -3 + 2*x
     p3:            1 < y    or p3': 0 < -1 + y,

and we wish to prove that a < 0.  As described elsewhere (see
LINEAR-ARITHMETIC), we proceed by assuming the negation of our goal:

     p4:            0 <= a,

and looking for a contradiction.

There are no cancellations which can be performed by linear arithmetic
in the above situation.  (Recall that two polynomials are cancelled
against each other only when they have the same largest unknown.)
However, p1 has a product as its largest unknown, and for each of the
factors of that product there is a poly that has that factor as a
largest unknown.  When non-linear arithmetic is enabled, ACL2 will
therefore multiply p1' and p2' obtaining

     p5:            0 < 3 + -2*x + -3*y + 2*x*y.

The addition of this polynomial will allow cancelation to continue and,
in this case, we will prove our goal.  Thus, just as ACL2 adds two
polynomials together when they have the same largest unknown of
opposite signs in order to create a new "smaller" polynomial; so ACL2
multiplies polynomials together when the product of their largest
unknowns is itself the largest unknown of another polynomial.  As the
use of :linear lemmas to further seed the arithmetic data base may
allow cancellation to proceed, so may the use of non-linear arithmetic.

This multiplication of polynomials is the other situation in which
terms are rewritten under the arithmetic-theory rather than the normal
one.  Because this may be done so often, and because the individual
factors have presumably already been rewritten, it is important that
this be done in an efficient way.  The use of a small, specialized,
theory helps avoid the repeated application of rewrite rules to already
stabilized terms.

NONLINEARP    hints keyword :NONLINEARP

See HINTS.

NORMALIZE    xargs keyword :NORMALIZE

See XARGS.

NU-REWRITER    rewriting NTH/UPDATE-NTH expressions

The rewriter contains special provisions for rewriting expressions
composed of nth, update-nth, update-nth-array, together with let
expressions and other applications of non-recursive functions or lambda
expressions.  For details see the paper "Rewriting for Symbolic
Execution of State Machine Models" by J Strother Moore.  Also see
SET-NU-REWRITER-MODE.

The "nu-rewriter" is a recent addition to the main rewrite engine in
ACL2.  Consider the expression

      (let ((s (update-nth 1 (new-a x s) s)))
        (let ((s (update-nth 2 (new-b x s) s)))
          (let ((s (update-nth 3 (new-c x s) s)))
            s)))

If the lets in this expression are expanded, a very large expression
results because of the duplicate occurrences of s:

     (update-nth 3
                 (new-c x
                        (update-nth 2
                                    (new-b x
                                           (update-nth 1
                                                       (new-a x s)
                                                       s))
                                    (update-nth 1
                                                (new-a x s)
                                                s)))
                 (update-nth 2
                             (new-b x
                                    (update-nth 1
                                                (new-a x s)
                                                s))
                             (update-nth 1
                                         (new-a x s)
                                         s))).

This expansion of the let expression can be very expensive in space and
time.  In particular, the (new-a x s) expression might be rewritten
many times.

Now imagine asking what 2nd component of the structure is.  That is,
consider

      (nth 2
           (let ((s (update-nth 1 (new-a x s) s)))
             (let ((s (update-nth 2 (new-b x s) s)))
               (let ((s (update-nth 3 (new-c x s) s)))
                 s))))

The normal ACL2 rewrite engine would answer this question by first
rewriting the arguments to the nth expression; in particular, it would
expand the nested let expression to the large nested update-nth
expression and then, using rules such as

     (defthm nth-update-nth
       (equal (nth m (update-nth n val l))
              (if (equal (nfix m) (nfix n))
                  val (nth m l))))

would reduce the expression to (new-b x (update-nth 1 (new-a x s) s)).

The purpose of the nu-rewriter is to allow simplifications like this
without first expanding the lets.  The "nu" in the name is an acronym
for "nth/update-nth".  The nu-rewriter knows how to move an nth into a
let without expanding the let and how to simplify it if it nestles up
against an update-nth.

There are four characteristics of this problem: the presence of nth,
the presence of update-nth, the use of let to provide "sequential"
updates, and the use of constant indices.  Nth and update-nth need not
occur explicitly; they may be used inside of definitions of "wrapper"
functions.

Because the nu-rewriter changes the order in which things are rewritten,
its routine use can make ACL2 unable to reproduce old proofs.  It is
therefore switched off by default.  If your application exhibits the
characteristics above, you might wish to switch the nu-rewriter on
using set-nu-rewriter-mode.

More will eventually be written about the nu-rewriter.  However, it is
described in detail in the paper cited at the beginning of this
documentation topic.

OBDD    ordered binary decision diagrams with rewriting

See BDD for information on this topic.

ORDINALS    ordinals in ACL2

Ordinals are used in ACL2 for proving termination in the admission of
recursive function definitions.  For a proof that the ACL2 ordinals are
well-founded, see PROOF-OF-WELL-FOUNDEDNESS.

The representation of ordinals changed in ACL2 Version_2.8, and is due
to Pete Manolios and Daron Vroon.  They have also defined algorithms
for ordinal arithmetic, created a library of theorems to reason about
ordinal arithmetic, and written the rest of this documentation in order
to explain this change.  We thank them for their efforts.  Although
they have provided the implementation and even modified the distributed
books and workshop books as needed, we have looked over their work and
are maintaining it (and this documentation); if there are any bugs,
they should be considered ours (Matt Kaufmann and J Moore).

A book is included for compatibility with the representation before
Version_2.8.  For books that contain events relying on the previous
ordinal implementation, insert the following lines before the first
such event:

     (include-book "ordinals/e0-ordinal" :dir :system)
     (set-well-founded-relation e0-ord-<)

The new ordinal representation is based on a slightly different version
of Cantor Normal Form than that used by the old ordinals.  An advantage
of the new representation is that it is exponentially more succinct
than the old representation.

While pre-Version_2.8 ACL2 versions provided built-in functions for
checking if an object is an ordinal and for comparing two ordinals,
they did not provide support for reasoning about and constructing
ordinals.  The books in the directory books/ordinals provide such
support.  First, they provide efficient algorithms for ordinal
arithmetic (including addition, subtraction, multiplication, and
exponentiation).  The algorithms and their complexity are described in
the following paper.

     Manolios, Panagiotis & Vroon, Daron.
     Algorithms for ordinal arithmetic.
     Baader, Franz (ed),
     19th International Conference on Automated Deduction--CADE-19.
     Pages 243-257 of LNAI, vol. 2741.  Springer-Verlag.

Second, the algorithms are mechanically verified and libraries of
theorems which can be used to automate reasoning involving the ordinals
are provided.  For details, see the following paper.

     Manolios, Panagiotis & Vroon, Daron.
     Ordinal arithmetic in ACL2.
     Kaufmann, Matt, & Moore, J Strother (eds).
     Fourth International Workshop on the ACL2 Theorem
     Prover and Its Applications (ACL2-2003),
     July, 2003.
     See `http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/'.

We now describe aspects of the above mentioned books in more detail.

The new ordering function is o< and the new ordinal recognizer is o-p.
See also natp, posp, o<=, o>, o>=, o-first-expt, o-first-coeff, o-rst,
make-ord, o-finp, and o-infp.

The old ordinals were based on the following formulation of Cantor
Normal Form:

For any ordinal, a < epsilon-0, there exist natural numbers p and n,
and ordinals a1 >= a2 >= ... >= an > 0 such that a > a1 and a = w^(a1)
+ w^(a2) + ... + w^(an) + p.

Thus, a predicate recognizing ACL2's old ordinals is given by the
following definition.

     (defun e0-ordinalp (x)
       (if (consp x)
           (and (e0-ordinalp (car x))
                (not (equal (car x) 0))
                (e0-ordinalp (cdr x))
                (or (atom (cdr x))
                    (not (e0-ord-< (car x) (cadr x)))))
         (and (integerp x)
              (>= x 0))))

The new representation is based on a corollary to the above theorem,
which we get by the left distributive property of ordinal
multiplication over ordinal addition. Thus, w^a + w^a = (w^a)2, w^a +
w^a + w^a = (w^a)3 and so forth. The corollary is as follows:

For any ordinal, a < epsilon-0, there exist natural numbers p and n,
positive integers x1, x2, ..., xn and ordinals a1 > a2 > ... > an > 0
such that a > a1 and a = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn + p.

Instead of representing an ordinal as a list of non-increasing
ordinals, we represent it as a list of exponent-coefficient pairs, such
that the exponents are strictly decreasing (see O-P).  Note
that this representation is exponentially more efficient than the old
representation.

The ordinal arithmetic functions: o+, o-, o*, and o^ are defined in the
ordinals library (in the subdirectory books/ordinals). To use them,
include the book ordinals-without-arithmetic or ordinals, depending on
whether you want the arithmetic books included or not (ordinals
includes books/arithmetic/top-with-meta). To use the old ordinals,
include the book e0-ordinal and run the command
(set-well-founded-relation e0-ord-<)

The file books/arithmetic/natp-posp is a book for reasoning about posp
and natp.  We recommend using this book if you have to reason about
posp and natp.  It is included in books/arithmetic/top, which is
included in books/arithmetic/top-with-meta, which is included in
books/ordinals/ordinals.

If you have a good reason to use the old definitions of the ordinals
(e.g., because of legacy code and theorems), then we provide a
convenient way to do this.  In the book ordinal-isomorphism we prove
that the new ordinals are order-isomorphic to the old ordinals and thus
theorems proved in one context can be directly transferred to the
other.  For an example of how to do this, look at the book defmul in
the directory books/workshops/2000/ruiz/multiset.

The ordinals books have been used to prove non-trivial theorems.  For a
good example, see the books in the directory
books/workshops/2003/sustik/support, where Matyas Sustik proves
Dickson's lemma.

Finally, many termination proofs can be carried out with weaker
orderings than the ordinals up to epsilon-0.  For example, many
inductive theorem provers only know that the lexicographic ordering on
natural numbers is well-founded.  The book lexicographic-ordering
contains a definition of such an ordering l< whose arguments are either
a list of natural numbers, or a natural number.  In the book we prove
that l< is well-founded (that is, we prove a :well-founded-relation
defthm and provide a macro llist to simplify the generation of measure
functions.  We also show how to use l< to prove that the famous
Ackermann function terminates.  Finally, since l< does something
reasonable with natural numbers, it gets along with acl2-count, the
default measure chosen by ACL2.

OTF-FLG    pushing all the initial subgoals

The value of this flag is normally nil.  If you want to prevent the
theorem prover from abandoning its initial work upon pushing the second
subgoal, set :otf-flg to t.

Suppose you submit a conjecture to the theorem prover and the system
splits it up into many subgoals.  Any subgoal not proved by other
methods is eventually set aside for an attempted induction proof.  But
upon setting aside the second such subgoal, the system chickens out and
decides that rather than prove n>1 subgoals inductively, it will
abandon its initial work and attempt induction on the originally
submitted conjecture.  The :otf-flg (Onward Thru the Fog) allows you to
override this chickening out. When :otf-flg is t, the system will push
all the initial subgoals and proceed to try to prove each,
independently, by induction.

Even when you don't expect induction to be used or to succeed, setting
the :otf-flg is a good way to force the system to generate and display
all the initial subgoals.

For defthm and thm, :otf-flg is a keyword argument that is a peer to
:rule-classes and :hints.  It may be supplied as in the following
examples; also see DEFTHM.

     (thm (my-predicate x y) :rule-classes nil :otf-flg t)

     (defthm append-assoc
       (equal (append (append x y) z)
              (append x (append y z)))
       :hints (("Goal" :induct t))
       :otf-flg t)

The :otf-flg may be supplied to defun via the xargs declare option.
When you supply an :otf-flg hint to defun, the flag is effective for
the termination proofs and the guard proofs, if any.

OVERRIDE-HINTS    a list of hints given priority in every proof attempt

This is an advanced feature, originally implmented to help system
designers to create "modes" that control the way hints are supplied to
the theorem prover.  Please see DEFAULT-HINTS for the much more
usual way to install hints that may be applied by default.

Related topics other than immediate subtopics:

     Examples:
     ACL2 !>(override-hints (w state))
     ((computed-hint-1 clause keyword-alist processor)
      (computed-hint-2 clause keyword-alist stable-under-simplificationp))

Override-hints returns a list of computed hints (see
COMPUTED-HINTS) which, unlike other computed hints, may mention the
variable KEYWORD-ALIST.

Before reading further, please see HINTS-AND-THE-WATERFALL to
review the basics of how hints are applied during a proof.  In
particular, we assume familiarity with the notion of selecting a hint
to be applied to the current goal.  If there are override-hints, that
hint selection is tentative, because if it reduced to nil after the
application of override-hints, then that hint will be skipped and the
attempt will continue for selecting an applicable hint.  (Craft your
override-hints so that :no-op t is returned in such cases instead of
nil, if you don't want the hint to be skipped.)  But we must explain
what is meant by "the application of override-hints", and we do that
now.

Suppose that there are override-hints when a hint is selected for the
current goal.  The hint object selected is a keyword-alist, which is an
alternating list of hint keywords and their values, provided either
from an explicit hint (goal-name :key1 val1 ... :keyn valn) where the
:keyi are allowed to be custom hint keywords which are expanded away
(see CUSTOM-KEYWORD-HINTS), or else is the non-nil result from
evaluating a computed hint.  Then the override-hints are applied to
that keyword-alist as follows, one at a time, in order of their
occurrence in the list of override-hints (as determined by the use of
set-override-hints and add-override-hints).  The first override-hint is
evaluated, in the usual manner of evaluating computed hints but with
KEYWORD-ALIST bound to the above keyword-alist.  That evaluation
produces a result that should also be a keyword-alist.  Then
KEYWORD-ALIST is bound to that result, and the second override-hint is
evaluated.  This process continues, and the keyword-alist returned by
the final override-hint is the one used when processing the goal at
hand.  If at any iteration the keyword-alist fails to satisfy the
predicate keyword-value-listp or contains the :ERROR hint keyword, an
error is reported.  If the final result is nil, then the hint is
discarded and the remaining hints are considered as above, regardless
of whether the tentatively selected hint object came from a computed
hint or from an explicit hint.

If finally no hint is selected for the current goal, then KEYWORD-ALIST
is bound to nil and the override-hints are applied as described above.
But note that this final step is skipped if hint selection is being
performed because stable-under-simplificationp has just become true,
rather than at the top of the waterfall.  (Otherwise the override-hints
could easily keep firing uselessly yet putting us back at the top of
the waterfall, with no change to the given goal, resulting in an
infinite loop.)

The :COMPUTED-HINT-REPLACEMENT keyword is illegal for the value of an
override-hint.  But a selected hint may be a computed hint that
evaluates to a keyword-alist beginning with prefix
:COMPUTED-HINT-REPLACEMENT val.  What value does ACL2 return for such a
computed hint in the presence of override-hints?  First, this prefix is
stripped off before passing the resulting keyword-alist to the
override-hints as described above.  If the result of applying
override-hints to that keyword-alist is not nil, then the prefix is put
back on the front of that resulting keyword-alist after doing internal
processing of the hint, including expansion of any custom keyword
hints.  Otherwise, the application of override-hints to the computed
hint is nil, so this hint is not selected after all.

*WARNING*: Unlike ordinary computed hints, a value of nil for an
override-hint is not ignored.  That is: When an ordinary computed hint
evaluates to nil, it is deemed not to apply, and the next available hint
is consulted.  But when an override-hint is evaluated, the result is
always supplied for the next binding of the variable KEYWORD-ALIST,
even if that result is nil.  If you want an override-hint to be a
no-op, return as the expression the variable KEYWORD-ALIST rather than
an expression that evaluates to nil.

This feature can be used in order to implement a form of additive hints.
Suppose for example that you want a hint that turns off generalization.
A simple but inadequate solution is:

     (add-default-hints '((quote (:do-not '(generalize)))))

The problem is that if there is any explicit hint supplied for a given
goal, then it will be the one selected, and the above will be ignored.
But suppose that the explicit hint supplied is of the form ("Subgoal
x.y" :do-not '(fertilize)).  What we would really want in this case is
to generate the hint for the indicated subgoal that binds :do-not to a
list indicating that both fertilization _and_ generalization are
disabled for that goal.  A solution is to merge, as follows.

     (add-override-hints
      '((let ((tmp (assoc-eq :do-not KEYWORD-ALIST)))
          (put-assoc-eq :do-not
                        (add-to-set-eq 'generalize
                                       (cdr tmp))
                        KEYWORD-ALIST))))

REMARKS

(1) The utilities add-override-hints, add-override-hints!,
set-override-hints, set-override-hints!, remove-override-hints, and
remove-override-hints! are also available, in complete analogy to their
default-hints versions.

(2) The distributed book hints/basic-tests.lisp illustrates the use of
override-hints and illuminates a number of corner cases; search in that
file for "Test override-hints."

(3) The distributed book hints/merge-hint.lisp provides support for
merging hints that might be useful for writers of override-hint
expressions (see the examples at the end of that file).

(4) Override-hints are used in the processing of :BACKTRACK hints (see
HINTS).

PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS    re-defining undone defpkgs

Suppose (defpkg "pkg" imports) is the most recently executed successful
definition of "pkg" in this ACL2 session and that it has since been
undone, as by :ubt.  Any future attempt in this session to define "pkg"
as a package must specify an identical imports list.

The restriction stems from the need to implement the reinstallation of
saved logical worlds as in error recovery and the :oops command.
Suppose that the new defpkg attempts to import some symbol, a::sym, not
imported by the previous definition of "pkg".  Because it was not
imported in the original package, the symbol pkg::sym, different from
a::sym, may well have been created and may well be used in some saved
worlds.  Those saved worlds are Common Lisp objects being held for you
"behind the scenes."  In order to import a::sym into "pkg" now we would
have to unintern pkg::sym, rendering those saved worlds ill-formed.  It
is because of saved worlds that we do not actually clear out a package
when it is undone.

At one point we thought it was sound to allow the new defpkg to import
a subset of the old.  But that is incorrect.  Suppose the old
definition of "pkg" imported a::sym but the new one does not.  Suppose
we allowed that and implemented it simply by setting the imports of
"pkg" to the new subset.  Then consider the conjecture (eq a::sym
pkg::sym).  This ought not be a theorem because we did not import
a::sym into "pkg".  But in fact in AKCL it is a theorem because
pkg::sym is read as a::sym because of the old imports.

PRINT-DOC-START-COLUMN    printing the one-liner

     Examples:
     (assign print-doc-start-column nil)
     (assign print-doc-start-column 17)

This state global variable controls the column in which the "one-liner"
of a formatted documentation string is printed.  Generally, when :doc
is used to print a documentation string, the name of the documented
concept is printed and then :doc tabs over to print-doc-start-column
and prints the one-liner.  If the name extends past the desired column,
:doc outputs a carriage return and then tabs over to the column.  If
print-doc-start-column is nil, :doc just starts the one-liner two
spaces from the end of the name, on the same line.  The initial value
of print-doc-start-column is 15.

PROMPT    the prompt printed by ld

The prompt printed by ACL2 conveys information about various "modes."
See DEFAULT-PRINT-PROMPT and see LD-PROMPT for details.

The prompt during raw Lisp breaks is, with most Common Lisp
implementations, adjusted by ACL2 to include the string "[RAW LISP"],
in order to reminder users not to submit ACL2 forms there; see
BREAKS.  For Lisps that seem to use the same code for printing
prompts at the top-level as in breaks, the top-level prompt is
similarly adjusted.  For Lisps with the above prompt adjustment, The
following forms may be executed in raw Lisp (i.e., after typing :q).

     (install-new-raw-prompt) ; install prompt with [RAW LISP] as described above
     (install-old-raw-prompt) ; revert to original prompt from host Common Lisp

PROOF-OF-WELL-FOUNDEDNESS    a proof that o< is well-founded on o-ps

The soundness of ACL2 rests in part on the well-foundedness of o< on
o-ps.  This can be taken as obvious if one is willing to grant that
those concepts are simply encodings of the standard mathematical
notions of the ordinals below epsilon-0 and its natural ordering
relation.  But it is possible to prove that o< is well-founded on o-ps
without having to assert any connection to the ordinals and that is
what we do here.  The book books/ordinals/proof-of-well-foundedness
carries out the proof outlined below in ACL2, using only that the
natural numbers are well-founded.

Before outlining the above mentioned proof, we note that in the
analogous documentation page of ACL2 Version_2.7, there is a proof of
the well-foundedness of e0-ord-< on e0-ordinalps, the less-than relation
and recognizer for the old ordinals (that is, for the ordinals
appearing in ACL2 up through that version).  Manolios and Vroon have
given a proof in ACL2 Version_2.7 that the current ordinals (based on
o< and o-p) are order-isomorphic to the old ordinals (based on e0-ord-<
and e0-ordinalp).  Their proof establishes that switching from the old
ordinals to the current ordinals preserves the soundness of ACL2.  For
details see their paper:

     Manolios, Panagiotis & Vroon, Daron.
     Ordinal arithmetic in ACL2.
     Kaufmann, Matt, & Moore, J Strother (eds).
     Fourth International Workshop on the ACL2 Theorem
     Prover and Its Applications (ACL2-2003),
     July, 2003.
     See `http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/'.

We now give an outline of the above mentioned proof of
well-foundedness.  We first observe three facts about o< on ordinals
that have been proved by ACL2 using only structural induction on lists.
These theorems can be proved by hand.

     (defthm transitivity-of-o<
       (implies (and (o< x y)
                     (o< y z))
                (o< x z))
       :rule-classes nil)

     (defthm non-circularity-of-o<
       (implies (o< x y)
                (not (o< y x)))
       :rule-classes nil)

     (defthm trichotomy-of-o<
       (implies (and (o-p x)
                     (o-p y))
                (or (equal x y)
                    (o< x y)
                    (o< y x)))
       :rule-classes nil)

These three properties establish that o< orders the o-ps.  To put such
a statement in the most standard mathematical nomenclature, we can
define the macro:

     (defmacro o<= (x y)
       `(not (o< ,y ,x)))

and then establish that o<= is a relation that is a simple, complete
(i.e., total) order on ordinals by the following three lemmas, which
have been proved:

     (defthm antisymmetry-of-o<=
       (implies (and (o-p x)
                     (o-p y)
                     (o<= x y)
                     (o<= y x))
                (equal x y))
       :rule-classes nil
       :hints (("Goal" :use non-circularity-of-o<)))

     (defthm transitivity-of-o<=
       (implies (and (o-p x)
                     (o-p y)
                     (o<= x y)
                     (o<= y z))
                (o<= x z))
       :rule-classes nil
       :hints (("Goal" :use transitivity-of-o<)))

     (defthm trichotomy-of-o<=
       (implies (and (o-p x)
                     (o-p y))
                (or (o<= x y)
                    (o<= y x)))
       :rule-classes nil
       :hints (("Goal" :use trichotomy-of-o<)))

Crucially important to the proof of the well-foundedness of o< on o-ps
is the concept of ordinal-depth, abbreviated od:

     (defun od (l)
       (if (o-finp l)
           0
         (1+ (od (o-first-expt l)))))

If the od of an o-p x is smaller than that of an o-p y, then x is o< y:

     (defun od-1 (x y)
       (if (o-finp x)
           (list x y)
         (od-1 (o-first-expt x) (o-first-expt y))))

     (defthm od-implies-ordlessp
       (implies (and (o-p x)
                     (< (od x) (od y)))
                (o< x y))
       :hints (("Goal"
                :induct (od-1 x y))))

Remark.  A consequence of this lemma is the fact that if s = s(1),
s(2), ... is an infinite, o< descending sequence of o-ps, then
od(s(1)), od(s(2)), ... is a "weakly" descending sequence of
non-negative integers: od(s(i)) is greater than or equal to od(s(i+1)).

_Lemma Main._  For each non-negative integer n, o< well-orders the set
of o-ps with od less than or equal to n .

      Base Case.  n = 0.  The o-ps with 0 od are the non-negative
      integers.  On the non-negative integers, o< is the same as <.

      Induction Step.  n > 0.  We assume that o< well-orders the
      o-ps with od less than n.

        If o< does not well-order the o-ps with od less than or equal to n,
        consider, D, the set of infinite, o< descending sequences of o-ps of od
        less than or equal to n.  The first element of a sequence in D has od n.
        Therefore, the o-first-expt of the first element of a sequence in D has od
        n-1.  Since o<, by IH, well-orders the o-ps with od less than n, the set
        of o-first-expts of first elements of the sequences in D has a minimal
        element, which we denote by B and which has od of n-1.

        Let k be the minimum integer such that for some infinite, o< descending
        sequence s of o-ps with od less than or equal to n, the first element of s
        has an o-first-expt of B and an o-first-coeff of k.  Notice that k is
        positive.

        Having fixed B and k, let s = s(1), s(2), ... be an infinite, o<
        descending sequence of o-ps with od less than or equal to n such that s(1)
        has a o-first-expt of B and an o-first-coeff of k.

        We show that each s(i) has a o-first-expt of B and an o-first-coeff of
        k. For suppose that s(j) is the first member of s either with o-first-expt
        B and o-first-coeff m (m neq k) or with o-first-expt B' and o-first-coeff
        B' (B' neq B). If (o-first-expt s(j)) = B', then B' has od n-1 (otherwise,
        by IH, s would not be infinite) and B' is o< B, contradicting the
        minimality of B. If 0 < m < k, then the fact that the sequence beginning
        at s(j) is infinitely descending contradicts the minimality of k. If m >
        k, then s(j) is greater than its predecessor; but this contradicts the
        fact that s is descending.

        Thus, by the definition of o<, for s to be a decreasing sequence of o-ps,
        (o-rst s(1)), (o-rst s(2)), ... must be a decreasing sequence. We end by
        showing this cannot be the case. Let t = t(1), t(2), ... be an infinite
        sequence of o-ps such that t(i) = (o-rst s(i)). Then t is infinitely
        descending. Furthermore, t(1) begins with an o-p B' that is o< B. Since t
        is in D, t(1) has od n, therefore, B' has od n-1. But this contradicts the
        minimality of B. Q.E.D.

Theorem.  o< well-orders the o-ps.  Proof.  Every infinite, o<
descending sequence of o-ps has the property that each member has od
less than or equal to the od, n, of the first member of the sequence.
This contradicts Lemma Main.  Q.E.D.

PSEUDO-TERMP    a predicate for recognizing term-like s-expressions

     Example Forms:
     (pseudo-termp '(car (cons x 'nil)))      ; has value t
     (pseudo-termp '(car x y z))              ; also has value t!
     (pseudo-termp '(delta (h x)))            ; has value t
     (pseudo-termp '(delta (h x) . 7))        ; has value nil (not a true-listp)
     (pseudo-termp '((lambda (x) (car x)) b)) ; has value t
     (pseudo-termp '(if x y 123))             ; has value nil (123 is not quoted)
     (pseudo-termp '(if x y '123))            ; has value t

If x is the quotation of a term, then (pseudo-termp x) is t.  However,
if x is not the quotation of a term it is not necessarily the case that
(pseudo-termp x) is nil.

See TERM for a discussion of the various meanings of the word
"term" in ACL2.  In its most strict sense, a term is either a legal
variable symbol, a quoted constant, or the application of an n-ary
function symbol or closed lambda-expression to n terms.  By "legal
variable symbol" we exclude constant symbols, such as t, nil, and
*ts-rational*.  By "quoted constants" we include 't (aka (quote t)),
'nil, '31, etc., and exclude constant names such as t, nil and
*ts-rational*, unquoted constants such as 31 or 1/2, and ill-formed
quote expressions such as (quote 3 4).  By "closed lambda expression"
we exclude expressions, such as (lambda (x) (cons x y)), containing
free variables in their bodies.  Terms typed by the user are translated
into strict terms for internal use in ACL2.

The predicate termp checks this strict sense of "term" with respect to
a given ACL2 logical world; See WORLD.  Many ACL2 functions,
such as the rewriter, require certain of their arguments to satisfy
termp.  However, as of this writing, termp is in :program mode and thus
cannot be used effectively in conjectures to be proved.  Furthermore,
if regarded simply from the perspective of an effective guard for a
term-processing function, termp checks many irrelevant things.  (Does
it really matter that the variable symbols encountered never start and
end with an asterisk?)  For these reasons, we have introduced the
notion of a "pseudo-term" and embodied it in the predicate
pseudo-termp, which is easier to check, does not require the logical
world as input, has :logic mode, and is often perfectly suitable as a
guard on term-processing functions.

A pseudo-termp is either a symbol, a true list of length 2 beginning
with the word quote, the application of an n-ary pseudo-lambda
expression to a true list of n pseudo-terms, or the application of a
symbol to a true list of n pseudo-termps.  By an "n-ary pseudo-lambda
expression" we mean an expression of the form (lambda (v1 ... vn)
pterm), where the vi are symbols (but not necessarily distinct legal
variable symbols) and pterm is a pseudo-termp.

Metafunctions may use pseudo-termp as a guard.

REDEF    a common way to set ld-redefinition-action

     Example and General Form:
     ACL2 !>:redef

This command sets ld-redefinition-action to '(:query . :overwrite).

This command allows redefinition of functions and other events without
undoing, but with a query that requires the user to acknowledge that the
redefinition is intentional.  To avoid that query, see REDEF!
or for more options, see LD-REDEFINITION-ACTION.

REDEF!    a common way to set ld-redefinition-action

     Example and General Form:
     ACL2 !>:redef!

This command sets ld-redefinition-action to '(:warn! . :overwrite).

This command allows redefinition of functions and other events without
undoing, but with a warning.  The command :redef is similar, but
queries the user first before doing the redefinition.  For more related
options, see LD-REDEFINITION-ACTION.

REDEF+    system hacker's redefinition command

     Example and General Form:
     ACL2 !>:redef+
     ACL2 p!>

This command is intended only for system hackers, not typical users.  It
sets ld-redefinition-action to '(:warn! . :overwrite), sets the default
defun-mode to :program, and invokes set-state-ok with value t.  It also
introduces (defttag :redef+), so that redefinition of system functions
will be permitted; see DEFTTAG.  Finally, it removes as
untouchable all variables and functions.

This command is intended for those who are modifying ACL2 source code
definitions.  Thus, note that even system functions can be redefined
with a mere warning.  Be careful!

REDEF-    turn off system hacker's redefinition command

     Example and General Form:
     ACL2 !>:redef-
     ACL2 p!>

This macro, for system hackers only, is a convenient way to reverse the
effects of :redef+.  See REDEF+.

Note that this macro starts by executing :redef+, in case some effects
of a previous :redef+ have already been removed or perhaps :redef+ had
not been done at all.

REDEFINED-NAMES    to collect the names that have been redefined

     Example and General Forms:
     (redefined-names state)

This function collects names that have been redefined in the current
ACL2 state.  :Program mode functions that were reclassified to :logic
functions are not collected, since such reclassification cannot imperil
soundness because it is allowed only when the new and old definitions
are identical.

Thus, if (redefined-names state) returns nil then no unsafe definitions
have been made, regardless of ld-redefinition-action.  See
LD-REDEFINITION-ACTION.

WARNING: This function does not report names that are not explicitly
redefined in the current logical world.  Consider for example:

     (encapsulate
      ()
      (defun foo () t)
      (local (defun foo () nil))
      (defthm foo-prop
        (equal (foo) nil)
        :rule-classes nil))

If you attempt to call certify-book in the resulting world, ACL2 will
appropriately refuse to do the certification:

     ACL2 Error in (CERTIFY-BOOK "foo" ...):  At least one command in the
     current ACL2 world was executed while the value of state global variable
     'LD-REDEFINITION-ACTION was not nil:

       (DEFUN FOO NIL T)

     Certification is therefore not allowed in this world.  You can use
     :ubt to undo back through this command; see :DOC ubt.

However, since the local redefinition of foo is gone in the
certification world, (redefined-names state) will return nil.
(Technical aside, to be ignored except for those interested in
implementation details: ACL2 inhibits certify-book in this example
because the definition of foo is the value of (global-val 'redef-seen
(w state)).)

REDUNDANT-EVENTS    allowing a name to be introduced "twice"

Sometimes an event will announce that it is "redundant".  When this
happens, no change to the logical world has occurred.  This happens
when the logical name being defined is already defined and has exactly
the same definition, from the logical point of view.  This feature
permits two independent books, each of which defines some name, to be
included sequentially provided they use exactly the same definition.

When are two logical-name definitions considered exactly the same?  It
depends upon the kind of name being defined.  See also the Notes below.

A deflabel event is never redundant.  This means that if you have a
deflabel in a book and that book has been included (without error),
then references to that label denote the point in history at which the
book introduced the label.  See the note about shifting logical names,
below.

A defun or mutual-recursion (or defuns) event is redundant if for each
function to be introduced, there has already been introduced a function
with the same name, the same formals, and syntactically identical
:guard, :measure, type declarations, stobjs declarations and body
(before macroexpansion), and an appropriate mode (see the discussion of
"appropriate modes" below).  Moreover, the order of the combined :guard
and type declarations must be the same in both cases.  Exceptions: (1)
If either definition is declared :non-executable (see XARGS),
then the two events must be identical.  (2) It is permissible for one
definition to have a :guard of t and the other to have no explicit
guard (hence, the guard is implicitly t).  (3) The :measure check is
avoided if we are skipping proofs (for example, during include-book),
and otherwise, the new definition may have a :measure of (:? v1 ...
vk), where (v1 ... vk) enumerates the variables occurring in the
measure stored for the old definition.  (4) If either the old or new
event is a mutual-recursion event, then redundancy requires that both
are mutual-recursion events that define the same set of function
symbols.

A verify-guards event is redundant if the function has already had its
guards verified.

A defaxiom or defthm event is redundant if there is already an axiom or
theorem of the given name and both the formula (after macroexpansion)
and the rule-classes are syntactically identical.  Note that a defaxiom
can make a subsequent defthm redundant, and a defthm can make a
subsequent defaxiom redundant as well.

A defconst is redundant if the name is already defined either with a
syntactically identical defconst event or one that defines it to have
the same value.

A defstobj is redundant if there is already a defstobj event with the
same name that has exactly the same field descriptors (see
DEFSTOBJ), in the same order, and with the same :renaming value if
:renaming is supplied for either event.

A defmacro is redundant if there is already a macro defined with the
same name and syntactically identical arguments, guard, and body.

A defpkg is redundant if a package of the same name with exactly the
same imports has been defined.

A deftheory is never redundant.  The "natural" notion of equivalent
deftheory forms is that the names and values of the two theory
expressions are the same.  But since most theory expressions are
sensitive to the context in which they occur, it seems unlikely to us
that two deftheorys coming from two sequentially included books will
ever have the same values.  So we prohibit redundant theory
definitions.  If you try to define the same theory name twice, you will
get a "name in use" error.

An in-theory event is never redundant because it doesn't define any
name.

A push-untouchable event is redundant if every name supplied is already
a member of the corresponding list of untouchable symbols.

A remove-untouchable event is redundant if no name supplied is a member
of the corresponding list of untouchable symbols.

A reset-prehistory event is redundant if it does not cause any change.

A set-body event is redundant if the indicated body is already the
current body.

Defdoc events are never redundant because they don't define any name.
A table event also does not define any name, but it is redundant when
it sets the value already associated with a key of the table, or when
it sets an entire table (using keyword :clear) to its existing value;
see TABLE.

An encapsulate event is redundant if and only if a syntactically
identical encapsulate has already been executed under the same
default-defun-mode, default-ruler-extenders, and
default-verify-guards-eagerness.

An include-book is redundant if the book has already been included.

_Note About Built-in (Predefined) Functions and Macros:_

Redundancy is restricted for built-in macros and functions that have
special raw Lisp code.  Such redundancy is only legal in the context of
LOCAL.  This restriction is needed for soundness, for technical reasons
omitted here (details may be found in a long comment about
redundant-events in source function chk-acceptable-defuns).

_Note About Appropriate Modes:_

Suppose a function is being redefined and that the formals, guards,
types, stobjs, and bodies are identical.  When are the modes (:program
or :logic) "appropriate?"  Identical modes are appropriate.  But what
if the old mode was :program and the new mode is :logic?  This is
appropriate, provided the definition meets the requirements of the
logical definitional principle.  That is, you may redefine "redundantly"
a :program mode function as a :logic mode function provide the measure
conjectures can be proved.  This is what verify-termination does.  Now
consider the reverse style of redefinition.  Suppose the function was
defined in :logic mode and is being identically redefined in :program
mode.  ACL2 will treat the redefinition as redundant, provided the
appropriate criteria are met (as though it were in :logic mode).

_Note About Shifting Logical Names:_

Suppose a book defines a function fn and later uses fn as a logical
name in a theory expression.  Consider the value of that theory
expression in two different sessions.  In session A, the book is
included in a world in which fn is not already defined, i.e., in a
world in which the book's definition of fn is not redundant.  In
session B, the book is included in a world in which fn is already
identically defined.  In session B, the book's definition of fn is
redundant.  When fn is used as a logical name in a theory expression,
it denotes the point in history at which fn was introduced.  Observe
that those points are different in the two sessions.  Hence, it is
likely that theory expressions involving fn will have different values
in session A than in session B.

This may adversely affect the user of your book.  For example, suppose
your book creates a theory via deftheory that is advertised just to
contain the names generated by the book.  But suppose you compute the
theory as the very last event in the book using:

     (set-difference-theories (universal-theory :here)
                              (universal-theory fn))

where fn is the very first event in the book and happens to be a defun
event.  This expression returns the advertised set if fn is not already
defined when the book is included.  But if fn were previously
(identically) defined, the theory is larger than advertised.

The moral of this is simple: when building books that other people will
use, it is best to describe your theories in terms of logical names
that will not shift around when the books are included.  The best such
names are those created by deflabel.

_Note About Unfortunate Redundancies:_

Notice that our syntactic criterion for redundancy of defun events does
not allow redefinition to take effect unless there is a syntactic change
in the definition.  The following example shows how an attempt to
redefine a function can fail to make any change.

     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defmacro mac (x) x)
     (defun foo (x) (mac x))
     (defmacro mac (x) (list 'car x))
     (defun foo (x) (mac x)) ; redundant, unfortunately; foo does not change
     (thm (equal (foo 3) 3)) ; succeeds, showing that redef of foo didn't happen

The call of macro mac was expanded away when the first definition of
foo was processed, so the new definition of mac is not seen in foo
unless foo is redefined; yet our attempt at redefinition failed!  An
easy workaround is first to supply a different definition of foo, just
before the last definition of foo above.  Then that final definition
will no longer be redundant.

The phenomenon illustrated above can occur even without macros.  Here
is a more complex example, based on one supplied by Grant Passmore.

     (defun n3 () 0)
     (defun n4 () 1)
     (defun n5 () (> (n3) (n4))) ; body is normalized to nil
     (thm (equal (n5) nil)) ; succeeds, trivially
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defun n3 () 2)

If now we execute (thm (equal (n5) nil)), it still succeeds even though
we expect (n5) = (> (n3) (n4)) = (> 2 1) = t.  That is because the body
of n5 was normalized to nil.  (Such normalization can be avoided; see
the brief discussion of :normalize in the documentation for defun.)
So, given this unfortunate situation, one might expect at this point
simply to redefine n5 using the same definition as before, in order to
pick up the new definition of n3.  Such "redefinition" would, however,
be redundant, for the same reason as in the previous example:  no
syntactic change was made to the definition.  The same workaround
applies as before: redefine n5 to be something different, and then
redefine n5 again to be as desired.

A related phenomenon can occur for encapsulate.  As explained above, an
encapsulate event is redundant if it is identical to one already in the
database.  Consider then the following contrived example.

     (encapsulate () (defun foo (x) x))
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defun foo (x) (cons x x))
     (encapsulate () (defun foo (x) x)) ; redundant!

The last encapsulate event is redundant because it meets the criterion
for redundancy: it is identical to the earlier encapsulate event.  A
workaround can be to add something trivial to the encapsulate, for
example:

     (encapsulate ()
       (deflabel try2) ; ``Increment'' to try3 next time, and so on.
       (defun foo (x) x))

The examples above are suggestive but by no means exhaustive.  Consider
the following example.

     (defstub f1 () => *)
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defun f1 () 3)
     (defstub f1 () => *) ; redundant -- has no effect

The reason that the final defstub is redundant is that defstub is a
macro that expands to a call of encapsulate; so this is very similar to
the immediately preceding example.

REORDER    hints keyword :REORDER

See HINTS.

RESTRICT    hints keyword :RESTRICT

See HINTS.

REWRITE-STACK-LIMIT    limiting the stack depth of the ACL2 rewriter

ACL2 users can create rules of class :rewrite (see RULE-CLASSES)
that have the potential of causing an infinite loop in the ACL2
rewriter.  This could lead to Lisp stack overflows and even
segmentation faults.  For this reason, the depth of certain calls of
functions in the ACL2 rewriter is limited by default using the value of
the form (rewrite-stack-limit (w state)).  To see the limit in action,
execute the following forms.

     (defthm app-assoc-1
       (equal (append (append x y) z)
              (append x y z)))
     (defthm app-assoc-2
       (equal (append x y z)
              (append (append x y) z)))
     (thm (equal (append a b c) xxx)
          ; try without these hints to see a slightly different error message
          :hints (("Goal" :do-not '(preprocess))))

The ensuing error message shows a stack of one greater than the value of
(rewrite-stack-limit (w state)), which by default is the value of the
constant *default-rewrite-stack-limit*.  The error message also explains
how to use :brr t and (cw-gstack) to find looping rewrite rules.

This limit can be changed; see SET-REWRITE-STACK-LIMIT.

For a related limit, see BACKCHAIN-LIMIT.

SAVING-AND-RESTORING    saving and restoring your logical state

One normally works on an ACL2-based project by developing books, which
can then be included when continuing on that project in later ACL2
sessions; see INCLUDE-BOOK.  However, this approach can be
time-consuming when there are very large collections of books to be
included.  See see SAVE-EXEC for the description of a utility
that saves your ACL2 state so that you can immediately re-start later
in that same state.

SHOW-BODIES    show the potential definition bodies

     Examples:
     (show-bodies foo)
     :show-bodies foo

A definition made using defun installs a so-called "body" of a function
symbol, as do certain :definition rules.  Such bodies are used in a
number of ways, including the application of :expand hints; see
DEFINITION, in particular the discussion of "body" there, and see
HINTS for a discussion of the :expand hint.  Also see
SET-BODY for how to change which of the available definitions (among
the original definition and appropriate :definition rules) is the one
that provides the body.  The show-bodies command displays the available
such bodies in an appropriate format, starting with the one that is
currently used as the body.

     General Forms:
     (show-bodies function-symbol)
     :show-bodies function-symbol

SIGNATURE    how to specify the arity of a constrained function

     Examples:
     ((hd *) => *)
     ((printer * state) => (mv * * state))
     ((mach * mach-state * state) => (mv * mach-state)

     General Form:
     ((fn ...) => *)
     ((fn ...) => stobj)
     or
     ((fn ...) => (mv ...))

where fn is the constrained function symbol, ... is a list of asterisks
and/or the names of single-threaded objects and stobj is a
single-threaded object name.  ACL2 also supports an older style of
signature described below after we describe the preferred style.

Signatures specify three syntactic aspects of a function symbol: (1)
the "arity" or how many arguments the function takes, (2) the
"multiplicity" or how many results it returns via MV, and (3) which of
those arguments and results are single-threaded objects and which
objects they are.

For a discussion of single-threaded objects, see STOBJ.  For
the current purposes it is sufficient to know that every single-
threaded object has a unique symbolic name and that state is the name
of the only built-in single-threaded object.  All other stobjs are
introduced by the user via defstobj.  An object that is not a
single-threaded object is said to be "ordinary."

The general form of a signature is ((fn x1 ... xn) => val).  So a
signature has two parts, separated by the symbol "=>".  The first part,
(fn x1 ... xn), is suggestive of a call of the constrained function.
The number of "arguments," n, indicates the arity of fn.  Each xi must
be a symbol.  If a given xi is the symbol "*" then the corresponding
argument must be ordinary.  If a given xi is any other symbol, that
symbol must be the name of a single-threaded object and the
corresponding argument must be that object.  No stobj name may occur
twice among the xi.

The second part, val, of a signature is suggestive of a term and
indicates the "shape" of the output of fn.  If val is a symbol then it
must be either the symbol "*" or the name of a single-threaded object.
In either case, the multiplicity of fn is 1 and val indicates whether
the result is ordinary or a stobj.  Otherwise, val is of the form (mv
y1 ... yk), where k > 1.  Each yi must be either the symbol "*" or the
name of a stobj.  Such a val indicates that fn has multiplicity k and
the yi indicate which results are ordinary and which are stobjs.  No
stobj name may occur twice among the yi.

Finally, a stobj name may appear in val only if appears among the xi.

Before ACL2 supported user-declared single-threaded objects there was
only one single-threaded object: ACL2's built-in notion of state.  The
notion of signature supported then gave a special role to the symbol
state and all other symbols were considered to denote ordinary objects.
ACL2 still supports the old form of signature, but it is limited to
functions that operate on ordinary objects or ordinary objects and
state.

     Old-Style General Form:
     (fn formals result)

where fn is the constrained function symbol, formals is a suitable list
of formal parameters for it, and result is either a symbol denoting
that the function returns one result or else result is an mv
expression, (mv s1 ... sn), where n>1, each si is a symbol, indicating
that the function returns n results.  At most one of the formals may be
the symbol STATE, indicating that corresponding argument must be ACL2's
built-in state.  If state appears in formals then state may appear once
in result.  All "variable symbols" other than state in old style
signatures denote ordinary objects, regardless of whether the symbol
has been defined to be a single-threaded object name!

We also support a variation on old style signatures allowing the user
to declare which symbols (besides state) are to be considered
single-threaded object names.  This form is

     (fn formals result :stobjs names)

where names is either the name of a single-threaded object or else is a
list of such names.  Every name in names must have been previously
defined as a stobj via defstobj.

SIMPLE    :definition and :rewrite rules used in preprocessing

     Example of simple rewrite rule:
     (equal (car (cons x y)) x)

     Examples of simple definition:
     (defun file-clock-p (x) (integerp x))
     (defun naturalp (x)
       (and (integerp x) (>= x 0)))

The theorem prover output sometimes refers to "simple" definitions and
rewrite rules.  These rules can be used by the preprocessor, which is
one of the theorem prover's "processes" understood by the :do-not hint;
see HINTS.

The preprocessor expands certain definitions and uses certain rewrite
rules that it considers to be "fast".  There are two ways to qualify as
fast.  One is to be an "abbreviation", where a rewrite rule with no
hypotheses or loop stopper is an "abbreviation" if the right side
contains no more variable occurrences than the left side, and the right
side does not call the functions if, not or implies.  Definitions and
rewrite rules can both be abbreviations; the criterion for definitions
is similar, except that the definition must not be recursive.  The
other way to qualify applies only to a non-recursive definition, and
applies when its body is a disjunction or conjunction, according to a
perhaps subtle criterion that is intended to avoid case splits.

SPECIOUS-SIMPLIFICATION    nonproductive proof steps

Occasionally the ACL2 theorem prover reports that the current goal
simplifies to itself or to a set including itself.  Such
simplifications are said to be "specious" and are ignored in the sense
that the theorem prover acts as though no simplification were possible
and tries the next available proof technique.  Specious simplifications
are almost always caused by forcing.

The simplification of a formula proceeds primarily by the local
application of :rewrite, :type-prescription, and other rules to its
various subterms.  If no rewrite rules apply, the formula cannot be
simplified and is passed to the next ACL2 proof technique, which is
generally the elimination of destructors.  The experienced ACL2 user
pays special attention to such "maximally simplified" formulas; the
presence of unexpected terms in them indicates the need for additional
rules or the presence of some conflict that prevents existing rules
from working harmoniously together.

However, consider the following interesting possibility: local rewrite
rules apply but, when applied, reproduce the goal as one of its own
subgoals.  How can rewrite rules apply and reproduce the goal?  Of
course, one way is for one rule application to undo the effect of
another, as when commutativity is applied twice in succession to the
same term.  Another kind of example is when two rules conflict and
undermine each other.  For example, under suitable hypotheses, (length
x) might be rewritten to (+ 1 (length (cdr x))) by the :definition of
length and then a :rewrite rule might be used to "fold" that back to
(length x).  Generally speaking the presence of such "looping" rewrite
rules causes ACL2's simplifier either to stop gracefully because of
heuristics such as that described in the documentation for loop-stopper
or to cause a stack overflow because of indefinite recursion.

A more insidious kind of loop can be imagined: two rewrites in
different parts of the formula undo each other's effects "at a
distance," that is, without ever being applied to one another's output.
For example, perhaps the first hypothesis of the formula is simplified
to the second, but then the second is simplified to the first, so that
the end result is a formula propositionally equivalent to the original
one but with the two hypotheses commuted.  This is thought to be
impossible unless forcing or case-splitting occurs, but if those
features are exploited (see FORCE and see CASE-SPLIT)
it can be made to happen relatively easily.

Here is a simple example.  Declare foo to be a function of one argument
returning one result:

     (defstub p1 (x) t)

Prove the following silly rule:

     (defthm bad
       (implies (case-split (p1 x))
                (p1 x)))

Now suppose we try the following.

     (thm (p1 x))

The rewrite rule bad will rewrite (p1 x) to t, but it will be unable to
prove the hypothesis (case-split (p1 x)).  As a result, the prover will
spawn a new goal, to prove (p1 x).  However, since this new goal is the
same as the original goal, ACL2 will recognize the simplification as
_specious_ and consider the attempted simplification to have failed.

In other words, despite the rewriting, no progress was made!  In more
common cases, the original goal may simplify to a set of subgoals, one
of which includes the original goal.

If ACL2 were to adopt the new set of subgoals, it would loop
indefinitely.  Therefore, it checks whether the input goal is a member
of the output subgoals.  If so, it announces that the simplification is
"specious" and pretends that no simplification occurred.

"Maximally simplified" formulas that produce specious simplifications
are maximally simplified in a very technical sense: were ACL2 to apply
every applicable rule to them, no progress would be made.  Since ACL2
can only apply every applicable rule, it cannot make further progress
with the formula.  But the informed user can perhaps identify some rule
that should not be applied and make it inapplicable by disabling it,
allowing the simplifier to apply all the others and thus make progress.

When specious simplifications are a problem it might be helpful to
disable all forcing (including case-splits) and resubmit the formula to
observe whether forcing is involved in the loop or not.  See
FORCE.  The commands

     ACL2 !>:disable-forcing
     and
     ACL2 !>:enable-forcing

disable and enable the pragmatic effects of both force and case-split.
If the loop is broken when forcing is disabled, then it is very likely
some forced hypothesis of some rule is "undoing" a prior
simplification.  The most common cause of this is when we force a
hypothesis that is actually false but whose falsity is somehow
temporarily hidden (more below).  To find the offending rule, compare
the specious simplification with its non-specious counterpart and look
for rules that were speciously applied that are not applied in the
non-specious case.  Most likely you will find at least one such rule
and it will have a forced hypothesis.  By disabling that rule, at least
for the subgoal in question, you may allow the simplifier to make
progress on the subgoal.