This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

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

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

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

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

REMOVE-BINOP    remove the association of a binary function name with a macro name

     Example:
     (remove-binop binary-append)

     General Form:
     (remove-binop binop)

See ADD-BINOP for a discussion of how to associate a macro name
with a binary function name for proof output purposes.  This form sets
binop-table to the result of deleting the association of a macro name
with the given binary function name.  If the function name has no such
association, then this form still generates an event, but the event has
no real effect.

REMOVE-DEFAULT-HINTS    remove from the default hints

     Examples:
     (remove-default-hints '((computed-hint-1 clause)
                             (computed-hint-2 clause
                                              stable-under-simplificationp)))

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
REMOVE-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (remove-default-hints lst)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.  Also see ADD-DEFAULT-HINTS.

If some elements of the given list do not belong to the existing default
hints, they will simply be ignored by this event.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

REMOVE-DEFAULT-HINTS!    remove from the default hints non-locally

Please see REMOVE-DEFAULT-HINTS, which is the same as
remove-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably
remove-default-hints is to be preferred unless you have a good reason
for wanting to export the effect of this event outside the enclosing
encapsulate or book.

REMOVE-DIVE-INTO-MACRO    removes association of proof-checker diving function with macro name

     Example:
     (remove-dive-into-macro logand)

This feature undoes the effect of add-dive-into-macro, which is used so
that the proof-checker's DV command and numeric diving commands (e.g.,
3) will dive properly into subterms.  Please see
ADD-DIVE-INTO-MACRO and especially see DIVE-INTO-MACROS-TABLE.

