This is documentation for ACL2 Version 6.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.

INDUCTION    make a rule that suggests a certain induction

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

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

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

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

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

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

     General Form of an :induction Lemma or Corollary:
     T

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

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

The induction rule created is used as follows.  When an instance of the
:pattern term occurs in a conjecture to be proved by induction and the
corresponding instance of the :condition term is known to be non-nil
(by type reasoning alone), the corresponding instance of the :scheme
term is created and the rule "suggests" the induction, if any,
suggested by that term.  (Analysis of that term may further involve
induction rules, though the applied rule is removed from consideration
during that further analysis, in order to avoid looping.)  If rec-fn is
recursive, then the suggestion is the one that unwinds that recursion.

Consider, for example, the example given above,

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

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

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

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

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

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

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

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

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

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

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

LINEAR    make some arithmetic inequality rules

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :linear rule might be built is:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

A non-nil list of function symbols must be supplied as the value of the
:trigger-fns field in a :meta rule class object (except that a macro
alias can stand in for a function symbol; see ADD-MACRO-ALIAS).

     General Forms:
     (implies (and (pseudo-termp x)        ; this hyp is optional
                   (alistp a)              ; this hyp is optional
                   (ev (hyp-fn x ...) a)   ; this hyp is optional
                   ; meta-extract hyps may also be included (see below)
                   )
              (equiv (ev x a)
                     (ev (fn x ...) a)))

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

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

Additional hypotheses are supported, called "meta-extract hypotheses".
These allow metafunctions to depend on the validity of certain terms
extracted from the context or the logical world.  These hypotheses
provide a relatively advanced form of metatheorem so we explain them
elsewhere; see META-EXTRACT.

