This is documentation for ACL2 Version 5.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

HINTS    advice to the theorem proving process

     Examples:
     The following :hints value is nonsensical.  Nevertheless, it
     illustrates all of the available hint keywords except the
     ``custom keywords'' (see CUSTOM-KEYWORD-HINTS) definable
     by the user.

     :hints (("Goal"
              :do-not-induct t
              :do-not '(generalize fertilize)
              :expand ((assoc x a)
                       :lambdas
                       (:free (y) (:with member (member y z))))
              :restrict ((<-trans ((x x) (y (foo x)))))
              :hands-off (length binary-append)
              :in-theory (set-difference-theories
                           (current-theory :here)
                           '(assoc))
              :induct (and (nth n a) (nth n b))
              :use ((:instance assoc-of-append
                               (x a) (y b) (z c))
                    (:functional-instance
                      (:instance p-f (x a) (y b))
                      (p consp)
                      (f assoc)))
              :bdd (:vars (c a0 b0 a1 b1) :prove nil :bdd-constructors (cons))
              :clause-processor (:function cl-proc :hint (my-hint clause))
              :instructions (:x :prove)
              :cases ((true-listp a) (consp a))
              :by (:instance rev-rev (x (cdr z)))
              :nonlinearp t
              :backchain-limit-rw 3
              :reorder (4 7 2)
              :case-split-limitations (20 10)
              :no-op t
              :no-thanks t
              :error ("Bad value ~x0." 123)
              :or (hint-kwd-alist-1 ... hint-kwd-alist-k)
              :rw-cache-state nil
              :backtrack (my-computed-hint clause processor clause-list)))

A very common hint is the :use hint, which in general takes as its
value a list of "lemma instances" (see LEMMA-INSTANCE) but
which allows a single lemma name as a special case:

     :hints (("[1]Subgoal *1/1.2'" :use lemma23))

ACL2 also provides "custom keyword" hints (see
CUSTOM-KEYWORD-HINTS) and even more general "computed hints" for the
advanced user (see COMPUTED-HINTS).

Only the first hint applicable to a goal, as specified in the
user-supplied list of :hints followed by the default hints (see
DEFAULT-HINTS-TABLE), will be applied to that goal.  For an advanced
exception, see OVERRIDE-HINTS.  For a detailed discussion of
how hints fit into the ACL2 waterfall, see
HINTS-AND-THE-WATERFALL.  For examples of the sophisticated use of
hints, primarily for experts, see distributed book
books/hints/basic-tests.lisp.

Background: Hints are allowed in all events that use the theorem
prover.  During defun events there are two different uses of the
theorem prover: one to prove termination and another to verify the
guards.  To pass a hint to the theorem prover during termination proofs,
use the :hints keyword in the defun's xargs declaration.  To pass a
hint to the theorem prover during the guard verification portion of
admitting a defun, use the :guard-hints keyword in the defun's xargs
declaration.  The verify-guards event and the defthm event also use the
theorem prover.  To pass hints to them, use the :hints keyword argument
to the event.

     General Form of Common :hints:
       ((goal-spec :key1 val1 ... :keyn valn)
        ...
        (goal-spec :key1 val1 ... :keyn valn))

where goal-spec is as described elsewhere (see GOAL-SPEC) and
the keys and their respective values are shown below with their
interpretations.  (We also provide "computed hints" but discuss them
separately; see COMPUTED-HINTS.)

:DO-NOT-INDUCT
Value is t, :otf-flg-override, :otf, name or nil, indicating whether
induction is permitted under the specified goal.  If value is t or
:otf-flg-override, then the attempt to apply induction to the indicated
goal or any subgoal under the indicated goal will immediately cause the
theorem prover to report failure, except that if :otf-flg t is
specified (see OTF-FLG) and value is t, then the proof will
continue until the time at which the goal pushed for induction is
finally considered.  The latter behavior is also what occurs if value
is :otf.  Thus, any non-nil value requires the indicated goal to be
proved entirely by simplification, destructor elimination, and the other
"waterfall" processes.  Induction to prove the indicated goal (or any
subgoal) is not permitted.  See however the :induct hint below.  If
value is a symbol other than t, :otf-flg-override, :otf or nil, the
theorem prover will give a "bye" to any subgoal that would otherwise be
attacked with induction.  This will cause the theorem prover to fail
eventually but will collect the necessary subgoals.  If value is nil,
this hint means induction is permitted.  Since that is the default,
there is no reason to use the value nil.  Note that a :do-not-induct
hint is ignored for any goal on which an :induct hint is supplied.  For
an advanced example of the use of value :otf with override-hints, see
distributed book books/hints/basic-tests.lisp.

:DO-NOT
Value is a term having at most the single free variable world, which
when evaluated (with world bound to the current ACL2 logical world)
produces a list of symbols that is a subset of the list

     (preprocess ;propositional logic, simple rules
      simplify   ;as above plus rewriting, linear arithmetic
      eliminate-destructors
      fertilize  ;use of equalities
      generalize
      eliminate-irrelevance).

The hint indicates that the "processes" named should not be used at or
below the goal in question.  Thus, to prevent generalization and
fertilization, say, include the hint

     :do-not '(generalize fertilize)

If value is a single symbol, as in

     :do-not generalize,

it is taken to be '(value).

:EXPAND
Value is a true list of terms, each of which is of one of the forms
(let ((v1 t1)...) b) or (fn t1 ... tn), where fn is a defined function
symbol with formals v1, ..., vn, and body b.  Such a term is said to be
"expandable:" it can be replaced by the result of substituting the ti's
for the vi's in b.  The terms listed in the :expand hint are expanded
when they are encountered by the simplifier while working on the
specified goal or any of its subgoals.  We permit value to be a single
such term instead of a singleton list.  *Remarks*: (1) Allowed are
"terms" of the form (:free (var1 var2 ...  varn) pattern) where the
indicated variables are distinct and pattern is a term.  Such "terms"
indicate that we consider the indicated variables to be instantiatable,
in the following sense: whenever the simplifier encounters a term that
can be obtained from pattern by instantiating the variables (var1 var2
...  varn), then it expands that term.  (2) Also allowed are "terms" of
the form (:with name term), where name is a function symbol, a macro
name that denotes a function symbol (see MACRO-ALIASES-TABLE),
or a rune.  The corresponding rule of class :rewrite, which is often a
definition rule but need not be, is then used in place of the current
body for the function symbol of term; see SHOW-BODIES and see
SET-BODY.  If the rule is of the form (implies hyp (equiv lhs
rhs)), then after matching lhs to the current term in a context that is
maintaining equivalence relation equiv, ACL2 will replace the current
term with (if hyp rhs (hide term)), or just rhs if the rule is just
(equal lhs rhs).  (3) A combination of both :free and :with, as
described above, is legal.  (4) The term :LAMBDAS is treated specially.
It denotes the list of all lambda applications (i.e., let expressions)
encountered during the proof.  Conceptually, this use of :LAMBDAS tells
ACL2 to treat lambda applications as a notation for substitutions,
rather than as function calls whose opening is subject to the ACL2
rewriter's heuristics (specifically, not allowing lambda applications
to open when they introduce "too many" if terms).

:HANDS-OFF
Value is a true list of function symbols or lambda expressions,
indicating that under the specified goal applications of these
functions are not to be rewritten.  Note however that subterms will
still be rewritten; see HIDE if that is not what is intended.
(The distributed book books/clause-processors/autohide.lisp from Jared
Davis may also be helpful in that case.) Value may also be a single
function symbol or lambda expression instead of a list.

:IN-THEORY
Value is a "theory expression," i.e., a term having at most the single
free variable world which when evaluated (with world bound to the
current ACL2 logical world (see WORLD)) will produce a theory
to use as the current theory for the goal specified.  See
THEORIES.

Note that an :IN-THEORY hint will always be evaluated relative to the
current ACL2 logical world, not relative to the theory of a previous
goal.  Consider the following example.

     (defthm prop
       (p (f (g x)))
       :hints (("Goal"      :in-theory (disable f))
               ("Subgoal 3" :in-theory (enable  g))))

Consider in particular the theory in effect at Subgoal 3.  This call of
the enable macro enables g relative to the current-theory of the
current logical world, _not_ relative to the theory produced by the
hint at Goal.  Thus, the disable of f on behalf of the hint at Goal
will be lost at Subgoal 3, and f will be enabled at Subgoal 3 if was
enabled globally when prop was submitted.

:INDUCT
Value is either t or a term containing at least one recursively defined
function symbol; if t, this hint indicates that the system should
proceed to apply its induction heuristic to the specified goal produced
(without trying simplification, etc.); if value is a term other than t,
then not only should the system apply induction immediately, but it
should analyze value rather than the goal to generate its induction
scheme.  Merging and the other induction heuristics are applied.  Thus,
if value contains several mergeable inductions, the "best" will be
created and chosen.  E.g., the :induct hint

      (and (nth i a) (nth j a))

suggests simultaneous induction on i, j, and a.

If both an :induct and a :do-not-induct hint are supplied for a given
goal then the indicated induction is applied to the goal and the
:do-not-induct hint is inherited by all subgoals generated.

:USE
Value is a lemma-instance or a true list of lemma-instances, indicating
that the propositions denoted by the instances be added as hypotheses
to the specified goal.  See LEMMA-INSTANCE.  Note that :use
makes the given instances available as ordinary hypotheses of the
formula to be proved.  The :instance form of a lemma-instance permits
you to instantiate the free variables of previously proved theorems any
way you wish; but it is up to you to provide the appropriate
instantiations because once the instances are added as hypotheses their
variables are no longer instantiable.  These new hypotheses participate
fully in all subsequent rewriting, etc.  If the goal in question is in
fact an instance of a previously proved theorem, you may wish to use
:by below.  Note that theories may be helpful when employing :use
hints; see MINIMAL-THEORY.

Note that if the value is the name of a function symbol introduced by
defun, then the "normalized" body of that definition is used, for which
ACL2 has propagated IF tests upward.  This behavior differs from that
provided by a :by hint, where the original body of the definition is
used.

:BDD
This hint indicates that ordered binary decision diagrams (BDDs) with
rewriting are to be used to prove or simplify the goal.  See
BDD for an introduction to the ACL2 BDD algorithm.

Value is a list of even length, such that every other element, starting
with the first, is one of the keywords :vars, :bdd-constructors,
:prove, or :literal.  Each keyword that is supplied should be followed
by a value of the appropriate form, as shown below; for others, a
default is used.  Although :vars must always be supplied, we expect
that most users will be content with the defaults used for the other
values.

:vars -- A list of ACL2 variables, which are to be treated as Boolean
variables.  The prover must be able to check, using trivial reasoning
(see TYPE-SET), that each of these variables is Boolean in the
context of the current goal.  Note that the prover will use very simple
heuristics to order any variables that do not occur in :vars (so that
they are "greater than" the variables that do occur in :vars), and
these heuristics are often far from optimal.  In addition, any
variables not listed may fail to be assumed Boolean by the prover,
which is likely to seriously impede the effectiveness of ACL2's BDD
algorithm.  Thus, users are encouraged _not_ to rely on the default
order, but to supply a list of variables instead.  Finally, it is
allowed to use a value of t for vars.  This means the same as a nil
value, except that the BDD algorithm is directed to fail unless it can
guarantee that all variables in the input term are known to be Boolean
(in a sense discussed elsewhere; see BDD-ALGORITHM).

:literal -- An indication of which part of the current goal should
receive BDD processing.  Possible values are:

       :all     treat entire goal as a single literal (the default)
       :conc    process the conclusion
       n        process the hypothesis with index n (1, 2, ...)

:bdd-constructors -- When supplied, this value should be a list of
function symbols in the current ACL2 world; it is (cons) by default,
unless :bdd-constructors has a value in the acl2-defaults-table by
default, in which case that value is the default.  We expect that most
users will be content with the default.  See BDD-ALGORITHM for
information about how this value is used.

:prove -- When supplied, this value should be t or nil; it is t by
default.  When the goal is not proved and this value is t, the entire
proof will abort.  Use the value nil if you are happy to the proof to
go on with the simplified term.

:CLAUSE-PROCESSOR

Value specifies the application of a user-defined simplifier to the
current goal.  See CLAUSE-PROCESSOR, which provides necessary
background and hint syntax.  Also see
DEFINE-TRUSTED-CLAUSE-PROCESSOR for a discussion of "trusted
clause-processors":  goal-level simplifiers that may be external to
ACL2 and do not need to be proved correct in ACL2.

You can see all current :clause-processor rules by issuing the command
(print-clause-processor-rules), and you can see the names of all trusted
clause-processors by issuing the command (table
trusted-clause-processor-table).

:INSTRUCTIONS

Value is a list of proof-checker instructions; see INSTRUCTIONS.
Unlike other hint keywords described here, this one is actually a custom
keyword hint (see CUSTOM-KEYWORD-HINTS) that generates a
suitable :clause-processor hint.

:CASES
Value is a non-empty list of terms.  For each term in the list, a new
goal is created from the current goal by assuming that term; and also,
in essence, one additional new goal is created by assuming all the
terms in the list false.  We say "in essence" because if the
disjunction of the terms supplied is a tautology, then that final goal
will be a tautology and hence will in fact never actually be created.

:BY
Value is a lemma-instance, nil, or a new event name. If the value is a
lemma-instance (see LEMMA-INSTANCE), then it indicates that the
goal (when viewed as a clause) is either equal to the proposition
denoted by the instance, or is subsumed by that proposition when both
are viewed as clauses.  To view a formula as a clause, union together
the negations of the hypotheses and add the conclusion.  For example,

     (IMPLIES (AND (h1 t1) (h2 t2)) (c t1))

may be viewed as the clause

     {~(h1 t1) ~(h2 t2) (c t1)}.

Clause c1 is "subsumed" by clause c2 iff some instance of c2 is a
subset of c1.  For example, the clause above is subsumed by {~(h1 x) (c
x)}, which when viewed as a formula is (implies (h1 x) (c x)).

Note that if the value is the name of a function symbol introduced by
defun, then the original form of the body of that definition is used.
This behavior differs from that provided by a :use hint, where the
so-called "normalized" body, for which ACL2 has propagated IF tests
upward.

If the value is nil or a new name, the prover does not even attempt to
prove the goal to which this hint is attached.  Instead the goal is
given a "bye", i.e., it is skipped and the proof attempt continues as
though the goal had been proved.  If the prover terminates without
error then it reports that the proof would have succeeded had the
indicated goals been proved and it prints an appropriate defthm form to
define each of the :by names.  The "name" nil means "make up a name."
Here is an example (admittedly contrived for illustration purposes).

     ACL2 !>(thm (equal (append (append x y) z)
                        (append x y z))
                 :hints (("Subgoal *1/2'" :by nil)))

     Name the formula above *1.

     [[... output omitted here ...]]

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

     Subgoal *1/2'
     (IMPLIES (AND (CONSP X)
                   (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                          (APPEND (CDR X) Y Z)))
              (EQUAL (APPEND (APPEND X Y) Z)
                     (APPEND X Y Z))).

     But we have been asked to pretend that this goal is subsumed by the
     yet-to-be-proved |THM Subgoal *1/2'|.

     Subgoal *1/1
     [[... proof goes on; further output omitted here ...]]

The system does not attempt to check the uniqueness of the :by names
(supplied or made up), since by the time those goals are proved the
namespace will be cluttered still further.  Therefore, the final list
of "appropriate" defthm forms may be impossible to admit without some
renaming by the user.  If you must invent new names, remember to
substitute the new ones for the old ones in the :by hints themselves.

:RESTRICT
Warning: This is a sophisticated hint, suggested by Bishop Brock, that
is intended for advanced users.  In particular, :restrict hints are
ignored by the preprocessor, so you might find it useful to give the
hint :do-not '(preprocess) when using any :restrict hints, at least if
the rules in question are abbreviations (see SIMPLE).

Value is an association list.  Its members are of the form (x subst1
subst2 ...), where: x is either (1) a rune whose car is :rewrite or
:definition or (2) an event name corresponding to one or more such
runes; and (subst1 subst2 ...) is a non-empty list of substitutions,
i.e., of association lists pairing variables with terms.  First
consider the case that x is a :rewrite or :definition rune.  Recall
that without this hint, the rule named x is used by matching its
left-hand side (call it lhs) against the term currently being
considered by the rewriter, that is, by attempting to find a
substitution s such that the instantiation of lhs using s is equal to
that term.  If however the :restrict hint contains (x subst1 subst2
...), then this behavior will be modified by restricting s so that it
must extend subst1; and if there is no such s, then s is restricted so
that it must extend subst2; and so on, until the list of substitutions
is exhausted.  If no such s is found, then the rewrite or definition
rule named x is not applied to that term.  Finally, if x is an event
name corresponding to one or more :rewrite or :definition runes (that
is, x is the "base symbol" of such runes; see RUNE), say runes
r1, ... rn, then the meaning is the same except that (x subst1 subst2
...) is replaced by (ri subst1 subst2 ...) for each i.  Once this
replacement is complete, the hint may not contain two members whose car
is the same rune.