REMOVE-INVISIBLE-FNS    make some unary functions no longer invisible

     Examples:
     (remove-invisible-fns (binary-+ unary-- foo)

The setting above has makes unary functions unary- and foo no longer
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.

     General Form:
     (remove-invisible-fns top-fn unary-fn1 ... unary-fnk)

where top-fn is a function symbol and the unary-fni are unary function
symbols.

See ADD-INVISIBLE-FNS and also see INVISIBLE-FNS-TABLE
and see SET-INVISIBLE-FNS-TABLE.

REMOVE-MACRO-ALIAS    remove the association of a function name with a macro name

     Example:
     (remove-macro-alias append)

     General Form:
     (remove-macro-alias macro-name)

See MACRO-ALIASES-TABLE for a discussion of macro aliases; also
see ADD-MACRO-ALIAS.  This form sets macro-aliases-table to the
result of deleting the key macro-name from that table.  If the name
does not occur in the table, then this form still generates an event,
but the event has no real effect.

REMOVE-NTH-ALIAS    remove the association of one symbol with another for printing of nth/update-nth terms

     Example:
     (remove-nth-alias append)

     General Form:
     (remove-nth-alias alias-name)

See NTH-ALIASES-TABLE for further discussion; also see
ADD-NTH-ALIAS.  This form sets nth-aliases-table to the result of
deleting the key alias-name from that table.  If the name does not
occur in the table, then this form still generates an event, but the
event has no real effect.

REMOVE-UNTOUCHABLE    remove names from lists of untouchable symbols

Also see PUSH-UNTOUCHABLE.

This documentation topic is directed at those who build systems on top
of ACL2.  We first describe a means for removing restrictions related to
so-called "untouchables": functions (or macros) that cannot be called,
or state global variables that cannot be modified or unbound, without
intervention that requires an active trust tag (see DEFTTAG).
Then we describe the remove-untouchable event.

We begin by discussing untouchable state global variables
temp-touchable-vars and temp-touchable-fns, which initially have value
nil.  These can often be used in place of remove-untouchable.  When the
value is t, no variable (respectively, no function or macro) is treated
as untouchable, regardless of the set of initial untouchables or the
remove-untouchable or push-untouchable events that have been admitted.
Otherwise the value of each of these two variables is a symbol-listp,
and no member of this list is treated as an untouchable variable (in
the case of temp-touchable-vars) or as an untouchable function or macro
(in the case of temp-touchable-fns).  These two state global variables
can be set by set-temp-touchable-vars and set-temp-touchable-fns,
respectively, provided there is an active trust tag (see
DEFTTAG).  Here is an illustrative example.  This macro executes the
indicated forms in a context where there are no untouchable variables,
but requires an active trust tag when invoked.

     (defmacro with-all-touchable (&rest forms)
       `(progn!
         :state-global-bindings
         ((temp-touchable-vars t set-temp-touchable-vars))
         (progn! ,@forms)))
          An equivalent version, which however is not recommended since
          state-global-let* may have surprising behavior in raw Lisp, is as
          follows.

     (defmacro with-all-touchable (&rest forms)
       `(progn!
         (state-global-let*
          ((temp-touchable-vars t set-temp-touchable-vars))
          (progn! ,@forms))))

Finally, the value t for temp-touchable-vars removes the requirement
that built-in state globals cannot be made unbound (with
makunbound-global).

We now turn to the remove-untouchable event, in case the approach above
is for some reason not adequate.  This event is illegal by default,
since it can be used to provide access to ACL2 internal functions and
data structures that are intentionally made untouchable for the user.
If you want to call it, you must first create an active trust tag; see
DEFTTAG.

     Examples:
     (remove-untouchable my-var nil)
     (remove-untouchable set-mem t)

     General Form:
     (remove-untouchable name{s}  fn-p :doc doc-string)

where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string is an
optional documentation string not beginning with ":doc-section ...".
If name{s} is a symbol it is treated as the singleton list containing
that symbol.  The effect of this event is to remove the given symbols
from the list of "untouchable variables" in the current world if fn-p
is nil, else to remove the symbols into the list of "untouchable
functions".  This event is redundant if no symbol listed is a member of
the appropriate untouchables list (variables or functions).

RESET-PREHISTORY    reset the prehistory

     Examples:
     (reset-prehistory)     ; restart command numbering at 0
     (reset-prehistory nil) ; same as above
     (reset-prehistory t)   ; as above except also disable ubt-prehistory

     General Forms:
     (reset-prehistory)
     (reset-prehistory permanent-p)
     (reset-prehistory permanent-p doc-string)

where permanent-p is t or nil, and doc-string is an optional
documentation string not beginning with ":doc-section ...".  After
execution of this command, ACL2 will change the numbering provided by
its history utilities so that this reset-prehistory command (or the
top-level compound command containing it, which for example might be an
include-book) is assigned the number 0.  The only way to undo this
command is with command ubt-prehistory.  However, even that is
disallowed if permanent-p is t.

Note that the second argument of certify-book, which specifies the
number of commands in the certification world (i.e., since
ground-zero), is not sensitive to reset-prehistory; rather, it expects
the number of commands since ground-zero.  To see such commands, :pbt
:start.

A reset-prehistory event with value nil for permanent-p (the default)
is always skipped during certify-book and include-book (indeed,
whenever ld-skip-proofsp is t).  Otherwise one would find the history
numbering reset to 0 just by virtue of including (or certifying) a book
-- probably not what was intended.

See UBT-PREHISTORY for how to undo a reset-prehistory command
that does not have a permanent-p of t.

SET-BACKCHAIN-LIMIT    Sets the backchain-limit used by the rewriter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

This event sets the global backchain-limit used by the ACL2 rewriter.
It must be nil or a non-negative integer.  (See BACKCHAIN-LIMIT
for details.)

     :set-backchain-limit nil  ; do not impose any additional limits
     :set-backchain-limit 0    ; allow only type reasoning for relieving
                               ; hypotheses
     :set-backchain-limit 500  ; allow backchaining to a depth of no more
                               ; than 500
     (set-backchain-limit 500) ; same as above

The default limit is nil.

SET-BOGUS-DEFUN-HINTS-OK    allow unnecessary ``mutual recursion''

     General Forms:
     (set-bogus-defun-hints-ok t)
     (set-bogus-defun-hints-ok nil)
     (set-bogus-defun-hints-ok :warn)

By default, ACL2 causes an error when the keyword :hints is supplied in
an xargs declare form for a definition (see DEFUN).  This
behavior can be defeated with (set-bogus-defun-hints-ok t), or if you
still want to see a warning in such cases, (set-bogus-defun-hints-ok
:warn).

SET-BOGUS-MUTUAL-RECURSION-OK    allow unnecessary ``mutual recursion''

     Examples:
     (set-bogus-mutual-recursion-ok t)
     (set-bogus-mutual-recursion-ok nil)
     (set-bogus-mutual-recursion-ok :warn)

By default, ACL2 checks that when a "clique" of more than one function
is defined simultaneously (using mutual-recursion or defuns), then
every body calls at least one of the functions in the "clique."  Below,
we refer to definitional events that fail this check as "bogus" mutual
recursions.  The check is important because ACL2 does not store
induction schemes for functions defined with other functions in a
mutual-recursion or defuns event.  Thus, ACL2 may have difficulty
proving theorems by induction that involve such functions.  Moreover,
the check can call attention to bugs, since users generally intend that
their mutual recursions are not bogus.

Nevertheless, there are times when it is advantageous to allow bogus
mutual recursions, for example when they are generated mechanically,
even at the expense of losing stored induction schemes.  The first
example above allows bogus mutual recursion.  The second example
disallows bogus mutual recursion; this is the default.  The third
example allows bogus mutual recursion, but prints an appropriate
warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-bogus-mutual-recursion-ok flg)