One might think that metafunctions and (if supplied) hypothesis
metafunctions must be executable: that is, not constrained (i.e.,
introduced in the signature of encapsulate events), and not declared
:non-executable.  After all, there is no point in installing a
simplifier that cannot be run!  However, such a restriction is not
enforced, because one could introduce a metafunction using encapsulate
and then use defattach to attach it to an executable function; see
DEFATTACH.

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

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

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

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

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

     term1 = (ev* 'term1 a)      ; (1) by construction of ev* and a
           = (ev* (fn 'term1) a) ; (2) by the metatheorem for ev*
           = (ev* 'term2 a)      ; (3) by evaluation of fn
           = term2               ; (4) by construction of ev* and a

Note that in line (2) above, where we appeal to the (functional
instantiation of the) metatheorem, we can relieve its (optional)
pseudo-termp and alistp hypotheses by appealing to the facts that term1
is a term and a is an alist by construction.  [End of Aside for the
logic-minded.]

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

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

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

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

is logically equivalent to the rule

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

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

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

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

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

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

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

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

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

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

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

     (in-theory (disable unhide))

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

     (in-theory (disable my-plus))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

In a nutshell, we require that a rule's evaluator does not support other
functions in the rule, and we require that the evaluator not be
introduced under a non-trivial encapsulate.  We also require that no
function has an attachment (see DEFATTACH) that is both
ancestral in the evaluator and also ancestral in the meta or
clause-processor functions.  We explain these restrictions in detail
below.

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

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

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

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

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

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

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

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

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

      (local (defstub c () t))

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

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

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

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

     (defun f (x)
       (not x))

     (defun g ()
       nil)

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

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

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

It follows that the current session logically yields a contradiction!

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

     (in-package "ACL2")

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

     (defun f2 (x)
        (not x))

     (defun g2 ()
        nil)

     (encapsulate
       ((f (x) t))

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

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

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

     (encapsulate
       ()

       (local (defstub c () t))

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

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

     (defun g ()
        nil)

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

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

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

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

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

Finally, we also require that no function has an attachment (see
DEFATTACH) that is both ancestral in the evaluator and also ancestral
in the meta or clause-processor functions.  (If you don't use defattach
then you can ignore this condition.)  Without this restriction, the
following events prove nil.

     (in-package "ACL2")
     (defstub f () t)
     (defevaluator evl evl-list
       ((f)))
     (defun my-meta-fn (x)
       (if (equal x '(f))
           (list 'quote (f))
         x))
     (defthm my-meta-fn-correct
       (equal (evl x a)
              (evl (my-meta-fn x) a))
       :rule-classes ((:meta :trigger-fns (f))))
     (defun constant-nil ()
       (declare (xargs :guard t))
       nil)
     (defattach f constant-nil)
     (defthm f-is-nil
     ; proved using my-meta-fn-correct
       (equal (f) nil)
       :rule-classes nil)
     (defthm contradiction
       nil
       :hints (("Goal" :use ((:functional-instance
                              f-is-nil
                              (f (lambda () t))))))
       :rule-classes nil)

To see why this restriction is sufficient, see a comment in the ACL2
source code entitled "; Essay on Correctness of Meta Reasoning."

REFINEMENT    record that one equivalence relation refines another

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :refinement rule might be built is:

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

Also see DEFREFINEMENT.

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

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

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

Suppose we have the :rewrite rule

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

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

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

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

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

REWRITE    make some :rewrite rules (possibly conditional ones)

This doc topic discusses the rule-class :rewrite.  If you want a general
discussion of how rewriting works in ACL2 and some guidance on how to
construct effective rewrite rules, see
INTRODUCTION-TO-REWRITE-RULES-PART-1 and then see
INTRODUCTION-TO-REWRITE-RULES-PART-2.

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Example :corollary
formulas from which :rewrite rules might be built are:

     Example:
     (equal (+ x y) (+ y x))            replace (+ a b) by (+ b a) provided
                                        certain heuristics approve the
                                        permutation.

     (implies (true-listp x)            replace (append a nil) by a, if
              (equal (append x nil) x)) (true-listp a) rewrites to t

     (implies                           replace (member a (append b c)) by
         (and (eqlablep e)              (member a (append c b)) in contexts
              (true-listp x)            in which propositional equivalence
              (true-listp y))           is sufficient, provided (eqlablep a)
         (iff (member e (append x y))   (true-listp b) and (true-listp c)
              (member e (append y x)))) rewrite to t and the permutative
                                        heuristics approve

     * Menu:

     Related topics other than immediate subtopics:
     * BIND-FREE:: to bind free variables of a rewrite or linear rule

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

     * DOUBLE-REWRITE:: cause a term to be rewritten twice

     * FORCE:: identity function used to force a hypothesis

     * FREE-VARIABLES:: free variables in rules

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

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

Note: One :rewrite rule class object might create many rewrite rules
from the :corollary formula.  To create the rules, we first translate
the formula, expanding all macros (see TRANS) and also
expanding away calls of all so-called "guard holders," mv-list and
return-last (the latter resulting for example from calls of prog2$,
mbe, or ec-call), as well as expansions of the macro `the'.  Next, we
eliminate all lambdas; one may think of this step as simply substituting
away every let, let*, and mv-let in the formula.  We then flatten the
AND and IMPLIES structure of the formula; for example, if the
hypothesis or conclusion is of the form (and (and term1 term2) term3),
then we replace that by the "flat" term (and term1 term2 term3).  (The
latter is actually an abbreviation for the right-associated term (and
term1 (and term2 term3)).)  The result is a conjunction of formulas,
each of the form

     (implies (and h1 ... hn) concl)

where no hypothesis is a conjunction and concl is neither a conjunction
nor an implication.  If necessary, the hypothesis of such a conjunct
may be vacuous.  We then further coerce each concl into the form (equiv
lhs rhs), where equiv is a known equivalence relation, by replacing any
concl not of that form by (iff concl t).  A concl of the form (not
term) is considered to be of the form (iff term nil).  By these steps
we reduce the given :corollary to a sequence of conjuncts, each of
which is of the form

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

where equiv is a known equivalence relation.  See EQUIVALENCE
for a general discussion of the introduction of new equivalence
relations.  At this point, we check whether lhs and rhs are the same
term; if so, we cause an error, since this rule will loop.  (But this
is just a basic check; the rule could loop in other cases, for example
if rhs is an instance of lhs; see LOOP-STOPPER.)

We create a :rewrite rule for each such conjunct, if possible, and
otherwise cause an error.  It is possible to create a rewrite rule from
such a conjunct provided lhs is not a variable, a quoted constant, a
let-expression, a lambda application, or an if-expression.

A :rewrite rule is used when any instance of the lhs occurs in a
context in which the equivalence relation is an admissible congruence
relation.  First, we find a substitution that makes lhs equal to the
target term.  Then we attempt to relieve the instantiated hypotheses of
the rule.  Hypotheses that are fully instantiated are relieved by
recursive rewriting.  Hypotheses that contain "free variables"
(variables not assigned by the unifying substitution) are relieved by
attempting to guess a suitable instance so as to make the hypothesis
equal to some known assumption in the context of the target.  If the
hypotheses are relieved, and certain restrictions that prevent some
forms of infinite regress are met (see LOOP-STOPPER), the
target is replaced by the instantiated rhs, which is then recursively
rewritten.

ACL2's rewriting process has undergone some optimization.  In
particular, when a term t1 is rewritten to a new term t2, the rewriter
is then immediately applied to t2.  On rare occasions you may find that
you do not want this behavior, in which case you may wish to use a
trick involving hide; see META, near the end of that
documentation.

In another optimization, when the hypotheses and right-hand side are
rewritten, ACL2 does not really first apply the substitution and then
rewrite; instead, it as it rewrites those terms it looks up the already
rewritten values of the bound variables.  Sometimes you may want those
bindings rewritten again, e.g., because the variables occur in slots
that admit additional equivalence relations.  See double-rewrite.

See INTRODUCTION-TO-REWRITE-RULES-PART-1 and see
INTRODUCTION-TO-REWRITE-RULES-PART-2 for an extended discussion of how
to create effective rewrite rules.

TAU-SYSTEM    make a rule for the ACL2 "type checker"

This documentation topic describes the syntactic form of "tau-system"
rules; these rules extend ACL2's "type checker."  For an introduction to
the tau system, see INTRODUCTION-TO-THE-TAU-SYSTEM.

There happens to be a function named tau-system, defined as the
identity function.  Its only role is to provide the rune
(:EXECUTABLE-COUNTERPART TAU-SYSTEM), which is used to enable and
disable the tau system.  Otherwise the function tau-system has no
purpose and we recommend that you avoid using it so you are free to
enable and disable the tau system.

When in the default ("greedy") mode (see set-tau-auto-mode), every
defun and every :corollary (see :rule-classes) of every defthm stored
as a rule of any :rule-class is inspected to determine if it is of one
of the forms below.  Rules of these forms are added to the tau
database, even if they are not labeled as :tau-system rules, e.g., a
:rewrite rule might contribute to the tau database!  To add a rule to
the tau database without adding any other kind of rule, tag it with
:rule-classes :tau-system.  If a theorem has :rule-classes nil, it is
not considered for the tau database.

     General Forms:
     Boolean:
     (booleanp (p v))

     Eval:
     (p 'const) or
     (p *const*)

     Simple:
     (implies (p v) (q v))

     Conjunctive:
     (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.

     Signature Form 1:
     (implies (and (p1 x1) (p2 x2) ...)
              (q (fn x1 x2 ...)))

     Signature Form 2:
     (implies (and (p1 x1) (p2 x2) ...)
              (q (mv-nth 'n (fn x1 x2 ...))))

     Big Switch:
     (equal (fn . formals) body)

     MV-NTH Synonym:
     (equal (nth-alt x y) (mv-nth x y)) or
     (equal (mv-nth x y) (nth-alt x y))

The symbols p, q, p1, etc., denote monadic (one-argument)
Boolean-valued function symbols, or equalities in which one argument is
constant, arithmetic comparisons in which one argument is a rational or
integer constant, or the logical negations of such terms.  By
"equalities" we allow EQUAL, EQ, EQL, and =.  By "arithmetic
comparison" we mean <, <=, >=, or >.  Any of these tau predicates may
appear negated.

The notation (p v) above might stand for any one of:

     (INTEGERP X)
     (EQUAL V 'MONDAY)
     (<= I 16)
     (NOT (EQUAL X 'SUNDAY))

The different rule forms above affect different aspects of the tau
system.  We discuss each form in more detail below.

The documentation below is written as though the tau system is in auto
mode!  To insure that the only rules added to the tau system are those
explicitly assigned to :rule-class :tau-system, you should use
set-tau-auto-mode to select manual mode.

     General Form: Boolean:
     (booleanp (p v))

Here p must be a function symbol and v must be a variable.  Such a
:tau-system rule adds p to the list of tau predicates.  If p was
recognized as Boolean when it was defined, there is no need to state
this rule.  This form is needed if you define a monadic Boolean
function in such a way that the system does not recognize that it is
Boolean.

     General Form: Eval:
     (p 'const) or
     (p *const*)

Here p must be a function symbol.  In addition, recall that these
general tau predicate forms may appear negated.  So the form above
includes such theorems as (NOT (GOOD-STATEP *INITIAL-STATE*)).  A
theorem of this form thus records whether a named predicate is true or
false on the given constant.

Generally, when the tau system must determine whether an enabled tau
predicate is true or false on a constant, it simply evaluates the
predicate on the constant.  This can be impossible or very inefficient
if p is not defined but constrained, or if p is defined in a
hard-to-compute way (e.g., (defun p (x) (evenp (ack x x))) where ack is
the Ackermann function), or perhaps if the constant is very large.  By
proving a :tau-system rule of Eval form, you cause the tau system to
note the value of the predicate on the constant and henceforth to look
it up instead of evaluating the definition.

A difficulty, however, is determining that a slow down is due to the
evaluation of tau predicates and not some other reason.  The first step
is determining that tau is slowing the proof down.  See time-tracker-tau
for an explanation of TIME-TRACKER-NOTEs output during some proofs
involving tau reasoning.  These notes can alert you to the fact that
significant amounts of time are being spent in the tau system.
Time-tracker-tau gives some ways of determining whether tau predicate
evaluation is involved.  (If worse comes to worst, consider the
following hack: In the ACL2 source file tau.lisp, immediately after the
definition of the system function ev-fncall-w-tau-recog, there is a
comment which contains some raw Lisp code that can be used to
investigate whether tau's use of evaluation on constants is causing a
problem.)  However, once a recognizer and the constants on which it is
being evaluated are identified, the tau system can be sped up by
proving Eval rules to pre-compute and store the values of the
recognizer on those constants.  Alternatively, at the possible loss of
some completeness in the tau system, the executable counterpart of the
recognizer can be disabled.

     General Form: Simple:
     (implies (p v) (q v))

Here v must be a variable symbol.  This rule builds-in the information
that anything satisfying p must also satisfy q, i.e., the "type" q
includes the "type" p.  Recall that the forms may be negated.  Most of
the time, p and q will be predicate symbols but it is possible they
will be equalities- or inequalities-with-constants.  Examples of Simple
rules include the following, which are in fact built-in:

     (implies (natp x) (integerp x))
     (implies (integerp x) (rationalp x))
     (implies (integerp x) (not (true-listp x)))
     (implies (natp x) (not (< x 0)))
     (implies (symbol-alistp x) (alistp x))

Because the tau system records the transitive closure of the Simple
rules, any time a term is known to satisfy natp it is also known to
satisfy integerp and rationalp, and known not to satisfy true-listp,
and known to be non-negative.

     General Form: Conjunctive:
     (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.

The pi and q may be any tau predicates or their negations, v must be a
variable symbol, and i must exceed 1 or else this is a Simple rule.  An
obvious operational interpretation of this rule is that if an object is
known to satisfy all of the pi, then it is known to satisfy q.
However, the actual interpretation is more general.  For example, if an
object is known to satisfy all but one of the pi and is known not to
satisfy q, then the object is known not to satisfy the "missing" pi.

For example, the following Conjunctive rule allows tau to conclude that
if weekday D is not MON, TUE, THU or FRI, then it is WED:

     (implies (and (weekdayp d)
                   (not (eq d 'MON))
                   (not (eq d 'TUE))
                   (not (eq d 'WED))
                   (not (eq d 'THU)))
              (eq d 'FRI))

The tau database is not closed under conjunctive rules; they are
applied dynamically.

     General Form: Signature Form 1:
     (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp)
              (q (fn x1 x2 ... xn)))

The pi and q may be any tau predicates or their negations, fn must be a
function symbol of arity n, the xi must be distinct variable symbols
and dep-hyp may be any term, provided it is not of the (pi xi) shape
and the only the variables in it are the xi.

The Signature form actually allows multiple tau predicates to be
applied to each variable, e.g., x1 might be required to be both an
INTEGERP and EVENP.  The Signature form allows there to be multiple
hypotheses classified as dep-hyps, i.e., not fitting any of the
previous shapes, and they are implicitly just conjoined.  The name
"dep-hyp" is an abbreviation of "dependent hypothesis" and stems from
the fact they often express relations between several of the function's
inputs rather than type-like constraints on individual inputs.

A Signature rule informs tau that the function fn returns an object
satisfying q provided that the arguments satisfy the respective pi and
provided that dep-hyp occurs in the current context.  Note: to be
precise, dependent hypotheses are relieved only by applying ACL2's most
primitive form of reasoning, type-set.  In particular, tau reasoning is
not used to establish dependent hypotheses.  The presence of a dep-hyp
in a signature rule may severely restrict its applicability.  We
discuss this after showing a few mundane examples.

An example Signature rule is

     (implies (and (integer-listp x)
                   (integer-listp y))
              (integer-listp (append x y)))

Of course, a function may have multiple signatures:

     (implies (and (symbol-listp x)
                   (symbol-listp y))
              (symbol-listp (append x y)))

Here is a Signature rule for the function pairlis$:

     (implies (and (symbol-listp x)
                   (integer-listp y))
              (symbol-alistp (pairlis$ x y)))

The tau system can consequently check this theorem by composing the
last two rules shown and exploiting Simple rule stating that
symbol-alists are also alists:

     (thm (implies (and (symbol-listp a)
                        (symbol-listp b)
                        (integer-listp y))
                   (alistp (pairlis$ (append a b) y))))

Since a and b are known to be lists of symbols and a signature for
append is that it preserves that predicate, the first argument to the
pairlis$ expression is known to be a list of symbols.  This means the
Signature rule for pairlis$ tells us the result is a symbol-alistp, but
the previously mentioned Simple rule, (implies (symbol-alistp x)
(alistp x)), tells us the result is also an alistp.

When a Signature rule has an dep-hyp, that hypothesis is not an
expression in the tau system.  Tau is not used to check that
hypothesis.  Instead, tau uses the more primitive type-set mechanism of
ACL2.  Here is an example of a Signature rule with a dep-hyp:

     (implies (and (natp n)
                   (integer-listp a)
                   (< n (len a)))
              (integerp (nth n a)))

Note that the last hypothesis is a dependent hypothesis: it is not a tau
predicate but a relationship between n and a.  It is relieved by
type-set.  If one is trying to compute the signature of an (nth n a)
expression in a context in which (< n (len a)) is explicitly assumed,
then this mechanism would establish the dependent hypothesis.  But one
can easily imagine an almost identical context where, say (< n (len
(rev a))) is explicitly assumed.  In that context, the Signature rule
would not be fired because type-set cannot establish (< n (len a)) from
(< n (len (rev a))), even though it would be easily proved by rewriting
using the theorem (equal (len (rev a)) (len a)).

Note also that if this signature could be phrased in a way that
eliminates the dependency between n and a it would be more effective.
For example, here is a related Signature rule without a dependent
hypothesis:

     (implies (and (natp n)
                   (register-filep a)
                   (< n 16))
              (integerp (nth n a)))

In this theorem we require only that n be less than 16, which is a tau
predicate and hence just an additional tau constraint on n.

     General Form: Signature Form 2:
     (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp)

              (q (mv-nth 'n (fn x1 x2 ... xn))))

This form of signature rule is just like form 1 except that it is
useful for functions that return multiple-values and allows us to
"type-check" their individual outputs.

     General Form: Big Switch:
     (equal (fn . formals) body)

In the Big Switch form, fn must be a function symbol, formals must be a
list of distinct variable symbols, and body must be a "big switch"
term, i.e., one that case splits on tau predicates about a single
variable and produces a term not involving that variable.  An example
of a Big Switch rule is

     (equal (conditional-type x y)
            (if (consp x)
                (consp y)
                (integerp y)))

The idea is that the tau system can treat calls of conditional-type as
a tau-predicate after determining the tau of an argument.

Since equality-to-constants are tau predicates, a more common example
of a Big Switch rule is

     (equal (dtypep x expr)
            (case x
                  (STMT (stmt-typep expr))
                  (EXPR (expr-typep expr))
                  (MODULE (module-typep expr))
                  (otherwise nil)))

This is because (case x (STMT ...) ...) macroexpands in ACL2 to (if
(eql x 'STMT) ... ...) and (eql x 'STMT) is a tau predicate about x.

Big Switch rules are recognized when a function is defined (if tau is in
automatic mode).  They generally do not have to be proved explicitly,
though they might be when mutual recursion is involved.  Only the first
detected Big Switch rule about a function fn is recognized.

     General Form: MV-NTH Synonym:
     (equal (nth-alt x y) (mv-nth x y)) or
     (equal (mv-nth x y) (nth-alt x y))

Rules of this form just tell the tau system that the user-defined
function nth-alt is synonymous with the ACL2 primitive function mv-nth.
Because ACL2's rewriter gives special handling to mv-nth, users
sometimes define their own versions of that function so they can
disable them and control rewriting better.  By revealing to the tau
system that such a synonym has been introduced you allow Signature
rules of Form 2 to be used.

TYPE-PRESCRIPTION    make a rule that specifies the type of a term

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Some example :corollary
formulas from which :type-prescription rules might be built are:

     Examples:
     (implies                           (nth n lst) is of type characterp
      (and (character-listp lst)        provided the two hypotheses can
           (< n (length lst)))          be established by type reasoning
      (characterp (nth n lst))).

     (implies                           (demodulize a lst 'value ans) is
      (and (atom a)                     either a nonnegative integer or
           (true-listp lst)             of the same type as ans, provided
           (member-equal a lst))        the hyps can be established by type
      (or (and                          reasoning
            (integerp
             (demodulize a lst 'value ans))
            (>= (demodulize a lst 'value ans) 0))
          (equal (demodulize a lst 'value ans) ans))).

To specify the term whose type (see TYPE-SET) is described by
the rule, provide that term as the value of the :typed-term field of
the rule class object.

     General Form (after preprocessing; see below):
     (implies hyps
              (or type-restriction1-on-pat
                  ...
                  type-restrictionk-on-pat
                  (equal pat var1)
                  ...
                  (equal pat varj)))

where pat is the application of some function symbol to some arguments,
each type-restrictioni-on-pat is a term involving pat and containing no
variables outside of the occurrences of pat, and each vari is one of
the variables of pat.  Generally speaking, the type-restriction terms
ought to be terms that inform us as to the type of pat.  Ideally, they
should be "primitive recognizing expressions" about pat; see
COMPOUND-RECOGNIZER.  We describe preprocessing at the end of this
topic.

If the :typed-term is not provided in the rule class object, it is
computed heuristically by looking for a term in the conclusion whose
type is being restricted.  An error is caused if no such term is found.

Roughly speaking, the effect of adding such a rule is to inform the ACL2
typing mechanism that pat has the type described by the conclusion, when
the hypotheses are true.  In particular, the type of pat is within the
union of the types described by the several disjuncts.  The "type
described by" (equal pat vari) is the type of vari.

More operationally, when asked to determine the type of a term that is
an instance of pat, ACL2 will first attempt to establish the hypotheses.
*This is done by type reasoning alone, not rewriting!*  However, if some
hypothesis is a call of force, then forcing may occur, which may
ultimately invoke the rewriter; see FORCE and see
CASE-SPLIT.  So-called free variables in hypotheses are treated
specially; see FREE-VARIABLES.  Provided the hypotheses are
established by type reasoning, ACL2 then unions the types described by
the type-restrictioni-on-pat terms together with the types of those
subexpressions of pat identified by the vari.  The final type computed
for a term is the intersection of the types implied by each applicable
rule.  Type prescription rules may be disabled.

You can limit the recursive establishment of hypotheses of rules; see
SET-BACKCHAIN-LIMIT.

Because only type reasoning is used to establish the hypotheses of
:type-prescription rules, some care must be taken with the hypotheses.
Suppose, for example, that the non-recursive function my-statep is
defined as

       (defun my-statep (x)
         (and (true-listp x)
              (equal (length x) 2)))

and suppose (my-statep s) occurs as a hypothesis of a
:type-prescription rule that is being considered for use in the proof
attempt for a conjecture with the hypothesis (my-statep s).  Since the
hypothesis in the conjecture is rewritten, it will become the
conjunction of (true-listp s) and (equal (length s) 2).  Those two
terms will be assumed to have type t in the context in which the
:type-prescription rule is tried.  But type reasoning will be unable to
deduce that (my-statep s) has type t in this context.  Thus, either
my-statep should be disabled (see DISABLE) during the proof
attempt or else the occurrence of (my-statep s) in the
:type-prescription rule should be replaced by the conjunction into
which it rewrites.

While this example makes it clear how non-recursive predicates can cause
problems, non-recursive functions in general can cause problems.  For
example, if (mitigate x) is defined to be (if (rationalp x) (1- x) x)
then the hypothesis (pred (mitigate s)) in the conjecture will rewrite,
opening mitigate and splitting the conjecture into two subgoals, one in
which (rationalp s) and (pred (1- x)) are assumed and the other in
which (not (rationalp s)) and (pred x) are assumed.  But (pred
(mitigate s)) will not be typed as t in either of these contexts.  The
moral is: beware of non-recursive functions occuring in the hypotheses
of :type-prescription rules.

Because of the freedom one has in forming the conclusion of a
type-prescription, we have to use heuristics to recover the pattern,
pat, whose type is being specified.  In some cases our heuristics may
not identify the intended term and the :type-prescription rule will be
rejected as illegal because the conclusion is not of the correct form.
When this happens you may wish to specify the pat directly.  This may
be done by using a suitable rule class token.  In particular, when the
token :type-prescription is used it means ACL2 is to compute pat with
its heuristics; otherwise the token should be of the form
(:type-prescription :typed-term pat), where pat is the term whose type
is being specified.

The defun event may generate a :type-prescription rule.  Suppose fn is
the name of the function concerned.  Then (:type-prescription fn) is
the rune given to the type-prescription, if any, generated for fn by
defun.  (The trivial rule, saying fn has unknown type, is not stored,
but defun still allocates the rune and the corollary of this rune is
known to be t.)

We close with a discussion of how, before a term is parsed into a
:type-prescription rule, it is preprocessed.  We describe this
preprocessing in some detail below, but first consider the following
(contrived) example.

     (defthm append-tp-example
       (let ((result (append x y)))
         (implies (nat-listp x)
                  (implies (let ((second-hyp (integer-listp y)))
                             second-hyp)
                           (true-listp result))))
       :rule-classes :type-prescription)

This theorem is parsed into a type-prescription rule with the following
hypotheses and conclusion.

     (nat-listp x) ; first hypothesis
     ((lambda (second-hyp) second-hyp) (integer-listp y)) ; second hypothesis
     (true-listp (binary-append x y)) ; conclusion

Notice that the top-level LET was expanded, i.e., (append x y) was
substituted for result -- more accurately, (binary-append x y) was
substituted for result, since append is a macro that abbreviates
binary-append.  Also notice that the two hypotheses were "flattened" in
the sense that they were gathered up into a list.  Finally, notice that
the LET in the second hypothesis was not expanded (it was merely
translated to internal form, using LAMBDA).  If you actually submit the
theorem above, you will get warnings, which you may choose to ignore;
the application of type-prescription rules is somewhat subtle, so if
you use them then you may wish to experiment to see which forms work
best for you.

Here is the detail promised above, for parsing a term into a
:type-prescription rule.  There are two steps.  (1) ACL2 first
translates the term, expanding all macros (see TRANS) and also
expanding away calls of all so-called "guard holders," mv-list and
return-last (the latter resulting for example from calls of prog2$,
mbe, or ec-call), as well as expansions of the macro `the'.  (2) Then
the the translated term is traversed top-down, expanding away lambdas
(let, let*, and mv-let expressions) and flattening the IMPLIES
structure, until the conclusion is exposed; then the conclusion's
lambdas are also expanded away.  The simplest way to understand (2) may
be to look at the definition of ACL2 source function unprettyify-tp,
which implements Step (2), say by evaluating :pe unprettyify-tp.

TYPE-SET-INVERTER    exhibit a new decoding for an ACL2 type-set

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.

     Example Rule Class:
     (:type-set-inverter
       :corollary (equal (and (counting-number x) (not (equal x 0)))
                         (and (integerp x) (< x 0)))
       :type-set 2)

     General Forms of Rule Class:
     :type-set-inverter, or
     (:type-set-inverter :type-set n)

     General Form of Theorem or Corollary:
     (EQUAL new-expr old-expr)

where n is a type-set (see TYPE-SET) and old-expr is the term
containing x as a free variable that ACL2 currently uses to recognize
type-set n.  For a given n, the exact form of old-expr is generated by

     (convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the :type-set field of the rule-class is omitted, we attempt to
compute it from the right-hand side, old-expr, of the corollary.  That
computation is done by type-set-implied-by-term (see TYPE-SET).
However, it is possible that the type-set we compute from lhs does not
have the required property that when inverted with
convert-type-set-to-term the result is lhs.  If you omit :type-set and
an error is caused because lhs has the incorrect form, you should
manually specify both :type-set and the lhs generated by
convert-type-set-to-term.

The rule generated will henceforth make new-expr be the term used by
ACL2 to recognize type-set n.  If this rule is created by a defthm
event named name then the rune of the rule is (:type-set-inverter name)
and by disabling that rune you can prevent its being used to decode
type-sets.

Type-sets are inverted when forced assumptions are turned into formulas
to be proved.  In their internal form, assumptions are essentially
pairs consisting of a context and a goal term, which was forced.
Abstractly a context is just a list of hypotheses which may be assumed
while proving the goal term.  But actually contexts are alists which
pair terms with type-sets, encoding the current hypotheses.  For
example, if the original conjecture contained the hypothesis (integerp
x) then the context used while working on that conjecture will include
the assignment to x of the type-set *ts-integer*.

WELL-FOUNDED-RELATION    show that a relation is well-founded on a set

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :well-founded-relation rule might be built is as
follows.  (Of course, the functions pairp, lex2p, and ordinate would
have to be defined first.)

     Example:
     (and (implies (pairp x) (o-p (ordinate x)))
          (implies (and (pairp x)
                        (pairp y)
                        (lex2p x y))
                   (o< (ordinate x) (ordinate y))))

The above example establishes that lex2p is a well-founded relation on
pairps.  We explain and give details below.

Exactly two general forms are recognized:

     General Forms
     (AND (IMPLIES (mp x) (O-P (fn x)))              ; Property 1
          (IMPLIES (AND (mp x)                       ; Property 2
                        (mp y)
                        (rel x y))
                   (O< (fn x) (fn y)))),

or

     (AND (O-P (fn x))                               ; Property 1
          (IMPLIES (rel x y)                         ; Property 2
                   (O< (fn x) (fn y))))

where mp, fn, and rel are function symbols, x and y are distinct
variable symbols, and no other :well-founded-relation theorem about fn
has been proved.  When the second general form is used, we act as
though the first form were used with mp being the function that ignores
its argument and returns t.  The discussion below therefore considers
only the first general form.

Note: We are very rigid when checking that the submitted formula is of
one of these forms.  For example, in the first form, we insist that all
the conjuncts appear in the order shown above.  Thus, interchanging the
two properties in the top-level conjunct or rearranging the hyptheses
in the second conjunct both produce unrecognized forms.  The
requirement that each fn be proved well-founded at most once ensures
that for each well-founded relation, fn, there is a unique mp that
recognizes the domain on which rel is well-founded.  We impose this
requirement simply so that rel can be used as a short-hand when
specifying the well-founded relations to be used in definitions;
otherwise the specification would have to indicate which mp was to be
used.

We also insist that the new ordering be embedded into the ordinals as
handled by o-p and o< and not some into previously admitted user-defined
well-founded set and relation.  This restriction should pose no
hardship.  If mp and rel were previously shown to be well-founded via
the embedding fn, and you know how to embed some new set and relation
into mp and rel, then by composing fn with your new embedding and using
the previously proved well-founded relation lemma you can embed the new
set and relation into the ordinals.

Mp is a predicate that recognizes the objects that are supposedly
ordered in a well-founded way by rel.  We call such an object an
"mp-measure" or simply a "measure" when mp is understood.  Property 1
tells us that every measure can be mapped into an ACL2 ordinal.  (See
O-P.)  This mapping is performed by fn.  Property 2 tells us
that if the measure x is smaller than the measure y according to rel
then the image of x under fn is a smaller than that of y, according to
the well-founded relation o<.  (See O<.)  Thus, the general
form of a :well-founded-relation formula establishes that there exists a
rel-order preserving embedding (namely via fn) of the mp-measures into
the ordinals.  We can thus conclude that rel is well-founded on
mp-measures.

Such well-founded relations are used in the admissibility test for
recursive functions, in particular, to show that the recursion
terminates.  To illustrate how such information may be used, consider a
generic function definition

     (defun g (x) (if (test x) (g (step x)) (base x))).

If rel has been shown to be well-founded on mp-measures, then g's
termination can be ensured by finding a measure, (m x), with the
property that m produces a measure:

     (mp (m x)),                                     ; Defun-goal-1

and that the argument to g gets smaller (when measured by m and
compared by rel) in the recursion,

     (implies (test x) (rel (m (step x)) (m x))).    ; Defun-goal-2

If rel is selected as the :well-founded-relation to be used in the
definition of g, the definitional principal will generate and attempt
to prove defun-goal-1 and defun-goal-2 to justify g.  We show later why
these two goals are sufficient to establish the termination of g.
Observe that neither the ordinals nor the embedding, fn, of the
mp-measures into the ordinals is involved in the goals generated by the
definitional principal.

Suppose now that a :well-founded-relation theorem has been proved for
mp and rel.  How can rel be "selected as the :well-founded-relation" by
defun?  There are two ways.  First, an xargs keyword to the defun event
allows the specification of a :well-founded-relation.  Thus, the
definition of g above might be written

     (defun g (x)
      (declare (xargs :well-founded-relation (mp . rel)))
      (if (test x) (g (step x)) (base x)))

Alternatively, rel may be specified as the
:default-well-founded-relation in acl2-defaults-table by executing the
event

     (set-well-founded-relation rel).

When a defun event does not explicitly specify the relation in its
xargs the default relation is used.  When ACL2 is initialized, the
default relation is o<.

Finally, though it is probably obvious, we now show that defun-goal-1
and defun-goal-2 are sufficient to ensure the termination of g provided
property-1 and property-2 of mp and rel have been proved.  To this end,
assume we have proved defun-goal-1 and defun-goal-2 as well as
property-1 and property-2 and we show how to admit g under the
primitive ACL2 definitional principal (i.e., using only the ordinals).
In particular, consider the definition event

     (defun g (x)
      (declare (xargs :well-founded-relation o<
                      :measure (fn (m x))))
      (if (test x) (g (step x)) (base x)))

Proof that g is admissible:  To admit the definition of g above we must
prove

     (o-p (fn (m x)))                        ; *1

and

     (implies (test x)                               ; *2
              (o< (fn (m (step x))) (fn (m x)))).

But *1 can be proved by instantiating property-1 to get

     (implies (mp (m x)) (o-p (fn (m x)))),

and then relieving the hypothesis with defun-goal-1, (mp (m x)).

Similarly, *2 can be proved by instantiating property-2 to get

     (implies (and (mp (m (step x)))
                   (mp (m x))
                   (rel (m (step x)) (m x)))
              (o< (fn (m (step x))) (fn (m x))))

and relieving the first two hypotheses by appealing to two instances of
defun-goal-1, thus obtaining

     (implies (rel (m (step x)) (m x))
              (o< (fn (m (step x))) (fn (m x)))).

By chaining this together with defun-goal-2,

     (implies (test x)
              (rel (m (step x)) (m x)))

we obtain *2.  Q.E.D.

SERIALIZE    routines for saving ACL2 objects to files, and later restoring them

This documentation topic relates to an experimental extension of ACL2
that supports hons, memoization, and fast alists.  See
HONS-AND-MEMOIZATION.  Thanks to Jared Davis for contributing the
"serialization" routines for saving ACL2 objects in files for later
loading.

We implement some routines for writing arbitrary ACL2 objects to files,
and for loading those files later.  We usually call these ".sao" files,
which stands for (S)erialized (A)CL2 (O)bject.

Our serialization scheme uses a compact, binary format that preserves
structure sharing in the original object.  We optimize for read
performance.

SERIALIZE-ALTERNATIVES    alternatives to the serialize routines

Hons users could previously use the routines compact-print-file and
compact-read-file.  These are deprecated and are no longer built into
ACL2.  However, they are still available by loading the new community
book, serialize/compact-print.  Note that loading this book requires a
ttag, and these routines are still only available in raw lisp.

Another predecessor of the serialization routines were hons archives,
which are still available in the hons-archive library.  The
serialization routines are generally better and we recommend against
using hons archives for new projects.

SERIALIZE-IN-BOOKS    using serialization efficiently in books

Our serialize scheme was developed in order to allow very large ACL2
objects to be loaded into books.  Ordinarily this is carried out using
serialize-read within a make-event, e.g.,

       (make-event (mv-let (obj state)
                           (serialize-read "my-file")
                           (value `(defconst *my-file* ',obj))))

But this scheme is not particularly efficient.

During certify-book, the actual call of serialize-read is carried out,
and this is typically pretty fast.  But then a number of possibly
inefficient things occur.

     - The ACL2 function bad-lisp-object is run on the resulting
     object.  This is memoized for efficiency, but may still take
     considerable time when the file is very large.

     - The checksum of the resulting object is computed.  This is also
     memoized, but as before may still take some time.

     - The object that was just read is then written into book.cert,
     essentially with serialize-write.  This can take some time, and
     results in large certifiate files.

Then, during include-book, the make-event expansion of is loaded.  This
is now basically just a serialize-read.

The moral of the story is that using serialize will only help your
certify-book time, and it only impacts a portion of the overall time.

To avoid this overhead, we have developed an UNSOUND alternative to
serialize-read, which is available only by loading an additional book.
So, if the above scheme is not performing well for you, you may wish to
see the community book serialize/unsound-read.

SERIALIZE-READ    read a serialized ACL2 object from a file

General form:

      (serialize-read filename
                      [:hons-mode {:always, :never, :smart}]   ; :smart by default
                      [:verbosep  {t, nil}])                   ; nil by default
       -->
      (mv obj state)

In the logic this is an oracle read.

Under the hood, we try to read and return a serialized object form a
file that was presumably created by serialize-write.  On success we
return the contents of the file.  Any failures (e.g., file not found,
bad file contents, etc.) will result in a hard Lisp error.

The filename should be a string that gives the path to the file.

The hons-mode controls how whether to use hons or cons to restore the
object.  The default mode is :smart, which means that conses that were
normed at the time of the file's creation should be restored with hons.
But you can override this and insist that hons is to :always or :never
be used, instead.

Why would you use :never?  If your object previously had a lot of
honses, but you no longer have any need for them to be normed, then
using :never may sometimes be a lot faster since it can avoid hons
calls.  On the other hand, if you are going to hons-copy some part of
the file's contents, then it is likely faster to use :smart or :always
instead of first creating normal conses and then copying them to build
honses.

The :verbosep flag just controls whether to print some low-level details
related to timing and memory usage as the file is being read.

SERIALIZE-WRITE    write an ACL2 object into a file

General form:

      (serialize-write filename obj
                       [:verbosep  {t, nil}])    ; nil by default
       -->
      state

In the logic this carries out an oracle read.

Under the hood, we try to save obj into the file indicated by filename,
which must be a string.  The object can later be recovered with
serialize-read.  We just return state, and any failures (e.g., file not
openable) will result in a hard Lisp error.

Writing objects to disk is generally slower than reading them back in
since some analysis is required to convert an object into our
serialized object format.

The verbosep flag just says whether to print some low-level details
related to timing and memory usage as the file is being read.

SET-SERIALIZE-CHARACTER    See WITH-SERIALIZE-CHARACTER.

WITH-SERIALIZE-CHARACTER    control output mode for print-object$

This documentation topic relates to an experimental extension of ACL2
that supports hons, memoization, and fast alists.  See
HONS-AND-MEMOIZATION.  See SERIALIZE for a discussion of
"serialization" routines, contributed by Jared Davis for saving ACL2
objects in files for later loading.

The expression (with-serialize-character char form) evaluates to the
value of form, but with the serialize-character of the state assigned to
char, which should be one of nil, #\Y, or #\Z.  We describe the effect
of that assignment below.  But note that if you are doing this because
of one or more specific calls of print-object$, such as (print-object$
x channel state), then you may wish instead to evaluate
(print-object$-ser x serialize-character channel state), in which case
you will not need to use with-serialize-character.  (Note however that
serialize-character is treated as nil for other than a HONS version.)

     General forms:
     (with-serialize-character nil form)
     (with-serialize-character #Y form)
     (with-serialize-character #Z form)

where form should evaluate to an error triple (see
ERROR-TRIPLES).

Note that if you prefer to obtain the same behavior (as described below)
globally, rather than only within the scope of with-serialize-character,
then use set-serialize-character in a corresponding manner:

     (set-serialize-character nil state)
     (set-serialize-character #Y state)
     (set-serialize-character #Z state)

In each case above, calls of print-object$ (see IO) in form will
produce an object that can be read by the HONS version of ACL2.  In the
first case, that object is printed as one might expect at the terminal,
as an ordinary Lisp s-expression.  But in the other cases, the object
is printed by first laying down either #Y or #Z (as indicated) and then
calling serialize-write (or more precisely, the underlying function
called by serialize-write that prints to a stream).

Consider what happens when the ACL2 reader encounters an object
produced as described above (in the #Y or #Z case).  When the object
was written, information was recorded on whether that object was a
hons.  In the case of #Z, the object will be read as a hons if and only
if it was originally written as a hons.  But in the case of #Y, it will
never be read as a hons.  Thus, #Y and #Z will behave the same if the
original written object was not a hons, creating an object that is not
a hons.  For an equivalent explanation and a bit more discussion, see
SERIALIZE-READ, in particular the discussion of the hons-mode.
The value :smart described there corresponds to #Z, while :never
corresponds to #Y.

STOBJ    single-threaded objects or "von Neumann bottlenecks"

In ACL2, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist and its fields can be updated by destructive assignments.

Note: Novices are advised to avoid using single-threaded objects,
perhaps instead using community book
books/data-structures/structures.lisp.  At the least, consider using
(set-verify-guards-eagerness 0) to avoid guard verification.

The documentation in this section is laid out in the form of a tour that
visits the documented topics in a reasonable order.  We recommend that
you follow the tour the first time you read about stobjs.  The list of
all stobj topics is shown below.  The tour starts immediately
afterwards.  Also see DEFSTOBJ and, for so-called abstract
stobjs, see DEFABSSTOBJ.

Related topics other than immediate subtopics:

As noted, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist.  Updates to the object must be sequentialized.  This allows us to
update its fields with destructive assignments without wrecking the
axiomatic semantics of update-by-copy.  For this reason,
single-threaded objects are sometimes called "von Neumann bottlenecks."

From the logical perspective, a single-threaded object is an ordinary
ACL2 object, e.g., composed of integers and conses.  Logically
speaking, ordinary ACL2 functions are defined to allow the user to
"access" and "update" its fields.  Logically speaking, when fields in
the object, obj, are "updated" with new values, a new object, obj', is
constructed.

But suppose that by syntactic means we could ensure that there were no
more references to the "old" object, obj.  Then we could create obj' by
destructively modifying the memory locations involved in the
representation of obj.  The syntactic means is pretty simple but
draconian: the only reference to obj is in the variable named OBJ.

The consequences of this simple rule are far-reaching and require some
getting used to.  For example, if OBJ has been declared as a
single-threaded object name, then the following consequences ensue (but
see the discussion of congruent stobjs below for a slight relaxation).

o OBJ is a top-level global variable that contains the current object,
obj.

o If a function uses the formal parameter OBJ, the only "actual
expression" that can be passed into that slot is the variable OBJ, not
merely a term that "evaluates to an obj"; thus, such functions can only
 operate on the current object.  So for example, instead of   (FOO
(UPDATE-FIELD1 3 ST)) write   (LET ((ST (UPDATE-FIELD1 3 ST))) (FOO
ST)).

o The accessors and updaters have a formal parameter named OBJ, thus,
those functions can only be applied to the current object.

o The ACL2 primitives, such as CONS, CAR and CDR, may not be   applied
to the variable OBJ.  Thus, for example, obj may not be consed   into a
list (which would create another pointer to it) or accessed or   copied
via "unapproved" means.

o The updaters return a "new OBJ object", i.e., obj'; thus, when   an
updater is called, the only variable which can hold its result is   OBJ.

o If a function calls an OBJ updater, it must return an OBJ object
(either as the sole value returned, or in (mv ... OBJ ...); see
MV).

o When a top-level expression involving OBJ returns an OBJ object,
that object becomes the new current value of OBJ.

What makes ACL2 different from other functional languages supporting
such operations (e.g., Haskell's "monads" and Clean's "uniqueness type
system") is that ACL2 also gives single-threaded objects an explicit
axiomatic semantics so that theorems can be proved about them.  In
particular, the syntactic restrictions noted above are enforced only
when single-threaded objects are used in function definitions (which
might be executed outside of the ACL2 read-eval-print loop in Common
Lisp).  The accessor and update functions for single-threaded objects
may be used without restriction in formulas to be proved.  Since
function evaluation is sometimes necessary during proofs, ACL2 must be
able to evaluate these functions on logical constants representing the
object, even when the constant is not "the current object."  Thus, ACL2
supports both the efficient von Neumann semantics and the clean
applicative semantics, and uses the first in contexts where execution
speed is paramount and the second during proofs.

Defstobj and defabsstobj events introduce stobjs.  See DEFSTOBJ
for more details about stobjs.  In particular, a relatively advanced
notion of "congruent stobjs" is discussed there.  The idea is to allow
a stobj, st2, of the same "shape" as a given stobj, st1, to be used in
place of st1.  Other defstobj keywords allow inlining and renaming of
stobj accessors and updaters.

But we are getting ahead of ourselves.  To start the stobj tour, see
STOBJ-EXAMPLE-1.

DECLARE-STOBJS    declaring a formal parameter name to be a single-threaded object

When a defun uses one of its formals as a single-threaded object
(stobj), the defun _must_ include a declaration that the formal is to
be so used.  An exception is the formal "state," which if not declared
as explained below, may still be used provided an appropriate global
"declaration" is issued: see SET-STATE-OK.

If the formal in question is counters then an appropriate declaration is

     (declare (xargs :stobjs counters))

or, more generally,

     (declare (xargs :stobjs (... counters ...)))

where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the
names have previously been defined as single-threaded objects with
defstobj.

When an argument is declared to be single-threaded the guard of the
function is augmented by conjoining to it the condition that the
argument satisfy the recognizer for the single-threaded object.
Furthermore, the syntactic checks done to enforce the legal use of
single-threaded objects are also sufficient to allow these guard
conjuncts to be automatically proved.

The obvious question arises:  Why does ACL2 insist that you declare
stobj names before using them in defuns if you can only declare names
that have already been defined with defstobj?  What would go wrong if a
formal were treated as a single-threaded object if and only if it had
already been so defined?

Suppose that one user, say Jones, creates a book in which counters is
defined as a single-threaded object.  Suppose another user, Smith,
creates a book in which counters is used as an ordinary formal
parameter.  Finally, suppose a third user, Brown, wishes to use both
books.  If Brown includes Jones' book first and then Smith's, then
Smith's function treats counters as single-threaded.  But if Brown
includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to ensure that the definition is
processed the same way no matter what the context.

RESIZE-LIST    list resizer in support of stobjs

(Resize-list lst n default-value) takes a list, lst, and a desired
length, n, for the result list, as well as a default-value to use for
the extra elements if n is greater than the length of lst.

Resize-list has a guard of t.  This function is called in the body of
function, resize-<a> where <a> is an array field of a stobj.  See
STOBJ and see DEFSTOBJ.

STOBJ-EXAMPLE-1    an example of the use of single-threaded objects

Suppose we want to sweep a tree and (1) count the number of interior
nodes, (2) count the number of tips and (3) keep a record of every tip
we encounter that is an integer.  We could use a single-threaded object
as our "accumulator".  Such an object would have three fields, one
holding the number of nodes seen so far, one holding the number of
tips, and one holding all the integer tips seen.

The following event declares counters to be a single-threaded object.

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

It has three fields, NodeCnt, TipCnt, and IntTipsSeen.  (As always in
ACL2, capitalization is irrelevant in simple symbol names, so the first
name could be written nodecnt or NODECNT, etc.) Those are the name of
the accessor functions for the object.  The corresponding update
functions are named update-NodeCnt, update-TipCnt and
update-IntTipsSeen.

If you do not like the default function names chosen above, there is a
feature in the defstobj event that allows you to specify other names.

If you want to see the ACL2 definitions of all the functions defined by
this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level "global variable"
counters in the ACL2 read-eval-print loop we get:

     ACL2 !>counters
     <counters>

Note that the value printed is "<counters>".  Actually, the value of
counters in the logic is (0 0 NIL).  But ACL2 always prints
single-threaded objects in this non-informative way because they are
usually so big that to do otherwise would be unpleasant.

Had you tried to evaluate the "global variable" counters before
declaring it a single-threaded object, ACL2 would have complained that
it does not support global variables.  So a lesson here is that once
you have declared a new single-threaded object your top-level forms can
reference it.  In versions of ACL2 prior to Version  2.4 the only
variable enjoying this status was STATE.  single-threaded objects are a
straightforward generalization of the long-implemented von Neumann
state feature of ACL2.

We can access the fields of counters as with:

     ACL2 !>(NodeCnt counters)
     0
     ACL2 !>(IntTipsSeen counters)
     NIL

and we can set the fields of counters as with:

     ACL2 !>(update-NodeCnt 3 counters)
     <counters>
     ACL2 !>(NodeCnt counters)
     3

Observe that when we evaluate an expression that returns a counter
object, that object becomes the "current value" of counters.

Here is a function that "converts" the counters object to its
"ordinary" representation:

     (defun show-counters (counters)
       (declare (xargs :stobjs (counters)))
       (list (NodeCnt counters)
             (TipCnt counters)
             (IntTipsSeen counters)))

Observe that we _must_ declare, at the top of the defun, that we mean
to use the formal parameter counters as a single-threaded object!  If
we did not make this declaration, the body of show-counters would be
processed as though counters were an ordinary object.  An error would
be caused because the accessors used above cannot be applied to
anything but the single-threaded object counters.  If you want to know
why we insist on this declaration, see DECLARE-STOBJS.

When show-counters is admitted, the following message is printed:

     Since SHOW-COUNTERS is non-recursive, its admission is trivial.  We
     observe that the type of SHOW-COUNTERS is described by the theorem
     (AND (CONSP (SHOW-COUNTERS COUNTERS))
          (TRUE-LISTP (SHOW-COUNTERS COUNTERS))).
     We used primitive type reasoning.

     (SHOW-COUNTERS COUNTERS) => *.

     The guard conjecture for SHOW-COUNTERS is trivial to prove.
     SHOW-COUNTERS is compliant with Common Lisp.

The line above containing the "=>" is called the "signature" of
show-counters; it conveys the information that the first argument is
the single-threaded object counters and the only result is an ordinary
object.  Here is an example of another signature:

     (PROCESSOR * * COUNTERS) => (MV * COUNTERS)

which indicates that the function PROCESSOR (which we haven't shown
you) takes three arguments, the third of which is the COUNTERS stobj,
and returns two results, the second of which is the modified COUNTERS.

Returning to the admission of show-counters above, the last sentence
printed indicates that the guard conjectures for the function were
proved.  When some argument of a function is declared to be a
single-threaded object via the xargs :stobj, we automatically add
(conjoin) to the guard the condition that the argument satisfy the
recognizer for that single-threaded object.  In the case of
show-counters the guard is (countersp counters).

Here is an example of show-counters being called:

     ACL2 !>(show-counters counters)
     (3 0 NIL)

This is what we would see had we set the NodeCnt field of the initial
value of counters to 3, as we did earlier in this example.

We next wish to define a function to reset the counters object.  We
could define it this way:

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters))))

which "successively" sets the NodeCnt field to 0, then the TipCnt field
to 0, and then the IntTipsSeen field to nil and returns the resulting
object.

However, the nest of let expressions is tedious and we use this
definition instead.  This definition exploits a macro, here named "seq"
(for "sequentially") which evaluates each of the forms given, binding
their results successively to the stobj name given.

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

This definition is syntactically identical to the one above, after macro
expansion.  Our definition of seq is shown below and is not part of
native ACL2.

     (defmacro seq (stobj &rest rst)
       (cond ((endp rst) stobj)
             ((endp (cdr rst)) (car rst))
             (t `(let ((,stobj ,(car rst)))
                  (seq ,stobj ,@(cdr rst))))))

The signature printed for reset-counters is

     (RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example.

     ACL2 !>(show-counters counters)
     (3 0 NIL)
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

Here finally is a function that uses counters as a single-threaded
accumulator to collect the desired information about the tree x.

     (defun sweep-tree (x counters)
       (declare (xargs :stobjs (counters)))
       (cond ((atom x)
              (seq counters
                   (update-TipCnt (+ 1 (TipCnt counters)) counters)
                   (if (integerp x)
                       (update-IntTipsSeen (cons x (IntTipsSeen counters))
                                       counters)
                     counters)))
             (t (seq counters
                     (update-NodeCnt (+ 1 (NodeCnt counters)) counters)
                     (sweep-tree (car x) counters)
                     (sweep-tree (cdr x) counters)))))

We can paraphrase this definition as follows.  If x is an atom, then
increment the TipCnt field of counters and _then_, if x is an integer,
add x to the IntTipsSeen field, and return counters.  On the other
hand, if x is not an atom, then increment the NodeCnt field of
counters, and _then_ sweep the car of x and _then_ sweep the cdr of x
and return the result.

Here is an example of its execution.  We have displayed the input tree
in full dot notation so that the number of interior nodes is just the
number of dots.

     ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3)
                          . (4 . (5 . d)))
                        counters)
     <counters>
     ACL2 !>(show-counters counters)
     (7 8 (5 4 3 2 1))
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

The counters object has two integer fields and a field whose type is
unrestricted.  single-threaded objects support other types of fields,
such as arrays.  We deal with that in the stobj-example-2.  But we
recommend that you first consider the implementation issues for the
counters example (in stobj-example-1-implementation) and then consider
the proof issues (in stobj-example-1-proofs).

To continue the stobj tour, see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-1-DEFUNS    the defuns created by the counters stobj

Consider the event shown in stobj-example-1:

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the counters argument below is _not_
declared with the :stobjs xarg even though we insist that the argument
be a stobj in calls of these functions.  This "mystery" is explained
below.

     (defun NodeCntp (x)                 ;;; Recognizer for 1st field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun TipCntp (x)                  ;;; Recognizer for 2nd field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun IntTipsSeenp (x)             ;;; Recognizer for 3rd field
       (declare (xargs :guard t :verify-guards t) (ignore x))
       t)

     (defun countersp (counters)         ;;; Recognizer for object
       (declare (xargs :guard t :verify-guards t))
       (and (true-listp counters)
            (= (length counters) 3)
            (NodeCntp (nth 0 counters))
            (TipCntp (nth 1 counters))
            (IntTipsSeenp (nth 2 counters))
            t))

     (defun create-counters ()           ;;; Creator for object
       (declare (xargs :guard t :verify-guards t))
       (list '0 '0 'nil))

     (defun NodeCnt (counters)           ;;; Accessor for 1st field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 0 counters))

     (defun update-NodeCnt (v counters)  ;;; Updater for 1st field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 0 v counters))

     (defun TipCnt (counters)            ;;; Accessor for 2nd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 1 counters))

     (defun update-TipCnt (v counters)   ;;; Updater for 2nd field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 1 v counters))

     (defun IntTipsSeen (counters)       ;;; Accessor for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 2 counters))

     (defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and
then a recognizer for the counters object itself.  Then, for each
field, there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a
countersp for their counters argument and an appropriate value for the
new field values.

You can see all of the defuns added by a defstobj event by executing
the event and then using the :pcb! command on the stobj name.  E.g.,

     ACL2 !>:pcb! counters

will print the defuns above.

We now clear up the "mystery" mentioned above.  Note, for example in
TipCnt, that the formal counters is used.  From the discussion in
stobj-example-1 it has been made clear that TipCnt can only be called
on the counters object.  And yet, in that same discussion it was said
that an argument is so treated only if it it declared among the :stobjs
in the definition of the function.  So why doesn't TipCnt include
something like (declare (xargs :stobjs (counters)))?

The explanation of this mystery is as follows.  At the time TipCnt was
defined, during the introduction of the counters stobj, the name
"counters" was not yet a single-threaded object.  The introduction of a
new single-threaded object occurs in three steps: (1) The new primitive
recognizers, accessors, and updaters are introduced as "ordinary
functions," producing their logical axiomatizations.  (2) The
executable counterparts are defined in raw Lisp to support destructive
updating.  (3) The new name is declared a single-threaded object to
ensure that all future use of these primitives respects the
single-threadedness of the object.  The functions defined as part of
the introduction of a new single-threaded object are the only functions
in the system that have undeclared stobj formals other than state.

You may return to stobj-example-1 here.

STOBJ-EXAMPLE-1-IMPLEMENTATION    the implementation of the counters stobj

the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, creates a Common Lisp object to represent
the current value of counters.  That object is created by evaluating
either of the following "raw" (non-ACL2) Common Lisp forms:

     (create-counters)

     (vector (make-array 1 :element-type 'integer
                           :initial-element '0)
             (make-array 1 :element-type 'integer
                           :initial-element '0)
             'nil)

and the value is stored in the Common Lisp global variable named
*the-live-counters*.

Thus, the counters object is an array of length three.  The first two
elements are arrays of size 1 and are used to hold the NodeCnt and
TipCnt fields.  The third element is the IntTipsSeen field.  The first
two fields are represented by arrays so that we can implement the
integer type specification efficiently.  Generally, integers are
"boxed" in some Common Lisp implementations, for example, GCL.
Creating a new integer requires creating a new box to put it in.  But
in some lisps, including GCL, the integers inside arrays of integers
are not boxed.

The function NodeCnt is defined in raw Lisp as:

     (defun NodeCnt (counters)
       (the integer
            (aref (the (simple-array integer (1))
                       (svref counters 0))
                  0)))

Observe that the form (svref counters 0) is evaluated to get an array
of size 1, which is followed by a call of aref to access the 0th
element of that array.

The function update-NodeCnt is defined in raw Lisp as:

     (defun update-NodeCnt (v counters)
       (declare (type integer v))
       (progn
        (setf (aref (the (simple-array integer (1))
                         (svref counters 0))
                    0)
              (the integer v))
        counters))

Note that when this function is called, it does not create a new vector
of length three, but "smashes" the existing one.

One way to see all the raw Lisp functions defined by a given defstobj is
to evaluate the defstobj event and then evaluate, in the ACL2 loop, the
expression (nth 4 (global-val 'cltl-command (w state))).  Those
functions that contain (DECLARE (STOBJ-INLINE-FN T)) will generate
defabbrev forms because the :inline keyword of defstobj was supplied the
value t.  The rest will generate defuns.

We now recommend that you look at stobj-example-1-proofs.

STOBJ-EXAMPLE-1-PROOFS    some proofs involving the counters stobj

Consider again the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, followed by the definition

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

which, because of the seq macro in stobj-example-1, is just syntactic
sugar for

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters)))).

Here is a simple theorem about reset-counters.

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem
is unusual in two respects.

First, it calls reset-counters on an argument other than the variable
counters!  That is allowed in theorems; logically speaking, the stobj
functions are indistinguishable from ordinary functions.  Their use is
syntactically restricted only in defuns, which might be compiled and
run in raw Lisp.  Those restrictions allow us to implement stobj
modification destructively.  But logically speaking, reset-counters and
other stobj "modifying" functions just create new objects,
constructively.

Second, the theorem above explicitly provides the hypothesis that
reset-counters is being applied to an object satisfying countersp.
Such a hypothesis is not always required: reset-counters is total and
will do something no matter what x is.  But in this particular case,
the result is not '(0 0 nil) unless x is, at least, a true-list of
length three.

To make a long story short, to prove theorems about stobj functions you
behave in exactly the way you would to prove the same theorems about the
same functions defined without the stobj features.

How can we prove the above theorem?  Unfolding the definition of
reset-counters shows that (reset-counters x) is equal to

     (update-IntTipsSeen nil
       (update-TipCnt 0
         (update-NodeCnt 0 x)))

which in turn is

     (update-nth 2 nil
      (update-nth 1 0
       (update-nth 0 0 x))).

Opening up the definition of update-nth reduces this to

     (list* 0 0 nil (cdddr x)).

This is clearly equal to '(0 0 nil), provided we know that (cdddr x) is
nil.

Unfortunately, that last fact requires a lemma.  The most specific
lemma we could provide is

     (defthm special-lemma-for-counters
       (implies (countersp x)
                (equal (cdddr x) nil)))

but if you try to prove that lemma you will find that it requires some
reasoning about len and true-listp.  Furthermore, the special lemma
above is of interest only for counters.

The following lemma about len is the one we prefer.

     (defthm equal-len-n
       (implies (syntaxp (quotep n))
                (equal (equal (len x) n)
                       (if (integerp n)
                           (if (< n 0)
                               nil
                             (if (equal n 0)
                                 (atom x)
                               (and (consp x)
                                    (equal (len (cdr x)) (- n 1)))))
                         nil))))

This lemma will simplify any equality in which a len expression is
equated to any explicitly given constant _n_, e.g., 3, reducing the
equation to a conjunction of consp terms about the first _n_ cdrs.

If the above lemma is available then ACL2 immediately proves

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

The point is presumably well made: proving theorems about
single-threaded object accessors and updaters is no different than
proving theorems about other recursively defined functions on lists.

As we have seen, operations on stobjs turn into definitions involving
nth and update-nth in the logic.  Here are two lemmas that are useful
for simplifying terms involving nth and update-nth, which are therefore
useful in reasoning about single-threaded objects.

     (defthm update-nth-update-nth-same
       (implies (equal (nfix i1) (nfix i2))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i1 v1 l))))

     (defthm update-nth-update-nth-diff
       (implies (not (equal (nfix i1) (nfix i2)))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i2 v2 (update-nth i1 v1 l))))
       :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))

These lemmas are due to Matt Wilding.  See NU-REWRITER for a
discussion of the efficient simplification of terms of the form (nth n
(update-nth key val lst)), which can be critical in settings involving
sequential bindings that commonly arise in operations involving stobjs.

We now recommend that you see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-2    an example of the use of arrays in single-threaded objects

The following event

     (defstobj ms
       (pcn  :type integer                  :initially 0)
       (mem  :type (array integer (100000)) :initially -1)
       (code :type t                        :initially nil))

introduces a single-threaded object named ms (which stands for "machine
state").  The object has three fields, a pcn or program counter, a mem
or memory, and a code field.

The mem field is occupied by an object initially of type (array integer
(100000)).  Logically speaking, this is a list of length 100000, each
element of which is an integer.  But in the underlying implementation
of the ms object, this field is occupied by a raw Lisp array, initially
of size 100000.

You might expect the above defstobj to define the accessor function mem
and the updater update-mem.  _That does not happen!_.

The above event defines the accessor function memi and the updater
update-memi.  These functions do not access/update the mem field of the
ms object; they access/update the individual elements of the array in
that field.

In particular, the logical definitions of the two functions are:

     (defun memi (i ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms)))))
       (nth i (nth 1 ms)))

     (defun update-memi (i v ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms))
                            (integerp v))))
       (update-nth-array 1 i v ms))