Note that the substitutions in :restrict hints refer to the variables
actually appearing in the goals, not to the variables appearing in the
rule being restricted.

Here is an example, supplied by Bishop Brock.  Suppose that the
database includes the following rewrite rule, which is probably kept
disabled.  (We ignore the question of how to prove this rule.)

     cancel-<-*$free:
     (implies (and (rationalp x)
                   (rationalp y)
                   (rationalp z))
              (equal (< y z)
                     (if (< x 0)
                         (> (* x y) (* x z))
                       (if (> x 0)
                           (< (* x y) (* x z))
                         (hide (< y z))))))

Then ACL2 can prove the following theorem (unless other rules get in
the way), essentially by multiplying both sides by x.

     (thm
       (implies (and (rationalp x)
                     (< 1 x))
                (< (/ x) 1))
       :hints
       (("Goal"
         :in-theory (enable cancel-<-*$free)
         :restrict ((cancel-<-*$free ((x x) (y (/ x)) (z 1)))))))

The :restrict hint above says that the variables x, y, and z in the
rewrite rule cancel-<-*$free above should be instantiated respectively
by x, (/ x), and 1.  Thus (< y z) becomes (< (/ x) 1), and this
inequality is replaced by the corresponding instance of the
right-hand-side of cancel-<-*$free.  Since the current conjecture
assumes (< 1 x), that instance of the right-hand side simplifies to

     (< (* x (/ x)) (* x 1))

which in turn simplifies to (< 1 x), a hypothesis in the present
theorem.

:NONLINEARP
Value is t or nil, indicating whether non-linear-arithmetic is active.
The default value is nil.  See NON-LINEAR-ARITHMETIC.

:BACKCHAIN-LIMIT-RW
Value is a natural number or nil, indicating the level of backchaining
for rewrite, meta, and linear rules.  This overrides, for the current
goal and (as with :in-theory hints) descendent goals, the default
backchain-limit (see SET-BACKCHAIN-LIMIT).

:REORDER
Value is a list of positive integers without duplicates, corresponding
to the numbering of subgoals generated for the goal-spec, say "G.k"
down to "G.1".  Those subgoals are reordered so that if value is (n1 n2
... nk), then the goal now numbered "G.k" will be the goal originally
numbered "G.n1"; the goal now numbered "G.k-1" will be the goal
formerly numbered "G.n2"; and so on, down the list of ni, after which
the goals not yet printed are printed in their original order.

:CASE-SPLIT-LIMITATIONS
Value is the same as for set-case-split-limitations.  The simplifier
will behave as though the value had instead been supplied to
set-case-split-limitations; see SET-CASE-SPLIT-LIMITATIONS.
This behavior will persist through subgoals unless overridden by another
:CASE-SPLIT-LIMITATIONS hint.

:NO-OP
Value is any object and is irrelevant.  This hint does nothing.  But
empty hints, such as ("Goal"), are illegal and there are occasions,
especially when writing custom keyword hints (see
CUSTOM-KEYWORD-HINTS) and computed hints (see COMPUTED-HINTS)
where it is convenient to be able to generate a non-empty no-op hint.
The standard idiom is ("Goal" :NO-OP T) but the T is completely
ignored.  Unlike other hint keywords, multiple occurrences of the
keyword :NO-OP are tolerated.

:NO-THANKS
Value is any object.  This hint does nothing, except that if value is
non-nil then the usual "[Note:  A hint was supplied... Thanks!]" is not
printed.