where flg is either t, nil, or :warn.

SET-CASE-SPLIT-LIMITATIONS    set the case-split-limitations

     Examples:
     (set-case-split-limitations '(500 100))
     (set-case-split-limitations 'nil)
     (set-case-split-limitations '(500 nil))

The first of these prevents clausify from trying the
subsumption/replacement (see below) loop if more than 500 clauses are
involved.  It also discourages the clause simplifier from splitting
into more than 100 cases at once.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-case-split-limitations lst)

where lst is either nil (denoting a list of two nils), or a list of
length two, each element of which is either nil or a natural number.
When nil is used as an element, it is treated as positive infinity.
The default setting is (500 100).

The first number specifies the maximum number of clauses that may
participate in the "subsumption/replacement" loop.  Because of the
expensive nature of that loop (which compares every clause to every
other in a way that is quadratic in the number of literals in the
clauses), when the number of clauses exceeds about 1000, the system
tends to "go into a black hole," printing nothing and not even doing
many garbage collections (because the subsumption/replacement loop does
not create new clauses so much as it just tries to delete old ones).
The initial setting is lower than the threshold at which we see
noticeably bad performance, so you probably will not see this behavior
unless you have raised or disabled the limit.

Why raise the subsumption/replacement limit?  The
subsumption/replacement loop cleans up the set of subgoals produced by
the simplifier.  For example, if one subgoal is

     (implies (and p q r) s)            [1]

and another is

     (implies (and p (not q) r) s)      [2]

then the subsumption/replacement loop would produce the single subgoal

     (implies (and p r) s)              [3]

instead.  This cleanup process is simply skipped when the number of
subgoals exceeds the subsumption/replacement limit.  But each subgoal
must nonetheless be proved.  The proofs of [1] and [2] are likely to
duplicate much work, which is only done once in proving [3].  So with a
low limit, you may find the system quickly produces a set of subgoals
but then takes a long time to prove that set.  With a higher limit, you
may find the set of subgoals to be "cleaner" and faster to prove.

Why lower the subsumption/replacement limit?  If you see the system go
into a "black hole" of the sort described above (no output, and few
garbage collections), it could due to the subsumption/replacement loop
working on a large set of large subgoals.  You might temporarily lower
the limit so that it begins to print the uncleaned set of subgoals.
Perhaps by looking at the output you will realize that some function
can be disabled so as to prevent the case explosion.  Then raise or
disable the limit again!

The second number in the case-split-limitations specifies how many case
splits the simplifier will allow before it begins to shut down case
splitting.  In normal operation, when a literal rewrites to a nest of
IFs, the system simplifies all subsequent literals in all the contexts
generated by walking through the nest in all possible ways.  This can
also cause the system to "go into a black hole" printing nothing except
garbage collection messages.  This "black hole" behavior is different
from than mentioned above because space is typically being consumed at
a prodigious rate, since the system is rewriting the literals over and
over in many different contexts.

As the simplifier sweeps across the clause, it keeps track of the
number of cases that have been generated.  When that number exceeds the
second number in case-split-limitations, the simplifier stops rewriting
literals.  The remaining, unrewritten, literals are copied over into
the output clauses.  IFs in those literals are split out, but the
literals themselves are not rewritten.  Each output clause is then
attacked again, by subsequent simplification, and eventually the
unrewritten literals in the tail of the clause will be rewritten
because the earlier literals will stabilize and stop producing case
splits.

The default setting of 100 is fairly low.  We have seen successful
proofs in which thousands of subgoals were created by a simplification.
By setting the second number to small values, you can force the system
to case split slowly.  For example, a setting of 5 will cause it to
generate "about 5" subgoals per simplification.

You can read about how the simplifier works in the book Computer-Aided
Reasoning: An Approach (Kaufmann, Manolios, Moore).  If you think about
it, you will see that with a low case limit, the initial literals of a
goal are repeatedly simplified, because each time a subgoal is
simplified we start at the left-most subterm.  So when case splitting
prevents the later subterms from being fully split out, we revisit the
earlier terms before getting to the later ones.  This can be good.
Perhaps it takes several rounds of rewriting before the earlier terms
are in normal form and then the later terms rewrite quickly.  But it
could happen that the earlier terms are expensive to rewrite and do not
change, making the strategy of delayed case splits less efficient.  It
is up to you.

Sometimes the simplifier produces more clauses than you might expect,
even with case-split-limitations in effect.  As noted above, once the
limit has been exceeded, the simplifier does not rewrite subsequent
literals.  But IFs in those literals are split out nonetheless.
Furthermore, the enforcement of the limit is - as described above - all
or nothing: if the limit allows us to rewrite a literal then we rewrite
the literal fully, without regard for limitations, and get as many
cases as "naturally" are produced.  It quite often happens that a
single literal, when expanded, may grossly exceed the specified limits.

If the second "number" is nil and the simplifier is going to produce
more than 1000 clauses, a "helpful little message" to this effect is
printed out.  This output is printed to the system's "comment window"
not the standard proofs output.

SET-CHECKPOINT-SUMMARY-LIMIT    control printing of key checkpoints upon a proof's failure

See SET-GAG-MODE for a discussion of key checkpoints.

     Examples:

     ; (Default) When a proof fails, print all key checkpoints before
     ; induction but at most 3 key checkpoints after induction:
     (set-checkpoint-summary-limit (nil . 3))

     ; When a proof fails, print at most 3 key checkpoints before
     ; induction but all 3 key checkpoints after induction:
     (set-checkpoint-summary-limit (3 . nil))

     ; When a proof fails, print at most 3 key checkpoints before
     ; induction and at most 5 key checkpoints after induction:
     (set-checkpoint-summary-limit (3 . 5))

     ; When a proof fails, print at most 3 key checkpoints before
     ; induction and at most 3 key checkpoints after induction:
     (set-checkpoint-summary-limit (3 . 3))
     ; or equivalently,
     (set-checkpoint-summary-limit 3)

     ; When a proof fails, print all key checkpoints:
     (set-checkpoint-summary-limit (nil . nil))
     ; or equivalently,
     (set-checkpoint-summary-limit nil)

     ; When a proof fails, print no information at all about key checkpoints:
     (set-checkpoint-summary-limit t)

     General Forms:
     (set-checkpoint-summary-limit (n1 . n2))
     (set-checkpoint-summary-limit n)
     (set-checkpoint-summary-limit t)

where each of n1 and n2 is a natural number or nil.  For the second
form, n can be a natural number or nil and is treated as (n . n).  The
value t inhibits all printing of checkpoint summary information.  The
values n1 and n2 determine printing of key checkpoints generated before
the first induction and generated after the first induction,
respectively, where at most n1 or n2 (respectively) such key
checkpoints are printed unless the value is nil, in which case there is
no limitation.

The argument x for set-checkpoint-summary-limit, as described above,
may be quoted, i.e. supplied as 'x or (quote x).  Thus, you may use the
keyword form (see KEYWORD-COMMANDS) if you prefer, for example:

     :set-checkpoint-summary-limit (nil . 3)

SET-COMPILE-FNS    have each function compiled as you go along.

     Example Forms:
     (set-compile-fns t)    ; new functions compiled after DEFUN
     (set-compile-fns nil)  ; new functions not compiled after DEFUN

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

Also see COMP, because it may be more efficient in some Common
Lisps to compile many functions at once rather than to compile each one
as you go along.

     General Form:
     (set-compile-fns term)

where term is a variable-free term that evaluates to t or nil.  This
macro is equivalent to

     (table acl2-defaults-table :compile-fns term)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-compile-fns event.

Set-compile-fns may be thought of as an event that merely sets a flag
to t or nil.  The flag's effect is felt when functions are defined, as
with defun.  If the flag is t, functions are automatically compiled
after they are defined, as are their executable counterparts (see
EXECUTABLE-COUNTERPART).  Otherwise, functions are not automatically
compiled.  Exception: The flag has no effect when explicit compilation
is suppressed; see COMPILATION.

Because set-compile-fns is an event, the old value of the flag is
restored when a set-compile-fns event is undone.

Even when :set-compile-fns t has been executed, functions are not
individually compiled when processing an include-book event.  If you
wish to include a book of compiled functions, we suggest that you first
certify it with the compilation flag set (see CERTIFY-BOOK) or
else compile the book by supplying the appropriate load-compiled-file
argument to include-book.  More generally, compilation via
set-compile-fns is suppressed when the state global variable
ld-skip-proofsp has value 'include-book.

SET-DEBUGGER-ENABLE    control whether Lisp errors and breaks invoke the Lisp debugger

_Introduction._  Suppose we define foo in ::program mode to take the
car of its argument.  This can cause a raw Lisp error.  ACL2 will then
return control to its top-level loop unless you enable the Lisp
debugger, as shown below (except:  the error message can be a little
different in GCL).

       ACL2 !>(defun foo (x) (declare (xargs :mode :program)) (car x))

       Summary
       Form:  ( DEFUN FOO ...)
       Rules: NIL
       Warnings:  None
       Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
        FOO
       ACL2 !>(foo 3)
       ***********************************************
       ************ ABORTING from raw Lisp ***********
       Error:  Attempt to take the car of 3 which is not listp.
       ***********************************************

       If you didn't cause an explicit interrupt (Control-C),
       then the root cause may be call of a :program mode
       function that has the wrong guard specified, or even no
       guard specified (i.e., an implicit guard of t).
       See :DOC guards.

       To enable breaks into the debugger (also see :DOC acl2-customization):
       (SET-DEBUGGER-ENABLE T)
       ACL2 !>(SET-DEBUGGER-ENABLE T)
       <state>
       ACL2 !>(foo 3)
       Error: Attempt to take the car of 3 which is not listp.
         [condition type: TYPE-ERROR]

       Restart actions (select using :continue):
        0: Abort entirely from this (lisp) process.
       [Current process: Initial Lisp Listener]
       [1] ACL2(1): [RAW LISP]

_Details._  ACL2 usage is intended to take place inside the ACL2
read-eval-print loop (see LP).  Indeed, in most Lisp
implementations ACL2 comes up inside that loop, as evidenced by the
prompt:

     ACL2 !>

However, one can occasionally hit a raw Lisp error.  Here is the above
example again, this time for a GCL implementation, which unfortunately
gives a slightly less aesthetic report.

       ACL2 !>(foo 3)

       Error: 3 is not of type LIST.
       Fast links are on: do (si::use-fast-links nil) for debugging
       Error signalled by CAR.
       Backtrace: funcall > system:top-level > lisp:lambda-closure > lp > acl2_*1*_acl2::foo > foo > car > system:universal-error-handler > system::break-level-for-acl2 > let* > UNLESS
       ACL2 !>

Here, the user has defined foo in :program mode, with an implicit guard
of t.  The ACL2 evaluator therefore called the Lisp evaluator, which
expected nil or a consp argument to car.

By default, ACL2 will return to its top-level loop (at the same level of
LD) when there is a raw Lisp error, as though a call of ER with flag
HARD has been evaluated.  If instead you want to enter the raw Lisp
debugger in such cases, evaluate the following form.

     (set-debugger-enable t)

You can subsequently return to the default behavior with:

     (set-debugger-enable nil)

Either way, you can enter the Lisp debugger from within the ACL2 loop by
evaluating (break$).  If you want break$ disabled, then evaluate the
following, which disables entry to the Lisp debugger not only for Lisp
errors but also when executing (break$).

     (set-debugger-enable :never)

The discussion above also applies to interrupts (from Control-C) in
some, but not all, host Common Lisps.

SET-DEFAULT-BACKCHAIN-LIMIT    sets the default backchain-limit used when admitting a rule

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

This event sets the default backchain-limit used when a new rewrite or
linear rule is admitted.  It must be nil or a non-negative integer.
(See BACKCHAIN-LIMIT for details.)

     :set-default-backchain-limit nil  ; do not impose additional limits
     :set-default-backchain-limit 0    ; allow only type-reasoning for
                                       ; relieving hypotheses
     :set-default-backchain-limit 500  ; allow backchaining to a depth of
                                       ; no more than 500
     (set-default-backchain-limit 500) ; same as above

The initial default backchain-limit is nil.

SET-DEFAULT-HINTS    set the default hints

     Examples:
     (set-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))
     (set-default-hints nil)

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
SET-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (set-default-hints lst)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.

Whenever a defthm or thm command is executed, the default hints are
appended to the right of any explicitly provided :hints in the command.
The same applies to defuns as well (:hints, :guard-hints, and (for
ACL2(r)) :std-hints).  The hints are then translated and processed just
as though they had been explicitly included.

Technically, we do not put restrictions on lst, beyond that it is a
true list.  It would be legal to execute

     (set-default-hints '(("Goal" :use lemma23)))

with the effect that the given hint is added to subsequent hints
supplied explicitly.  An explicit "Goal" hint would, however, take
priority, as suggested by the mention above of "appended to the right."

Note that set-default-hints sets the default hints as specified.  To
add to or remove from the current default, see
ADD-DEFAULT-HINTS and see REMOVE-DEFAULT-HINTS.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

SET-DEFAULT-HINTS!    set the default hints non-locally

Please see SET-DEFAULT-HINTS, which is the same as
set-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably set-default-hints
is to be preferred unless you have a good reason for wanting to export
the effect of this event outside the enclosing encapsulate or book.

SET-ENFORCE-REDUNDANCY    require most events to be redundant

     General Forms:
     (set-enforce-redundancy nil)   ; do not require redundancy (default)
     (set-enforce-redundancy t)     ; most events (see below) must be redundant
     (set-enforce-redundancy :warn) ; warn for most non-redundant events

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     General Form:
     (set-enforce-redundancy flag)

where flag is nil, t, or :warn, as indicated above.  This macro is
essentially equivalent to

     (table acl2-defaults-table :enforce-redundancy flag)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-enforce-redundancy event.

Set-enforce-redundancy may be thought of as an event that merely sets a
flag as indicated above, which determines whether most events, including
defun and defthm events, are allowed to be redundant; see
REDUNDANT-EVENTS.  The exceptions are deflabel, defpkg, encapsulate,
include-book, push-untouchable, remove-untouchable, set-body, and table
events.  Any other type of non-redundant event will cause an error if
flag is t and a warning if flag is nil, _except_ in the course of
carrying out an include-book form.

Note that because table events that set the acl2-defaults-table are
implicitly local, set-enforce-redundancy events are ignored when
including books.  However, the presence of the event
(set-enforce-redundancy t) in a book guarantees that its subsequent
definitions and theorems are redundant.  This can be a useful property
to maintain in library development, as we now describe.

An example of the use of this form can be found in the distributed books
under directory books/rtl/rel4/.  The intention in that directory has
been to put all the gory details in subdirectories support/ and
arithmetic/, so that the books in subdirectory lib/ contain only the
"exported" definitions and theorems.  This approach is useful for human
readability.  Moreover, suppose we want to prove new theorems in lib/.
Typically we wish to prove the new theorems using the existing books in
lib/; however, our methodology demands that the proofs go into books in
support/.  If every theorem in lib/ is redundant, then we can _develop_
the proofs in lib/ but then when we are done, _move_ each book with
such proofs into support/ as follows.  In any such book, we first
replace include-book forms referring to books in lib/ by include-book
forms referring to corresponding books in support/ and/or arithmetic/.
Then, we add suitable in-theory events to get us back into the original
lib/ proof environment.

The default behavior of the system is as though the :enforce-redundancy
value is nil.  The current behavior can be ascertained by evaluating the
following form.

     (cdr (assoc-eq :enforce-redundancy (table-alist 'acl2-defaults-table wrld)))

SET-GAG-MODE    modify the nature of proof output

     Examples:

     :set-gag-mode t      ; enable gag-mode
     (set-gag-mode t)     ; same as above
     :set-gag-mode :goals ; same as above, but print names of goals when produced
     :set-gag-mode nil    ; disable gag-mode

     General Forms:
     (set-gag-mode val)
     :set-gag-mode val

where val is one of t, nil, or :goals.

The basic idea of gag-mode is to avoid much of the verbose output from
the theorem prover, leaving only output that is expected to be helpful.
You are strongly encouraged to put the form

     (set-gag-mode t) ; or, (set-gag-mode :goals)

in your ACL2 customization file; see ACL2-CUSTOMIZATION.
Future releases of ACL2 may install this setting as the default.
Please contact the ACL2 implementors if you have suggestions for
improving output in gag-mode.

The basic idea of gag-mode is to focus attention on so-called "key
checkpoints".  By default, a checkpoint is a goal that cannot be
simplified.  (Below we discuss how to change this default.)  A key
checkpoint is a checkpoint that is not descended from another
checkpoint.  (Technical point: "Descended" signifies that both goals
are at the top level in the same forcing round, or are in the same
proof by induction.)  Successful ACL2 users generally focus their
attention on key checkpoints; for a discussion of how to use ACL2
prover output in an effective manner, see THE-METHOD.  In
gag-mode, a key checkpoint is only displayed when ACL2 is unable to
make any further progress on that goal or some descendent of it, other
than with a proof by induction.

Evaluation of set-gag-mode t enters gag-mode, so that only key
checkpoints are printed.  Evaluation of set-gag-mode :goals also enters
gag-mode, but will additionally cause the name of a goal to be printed
as soon as it is generated (by invoking see
SET-PRINT-CLAUSE-IDS).  The :goals setting is useful for cases in
which the prover spends very little of its time generating goals to be
proved by induction, yet you want to see that it is making progress.
For finer-grained feedback about the simplifier's activity, see
DMR.

The current value of gag-mode is returned by a macro of the same name:

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

(Remark for advanced users.  The notion of "checkpoint" can be modified
by the user.  The default, as discussed above, is for a checkpoint to
be a goal that cannot be simplified.  Put differently, a checkpoint is
acted on by one of the processes in the value of the form (@
checkpoint-processors); see @.  Any or all of the
symbols eliminate-destructors-clause, fertilize-clause,
generalize-clause, or eliminate-irrelevance-clause can be removed from
this value in order that invocation of the corresponding proof process
does not cause its input goal to be labeled a checkpoint.  For example,
if you do not want destructor elimination to be treated differently
from simplification for purposes of labeling checkpoints, you can
evaluate the following form (see ASSIGN):

     (assign checkpoint-processors
             (remove 'eliminate-destructors-clause
                     (@ checkpoint-processors)))

Note that the value of (@ checkpoint-processors) also affects the proof
tree display; see PROOF-TREE-DETAILS.  End of Remark.)

An alternative to gag-mode is to use proof-trees; see
PROOF-TREE.  With proof-trees it is not so important to avoid
excessive prover output, since the proof-tree display provides
structure that makes it easy to monitor proof attempts and navigate
output for a proof that has failed or seems to be failing.  Still,
output can take time to print, so you may get better performance with
gag-mode.

The intention of gag-mode is to show you only the parts of a proof
attempt that are relevant for debugging a failure; additional output is
generally more likely to be distracting than truly helpful.  But on
occasion you may want to see the full proof output after an attempt
made with gag-mode.  If so, then see PSO and see PSO!.
Since set-gag-mode takes responsibility for the saving of output,
related utility set-saved-output is disabled when gag-mode is active.
Also note that calling set-gag-mode erases the currently saved output,
if any.

You may notice that gag-mode tends to print relatively little
information about goals pushed for proof by sub-induction - i.e., a
proof of *i.j, *i.j.k, etc.  The principle here is that sub-inductions
that do not succeed should generally be avoided, not analyzed for ways
to make them succeed.  Instead, the key checkpoint that generated the
goal pushed for this induction is more appropriate to analyze.  In
general, the "higher level" the checkpoint, the more worthy it is of
attention.  Thus, we suggest that look at the top-level checkpoints
before looking at those labeled "Key checkpoints under a top-level
induction".

SET-GUARD-CHECKING    control checking guards during execution of top-level forms

Detailed comments about the arguments of this function may be found
elsewhere: see GUARD-EVALUATION-TABLE.  Here we provide an
introduction to the use of set-guard-checking.

New users are encouraged to execute one of the following forms in order
to avoid evaluation errors due to guards:

     (set-guard-checking :none)
     (set-guard-checking nil)

The former avoids all guard-checking on user-defined functions and
should generally work fine for new users, the only drawback being
efficiency loss on compute-intensive problems.  All settings other than
:none check guards, but a value of nil allows evaluation to continue in
the logic when guards fail (avoiding the raw Lisp definition in that
case).

You may put one of the above forms in the "acl2-customization.lisp"
file in your current directory (see CBD) or your home directory;
see ACL2-CUSTOMIZATION.

Note that guards are not part of the ACL2 logic, and hence new users can
completely ignore the notion of guard (and the rest of this
documentation section after this paragraph!).  For example, (car 3) and
nil can be proved equal in the ACL2 logic, as follows, even though the
guard on car requires its first argument to be a cons pair or nil.

     (thm (equal (car 3) nil))

Moreover, unless your functions or top-level forms call built-in ACL2
functions that are defined in :program mode, the following property
will hold.

     Evaluation of (set-guard-checking :none) will allow evaluation of
     forms such as (car 3) to take place without error in the top level
     loop, not only when proving theorems.

If you feel bold, then you may wish to read the rest of this
documentation topic; also see GUARD.

See GUARD-EVALUATION-TABLE for a succinct table, with
associated discussion, that covers in detail the material presented in
the rest of the present topic.

The top-level ACL2 loop has a variable which controls which sense of
execution is provided.  To turn "guard checking on," by which we mean
that guards are checked at runtime, execute the top-level form
:set-guard-checking t.  To allow guard violations, do
:set-guard-checking nil, or do :set-guard-checking :none to turn off
all guard-checking, so that raw Lisp definitions of user-defined
functions are avoided unless their guard is t. The status of
guard-checking is reflected in the prompt.

     ACL2 !>

means guard checking is on and

     ACL2 >

means guard checking is off.  The exclamation mark can be thought of as
"barring" certain computations.  The absence of the mark suggests the
absence of error messages or unbarred access to the logical axioms.
Thus, for example

     ACL2 !>(car 'abc)

will signal an error, while

     ACL2 >(car 'abc)

will return nil.

We will return at the end of this documentation topic to discuss two
other values, :all and :nowarn, for :set-guard-checking.  We also note
that evaluation of built-in :program mode functions always takes place
in raw Lisp.

Whether guards are checked during evaluation is independent of the
default-defun-mode.  We note this simply because it is easy to confuse
":program mode" with "evaluation in Common Lisp" and thus with "guard
checking on;" and it is easy to confuse ":logic mode" with "evaluation
in the logic" and with "guard checking off."  But the
default-defun-mode determines whether newly submitted definitions
introduce programs or add logical axioms.  That mode is independent of
whether evaluation checks guards or not.  You can operate in :logic
mode with runtime guard checking on or off.  Analogously, you can
operate in :program mode with runtime guard checking on or off.

For further discussion on evaluation and guards see
GUARDS-AND-EVALUATION, in particular the exception for safe-mode in
the "Aside" there.  See GUARD for a general discussion of
guards.

Now we fulfill our promise above to discuss two other values for
:set-guard-checking:

     :set-guard-checking :nowarn
     :set-guard-checking :all

The meaning of these values is perhaps best described by the following
example provided by David Rager.

     ACL2 !>(defun my-test (expr)
              (declare (xargs :guard (true-listp expr)
                              :verify-guards nil))
              (if (atom expr)
                  expr
                (cons (my-test (car expr))
                      (my-test (cdr expr)))))

     The admission of MY-TEST is trivial, using the relation O< (which is
     known to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT EXPR).  We could deduce no constraints on the type of MY-
     TEST.  However, in normalizing the definition we used primitive type
     reasoning.

     Summary
     Form:  ( DEFUN MY-TEST ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      MY-TEST
     ACL2 !>(my-test '(a b c))

     ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
     on recursive calls of the executable counterpart (i.e., in the ACL2
     logic) of MY-TEST.  To check guards on all recursive calls:
       (set-guard-checking :all)
     To leave behavior unchanged except for inhibiting this message:
       (set-guard-checking :nowarn)

     (A B C)
     ACL2 !>

If you think about evaluation of (my-test '(a b c)), you will see that
it leads to the recursive call (my-test 'a), which one might expect to
cause a guard violation since the symbol a is not a true-listp.
However, as the warning above explains, we do not by default check
guards on recursive calls.  The reason is efficiency -- imagine a
simple definition with a guard that is slow to evaluate.  The values
:nowarn and :all for :set-guard-checking have been introduced as ways
of dealing with the above warning.  The value :nowarn simply turns off
the warning above.  The value :all causes all guards to be checked,
even on recursive calls and even on all calls of non-built-in :program
mode functions -- unless, of course, a call is made of a function whose
guard has been verified (see VERIFY-GUARDS), where the
arguments satisfy the guard, in which case the corresponding call is
made in raw Lisp without subsidiary guard-checking.  We still say that
"guard-checking is on" after :set-guard-checking is invoked with values
t, :nowarn, and :all, otherwise (after value nil) we say
"guard-checking is off.

For technical reasons, :all does not have its advertised effect in the
case of built-in :program-mode functions.  If you are interested in
this technical detail, see the comment "In the boot-strap world..." in
source function oneify-cltl-code.

We conclude with a remark about the use of :set-guard-checking for
experimenting with ACL2 as a logic or as a programming language.  If one
views ACL2 as a logic, one may wish to use :set-guard-checking :none,
while if instead one views ACL2 as a functional programming language,
one may wish to use :set-guard-checking :all.  The following transcript
illustrates this distinction by way of example.  Specifically, (car 3)
is equal to nil in the ACL2 logic, but may be viewed as a programming
error.  The default of :set-guard-checking t is problematic for learning
ACL2 using :program mode functions, since one can get raw Lisp errors.
In the example below, the raw Lisp error occurs because foo implicitly
has a guard of t, hence (foo 3) is evaluated in raw Lisp, which leads
to a raw Lisp call of c[(car 3)].

     ACL2 !>(defun foo (x)
              (declare (xargs :mode :program))
              (car x))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FOO
     ACL2 !>(foo 3)
     Error: Attempt to take the car of 3 which is not listp.
       [condition type: TYPE-ERROR]

     Restart actions (select using :continue):
      0: Abort entirely from this (lisp) process.
     [Current process: Initial Lisp Listener]
     [1] ACL2(1): [RAW LISP] :pop
     ACL2 !>:set-guard-checking :none

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

     ACL2 >(foo 3)
     NIL
     ACL2 >:set-guard-checking :all

     Turning guard checking on, value :ALL.

     ACL2 !>(foo 3)

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

     ACL2 !>