For example, to access the 511th (0-based) memory location of the
current ms you could evaluate:

     ACL2 !>(memi 511 ms)
     -1

The answer is -1 initially, because that is the above-specified initial
value of the elements of the mem array.

To set that element you could do

     ACL2 !>(update-memi 511 777 ms)
     <ms>
     ACL2 !>(memi 511 ms)
     777

The raw Lisp implementing these two functions is shown below.

     (defun memi (i ms)
       (declare (type (and fixnum (integer 0 *)) i))
       (the integer
            (aref (the (simple-array integer (*))
                       (svref ms 1))
                  (the (and fixnum (integer 0 *)) i))))

     (defun update-memi (i v ms)
       (declare (type (and fixnum (integer 0 *)) i)
                (type integer v))
       (progn
        (setf (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (and fixnum (integer 0 *)) i))
              (the integer v))
        ms))

If you want to see the raw Lisp supporting a defstobj, execute the
defstobj and then evaluate the ACL2 form (nth 4 (global-val
'cltl-command (w state))).

To continue the stobj tour, see STOBJ-EXAMPLE-3.

STOBJ-EXAMPLE-3    another example of a single-threaded object

The event

     (defstobj $s
       (x :type integer :initially 0)
       (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))

introduces a stobj named $S.  The stobj has two fields, X and A.  The A
field is an array.  The X field contains an integer and is initially 0.
The A field contains a list of integers, each between 0 and 9,
inclusively.  (Under the hood, this "list" is actually implemented as
an array.)  Initially, the A field has three elements, each of which is
9.

This event introduces the following sequence of function definitions:

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN CREATE-$S NIL ...)        ; creator for stobj $S
     (DEFUN X ($S) ...)               ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Here is the definition of $SP:

     (DEFUN $SP ($S)
       (DECLARE (XARGS :GUARD T :VERIFY-GUARDS T))
       (AND (TRUE-LISTP $S)
            (= (LENGTH $S) 2)
            (XP (NTH 0 $S))
            (AP (NTH 1 $S))
            T))

This reveals that in order to satisfy $SP an object must be a true list
of length 2 whose first element satisfies XP and whose second satisfies
AP.  By printing the definition of AP one learns that it requires its
argument to be a true list, each element of which is an integer between
0 and 9.

The initial value of stobj $S is given by zero-ary "creator" function
CREATE-$S.  Creator functions may only be used in limited contexts.
See WITH-LOCAL-STOBJ.

Here is the definition of UPDATE-AI, the updater for the A field at
index I:

     (DEFUN UPDATE-AI (I V $S)
       (DECLARE (XARGS :GUARD
                       (AND ($SP $S)
                            (INTEGERP I)
                            (<= 0 I)
                            (< I (A-LENGTH $S))
                            (AND (INTEGERP V) (<= 0 V) (<= V 9)))
                       :VERIFY-GUARDS T))
       (UPDATE-NTH-ARRAY 1 I V $S))

By definition (UPDATE-NTH-ARRAY 1 I V $S) is (UPDATE-NTH 1 (UPDATE-NTH
I V (NTH 1 $S)) $S).  This may be a little surprising but should be
perfectly clear.

First, ignore the guard, since it is irrelevant in the logic.  Reading
from the inside out, (UPDATE-AI I V $S) extracts (NTH 1 $S), which is
array a of $S.  (Recall that NTH is 0-based.)  The next higher
expression in the definition above, (UPDATE-NTH I V a), "modifies" a by
setting its Ith element to V.  Call this a'.  The next higher
expression, (UPDATE-NTH 1 a' $S), "modifies" $S by setting its 1st
component to a'.  Call this result $s'.  Then $s' is the result
returned by UPDATE-AI.

So the first useful observation is that from the perspective of the
logic, the type "restrictions" on stobjs are irrelevant.  They are
"enforced" by ACL2's guard mechanism, not by the definitions of the
updater functions.

As one might also imagine, the accessor functions do not really "care,"
logically, whether they are applied to well-formed stobjs or not.  For
example, (AI I $S) is defined to be (NTH I (NTH 1 $S)).

Thus, you will not be able to prove that (AI 2 $S) is an integer.  That
is,

     (integerp (AI 2 $S))

is not a theorem, because $S may not be well-formed.

Now (integerp (AI 2 $S)) will always evaluate to T in the top-level
ACL2 command loop, because we insist that the current value of the
stobj $S always satisfies $SP by enforcing the guards on the updaters,
independent of whether guard checking is on or off; see
SET-GUARD-CHECKING.  But in a theorem $S is just another variable,
implicitly universally quantified.

So (integerp (AI 2 $S)) is not a theorem because it is not true when
the variable $S is instantiated with, say,

     '(1 (0 1 TWO))

because, logically speaking, (AI 2 '(1 (0 1 TWO))) evaluates to the
symbol TWO.  That is,

     (equal (AI 2 '(1 (0 1 TWO))) 'TWO)

is true.

However,

     (implies (and ($SP $S) (< 2 (A-LENGTH $S))) (integerp (AI 2 $S)))

is a theorem.  To prove it, you will have to prove a lemma about AP.
The following will do:

     (defthm ap-nth
       (implies (and (AP x)
                     (integerp i)
                     (<= 0 i)
                     (< i (len x)))
                (integerp (nth i x)))).

Similarly,

     (implies (and (integerp i)
                   (<= 0 i)
                   (< i (A-LENGTH $S))
                   (integerp v)
                   (<= 0 v)
                   (<= v 9))
              ($SP (UPDATE-AI i v $S)))

is not a theorem until you add the additional hypothesis ($SP $S).  To
prove the resulting theorem, you will need a lemma such as the
following.

     (defthm ap-update-nth
       (implies (and (AP a)
                     (integerp v)
                     (<= 0 v)
                     (<= v 9)
                     (integerp i)
                     (<= 0 i)
                     (< i (len a)))
                (AP (update-nth i v a))))

The moral here is that from the logical perspective, you must provide
the hypotheses that, as a programmer, you think are implicit on the
structure of your stobjs, and you must prove their invariance.  This is
a good area for further support, perhaps in the form of a library of
macros.

_Resizing Array Fields_

Recall the specification of the array field, A for the stobj $S
introduced above:

     (a :type (array (integer 0 9) (3)) :initially 9 :resizable t)

Logically, this field is a list, initially of length 3.  Under the
hood, this field is implemented using a Common Lisp array with 3
elements.  In some applications, one may wish to lengthen an array
field, or even (to reclaim space) to shrink an array field.  The
defstobj event provides functions to access the current length of an
array field and to change the array field, with default names obtained
by suffixing the field name with "LENGTH-" or prefixing it with
"RESIZE-," respectively.  The following log shows the uses of these
fields in the above example.

     ACL2 !>(A-LENGTH $S)
     3
     ACL2 !>(RESIZE-A 10 $S) ; change length of A to 10
     <$s>
     ACL2 !>(A-LENGTH $S)
     10
     ACL2 !>(AI 7 $S)        ; new elements get value from :initially
     9
     ACL2 !>(RESIZE-A 2 $S)  ; truncate A down to first 2 elements
     <$s>
     ACL2 !>(A-LENGTH $S)
     2
     ACL2 !>(AI 7 $S)        ; error:  access past array bound

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol AI, which
     is (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S))), is violated
     by the arguments in the call (AI 7 $S).

     ACL2 !>

Here are the definitions of the relevant functions for the above
example; also see RESIZE-LIST.

     (DEFUN A-LENGTH ($S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (LEN (NTH 1 $S)))

     (DEFUN RESIZE-A (K $S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (UPDATE-NTH 1
                   (RESIZE-LIST (NTH 1 $S) K 9)
                   $S))

It is important to note that the implementation of array resizing in
ACL2 involves copying the entire array into a newly allocated space and
thus can be quite costly if performed often.  This approach was chosen
in order to make array access and update as efficient as possible, with
the suspicion that for most applications, array access and update are
considerably more frequent than resizing (especially if the programmer
is aware of the relative costs beforehand).

It should also be noted that computations of lengths of stobj array
fields should be fast (constant-time) in all or most Common Lisp
implementations.

Finally, if :resizable t is not supplied as shown above, then an
attempt to resize the array will result in an error.  If you do not
intend to resize the array, it is better to omit the :resizable option
(or to supply :resizable nil), since then the length function will be
defined to return a constant, namely the initial length, which can
simplify guard proofs (compare with the definition of A-LENGTH above).

This completes the tour through the documentation of stobjs.  However,
you may now wish to read the documentation for the event that
introduces a new single-threaded object; see DEFSTOBJ.

WITH-LOCAL-STATE    locally bind state

This is an advanced topic, probably of interest only to system
developers.

Consider the following example form:

     (with-local-state
      (mv-let (result state)
              (compute-with-state x state)
              result))

This is equivalent to the following form.

     (with-local-stobj
      state
      (mv-let (result state)
              (compute-with-state x state)
              result))

By default, this form is illegal, because ACL2 does not have a way to
unwind all changes to the ACL2 state; we say more on this issue below.
There may however be situations where you are willing to manage or
overlook this issue.  In that case you may execute the following form
to enable the use of with-local-state, by enabling the use of
with-local-stobj on state; but note that it requires an active trust
tag (see DEFTTAG).

     (remove-untouchable create-state t)

Please be aware that no local state is actually created, however!  In
particular, users of with-local-state need either to ensure that
channels are closed and state global variables are returned to their
original values, or else be willing to live with changes made to state
that are not justified by the code that has been evaluated.  You are
welcome to look in the the ACL2 source code at the definition of macro
channel-to-string, which employs with-local-state to create a local
state for the purpose of creating a string.

Here is an example use of with-local-state.  Notice the use of defttag
-- and indeed, please understand that we are just hacking here, and in
general it takes significant effort to be sure that one is using
with-local-state correctly!

     (defttag t)

     (remove-untouchable create-state t)

     (set-state-ok t)

     (defun foo (state)
       (declare (xargs :mode :program))
       (mv-let
        (channel state)
        (open-input-channel "my-file" :object state)
        (mv-let (eofp obj state)
                (read-object channel state)
                (declare (ignore eofp))
                (let ((state (close-input-channel channel state)))
                  (mv obj state)))))

     (defun bar ()
       (declare (xargs :mode :program))
       (with-local-state (mv-let (result state)
                                 (foo state)
                                 result)))

     ; Multiple-value return version:

     (defun foo2 (state)
       (declare (xargs :mode :program))
       (mv-let
        (channel state)
        (open-input-channel "my-file" :object state)
        (mv-let (eofp obj state)
                (read-object channel state)
                (let ((state (close-input-channel channel state)))
                  (mv eofp obj state)))))

     (defun bar2 ()
       (declare (xargs :mode :program))
       (with-local-state (mv-let (eofp result state)
                                 (foo2 state)
                                 (mv eofp result))))

WITH-LOCAL-STOBJ    locally bind a single-threaded object

See STOBJ for an introduction to single-threaded objects.

     Example Form:
     (with-local-stobj
      st
      (mv-let (result st)
              (compute-with-st x st)
              result))

With-local-stobj can be thought of as a macro, where the example form
above expands as follows.

     (mv-let (result st)
             (let ((st (create-st)))
               (compute-with-st x st))
             (declare (ignore st))
             result)

However, ACL2 expects you to use with-local-stobj, not its expansion.
More precisely, stobj creator functions are not allowed except
(implicitly) via with-local-stobj and in logic-only situations (like
theorems and hints).  Moreover, neither with-local-stobj nor its
expansions are legal when typed directly at the top-level loop.  See
TOP-LEVEL for a way to use with-local-stobj in the top-level
loop.

     General Forms:
     (with-local-stobj stobj-name mv-let-form)
     (with-local-stobj stobj-name mv-let-form creator-name)

where stobj-name is the name of a stobj, mv-let-form is a call of
mv-let, and if creator-name is supplied then it should be the name of
the creator function for stobj-name; see DEFSTOBJ.  For the
example form above, its expansion would use creator-name, if supplied,
in place of create-st.  Note that stobj-name must not be state (the
ACL2 state), except in special situations probably of interest only to
system developers; see WITH-LOCAL-STATE.

With-local-stobj can be useful when a stobj is used to memoize
intermediate results during a computation, yet it is desired not to
make the stobj a formal parameter for the function and its callers.

ACL2 can reason about these "local stobjs," and in particular about
stobj creator functions.  For technical reasons, ACL2 will not allow
you to enable the :EXECUTABLE-COUNTERPART rune of a stobj creator
function.

Finally, here is a small example concocted in order to illustrate that
with-local-stobj calls can be nested.

     (defstobj st fld1)

     (defun foo ()
       (with-local-stobj
        st ; Let us call this the ``outer binding of st''.
        (mv-let (val10 val20 st)
          (let ((st (update-fld1 10 st)))
            ;; At this point the outer binding of st has fld1 = 10.
            (let ((result (with-local-stobj
                           st ; Let us call this the ``inner binding of st''.
                           (mv-let (val st)
                             (let ((st (update-fld1 20 st)))
                               ;; Now fld1 = 20 for the inner binding of st.
                               (mv (fld1 st) st))
                             val))))
              ;; So result has been bound to 20 above, but here we are once again
              ;; looking at the outer binding of st, where fld1 is still 10.
              (mv (fld1 st) result st)))
          (mv val10 val20))))

     (thm (equal (foo) (mv 10 20))) ; succeeds

SWITCHES-PARAMETERS-AND-MODES    a variety of ways to modify the ACL2 environment

The beginning user might pay special attention to documentation for
logic and program.  Other topics in this section can be read as one
gains familiarity with ACL2.

ACL2-CUSTOMIZATION    file of initial commands for ACL2 to run at startup

ACL2 provides a mechanism to load automatically a so-called "ACL2
customization file," via ld, the first time lp is called in an ACL2
session.  ACL2 looks for this file as follows.

     o If the host Lisp reads a non-empty value for the system's
     environment variable ACL2_CUSTOMIZATION, then that string value is
     used for the customization file name.  In this case, if the file
     does not exist or if the string is "NONE" then there is no
     customization file.  Notes.  (1) If the customization file name is
     a relative pathname (see PATHNAME), then the pathname is
     considered relative to the connected book directory (see
     CBD).  (2) If this variable is not already defined, then its
     value is set to NONE when the ACL2 makefile system is invoked
     (specifically, using community books file books/Makefile-generic),
     e.g., for a regression.

     o Otherwise (empty environment variable value), file
     "acl2-customization.lsp" or "acl2-customization.lisp" on the
     connected book directory (see CBD), generally the current
     directory, is the customization file (in that order) if either
     exists.

     o Otherwise file "acl2-customization.lsp" or
     "acl2-customization.lisp" on your home directory is the
     customization file (in that order), if either exists (except, this
     case is skipped on Windows operating systems.

Except for the fact that this ld command is not typed explicitly by
you, it is a standard ld command, with one exception: any settings of
ld specials are remembered once this call of ld has completed.  For
example, suppose that you start your customization file with
(set-ld-skip-proofsp t state), so that proofs are skipped as it is
loaded with ld.  Then the ld special ld-skip-proofsp will remain t
after the ld has completed, causing proofs to be skipped in your ACL2
session, unless your customization file sets this variable back to nil,
say with (set-ld-skip-proofsp nil state).

If the customization file exists, it is loaded with ld using the usual
default values for the ld specials (see LD).  Thus, if an error
is encountered, no subsequent forms in the file will be evaluated.

To create a customization file it is recommended that you first give it
a name other than "acl2-customization.lsp" or "acl2-customization.lisp"
so that ACL2 does not try to include it prematurely when you next enter
lp.  Then, while in the uncustomized lp, explicitly invoke ld on your
evolving (but renamed) customization file until all forms are
successfully evaluated.  The same procedure is recommended if for some
reason ACL2 cannot successfully evaluate all forms in your
customization file: temporarily rename your customization file so that
ACL2 does not try to ld it automatically and then debug the new file by
explicit calls to ld.

WARNING!  If you certify a book after the (automatic) loading of a
customization file, the forms in that file will be part of the
portcullis of the books you certify!  That is, the forms in your
customization file at certification time will be loaded whenever
anybody uses the books you are certifying.  Since customization files
generally contain idiosyncratic commands, you may not want yours to be
part of the books you create for others.  Thus, if you have a
customization file then you may want to invoke :ubt 1 before certifying
any books; alternatively, see CERTIFY-BOOK! for automatic
invocation of ubt.

On the other hand, if you wish to prevent undoing commands from the
customization file, see RESET-PREHISTORY.

Finally, we note that except on Windows-based systems, if there is a
file acl2-init.lsp in your home directory, then it will be loaded into
raw Lisp when ACL2 is invoked.

ADD-BINOP    associate a function name with a macro name

The form (add-binop macro macro-fn) is an abbreviation for the form
(add-macro-fn macro macro-fn t).  See ADD-MACRO-FN.

ADD-DEFAULT-HINTS    add to the default hints

     Examples:
     (add-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))
     (add-default-hints '((computed-hint-3 id clause world))
                        :at-end t)

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
ADD-DEFAULT-HINTS! for a corresponding non-local event).

     General Forms:
     (add-default-hints lst)
     (add-default-hints lst :at-end flg)

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

This event is completely analogous to set-default-hints, the difference
being that add-default-hints appends the indicated hints to the front of
the list of default hints, so that they are tried first -- or, if flg
is supplied and evaluates to other than nil, at the end of the list, so
that they are tried last -- rather than *replacing* the default hints
with the indicated hints.  Each new hint is thus considered after each
existing hints when both are applied to the same goal.  Also See
SET-DEFAULT-HINTS, see REMOVE-DEFAULT-HINTS, and see
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!.

For a related feature, which however is only for advanced system
builders, see OVERRIDE-HINTS.

ADD-DEFAULT-HINTS!    add to the default hints non-locally

Please see ADD-DEFAULT-HINTS, which is the same as
add-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably add-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.

ADD-DIVE-INTO-MACRO    associate proof-checker diving function with macro name

     Examples:
     (add-dive-into-macro cat expand-address-cat)

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

ADD-INCLUDE-BOOK-DIR    link keyword for :dir argument of ld and include-book

     Example Form:
     (add-include-book-dir :smith "/u/smith/")
      ; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".

     General Form:
     (add-include-book-dir kwd dir)

where kwd is a keywordp and dir is the pathname of a directory.  (If
the final '/' is missing, ACL2 will add it for you.)  The effect of
this event is to modify the meaning of the :dir keyword argument of
include-book as indicated by the examples above, and similarly for ld,
namely by associating the indicated directory with the indicated
keyword for purposes of the :dir argument.  By the "indicated
directory" we mean, in the case that the pathname is a relative
pathname, the directory relative to the current connected book
directory; see CBD.  See DELETE-INCLUDE-BOOK-DIR for
how to undo this effect.

A keyword that is already associated with a directory string by an
existing invocation of add-include-book-dir cannot be associated with a
different directory string.  If that is your intention, first apply
delete-include-book-dir to that keyword; see
DELETE-INCLUDE-BOOK-DIR.  If however the new directory string is
identical with the old, then the call of add-include-book-dir will be
redundant (see REDUNDANT-EVENTS).

The keyword :system can never be redefined.  It will always point to the
absolute pathname of the system books directory, which by default is
immediately under the directory where the ACL2 executable was originally
built (see INCLUDE-BOOK, in particular the discussion there of
"books directory").

This macro generates (in essence) a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which it occurs.  See
ACL2-DEFAULTS-TABLE.  Even if you invoke add-include-book-dir before
certifying a book, so that this event is among the book's portcullis
commands rather than in the book itself, nevertheless that
add-include-book-dir event will not be visible after the book is
included.  (Note: The above behavior is generally preserved in raw-mode
(see SET-RAW-MODE),though by means other than a table.)

ADD-INVISIBLE-FNS    make some unary functions invisible to the loop-stopper algorithm

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

Each of the events above makes unary functions unary- and foo
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Thus, arg and (unary- arg) will be given the same
weight and will be permuted so as to be adjacent.

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

where top-fn is a function symbol and the unary-fni are unary function
symbols, or more generally, these are all macro aliases for function
symbols (see MACRO-ALIASES-TABLE).

For more information see INVISIBLE-FNS-TABLE.  Also see
SET-INVISIBLE-FNS-TABLE, which explains how to set the entire table
in a single event, and see REMOVE-INVISIBLE-FNS.

ADD-MACRO-ALIAS    associate a function name with a macro name

     Example:
     (add-macro-alias append binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.  See
MACRO-ALIASES-TABLE for more details.  Also see
ADD-MACRO-FN for an extension of this utility that also affects
printing.

     General Form:
     (add-macro-alias macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table.  See
MACRO-ALIASES-TABLE and also see REMOVE-MACRO-ALIAS.

ADD-MACRO-FN    associate a function name with a macro name

     Examples:
     (add-macro-fn append binary-append)
     (add-macro-fn append binary-append t)

These examples each associate the function symbol binary-append with
the macro name append.  As a result, theory functions will understand
that append refers to binary-append -- see ADD-MACRO-ALIAS --
and moreover, proof output will be printed using append rather than
binary-append.  In the first case, (append x (append y z)) is printed
rather than (append x y z).  In the second case, right-associated
arguments are printed flat: (append x y z).  Such right-association is
considered only for binary function symbols; otherwise the optional
third argument is ignored.

     General Forms:
     (add-macro-fn macro-name function-name)
     (add-macro-fn macro-name function-name nil) ; same as abov
     (add-macro-fn macro-name function-name t)

This is a convenient way to add an entry to macro-aliases-table and at
the same time extend the untrans-table.  As suggested by the example
above, calls of a function in this table will be printed as
corresponding calls of macros, with right-associated arguments printed
flat in the case of a binary function symbol if the optional third
argument is t.  In that case, for a binary function symbol fn
associated with macro name mac, then a call (fn arg1 (fn arg2 (... (fn
argk arg)))) will be displayed to the user as though the "term" were
(mac arg1 arg2 ... argk arg).  For a call (f a1 ... ak) of a function
symbol that is not binary, or the optional argument is not supplied as
t, then the effect is simply to replace f by the corresponding macro
symbol.  See ADD-MACRO-ALIAS, which is invoked on the first two
arguments.  Also see REMOVE-MACRO-ALIAS, see
UNTRANS-TABLE, and see REMOVE-MACRO-FN.

ADD-MATCH-FREE-OVERRIDE    set :match-free value to :once or :all in existing rules

     Example Forms:
     (add-match-free-override :once t)
         ; Try only the first binding of free variables when relieving hypotheses
         ; of any rule of class :rewrite, :linear, or :forward-chaining.
     (add-match-free-override :all (:rewrite foo) (:rewrite bar))
         ; For rewrite rules foo and bar, try all bindings of free variables when
         ; relieving hypotheses.
     (add-match-free-override :clear)
         ; Restore :match-free to what was originally stored for each rule (either
         ; :all or :once).

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving a hypothesis, as a basis for relieving
subsequent hypotheses.  This direction is generally provided by
specifying either :match-free :once or :match-free :all in the
:rule-classes of the rule, or by using the most recent
set-match-free-default event.  Also see RULE-CLASSES.

However, if a proof is going slowly, you may want to modify the
behavior of some such rules so that they use only the first match for
free variables in a hypothesis when relieving subsequent hypotheses,
rather than backtracking and trying additional matches as necessary.
(But note: add-match-free-override is not relevant for type-prescription
rules.)  The event (add-match-free-override :once t) has that effect.
Or at the other extreme, perhaps you want to specify all rules as :all
rules except for a some specific exceptions.  Then you can execute
(add-match-free-override :all t) followed by, say,
(add-match-free-override :once (:rewrite foo) (:linear bar)).

     General Forms:
     (add-match-free-override :clear)
     (add-match-free-override flg t)
     (add-match-free-override flg rune1 rune2 ... runek)

where flg is :once or :all and the runei are runes.  If :clear is
specified then all rules will have the :all/:once behavior from when
they were first stored.  The second general form causes all rewrite
linear, and forward-chaining rules to have the behavior specified by
flg (:all or :once).  Finally, the last of these, where runes are
specified, is additive in the sense that only the indicated rules are
affected; all others keep the behavior they had just before this event
was executed (possible because of earlier add-match-free-override
events).

At the conclusion of this event, ACL2 prints out the list of all
:linear, :rewrite, and :forward-chaining runes whose rules contain free
variables in hypotheses that are to be bound :once, except that if
there are no overrides (value :clear was used), then :clear is printed.

This event only affects rules that exist at the time it is executed.
Future rules are not affected by the override.

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
uses the acl2-defaults-table, and hence its effect is local to the book
or encapsulate form in which it occurs.

_Remarks_

Lists of the :rewrite, :linear, and :forward-chaining runes whose
behavior was originally :once or :all are returned by the following
forms, respectively.

     (free-var-runes :once (w state))
     (free-var-runes :all  (w state))

The form

     (match-free-override (w state))

evaluates to a pair, whose car is a number used by ACL2 to determine
whether a rune is sufficiently old to be affected by the override, and
whose cdr is the list of runes whose behavior is specified as :once by
add-match-free-override; except, if no runes have been overridden, then
the keyword :clear is returned.

ADD-NTH-ALIAS    associate one symbol with another for printing of nth/update-nth terms

     Example:
     (add-nth-alias st0 st)

This example associates the symbol st0 with the symbol st for purposes
of printing certain terms of the form (nth n st0) and (update-nth n val
st0).

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

This is a convenient way to add an entry to nth-aliases-table.  See
NTH-ALIASES-TABLE and also see REMOVE-NTH-ALIAS.

ADD-OVERRIDE-HINTS    add to the override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to extend the list of override-hints.  Note that the
effects of add-override-hints events are local to the books or
encapsulate events in which they reside; see
ADD-OVERRIDE-HINTS! to avoid that restriction.  Also see
SET-OVERRIDE-HINTS to set a new list of override-hints to it,
ignoring the present list rather than adding to it.

     General Forms:
     (add-override-hints form)
     (add-override-hints form :at-end t)
     (add-override-hints form :at-end nil) ; default for :at-end

where form evaluates to a list of computed hint forms.  The effect of
this event is to extend the current list of override-hints by appending
the result of that evaluation.  The default is to append the evaluation
result to the front of the current list of override-hints, but if
:at-end t is specified, then the evaluation result is appended to the
end of the current list.

ADD-OVERRIDE-HINTS!    add non-locally to the override-hints

Add-override-hints! is the same as add-override-hints, except that the
former is not local to books or encapsulate events in which it occurs.
See ADD-OVERRIDE-HINTS; also see SET-OVERRIDE-HINTS.

DEFAULT-HINTS-TABLE    a table used to provide hints for proofs

Please see SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see REMOVE-DEFAULT-HINTS for how to use this table.  For
completeness, we mention here that under the hood, these events all
update the default-hints-table by updating its key, t, for example as
follows.

     (table default-hints-table t
            '((computed-hint-1 clause)
              (computed-hint-2 clause
                               stable-under-simplificationp)))

The use of default hints is explained elsewhere; see
SET-DEFAULT-HINTS.

Advanced users only: see OVERRIDE-HINTS for an advanced variant
of default hints.

DEFAULT-VERIFY-GUARDS-EAGERNESS    See SET-VERIFY-GUARDS-EAGERNESS.

DELETE-INCLUDE-BOOK-DIR    unlink keyword for :dir argument of ld and include-book

     Example Forms:
     (delete-include-book-dir :smith)
      ; Remove association of directory with :smith for include-book.

     General Form:
     (delete-include-book-dir kwd)

where kwd is a keywordp.  The effect of this event is to modify the
meaning of the :dir keyword argument of include-book and ld as
indicated by the examples above, namely by removing association of any
directory with the indicated keyword for purposes of the include-book
(and ld) :dir argument.  Normally one would instead use
add-include-book-dir to associate a new directory with that keyword;
see ADD-INCLUDE-BOOK-DIR.

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

This macro is local to any books and encapsulate events in which it
occurs; see ADD-INCLUDE-BOOK-DIR for a discussion of this aspect
of both macros.

DIVE-INTO-MACROS-TABLE    right-associated function information for the proof-checker

     Examples:
     ACL2 !>(dive-into-macros-table (w state))
     ((CAT . EXPAND-ADDRESS-CAT)
      (LXOR . EXPAND-ADDRESS-LXOR)

This table associates macro names with functions used by the
proof-checker's DV and numeric diving commands (e.g., 3) in order to
dive properly into subterms.  See PROOF-CHECKER, in particular
the documentation for DV.

This table can be extended easily.  See ADD-DIVE-INTO-MACRO and
also see REMOVE-DIVE-INTO-MACRO.

The symbol associated with a macro should be a function symbol taking
four arguments, in this order:

     car-addr ; the first number in the list given to the proof-checker's
                DV command
     raw-term ; the untranslated term into which we will dive
     term     ; the translated term into which we will dive
     wrld     ; the current ACL2 logical world

The function will normally return a list of positive integers,
representing the (one-based) address for diving into term that
corresponds to the single-address dive into raw-term by car-address.
However, it can return (cons str alist), where str is a string suitable
for fmt and args is the corresponding alist for fmt.

Referring to the example above, expand-address-cat would be such a
function, which will be called on raw-term values that are calls of
cat.  See the community book books/misc/rtl-untranslate.lisp for the
definition of such a function.

See TABLE for a general discussion of tables.

INVISIBLE-FNS-TABLE    functions that are invisible to the loop-stopper algorithm

     Examples:
     ACL2 !>(invisible-fns-table (w state))
     ((binary-+ unary--)
      (binary-* unary-/)
      (unary-- unary--)
      (unary-/ unary-/))

Among other things, the setting above has the effect of making unary-
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Also see ADD-INVISIBLE-FNS and see
REMOVE-INVISIBLE-FNS, which manage macro aliases (see
MACRO-ALIASES-TABLE), as well as see SET-INVISIBLE-FNS-TABLE.

See TABLE for a general discussion of tables.

The "invisible functions table" is an alist with elements of the
following form, where fn is a function symbol and the ufni are unary
function symbols in the current ACL2 world, and k is at least 1.

     (fn ufn1 ufn2 ... ufnk)

This table thus associates with certain function symbols, e.g., fn
above, a set of unary functions, e.g., the ufni above.  The ufni
associated with fn in the invisible functions table are said to be
"invisible with respect to fn."  If fn is not the car of any pair in
the alist, then no function is invisible for it.  Thus for example,
setting the invisible functions alist to nil completely eliminates the
consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper
field of :rewrite rules to prevent the indefinite application of
permutative rewrite rules.  Roughly speaking, if rewrite rules are
being used to permute arg and (ufni arg) inside of a nest of fn calls,
and ufni is invisible with respect to fn, then arg and (ufni arg) are
considered to have the same "weight" and will be permuted so as to end
up as adjacent tips in the fn nest.  See LOOP-STOPPER.

LOGIC    to set the default defun-mode to :logic

     Example:
     ACL2 p!>:logic
     ACL2 !>

Typing the keyword :logic sets the default defun-mode to :logic.

Functions defined in :logic mode are logically defined.  See
DEFUN-MODE.

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

See DEFUN-MODE for a discussion of the defun-modes available
and what their effects on the logic are.  See
DEFAULT-DEFUN-MODE for a discussion of how the default defun-mode is
used.  This event is equivalent to (table acl2-defaults-table
:defun-mode :logic), and hence is local to any books and encapsulate
events in which it occurs. See ACL2-DEFAULTS-TABLE.

Recall that the top-level form :logic is equivalent to (logic); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:logic in a book, use (logic), which is an embedded event form, rather
than :logic, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

MACRO-ALIASES-TABLE    a table used to associate function names with macro names

     Example:
     (table macro-aliases-table 'append 'binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.
Thus, for example, it will be legal to write

     (in-theory (disable append))

as an abbreviation for

     (in-theory (disable binary-append))

which in turn really abbreviates

     (in-theory (set-difference-theories (current-theory :here)
                                         '(binary-append)))

     General Form:

     (table macro-aliases-table 'macro-name 'function-name)

or very generally

     (table macro-aliases-table macro-name-form function-name-form)

where macro-name-form and function-name-form evaluate, respectively, to
a macro name and a symbol in the current ACL2 world.  See TABLE
for a general discussion of tables and the table event used to
manipulate tables.

Note that function-name-form (above) does not need to evaluate to a
function symbol, but only to a symbol.  As a result, one can introduce
the alias before defining a recursive function, as follows.

     (table macro-aliases-table 'mac 'fn)
     (defun fn (x)
       (if (consp x)
           (mac (cdr x))
         x))

Although this is obviously contrived example, this flexibility can be
useful to macro writers; see for example the definition of ACL2 system
macro defun-inline.

The table macro-aliases-table is an alist that associates macro symbols
with function symbols, so that macro names may be used as runic
designators (see THEORIES).  For a convenient way to add
entries to this table, see ADD-MACRO-ALIAS.  To remove entries
from the table with ease, see REMOVE-MACRO-ALIAS.

This table is used by the theory functions; see THEORIES.  For
example, in order that (disable append) be interpreted as (disable
binary-append), it is necessary that the example form above has been
executed.  In fact, this table does indeed associate many of the macros
provided by the ACL2 system, including append, with function symbols.
Loosely speaking, it only does so when the macro is "essentially the
same thing as" a corresponding function; for example, (append x y) and
(binary-append x y) represent the same term, for any expressions x and
y.

NTH-ALIASES-TABLE    a table used to associate names for nth/update-nth printing

     Example:
     (table nth-aliases-table 'st0 'st)

This example associates the symbol st0 with the symbol st.  As a
result, when the theorem prover prints terms of the form (nth n st0) or
(update-nth n val st0), where st is a stobj whose nth accessor function
is f-n, then it will print n as *f-n*.

     General Form:
     (table nth-aliases-table 'alias-name 'name)

This event causes alias-name to be treated like name for purposes of
the printing of terms that are calls of nth and update-nth.  (Note
however that name is not recursively looked up in this table.)  Both
must be symbols other than state.  See TERM, in particular the
discussion there of untranslated terms.

For a convenient way to add entries to this table, see
ADD-NTH-ALIAS.  To remove entries from the table with ease, see
REMOVE-NTH-ALIAS.

PRINT-SUMMARY-USER    causing additional summary output

ACL2 prints summaries at the conclusions of processing events (unless
summaries are inhibited; see SET-INHIBIT-OUTPUT-LST and also
see SET-INHIBITED-SUMMARY-TYPES).  You may arrange for
information to be printed at the end of the summary, by defining a
function of state that returns an ordinary value (typically nil, but
the value is irrelevant).  This function should normally be a
guard-verified :logic mode function with no explicit guard (hence, its
guard is actually (state-p state)), but later below we discuss how to
avoid this requirement.  It is then attached (see DEFATTACH) to
the function print-summary-user.  The following example illustrates how
this all works.

     (defun print-summary-user-test (state)
       (declare (xargs :stobjs state))
       (and (f-boundp-global 'abbrev-evisc-tuple state)
            (observation-cw
             'my-test
             "~|Value of abbrev-evisc-tuple: ~x0~|"
             (f-get-global 'abbrev-evisc-tuple state))))

     (defattach print-summary-user print-summary-user-test)

After admission of the two events above, every event summary will
conclude with extra printout, for example:

     ACL2 Observation in MY-TEST:
     Value of abbrev-evisc-tuple: :DEFAULT

If the attachment function (above, print-summary-user-test) does not
meet all the requirements stated above, then you can use the
:skip-checks argument of defattach to get around the requirement, as
illustrated by the following example.

     (defun print-summary-user-test2 (state)
       (declare (xargs :stobjs state
                       :mode :program))
       (observation-cw
        'my-test
        "~|Value of term-evisc-tuple: ~x0~|"
        (f-get-global 'term-evisc-tuple state)))

     (defttag t) ; needed for :skip-checks t

     (defattach (print-summary-user print-summary-user-test2)
                :skip-checks t)

PROGRAM    to set the default defun-mode to :program

     Example:
     ACL2 !>:program
     ACL2 p!>

Typing the keyword :program sets the default defun-mode to :program.

Functions defined in :program mode are logically undefined but can be
executed on constants outside of deductive contexts.  See
DEFUN-MODE.

Calls of the following macros are ignored (skipped) when in :program
mode.

     local
     verify-guards
     verify-termination
     defaxiom
     defthm
     deftheory
     in-theory
     in-arithmetic-theory
     regenerate-tau-database
     theory-invariant
     defchoose

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

See DEFUN-MODE for a discussion of the defun-modes available
and what their effects on the logic are.  See
DEFAULT-DEFUN-MODE for a discussion of how the default defun-mode is
used.  This event is equivalent to (table acl2-defaults-table
:defun-mode :program), and hence is local to any books and encapsulate
events in which it occurs. See ACL2-DEFAULTS-TABLE.

Recall that the top-level form :program is equivalent to (program); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:program in a book, use (program), which is an embedded event form,
rather than :program, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

PUSH-UNTOUCHABLE    add name or list of names to the list of untouchable symbols

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

     General Form:
     (push-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 union the given symbols
into the list of "untouchable variables" in the current world if fn-p is
nil, else to union the symbols into the list of "untouchable
functions".  This event is redundant if every symbol listed is already
a member of the appropriate untouchables list (variables or functions).

When a symbol is on the untouchables list it is syntactically illegal
for any event to call a function or macro of that name, if fn-p is
non-nil, or to change the value of a state global variable of that
name, if fn-p is nil.  Thus, the effect of pushing a function symbol,
name, onto untouchables is to prevent any future event from using that
symbol as a function or macro, or as a state global variable (according
to fn-p).  This is generally done to "fence off" some primitive
function symbol from "users" after the developer has used the symbol
freely in the development of some higher level mechanism.

Also see REMOVE-UNTOUCHABLE.

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

The form (remove-binop macro-fn) is an abbreviation for the form
(remove-macro-fn macro-fn).  See REMOVE-MACRO-FN.

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.

Also See SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see 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!.

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)
     (remove-invisible-fns (+ 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, or more generally, these are all macro aliases for function
symbols (see MACRO-ALIASES-TABLE).

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-MACRO-FN    remove the association of a function name with a macro name

     Example:
     (remove-macro-fn binary-append)

     General Form:
     (remove-macro-fn macro-fn)

See ADD-MACRO-FN for a discussion of how to associate a macro
name with a function name.  This form sets untrans-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-NTH-ALIAS    remove a symbol alias 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-OVERRIDE-HINTS    delete from the list of override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to delete from the list of override-hints.  Note that the
effects of remove-override-hints events are local to the books or
encapsulate events in which they reside; see
REMOVE-OVERRIDE-HINTS! to avoid that restriction.  Also see
ADD-OVERRIDE-HINTS and see SET-OVERRIDE-HINTS.

     General Form:
     (remove-override-hints form)

where form should evaluate to a list of computed hint forms.  The effect
of this event is to set the list of override-hints to the result of
deleting each element of the evaluation result from the override-hints,
if that element indeed belongs to the override-hints; no check is made
that these elements are actually elements of the existing
override-hints.

REMOVE-OVERRIDE-HINTS!    delete non-locally from the list of override-hints

Remove-override-hints! is the same as remove-override-hints, except
that the former is not local to books or encapsulate events in which it
occurs.  See REMOVE-OVERRIDE-HINTS; also see
ADD-OVERRIDE-HINTS and see SET-OVERRIDE-HINTS.

REMOVE-UNTOUCHABLE    remove names from lists of untouchable symbols

     Example Forms:
     (remove-untouchable my-var nil) ; then state global my-var is not untouchable
     (remove-untouchable set-mem t)  ; then function set-mem is not untouchable

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.

     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.

RETURN-LAST-TABLE    install special raw Lisp behavior

Please first see RETURN-LAST for relevant background.

This table is for advanced users only, and requires an active trust tag
(see DEFTTAG).  We recommend that you do not modify this table
directly, but instead use the macro defmacro-last.  Here we augment
that discussion with some highly technical observations that can
probably be ignored if you use defmacro-last.

This table has a :guard requiring that each key be a symbol defined in
raw Lisp, generally as a macro, and requiring that each non-nil value
be associated either with a symbol that names a macro defined in ACL2,
or else with a list of one element containing such a symbol.  The table
can only be modified when there is an active trust tag; see
DEFTTAG.  If a key is associated with the value nil, then that key is
treated as though it were not in the table.

Note that keys of this table are not eligible to be bound by flet.  The
current value of this table may be obtained by evaluating the form
(table-alist 'return-last-table (w state)).  The built-in constant
*initial-return-last-table* holds the initial value of this table.

RULER-EXTENDERS    control for ACL2's termination and induction analyses

*Introduction*

Consider the following recursive definition, which returns a list of
threes of length one more than the length of x.

       (defun f (x)
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

One might expect ACL2's termination analysis to admit this function,
since we know that (cdr x) is "smaller" than x if (consp x) is true.
(By default, ACL2's notion of "smaller" is ordinary natural-number <,
and the argument x is measured by applying function acl2-count to x.)
However, that termination analysis does not consider IF tests, like
(consp x) above, when they occur under calls of functions other than
IF, such as CONS in the case above.

One way to overcome this problem is to "lift" the IF test to the top
level, as follows.

       (defun f (x)
         (if (consp x)
             (cons 3 (f (cdr x)))
           (cons 3 nil)))

But another way to overcome the problem is to tell ACL2 to extend its
termination (and induction) analysis through calls of cons, as follows.

       (defun f (x)
         (declare (xargs :ruler-extenders (cons)))
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

You may even wish to provide value :all instead of an explicit list of
ruler-extenders, so that no function call blocks the termination
analysis:

       (defun f (x)
         (declare (xargs :ruler-extenders :all))
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

Alternatively, you can omit the XARGS :RULER-EXTENDERS form, instead
modifying the global default set of ruler-extenders:

       (set-ruler-extenders :all)

       ; or, for example:
       (set-ruler-extenders '(cons return-last))

You can call the function default-ruler-extenders as follows to see the
current global default set of ruler-extenders:

     (default-ruler-extenders (w state))

We conclude this introduction by considering the handling of LET
expressions by termination analysis.  Consider the following example.

       (defun fact (n)
         (the (integer 1 *)
              (if (posp n)
                  (* n (fact (1- n)))
                1)))

ACL2 treats the call of THE in the body of this definition as follows.

       (let ((var (if (posp n)
                      (* n (fact (1- n)))
                    1)))
         (if (and (integerp var) (<= 1 var))
             var
           <some_error>))

A LET expression, in turn, is treated as a LAMBDA application:

       ((lambda (var)
          (if (if (integerp var)
                  (not (< var 1))
                nil)
              var
            <some_error>))
        (if (posp n)
            (* n (fact (1- n)))
          1))

Notice that the posp test, which governs the recursive call of fact, is
inside an argument of a function application, namely the application of
the LAMBDA expression.  So by default, ACL2 will not consider this posp
test in its termination analysis.  The keyword :LAMBDAS in the list of
ruler-extenders denotes all calls of lambda expressions, much as the
inclusion of CONS in the ruler-extenders denotes all calls of CONS.
The following definition is thus accepted by ACL2.

       (defun fact (n)
         (declare (xargs :ruler-extenders (:lambdas)))
         (the (integer 1 *)
              (if (posp n)
                  (* n (fact (1- n)))
                1)))

As a convenience, ACL2 allows the symbol :lambdas in place of
(:lambdas), and in fact the former will also include the default
ruler-extenders: RETURN-LAST (which comes from macroexpansion of calls
of PROG2$, EC-CALL, and others) and MV-LIST.

IMPORTANT REMARKS.  (1) Notice that the argument to set-ruler-extenders
is evaluated, but the argument to :RULER-EXTENDERS in XARGS is not
evaluated.  (2) Do not put macro names in your list of ruler-extenders.
For example, if you intend that + should not block the termination
analysis, in analogy to cons in the example above, then the list of
ruler-extenders should include binary-+, not +.  Of course, if you use
:all then this is not an issue, but see the next remark.  (3) Also
please note that by taking advantage of the ruler-extenders, you may be
complicating the induction scheme stored for the function, whose
computation takes similar advantage of the additional IF structure that
you are specifying.

Below we describe the notion of ruler-extenders in detail, as well as
how to set its default using set-ruler-extenders.

*Details*

We begin by discussing how to set the ruler-extenders by using the macro
set-ruler-extenders; below we will discuss the use of keyword
:ruler-extenders in XARGS declare forms.

     Examples:
     (set-ruler-extenders :basic) ; return to default
     (set-ruler-extenders *basic-ruler-extenders*) ; same as immediately above
     (set-ruler-extenders :all) ; every governing IF test rules a recursive call
     (set-ruler-extenders :lambdas) ; LET does not block termination analysis
     (set-ruler-extenders (cons :lambdas *basic-ruler-extenders*))
                                    ; same as immediately above
     (set-ruler-extenders '(f g)) ; termination analysis goes past calls of f, g

     General Form:
     (set-ruler-extenders val)

where val evaluates to one of :basic, :all, :lambdas, or a true list of
symbols containing no keyword other than, optionally, :lambdas.

When a recursive definition is submitted to ACL2 (in :logic mode), the
recursion must be proved to terminate; see DEFUN.  More
precisely, ACL2 explores the IF structure of the body of the definition
to accumulate the tests that "rule" any given recursive call.  The
following example reviews how this works.  Suppose that f has already
been defined.

       (defun g (x y)
         (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
         (if (consp x)
             (g (cdr x) y)
           (if (consp y)
               (f (g x (cdr y)))
             (f (list x y)))))

ACL2 makes the following response to this proposed definition.  Notice
that the :measure proposed above must be proved to be an ACL2 ordinal --
that is, to satisfy O-P -- and that the arguments to each recursive
call must be smaller (in the sense of that measure and O<, which here
reduces to the ordinary < relation) than the formals under the
assumption of the ruling IF tests.  The first IMPLIES term below thus
corresponds to the recursive call (g (cdr x) y), while the second
corresponds to the recursive call (g x (cdr y)).

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

       Goal
       (AND (O-P (+ (ACL2-COUNT X) (ACL2-COUNT Y)))
            (IMPLIES (CONSP X)
                     (O< (+ (ACL2-COUNT (CDR X)) (ACL2-COUNT Y))
                         (+ (ACL2-COUNT X) (ACL2-COUNT Y))))
            (IMPLIES (AND (NOT (CONSP X)) (CONSP Y))
                     (O< (+ (ACL2-COUNT X) (ACL2-COUNT (CDR Y)))
                         (+ (ACL2-COUNT X) (ACL2-COUNT Y))))).

Now consider the following alternate version of the above definition.

       (defun g (x y)
         (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
         (if (consp x)
             (g (cdr x) y)
           (f (if (consp y)
                  (g x (cdr y))
                (list x y)))))

The first test, (consp x), still rules the first recursive call, (g
(cdr x) y).  And the negation of that test, namely (not (consp x)),
still rules the second recursive call (g x (cdr y)).  But the call of f
blocks the top-down exploration of the IF structure of the body of g,
so (consp y) does not rule that second recursive call, which (again) is
(g x (cdr y)).  As a result, ACL2 fails to admit the above definition.

Set-ruler-extenders is provided to overcome the sort of blocking
described above.  Suppose for example that the following event is
submitted:

       (set-ruler-extenders '(f))

Then the alternate definition of g above is admissible, because the call
of f no longer blocks the top-down exploration of the IF structure of
the body of g: that is, (consp y) becomes a ruler of the recursive call
(g x (cdr y)).  In this case, we say that f is a "ruler-extender".  The
same result obtains if we first submit

       (set-ruler-extenders :all)

as this removes all function calls as blockers of the top-down
analysis.  In other words, with :all it is the case that for every
recursive call, every test argument of a superior call of IF
contributes a ruler of that recursive call.

ACL2 handles LET (and LET*) expressions by translating them to LAMBDA
expressions (see TERM).  The next examples illustrates
termination analysis involving such expressions.  First consider the
following (admittedly inefficient) definition.

       (defun fact (n)
         (let ((k (if (natp n) n 0)))
           (if (equal k 0)
               1
             (* k (fact (+ -1 k))))))

ACL2 translates the body of this definition to a LAMBDA application,
essentially:

       ((lambda (k)
          (if (equal k 0)
              1
            (* k (fact (+ -1 k)))))
        (if (natp n) n 0))

As with the application of any function other than IF, the top-down
termination analysis does not dive into arguments: the LAMBDA blocks the
continuation of the analysis into its argument.  But here, the argument
of the LAMBDA is (if (natp n) n 0), which has no recursive calls to
consider anyhow.  What is more interesting: ACL2 does continue its
termination analysis into the body of the LAMBDA, in an environment
binding the LAMBDA formals to its actuals.  In this case, the
termination analysis thus continues into the term

       (if (equal k 0)
           1
         (* k (fact (+ -1 k))))

in the environment that binds k to the term (if (natp n) n 0).  Thus,
the proof obligation is successfully discharged, as reported by ACL2:

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

       Goal
       (IMPLIES (NOT (EQUAL (IF (NATP N) N 0) 0))
                (O< (ACL2-COUNT (+ -1 (IF (NATP N) N 0)))
                    (ACL2-COUNT N))).
       .....
       Q.E.D.

       That completes the proof of the measure theorem for FACT.

But now consider the following definition, in which the recursion takes
place inside the argument of the LAMBDA rather than inside the LAMBDA
body.

       (defun app (x y)
         (let ((result (if (endp x)
                           y
                         (cons (car x)
                               (app (cdr x) y)))))
           (if (our-test result)
               result
             0)))

Writing the body in LAMBDA notation:

       ((lambda (result)
          (if (our-test result)
              result
            0))
        (if (endp x)
            y
          (cons (car x)
                (app (cdr x) y))))

By default, the LAMBDA call blocks the top-down termination analysis
from proceeding into the term (if (endp x) ...).  To solve this, one can
submit the event:

       (set-ruler-extenders :lambdas)

The above definition of app is then admitted by ACL2, because the
termination analysis is no longer blocked by the LAMBDA call.

The example just above illustrates that the heuristically-chosen
measure is suitably sensitive to the ruler-extenders.  Specifically:
that measure is the application of acl2-count to the first formal
parameter of the function that is tested along every branch of the
relevant IF structure (as determined by the rulers) and occurs as a
proper subterm at the same argument position in every recursive call.
The heuristics for choosing the controller-alist for a definition rule
are similarly sensitive to the ruler-extenders (see DEFINITION).

The remarks above for defun events are equally applicable when a
definition sits inside a mutual-recursion event, except of course that
in this case, a "recursive call" is a call of any function being
defined by that mutual-recursion event.

Rules of class :definition are sensitive to set-ruler-extenders in
analogy to the case of defun events.

This macro generates a call (table acl2-defaults-table :ruler-extenders
val) and hence is local to any books and encapsulate events in which it
occurs. See ACL2-DEFAULTS-TABLE.  The current list of
ruler-extenders may be obtained as

       (cdr (assoc-eq :ruler-extenders
            (table-alist 'acl2-defaults-table (w state))))

or more conveniently, as:

       (default-ruler-extenders (w state))

Note that evaluation of (set-ruler-extenders lst), where lst evaluates
to a list, does not necessarily include the default ruler-extenders --
i.e., those included for the argument, :basic -- which are the elements
of the list constant *basic-ruler-extenders*, namely return-last and
mv-list.  You may, of course, include these explicitly in your list
argument.

We conclude our discussion by noting that the set of ruler-extenders can
affect the induction scheme that is stored with a recursive definition.
The community book books/misc/misc2/ruler-extenders-tests.lisp explains
how induction schemes are derived in this case.  Consider the following
example.

       (defun tree-of-nils-p (x)
         (if (consp x)
             (and (tree-of-nils-p (car x))
                  (tree-of-nils-p (cdr x)))
           (null x)))

The above definition generates the following induction scheme.  Note
that (and u v) expands to (if u v nil), which explains why the term
(tree-of-nils-p (car x)) rules the recursive call (tree-of-nils-p (cdr
x)), resulting in the hypothesis (tree-of-nils-p (car x)) in the final
conjunct below.

       (AND (IMPLIES (NOT (CONSP X)) (:P X))
            (IMPLIES (AND (CONSP X)
                          (NOT (TREE-OF-NILS-P (CAR X)))
                          (:P (CAR X)))
                     (:P X))
            (IMPLIES (AND (CONSP X)
                          (TREE-OF-NILS-P (CAR X))
                          (:P (CAR X))
                          (:P (CDR X)))
                     (:P X)))

Now consider the following variant of the above definition, in which a
call of the function identity blocks the termination analysis.

       (defun tree-of-nils-p (x)
         (if (consp x)
             (identity (and (tree-of-nils-p (car x))
                            (tree-of-nils-p (cdr x))))
           (null x)))

This time the induction scheme is as follows, since only the top-level
IF test contributes rulers to the termination analysis.

       (AND (IMPLIES (NOT (CONSP X)) (:P X))
            (IMPLIES (AND (CONSP X)
                          (:P (CAR X))
                          (:P (CDR X)))
                     (:P X)))

But now suppose we first designate identity as a ruler-extender.

     (set-ruler-extenders '(identity))

Then the induction scheme generated for the both of the above variants
of tree-of-nils-p is the one shown for the first variant, which is
reasonable because both definitions now produce essentially the same
termination analysis.

SET-ABSSTOBJ-DEBUG    obtain debugging information upon atomicity violation for an abstract stobj

This documentation topic assumes familiarity with abstract stobjs.  See
DEFABSSTOBJ.

Below we explain what is meant by an error message such as the
following.

     ACL2 Error in CHK-ABSSTOBJ-INVARIANTS:  Possible invariance violation
     for an abstract stobj!  See :DOC set-absstobj-debug, and PROCEED AT
     YOUR OWN RISK.

The use of (set-absstobj-debug t) will make this error message more
informative, as follows, at the cost of slower execution -- but in
practice, the slowdown may be negligible (more on that below).

     ACL2 Error in CHK-ABSSTOBJ-INVARIANTS:  Possible invariance violation
     for an abstract stobj!  See :DOC set-absstobj-debug, and PROCEED AT
     YOUR OWN RISK.  Evaluation was aborted under a call of abstract stobj
     export UPDATE-FLD-NIL-BAD.

You may be best off starting a new ACL2 session if you see one of the
errors above.  But you can continue at your own risk.  With a trust tag
(see DEFTTAG), you can even fool ACL2 into thinking nothing is
wrong, and perhaps you can fix up the abstract stobj so that indeed,
nothing really is wrong.  See the community book
books/misc/defabsstobj-example-4.lisp for how to do that.  That book
also documents the :always keyword and a special value for the first
argument, :RESET.

     Examples:
     (set-absstobj-debug t)                 ; obtain extra debug info, as above
     (set-absstobj-debug t :event-p t)      ; same as above
     (set-absstobj-debug t
                         :on-skip-proofs t) ; as above, but even in include-book
     (set-absstobj-debug t :event-p nil)    ; returns one value, not error triple
     (set-absstobj-debug nil)               ; avoid extra debug info (default)

     General Form:
     (set-absstobj-debug val
                         :event-p        event-p        ; default t
                         :always         always         ; default nil
                         :on-skip-proofs on-skip-proofs ; default nil
                         )

where the keyword arguments are optional with defaults as indicated
above, and all supplied arguments are evaluated except for
on-skip-proofsp, which must be Boolean (if supplied).  Keyword
arguments are discussed at the end of this topic.

Recall (see DEFABSSTOBJ) that for any exported function whose
:EXEC function might (according to ACL2's heuristics) modify the
concrete stobj non-atomically, one must specify :PROTECT t.  This
results in extra code generated for the exported function, which
provides a check that atomicity was not actually violated by a call of
the exported function.  The extra code might slow down execution, but
perhaps only negligibly in typical cases.  If you can tolerate a bit
extra slow-down, then evaluate the form (set-absstobj-debug t).
Subsequent such errors will provide additional information, as in the
example displayed earlier in this documentation topic.

Finally we document the keyword arguments, other than :ALWAYS, which is
discussed in a book as mentioned above.  When the value of :EVENT-P is
true, which it is by default, the call of set-absstobj-debug will expand
to an event.  That event is a call of value-triple.  In that case,
:ON-SKIP-PROOFS is passed to that call so that set-absstobj-debug has
an effect even when proofs are being skipped, as during include-book.
That behavior is the default; that is, :ON-SKIP-PROOFS is nil by
default.  Also see VALUE-TRIPLE.  The value of keyword
:ON-SKIP-PROOFS must always be either t or nil, but other than that, it
is ignored when EVENT-P is nil.

SET-BACKCHAIN-LIMIT    sets the backchain-limit used by the type-set and rewriting mechanisms

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 type-set
and rewriting mechanisms.  Its value may be a cons whose car and cdr
are each either nil or a non-negative integer.  Its value x may also be
nil or a non-negative integer, which is treated as a cons whose car and
cdr are both x.

The car is used to limit backchaining used by the ACL2 type-set
mechanism, while the cdr is used to limit backchaining used by the
rewriting mechanism.  See BACKCHAIN-LIMIT for details about how
backchain-limits are used.  Rewrite backchain limits may also be
installed at the level of hints; see HINTS for a discussion of
:backchain-limit-rw.

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

The default limit is (nil 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.

Also see HINTS for discussion of a related hint,
:case-split-limitations.

     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); also see
INTRODUCTION-TO-THE-THEOREM-PROVER for a detailed tutorial on using
the ACL2 prover.  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-COMPILER-ENABLED    See COMPILATION.

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

     Forms (see below for explanations and GCL exceptions):

     (set-debugger-enable t)         ; enable breaks into the raw Lisp debugger
     (set-debugger-enable :break)    ; same as above
     :set-debugger-enable t          ; same as above
     (set-debugger-enable :break-bt) ; as above, but print a backtrace first
     (set-debugger-enable :bt-break) ; as above, but print a backtrace first
     (set-debugger-enable :bt)       ; print a backtrace but do not enter debugger
     (set-debugger-enable :never)    ; disable all breaks into the debugger
     (set-debugger-enable nil)       ; disable debugger except when calling break$

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

It remains to discuss options :break, :bt, :break-bt, and :bt-break.
Option :break is synonymous with option t, while option :bt prints a
backtrace (except in GCL, where a backtrace is already printed for
:break).  Options :break-bt and :bt-break are equivalent, and each has
the combined effect of :bt and :break: a backtrace is printed and then
the debugger is entered.

Note that set-debugger-enable applies not only to raw Lisp errors, but
also to ACL2 errors: those affected by break-on-error.  However, for
ACL2 errors, entering the debugger is controlled only by break-on-error,
not by set-debugger-enable; so for ACL2 errors, set-debugger-enable
values of :bt, :break-bt, and :bt-break have the same effect (namely,
of causing a backtrace to be printed, other than for GCL).

Remark for Common Lisp hackers (except for GCL).  You can customize the
form of the backtrace printed by entering raw Lisp (with :q) and then
redefining function print-call-history, whose definition immediately
precedes that of break-on-error in ACL2 source file ld.lisp.  Of
course, all bets are off when defining any function in raw Lisp, but as
a practical matter you are probably fine as long as your books are
ultimately certified with an unmodified copy of ACL2.  If you come up
with improvements to print-call-history, please pass them along to the
ACL2 implementors.

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,
linear, meta, or type-prescription rule is admitted.  Its value may be
a two-element list whose elements are each either nil or a non-negative
integer.  Its value x may also be nil or a non-negative integer, which
is treated as the two element list (x x).

The first element of the list is used to limit backchaining for a rule
of class type-prescription while the second element is used to limit
backchaining for the other three classes of rules mentioned above.  See
BACKCHAIN-LIMIT for details about how backchain-limits are
used.  The examples below assume that a new rule doesn't itself specify
a value for :backchain-limit-lst.

     :set-default-backchain-limit nil  ; do not impose backchain limits for the
                                       ; rule
     :set-default-backchain-limit 0    ; allow only type-set reasoning for
                                       ; relieving a new rule's hypotheses
     :set-default-backchain-limit 500  ; allow backchaining through a new rewrite,
                                       ; linear, or meta rule's hypotheses to a
                                       ; depth of no more than 500
     (set-default-backchain-limit 500) ; same as above
     :set-default-backchain-limit (nil 500)
                                       ; same as above
     (set-default-backchain-limit '(nil 500))
                                       ; same as above
     (set-default-backchain-limit '(3 500))
                                       ; for a new :type-prescription rule, allow
                                       ; type-set backchaining to a depth
                                       ; of no more than 3; for a new
                                       ; rule of class :rewrite, :linear,
                                       ; or :meta, allow backchaining to
                                       ; a depth of no more than 50
     (set-default-backchain-limit '(nil 500))
                                       ; do not limit backchaining for a
                                       ; new :type-prescription rule; for
                                       ; a new rule of class :rewrite,
                                       ; :linear, or :meta, allow
                                       ; backchaining to a depth of no
                                       ; more than 50

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.  To see the
current default hints, see 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!.

For a related feature, which however is only for advanced system
builders, see OVERRIDE-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-DEFERRED-TTAG-NOTES    modify the verbosity of TTAG NOTE printing

     General Form:
     (set-deferred-ttag-notes val state)

where val is t or nil.

See DEFTTAG for a discussion of trust tags (ttags).  By
default, a "TTAG NOTE" is printed in order to indicate reliance on a
ttag.  When many such notes are printed, it may be desirable to avoid
seeing them all.  Upon evaluation of the form

     (set-deferred-ttag-notes t state)

ACL2 will enter a deferred mode for the printing of ttag notes.  In this
mode, only the first ttag note is printed for each top-level command,
and the remainder are summarized before the next top-level prompt (if
any) is printed, hence before the next command is evaluated.  That
summary is merely a list of ttags, but the summary explains that the
full ttag notes may be printed with the command (show-ttag-notes).

Note that (show-ttag-notes) spares you duplicate ttag notes.  If you
want to see every ttag note as it would normally appear, for maximum
security, do not evaluate the command (set-deferred-ttag-notes t
state).  You can undo the effect of this command, returning to an
immediate mode for printing ttag notes, by evaluating:

     (set-deferred-ttag-notes nil state)

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 community 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, suppressing most proof commentary
     (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.  The
default value is :goals.

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, and see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed
tutorial.  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.lsp" 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 !>

SET-IGNORE-DOC-STRING-ERROR    allow ill-formed documentation strings

     General Forms:
     (set-ignore-doc-string-error nil)   ; :doc strings must be well-formed
     (set-ignore-doc-string-error t)     ; ill-formed :doc strings are ignored
     (set-ignore-doc-string-error :warn) ; ill-formed :doc strings are ignored
                                         ;   except for causing a 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.

     General Form:
     (set-ignore-doc-string-error flag)

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

     (table acl2-defaults-table :ignore-doc-string-error 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-ignore-doc-string-error event.

Note that since defdoc events have the sole purpose of installing
documentation strings, these require well-formed documentation strings
even after executing a call of ignore-doc-string-error.

The default behavior of the system is as though the
:ignore-doc-string-error value is nil.  The current behavior can be
ascertained by evaluating the following form.

     (ignore-doc-string-error (w state))

SET-IGNORE-OK    allow unused formals and locals without an ignore or ignorable declaration

     Examples:
     (set-ignore-ok t)
     (set-ignore-ok nil)
     (set-ignore-ok :warn)

The first example above allows unused formals and locals, i.e.,
variables that would normally have to be declared ignored or ignorable.
The second example disallows unused formals and locals; this is the
default.  The third example allows them, 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-ignore-ok flg)

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

One might find this event useful when one is generating function
definitions by an automated procedure, when that procedure does not
take care to make sure that all formals are actually used in the
definitions that it generates.

Note:  Defun will continue to report irrelevant formals even if
:set-ignore-ok has been set to t, unless you also use
set-irrelevant-formals-ok to instruct it otherwise.

SET-INHIBIT-OUTPUT-LST    control output

     Examples:
     (set-inhibit-output-lst '(warning))
     (set-inhibit-output-lst '(proof-tree prove proof-checker))
     (set-inhibit-output-lst *valid-output-names*) ; inhibit all prover output
     :set-inhibit-output-lst (proof-tree prove)

     General Form:
     (set-inhibit-output-lst lst)

where lst is a form (which may mention state) that evaluates to a list
of names, each of which is the name of one of the following "kinds" of
output produced by ACL2.

       error          error messages
       warning        warnings other than those related to soundness
       warning!       warnings (of all degrees of importance)
       observation    observations
       prove          commentary produced by the theorem prover
       proof-checker  commentary produced by the proof-checker
       event          non-proof commentary produced by events such as defun
                      and encapsulate
       expansion      commentary produced by make-event expansion
       summary        the summary at the successful conclusion of an event
       proof-tree     proof-tree output

It is possible to inhibit each kind of output by putting the
corresponding name into lst.  For example, if 'warning is included in
(the value of) lst, then no warnings are printed except those related
to soundness, e.g., the inclusion of an uncertified book.  Note that
proof-tree output is affected by set-inhibit-output-lst; see
PROOF-TREE.

See WITH-OUTPUT for a variant of this utility that can be used
in books.  Also see SET-INHIBIT-WARNINGS for how to inhibit
individual warning types and see SET-INHIBITED-SUMMARY-TYPES
for how to inhibit individual parts of the summary.

Printing of events on behalf of certify-book and encapsulate is
inhibited when both 'event and 'prove belong to lst.  Otherwise,
printing of events is controlled by the ld special ld-pre-eval-print.

_Note for advanced users._  By including warning! in lst, you are
automatically including warning as well: all warnings will be inhibited.
This is not the case if you modify value of state global variable
'inhibit-output-lst directly (with assign or f-put-global); then, if
you include warning! but not warning, then warnings not related to
soundness will still be printed (which is probably not what was
intended).

SET-INHIBIT-WARNINGS    control warnings

     Examples:
     (set-inhibit-warnings "theory" "use")

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-inhibit-warnings string1 string2 ...)

where each string is considered without regard to case.  This macro is
equivalent to (table acl2-defaults-table :inhibit-warnings lst), where
lst is the list of strings supplied.  This macro is an event (see
TABLE), but no output results from a set-inhibit-warnings event.

The effect of this event is to suppress any warning whose label is a
member of this list (where again, case is ignored).  For example, the
warning

       ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....

will not be printed if "use" (or "USE", etc.) is a member of the given
list of strings.

Of course, if warnings are inhibited overall -- see
SET-INHIBIT-OUTPUT-LST -- then the value of :inhibit-warnings is
entirely irrelevant.

SET-INHIBITED-SUMMARY-TYPES    control which parts of the summary are printed

     Example:
     (set-inhibited-summary-types '(rules time))

Note: This is not an event.  Rather, it changes the state, in analogy to
set-inhibit-output-lst.

     General Form:
     (set-inhibited-summary-types form)

where form evaluates to a true-list of symbols, each of which is among
the values of the constant *summary-types*, i.e.: header, form, rules,
hint-events warnings, time, steps, and value.  Each specified type
inhibits printing of the corresponding portion of the summaries printed
at the conclusions of events, where header refers to an initial newline
followed by the line containing just the word Summary.

Note the distinction between rules and hint-events.  Rules provides a
record of automatic rule usage by the prover, while hint-events shows
the names of events given to :USE or :BY hints, as well as
clause-processor functions given to :CLAUSE-PROCESSOR hints that have
an effect on the proof.

Also see SET-INHIBIT-OUTPUT-LST.  Note that
set-inhibited-summary-types has no effect when summary is one of the
types inhibited by set-inhibit-output-lst, because in that case none of
the summary will be printed.

To control summary types for a single event, see WITH-OUTPUT.

SET-INVISIBLE-FNS-TABLE    set the invisible functions table

     Examples:
     (set-invisible-fns-table ((binary-+ unary--)
                               (binary-* unary-/)
                               (unary-- unary--)
                               (unary-/ unary-/)))
     (set-invisible-fns-table t) ; restore original invisible-fns-table

Among other things, the setting above has the effect of making unary-
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Thus, arg and (unary- arg) will be given the same
weight and will be permuted so as to be adjacent.  The form
(invisible-fns-table (w state)) returns the current value of the
invisible functions table.

Also see ADD-INVISIBLE-FNS and see REMOVE-INVISIBLE-FNS
for events that add to and remove from the invisible functions table,
while accounting for macro aliases (see MACRO-ALIASES-TABLE).

     General Form:
     (set-invisible-fns-table alist)

where alist is either t or a true list of pairs, each element of which
is of the form (fn ufn1 ... ufnk), where fn is a function symbol and
each ufni is a unary function symbol.  When alist is t, the initial
value of this table is used in its place.  Modulo the replacement of
alist by the default setting when alist is t, this macro is equivalent
to

     (table invisible-fns-table nil 'alist :clear)

which is also an event (see TABLE).

Note that set-invisible-fns-table does not evaluate its argument.
However, you can call table directly for that purpose.  For example,

     (set-invisible-fns-table ((binary-+ unary--)
                               (binary-* unary-/)
                               (unary-- unary--)
                               (unary-/ unary-/)))

ie equivalent to the following; see TABLE.

     (table invisible-fns-table nil
            (quote ((binary-+ unary--)
                    (binary-* unary-/)
                    (unary-- unary--)
                    (unary-/ unary-/)))
            :clear)

See INVISIBLE-FNS-TABLE for a description of the invisible
functions table.

SET-IRRELEVANT-FORMALS-OK    allow irrelevant formals in definitions

     Examples:
     (set-irrelevant-formals-ok t)
     (set-irrelevant-formals-ok nil)
     (set-irrelevant-formals-ok :warn)

The first example above allows irrelevant formals in definitions; see
IRRELEVANT-FORMALS.  The second example disallows irrelevant
formals; this is the default.  The third example allows irrelevant
formals, 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-irrelevant-formals-ok flg)

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

SET-LD-KEYWORD-ALIASES    See LD-KEYWORD-ALIASES.

SET-LD-REDEFINITION-ACTION    See LD-REDEFINITION-ACTION.

SET-LD-SKIP-PROOFS    See SET-LD-SKIP-PROOFSP.

SET-LD-SKIP-PROOFSP    See LD-SKIP-PROOFSP.

SET-LET*-ABSTRACTION    See SET-LET*-ABSTRACTIONP.

SET-LET*-ABSTRACTIONP    to shorten many prettyprinted clauses

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.

When this flag is set to t, subterms that occur more than once in a
clause are abstracted away with let*, generally shortening the
displayed size of the clauses.  This flag only affects how clauses are
printed.  It does not change what terms the theorem prover manipulates.

     :set-let*-abstractionp t ;;; or, (set-let*-abstractionp t)

will cause the prettyprinter to do "let* abstraction" on clauses before
they are printed.  The algorithm finds the maximal multiply-occuring
subterm and extracts it, binding it to some new variable and replacing
its occurrences by that variable.  This produces a let* form.  This
process is iterated until no subterm occurs more than once.  This
process generally takes a little time, but less time than to print
large clauses.  The process can greatly reduce the amount of text
produced by the prover.

THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED!  The unabstracted
clauses are manipulated by the theorem prover.

     :set-let*-abstractionp nil

restores normal clause printing.

The mode is stored in the defaults table, See
ACL2-DEFAULTS-TABLE.  Thus, the mode may be set locally in books.

SET-MATCH-FREE-DEFAULT    provide default for :match-free in future rules

     General Forms:
     (set-match-free-default :once)
     (set-match-free-default :all)
     (set-match-free-default nil)

Note: This utility does not apply to type-prescription rules; for a
related topic pertinent to such rules, see
FREE-VARIABLES-TYPE-PRESCRIPTION.

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving that hypothesis, as a basis for
relieving subsequent hypotheses.  This directing of :all or :once is
generally provided by specifying either :match-free :once or
:match-free :all in the :rule-classes of the rule.  If neither of these
is specified, then the most recent set-match-free-default is used by
ACL2 to fill in this missing :match-free field.  See
RULE-CLASSES.  Except: If the last set-match-free-default specifies
nil, then ACL2 reverts to the behavior it had at start-up, as described
in Remarks (2) and (3) below.

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
uses the acl2-defaults-table, and hence its effect is local to the book
or encapsulate form in which it occurs.

Remarks.

(1) The use of set-match-free-default has no effect on existing rules.
In order to change the behavior of existing rules with respect to
free-variable matching, see ADD-MATCH-FREE-OVERRIDE.

(2) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting was previously
specified with set-match-free-default or the default setting is nil,
and the rule is not within a book being processed with include-book,
certify-book, or rebuild, then a warning or error is caused.  In order
to make this an error instead of a warning, see
SET-MATCH-FREE-ERROR.

(3) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting has been
previously specified with set-match-free-default or the default setting
is nil, and no error is caused (see (2) above), then the default :all
is used.

SET-MATCH-FREE-ERROR    control error vs. warning when :match-free is missing

     Legal Forms:
     (set-match-free-error nil)
     :set-match-free-error nil
     (set-match-free-error t)
     :set-match-free-error t

As described elsewhere (see FREE-VARIABLES), when a rewrite,
linear, or forward-chaining rule has free variables in its hypotheses,
the user can specify whether to try all bindings (":all") or just the
first (":once") when relieving its hypotheses, as a basis for relieving
subsequent hypotheses.  This direction of :all or :once is generally
provided by specifying either :match-free :once or :match-free :all in
the :rule-classes of the rule.

But suppose that neither of these is specified for such a rule.  (Note:
set-match-free-error is not relevant for type-prescription rules.)
Also suppose that set-match-free-default has not specified a default of
:once or :all (see SET-MATCH-FREE-DEFAULT).  In this case a
warning will occur except when in the context of include-book.  If you
prefer to see an error in such cases, except in the context of
certify-book, execute (set-match-free-error t).  If there is no error,
then a default of :all is used.

Note: This is NOT an event!  Instead, set-match-free-error sets the
state global 'match-free-error (see STATE and see
ASSIGN).  Thus, this form cannot be put into a book.  If you are
tempted to put it into a book, consider the fact that it really isn't
needed there, since the absence of :match-free does not cause an error
in the context of certify-book or include-book.  If you still feel the
need for such a form, consider using set-match-free-default to provide
a default, at least within the scope of the current book (if any); see
SET-MATCH-FREE-DEFAULT.

SET-MEASURE-FUNCTION    set the default measure function symbol

     Examples:
     (set-measure-function nqthm::count)

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-measure-function name)

where name is a function symbol of one argument.  This macro is
equivalent to (table acl2-defaults-table :measure-function 'name), and
hence is local to any books and encapsulate events in which it occurs;
see ACL2-DEFAULTS-TABLE.  Although this is thus an event (see
TABLE), nevertheless no output results from a
set-measure-function event.

This event sets the default measure function to name.  Subsequently, if
a recursively defined function is submitted to defun with no explicitly
given :measure argument, defun "guesses" the measure (name var), where
name is the then current default measure function and var is the first
formal found to be tested along every branch and changed in every
recursive call.

Note that if (table acl2-defaults-table :measure-function 'name) has its
default value of nil, then the default measure function is acl2-count.

SET-NON-LINEAR    See SET-NON-LINEARP.

SET-NON-LINEARP    to turn on or off non-linear arithmetic reasoning

     Examples:
     (set-non-linearp t)
     (set-non-linearp nil)

See NON-LINEAR-ARITHMETIC.   This event is equivalent to (table
acl2-defaults-table :non-linearp <t-or-nil>), and hence is local to any
books and encapsulate events in which it occurs; see
ACL2-DEFAULTS-TABLE.

The initial value is nil.

SET-NU-REWRITER-MODE    to turn on and off the nu-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.

This event sets a flag that controls whether the ACL2 rewriter uses the
special-purpose nth/update-nth rewriter (nu-rewriter).  The flag may
have one of three values: nil, t, or :literals.

     :set-nu-rewriter-mode nil        ; do not use nu-rewriter
     :set-nu-rewriter-mode t          ; use nu-rewriter in rewriting
     :set-nu-rewriter-mode :literals  ; use nu-rewriter in rewriting after
                                      ;  a pre-pass through every literal
     (set-nu-rewriter-mode :literals) ; same as above

The value nil prevents the use of the nu-rewriter.  The other two
values allow the use of the nu-rewriter.

When the flag is non-nil and the rewriter encounters a term that
"begins with an nth", the nu-rewriter is applied.  By "begins with an
nth" here we mean either the term is an application of nth or is an
application of some nonrecursive function or lambda expression whose
body contains an expression that begins with an nth.

Note that the use of the nu-rewriter here described above is driven by
the rewriter, i.e., the nu-rewriter is applied only to terms visited by
the rewriter in its inside-out sweep.  When the flag is set to
:literals the system makes a pre-pass through every goal clause and
applies the nu-rewriter to every subterm.  The rewriter is then used on
the output of that pre-pass.

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.

We expect to write more documentation as we gain experience with the
nu-rewriter.

SET-OVERRIDE-HINTS    set the override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to set them.  Note that the effects of set-override-hints
events are local to the books or encapsulate events in which they
reside; see SET-OVERRIDE-HINTS! to avoid that restriction.  Also
see ADD-OVERRIDE-HINTS to add to the list of override-hints,
rather than setting a new list and ignoring the present list.

     General Form:
     (set-override-hints form)

where form evaluates to a list of computed hint forms.  The effect of
this event is to set the list of override-hints to the result of that
evaluation.

SET-OVERRIDE-HINTS!    set the override-hints non-locally

Set-override-hints! is the same as set-override-hints, except that the
former is not local to books or encapsulate events in which it occurs.
See SET-OVERRIDE-HINTS; also see ADD-OVERRIDE-HINTS.

SET-PARALLEL-EXECUTION    for ACL2(p): enabling parallel execution for four parallelism primitives

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.  See
PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel execution in ACL2.

     General Forms:
     (set-parallel-execution nil) ; default for images not built for parallelism
     (set-parallel-execution t)   ; default for images built for parallelism
     (set-parallel-execution :bogus-parallelism-ok)

Set-parallel-execution takes an argument that specifies the enabling or
disabling of parallel execution for the primitives pand, por, plet, and
pargs (but not spec-mv-let, whose parallel execution remains enabled).
However, without using top-level, calls of parallelism primitives made
explicitly in the ACL2 top-level loop, as opposed to inside function
bodies, will never cause parallel execution; see
PARALLELISM-AT-THE-TOP-LEVEL.  Parallel execution is determined by
the value of the argument to set-parallel-execution, as follows.

Value t:
All parallelism primitives used in bodies of function definitions are
given the opportunity to execute in parallel.  However, the use of
parallelism primitives directly in the ACL2 top-level loop causes an
error.

Value :bogus-parallelism-ok:
Parallel execution is enabled, as for value t.  However, the use of
parallelism primitives directly in the ACL2 top-level loop does not
cause an error, but rather, simply results in serial execution for
these primitives.

Value nil:
All parallelism primitives degrade to their serial equivalents,
including their calls made directly in the ACL2 top-level loop.  Thus,
uses of parallelism primitives do not in themselves cause errors.

SET-PRINT-CLAUSE-IDS    cause subgoal numbers to be printed when 'prove output is inhibited

     General Forms:
     (set-print-clause-ids t)
     :set-print-clause-ids t
     (set-print-clause-ids nil)
     :set-print-clause-ids nil

This command affects output from the theorem prover only when 'prove
output is inhibited (see SET-INHIBIT-OUTPUT-LST) or gag-mode is
on (but in that case the :goals setting issues this command
automatically; see SET-GAG-MODE).  Calling this macro with
value t as shown above will cause subsequent proof attempts with 'prove
output inhibited to print the subgoal number, so that you can see the
progress of the proof; value nil reverts to the default behavior, where
this is not the case.  On a related note, we point out that you can
cause output to be saved for later display; see PSO and see
PSO!.

If 'prove output is inhibited or gag-mode is on, and if you issue
(set-print-clause-ids t) (either explicitly or with (set-gag-mode
:goals)), then you can restrict when subgoal numbers are printed.  In
the following example we restrict to subgoals that are no more than
four inductions deep, no more than four casesplits deep, and no more
than four single-subgoals deep.  For additional relevant explanation,
see CLAUSE-IDENTIFIER and see DEFATTACH.

     (defun print-clause-id-okp-level-4 (cl-id)
       (declare (xargs :mode :logic :guard (clause-id-p cl-id)))
       (and (<= (length (access clause-id cl-id :pool-lst))
                4)
            (<= (length (access clause-id cl-id :case-lst))
                4)
            (<= (access clause-id cl-id :primes)
                4)))

     (defattach print-clause-id-okp print-clause-id-okp-level-4)