:ERROR
Value is typically a "fmt message" to be printed by the fmt
tilde-directive ~@ but may be any object.  The effect of this hint is
to cause an error when the hint is translated.  There is no reason to
include an :ERROR hint in any user-typein, since it will only cause an
error when the form is evaluated.  :ERROR hints are useful in the
definition of functions that generate custom keyword hints
(custom-keyword-hints) and computed hints (computed-hints).  For
example, if you wish to define a custom keyword hint :my-hint val and
you wish the hint to signal an error if there is something
inappropriate about val in the context of the hint, use the following
code to generate the hint

     (list :ERROR (cons "Your specified value, ~x0, is inappropriate"
                        (list (cons #0 val))))

which is equivalent to

     (list :ERROR (msg "Your specified value, ~x0, is inappropriate"
                       val))

which, if val has the value 123, would evaluate to the hint

     (:ERROR ("Your specified value, ~x0, is inappropriate" (#0 . 123))).

Note that any time an :ERROR keyword is produced during hint processing,
including iterations of the expansions of custom keyword hints or of
override-hints, an error will occur.

:OR
Value is a list (kwd-val-listp-1 ... kwd-val-listp-k), where each
kwd-val-listp-i is a list satisfying keyword-value-listp, i.e., an
alternating list of keywords and values.  This hint causes an attempt to
prove the specified goal using hints kwd-val-listp-i in sequence (first
kwd-val-listp-1, then kwd-val-listp-2, and so on), until the first of
these succeeds.  If none succeeds, then the prover proceeds after
heuristically choosing the "best" result, taking into account the goals
pushed in each case for proof by induction.

The following (contrived but illustrative example illustrates how :or
hints work.

       ACL2 !>(thm (f x)
                   :hints
                   (("Goal"
                     :expand ((nth x 3))
                     :or ((:in-theory (disable car-cons))
                          (:use cdr-cons :in-theory (enable append)))
                     :do-not '(generalize))))

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

       The :OR hint for Goal gives rise to two disjunctive branches.  Proving
       any one of these branches would suffice to prove Goal.  We explore
       them in turn, describing their derivations as we go.

       ---
       Subgoal D2
       ( same formula as Goal ).

       The first disjunctive branch (of 2) for Goal can be created by applying
       the hint:
       ("Subgoal D2" :EXPAND ((NTH X 3))
                     :IN-THEORY (DISABLE CAR-CONS)
                     :DO-NOT '(GENERALIZE)).

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

       Normally we would attempt to prove this formula by induction.  However,
       we prefer in this instance to focus on the original input conjecture
       rather than this simplified special case.  We therefore abandon our
       previous work on this conjecture and reassign the name *1 to the original
       conjecture.  (See :DOC otf-flg.)  [Note:  Thanks again for the hint.]

       ---
       Subgoal D1
       ( same formula as Goal ).

       The second disjunctive branch (of 2) for Goal can be created by applying
       the hint:
       ("Subgoal D1" :EXPAND ((NTH X 3))
                     :USE CDR-CONS
                     :IN-THEORY (ENABLE APPEND)
                     :DO-NOT '(GENERALIZE)).

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

       ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE an enabled
       :REWRITE or :DEFINITION rule, so you may want to consider disabling
       (:REWRITE CDR-CONS).

       We augment the goal with the hypothesis provided by the :USE hint.
       The hypothesis can be obtained from CDR-CONS.  We are left with the
       following subgoal.

       Subgoal D1'
       (IMPLIES (EQUAL (CDR (CONS X Y)) Y)
                (F X)).

       By the simple :rewrite rule CDR-CONS we reduce the conjecture to

       Subgoal D1''
       (F X).

... and so on.  This example illustrates how ACL2 processes :or hints in
general.  For each i from 1 to k, a so-called "disjunctive" subgoal is
created by splicing kwd-val-listp-i into the other hint values (if any)
supplied for the given goal, in order.  A corresponding subgoal is
created for each i, numbered in the usual manner (hence, counting down)
except that the "D" is prefixed to each resulting goal.

:RW-CACHE-STATE
Value is an element of the list constant *legal-rw-cache-states*: :atom
(the default), nil, t, or :disabled.  This hint applies to the
indicated goal and all its descendents, to set the so-called
"rw-cache-state" to the indicated value; see SET-RW-CACHE-STATE.

:BACKTRACK
This is an advanced hint.  You can probably accomplish its effect by
the use of ordinary computed hints; see COMPUTED-HINTS.  But if
you are an expert, read on.  (See HINTS-AND-THE-WATERFALL for
some relevant background.)

Value is a computed hint, which is an expression that evaluates either
to nil -- indicating that the :backtrack hint is to have no effect --
or to a non-empty alternating list of :keyi :vali pairs, as expected
for a hint.  However, unlike ordinary computed hints, :backtrack hints
are evaluated *after* a goal has been processed to yield zero or more
subgoals, not before.  Moreover, variables PROCESSOR and CLAUSE-LIST
are allowed, but variable STABLE-UNDER-SIMPLIFICATIONP is not.  We
explain in more detail below, but first consider the following simple
example.  First we define a standard list reversal function:

     (defun rev (x)
       (if (consp x)
           (append (rev (cdr x)) (cons (car x) nil))
         nil))

Now we prove:

     (thm (true-listp (rev x)))

The successful proof includes the following output.

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

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

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

But suppose that we attach a :backtrack hint to the goal above at which
destructor elimination was applied:

     (thm (true-listp (rev x))
          :hints (("Subgoal *1/1'"
                   :backtrack
                   (quote (:do-not '(eliminate-destructors))))))

Then when ACL2 applies destructor elimination as displayed above, this
time the :backtrack hint applies, evaluating to (:do-not
'(eliminate-destructors)).  Since this list is not nil, the prover
decides not to keep the new subgoal, and instead supplies this :do-not
hint before attacking the goal again.  In this example, ACL2 happens to
use a technique later in its "waterfall" arsenal than destructor
elimination, namely, generalization:

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

     [Note:  A hint was supplied for our processing
     of the goal above, because of a :backtrack hint
     that is preventing destructor elimination.
     Thanks!]

     We generalize this conjecture, replacing
     (REV (CDR X)) by RV.  This produces

     Subgoal *1/1''
     (IMPLIES (AND (CONSP X) (TRUE-LISTP RV))
              (TRUE-LISTP (APPEND RV (LIST (CAR X))))).

We now provide a careful explanation of how :backtrack hints work, but
we suggest that you keep the example above in mind.  If ":backtrack
form" is part of the hint that has been selected for a goal, then form
is evaluated when one of ACL2's clause processors successfully applies
to the current goal to produce a list of subgoals.  This evaluation
takes place in an environment just like that for any computed hint (see
COMPUTED-HINTS), with the following exceptions.  First, the
variable STABLE-UNDER-SIMPLIFICATIONP is not allowed to occur free in
form, but instead the following new variables are allowed to occur free
and are bound for this evaluation as follows: PROCESSOR is bound to the
processor in the list *preprocess-clause-ledge* that has applied to the
goal, and CLAUSE-LIST is bound to the list of clauses (each a list of
literals that is implicitly disjoined) returned by that clause
processor.  Second, the variables HIST and PSPV are bound to the
history and pspv returned by the clause processor, *not* the ones that
were passed to the clause processor.  If this evaluation returns an
error, then the proof aborts, as for any computed hint whose evaluation
returns an error.  If this evaluation returns nil, then the :backtrack
hint has no effect, and the goal is replaced by the list of goals (the
value of CLAUSE-LIST described above), as usual.  Otherwise, the clause
processor is deemed to have failed, and the goal clause is tried again
starting at the top of the waterfall after selecting the hint returned
by the above evaluation.  That hint will normally be an alternating
list of hint keywords and their values, but if it is a custom keyword
hint (see CUSTOM-KEYWORD-HINTS), then it will be handled in the
usual manner but with the first three variables above bound to the
symbol :OMITTED.  Of course, if the new hint includes a value for
:BACKTRACK then this process can loop; care should be taken to keep
that from happening.

A final note about :BACKTRACK hints: since these are a form of computed
hints, override-hints (if any) are applied to their evaluation result
just as with any computed hint.  That is, the backtrack hint is
successively modified with each override-hint, to produce a final hint
that is actually used (or, ignored if that final hint is nil).  See
OVERRIDE-HINTS.

HINTS-AND-THE-WATERFALL    how hints fit into the ACL2 proof waterfall

Below we describe the flow of an ACL2 proof attempt, with special
attention to how hints are applied during a proof.  For most ACL2
users, only one point is important to take away from this documentation
topic: you may specify hints during a proof (see HINTS; perhaps
also see COMPUTED-HINTS and see DEFAULT-HINTS), and
they can be expected to behave intuitively.  See THE-METHOD for
a summary of how to interact with the ACL2 prover; see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed tutorial; and
see HINTS for an introduction to ACL2 hints, including detailed
documentation for specific hint types.

The remainder of this topic serves as a reference in case one needs a
deeper understanding of the workings of ACL2's handling of hints.
Also, for examples of the sophisticated use of hints, primarily for
experts, see distributed book books/hints/basic-tests.lisp.

First, we describe the ACL2 "waterfall", which handles each goal either
by replacing it with a list (possibly empty) of child goals, or else by
putting the goal into a "pool" for later proof by induction.  Then, we
describe how hints are handled by the waterfall.

*The Waterfall.*

Each goal considered by the ACL2 prover passes through a series of proof
processes, called the "waterfall processes", as stored in the constant
*preprocess-clause-ledge*.  The top process applies top-level hints,
including :use hints; the next is a lightweight "preprocess" simplifier
for "simple" rules (see SIMPLE); the next is the main ACL2
simplifier; and finally ACL2 attempts (in this order) destructor
elimination, fertilization (heuristic use of equalities),
generalization, and elimination of irrelevance.  Each process may
"hit", creating zero or more child goals that are each then handled at
the top of the waterfall; or it may "miss", in which case the next
process in the above sequence is considered.  If all processes miss,
then a "push" process defers the goal until it is later considered for
proof by induction.  When all goals have been thus handled, the goal
most recently pushed for proof by induction is considered, and the
process repeats.

We next describe the two additional ways in which control can be
returned to the top of the waterfall.

When the simplification process is attempted unsuccessfully for a goal,
the goal is deemed to have "settled down".  In this case, and if no
ancestor of the goal has settled down, then the "settled-down" process
is deemed to have "hit" on the goal, the effect being that the goal
makes a new pass through all the waterfall processes.  (Other processes
can then notice that settling down has occurred and modify their
heuristics accordingly.)  For example, if "Goal" simplifies to "Subgoal
2" (among others), and "Subgoal 2" simplifies to "Subgoal 2.3" (among
others), which in turn is not further simplified, then the
"settled-down" process hits on "Subgoal 2.3" but not on any of its
children, their children, and so on.

When simplification has missed (and thus the goal has settled down),
the next proof process is normally destructor elimination.  However, if
a computed hint is suitable (in a sense described below; also see
COMPUTED-HINTS, especially the discussion of
stable-under-simplificationp), then that hint is selected as control is
returned to the top of the waterfall.  A subtlety is that in this case,
if the most recent hit had been from settling down, then the prover
"changes its mind" and considers that the goal has not yet settled down
after all as it continues through the waterfall.

Each time a goal is considered at the top of the waterfall, then before
passing through the proof processes as described above, ACL2 searches
for a relevant hint to select unless it has already been provided a
hint in the "stable-under-simplificationp" case mentioned above.  We
turn now to a more thorough discussion of how hints are selected and
applied.

*The handling of hints.*

In the discussion below we will ignore forcing rounds, as each forcing
round is simply treated as a new proof attempt that uses the list of
hints provided at the start of the proof.

When the theorem prover is called by thm or events such as defthm,
defun, and verify-guards, it gathers up the hints that have been
supplied, often provided as a :hints argument, but for example using a
:guard-hints argument for guard verification proofs.  (ACL2(r) users
(see REAL) may also employ :std-hints.)  It then appends these
to the front of the list of default hints (see DEFAULT-HINTS).
The resulting list becomes the initial value of the list of "pending
hints", one of two critical lists maintained by the theorem prover to
manage hints.  The other critical list is a list of "hint settings";
the two lists are maintained as follows.

When a goal is first considered, a hint is selected from the list of
pending hints if any is found to apply, as described below.  If a hint
is selected, then it takes effect and is removed from the pending
hints.  Except: if the selected hint is a computed hint with value t
specified for :computed-hint-replacement, then it is not removed; and
if that value is a list of hints, then that list is appended to the
front of the list of pending hints after the selected hint is removed
(also see COMPUTED-HINTS).  The selected hint is also used to
update the hint settings, as described below.

The list of hint settings associates hint keywords with values.  It is
passed from the current goal to its children (and hence the children's
children, and so on), though modified by hints selected from pending
hints, as described below.  This list is maintained so that when a goal
is pushed for proof by induction, the hint settings are applied at the
start of the proof by induction.  Note that the list of hint settings
is not re-applied to descendents of a goal in the current waterfall; a
hint is applied only when it is selected (and also perhaps later as
just described, through the stored hint settings at the start of a
proof by induction).  For example, if the hint selected for "Subgoal 3"
includes :in-theory (enable foo), then the hint settings are
correspondingly updated when processing "Subgoal 3", and they persist
at subgoals such as "Subgoal 3.2" and "Subgoal 3.2.1" (unless overriden
by hints on those goals); but the theory specifying foo is not
re-installed at every such subgoal.

When a hint is selected, the list of hint settings is updated so that
for each keyword :kwd and associated value val from the hint, :kwd is
associated with val in the hint settings, discarding any previous
association of :kwd with a value in the hint settings.  Except, certain
"top-level" hints are never saved in the hint settings: :use, :cases,
:by, :bdd, :or, and :clause-processor.

For example, suppose that we specify the following hints, with no
default hints.

     (("Goal" :expand ((bar x y)))
      ("Subgoal 3" :in-theory (enable foo)))

These hints then become the initial list of pending hints.  When the
proof attempt begins, the prover encounters the top-level goal ("Goal")
and pulls the "Goal" hint from the pending hints, so that the list of
hint settings contains a value only for keyword :expand.  This hint
setting will remain for all children of the top-level goal as well, and
their children, and so on, and will be inherited by induction -- in
other words, it will remain throughout the entire proof.  Now consider
what happens when the proof reaches "Subgoal 3".  At this point there
is only one pending hint, which is in fact attached to that subgoal.
Therefore, this hint is pulled from the pending hints (leaving that
list empty), and the hint settings are extended by associating the
:in-theory keyword with the theory represented by (enable foo).  That
theory is immediately installed until the prover finishes addressing
"Subgoal 3", its children, their children, and so on; and until that
completion is reached, the :in-theory keyword remains associated with
the (enable foo) in the hint settings, although of course there is no
re-installation of the theory at any ensuing child goal.  When finally
"Subgoal 3" and its descendents have been completed and the prover is
about to consider "Subgoal 2", the :in-theory association is removed
from the hint settings and the global theory is re-installed.  However,
the list of pending hints remains empty.

It remains to describe how a hint is selected for a goal.  When a goal
is first considered (hence at the top of the waterfall), the list of
pending hints is scanned, in order, until one of the hints is suitable
for the goal.  An explicit hint (goal-name :kwd1 val1 ... :kwdn valn)
is suitable if goal-name is the name of the current goal and there is
at least one keyword.  A computed hint is suitable if it evaluates to a
non-nil value.  As indicated earlier in this documentation topic, an
exception occurs when a computed hint is selected after simplification
fails (the "stable-under-simplificationp" case): in that case, the goal
returns to the top of the waterfall with that hint as the selected
hint, and no additional search for a hint to select is made at that
time.

The following slightly tricky example illustrates handling of hints.

     ACL2 !>(set-default-hints '(("Goal" :do-not '(preprocess))))
      (("Goal" :DO-NOT '(PREPROCESS)))
     ACL2 !>(thm (equal (append (append x y) z) (append x y z))
                 :hints (("Goal" :in-theory (disable car-cons))))

     ACL2 Warning [Hints] in ( THM ...):  The goal-spec "Goal" is explicitly
     associated with more than one hint.  All but the first of these hints
     may be ignored.  If you intended to give all of these hints, combine
     them into a single hint of the form ("Goal" :kwd1 val1 :kwd2 val2 ...).
     See :DOC hints-and-the-waterfall.

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

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

     Name the formula above *1.

The warning above is printed because "Goal" is associated with two
pending hints: one given by the set-default-hints call and one supplied
by the :hints keyword of the thm form.  The :in-theory hint is selected
because user-supplied hints are ahead of default hints in the list of
pending hints; we then get the first "Note" above.  The goal progresses
through the waterfall without any proof process applying to the goal;
in particular, it cannot be further simplified.  After the
simplification process, a "settled-down" process applies, as discussed
above, immediately causing another trip through the waterfall.  Since
the :in-theory hint was earlier removed from the list of pending hints
when it was applied, the default (:do-not) hint is now the only pending
hint.  That hint is applied, resulting in the second "Note" above.

Again, more examples may be found in the distributed book
books/hints/basic-tests.lisp.  A particularly tricky but informative
example in that book is the one related to nonlinearp-default-hint.

Also see OVERRIDE-HINTS for an advanced feature that allows
modification of the hint selected for a goal.

I-AM-HERE    a convenient marker for use with rebuild

     Example Input File for Rebuild:
     (defun fn1 (x y) ...)
     (defthm lemma1 ...)
     (defthm lemma2 ...)
     (i-am-here)
     The following lemma won't go through.  I started
     typing the hint but realized I need to prove a
     lemma first.  See the failed proof attempt in foo.bar.
     I'm going to quit for the night now and resume tomorrow
     from home.

     (defthm lemma3 ...
       :hints (("Goal" :use (:instance ???
     ...

By putting an (i-am-here) form at the "frontier" of an evolving file of
commands, you can use rebuild to load the file up to the (i-am-here).
I-am-here simply returns an ld error triple and any form that "causes
an error" will do the same job.  Note that the text of the file after
the (i-am-here) need not be machine readable.

IMMEDIATE-FORCE-MODEP    when executable counterpart is enabled,
 forced hypotheses are attacked immediately

Also see DISABLE-IMMEDIATE-FORCE-MODEP and see
ENABLE-IMMEDIATE-FORCE-MODEP.

This function symbol is defined simply to provide a rune which can be
enabled and disabled.  Enabling

     (:executable-counterpart immediate-force-modep)

causes ACL2 to attack forced hypotheses immediately instead of delaying
them to the next forcing round.

     Example Hints
     :in-theory (disable (:executable-counterpart immediate-force-modep))
                ; delay forced hyps to forcing round
     :in-theory (enable (:executable-counterpart immediate-force-modep))
                ; split on forced hyps immediately

See FORCE for background information.  When a forced hypothesis
cannot be established a record is made of that fact and the proof
continues.  When the proof succeeds a "forcing round" is undertaken in
which the system attempts to prove each of the forced hypotheses
explicitly.  However, if the rune (:executable-counterpart
immediate-force-modep) is enabled at the time the hypothesis is forced,
then ACL2 does not delay the attempt to prove that hypothesis but
undertakes the attempt more or less immediately.

INDUCT    hints keyword :INDUCT

See HINTS.

KEYWORD    See KEYWORDP.

KEYWORD-COMMANDS    how keyword commands are processed

     Examples:
     user type-in                 form evaluated
     :pc 5                        (ACL2::PC '5)
     :pcs app rev                 (ACL2::PCS 'app 'rev)
     :length (1 2 3)              (ACL2::LENGTH '(1 2 3))
     :quit                        (ACL2::QUIT) ; Note: avoid optional argument

When a keyword, :key, is read as a command, ACL2 determines whether the
symbol with the same name in the "ACL2" package, acl2::key, is a
function or simple macro of n arguments.  If so, ACL2 reads n more
objects, obj1, ..., objn, and then acts as though it had read the
following form (for a given key):

     (ACL2::key 'obj1 ... 'objn)

Thus, by using the keyword command hack you avoid typing the
parentheses, the "ACL2" package name, and the quotation marks.

See LD-KEYWORD-ALIASES for how to customize this behavior.

Note the generality of this hack.  Any function or macro in the "ACL2"
package can be so invoked, not just "commands."  Indeed, there is no
such thing as a distinguished class of commands.  Users may take
advantage of the keyword command hack by defining functions and macros
in the "ACL2" package.

The one caveat is that when the keyword hack is used to invoke a macro,
only the required arguments for that macro are read before calling that
macro: none of the &optional, &rest, &body, or &key arguments are read
for that call.  The macro is thus called with only its required
arguments.  The following log illustrates this caveat.

     ACL2 !>:set-iprint t

     ACL2 Query (:SET-IPRINT):  Action  (T, NIL, RESET, RESET-ENABLE, SAME,
     Q or ?):
     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>

What happened?  First, the command :set-iprint was read.  Since the
macro set-iprint has no required arguments, the ACL2 evaluator was then
called on the form (set-iprint), that is, calling the macro on no
arguments.  Set-iprint is defined to query the ACL2 user when its first
argument is omitted.  The log shows that query, which is set up to read
the next form from the input stream.  That form was available
immediately: the form t that had been supplied by the user.  So the
query returned immediately and the set-iprint call was completed.

LAMBDA    See TERM.

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, :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.  Suppose that ld-error-triples is t and
a form evaluates to a so-called "error triple" (mv erp val state),
where state is the ACL2 state object (see STATE).  If the
"error component", erp, is non-nil, then 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 or :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 by returning an error triple
with non-nil error component, and reverting the logical world to its
value just before that call of ld.

To see this effect of :ERROR for ld-error-action, consider the
following example.

     (ld '((defun f (x) x) (defun bad (x)) (defun g (x) x)))

When the defun of bad fails (because its body is missing), evaluation
of the ld call stops; thus, the defun of g is not evaluated.  The
definition of f will be removed from the logical world before the call
of ld returns.

However, by default each user call of ld is made with a ld-error-action
of :RETURN! (not :ERROR).  In the common case that all nested calls of
ld inside the ACL2 loop are made this way, an error will not roll back
the logical world.  However, it will still halt evaluation of forms for
the current call of ld and any parent calls of ld (other than the call
made on behalf of lp that entered the ACL2 loop in the first place), as
though there were no more forms to evaluate.

We have already discussed the behavior of ld when an error occurs.  But
there is another case when ld can stop processing more forms: when
ld-error-action is not :CONTINUE, ld-error-triples is t, and evaluation
of a form returns an error triple (mv nil val state), where nil is the
error component and whose "value component", val is a cons pair whose
car is the symbol :STOP-LD.  Let val be the pair (:STOP-LD . x).  Then
the call of ld returns the error triple (mv nil (:STOP-LD n . x)
state), where n is the value of state global variable 'ld-level at the
time of termination.  The following example illustrates how this works.

     (ld '((defun f1 (x) x)
           (ld '((defun f2 (x) x)
                 (mv nil '(:STOP-LD my-error more-info) state)
                 (defun g2 (x) x)))
           (defun g1 (x) x)))

The outer call of ld returns the value

     (:STOP-LD 2 3 MY-ERROR MORE-INFO)

and leaves us in a world the includes definitions for f1 and f2, but no
definition for g1 or g2 since neither of their two defun forms was
evaluated.  The value of state global 'ld-level is incremented from 1
to 2 when the outer ld is entered and then again to 3 when the inner ld
is entered.  When the inner ld escounters the error triple (mv nil
(:STOP-LD my-error more-info) state), it sees :STOP-LD in the car of
the value component and pushes the current value of 'ld-level, 3, onto
the cdr of that value, to return the value triple (mv nil (:STOP-LD
my-error 3 more-info) state).  The outer of ld then sees this value and
returns (mv nil (:STOP-LD my-error 2 3 more-info) state), since its
current value of 'ld-level is 2 after the inner ld exits.

That concludes our discussion of how these special :STOP-LD values are
handled; but how are they created?  While they can be created directly
by evaluation results as suggested in the example above, that is not the
standard way.  Rather, ld returns an error triple (mv nil (:STOP-LD n)
state), where n is the value of variable ld-level at the time of
termination, when the following conditions hold: an error occurs,
ld-error-action is RETURN! (which is the default), and ld-error-triples
is t (the default).  The following example, which is a bit similar to
the preceding one, illustrates both creation and handling of the
special :STOP-LD values.

     (ld '((defun f1 (x) x)
           (ld '((defun f2 (x) x)
                 (ld '((defun f3 (x) x)
                       (defun bad (x)) ; ERROR -- missing the body
                       (defun g3 (x) x)))
                 (defun g2 (x) x)))
           (defun g1 (x) x)))

The result is that f1, f2, and f3 are defined, but none of g1, g2, or
g3 is defined.  Let's see why.  The innermost call of ld has a default
:ld-error-action of :RETURN! (as do the other calls).  So when the
definition of bad fails, then the innermost ld returns (mv nil
(:STOP-LD 4) state).  The middle ld sees this value, and since its
:ld-error-action is not :CONTINUE (because it has the default value of
:RETURN!), it returns before considering the definition of g2, with
value (mv nil (:STOP-LD 3 4) state).  The topmost call of ld similarly
sees the :STOP-LD; stops evaluation of forms, without defining g1; and
returns (mv nil (:STOP-LD 2 3 4) state).

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 and also
ld-error-triples is t, 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).  For more
information about error triples, see PROGRAMMING-WITH-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.  Normally ACL2
enforces the requirement that every variable vi must be bound in the
formula denoted by lmi.  However, the keyword :extra-bindings-ok may be
inserted immediately after the lemma instance in order to remove that
requirement: (:instance lmi :extra-bindings-ok (v1 t1) ... (vn tn)).

(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 !>(foo :k1 3 :bad-key 7)

     ACL2 Error in macro expansion:  Illegal key/value args (:BAD-KEY 7)
     in macro expansion of (FOO :K1 3 :BAD-KEY 7).  The argument list for
     FOO is
     (&REST ARGS &KEY K1 K2 K3).

     ACL2 !>

If we don't want to get the error above, we can use &allow-other-keys,
as follows.

     ACL2 !>(defmacro bar (&rest args &key k1 k2 k3
                                 &allow-other-keys)
              (list 'quote (list args k1 k2 k3)))

     Summary
     Form:  ( DEFMACRO BAR ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      BAR
     ACL2 !>(bar :k1 3 :bad-key 7)
     ((:K1 3 :BAD-KEY 7) 3 NIL NIL)
     ACL2 !>

Also see TRANS.

MAKE-WORMHOLE-STATUS    creates a wormhole status object from given status, entry code, and data

     General Form:  (make-wormhole-status whs code data)

See WORMHOLE.  Whs should be a well-formed wormhole status, code
should be :ENTER or :SKIP, and data is arbitrary.  This function
returns a new status with the specified entry code and data, reusing whs
if it is appropriate.

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.

NIL-GOAL    how to proceed when the prover generates a goal of nil

At the end of a failed proof, one typically sees so-called "key
checkpoints" (see SET-GAG-MODE).  These may be annotated as
follows.

     [NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

This documentation topic gives some ideas about how to think about the
situation described by that message: some goal has reduced to nil.

Suppose then that you see the above NOTE.  If you look back at the
proof log, even with gag-mode enabled, you will see a message saying
that a goal of NIL "has been generated".  This may indicate that the
original goal is not a theorem, since most of the prover's activity is
to replace a goal by an equivalent conjunction of its child subgoals.
However, if some ancestor of the nil goal has undergone a process other
than simplification or destructor elimination -- fertilization
(heuristic use of equalities), generalization, or elimination of
irrelevance -- then it is quite possible that the prover got to the nil
goal by replacing a goal by a stronger (and perhaps false) conjunction
of child subgoals.

At present, if you are using gag-mode (the default) then you will need
to issue the command :pso ("Print Saved Output") if you want to see
whether the situation above has occurred.  However, that might not be
necessary.  A good rule of thumb is that if the nil goal is under more
level of induction (e.g., with a prefix "*i.j" such as "Subgoal
*1.1/2.2"), then there is some likelihood that the situation above did
indeed occur, and you can spend your time and energy looking at the key
checkpoints printed in the summary to see if they suggest useful rewrite
rules to prove.  On the other hand, if the nil goal is at the top level
(e.g. with a name not starting with "*", such as "Subgoal 3.2"), then
the original conjecture is probably not a theorem.  If you do not
quickly see why that is the case, then you might find it useful to
issue the command :pso to see which case reduced to nil, in order to get
insight about how the theorem might be falsified.

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 motivation for an
arithmetic-theory distinct from 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    allow more than one initial subgoal to be pushed for induction

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 implemented 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.  That selected hint is a keyword-alist, which is an
alternating list of hint keywords and their values, whose source is
either 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 keyword-alist
produced by 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 the variable KEYWORD-ALIST bound to the above
keyword-alist.  That evaluation produces a result that should also be a
keyword-alist, or else an error occurs.  Any custom keyword hints are
then eliminated from that keyword-alist.  The resulting keyword-alist
must not contain the :ERROR hint keyword and must not start with the
:COMPUTED-HINT-REPLACEMENT keyword; otherwise an error occurs.  With
KEYWORD-ALIST bound to this result, the second override-hint is
similarly evaluated.  This process continues, and the keyword-alist
returned by the final override-hint is the one used when processing the
goal at hand.  Except: If that keyword-alist is nil, then the next hint
among the pending hints is tentatively selected and the process
repeats, applying each override hint to that new tentative selection.
Of course we might obtain nil again, in which case we tentatively
select the next pending hint; and so on.

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

As mentioned above, 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, for example as follows.
(The use of prog2$ and cw is of course optional, included here to
provide debug printing.)

     (add-override-hints
      '((let* ((tmp (assoc-keyword :do-not KEYWORD-ALIST))
               (new-keyword-alist
                (cond (tmp (list* :do-not
                                  `(cons 'generalize ,(cadr tmp))
                                  (remove-keyword :do-not KEYWORD-ALIST)))
                      (t (list* :do-not ''(generalize) KEYWORD-ALIST)))))
          (prog2$ (cw "New: ~x0~|" new-keyword-alist)
                  new-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).

P!    to pop up (at least) one level of ACL2's command loop

Logically speaking, (p!) = nil.  If you are already at the top level of
the ACL2 command loop, rather than being in a subsidiary call of ld,
then the keyword then a call of (p!) returns nil and has no other
effect.

Otherwise, (p!) is evaluated inside a call of ld that was made inside
ACL2's command loop.  In that case, the current computation is aborted
and treating as causing an error, and control returns to the superior
call of ld.

Here is a more detailed description of the effect of (p!) when not at
the top level of the ACL2 command loop.  The current call of LD is
treated as though ld-error-action is :RETURN! (the default) and hence
immediately returns control to the superior call of ld.  If all calls
of ld were made with the default ld-error-action of :RETURN!, then all
superior calls of ld will then complete until you are back at top level
of the ACL2 loop.  For more information, see LD-ERROR-ACTION.

If you are at an ACL2 prompt (as opposed to a raw Lisp break), then you
may type :p! in place of (p!); see KEYWORD-COMMANDS.

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.

PARALLEL    evaluating forms in parallel

See PARALLELISM.

PARALLELISM-BUILD    building an ACL2 executable with parallel execution enabled

See COMPILING-ACL2P.

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.

PROOF-SUPPORTERS-ALIST    See DEAD-EVENTS.

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 (see PUSH-UNTOUCHABLE) all variables and functions.

WARNING: If the form (redef+) is used in a book, then including the book
can leave you in a state in which dangerous actions are allowed,
specifically: redefinition, and access to functions and variables
normally prohibited because they are untouchable.  To avoid this
problem, insert the form (redef-) into your book after (redef+).

To see the code for redef+, evaluate :trans1 (redef+).  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+.  We do not guarantee that
:redef- will restore everything one might expect to its state before
the earlier :redef+.  To see exactly what :redef- does, look at its
code, for example by evaluating :trans1 (redef-)

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
DEFUN-NX), 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 defabsstobj is redundant if
there is already an identical defabsstobj 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, defattach or regenerate-tau-data-base 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.

In most cases, 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.  There are two rather obscure
exceptions to this rule.  One exception is relevant only if make-event
is invoked in the earlier encapsulate; in that case, it suffices that
the two encapsulates are equal after replacing each top-level sub-event
of the earlier encapsulate by its make-event expansion.  The other
exception is in the case of redefinition (see
LD-REDEFINITION-ACTION), in which case an attempt is made to ignore
an earlier encapsulate that has already been superseded by redefinition.

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

_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 may
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))
     (set-ld-redefinition-action nil state)
     (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 before storing the first
definition of foo for the theorem prover.  Therefore, the new definition
of mac does not affect the expansion of foo by the theorem prover,
because the new definition of foo is ignored.

One 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.  However, as a courtesy to users, we
strengthen the redundancy check for function definitions when
redefinition is active.  If in the example above we remove the form
(set-ld-redefinition-action nil state), then the problem goes away:

     (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)) ; no longer redundant
     (thm (equal (foo 3) 3)) ; fails, as we would like

To summarize: If a defun form is submitted that meets the usual
redundancy criteria, then it may be considered redundant even if a macro
called in the definition has since been redefined.  The analogous
problem applie to constants, i.e., symbols defined by defconst that
occur in the definition body.  However, if redefinition is currently
active the problem goes away: that is, the redundancy check is
strengthened to check the "translated" body, in which macro calls and
constants defined by defconst are expanded away.

The above discussion for defun forms applies to defconst forms as well.
However, for defmacro forms ACL2 always checks translated bodies, so
such bogus redundancy does not occur.

Here is more complex example illustrating the limits of redefinition,
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)
     (thm (equal (n5) nil)) ; still succeeds, sadly

We may expect the final thm call to fail because of the following
reasoning: (n5) = (> (n3) (n4)) = (> 2 1) = t.  Unfortunatly, the body
of n5 was simplified ("normalized") to nil when n5 was admitted, so the
redefinition of n3 is ignored during the final thm call.  (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.  Even with redefinition active, there is no change in the
body of n5, even with macros and constants (defined by defconst)
expanded; there are none such!  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.

     (defmacro mac (x) x)
     (encapsulate () (defun foo (x) (mac x)))
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defmacro mac (x) (list 'car x))
     (encapsulate () (defun foo (x) (mac x)))

The last encapsulate event is redundant because it meets the criterion
for redundancy: it is identical to the earlier encapsulate event.  Even
though redefinition is active, and hence ACL2 "should" be able to see
that the new defun of foo is not truly redundant, nevertheless the
criterion for redundancy of encapsulate allows the new encapsulate form
to be redundant.

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

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.

SET-WORMHOLE-DATA    sets the wormhole data object in a wormhole status object

     General Form:  (set-wormhole-data whs data)

See WORMHOLE.  Whs should be a well-formed wormhole status;
data is arbitrary.  This function returns a new status with the same
entry code as whs but with the new data.  It avoids unnecessary consing
if the data for whs is already set to data.  This function does not
affect state or a wormhole's hidden status.  It just returns a
(possibly) new status object suitable as the value of the lambda
expressions in wormhole-eval and wormhole.

SET-WORMHOLE-ENTRY-CODE    sets the wormhole entry code in a wormhole status object

     General Form:  (set-wormhole-entry-code whs code)

See WORMHOLE.  Whs should be a well-formed wormhole status and
code should be :ENTER or :SKIP.  This function returns a new status with
the specified entry code but the same data as whs.  It avoids
unnecessary consing if the entry code for whs is already set to code.
This function does not affect state or a wormhole's hidden status.  It
just returns a (possibly) new status object suitable as the value of the
lambda expressions in wormhole-eval and wormhole.

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 *) => *)
     ((hd *) => * :formals (x) :guard (consp x))
     ((printer * state) => (mv * * state))
     ((mach * mach-state * state) => (mv * mach-state)

     General Form:
     ((fn ...) => *)
     ((fn ...) => stobj)
     or
     ((fn ...) => (mv ...))
     or for part1 and part2 as above,
     (part1 => part2 :kwd1 val1 ... :kwdn valn)

where fn is the constrained function symbol, ... is a list of asterisks
and/or the names of single-threaded objects, stobj is a single-threaded
object name, and the optional :kwdi and :vali are as described below.
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 or defabsstobj.  An object that is
not a single-threaded object is said to be "ordinary."

A signature typically has the form ((fn x1 ... xn) => val).  Such 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, and a stobj name may appear in
val only if appears among the xi.

A signature may have the form ((fn x1 ... xn) => val . k), where k is a
keyword-value-listp, i.e., an alternating list of keywords and values
starting with a keyword.  In this case ((fn x1 ... xn) => val) must be a
legal signature as described above.  The legal keywords in k are :GUARD
and :FORMALS.  The value following :FORMALS is to be the list of formal
parameters of fn, while the value following :GUARD is a term that is to
be the guard of fn.  Note that this guard is never actually evaluated,
and is not subject to the guard verification performed on functions
introduced by defun (see VERIFY-GUARDS).  Said differently:
this guard need not itself have a guard of t.  Indeed, the guard is
only used for attachments; see DEFATTACH.  Note that if :GUARD
is supplied then :FORMALS must also be supplied (in order to related
the variables occurring in the guard to the parameters of fn).  One
final observation about guards: if the :GUARD keyword is omitted, then
the guard defaults to T.

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

where fn is the constrained function symbol, formals is a suitable list
of formal parameters for it, k is an optional keyword-value-listp (see
below), 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!

The optional k is as described above for newer-style signatures, except
that the user is also allowed to declare which symbols (besides state)
are to be considered single-threaded object names.  Thus :STOBJS is also
a legal keyword.  The form

     (fn formals result ... :stobjs names ...)

specifies that 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 or defabsstobj.

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.

STOBJS    xargs keyword :STOBJS

See XARGS.

SUBVERSIVE-INDUCTIONS    why we restrict encapsulated recursive functions

See SUBVERSIVE-RECURSIONS.

SUBVERSIVE-RECURSIONS    why we restrict encapsulated recursive functions

Subtleties arise when one of the "constrained" functions, f, introduced
in the signature of an encapsulate event, is involved in the
termination argument for a non-local recursively defined function, g, in
that encapsulate.  During the processing of the encapsulated events, f
is locally defined to be some witness function, f'.  Properties of f'
are explicitly proved and exported from the encapsulate as the
constraints on the undefined function f.  But if f is used in a
recursive g defined within the encapsulate, then the termination proof
for g may use properties of f' -- the witness -- that are not
explicitly set forth in the constraints stated for f.

Such recursive g are said be "subversive" because if naively treated
they give rise to unsound induction schemes or (via functional
instantiation) recurrence equations that are impossible to satisfy.  We
illustrate what could go wrong below.

Subversive recursions are not banned outright.  Instead, they are
treated as part of the constraint.  That is, in the case above, the
definitional equation for g becomes one of the constraints on f.  This
is generally a severe restriction on future functional instantiations
of f.  In addition, ACL2 removes from its knowledge of g any
suggestions about legal inductions to "unwind" its recursion.

What should you do?  Often, the simplest response is to move the
offending recursive definition, e.g., g, out of the encapsulate.  That
is, introduce f by constraint and then define g as an "independent"
event.  You may need to constrain "additional" properties of f in order
to admit g, e.g., constrain it to reduce some ordinal measure.  However,
by separating the introduction of f from the admission of g you will
clearly identify the necessary constraints on f, functional
instantiations of f will be simpler, and g will be a useful function
which suggests inductions to the theorem prover.

Note that the functions introduced in the signature should not even
occur ancestrally in the termination proofs for non-local recursive
functions in the encapsulate.  That is, the constrained functions of an
encapsulate should not be reachable in the dependency graph of the
functions used in the termination arguments of recursive functions in
encapsulate.  If they are reachable, their definitions become part of
the constraints.

The following event illustrates the problem posed by subversive
recursions.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun g (x)
         (if (consp x) (not (g (f x))) t)))

Suppose, contrary to how ACL2 works, that the encapsulate above were to
introduce no constraints on f on the bogus grounds that the only use of
f in the encapsulate is in an admissible function.  We discuss the
plausibility of this bogus argument in a moment.

Then it would be possible to prove the theorem:

     (defthm f-not-identity
       (not (equal (f '(a . b)) '(a . b)))
       :rule-classes nil
       :hints (("Goal" :use (:instance g (x '(a . b))))))

simply by observing that if (f '(a . b)) were '(a . b), then (g '(a .
b)) would be (not (g '(a . b))), which is impossible.

But then we could functionally instantiate f-not-identity, replacing f
by the identity function, to prove nil!  This is bad.

     (defthm bad
       nil
       :rule-classes nil
       :hints
       (("Goal" :use (:functional-instance f-not-identity (f identity)))))

This sequence of events was legal in versions of ACL2 prior to Version
1.5.  When we realized the problem we took steps to make it illegal.
However, our steps were insufficient and it was possible to sneak in a
subversive function (via mutual recursion) as late as Version 2.3.

We now turn to the plausibility of the bogus argument above.  Why might
one even be tempted to think that the definition of g above poses no
constraint on f?  Here is a very similar encapsulate.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun map (x)
         (if (consp x)
             (cons (f x) (map (cdr x)))
           nil)))

Here map plays the role of g above.  Like g, map calls the constrained
function f.  But map truly does not constrain f.  In particular, the
definition of map could be moved "out" of the encapsulate so that map
is introduced afterwards.  The difference between map and g is that the
constrained function plays no role in the termination argument for the
one but does for the other.

As a "user-friendly" gesture, ACL2 implicitly moves map-like functions
out of encapsulations; logically speaking, they are introduced after the
encapsulation.  This simplifies the constraint.  When the constraint
cannot be thus simplfied the user is advised, via the "infected"
warning, to phrase the encapsulation in the simplest way possible.

The lingering bug between Versions 1.5 and 2.3 mentioned above was due
to our failure to detect the g-like nature of some functions when they
were defined in mutually recursively cliques with other functions.  The
singly recursive case was recognized.  The bug arose because our
detection "algorithm" was based on the "suggested inductions" left
behind by successful definitions.  We failed to recall that
mutually-recursive definitions do not, as of this writing, make any
suggestions about inductions and so did not leave any traces of their
subversive natures.

We conclude by elaborating on the criterion "involved in the termination
argument" mentioned at the outset.  Suppose that function f is
recursively defined in an encapsulate, where the body of f has no
"ancestor" among the functions introduced in the signature of that
encapsulate, i.e.: the body contains no call of a signature function,
no call of a function whose body calls a signature function, and so on.
Then ACL2 treats f as though it is defined in front of that encapsulate
form; so f is not constrained by the encapsulate, and its definition is
hence certainly not subversive in the sense discussed above.  But
suppose to the contrary that some function introduced in the signature
is an ancestor of the body of f.  Then the definition of f is
subversive if moreover, its termination proof obligation has an
ancestor among the signature functions.  Now, that proof obligation
involves terms from the first argument of selected calls of IF, as well
as recursive calls; for a detailed discussion, see
RULER-EXTENDERS.  The important point here is that for the recursive
calls, only the arguments in "measured" positions are relevant to the
termination proof obligation.  Consider the following example.

       (encapsulate
        (((h *) => *))
        (local (defun h (n) n))
        (defun f (i n)
          (if (zp i)
              n
            (f (1- i) (h n)))))

ACL2 heuristically picks the measure (acl2-count i) for the definition
of f; thus, i is the only "measured formal" of f.  Since i is the first
formal of f, then for the recursive call of f, only the first argument
contributes to the termination proof obligation: in this case, (1- i)
but not (h n).  Thus, even though h is a signature function, the
definition of f is not considered to be subversive; an induction scheme
is thus stored for f.  (This restriction to measured formal positions
of recursive calls, for determining subversive definitions, is new in
Version_3.5 of ACL2.)

SYNTAX    the syntax of ACL2 is that of Common Lisp

For the details of ACL2 syntax, see CLTL.  For examples of ACL2 syntax,
use :pe to print some of the ACL2 system code.  For example:

     :pe assoc-equal
     :pe dumb-occur
     :pe var-fn-count
     :pe add-linear-variable-to-alist

There is no comprehensive description of the ACL2 syntax yet, except
that found in CLTL.  Also see TERM.

SYNTAXP    attach a heuristic filter on a :rewrite, :meta, or :linear rule

     Example:
     Consider the :REWRITE rule created from

     (IMPLIES (SYNTAXP (NOT (AND (CONSP X)
                                 (EQ (CAR X) 'NORM))))
              (EQUAL (LXD X)
                     (LXD (NORM X)))).

The syntaxp hypothesis in this rule will allow the rule to be applied
to (lxd (trn a b)) but will not allow it to be applied to (lxd (norm
a)).

     General Form:
     (SYNTAXP test)

Syntaxp always returns t and so may be added as a vacuous hypothesis.
However, when relieving the hypothesis, the test "inside" the syntaxp
form is actually treated as a meta-level proposition about the proposed
instantiation of the rule's variables and that proposition must
evaluate to true (non-nil) to "establish" the syntaxp hypothesis.

Note that the test of a syntaxp hypothesis does not, in general, deal
with the meaning or semantics or values of the terms, but rather with
their syntactic forms.  In the example above, the syntaxp hypothesis
allows the rule to be applied to every target of the form (lxd u),
provided u is not of the form (norm v).  Observe that without this
syntactic restriction the rule above could loop producing a sequence of
increasingly complex targets (lxd a), (lxd (norm a)), (lxd (norm (norm
a))), etc.  An intuitive reading of the rule might be "norm the
argument of lxd unless it has already been normed."

Note also that a syntaxp hypothesis deals with the syntactic form used
internally by ACL2, rather than that seen by the user.  In some cases
these are the same, but there can be subtle differences with which the
writer of a syntaxp hypothesis must be aware.  You can use :trans to
display this internal representation.

There are two types of syntaxp hypotheses.  The simpler type of syntaxp
hypothesis may be used as the nth hypothesis in a :rewrite or :linear
rule whose :corollary is (implies (and hyp1 ... hypn ... hypk) (equiv
lhs rhs)) provided test is a term, test contains at least one variable,
and every variable occuring freely in test occurs freely in lhs or in
some hypi, i<n.  In addition, test must not use any stobjs.  The case
of :meta rules is similar to the above, except that it applies to the
result of applying the hypothesis metafunction.  (Later below we will
describe the second type, an _extended_ syntaxp hypothesis, which may
use state.)

We illustrate the use of simple syntaxp hypotheses by slightly
elaborating the example given above.  Consider a :rewrite rule whose
:corollary is:

     (IMPLIES (AND (RATIONALP X)
                   (SYNTAXP (NOT (AND (CONSP X)
                                      (EQ (CAR X) 'NORM)))))
              (EQUAL (LXD X)
                     (LXD (NORM X))))

How is this rule applied to (lxd (trn a b))?  First, we form a
substitution that instantiates the left-hand side of the conclusion of
the rule so that it is identical to the target term.  In the present
case, the substitution replaces x with (trn a b).

     (LXD X) ==> (LXD (trn a b)).

Then we backchain to establish the hypotheses, in order.  Ordinarily
this means that we instantiate each hypothesis with our substitution and
then attempt to rewrite the resulting instance to true.  Thus, in order
to relieve the first hypothesis above, we rewrite

     (RATIONALP (trn a b)).

If this rewrites to true, we continue.

Of course, most users are aware of some exceptions to this general
description of the way we relieve hypotheses.  For example, if a
hypothesis contains a "free-variable" -- one not bound by the current
substitution -- we attempt to extend the substitution by searching for
an instance of the hypothesis among known truths.  See
FREE-VARIABLES.  Forced hypotheses are another exception to the
general rule of how hypotheses are relieved.

Hypotheses marked with syntaxp, as in (syntaxp test), are also
exceptions.  We instantiate such a hypothesis; but instead of rewriting
the instantiated instance, we evaluate the instantiated test.  More
precisely, we evaluate test in an environment in which its variable
symbols are bound to the quotations of the terms to which those
variables are bound in the instantiating substitution.  So in the case
in point, we (in essence) evaluate

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

This clearly evaluates to t.  When a syntaxp test evaluates to true, we
consider the syntaxp hypothesis to have been established; this is sound
because logically (syntaxp test) is t regardless of test.  If the test
evaluates to nil (or fails to evaluate because of guard violations) we
act as though we cannot establish the hypothesis and abandon the
attempt to apply the rule; it is always sound to give up.

The acute reader will have noticed something odd about the form

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

When relieving the first hypothesis, (RATIONALP X), we substituted (trn
a b) for X; but when relieving the second hypothesis, (SYNTAXP (NOT
(AND (CONSP X) (EQ (CAR X) 'NORM)))), we substituted the quotation of
(trn a b) for X.  Why the difference?  Remember that in the first
hypothesis we are talking about the value of (trn a b) -- is it
rational -- while in the second one we are talking about its syntactic
form.  Remember also that Lisp, and hence ACL2, evaluates the arguments
to a function before applying the function to the resulting values.
Thus, we are asking "Is the list (trn a b) a consp and if so, is its
car the symbol NORM?"  The quotes on both (trn a b) and NORM are
therefore necessary.  One can verify this by defining trn to be, say
cons, and then evaluating forms such as

     (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))
     (AND (CONSP (trn a b)) (EQ (CAR (trn a b)) NORM))
     (AND (CONSP (trn 'a 'b)) (EQ (CAR (trn 'a 'b)) NORM))
     (AND (CONSP '(trn a b)) (EQ '(CAR (trn a b)) ''NORM))

at the top-level ACL2 prompt.

See SYNTAXP-EXAMPLES for more examples of the use of syntaxp.

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

SYNTAXP-EXAMPLES    examples pertaining to syntaxp hypotheses

See SYNTAXP for a basic discussion of the use of syntaxp to
control rewriting.

A common syntactic restriction is

     (SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE)))

or, equivalently,

     (SYNTAXP (QUOTEP X)).

A rule with such a hypothesis can be applied only if x is bound to a
specific constant.  Thus, if x is 23 (which is actually represented
internally as (quote 23)), the test evaluates to t; but if x prints as
(+ 11 12) then the test evaluates to nil (because (car x) is the symbol
binary-+).  We see the use of this restriction in the rule

     (implies (and (syntaxp (quotep c))
                   (syntaxp (quotep d)))
              (equal (+ c d x)
                     (+ (+ c d) x))).

If c and d are constants, then the executable-counterpart of binary-+
will evaluate the sum of c and d.  For instance, under the influence of
this rule

     (+ 11 12 foo)

rewrites to

     (+ (+ 11 12) foo)

which in turn rewrites to (+ 23 foo).  Without the syntactic
restriction, this rule would loop with the built-in rules
ASSOCIATIVITY-OF-+ or COMMUTATIVITY-OF-+.

We here recommend that the reader try the affects of entering
expressions such as the following at the top level ACL2 prompt.

     (+ 11 23)
     (+ '11 23)
     (+ '11 '23)
     (+ ''11 ''23)
     :trans (+ 11 23)
     :trans (+ '11 23)
     :trans (+ ''11 23)
     :trans (+ c d x)
     :trans (+ (+ c d) x)

We also recommend that the reader verify our claim above about looping
by trying the affect of each of the following rules individually.

     (defthm good
        (implies (and (syntaxp (quotep c))
                      (syntaxp (quotep d)))
                 (equal (+ c d x)
                        (+ (+ c d) x))))

     (defthm bad
        (implies (and (acl2-numberp c)
                      (acl2-numberp d))
                 (equal (+ c d x)
                        (+ (+ c d) x))))

on (the false) theorems:

     (thm
       (equal (+ 11 12 x) y))

     (thm
       (implies (and (acl2-numberp c)
                     (acl2-numberp d)
                     (acl2-numberp x))
                (equal (+ c d x) y))).

One can use :brr, perhaps in conjunction with cw-gstack, to investigate
any looping.

Here is a simple example showing the value of rule good above.  Without
good, the thm form below fails.

     (defstub foo (x) t)

     (thm (equal (foo (+ 3 4 x)) (foo (+ 7 x))))

The next three examples further explore the use of quote in syntaxp
hypotheses.

We continue the examples of syntaxp hypotheses with a rule from
books/finite-set-theory/set-theory.lisp.  We will not discuss here the
meaning of this rule, but it is necessary to point out that
(ur-elementp nil) is true in this book.

     (defthm scons-nil
       (implies (and (syntaxp (not (equal a ''nil)))
                     (ur-elementp a))
                (= (scons e a)
                   (scons e nil)))).

Here also, syntaxp is used to prevent looping.  Without the
restriction, (scons e nil) would be rewritten to itself since
(ur-elementp nil) is true.
Question: Why the use of two quotes in "nil?
Hints: Nil is a constant just as 23 is.  Try :trans (cons a nil),
:trans (cons 'a 'nil), and :trans (cons "a "nil).  Also, don't forget
that the arguments to a function are evaluated before the function is
applied.

The next two rules move negative constants to the other side of an
inequality.

     (defthm |(< (+ (- c) x) y)|
       (implies (and (syntaxp (quotep c))
                     (syntaxp (< (cadr c) 0))
                     (acl2-numberp y))
                (equal (< (+ c x) y)
                       (< (fix x) (+ (- c) y)))))

     (defthm |(< y (+ (- c) x))|
       (implies (and (syntaxp (quotep c))
                     (syntaxp (< (cadr c) 0))
                     (acl2-numberp y))
                (equal (< y (+ c x))
                       (< (+ (- c) y) (fix x)))))

Questions: What would happen if (< (cadr c) '0) were used?  What about
(< (cadr c) "0)?

One can also use syntaxp to restrict the application of a rule to a
particular set of variable bindings as in the following taken from
books/ihs/quotient-remainder-lemmas.lisp.

     (encapsulate ()

       (local
        (defthm floor-+-crock
          (implies
           (and (real/rationalp x)
                (real/rationalp y)
                (real/rationalp z)
                (syntaxp (and (eq x 'x) (eq y 'y) (eq z 'z))))
           (equal (floor (+ x y) z)
                  (floor (+ (+ (mod x z) (mod y z))
                            (* (+ (floor x z) (floor y z)) z)) z)))))

       (defthm floor-+
         (implies
          (and (force (real/rationalp x))
               (force (real/rationalp y))
               (force (real/rationalp z))
               (force (not (equal z 0))))
          (equal (floor (+ x y) z)
                 (+ (floor (+ (mod x z) (mod y z)) z)
                    (+ (floor x z) (floor y z))))))

       )

We recommend the use of :brr to investigate the use of floor-+-crock.

Another useful restriction is defined by

     (defun rewriting-goal-literal (x mfc state)

       ;; Are we rewriting a top-level goal literal, rather than rewriting
       ;; to establish a hypothesis from a rewrite (or other) rule?

       (declare (ignore x state))
       (null (access metafunction-context mfc :ancestors))).

We use this restriction in the rule

     (defthm |(< (* x y) 0)|
         (implies (and (syntaxp (rewriting-goal-literal x mfc state))
                       (rationalp x)
                       (rationalp y))
                  (equal (< (* x y) 0)
                         (cond ((equal x 0)
                                nil)
                               ((equal y 0)
                                nil)
                               ((< x 0)
                                (< 0 y))
                               ((< 0 x)
                                (< y 0))))))

which has been found to be useful, but which also leads to excessive
thrashing in the linear arithmetic package if used indiscriminately.

See EXTENDED-METAFUNCTIONS for information on the use of mfc
and metafunction-context.

TERM    the three senses of well-formed ACL2 expressions or formulas

     Examples of Terms:
     (cond ((caar x) (cons t x)) (t 0))   ; an untranslated term

     (if (car (car x)) (cons 't x) '0)    ; a translated term

     (car (cons x y) 'nil v)              ; a pseudo-term

In traditional first-order predicate calculus a "term" is a syntactic
entity denoting some object in the universe of individuals.  Often, for
example, the syntactic characterization of a term is that it is either
a variable symbol or the application of a function symbol to the
appropriate number of argument terms.  Traditionally, "atomic formulas"
are built from terms with predicate symbols such as "equal" and
"member;" "formulas" are then built from atomic formulas with
propositional "operators" like "not," "and," and "implies." Theorems
are formulas.  Theorems are "valid" in the sense that the value of a
theorem is true, in any model of the axioms and under all possible
assignments of individuals to variables.

However, in ACL2, terms are used in place of both atomic formulas and
formulas.  ACL2 does not have predicate symbols or propositional
operators as distinguished syntactic entities.  The ACL2 universe of
individuals includes a "true" object (denoted by t) and a "false"
object (denoted by nil), predicates and propositional operators are
functions that return these objects.  Theorems in ACL2 are terms and
the "validity" of a term means that, under no assignment to the
variables does the term evaluate to nil.

We use the word "term" in ACL2 in three distinct senses.  We will speak
of "translated" terms, "untranslated" terms, and "pseudo-" terms.

_Translated Terms:  The Strict Sense and Internal Form_

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 a true list of n terms.

The legal variable symbols are symbols other than t or nil which are
not in the keyword package, do not start with ampersand, do not start
and end with asterisks, and if in the main Lisp package, do not violate
an appropriate restriction (see NAME).

Quoted constants are expressions of the form (quote x), where x is any
ACL2 object.  Such expressions may also be written 'x.

Closed lambda expressions are expressions of the form (lambda (v1 ...
vn) body) where the vi are distinct legal variable symbols, body is a
term, and the only free variables in body are among the vi.

The function termp, which takes two arguments, an alleged term x and a
logical world w (see WORLD), recognizes terms of a given
extension of the logic.  Termp is defined in :program mode.  Its
definition may be inspected with :pe termp for a complete specification
of what we mean by "term" in the most strict sense.  Most ACL2
term-processing functions deal with terms in this strict sense and use
termp as a guard.  That is, the "internal form" of a term satisfies
termp, the strict sense of the word "term."

_Untranslated Terms:  What the User Types_

While terms in the strict sense are easy to explore (because their
structure is so regular and simple) they can be cumbersome to type.
Thus, ACL2 supports a more sugary syntax that includes uses of macros
and constant symbols.  Very roughly speaking, macros are functions that
produce terms as their results.  Constants are symbols that are
associated with quoted objects.  Terms in this sugary syntax are
"translated" to terms in the strict sense; the sugary syntax is more
often called "untranslated."  Roughly speaking, translation just
implements macroexpansion, the replacement of constant symbols by their
quoted values, and the checking of all the rules governing the strict
sense of "term."

More precisely, macro symbols are as described in the documentation for
defmacro.  A macro, mac, can be thought of as a function, mac-fn, from
ACL2 objects to an ACL2 object to be treated as an untranslated term.
For example, caar is defined as a macro symbol; the associated macro
function maps the object x into the object (car (car x)).  A macro form
is a "call" of a macro symbol, i.e., a list whose car is the macro
symbol and whose cdr is an arbitrary true list of objects, used as a
term.  Macroexpansion is the process of replacing in an untranslated
term every occurrence of a macro form by the result of applying the
macro function to the appropriate arguments.  The "appropriate"
arguments are determined by the exact form of the definition of the
macro; macros support positional, keyword, optional and other kinds of
arguments.  See DEFMACRO.

In addition to macroexpansion and constant symbol dereferencing,
translation implements the mapping of let and let* forms into
applications of lambda expressions and closes lambda expressions
containing free variables.  Thus, the translation of

     (let ((x (1+ i))) (cons x k))

can be seen as a two-step process that first produces

     ((lambda (x) (cons x k)) (1+ i))

and then

     ((lambda (x k) (cons x k)) (1+ i) k) .

Observe that the body of the let and of the first lambda expression
contains a free k which is finally bound and passed into the second
lambda expression.

Translation also maps flet forms into applications of lambda
expressions.  See FLET.

When we say, of an event-level function such as defun or defthm, that
some argument "must be a term" we mean an untranslated term.  The event
functions translate their term-like arguments.

To better understand the mapping between untranslated terms and
translated terms it is convenient to use the keyword command :trans to
see examples of translations.  See TRANS and also see
TRANS1.

Finally, we note that the theorem prover prints terms in untranslated
form.  But there can be more than one correct untranslated term
corresponding to a given translated term.  For example, the translated
term (if x y 'nil) can be untranslated as (if x y nil) and can also be
untranslated as (and x y).  The theorem prover attempts to print an
untranslated term that is as helpful to the user as possible.  In
particular, consider a term of the form (nth k st) where st is a
single-threaded object (see STOBJ) and the kth accessor of st
is, say, kn.  The theorem prover typically would expand (kn st) to (nth
k st).  If k is large then it could be difficult for the user to make
sense out of a proof transcript that mentions the expanded term.
Fortunately, the untranslation of (nth k st) would be (nth *kn* st);
here *kn* would be a constant (see DEFCONST) added by the
defstobj event introducing st, defined to have value k.  The user can
extend this user-friendly style of printing applications of nth to
stobjs; see ADD-NTH-ALIAS.  These remarks about printing
applications of function nth extend naturally to function update-nth.
Moreover, the prover will attempt to treat terms as stobjs for the
above purpose when appropriate.  For example, if function foo has
signature ((foo * st) => (mv * * * st)), where st is introduced with
(defstobj st f0 f1), then the term (nth '1 (mv-nth '3 (foo x st0)))
will be printed as (nth *f1* (mv-nth 3 (foo x st0))).

_Pseudo-Terms:  A Common Guard for Metafunctions_

Because termp is defined in :program mode, it cannot be used
effectively in conjectures to be proved.  Furthermore, from the
perspective of merely guarding a term processing function, termp often
checks more than is required.  Finally, because termp requires the
logical world as one of its arguments it is impossible to use termp as
a guard in places where the logical world is not itself one of the
arguments.

For these reasons we support the idea of "pseudo-terms."  A pseudo-term
is either a symbol (but not necessarily one having the syntax of a
legal variable symbol), a true list beginning with quote (but not
necessarily well-formed), or the "application of" a symbol or pseudo
lambda expression to a true list of pseudo-terms.  A pseudo lambda
expression is an expression of the form (lambda (v1 ... vn) body) where
the vi are all symbols and body is a pseudo-term.

Pseudo-terms are recognized by the unary function pseudo-termp.  If
(termp x w) is true, then (pseudo-termp x) is true.  However, if x
fails to be a (strict) term it may nevertheless still be a pseudo-term.
For example, (car a b) is not a term, because car is applied to the
wrong number of arguments, but it is a pseudo-term.

The structures recognized by pseudo-termp can be recursively explored
with the same simplicity that terms can be.  In particular, if x is not
a variablep or an fquotep, then (ffn-symb x) is the function (symbol or
lambda expression) and (fargs x) is the list of argument pseudo-terms.
A metafunction (see META) or clause-processor (see
CLAUSE-PROCESSOR) may use pseudo-termp as the guard.

THE-METHOD    how to find proofs

Also see INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed
tutorial on how to prove theorems with ACL2.

Many users develop proof scripts in an Emacs buffer and submit one
event at a time to the theorem prover running in a *shell* buffer.  The
script buffer is logically divided into two regions: the events that
have been accepted by the theorem prover and those that have not yet
been accepted.  An imaginary "barrier" divides these two regions.  The
region above the barrier describes the state of the *shell* buffer (and
ACL2's logical world).  The region below the barrier is the "to do"
list.

We usually start a proof project by typing the key lemmas, and main
goal into the to do list.  Definitions are here just regarded as
theorems to prove (i.e., the measure conjectures).  Then we follow "The
Method."

(1) Think about the proof of the first theorem in the to do list.
Structure the proof either as an induction followed by simplification
or just simplification.  Have the necessary lemmas been proved? That
is, are the necessary lemmas in the done list already?  If so, proceed
to Step 2.  Otherwise, add the necessary lemmas at the front of the to
do list and repeat Step 1.

(2) Call the theorem prover on the first theorem in the to do list and
let the output stream into the *shell* buffer.  Abort the proof if it
runs more than a few seconds.

(3) If the theorem prover succeeded, advance the barrier past the
successful command and go to Step 1.

(4) Otherwise, inspect the failed proof attempt, starting from the
beginning, not the end.  Basically you should look for the first place
the proof attempt deviates from your imagined proof.  If your imagined
proof was inductive, inspect the induction scheme used by ACL2.  If
that is ok, then find the first subsequent subgoal that is stable under
simplification and think about why it was not proved by the simplifier.
If your imagined proof was not inductive, then think about the first
subgoal stable under simplification, as above.  Modify the script
appropriately.  It usually means adding lemmas to the to do list, just
in front of the theorem just tried.  It could mean adding hints to the
current theorem.  In any case, after the modifications go to Step 1.

We do not seriously suggest that this or any rotely applied algorithm
will let you drive ACL2 to difficult proofs.  Indeed, to remind you of
this we call this "The Method" rather than "the method."  That is, we
are aware of the somewhat pretentious nature of any such advice.  But
these remarks have helped many users approach ACL2 in a constructive
and disciplined way.

We say much more about The Method in the ACL2 book.  See the home page.
Also see SET-GAG-MODE for a discussion of a way for ACL2 to
help you to use The Method.  And again, see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed tutorial.

Learning to read failed proofs is a useful skill.  There are several
kinds of "checkpoints" in a proof: (1) a formula to which induction is
being (or would be) applied, (2) the first formula stable under
simplification, (3) a formula that is possibly generalized, either by
cross-fertilizing with and throwing away an equivalence hypothesis or
by explicit generalization of a term with a new variable.

At the induction checkpoint, confirm that you believe the formula being
proved is a theorem and that it is appropriately strong for an inductive
proof.  Read the selected induction scheme and make sure it agrees with
your idea of how the proof should go.

At the post-simplification checkpoint, which is probably the most
commonly seen, consider whether there are additional rewrite rules you
could prove to make the formula simplify still further.  Look for
compositions of function symbols you could rewrite.  Look for
contradictions among hypotheses and prove the appropriate implications:
for example, the checkpoint might contain the two hypotheses (P (F A))
and (NOT (Q (G (F A)))) and you might realize that (implies (p x) (q (g
x))) is a theorem.  Look for signs that your existing rules did not
apply, e.g., for terms that should have been rewritten, and figure out
why they were not.  Possible causes include that they do not exactly
match your old rules, that your old rules have hypotheses that cannot
be relieved here - perhaps because some other rules are missing, or
perhaps your old rules are disabled.  If you cannot find any further
simplifications to make in the formula, ask yourself whether it is
valid.  If so, sketch a proof.  Perhaps the proof is by appeal to a
combination of lemmas you should now prove?

At the two generalization checkpoints -- where hypotheses are discarded
or terms are replaced by variables -- ask yourself whether the result
is a theorem.  It often is not.  Think about rewrite rules that would
prove the formula.  These are often restricted versions of the
overly-general formulas created by the system's heuristics.

See PROOF-TREE for a discussion of a tool to help you navigate
through ACL2 proofs.

TRUST-TAG    See DEFTTAG.

TTAGS-SEEN    list some declared trust tags (ttags)

     General Forms:
     :ttags-seen
     (ttags-seen)

Suppose the output is as follows.

     (T NIL)
     (FOO "/home/bob/bar.lisp"
          "/home/cindy/bar.lisp")
     Warning: This output is minimally trustworthy (see :DOC TTAGS-SEEN).

This output indicates that the current logical world has seen the
declaration of trust tag T at the top-level (see DEFTTAG) and
the declaration of trust tag FOO in the two books included from the
listed locations.  The warning emphasizes that this command cannot be
used to validate the "purity" of an ACL2 session, because using a ttag
renders enough power to hide from this or any other command the fact
that the ttag was ever declared.

As discussed elsewhere (see DEFTTAG), the only reliable way to
validate the "purity" of a session is to watch for "TTAG NOTE" output.

Another shortcoming of this command is that it only checks the current
logical world for ttag declarations.  For example, one could execute a
defttag event; then use progn! and set-raw-mode to replace system
functions with corrupt definitions or to introduce inconsistent axioms
in the ground-zero world; and finally, execute :ubt! 1 to remove all
evidence of the ttag in the world while leaving in place the corrupt
definitions or axioms.  The base world is now tainted, meaning we could
prove nil or certify a book that proves nil, but the resulting session
or book would contain no trace of the ttag that tainted it!

Despite shortcomings, this command might be useful to system hackers.
It also serves to illustrate the inherent flaw in asking a session
whether or how it is "tainted", justifying the "TTAG NOTE" approach
(see DEFTTAG).

TTREE    tag-trees

Many low-level ACL2 functions take and return "tag trees" or "ttrees"
(pronounced "tee-trees") which contain various useful bits of
information such as the lemmas used, the linearize assumptions made,
etc.

Abstractly a tag-tree represents a list of sets, each member set having
a name given by one of the "tags" (which are symbols) of the ttree.  The
elements of the set named tag are all of the objects tagged tag in the
tree.  You are invited to browse the source code.  Definitions of
primitives are labeled with the comment "; Note: Tag-tree primitive".

The rewriter, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.  Term'
is equivalent to term (under the current assumptions) and the ttree' is
an extension of ttree.  If we focus just on the set associated with the
tag LEMMA in the ttrees, then the set for ttree' is the extension of
that for ttree obtained by unioning into it all the runes used by the
rewrite.  The set associated with LEMMA can be obtained by
(tagged-objects 'LEMMA ttree).

TYPE-SET    how type information is encoded in ACL2

To help you experiment with type-sets we briefly note the following
utility functions.

(type-set-quote x) will return the type-set of the object x.  For
example, (type-set-quote "test") is 2048 and (type-set-quote '(a b c))
is 512.

(type-set 'term nil nil nil (ens state) (w state) nil nil nil) will
return the type-set of term.  For example,

     (type-set '(integerp x) nil nil nil (ens state) (w state) nil nil nil)

will return (mv 192 nil).  192, otherwise known as *ts-boolean*, is the
type-set containing t and nil.  The second result may be ignored in
these experiments.  Term must be in the translated, internal form shown
by :trans.  See TRANS and see TERM.

(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil) will
return the type-set deduced for the variable symbol x assuming the
translated term, term, true.  The second result may be ignored in these
experiments.  For example,

     (type-set-implied-by-term 'v nil '(integerp v)
                               (ens state) (w state) nil)

returns 11.

(convert-type-set-to-term 'x ts (ens state) (w state) nil) will return
a term whose truth is equivalent to the assertion that the term x has
type-set ts.  The second result may be ignored in these experiments.
For example

     (convert-type-set-to-term 'v 523 (ens state) (w state) nil)

returns a term expressing the claim that v is either an integer or a
non-nil true-list.  523 is the logical-or of 11 (which denotes the
integers) with 512 (which denotes the non-nil true-lists).

The "actual primitive types" of ACL2 are listed in
*actual-primitive-types*, whose elements are shown below.  Each actual
primitive type denotes a set -- sometimes finite and sometimes not --
of ACL2 objects and these sets are pairwise disjoint.  For example,
*ts-zero* denotes the set containing 0 while *ts-positive-integer*
denotes the set containing all of the positive integers.

     *TS-ZERO*                  ;;; {0}
     *TS-POSITIVE-INTEGER*      ;;; positive integers
     *TS-POSITIVE-RATIO*        ;;; positive non-integer rationals
     *TS-NEGATIVE-INTEGER*      ;;; negative integers
     *TS-NEGATIVE-RATIO*        ;;; negative non-integer rationals
     *TS-COMPLEX-RATIONAL*      ;;; complex rationals
     *TS-NIL*                   ;;; {nil}
     *TS-T*                     ;;; {t}
     *TS-NON-T-NON-NIL-SYMBOL*  ;;; symbols other than nil, t
     *TS-PROPER-CONS*           ;;; null-terminated non-empty lists
     *TS-IMPROPER-CONS*         ;;; conses that are not proper
     *TS-STRING*                ;;; strings
     *TS-CHARACTER*             ;;; characters

The actual primitive types were chosen by us to make theorem proving
convenient.  Thus, for example, the actual primitive type *ts-nil*
contains just nil so that we can encode the hypothesis "x is nil" by
saying "x has type *ts-nil*" and the hypothesis "x is non-nil" by
saying "x has type complement of *ts-nil*."  We similarly devote a
primitive type to t, *ts-t*, and to a third type,
*ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.

Let *ts-other* denote the set of all Common Lisp objects other than
those in the actual primitive types.  Thus, *ts-other* includes such
things as floating point numbers and CLTL array objects.  The actual
primitive types together with *ts-other* constitute what we call
*universe*.  Note that *universe* is a finite set containing one more
object than there are actual primitive types; that is, here we are
using *universe* to mean the finite set of primitive types, not the
infinite set of all objects in all of those primitive types.
*Universe* is a partitioning of the set of all Common Lisp objects:
every object belongs to exactly one of the sets in *universe*.

Abstractly, a "type-set" is a subset of *universe*.  To say that a
term, x, "has type-set ts" means that under all possible assignments to
the variables in x, the value of x is a member of some member of ts.
Thus, (cons x y) has type-set {*ts-proper-cons* *ts-improper-cons*}.  A
term can have more than one type-set.  For example, (cons x y) also has
the type-set {*ts-proper-cons* *ts-improper-cons* *ts-nil*}.
Extraneous types can be added to a type-set without invalidating the
claim that a term "has" that type-set.  Generally we are interested in
the smallest type-set a term has, but because the entire theorem-proving
problem for ACL2 can be encoded as a type-set question, namely, "Does p
have type-set complement of *ts-nil*?," finding the smallest type-set
for a term is an undecidable problem.  When we speak informally of
"the" type-set we generally mean "the type-set found by our heuristics"
or "the type-set assumed in the current context."

Note that if a type-set, ts, does not contain *ts-other* as an element
then it is just a subset of the actual primitive types.  If it does
contain *ts-other* it can be obtained by subtracting from *universe*
the complement of ts.  Thus, every type-set can be written as a
(possibly complemented) subset of the actual primitive types.

By assigning a unique bit position to each actual primitive type we can
encode every subset, s, of the actual primitive types by the
nonnegative integer whose ith bit is on precisely if s contains the ith
actual primitive type.  The type-sets written as the complement of s
are encoded as the twos-complement of the encoding of s.  Those
type-sets are thus negative integers.  The bit positions assigned to
the actual primitive types are enumerated from 0 in the same order as
the types are listed in *actual-primitive-types*.  At the concrete
level, a type-set is an integer between *min-type-set* and
*max-type-set*, inclusive.

For example, *ts-nil* has bit position 6.  The type-set containing just
*ts-nil* is thus represented by 64.  If a term has type-set 64 then the
term is always equal to nil.  The type-set containing everything but
*ts-nil* is the twos-complement of 64, which is -65.  If a term has
type-set -65, it is never equal to nil.  By "always" and "never" we
mean under all, or under no, assignments to the variables, respectively.

Here is a more complicated example.  Let s be the type-set containing
all of the symbols and the natural numbers.  The relevant actual
primitive types, their bit positions and their encodings are:

     actual primitive type       bit    value

     *ts-zero*                    0       1
     *ts-positive-integer*        1       2
     *ts-nil*                     6      64
     *ts-t*                       7     128
     *ts-non-t-non-nil-symbol*    8     256

Thus, the type-set s is represented by (+ 1 2 64 128 256) = 451.  The
complement of s, i.e., the set of all objects other than the natural
numbers and the symbols, is -452.

USE    hints keyword :USE

See HINTS.

USING-COMPUTED-HINTS    how to use computed hints

Computed hints (see COMPUTED-HINTS) are extraordinarily
powerful.  We show a few examples here to illustrate their use.  We
recommend that the using-computed-hints-n topics be read in the order
using-computed-hints-1, using-computed-hints-2, and so on.

Related topics other than immediate subtopics:

USING-COMPUTED-HINTS-1    Driving Home the Basics

The common hint

     ("Subgoal 3.2.1''" :use lemma42)

has the same effect as the computed hint

     (if (equal id '((0) (3 2 1) . 2))
         '(:use lemma42)
         nil)

which, of course, is equivalent to

     (and (equal id '((0) (3 2 1) . 2))
          '(:use lemma42))

which is also equivalent to the computed hint

     my-special-hint

provided the following defun has first been executed

     (defun my-special-hint (id clause world)
       (declare (xargs :mode :program)
                (ignore clause world))
       (if (equal id '((0) (3 2 1) . 2))
           '(:use lemma42)
           nil))

It is permitted for the defun to be in :LOGIC mode (see
DEFUN-MODE) also.

Just to be concrete, the following three events all behave the same way
(if my-special-hint is as above):

     (defthm main (big-thm a b c)
       :hints (("Subgoal 3.2.1''" :use lemma42)))

     (defthm main (big-thm a b c)
       :hints ((and (equal id '((0) (3 2 1) . 2)) '(:use lemma42))))

     (defthm main (big-thm a b c)
       :hints (my-special-hint))

USING-COMPUTED-HINTS-2    One Hint to Every Top-Level Goal in a Forcing Round

Suppose the main proof completes with a forcing round on three
subgoals, "[1]Subgoal 3", "[1]Subgoal 2", and "[1]Subgoal 1".  Suppose
you wish to :use lemma42 in all top-level goals of the first forcing
round.  This can be done supplying the hint

     (if test '(:use lemma42) nil),

where test is an expression that returns t when ID is one of the clause
ids in question.

         goal-spec     (parse-clause-id goal-spec)

     "[1]Subgoal 3"        ((1) (3) . 0)
     "[1]Subgoal 2"        ((1) (2) . 0)
     "[1]Subgoal 1"        ((1) (1) . 0)

Recall (see CLAUSE-IDENTIFIER) that parse-clause-id maps from a
goal spec to a clause id, so you can use that function on the goal
specs printed in the failed proof attempt to determine the clause ids
in question.

So one acceptable test is

     (member-equal id '(((1) (3) . 0)
                        ((1) (2) . 0)
                        ((1) (1) . 0)))

or you could use parse-clause-id in your computed hint if you don't
want to see clause ids in your script:

     (or (equal id (parse-clause-id "[1]Subgoal 3"))
         (equal id (parse-clause-id "[1]Subgoal 2"))
         (equal id (parse-clause-id "[1]Subgoal 1")))

or you could use the inverse function (see CLAUSE-IDENTIFIER):

     (member-equal (string-for-tilde-@-clause-id-phrase id)
                   '("[1]Subgoal 3"
                     "[1]Subgoal 2"
                     "[1]Subgoal 1"))

Recall that what we've shown above are the tests to use in the computed
hint.  The hint itself is (if test '(:use lemma42) nil) or something
equivalent like (and test '(:use lemma42)).

The three tests above are all equivalent.  They suffer from the problem
of requiring the explicit enumeration of all the goal specs in the
first forcing round.  A change in the script might cause more forced
subgoals and the ones other than those enumerated would not be given
the hint.

You could write a test that recognizes all first round top-level
subgoals no matter how many there are.  Just think of the programming
problem:  how do I recognize all the clause id's of the form ((1) (n) .
0)?  Often you can come to this formulation of the problem by using
parse-clause-id on a few of the candidate goal-specs to see the common
structure.  A suitable test in this case is:

     (and (equal (car id) '(1))     ; forcing round 1, top-level (pre-induction)
          (equal (len (cadr id)) 1) ; Subgoal n (not Subgoal n.i ...)
          (equal (cddr id) 0))      ; no primes

The test above is "overkill" because it recognizes precisely the clause
ids in question.  But recall that once a computed hint is used, it is
(by default) removed from the hints available to the children of the
clause.  Thus, we can widen the set of clause ids recognized to include
all the children without worrying that the hint will be applied to
those children.

In particular, the following test supplies the hint to every top-level
goal of the first forcing round:

     (equal (car id) '(1))

You might worry that it would also supply the hint to the subgoal
produced by the hint - the cases we ruled out by the "overkill" above.
But that doesn't happen since the hint is unavailable to the children.
You could even write:

     (equal (car (car id)) 1)

which would supply the hint to every goal of the form "[1]Subgoal ..."
and again, because we see and fire on the top-level goals first, we
will not fire on, say, "[1]Subgoal *1.3/2", i.e., the id '((1 1 3) (2)
. 0) even though the test recognizes that id.

Finally, the following test supplies the hint to every top-level goal
of every forcing round (except the 0th, which is the "gist" of the
proof, not "really" a forcing round):

     (not (equal (car (car id)) 0))

Recall again that in all the examples above we have exhibited the test
in a computed hint of the form (if test '(:key1 val1 ...) nil).

USING-COMPUTED-HINTS-3    Hints as a Function of the Goal (not its Name)

Sometimes it is desirable to supply a hint whenever a certain term
arises in a conjecture.  For example, suppose we have proved

     (defthm all-swaps-have-the-property
        (the-property (swap x))
        :rule-classes nil)

and suppose that whenever (SWAP A) occurs in a goal, we wish to add the
additional hypothesis that (THE-PROPERTY (SWAP A)).  Note that this is
equivalent supplying the hint

     (if test
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

where test answers the question "does the clause contain (SWAP A)?"
That question can be asked with (occur-lst '(SWAP A) clause).  Briefly,
occur-lst takes the representation of a translated term, x, and a list
of translated terms, y, and determines whether x occurs as a subterm of
any term in y.  (By "subterm" here we mean proper or improper, e.g.,
the subterms of (CAR X) are X and (CAR X).)

Thus, the computed hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal
containing (SWAP A) - except the children of goals to which the
hypothesis was added.

A COMMON MISTAKE users are likely to make is to forget that they are
dealing with translated terms.  For example, suppose we wished to look
for (SWAP (LIST 1 A)) with occur-lst.  We would never find it with

     (occur-lst '(SWAP (LIST 1 A)) clause)

because that presentation of the term contains macros and other
abbreviations.  By using :trans (see TRANS) we can obtain the
translation of the target term.  Then we can look for it with:

     (occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)

Note in particular that you must

     * eliminate all macros and
     * explicitly quote all constants.

We recommend using :trans to obtain the translated form of the terms in
which you are interested, before programming your hints.

An alternative is to use the expression (prettyify-clause clause nil
nil) in your hint to convert the current goal clause into the
s-expression that is actually printed.  For example, the clause

     ((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y))

"prettyifies" to

     (IMPLIES (AND (CONSP X)
                   (NOT (SYMBOLP Y)))
              (EQUAL (CONS 1 (CAR X)) Y))

which is what you would see printed by ACL2 when the goal clause is
that shown.

However, if you choose to convert your clauses to prettyified form, you
will have to write your own explorers (like our occur-lst), because all
of the ACL2 term processing utilities work on translated and/or clausal
forms.  This should not be taken as a terrible burden.  You will, at
least, gain the benefit of knowing what you are really looking for,
because your explorers will be looking at exactly the s-expressions you
see at your terminal.  And you won't have to wade through our still
undocumented term/clause utilities.  The approach will slow things down
a little, since you will be paying the price of independently consing
up the prettyified term.

We make one more note on this example.  We said above that the computed
hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal
containing (SWAP A) - except the children of goals to which the
hypothesis was added.

It bears noting that the subgoals produced by induction and top-level
forcing round goals are not children.  For example, suppose the hint
above fires on "Subgoal 3" and produces, say, "Subgoal 3'".  Then the
hint will not fire on "Subgoal 3'" even though it (still) contains
(SWAP A) because "Subgoal 3'" is a child of a goal on which the hint
fired.

But now suppose that "Subgoal 3'" is pushed for induction.  Then the
goals created by that induction, i.e., the base case and induction
step, are not considered children of "Subgoal 3'".  All of the original
hints are available.

Alternatively, suppose that "Subgoal 3' is proved but forces some other
subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1.  That
top-level forced subgoal is not a child.  All the original hints are
available to it.  Thus, if it contains (SWAP A), the hint will fire and
supply the hypothesis, producing "[1]Subgoal 1'".  This may be
unnecessary, as the hypothesis might already be present in "[1]Subgoal
1".  In this case, no harm is done.  The hint won't fire on "[1]Subgoal
1" because it is a child of "[1]Subgoal 1" and the hint fired on that.

USING-COMPUTED-HINTS-4    Computing the Hints

So far we have used computed hints only to compute when a fixed set of
keys and values are to be used as a hint.  But computed hints can, of
course, compute the set of keys and values.  You might, for example,
write a hint that recognizes when a clause "ought" to be provable by a
:BDD hint and generate the appropriate hint.  You might build in a set
of useful lemmas and check to see if the clause is provable :BY one of
them.  You can keep all function symbols disabled and use computed
hints to compute which ones you want to :EXPAND.  In general, you can
write a theorem prover for use in your hints, provided you can get it
to do its job by directing our theorem prover.

Suppose for example we wish to find every occurrence of an instance of
(SWAP x) and provide the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  Obviously, we must explore the clause
looking for instances of (SWAP x) and build the appropriate instances
of the lemma.  We could do this in many different ways, but below we
show a general purpose set of utilities for doing it.  The functions
are not defined in ACL2 but could be defined as shown.

Our plan is:  (1) Find all instances of a given pattern (term) in a
clause, obtaining a set of substitutions.  (2) Build a set of :instance
expressions for a given lemma name and set of substitutions.  (3)
Generate a :use hint for those instances when instances are found.

The pair of functions below find all instances of a given pattern term
in either a term or a list of terms.  The functions each return a list
of substitutions, each substitution accounting for one of the matches
of pat to a subterm.  At this level in ACL2 substitutions are lists of
pairs of the form (var . term).  All terms mentioned here are presumed
to be in translated form.

The functions take as their third argument a list of substitutions
accumulated to date and add to it the substitutions produced by
matching pat to the subterms of the term.  We intend this accumulator
to be nil initially.  If the returned value is nil, then no instances
of pat occurred.

     (mutual-recursion

     (defun find-all-instances (pat term alists)
      (declare (xargs :mode :program))
      (mv-let
       (instancep alist)
       (one-way-unify pat term)
       (let ((alists (if instancep (add-to-set-equal alist alists) alists)))
         (cond
          ((variablep term) alists)
          ((fquotep term) alists)
          ((flambdap (ffn-symb term))
           (find-all-instances pat
                               (lambda-body (ffn-symb term))
                               (find-all-instances-list pat (fargs term) alists)))
          (t (find-all-instances-list pat (fargs term) alists))))))

     (defun find-all-instances-list (pat list-of-terms alists)
      (declare (xargs :mode :program))
      (cond
       ((null list-of-terms) alists)
       (t (find-all-instances pat
                              (car list-of-terms)
                              (find-all-instances-list pat
                                                       (cdr list-of-terms)
                                                       alists))))))

We now turn our attention to converting a list of substitutions into a
list of lemma instances, each of the form

     (:INSTANCE name (var1 term1) ... (vark termk))

as written in :use hints.  In the code shown above, substitutions are
lists of pairs of the form (var . term), but in lemma instances we must
write "doublets."  So here we show how to convert from one to the other:

     (defun pairs-to-doublets (alist)
       (declare (xargs :mode :program))
       (cond ((null alist) nil)
             (t (cons (list (caar alist) (cdar alist))
                      (pairs-to-doublets (cdr alist))))))

Now we can make a list of lemma instances:

     (defun make-lemma-instances (name alists)
       (declare (xargs :mode :program))
       (cond
        ((null alists) nil)
        (t (cons (list* :instance name (pairs-to-doublets (car alists)))
                 (make-lemma-instances name (cdr alists))))))

Finally, we can package it all together into a hint function.  The
function takes a pattern, pat, which must be a translated term, the
name of a lemma, name, and a clause.  If some instances of pat occur in
clause, then the corresponding instances of name are :USEd in the
computed hint.  Otherwise, the hint does not apply.

     (defun add-corresponding-instances (pat name clause)
       (declare (xargs :mode :program))
       (let ((alists (find-all-instances-list pat clause nil)))
         (cond
          ((null alists) nil)
          (t (list :use (make-lemma-instances name alists))))))

The design of this particular hint function makes it important that the
variables of the pattern be the variables of the named lemma and that
all of the variables we wish to instantiate occur in the pattern.  We
could, of course, redesign it to allow "free variables" or some sort of
renaming.

We could now use this hint as shown below:

     (defthm ... ...
       :hints ((add-corresponding-instances
                '(SWAP x)
                'ALL-SWAPS-HAVE-THE-PROPERTY
                clause)))

The effect of the hint above is that any time a clause arises in which
any instance of (SWAP x) appears, we add the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  So for example, if Subgoal *1/3.5
contains the subterm (SWAP (SWAP A)) then this hint fires and makes the
system behave as though the hint:

     ("Subgoal *1/3.5"
      :USE ((:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X A))
            (:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X (SWAP A)))))

had been present.

USING-COMPUTED-HINTS-5    Debugging Computed Hints

We have found that it is sometimes helpful to define hints so that they
print out messages to the terminal when they fire, so you can see what
hint was generated and which of your computed hints did it.

To that end we have defined a macro we sometimes use.  Suppose you have
a :hints specification such as:

     :hints (computed-hint-fn (hint-expr id))

If you defmacro the macro below you could then write instead:

     :hints ((show-hint computed-hint-fn 1)
             (show-hint (hint-expr id) 2))

with the effect that whenever either hint is fired (i.e., returns
non-nil), a message identifying the hint by the marker (1 or 2, above)
and the non-nil value is printed.

     (defmacro show-hint (hint &optional marker)
       (cond
        ((and (consp hint)
              (stringp (car hint)))
         hint)
        (t
         `(let ((marker ,marker)
                (ans ,(if (symbolp hint)
                          `(,hint id clause world stable-under-simplificationp)
                        hint)))
            (if ans
                (prog2$
                 (cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]~%~x2~%~%"
                     (if (null marker) 0 1)
                     marker
                     (cons (string-for-tilde-@-clause-id-phrase id)
                           ans))
                 ans)
              nil)))))

Note that when show-hint is applied to a hint that is a symbol, e.g.,
computed-hint-fn, it applies the symbol to the four computed-hint
arguments: id, clause, world, and stable-under-simplificationp.  If
computed-hint-fn is of arity 3 the code above would cause an error.
One way to avoid it is to write

     :hints ((show-hints (computed-hint-fn id clause world) 1)
             (show-hint (hint-expr id) 2)).

If you only use computed hints of arity 3, you might eliminate the
occurrence of stable-under-simplificationp in the definition of
show-hint above.

Putting a show-hint around a common hint has no effect.  If you find
yourself using this utility let us know and we'll consider putting it
into the system itself.  But it does illustrate that you can use
computed hints to do unusual things.

USING-COMPUTED-HINTS-6    Using the computed-hint-replacement feature

So far none of our computed hints have used the
:COMPUTED-HINT-REPLACEMENT feature.  We now illustrate that.

The :computed-hint-replacement feature can easily lead to loops.  So as
you experiment with the examples in this section and your own hints
using this feature, be ready to interrupt the theorem prover and abort!

A non-looping use of the :computed-hint-replacement feature would be a
hint like this:

     (if (certain-terms-present clause)
         '(:computed-hint-replacement t
           :in-theory (enable lemma25))
         '(:computed-hint-replacement t
           :in-theory (disable lemma25)))

In this hint, if certain terms are present in clause, as determined by
the function with the obvious name (here undefined), then this hint
enables lemma25 and otherwise disables it.  Lemma25 might be a very
expensive lemma, e.g., one that matches frequently and has an expensive
and rarely established hypothesis.  One might wish it enabled only
under certain conditions.  Recall that theories are inherited by
children.  So once lemma25 is enabled it "stays" enabled for the
children, until disabled; and vice versa.  If the
:computed-hint-replacement feature were not present and computed hints
were always deleted after they had been used, then lemma25 would be
left enabled (or disabled) for all the childen produced by the first
firing of the hint.  But with the arrangement here, every subgoal gets
a theory deemed suitable by the hint, and the hint persists.

Now we will set up a toy to allow us to play with computed hints to
understand them more deeply.  To follow the discussion it is best to
execute the following events.

     (defstub wrapper (x) t)
     (defaxiom wrapper-axiom (wrapper x) :rule-classes nil)

Now submit the following event and watch what happens.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x a)))))

The theorem prover adds (wrapper a) to the goal and then abandons the
proof attempt because it cannot prove the subgoal.  Since the computed
hint is deleted upon use, the hint is not applied to the subgoal (i.e.,
the child of the goal).

What happens if we do the following?

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x a)))))

As one might expect, this loops forever: The hint is applied to the
child and adds the hypothesis again.  When the hint fires, nothing is
actually changed, since (wrapper a) is already in the subgoal.

So let's change the experiment a little.  Let's make the hint add the
hypothesis (wrapper p) where p is the first literal of the clause.
This is silly but it allows us to explore the behavior of computed
hints a little more.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x ,(car clause))))))

So in this case, the theorem prover changes the goal to

     (IMPLIES (WRAPPER (EQUAL U V)) (EQUAL U V))

which then simplifies to

     (IMPLIES (WRAPPER NIL) (EQUAL U V))

because the concluding equality can be assumed false in the hypothesis
(e.g., think of the contrapositive version).  Nothing else happens
because the hint has been removed and so is not applicable to the child.

Now consider the following - and be ready to interrupt it and abort!

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x ,(car clause))))))

This time the hint is not removed and so is applied to the child.  So
from Goal we get

     Goal'
     (IMPLIES (WRAPPER (EQUAL U V))
              (EQUAL U V))

and then

     Goal''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER (EQUAL U V))))
                   (WRAPPER (EQUAL U V)))
              (EQUAL U V))

etc.

First, note that the hint is repeatedly applied to its children.  That
is because we wrote :computed-hint-replacement t.  But second, note
that Goal' is not even being simplified before Goal" is produced from
it.  If it were being simplified, the (equal u v)'s in the hypotheses
would be replaced by nil.  This is a feature.  It means after a
computed hint has fired, other hints are given a chance at the result,
even the hint itself unless it is removed from the list of hints.

As an exercise, let's arrange for the hint to stay around and be
applied indefinitely but with a simplification between each use of the
the hint.  To do this we need to pass information from one application
of the hint to the next, essentially to say "stay around but don't
fire."

First, we will define a function to use in the hint.  This is more than
a mere convenience; it allows the hint to "reproduce itself" in the
replacement.

     (defun wrapper-challenge (clause parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car clause))))
           `(:computed-hint-replacement ((wrapper-challenge clause t)))))

Note that this function is not recursive, even though it uses its own
name.  That is because the occurrence of its name is in a quoted
constant.

Now consider the following.  What will it do?

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

First, observe that this is a legal hint because it is a term that
mentions only the free variable CLAUSE.  When defining hint functions
you may sometimes think their only arguments are the four variables id,
clause, world, and stable-under-simplificationp.  That is not so.  But
in your hints you must call those functions so that those are the only
free variables.  Note also that the occurrence of clause inside the
:computed-hint-replacement is not an occurrence of the variable clause
but just a constant.  Just store this note away for a moment.  We'll
return to it momentarily.

Second, the basic cleverness of this hint is that every time it fires
it reproduces itself with the opposite parity.  When the parity is t it
actually changes the goal by adding a hypothesis.  When the parity is
nil it doesn't change the goal and so allows simplification to proceed
- but it swaps the parity back to t.  What you can see with this simple
toy is that we can use the computed hints to pass information from
parent to child.

Ok, so what happens when the event above is executed?  Try it.  You will
see that ACL2 applied the hint the first time.  It doesn't get around to
printing the output because an error is caused before it can print.
But here is a blow-by-blow description of what happens.  The hint is
evaluated on Goal with the clause ((equal u v)).  It produces a hint
exactly as though we had typed:

     ("Goal" :use (:instance wrapper-axiom (x (equal u v))))

which is applied to this goal. In addition, it produces the new hints
argument

     :hints ((wrapper-challenge clause nil)).

By applying the "Goal" hint we get the new subgoal

     Goal'
     (implies (wrapper (equal u v))
              (equal u v))

but this is not printed because, before printing it, the theorem prover
looks for hints to apply to it and finds

     (wrapper-challenge clause nil)

That is evaluated and produces a hint exactly as though we had typed:

     ("Goal'" )

and the new hints argument:

     :hints ((wrapper-challenge clause nil)).

But if you supply the hint ("Goal'" ), ACL2 will signal an error
because it does not allow you to specify an empty hint!

So the definition of wrapper-challenge above is almost correct but
fatally flawed.  We need a non-empty "no-op" hint.  One such hint is to
tell the system to expand a term that will always be expanded anyway.
So undo wrapper-challenge, redefine it, and try the proof again.  Now
remember the observation about clause that we asked you to "store"
above.  The new definition of wrapper-challenge illustrates what we
meant.  Note that the first formal parameter of wrapper-challenge,
below, is no longer named clause but is called cl instead.  But the
"call" of wrapper-challenge in the replacements is on clause.  This may
seem to violate the rule that a function definition cannot use
variables other than the formals.  But the occurrences of clause below
are not variables but constants in an object that will eventually be
treated as hint term.

     :ubt wrapper-challenge

     (defun wrapper-challenge (cl parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car cl))))
           `(:computed-hint-replacement ((wrapper-challenge clause t))
             :expand ((atom zzz)))))

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

This time, things go as you might have expected!  Goal' is produced and
simplified, to

     Goal''
     (implies (wrapper nil)
              (equal u v)).

Simplification gets a chance because when the new hint
(wrapper-challenge clause nil) is fired it does not change the goal.
But it does change the parity in the hints argument so that before
Goal" is simplified again, the hint fires and adds the hypothesis:

     Goal'''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER NIL)))
                   (WRAPPER NIL))
              (EQUAL U V)).

This simplifies, replacing the first (NOT (WRAPPER NIL)) by NIL, since
(WRAPPER NIL) is known to be true here.  Thus the goal simplifies to

     Goal'4'
     (IMPLIES (WRAPPER NIL) (EQUAL U V)).

The process repeats indefinitely.

So we succeeded in getting a hint to fire indefinitely but allow a full
simplification between rounds.

USING-COMPUTED-HINTS-7    Using the stable-under-simplificationp flag

A problem with the example in using-computed-hints-6 is that exactly
one simplification occurs between each (effective) firing of the hint.
Much more commonly we wish to fire a hint once a subgoal has become
stable under simplification.

A classic example of this is when we are dealing with an interpreter
for some state machine.  We typically do not want the "step" function
to open up on the symbolic representation of a state until that state
has been maximally simplified.  We will illustrate with a simple state
machine.

Let us start by defining the step function, stp, and the corresponding
run function that applies it a given number of times.

     (defun stp (s)
       (+ 1 s))

     (defun run (s n)
       (if (zp n)
           s
           (run (stp s) (- n 1))))

The step function here is trivial:  a state is just a number and the
step function increments it.  In this example we will not be interested
in the theorems we prove but in how we prove them.  The formula we will
focus on is

     (thm (equal (run s 7) xxx))

This is not a theorem, of course.  But we want to test our advice on
non-theorems because we do not want the advice to work only for proofs
that succeed.  (In the past, we gave advice about using computed hints
and that advice caused the theorem prover to run forever when given
formulas that it couldn't prove - but most of the time the system is
presented with formulas it cannot prove!)

Furthermore, without some kind of additional rules, the (run s 7)
expression in the conjecture above will not expand at all, because
ACL2's heuristics do not approve.

In fact, we do not want to take chances that run will be expanded - we
want to control its expansion completely.  Therefore, disable run.

     (in-theory (disable run))

Now, what do we want?  (That is always a good question to ask!)  We want
(run s 7) to expand "slowly."  In particular, we want it to expand
once, to (run (stp s) 6).  Then we want the stp to be expanded and
fully simplified before the run expression is expanded again.  That is,
we want to force the expansion of run whenever the goal is stable under
simplification.  This is sometimes called "staged simplification."

We can achieve staged simplification for any given function symbol by
defining the functions shown below and then using a simple computed
hint:

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

By inspecting how stage is defined you can see how to extend it, but we
explain as we go.  To experiment, you can just paste the definitions
(and defmacro) below into your ACL2 shell and then try the thm command.

First, define this pair of mutually recursive functions.
Find-first-call finds the first call of the function symbol fn in a
given term.

     (mutual-recursion
      (defun find-first-call (fn term)
      ; Find the first call of fn in term.
       (cond ((variablep term) nil)
             ((fquotep term) nil)
             ((equal (ffn-symb term) fn)
              term)
             (t (find-first-call-lst fn (fargs term)))))
      (defun find-first-call-lst (fn lst)
      ; Find the first call of fn in a list of terms.
       (cond ((endp lst) nil)
             (t (or (find-first-call fn (car lst))
                    (find-first-call-lst fn (cdr lst)))))))

We will arrange for the computed hint to generate an :EXPAND hint for
the first call of fn, whenever the goal becomes stable under
simplification.  If no call is found, the hint will do nothing.  To
make sure the hint will not loop indefinitely (for example, by forcing
fn to expand only to have the rewriter "fold" it back up again), we
will provide the hint with a bound that stops it after some number of
iterations.  Here is the basic function that creates the expand hint
and replaces itself to count down.

     (defun stage1 (fn max clause flg)
     ; If the clause is stable under simplification and there is a call of
     ; fn in it, expand it.  But don't do it more than max times.
      (let ((temp (and flg
                       (find-first-call-lst fn clause))))
        (if temp
            (if (zp max)
                (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                     your STAGE hint been reached without eliminating ~
                     all of the calls of ~x0.  You could supply a larger ~
                     count with the optional second argument to STAGE ~
                     (which defaults to 100).  But think about what is ~
                     happening! Is each stage permanently eliminating a ~
                     call of ~x0?~%~%"
                    fn)
              `(:computed-hint-replacement
                 ((stage1 ',fn ,(- max 1)
                          clause
                          stable-under-simplificationp))
                :expand (,temp)))
          nil)))

Suppose that when stage1 is called, fn is the function we want to
expand, max is the maximum number of iterations of this expansion,
clause is the current goal clause, and flg is the value of the
stable-under-simplificationp flag.  Then if clause is stable and we can
find a call of fn in it, we ask whether max is exhausted.  If so, we
print an "error message" to the comment window with cw and return nil
(the value of cw).  That nil means the hint does nothing.  But if max
is not yet exhausted, we return a new hint.  As you can see above, the
hint replaces itself with another stage1 hint with the same fn and a
decremented max to be applied to the new clause and the then-current
value of stable-under-simplificationp.  The hint also contains an
:expand directive for the call of fn found.

Thus, if the computed hint was:

     (stage1 'run 5 clause stable-under-simplificationp)

and (run s 7) occurs in the clause, then it will generate

     (:computed-hint-replacement
       ((stage1 'run 4 clause stable-under-simplificationp))
      :expand ((run s 7)))

which will in turn replace the old stage1 hint with the new one and
will apply :expand ((run s 7)) to the current goal.

We can make this more convenient by defining the macro:

     (defmacro stage (fn &optional (max '100))
      `(stage1 ',fn ,max clause stable-under-simplificationp))

Note that the macro allows us to either provide the maximum bound or
let it default to 100.

Henceforth, we can type

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

to stage the opening of run up to 100 times, or we can write

     (thm (equal (run s 7) xxx)
          :hints ((stage run 5)))

to stage it only 5 times.  In the latter example, the system with print
a "error message" after the fifth expansion.

Note that if we executed

     (set-default-hints '((stage run)))

then we could attack all theorems (involving run) with staged
simplification (up to bound 100), without typing an explicit hint.

     (thm (equal (run s 7) xxx))

Using techniques similar to those above we have implemented "priority
phased simplification" and provided it as a book.  See
books/misc/priorities.lisp.  This is an idea suggested by Pete
Manolios, by which priorities may be assigned to rules and then the
simplifier simplifies each subgoal maximally under the rules of a given
priority before enabling the rules of the next priority level.  The
book above documents both how we implement it with computed hints and
how to use it.

Here is another example of using the stable-under-simplificationp flag
to delay certain actions.  It defines a default hint, see
DEFAULT-HINTS, which will enable non-linear-arithmetic on precisely
those goals which are stable-under-simplificationp.  It also uses the
HISTORY and PSPV variables to determine when toggling
non-linear-arithmetic is appropriate.  These variables are documented
only in the source code.  If you start using these variables
extensively, please contact the developers of ACL2 or Robert Krug
(rkrug@cs.utexas.edu) and let us know how we can help.

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

USING-COMPUTED-HINTS-8    Some Final Comments

None of the examples show the use of the variable WORLD, which is
allowed in computed hints.  There are some (undocumented) ACL2
utilities that might be useful in programming hints, but these
utilities need access to the ACL2 logical world (see WORLD).

A very useful fact to know is that (table-alist name world) returns an
alist representation of the current value of the table named name.

The ACL2 source code is littered with :program mode functions for
manipulating world.  In our source code, the world is usually bound a
variable named wrld; so searching our code for that name might be
helpful.

Using these utilities to look at the WORLD one can, for example,
determine whether a symbol is defined recursively or not, get the body
and formals of a defined function, or fetch the statement of a given
lemma.  Because these utilities are not yet documented, we do not
expect users to employ WORLD in computed hints.  But experts might and
it might lead to the formulation of a more convenient language for
computed hints.

None of our examples illustrated the 7 argument form of a computed hint,
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX).  When
used, the variables HIST, PSPV, and CTX, are bound to the clause
history, the package of "special variables" governing the clause, and
the "error message context."  These variables are commonly used
throughout our source code but are, unfortunately, undocumented.
Again, we expect a few experts will find them useful in developing
computed hints.

If you start using computed hints extensively, please contact the
developers of ACL2 and let us know what you are doing with them and how
we can help.

USING-ENABLED-RULES    avoiding :use hints for enabled :rewrite rules

Consider the following (admittedly silly) example.

     (thm (equal (append (append x y) z) (append x y z))
          :hints (("Subgoal *1/1" :use cdr-cons)))

ACL2's output includes the following warning.

     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) in the hint provided for Subgoal *1/1.

The warning is saying that if you leave the rewrite rule enabled, ACL2
may simplify away the hypothesis added by the :use hint.  We now
explain this danger in more detail and show how disabling the rule can
solve this problem.

Recall (see HINTS) how :use hints work.  Such a hint specifies a
formula, F, which is based on an existing lemma.  Then the indicated
goal, G, is replaced by the implication (implies F G).  The intention
is that the truth of F will help in the simplification of G to T
(true).  The "[Use]" warning shown above is telling us of the danger
that F may be rewritten to T, reducing the implication above to
(implies T G) -- thus, sadly, F has disappeared and is not available to
help with the simplification of G.

Consider the following tiny example.

       (defun p (x) (cons x x))
       (defthm car-p
          (equal (car (p x)) x))
       (in-theory (disable p (:type-prescription p)))
       (thm (implies (equal (p x1) (p x2))
                     (equal x1 x2))
            :hints (("Goal"
                     :use ((:instance car-p (x x1))
                           (:instance car-p (x x2))))))

The proof of the final thm form fails, because the new hypotheses are
rewritten to t using the :rewrite rule CAR-P, in the manner described
above.  The following proof log shows the new hypotheses and their
disappearance via rewriting.

       We augment the goal with the hypotheses provided by the :USE hint.
       These hypotheses can be derived from CAR-P via instantiation.  We are
       left with the following subgoal.

       Goal'
       (IMPLIES (AND (EQUAL (CAR (P X1)) X1)
                     (EQUAL (CAR (P X2)) X2))
                (IMPLIES (EQUAL (P X1) (P X2))
                         (EQUAL X1 X2))).

       By the simple :rewrite rule CAR-P we reduce the conjecture to

       Goal''
       (IMPLIES (EQUAL (P X1) (P X2))
                (EQUAL X1 X2)).

When we disable the rule CAR-P as follows, the proof succeeds.

       (thm (implies (equal (p x1) (p x2))
                     (equal x1 x2))
            :hints (("Goal"
                     :use ((:instance car-p (x x1))
                           (:instance car-p (x x2)))
                     :in-theory (disable car-p))))

In general, then, a solution is to disable the rewrite rule that you are
supplying in a :use hint.

VERSION    ACL2 Version Number

To determine the version number of your copy of ACL2, evaluate the form
(@ acl2-version).  The value will be a string.  For example,

     ACL2 !>(@ acl2-version)
     "ACL2 Version 3.4"

The part of the string after "ACL2 Version " is of the form x.y or
x.y.z, optionally followed by a succession of values in parentheses,
where x, y, and z are natural numbers.  If z is omitted then it is
implicitly 0.  We refer to X, y, and z as the "major", "minor", and
"incrl" fields, respectively.  The incrl field is used for incremental
releases.  The discussion just below assumes that incremental releases
are not employed at the user's site, i.e., the incrl fields are always
0.  We remove this assumption when we discuss incremental releases at
the end of this documenttation topic.

Books are considered certified only in the same version of ACL2 in
which the certification was done.  The certificate file records the
version number of the certifying ACL2 and include-book considers the
book uncertified if that does not match the current version number.
Thus, each time we release a new version of ACL2, previously certified
books should be recertified.

Note that there are over 150 constants in the system, most having to do
with the fact that ACL2 is coded in ACL2.  Many of these, for example
*common-lisp-specials-and-constants* and *acl2-exports*, may change
from version to version, and this can cause unsoundness.  For example,
the symbol 'set-difference-eq was added to *acl2-exports* in
Version_2.9, so we can certify a book in Version_2.8 containing the
following theorem, which is false in Version_2.9.

     (null (member 'set-difference-eq *acl2-exports*))

Therefore, we need to disallow inclusion of such a book in a Version_2.9
session, which otherwise would allow us to prove nil.  Furthermore, it
is possible that from one version of the system to another we might
change, say, the default values on some system function or otherwise
make "intentional" changes to the axioms.  It is even possible one
version of the system is discovered to be unsound and we release a new
version to correct our error.

Therefore we adopted the draconian policy that books are certified by a
given version of ACL2 and "must" be recertified to be used in other
versions.  We put "must" in quotes because in fact, ACL2 allows a book
that was certified in one ACL2 version to be included in a later
version, using include-book.  But ACL2 does not allow certify-book to
succeed when such an include-book is executed on its behalf.  Also, you
may experience undesirable behavior if you avoid recertification when
moving to a different version.  Hence we recommend that you stick to
the draconion policy of recertifying books when updating to a new ACL2
version.

The string (@ acl2-version) can contain implementation-specific
information in addition to the version number.  For example, in
Macintosh Common Lisp (MCL) (char-code #Newline) is 13, while as far as
we know, it is 10 in every other Common Lisp.  Our concern is that one
could certify a book in an MCL-based ACL2 with the theorem

     (equal (char-code #Newline) 13)

and then include this book in another Lisp and thereby prove nil.  So,
when a book is certified in an MCL-based ACL2, the book's certificate
mentions "MCL" in its version string.  Moreover, (@ acl2-version)
similarly mentions "MCL" when the ACL2 image has been built on top of
MCL.  Thus, an attempt to include a book in an MCL-based ACL2 that was
certified in a non-MCL-based ACL2, or vice-versa, will be treated like
an attempt to include an uncertified book.

_Incremental releases._

From time to time, so-called "incremental releases" of ACL2 are made
available.  These releases are thoroughly tested on at least two
platforms; "normal" releases, on the other hand, are thoroughly tested
on many more platforms (perhaps a dozen or so) and are accompanied by
updates to the ACL2 home page.  We provide incremental releases in
order to provide timely updates for ACL2 users who want them, without
imposing unnecessary burdens on either on the ACL2 implementors or on
ACL2 users who prefer to update less frequently.  The implementors
expect users to update their copies of ACL2 when normal releases are
made available, but not necessarily when incremental releases are made
available.

Incremental releases are accompanied by a bump in the incrl field of the
version field, while normal releases are accompanied by a bump in the
minor or (much less frequently) major field and zeroing out of the
incrl field.  Note that incremental releases are full-fledged releases.

WATERFALL    See HINTS-AND-THE-WATERFALL.

WHY-BRR    an explanation of why ACL2 has an explicit brr mode

Why isn't brr mode automatically disabled when there are no monitored
runes?  The reason is that the list of monitored runes is kept in a
wormhole state.

See WORMHOLE for more information on wormholes in general.  But
the fundamental property of the wormhole function is that it is a
logical no-op, a constant function that does not take state as an
argument.  When entering a wormhole, arbitrary information can be
passed in (including the external state).  That information is used to
construct a near copy of the external state and that "wormhole state"
is the one with respect to which interactions occur during breaks.  But
no information is carried by ACL2 out of a wormhole -- if that were
allowed wormholes would not be logical no-ops.  The only information
carried out of a wormhole is in the user's head.

Break-rewrite interacts with the user in a wormhole state because the
signature of the ACL2 rewrite function does not permit it to modify
state.  Hence, only wormhole interaction is possible.  (This has the
additional desirable property that the correctness of the rewriter does
not depend on what the user does during interactive breaks within it;
indeed, it is logically impossible for the user to affect the course of
rewrite.)

Now consider the list of monitored runes.  Is that kept in the external
state as a normal state global or is it kept in the wormhole state?  If
it is in the external state then it can be inspected within the
wormhole but not changed.  This is unacceptable; it is common to change
the monitored rules as the proof attempt progresses, installing
monitors when certain rules are about to be used in certain contexts.
Thus, the list of monitored runes must be kept as a wormhole variable.
Hence, its value cannot be determined outside the wormhole, where the
proof attempt is ongoing.

This raises another question: If the list of monitored runes is unknown
to the rewriter operating on the external state, how does the rewriter
know when to break?  The answer is simple: it breaks every time, for
every rune, if brr mode is enabled.  The wormhole is entered
(silently), computations are done within the wormhole state to
determine if the user wants to see the break, and if so, interactions
begin.  For unmonitored runes and runes with false break conditions,
the silent wormhole entry is followed by a silent wormhole exit and the
user perceives no break.

Thus, the penalty for running with brr mode enabled when there are no
monitored runes is high: a wormhole is entered on every application of
every rune and the user is simply unware of it.  The user who has
finally unmonitored all runes is therefore strongly advised to carry
this information out of the wormhole and to do :brr nil in the external
state when the next opportunity arises.