This is documentation for ACL2 Version 3.6
Copyright (C) 2009  University of Texas at Austin

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

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

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

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

THEORY-INVARIANT    user-specified invariants on theories

     Examples:
     (theory-invariant (not (and (active-runep '(:rewrite left-to-right))
                                 (active-runep '(:rewrite right-to-left))))
                       :key my-invariant
                       :error nil)

     ; Equivalent to the above:
     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left))
                       :key my-invariant
                       :error nil)

     General Form:
     (theory-invariant term &key key error)

where:

     o term is a term that uses no variables other than ens and state;

     o key is an arbitrary "name" for this invariant (if omitted, an
     integer is generated and used); and

     o :error specifies the action to be taken when an invariant is
     violated -- either nil if a warning is to be printed, else t (the
     default) if an error is to be caused.

Theory-invariant is an event that adds to or modifies the table of
user-supplied theory invariants that are checked each time a theory
expression is evaluated.

The theory invariant mechanism is provided via a table (see
TABLE) named theory-invariant-table.  In fact, the theory-invariant
"event" is just a macro that expands into a use of the table event.
More general access to the theory-invariant table is provided by table
itself.  For example, the table can be inspected or cleared with table;
you can clear an individual theory invariant by setting the invariant
to t, or eliminate all theory invariants with the command (table
theory-invariant-table nil nil :clear).

Theory-invariant-table maps arbitrary keys to records containing terms
that mention, at most, the variables ens and state.  Every time an
alleged theory expression is evaluated, e.g., in the in-theory event or
:in-theory hint, each of the terms in theory-invariant-table is
evaluated with ens bound to a so-called "enabled structure" obtained
from the theory expression and state bound to the current ACL2 state
(see STATE).  Users generally need not know about the enabled
structure, other than that it can be accessed using the macros
active-runep and incompatible; see ACTIVE-RUNEP and see
INCOMPATIBLE.  If the result is nil, a message is printed and an
error occurs (except, only a warning occurs if :error nil is
specified).  Thus, the table can be thought of as a list of conjuncts.
Each term in the table has a "name," which is just the key under which
the term is stored.  When a theory violates the restrictions specified
by some term, both the name and the term are printed.  By calling
theory-invariant with a new term but the same name, you can overwrite
that conjunct of the theory invariant; but see the Local Redefinition
Caveat at the end of this note.  You may want to avoid using explicit
names, since otherwise the subsequent inclusion of another book that
defines a theory invariant with the same name will override your theory
invariant.

Theory invariants are particularly useful in the context of large rule
sets intended for re-use.  Such sets often contain conflicting rules,
e.g., rules that are to be enabled when certain function symbols are
disabled, rules that rewrite in opposite directions and thus loop if
simultaneously enabled, groups of rules which should be enabled in
concert, etc.  The developer of such rule sets understands these
restrictions and probably documents them.  The theory invariant
mechanism allows the developer to codify his restrictions so that the
user is alerted when they are violated.

Since theory invariants are arbitrary terms, macros may be used to
express commonly used restrictions.  For example, executing the event

     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left)))

would subsequently cause an error any time the current theory contained
both of the two runes shown.  Of course, incompatible is just defined as
a macro.  Its definition may be inspected with :pe incompatible.

In order for a theory-invariant event to be accepted, the proposed
theory invariant must be satisfied by the current theory (see
CURRENT-THEORY).  The value returned upon successful execution of the
event is the key (whether user-supplied or generated).

Local Redefinition Caveat.  Care needs to be taken when redefining a
theory invariant in a local context.  Consider the following example.

     (theory-invariant
      (active-runep '(:definition binary-append))
      :key app-inv)

     (encapsulate
      ()
      (local (theory-invariant t :key app-inv))
      (in-theory (disable binary-append))
      (defthm ...))

The second pass of the encapsulate will fail, because the in-theory
event violates the original theory-invariant and the local
theory-invariant is skipped in the second pass of the encapsulate.  Of
course, local theory-invariants in books can cause the analogous
problem in the second (include-book) pass of a certify-book.  In both
cases, though, the theory invariants are only checked at the conclusion
of the (include-book or encapsulate) event.  Indeed, theory invariants
are checked at the end of every event related to theories, including
defun, defthm, in-theory, encapsulate, and include-book, except for
events executed on behalf of an include-book or the second pass of an
encapsulate.

UNMEMOIZE    turn off memoization for the specified function

     Example:
     (unmemoize 'foo) ; turn off memoization of foo

     General Form:
     (unmemoize fn)

where fn evaluates to a function symbol that is currently memoized; see
MEMOIZE.  An exception is that as with memoize, fn may evaluate
to the name of a macro that is associated with such a function symbol;
see MACRO-ALIASES-TABLE.

Calls of this macro generate events of the form (table memoize-table fn
nil).  When successful, the returned value is of the form (mv nil
function-symbol state).

VALUE-TRIPLE    compute a value, optionally checking that it is not nil

     Examples:
     (value-triple (+ 3 4))
     (value-triple (cw "hi") :on-skip-proofs t)
     (value-triple (@ ld-pre-eval-print))
     (value-triple (@ ld-pre-eval-print) :check t)

     General Form:
     (value-triple form
                   :on-skip-proofs sp ; optional; nil by default
                   :check chk         ; optional; nil by default
                   )

Value-triple provides a convenient way to evaluate a form in an event
context, including progn and encapsulate and in books; see
EVENTS.  The form should evaluate to a single, non-stobj value.

Calls of value-triple are generally skipped when proofs are being
skipped, in particular when ACL2 is performing the second pass through
the events of an encapsulate form or during an include-book, or indeed
any time ld-skip-proofsp is non-nil.  If you want the call evaluated
during those times as well, use a non-nil value for :on-skip-proofs.
Note that the argument to :on-skip-proofs is not evaluated.

If you expect the form to evaluate to a non-nil value and you want an
error to occur when that is not the case, you can use :check t.  More
generally, the argument of :check can be a form that evaluates to a
single, non-stobj value.  If this value is not nil, then the
aforementioned test is made (that the given form is not nil).  If an
error occurs and the value of :check is a string or indeed any
"message" suitable for printing by fmt when supplied as a value for
tilde-directive ~@, then that string or message is printed.

VERIFY-GUARDS    verify the guards of a function

     Examples:
     (verify-guards flatten)
     (verify-guards flatten
                    :hints (("Goal" :use (:instance assoc-of-app)))
                    :otf-flg t
                    :guard-debug t ; default = nil
                    :doc "string")

     General Form:
     (verify-guards name
             :hints        hints
             :otf-flg      otf-flg
             :guard-debug  t ; typically t, but any value is legal
             :doc          doc-string)

See GUARD for a general discussion of guards.  In the General
Form above, name is the name of a :logic function (see
DEFUN-MODE) or of a theorem or axiom.  In the most common case name
is the name of a function that has not yet had its guards verified,
each subroutine of which has had its guards verified. hints, otf-flg,
and guard-debug are as described in the corresponding documentation
entries; and doc-string, if supplied, is a string *not* beginning with
":Doc-Section".  The four keyword arguments above are all optional.
Verify-guards will attempt to prove that the guard on the named
function implies the guards of all of the subroutines called in the
body of the function, and that the guards are satisfied for all function
calls in the guard itself (under an implicit guard of t).  If
successful, name is considered to have had its guards verified.

See VERIFY-GUARDS-FORMULA for a utility that lets you view the
formula to be proved by verify-guards, but without creating an event.

If name is one of several functions in a mutually recursive clique,
verify-guards will attempt to verify the guards of all of the functions.

If name is a theorem or axiom name, verify-guards verifies the guards
of the associated formula.  When a theorem has had its guards verified
then you know that the theorem will evaluate to non-nil in all Common
Lisps, without causing a runtime error (other than possibly a resource
error).  In particular, you know that the theorem's validity does not
depend upon ACL2's arbitrary completion of the domains of partial
Common Lisp functions.

For example, if app is defined as

     (defun app (x y)
       (declare (xargs :guard (true-listp x)))
       (if (endp x)
           y
           (cons (car x) (app (cdr x) y))))

then we can verify the guards of app and we can prove the theorem:

     (defthm assoc-of-app
       (equal (app (app a b) c) (app a (app b c))))

However, if you go into almost any Common Lisp in which app is defined
as shown and evaluate

     (equal (app (app 1 2) 3) (app 1 (app 2 3)))

we get an error or, perhaps, something worse like nil!  How can this
happen since the formula is an instance of a theorem?  It is supposed
to be true!

It happens because the theorem exploits the fact that ACL2 has completed
the domains of the partially defined Common Lisp functions like car and
cdr, defining them to be nil on all non-conses.  The formula above
violates the guards on app.  It is therefore "unreasonable" to expect
it to be valid in Common Lisp.

But the following formula is valid in Common Lisp:

     (if (and (true-listp a)
              (true-listp b))
         (equal (app (app a b) c) (app a (app b c)))
         t)

That is, no matter what the values of a, b and c the formula above
evaluates to t in all Common Lisps (unless the Lisp engine runs out of
memory or stack computing it).  Furthermore the above formula is a
theorem:

     (defthm guarded-assoc-of-app
       (if (and (true-listp a)
                (true-listp b))
           (equal (app (app a b) c) (app a (app b c)))
           t))

This formula, guarded-assoc-of-app, is very easy to prove from
assoc-of-app.  So why prove it?  The interesting thing about
guarded-assoc-of-app is that we can verify the guards of the formula.
That is, (verify-guards guarded-assoc-of-app) succeeds.  Note that it
has to prove that if a and b are true lists then so is (app a b) to
establish that the guard on the outermost app on the left is satisfied.
By verifying the guards of the theorem we know it will evaluate to
true in all Common Lisps.  Put another way, we know that the validity
of the formula does not depend on ACL2's completion of the partial
functions or that the formula is "well-typed."

One last complication:  The careful reader might have thought we could
state guarded-assoc-of-app as

     (implies (and (true-listp a)
                   (true-listp b))
              (equal (app (app a b) c)
                     (app a (app b c))))

rather than using the if form of the theorem.  We cannot!  The reason
is technical:  implies is defined as a function in ACL2.  When it is
called, both arguments are evaluated and then the obvious truth table
is checked.  That is, implies is not "lazy."  Hence, when we write the
guarded theorem in the implies form we have to prove the guards on the
conclusion without knowing that the hypothesis is true.  It would have
been better had we defined implies as a macro that expanded to the if
form, making it lazy.  But we did not and after we introduced guards we
did not want to make such a basic change.

Recall however that verify-guards is almost always used to verify the
guards on a function definition rather than a theorem.  We now return
to that discussion.

Because name is not uniquely associated with the verify-guards event
(it necessarily names a previously defined function) the documentation
string, doc-string, is not stored in the documentation data base.
Thus, we actually prohibit doc-string from having the form of an ACL2
documentation string; see DOC-STRING.

If the guard on a function is not t, then guard verification requires
not only consideration of the body under the assumption that the guard
is true, but also consideration of the guard itself.  Thus, for
example, guard verification fails in the following example, even though
there are no proof obligations arising from the body, because the guard
itself can cause a guard violation when evaluated for an arbitrary
value of x:

     (defun foo (x)
       (declare (xargs :guard (car x)))
       x)

Verify-guards must often be used when the value of a recursive call of
a defined function is given as an argument to a subroutine that is
guarded.  An example of such a situation is given below.  Suppose app
(read "append") has a guard requiring its first argument to be a
true-listp.  Consider

     (defun rev (x)
       (declare (xargs :guard (true-listp x)))
       (cond ((endp x) nil)
             (t (app (rev (cdr x)) (list (car x))))))

Observe that the value of a recursive call of rev is being passed into
a guarded subroutine, app.  In order to verify the guards of this
definition we must show that (rev (cdr x)) produces a true-listp, since
that is what the guard of app requires.  How do we know that (rev (cdr
x)) is a true-listp?  The most elegant argument is a two-step one,
appealing to the following two lemmas: (1) When x is a true-listp, (cdr
x) is a true-listp.  (2) When z is a true-listp, (rev z) is a
true-listp.  But the second lemma is a generalized property of rev, the
function we are defining.  This property could not be stated before rev
is defined and so is not known to the theorem prover when rev is
defined.

Therefore, we might break the admission of rev into three steps: define
rev without addressing its guard verification, prove some general
properties about rev, and then verify the guards.  This can be done as
follows:

     (defun rev (x)
       (declare (xargs :guard (true-listp x)
                       :verify-guards nil))    ; Note this additional xarg.
       (cond ((endp x) nil)
             (t (app (rev (cdr x)) (list (car x))))))

     (defthm true-listp-rev
       (implies (true-listp x2)
                (true-listp (rev x2))))

     (verify-guards rev)

The ACL2 system can actually admit the original definition of rev,
verifying the guards as part of the defun event.  The reason is that,
in this particular case, the system's heuristics just happen to hit
upon the lemma true-listp-rev.  But in many more complicated functions
it is necessary for the user to formulate the inductively provable
properties before guard verification is attempted.

*Remark on computation of guard conjectures and evaluation*.  When ACL2
computes the guard conjecture for the body of a function, it evaluates
any ground subexpressions (those with no free variables), for calls of
functions whose :executable-counterpart runes are enabled.  Note that
here, "enabled" refers to the current global theory, not to any :hints
given to the guard verification process; after all, the guard
conjecture is computed even before its initial goal is produced.  Also
note that this evaluation is done in an environment as though
:set-guard-checking :all had been executed, so that we can trust that
this evaluation takes place without guard violations; see
SET-GUARD-CHECKING.

VERIFY-TERMINATION    convert a function from :program mode to :logic mode

     Example:
     (verify-termination fact)

     General Forms:
     (verify-termination fn dcl ... dcl)
     (verify-termination (fn1 dcl ... dcl)
                         (fn2 dcl ... dcl)
                         ...)

where fn and the fni are function symbols having :program mode (see
DEFUN-MODE) and all of the dcls are either declare forms or
documentation strings.  The first form above is an abbreviation for

     (verify-termination (fn dcl ... dcl))

so we limit our discussion to the second form.  Each of the fni must be
in the same clique of mutually recursively defined functions, but not
every function in the clique need be among the fni.

Verify-termination attempts to establish the admissibility of the fni.
Verify-termination retrieves their definitions, creates modified
definitions using the dcls supplied above, and resubmits these
definitions.  You could avoid using verify-termination by typing the new
definitions yourself.  So in that sense, verify-termination adds no new
functionality.  But if you have prototyped your system in :program mode
and tested it, you can use verify-termination to resubmit your
definitions and change their defun-modes to :logic, addings hints
without having to retype or recopy the code.

The defun command executed by verify-termination is obtained by
retrieving the defun (or mutual-recursion) command that introduced the
clique in question and then possibly modifying each definition as
follows.  Consider a function, fn, in the clique.  If fn is not among
the fni above, its definition is left unmodified other than to add
(declare (xargs :mode :logic)).  Otherwise, fn is some fni and we
modify its definition by inserting into it the corresponding dcls listed
with fni in the arguments to verify-termination, as well as (declare
(xargs :mode :logic)).  In addition, we throw out from the old
declarations in fn the :mode specification and anything that is
specified in the new dcls.

For example, suppose that fact was introduced with:

     (defun fact (n)
       (declare (type integer n)
                (xargs :mode :program))
       (if (zp n) 1 (* n (fact (1- n))))).

Suppose later we do (verify-termination fact).  Then the following
definition is submitted.

     (defun fact (n)
       (declare (type integer n))
       (if (zp n) 1 (* n (fact (1- n))))).

Observe that this is the same definition as the original one, except
the old specification of the :mode has been deleted so that the
defun-mode now defaults to :logic.  Although the termination proof
succeeds, ACL2 also tries to verify the guard, because we have
(implicitly) provided a guard, namely (integerp n), for this function.
(See GUARD for a general discussion of guards, and see
TYPE-SPEC for a discussion of how type declarations are used in
guards.)  Unfortunately, the guard verification fails, because the
subterm (zp n) requires that n be nonnegative, as can be seen by
invoking :args zp.  (For a discussion of termination issues relating to
recursion on the naturals, see ZERO-TEST-IDIOMS.)  So we might
be tempted to submit the following:

     (verify-termination
      fact
      (declare (xargs :guard (and (integerp n) (<= 0 n))))).

However, this is considered a changing of the guard (from (integerp n)),
which is illegal.  If we instead change the guard in the earlier defun
after undoing that earlier definition with :ubt fact, then
(verify-termination fact) will succeed.

We conclude with a discussion of the use of make-event to implement
verify-termination.  This discussion can be skipped; we include it only
for the curious.

Consider the following proof of nil, which succeeded up through
Version_3.4 of ACL2.

     (encapsulate
      ()
      (defun foo (x y)
        (declare (xargs :mode :program))
        (if (or (zp x) (zp y))
            (list x y)
          (foo (1+ x) (1- y))))
      (local (defun foo (x y)
               (declare (xargs :measure (acl2-count y)))
               (if (or (zp x) (zp y))
                   (list x y)
                 (foo (1+ x) (1- y)))))
      (verify-termination foo))

     (defthm bad-lemma
       (zp x)
       :hints (("Goal" :induct (foo x 1)))
       :rule-classes nil)

How did this work?  In the first pass of the encapsulate, the second
defun of foo promoted foo from :program to :logic mode, with y as the
unique measured variable.  The following call to verify-termination was
then redundant.  However, on the second pass of the encapsulate, the
second (local) definition of foo was skipped, and the
verify-termination event then used the first definition of foo to guess
the measure, based (as with all guesses of measures) on a purely
syntactic criterion.  ACL2 incorrectly chose (acl2-count x) as the
measure, installing x as the unique measured variable, which in turn led
to an unsound induction scheme subsequently used to prove nil (lemma
bad-lemma, above)

Now, verify-termination is a macro whose calls expand to make-event
calls.  So in the first pass above, the verify-termination call
generated a defun event identical to the local defun of foo, which was
correctly identified as redundant.  That expansion was recorded, and on
the second pass of the encapsulate, the expansion was recalled and used
in place of the verify-termination call (that is how make-event works).
So instead of a measure being guessed for the verify-termination call
on the second pass, the same measure was used as was used on the first
pass, and a sound induction scheme was stored.  The attempt to prove nil
(lemma bad-lemma) then failed.

HISTORY    functions that display or change history

ACL2 keeps track of the commands that you have executed that have
extended the logic or the rule data base, as by the definition of
macros, functions, etc.  Using the facilities in this section you can
review the sequence of commands executed so far.  For example, you can
ask to see the most recently executed command, or the command 10 before
that, or the command that introduced a given function symbol.  You can
also undo back through some previous command, restoring the logical
world to what it was before the given command.

The annotations printed in the margin in response to some of these
commands (such as `P', `L', and `V') are explained in the documentation
for :pc.

Several technical terms are used in the documentation of the history
commands.  You must understand these terms to use the commands.  These
terms are documented via :doc entries of their own.  See
COMMAND, see EVENTS, see COMMAND-DESCRIPTOR, and see
LOGICAL-NAME.

OOPS    undo a :u or :ubt

The keyword command :oops will undo the most recent :ubt (or :u, which
we here consider just another :ubt).  A second :oops will undo the next
most recent :ubt, a third will undo the :ubt before that one, and a
fourth :oops will return the logical world to its configuration before
the first :oops.

Consider the logical world (see WORLD) that represents the
current extension of the logic and ACL2's rules for dealing with it.
The :ubt and :u commands "roll back" to some previous world (see
UBT).  Sometimes these commands are used to inadvertently undo useful
work and user's wish they could "undo the last undo."  That is the
function provided by :oops.

:Oops is best described in terms of an implementation.  Imagine a ring
of four worlds and a marker (*) indicating the current ACL2 world:

                  *
                w0
              /    \
            w3      w1
              \    /
                w2

This is called the "kill ring" and it is maintained as follows.  When
you execute an event the current world is extended and the kill ring is
not otherwise affected.  When you execute :ubt or :u, the current world
marker is moved one step counterclockwise and that world in the ring is
replaced by the result, say w0', of the :ubt or :u.

                w0
              /    \
           *w0'     w1
              \    /
                w2

If you were to execute events at this point, w0' would be extended and
no other changes would occur in the kill ring.

When you execute :oops, the marker is moved one step clockwise.  Thus
the kill ring becomes

                  *
                w0
              /    \
            w0'     w1
              \    /
                w2

and the current ACL2 world is w0 once again.  That is, :oops "undoes"
the :ubt that produced w0' from w0.  Similarly, a second :oops will
move the marker to w1, undoing the undo that produced w0 from w1.  A
third :oops makes w2 the current world.  Note however that a fourth
:oops restores us to the configuration previously displayed above in
which w0' has the marker.

In general, the kill ring contains the current world and the three most
recent worlds in which a :ubt or :u were done.

While :ubt may appear to discard the information in the events undone,
we can see that the world in which the :ubt occurred is still
available.  No information has been lost about that world.  But :ubt
does discard information!  :Ubt discards the information necessary to
recover from the third most recent ubt!  An :oops, on the other hand,
discards no information, it just selects the next available world on
the kill ring and doing enough :oopses will return you to your starting
point.

We can put this another way.  You can freely type :oops and inspect the
world that you thus obtain with :pe, :pc, and other history commands.
You can repeat this as often as you wish without risking the permanent
loss of any information.  But you must be more careful typing :ubt or
:u.  While :oops makes :ubt seem "safe" because the most recent :ubt
can always be undone, information is lost when you execute :ubt.

We note that :ubt and :u may remove compiled definitions (but note that
in some Lisps, including CCL (OpenMCL) and SBCL, functions are always
compiled).  When the original world is restored using :oops, restored
functions will not generally be compiled (except for Lisps as above),
though the user can remedy this situation; see COMP.

Finally, we note that our implementation of oops can use a significant
amount of memory, because of the saving of old logical worlds.  Most
users are unlikely to experience a memory problem, but if you do, then
you may want to disable oops by evaluting (reset-kill-ring 0 state);
see RESET-KILL-RING.

PBT    print the commands back through a command descriptor

     Examples:
     :pbt :max      ; print back through the most recent command
     :pbt :x        ; print back through the most recent command
     :pbt fn        ; print back through the introduction of fn
     :pbt 5         ; print back through the fifth command executed
     :pbt (:x -4)   ; print back through the most recent five commands

See COMMAND-DESCRIPTOR.

Pbt takes one argument, a command descriptor, and prints the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR for a description of what a command descriptor is.
See PC for a description of the format used to display
commands.  Pbt will print the commands that ubt will undo.

PC    print the command described by a command descriptor

     Examples:
     :pc 3    ; print the third command executed
     :pc :max ; print the most recent command
     :pc :x   ; print the most recent command
     :pc fn   ; print the command that introduced fn

See COMMAND-DESCRIPTOR.

Pc takes one argument, a command descriptor, and prints the command
identified by that descriptor.  See COMMAND-DESCRIPTOR.  For
example

     ACL2 !>:pc foo
      LVd     52 (DEFUN FOO (X) X)

Pc always prints a space first, followed by three (possibly blank)
characters ("LVd" above) explained below.  Then pc prints the command
number, a number uniquely identifying the command's position in the
sequence of commands since the beginning of the user's session.
Finally, the command itself is printed.

While pc always prints a space first, some history commands, for
example :pcs and :pe, use the first column of output to delimit a
region of commands or to point to a particular event within a command.

For example, :pcs 52 54 will print something like

     /LVd     52 (DEFUN FOO (X) X)
      LV      53 (DEFUN BAR (X) (CONS X X))
     \        54 (DEFTHM FOO-BAR (EQUAL (CAR (BAR X)) (FOO X)))
               : ...
             127 (DEFUN LATEST (X) X)

Here, the two slash characters in the first column are intended to
suggest a bracket delimiting commands 52 through 54.  The last command
printed by pcs is always the most recent command, i.e., the command at
:here, and is separated from the rest of the display by an elipsis if
some commands are omitted.

Similarly, the :pe command will print a particular event within a
command block and will indicate that event by printing a ">" in the
first column.  The symbol is intended to be an arrow pointing at the
event in question.

For example, :pe true-listp-app might print:

              1 (INCLUDE-BOOK "list-book")
                 \
     >           (DEFTHM TRUE-LISTP-APP
                         (EQUAL (TRUE-LISTP (APP A B)) (TRUE-LISTP B)))

using the arrow to indicate the event itself.  The slash printed to
connect the command, include-book, with the event, defthm, is intended
to suggest a tree branch indicating that the event is inferior to (and
part of) the command.

The mysterious three characters sometimes preceding a command have the
following interpretations.  The first two have to do with the function
symbols introduced by the command and are blank if no symbols were
introduced.

At any time we can classify our function symbols into three disjoint
sets, which we will here name with characters.  The "P" functions are
those in :program mode.  The "L" functions are those in :logic mode
whose guards have not been verified.  The "V" functions are those in
:logic mode whose guards have been verified.  Note that
verify-termination and verify-guards cause function symbols to be
reclassified.  If a command introduces function symbols then the first
mysterious character indicates the class of the symbols at the time of
introduction and the second character indicates the current class of
the symbols (if the current class is different from the introductory
class).

Thus, the display

      PLd     52 (DEFUN FOO (X) X)

tells us that command 52 introduced a :program function but that some
command after 52 changed its mode to :logic and that the guards of foo
have not been verified.  That is, foo's termination has been verified
even though it was not verified as part of the command that introduced
foo.  Had a subsequent command verified the guards of foo, the display
would contain a V where the L is.

The display

      P d     52 (DEFUN FOO (X) X)

indicates that foo was introduced in :program mode and still is in that
mode.

The third character indicates the enabled/disabled status of the runes
introduced by the command.  If the status character is blank then all
the runes (if any) introduced are enabled.  If the status character is
"D" then some runes were introduced and they are all disabled.  If the
status character is "d" then at least one, but not all, of the runes
introduced is disabled.  Thus, in the display

      L d     52 (DEFUN FOO (X) X)

we see that some rune introduced by command 52 is disabled.  As noted
in the documentation for rune, a defun command introduces many runes,
e.g., the axiomatic definition rule, (:definition fn), the executable
counterpart rule, (:executable-counterpart fn), and type-prescriptions,
(:type-prescription fn).  The display above does not say which of the
runes based on foo is disabled, but it does tell us one of them is; see
DISABLEDP for how to obtain the disabled runes for a given
function symbol.

PCB    print the command block described by a command descriptor

     Examples:
     :pcb :max ; print the most recent command block
     :pcb :x   ; print the most recent command block
     :pcb fn   ; print the command block that introduced fn
     :pcb 5    ; print the fifth command block

See COMMAND-DESCRIPTOR.

Pcb takes one argument, a command descriptor, and prints the command
block of the command described.  See COMMAND-DESCRIPTOR for
details of command descriptors.  See PC for description of the
format in which commands are displayed.  The command block of a command
consists of the command itself and all of the events it created.  If
the command created a single event and that event is in fact the
command (i.e., if the command typed was just an event such as a defun
or defthm rather than a macro that expanded to some event forms), then
pcb just prints the command.  Pcb sketches command and all of the
events it created, rather than printing them fully.  If you wish to see
just the command, in its entirety, use pc.  If you wish to see one of
the events within the block, in its entirety, use pe.  If you wish to
see the command sketched and all of the events it created, in their
entirety, use pcb!.

PCB!    print in full the command block described by a command descriptor

     Examples:
     :pcb! :max ; print the most recent command block
     :pcb! :x   ; print the most recent command block
     :pcb! fn   ; print the command block that introduced fn
     :pcb! 5    ; print the fifth command block

See COMMAND-DESCRIPTOR.

Pcb! takes one argument, a command descriptor, and prints the command
block of the command described.  Unlike pcb, pcb! prints the event
forms in full; see PCB for details.

PCS    print the sequence of commands between two command descriptors

     Examples:
     :pcs 1 5              ; print commands 1 through 5
     :pcs 5 1              ; same as above
     :pcs :x (:x -3)       ; print the 3 most recently executed commands
     :pcs fn assoc-of-fn   ; print the commands between the one that introduced
                           ; fn and the one that introduced assoc-of-fn

Pcs takes two arguments, both of which are command descriptors, and
prints the commands between them with pc.  The order of the two
descriptors is irrelevant.  See COMMAND-DESCRIPTOR for a
description of command descriptors.  See PC for a description
of the format in which commands are displayed.

PE    print the events named by a logical name

     Example:
     :pe fn   ; sketches the command that introduced fn and
              ; prints in full the event within it that created fn.

See LOGICAL-NAME.

Pe takes one argument, a logical name, and prints in full the event
corresponding to the name.  Pe also sketches the command responsible
for that event if the command is different from the event itself.  See
PC for a description of the format used to display a command.
To remind you that the event is inferior to the command, i.e., you can
only undo the entire command, not just the event, the event is indented
slightly from the command and a slash (meant to suggest a tree branch)
connects them.

If the given logical name corresponds to more than one event, then :pe
will print the above information for every such event.  Here is an
example of such behavior.

     ACL2 !>:pe nth
           -4270  (ENCAPSULATE NIL ...)
                  \
     >V            (VERIFY-TERMINATION NTH)

     Additional events for the logical name NTH:
      PV   -4949  (DEFUN NTH (N L)
                         "Documentation available via :doc"
                         (DECLARE (XARGS :GUARD (AND (INTEGERP N)
                                                     (>= N 0)
                                                     (TRUE-LISTP L))))
                         (IF (ENDP L)
                             NIL
                             (IF (ZP N)
                                 (CAR L)
                                 (NTH (- N 1) (CDR L)))))
     ACL2 !>

If you prefer to see only the formula for the given name, for example
if it is part of a large mutual-recursion, see PF.

PE!    deprecated (see PE)

Please see PE.  :Pe now has the functionality formerly provided
by :pe!.

PF    print the formula corresponding to the given name

     Examples:
     :pf (:definition fn) ; prints the definition of fn as an equality
     :pf fn               ; same as above

     :pf (:rewrite foo)   ; prints the statement of the rewrite rule foo
     :pf foo              ; same as above

pf takes one argument, an event name or a rune, and prints the formula
associated with name.  If the argument is the name of a macro
associated with a function name by macro-aliases-table, then the
function name is used as the argument.

PL    print the rules for the given name or term

     Examples:
     :pl foo     ; prints rules that rewrite some call of foo
     :pl (+ x y) ; prints rules that rewrite (+ x y)

Pl takes one argument, which should be a symbol or a term.  If the
argument is a function symbol (or a macro corresponding to a function;
see MACRO-ALIASES-TABLE), :pl displays the :rewrite,
:definition, and :meta rules that rewrite some term whose top function
symbol is the one specified.  Otherwise, :pl displays the :rewrite and
:definition rules that rewrite the specified term, followed by the
applicable :meta rules.  For :rewrite and :definition rules, :pl also
shows the substitution that, when applied to the left-hand side of the
rule, yields the specified term.  For :meta rules, only those are
displayed that meet two conditions: the application of the metafunction
returns a term different from the input term, and if there is a
hypothesis metafunction then it also returns a term.  (A subtlety: In
the case of extended metafunctions (see
EXTENDED-METAFUNCTIONS), a trivial metafunction context is used for
the application of the metafunction.)

The kinds of rules printed by :pl are :rewrite rules, :definition
rules, and meta rules (not, for example, :forward-chaining rules).  If
you want to see all :clause-processor rules, issue the command
:print-clause-processor-rules, and for trusted clause-processors,
(table trusted-clause-processor-table); see CLAUSE-PROCESSOR and
see DEFINE-TRUSTED-CLAUSE-PROCESSOR.

PR    print the rules stored by the event with the given name

     Examples:

     :pr fn ; prints the rules from the definition of fn (including any
            ; :type-prescription rule and :definition rule)

     :pr assoc-append ; if assoc-append is a rewrite rule, prints that rule

Also see PR!, which is similar but works at the command level
instead of at the event level, and see PL, which displays all
rewrite rules for calls of fn, not just those introduced at definition
time.

Pr takes one argument, a logical name, and prints the rules associated
with it.  In each case it prints the rune, the current enabled/disabled
status, and other appropriate fields from the rule.  It may be helpful
to read the documentation for various kinds of rules in order to
understand the information printed by this command.  For example, the
information printed for a linear rule might be:

       Rune:     (:LINEAR ABC)
       Status:   Enabled
       Hyps:     ((CONSP X))
       Concl:    (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
       Max-term: (ACL2-COUNT (CAR X))
       Backchain-limit-lst:    (3)

The hyps and concl fields for this rule are fairly self-explanatory,
but it is useful to see LINEAR to learn about maximal terms
(which, as one might guess, are stored under "Max-term").

Currently, this function does not print congruence rules or equivalence
rules.

The expert user might also wish to use find-rules-of-rune.  See
FIND-RULES-OF-RUNE.

PR!    print rules stored by the command with a given command descriptor

     Examples:

     :pr! fn ; prints the rules from the definition of fn (including any
             ; :type-prescription rule and :definition rule), as well as all other
             ; rules created by the command that created by fn (which could be
             ; many rules if, for example, fn was defined by an include-book
             ; command).

     :pr! :max ; prints all the rules stored by the most recent command

Also see PR, which is similar but works at the event level
instead of at the command level.

Pr takes one argument, a command descriptor, and prints the rules
created by the corresponding event.  In each case it prints the rune,
the current enabled/disabled status, and other appropriate fields from
the rule.  See PR for further details.

PUFF    replace a compound command by its immediate subevents

     Example Forms:
     ACL2 !>:puff :max
     ACL2 !>:puff :x
     ACL2 !>:puff 15
     ACL2 !>:puff "book"

     General Form:
     :puff cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command (see below).  Puff replaces the command at cd by the
immediate subevents of the command, executed as commands.  Puff then
prints, using pcs, the puffed region.

We consider puff to be a sort of hack; it is generally robust and sound,
but that is not guaranteed.  If any existing ACL2 event resulted from
puff, ACL2 considers proofs to have been skipped, and thus certify-book
is disallowed until such events have been undone (see UBT).

A "puffable" command is an encapsulate command, an include-book
command, or any command other than those consisting of a single
primitive event.  For example, since defun is a primitive event, a
defun command is not puffable.  But a macro form that expands into
several defun events is puffable.  The only primitive event commands
that are puffable are encapsulate and include-book commands.  A
puffable command contains (interesting) subevents, namely, the events
in the body of the encapsulate, in the file of the book included, or in
the command block.

(Obscure exceptions.  (1) An encapsulate command generated by the macro
define-trusted-clause-processor is not puffable.  (2) If a use of
make-event results in local events in the scope of an encapsulate or
include-book event within a command, then an attempt to puff that
command will result in an error, leaving the world unchanged, if any
such local event was necessary to support other events in the command.
(3) An include-book command may fail for a book that has been modified,
as describe late in this documentation topic.)

The puff command "lifts" the immediate subevents of the indicated
command so that they become commands themselves.  The command puff*
recursively puffs the newly introduced commands.  See PUFF*,
which also gives an example illustrating both puff and puff*.  Puff
undoes the command at cd and replaces it by its immediate subevents.
Thus, in general the length of the history grows when a puff command is
executed.  If puff causes an error (see below), the logical world
remains unchanged from its initial configuration.

The intended use of puff is to allow the user access to the events
"hidden" inside compound commands.  For example, while trying to prove
some theorem, p, about a constrained function, fn, one might find that
the encapsulate, cd, that introduced fn failed to include an important
constraint, q.  Without puff, the only way to proceed is to undo back
through cd, create a suitable encapsulate that proves and exports q as
well as the old constraints, re-execute the new encapsulate, re-execute
the events since cd, and then try p again.  Unfortunately, it may be
hard to prove q and additional events may have to be inserted into the
encapsulate to prove it.  It may also be hard to formulate the "right"
q, i.e., one that is provable in the encapsulate and provides the
appropriate facts for use in the proof of p.

Using puff, the user can erase the encapsulate at cd, replacing it by
the events in its body.  Now the formerly constrained function, fn, is
defined as its witness.  The user can experiment with formulations and
proofs of q suitable for p.  Of course, to get into the ultimately
desired state -- where fn is constrained rather than defined and q is
exported by an encapsulate at cd -- the user must ultimately undo back
to cd and carry out the more tedious program described above.  But by
using puff it is easier to experiment.

Similar applications of puff allow the user of a book to expose the
innards of the book as though they had all be typed as commands.  The
user might then "partially undo" the book, keeping only some of the
events in it.

Puff operates as follows.  First, it determines the list of immediate
subevents of the command indicated by cd.  It causes an error if there
is only one subevent and that subevent is identical to the command --
i.e., if the command at cd is a primitive.  Next, puff undoes back
through the indicated command.  This not only erases the command at cd
but all the commands executed after it.  Finally, puff re-executes the
subevents of (the now erased) cd followed by all the commands that were
executed afterwards.

Observe that the commands executed after cd will generally have higher
command numbers than they did before the puff.  For example, suppose
100 commands have been executed and that :puff 80 is then executed.
Suppose command 80 contains 5 immediate subevents (i.e., is an
encapsulation of five events).  Then, after puffing, command 80 is the
first event of the puffed command, command 81 is the second, and so on;
104 commands appear to have been executed.

When puffing an encapsulate or include-book, the local commands are
executed.  Note that this will replace constrained functions by their
witnesses.

Finally, it is impossible to puff in the presence of include-book
commands involving certified files that have been altered since they
were included.  To be specific, suppose "arith" is a certified book
that has been included in a session.  Suppose that after "arith" was
included, the source file is modified.  (This might happen if the user
of "arith" is not its author and the author happens to be working on a
new version of "arith" during the same time period.)  Now suppose the
user tries to puff the command that included "arith".  The attempt to
obtain the subevents in "arith" will discover that the check sum of
"arith" has changed and an error will be caused.  No change is made in
the logical world.  A similar error is caused if, in this same
situation, the user tries to puff any command that occurred before the
inclusion of "arith"!  That is, puff may cause an error and leave the
world unchanged even if the command puffed is not one involving the
modified book.  This happens because in order to reconstruct the world
after the puffed command, puff must obtain the events in the book and
if the book's source file has changed there is no assurance that the
reconstructed world is the one the user intends.

Warning: We do not detect changes to uncertified books that have been
included and are then puffed or re-included!  The act of including an
uncertified book leaves no trace of the check sum of the book.
Furthermore, the act prints a warning message disclaiming soundness.
In light of this, :puff quietly "re-"executes the current contents of
the book.

PUFF*    replace a compound command by its subevents

     Example Forms:
     ACL2 !>:puff* :max
     ACL2 !>:puff* :x
     ACL2 !>:puff* 15
     ACL2 !>:puff* "book"

     General Form:
     :puff* cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command.  See PUFF for the definition of "puffable"
and for a description of the basic act of "puffing" a command.  In
particular, see PUFF for a discussion of a sense in which puff,
and hence puff*, should be viewed as a hack.  Puff* is just the
recursive application of puff.  Puff* prints the region puffed, using
pcs.

To puff a command is to replace it by its immediate subevents, each of
which is executed as a command.  To puff* a command is to replace the
command by each of its immediate subevents and then to puff* each of
the puffable commands among the newly introduced ones.

For example, suppose "ab" is a book containing the following

     (in-package "ACL2")
     (include-book "a")
     (include-book "b")

Suppose that book "a" only contained defuns for the functions a1 and a2
and that "b" only contained defuns for b1 and b2.

Now consider an ACL2 state in which only two commands have been
executed, the first being (include-book "ab") and the second being
(include-book "c").  Thus, the relevant part of the display produced by
:pbt 1 would be:

     1 (INCLUDE-BOOK "ab")
     2 (INCLUDE-BOOK "c")

Call this state the "starting state" in this example, because we will
refer to it several times.

Suppose :puff 1 is executed in the starting state.  Then the first
command is replaced by its immediate subevents and :pbt 1 would show:

     1 (INCLUDE-BOOK "a")
     2 (INCLUDE-BOOK "b")
     3 (INCLUDE-BOOK "c")

Contrast this with the execution of :puff* 1 in the starting state.
Puff* would first puff (include-book "ab") to get the state shown
above.  But then it would recursively puff* the puffable commands
introduced by the first puff.  This continues recursively as long as
any puff introduced a puffable command.  The end result of :puff* 1 in
the starting state is

     1 (DEFUN A1 ...)
     2 (DEFUN A2 ...)
     3 (DEFUN B1 ...)
     4 (DEFUN B2 ...)
     5 (INCLUDE-BOOK "c")

Observe that when puff* is done, the originally indicated command,
(include-book "ab"), has been replaced by the corresponding sequence of
primitive events.  Observe also that puffable commands elsewhere in the
history, for example, command 2 in the starting state, are not affected
(except that their command numbers grow as a result of the splicing in
of earlier commands).

RESET-KILL-RING    save memory by resetting and perhaps resizing the kill ring used by oops

By default, ACL2 holds on to old logical worlds when you undo commands
(see UBT), as documented elswhere; see OOPS.  You can
free up memory by deleting those old worlds using reset-kill-ring.

     Examples:
     (reset-kill-ring t state)   ; replace each element of the kill ring by nil
     (reset-kill-ring 2 state)   ; create a new kill ring of '(nil nil)
     (reset-kill-ring 0 state)   ; create a new kill ring that is empty
     (reset-kill-ring nil state) ; just return the length of the kill ring

     General form:
     (reset-kill-ring n state)

where n evaluates either to t, to nil, or to a nonnegative integer (a
natp).  If n evaluates to t, it is treated as the length of the current
kill ring.  If n is nil, then the length k of the current kill ring is
returned as a value triple (mv nil k state).  If n is a natp, then the
kill ring is replaced with a list of n nils.

In particular, use (reset-kill-ring 0 state) to avoid saving any old
logical worlds, at the cost of disabling the effect of the oops command.

U    undo last command, without a query

     Example:
     :u

The keyword command :u is the same as :ubt :max, but with related
queries suppressed appropriately.  :Oops will undo the last :u.  See
UBT, see UBU, see UBT!, and see UBU!.

UBT    undo the commands back through a command descriptor

     Examples:
     :ubt :max      ; undo back through the most recent command
                    ; (which just means undo the most recent command)
     :ubt :x        ; same as :ubt :max
     :u             ; same as :ubt :max with no questions asked
     :ubt fn        ; undo back through the introduction of fn
                    ; (including all the other events in fn's block)
     :ubt 5         ; undo back through the fifth command executed
     :ubt (:max -4) ; undo back through the most recent five commands
     :ubt (:x -4)   ; undo back through the most recent five commands

See COMMAND-DESCRIPTOR.

Ubt takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR.  Pbt will print the commands that ubt will undo.
:Oops will undo the undo.  See OOPS.

Ubt can cause errors or queries.  To avoid these, see UBT!.

It is important to remember that a command may create several events.
That is, the command that introduces fn1 may also introduce fn2.
Undoing the command that created either of these will undo them both.
The events created by a command constitute the command's "block" and we
can only undo entire blocks.  Use pcb to print the command block of a
command if you wish to see what will be lost by undoing the command.

Ubt will not undo into "prehistory".  :Ubt 1 will undo all of your
commands.  But :ubt -5 will cause an error, warning you that :ubt
cannot undo system initialization.

See U for how to undo just the latest command, and see
UBU and see UBU! for how to undo back up to, but not
including, the current command.

UBT!    undo commands, without a query or an error

     Example:
     :ubt! :x-4

The keyword command :ubt! is the same as :ubt, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubt!  will always have a
first component of nil.  :Oops will undo the last :ubt!.  See
UBT, see UBU, and see U.

UBT-PREHISTORY    undo the commands back through the last reset-prehistory event

This command is only used to eliminate a reset-prehistory event.  If
your most recent reset-prehistory event does not have a flag argument
of t, then :ubt-prehistory undoes all command back through, and
including, that reset-prehistory event.

UBU    undo the commands back up to (not including) a command descriptor

     Examples:
     :ubu :x-3      ; undo the last three commands (same as :ubt :x-2)
     :ubu (:x -3)   ; same as above
     :ubu fn        ; undo back up to, but not including the introduction of fn
                    ; (so fn will continue to be defined)
     :ubu 5         ; undo back up to, but not including, the fifth command
                    ; executed (leaving the first five commands in place)

See COMMAND-DESCRIPTOR.

Ubu takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) up to, but not including, the indicated command.
See COMMAND-DESCRIPTOR.

Ubu can cause errors or queries.  To avoid these, see UBU!.

Also see UBT, which is similar but also undoes the indicated
command.  As for :ubt, :oops will undo the undo (see OOPS) and
ubu will not undo into "prehistory".

See U for how to undo just the latest command, and see
UBT and see UBT! for how to undo back through (that is,
including) the current command.

UBU!    undo commands, without a query or an error

     Example:
     :ubu! :x-4

The keyword command :ubu! is the same as :ubu, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubu!  will always have a
first component of nil.  :Oops will undo the last :ubu!.  Also see
UBU, see UBT, and see U.

HONS-AND-MEMOIZATION    hash cons, function memoization, and applicative hash tables

Bob Boyer and Warren Hunt have developed a canonical representation for
ACL2 data objects and a function memoization mechanism to facilitate
reuse of previously computed results.  This facility includes
procedures to read and print ACL2 expressions in such a way that
repetition of some ACL2 objects is eliminated, thereby permitting a
kind of on-the-fly file compression.  The implementation does not alter
the semantics of ACL2 except to add a handful of definitions.

Much of the documentation for this topic is taken from the paper
"Function Memoization and Unique Object Representation for ACL2
Functions" by Robert S. Boyer and Warren A. Hunt, Jr., which has
appeared in the Sixth International Workshop on the ACL2 Theorem Prover
and Its Applications, ACM Digital Library, 2006.

You can build an experimental version of ACL2 that includes hash cons,
function memoization, and fast association lists (applicative hash
tables).  An easy way is to include the following with a make command:

     ACL2_HONS=h

So for example, to make an executable image and also documentation
(which will appear in subdirectories doc/EMACS and doc/HTML):

     make large DOC ACL2_HONS=h

In the implementation of the ACL2 logic, ACL2 data objects are
represented by Common Lisp objects of the same type, and the ACL2
pairing operation is internally implemented by the Common Lisp cons
function.  In Common Lisp, cons is guaranteed to provide a new pair,
distinct from any previously created pair.  We have defined a new ACL2
function HONS that is logically identical to the ACL2 cons function,
but whose implementation usually reuses an existing pair if its
components are identical to the components of an existing pair.  A
record of ACL2 HONS objects is kept, and when an ACL2 function calls
hons ACL2 searches for an existing identical pair before allocating a
new pair; this operation been called "hash consing".

It appears that hash consing was first conceived by A. P. Ershov in
1957, to speed up the recognition of common subexpressions.  Ershov
showed how to collapse trees to minimal DAGs by traversing trees bottom
up, and he used hashing to eliminate the re-evaluation of common
subexpressions.  Later, Eiichi Goto implemented a Lisp system with a
built-in hash consing operation: his h-CONS cells were rewrite
protected and free of duplicate copies, and Goto used this hash consing
operation to facilitate the implementation of a symbolic algebra system
he developed.

Memoizing functions also has a long history.  In 1967, Donald Michie
proposed using memoized functions to improve the performance of machine
learning.  Rote learning was improved by a learning function not
forgetting what it had previously learned; this information was stored
as memoized function values.

The use of hash consing has appeared many times.  For instance, Henry
Baker using hash consing to improve the performance of the well-known
Boyer rewriting benchmark.  Baker used both hash consing and function
memoization to improve the speed of the Takeuchi function, exactly in
the spirit of our implementation, but without the automated,
system-wide integration we report here.

The ACL2 implementation permits memoization of user-defined functions.
During execution a user may enable or disable function memoization on
an individual function basis, may clear memoization tables, and may
even keep a stack of memoization tables.  This facility takes advantage
of our implementation where we keep one copy of each distinct ACL2 data
object.  Due to the functional nature of ACL2, it is sufficient to have
at most one copy of any data structure; thus, a user may arrange to
keep data canonicalized.  This implementation extends to the entire
ACL2 system the benefits enjoyed by BDDs: canonicalization,
memoization, and fast equality check.

We have defined various algorithms using these features, and we have
observed, in some cases, substantial performance increases.  For
instance, we have implemented unordered set intersection and union
operations that operate in time roughly linear in the size of the sets.
Without using arrays, we defined a canonical representation for
Boolean functions using ACL2 objects.  We have investigated the
performance of rewriting and tree consensus algorithms to good effect,
and we believe function memoization offers interesting opportunities to
simplify algorithm definition while simultaneously providing
performance improvements.

We recommend that users focus at first on the logical definitions of
hons and other primitives rather than their underlying Common Lisp
implementations.  Integrated with this memoization system is a
performance monitoring system, which can provide real-time feedback on
the operation and usefulness of hons and function memoization.  For a
more detailed description of these tools, please see the ACL2 2006
workshop paper mentioned above.

The Fibonacci function is a small example that demonstrates the utility
of function memoization.  The following definition exhibits a runtime
that is exponential in its input argument.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (mbe
        :logic
        (cond ((zp x) 0)
              ((= x 1) 1)
              (t (+ (fib (- x 1)) (fib (- x 2)))))
        :exec
        (if (< x 2)
            x
          (+ (fib (- x 1)) (fib (- x 2))))))

Below we show how the ACL2 time$ utility can measure the time to
execute a call to the fib function (with some editing to avoid noise
from the underlying Common Lisp implementation).  Memoize is actually
an ACL2 macro that expands to a call of the ACL2 function used to
identify a function for memoization; see MEMOIZE.  This
function also accepts a well-formed term that must be true in order for
the system to memoize a call of the memoized function; to ensure that
an instance of the term is safe for evaluation in Common Lisp, a check
is performed that if the guard of the memoized function is satisfied,
then this instance will execute without error.

     ... took 2,641 milliseconds (2.641 seconds) to run with 8 available
     CPU cores.  During that period, 2,644 milliseconds (2.644 seconds)
     were spent in user mode 0 milliseconds (0.000 seconds) were spent in
     system mode 16 bytes of memory allocated.  102334155 ACL2 !>(memoize
     'fib)

     Summary
     Form:  ( TABLE MEMOIZE-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)

     Summary
     Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
     Rules: NIL
     Warnings:  None
     Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
      FIB
     ACL2 !>(time$ (fib 40))

     ... took 19 milliseconds (0.019 seconds) to run with 8 available CPU
     cores.  During that period, 20 milliseconds (0.020 seconds) were
     spent in user mode 0 milliseconds (0.000 seconds) were spent in
     system mode
      539,088 bytes of memory allocated.
      193 minor page faults, 0 major page faults, 0 swaps.
     102334155
     ACL2 !>(time$ (fib 100))

     ... took 0 milliseconds (0.000 seconds) to run with 8 available CPU
     cores.  During that period, 0 milliseconds (0.000 seconds) were
     spent in user mode 0 milliseconds (0.000 seconds) were spent in
     system mode
      5,760 bytes of memory allocated.
      3 minor page faults, 0 major page faults, 0 swaps.
     354224848179261915075
     ACL2 !>(unmemoize 'fib)

We see that once the function fib is identified as a function for which
function calls should be memoized, the execution times are
substantially reduced.  Finally, we can prevent fib from being further
memoized; in fact, unmemoize erases the previously memoized values.

The implementation of hash consing, memoization, and applicative hash
tables involves several facets: canonical representation of ACL2 data,
function memoization, and the use of Lisp hash tables to improve the
performance of association list operations.  We discuss each of these
in turn, and we mention some subtle interrelationships.  Although it is
not necessary to understand the discussion in this section, it may
permit some users to better use this implementation.  This discussion
may be confusing for some ACL2 users as it makes references to Lisp
implementation features.

The ACL2 system is actually implemented as a Lisp program that is
layered on top of a Common Lisp system implementation.  ACL2 data
constants are implemented with their corresponding counterparts in
Common Lisp; that is, ACL2 cons pairs, strings, characters, numbers,
and symbols are implemented with their specific Common Lisp
counterparts.  This choice permits a number of ACL2 primitive functions
to be implemented with their corresponding Common Lisp functions, but
there are indeed differences.  ACL2 is a logic, and as such, it does
not specify anything to do with physical storage or execution
performance.  When ACL2 is used, the knowledgeable user can write
functions to facilitate the reuse of some previously computed values.

Recall the three mechanisms under discussion: hash consing, function
memoization, and fast association list operations.  The function
memoization mechanism takes advantage of the canonical representation
of data objects provided by the hons operation as does the fast
association list operation mechanism.  Each time hons is invoked, its
arguments are themselves converted, if necessary, to uniquely
represented objects.

The ACL2 universe is recursively closed under the cons pairing
operation and the atoms.  Hash consing (hons) is logically identical to
cons, but a set of tables is used to record each hons pair.  When a
hons pair is requested, the implementation checks, in the current set
of tables, whether the requested pair already exists.  If not, a new
pair is created and a record of that pair is made; otherwise, a
reference to the previously created pair is returned.  Thus, any data
object created with hons has a unique representation, as does every
subcomponent.  We also arrange for strings to have a unique
representation -- only one copy of each different string is kept -- and
when any previously unseen string is an argument to hons, we add the
string to a unique table of strings.  A system-wide benefit of having a
canonical representation for data is that equality comparisons between
any two data objects can be done in constant time.

The definition of hons in no way changes the operation of cons -- hons
creates a cons pair.  When asked to create a hons, the implementation
checks to see if there is a cons with the same car and cdr as the hons
being requested.  Thus, the only difference between the results of a
hons call and a corresponding cons call is a notation in some invisible
(to the ACL2 logic) tables where we record which cons elements are also
hons elements.  Since a hons is nothing but a cons, the operation of
car and cdr is unchanged.  In fact, the implementation is designed so
that at any time it is safe to clear the table identifying which cons
elements are also considered hons elements.

User-defined functions with defined and verified guards can be
memoized.  When a function is memoized, a user-supplied condition
restricts the domain when memoization is attempted.  When the condition
is satisfied, memoization is attempted (assuming that memoization for
the function is presently enabled); otherwise, the function is just
evaluated.  Each memoized function has a hash table that is used to
keep track of a unique list of function arguments paired with their
values.  If appropriate, for each function the corresponding table is
checked to see if a previous call with exactly the same arguments
already exists in the table: if so, then the associated value is
returned; if not, then the function is evaluated and a new key-value
pair is added to the table of memoized values so that some future call
will benefit from the memoization.  With ACL2 user functions
memoization can be dynamically enabled and disabled.  There is an ACL2
function that clears a specific memoization table.  And finally, just
as with the hons table, a stack of these function memoization tables is
maintained; that is, it is possible to memoize a function, use it a
bit, set the memoized values aside, start a new table, use it, and then
return to the original table.

We next discuss the fast lookup operation for association lists.  When
a pair is added to an association list using the functions hons-acons
or hons-acons!, the system also records the key-value pair in an
associated hash table.  As long as a user only used these two functions
when placing key-value pairs on an association list, the key-value
pairs in the corresponding hash table will be synchronized with the
key-value pairs in the association list.  Later, if hons-get is used to
look up a key, then instead of performing a linear search of the
association list we consult the associated hash table.  If a user does
not strictly follow this discipline, then a linear search may be
required.  In some sense, these association lists are much like ACL2
arrays, but without the burden of explicitly naming the arrays.  The
ACL2 array compress1 function is analogous to the functions
hons-shrink-alist and hons-shrink-alist!.  There are user-level ACL2
functions that allow the associated hash tables to be cleared and
removed.

Finally, we would advise anyone who is using CCL in a research
environment to stay plugged into the "trunk" or "bleeding edge" of CCL
development.  This is very easy to do by typing a few commands to a
shell, for example standing above the target directory as follows,
provided one has svn working.

      For linux:

        rm -rf ccl
        svn co http://svn.clozure.com/publicsvn/openmcl/trunk/linuxx8664/ccl

      For an x86 Macintosh running the Darwin OS:

        svn co http://svn.clozure.com/publicsvn/openmcl/trunk/darwinx8664/ccl

      To keep up to date, you may find it sufficient to do:

        cd ccl
        svn update

REFERENCES

Baker, Henry G., The Boyer Benchmark at Warp Speed. ACM Lisp Pointers
V,3 (Jul-Sep 1992), pages 13-14.

Baker, Henry G., A Tachy 'TAK'.  ACM Lisp Pointers Volume 3,
July-September, 1992, pages 22-23.

Robert S. Boyer and Warren A. Hunt, Jr., Function Memoization and
Unique Object Representation for ACL2 Functions, in the Sixth
International Workshop on the ACL2 Theorem Prover and Its Applications,
ACM Digital Library, 2006.

A. P. Ershov.  On Programming of Arithmetic  Operations.  In the
Communications of the ACM, Volume 118, Number 3, August, 1958, pages
427-430.

Eiichi Goto, Monocopy and Associative Algorithms in Extended Lisp,
TR-74-03, University of Toyko, 1974.

Richard P. Gabriel.  Performance and Evaluation of Lisp Systems.  MIT
Press, 1985.

Donald Michie.  Memo functions: a Language Feature with Rote Learning
Properties.  Technical Report MIP-R-29, Department of Artificial
Intelligence, University of Edinburgh, Scotland, 1967.

Donald Michie.  Memo Functions and Machine Learning.  In Nature,
Volumne 218, 1968, pages 19-22.

*UNTROUBLESOME-CHARACTERS*    Some not so weird characters.

*UNTROUBLESOME-CHARACTERS* should not include single quote, whitespace
characters, control characters, or anything else weird for a file name.
Such characters should only be used in file names by experts at
quoting.

CLEAR-MEMOIZE-TABLE    Forget values remembered for the function FN

A logical no-op.  The values memoized for fn are forgotten.

CLEAR-MEMOIZE-TABLES    Forget values remembered for all the memoized functions.

A logical no-op.  All memoized values are forgotten.

Returns NIL.  Invokes CLEAR-MEMOIZE-TABLE for each memoized function.

CONS-SUBTREES    Computes the hons graph of a term

(cons-subtrees x NIL) is an alist that associates each subtree of x
with t, without duplication.  It may run slower than
FASTER-CONS-SUBTREES.

HONS    hash cons

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

Logically, hons is merely another name for cons, i.e., the following is
an ACL2 theorem.

     (equal (hons x y) (cons x y))

However, hons creates a special kind of cons pair, which we call a hons
pair or, for short, hons.

Hons generally runs slower than cons because in creating a hons, an
attempt is made to see whether a hons already exists with the same car
and cdr.  This involves search and the use of hash-tables.  In the
worst case, honsing can be arbitrarily slow, but our experience in CCL
is that honsing is generally about 20 times as slow as consing.

In our implementation, every hons really is a cons pair, but not every
cons pair is a hons, as can be determined by using eq in raw Common
Lisp.  For example, consider this interaction in raw Common Lisp.

     ? (setq x (cons 1 2))
     (1 . 2)
     ? (setq y (hons 1 2))
     (1 . 2)
     ? (setq z (hons 1 2))
     (1 . 2)
     ? (eq y z)
     T
     ? (eq x y)
     NIL

HONS-ASSOC-EQUAL    like assoc-equal but does not cause an error.

Hash-Cons'ed association lists used with HONS-GET, HONS-ACONS, and
HONS-ACONS!, may have any symbol at the end instead of just NIL, as
ALISTP requires.  The symbol allows an association list to be 'named'.
Such naming may be important to keep fast hash alists from colliding
with one another, resulting in inefficient performance.

HONS-COPY    identity function that creates hons pairs

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

Logically, hons-copy is merely another name for the identity function,
i.e., the following is a theorem.

     (equal (hons-copy x) x)

Hons-copy returns a value in which all conses are honses.  You cannot
directly tell this from within ACL2, where both x and (hons-copy x) are
definitely equal.  But ACL2 will not permit you to call eq on them
because the guard for eq is (or (symbolp x) (symbolp y)).

HONS-EQUAL    equality for hons pairs

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

Logically, hons-equal is merely another name for equal, i.e., the
following is a theorem.

     (equal (hons-equal x y) (equal x y))

But hons-equal may run much faster than equal in some cases.  If both
arguments are determined to be honses, then hons-equal becomes a mere
eq.

HONS-ACONS    acons with hons

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

Logically, hons-acons is merely another name for the acons function,
i.e., the following is a theorem.

     (equal (hons-acons key value alist)
            (cons (cons key value) alist))

Practically speaking, HONS-COPY is called on the KEY so that fast
access with HONS-GET is a possibility.

Each time that HONS-ACONS is called when alist has an underlying hash
table for fast access, that hash table is 'stolen' and associated with
the result of the HONS-ACONS.

Has an 'under the hood' implementation.

HONS-ACONS!    acons with hons

Logically, hons-acons! is merely another name for the acons function,
i.e., the following is a theorem.

     (equal (hons-acons! key value alist)
            (cons (cons key value) alist))

Practically speaking, HONS-COPY is called on the KEY, VALUE, and ALIST,
so that fast access with HONS-GET is a possibility.

Each time that HONS-ACONS is called when alist has an underlying hash
table for fast access, that hash table is 'stolen' and associated with
the result of the HONS-ACONS.

Has an 'under the hood' implementation.  The (HONS KEY VALUE) below
will cause VALUE to have a unique representation, which, for large
structures, may require a substantial amount of work.

HONS-GET    assoc-equal for hons

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

Logically, HONS-GET is merely another name for the ASSOC-EQUAL function
when the guard of ASSOC-EQUAL is satisfied, i.e., the following is a
theorem.

       (implies (alistp alist)
                (equal (hons-get key alist)
                       (assoc-equal key alist)))

If alist has been formed via calls to HONS-ACONS, HONS-GET should
operate at hash-table lookup speed.

HONS-GET has an 'under the hood' implementation.

IO    input/output facilities in ACL2

     Example:
     (mv-let
       (channel state)
       (open-input-channel "foo.lisp" :object state)
       (mv-let (eofp obj state)
               (read-object channel state)
               (.
                 .
                  (let ((state (close-input-channel channel state)))
                        (mv final-ans state))..)))

Also see FILE-READING-EXAMPLE.

For advanced ways to control printing, see PRINT-CONTROL.

For a discussion of formatted printing, see FMT.

To control ACL2 abbreviation ("evisceration") of objects before printing
them, see SET-EVISC-TUPLE, see WITHOUT-EVISC, and see
SET-IPRINT.

ACL2 supports input and output facilities equivalent to a subset of
those found in Common Lisp.  ACL2 does not support random access files
or bidirectional streams.  In Common Lisp, input and output are to or
from objects of type stream.  In ACL2, input and output are to or from
objects called "channels," which are actually symbols.  Although a
channel is a symbol, one may think of it intuitively as corresponding
to a Common Lisp stream.  Channels are in one of two ACL2 packages,
"ACL2-INPUT-CHANNEL" and "ACL2-OUTPUT-CHANNEL".  When one "opens" a
file one gets back a channel whose symbol-name is the file name passed
to "open," postfixed with -n, where n is a counter that is incremented
every time an open or close occurs.

There are three channels which are open from the beginning and which
cannot be closed:

       acl2-input-channel::standard-character-input-0
       acl2-input-channel::standard-object-input-0
       acl2-input-channel::standard-character-output-0

All three of these are really Common Lisp's *standard-input* or
*standard-output*, appropriately.

For convenience, three global variables are bound to these rather
tedious channel names:

       *standard-ci*
       *standard-oi*
       *standard-co*

Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte.  ACL2 permits an additional type called
"object".  In ACL2 an "io-type" is a keyword, either :character, :byte,
or :object.  When one opens a file, one specifies a type, which
determines the kind of io operations that can be done on the channel
returned.  The types :character and :byte are familiar.  Type :object
is an abstraction not found in Common Lisp.  An :object file is a file
of Lisp objects.  One uses read-object to read from :object files and
print-object$ to print to :object files.  (The reading and printing are
really done with the Common Lisp read and print functions.)

File-names are strings.  ACL2 does not support the Common Lisp type
pathname.

Here are the names, formals and output descriptions of the ACL2 io
functions.

     Input Functions:
       (open-input-channel (file-name io-type state) (mv channel state))
       (open-input-channel-p (channel io-type state) boolean)
       (close-input-channel (channel state) state)
       (read-char$ (channel state) (mv char/nil state)) ; nil for EOF
       (peek-char$ (channel state) boolean)
       (read-byte$ (channel state) (mv byte/nil state)) ; nil for EOF
       (read-object (channel state) (mv eof-read-flg obj-read state))

     Output Functions:
       (open-output-channel  (file-name io-type state) (mv channel state))
       (open-output-channel! (file-name io-type state) (mv channel state))
       (open-output-channel-p (channel io-type state) boolean)
       (close-output-channel (channel state) state)
       (princ$ (obj channel state) state)
       (write-byte$ (byte channel state) state)
       (print-object$ (obj channel state) state)
       (fms  (string alist channel state evisc-tuple) state)
       (fms! (string alist channel state evisc-tuple) state)
       (fmt  (string alist channel state evisc-tuple) (mv col state))
       (fmt! (string alist channel state evisc-tuple) (mv col state))
       (fmt1 (string alist col channel state evisc-tuple) (mv col state))
       (fmt1! (string alist col channel state evisc-tuple) (mv col state))
       (cw (string arg0 arg1 ... argn) nil)

The "formatting" functions are particularly useful; see FMT and
see CW.  In particular, cw prints to a "comment window" and
does not involve the ACL2 state, so many may find it easier to use than
fmt and its variants.  The functions fms!, fmt!, and fmt1! are the same
as their respective functions without the "!," except that the "!"
functions are guaranteed to print forms that can be read back in (at a
slight readability cost).

When one enters ACL2 with (lp), input and output are taken from
*standard-oi* to *standard-co*.  Because these are synonyms for
*standard-input* and *standard-output*, one can drive ACL2 io off of
arbitrary Common Lisp streams, bound to *standard-input* and
*standard-output* before entry to ACL2.

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  See SET-PRINT-CASE
for how to get ACL2 to print symbols in lower case.

By default, numbers are printed in radix 10 (base 10).  See
SET-PRINT-BASE for how to get ACL2 to print numbers in radix 2, 8, or
16.

Comment for advanced users: Function open-output-channel! is identical
as a function to open-output-channel, except that the former may be
called even during make-event expansion and clause-processor hints, but
requires that there is an active trust tag (see DEFTTAG).

Finally, we note that the distributed book books/misc/file-io.lisp
contains useful file io functions whose definitions illustrate some of
the features described above.

EVISC-TUPLE    control suppression of details when printing

ACL2 output is generally printed in full.  However, ACL2 can be
directed to abbreviate, or "eviscerate", objects before printing them.
To "eviscerate" an object we replace certain substructures within it by
strings that are printed in their stead.  Such replacement is made
relative to a so-called "evisc-tuple", which has four components:
(evisc-tuple print-level print-length alist hiding-cars) is the same as
the value of (list alist print-level print-length hiding-cars), and the
components are used as follows (with priority order as discussed
below).  The alist component is used to replace any substructure
occurring as a key by the corresponding string.  The print-level and
print-length are analogous to Common Lisp variables *print-level* and
*print-length*, respectively, and cause replacement of substructures
deeper than print-level by `#' and those longer than print-length by
`...'.  Finally, any consp x that starts with one of the symbols in
hiding-cars is printed as <hidden>.

The following example illustrates the use of an evisc-tuple that limits
the print-level to 3 -- only three descents into list structures are
permitted before replacing a subexpression by `#' -- and limits the
print-length to 4 -- only the first four elements of any list structure
will be printed before replacing its tail by `...'.

     ACL2 !>(fms "~x0~%"
                 (list (cons #\0 '((a b ((c d)) e f g) u v w x y)))
                 *standard-co*
                 state
                 (evisc-tuple 3 4 nil nil))

     ((A B (#) E ...) U V W ...)
     <state>
     ACL2 !>

Notice that it is impossible to read the printed value back into ACL2,
since there is no way for the ACL2 reader to interpret `#' or `...'.  To
solve this problem, see SET-IPRINT.

In the above example we pass an evisc-tuple explicitly to a printing
function, in this case, fms (see FMT).  But ACL2 also does its
own printing, for example during a proof attempt.  There are global
evisc-tuples that control ACL2's printing; see SET-EVISC-TUPLE
and see WITHOUT-EVISC.

EVISCERATE-HIDE-TERMS    to print (hide ...) as <hidden>

     Example:
     (assign eviscerate-hide-terms t)
     (assign eviscerate-hide-terms nil)

Eviscerate-hide-terms is a state global variable whose value is either
t or nil.  The variable affects how terms are displayed by default (but
not if you have set the term-evisc-tuple to other than its default; see
SET-EVISC-TUPLE).  If t, terms of the form (hide ...)  are
printed as <hidden>.  Otherwise, they are printed normally.

IPRINT    See SET-IPRINT.

IPRINTING    See SET-IPRINT.

OPEN-OUTPUT-CHANNEL!    when trust tags are needed to open output channels

Use this function in place of open-output-channel if you want to open a
channel for output at times this would otherwise be prohibited, for
example during make-event expansion and clause-processor hints.  If
this functionality doesn't quite seem like what you need, take a look
at the definition of open-output-channel! in axioms.lisp, specifically
the binding of state global variable writes-okp.  The following
example, taken from books/hons-archive/hons-archive.lisp, illustrates
the latter approach.

     (defmacro har-zip! (x filename &key sortp)
       "See :doc hons-archive"
       `(mv-let (erp val state)
                (progn!
                 :state-global-bindings
                 ((temp-touchable-vars t set-temp-touchable-vars))
                 (state-global-let*
                  ((writes-okp t))
                  (let ((state (har-zip-fn ,x ,filename ,sortp state)))
                    (mv nil nil state))))
                (declare (ignore erp val))
                state))

The book below illustrates the soundness loophole plugged in ACL2
Version_3.2 related to file writes during book certification.

     ; The following example is adapted (with only very slight changes)
     ; from one written by Peter Dillinger.  It illustrates the prohibition
     ; against writing files enforced by with-output-channel during book
     ; certification (more specifically, during make-event expansion).

     ; This book certifies in ACL2 Version_3.1 before the fix discussed in the
     ; paragraph about it being ``possible to write files during book
     ; certification'' in :DOC NOTE-3-2.  The fix was actually made to ACL2
     ; function open-output-channel.

     ; After the fix, in order for certification to succeed one needs to do
     ; two things.  First, in raw lisp:
     ;   (push :after-writes-okp-fix *features*)
     ; Second, certify with this command:
     ;   (certify-book "writes-okp" 0 nil :ttags (:writes-okp))

     (in-package "ACL2")

     (local
      (defun write-objects-to-channel (obj-lst chan state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (true-listp obj-lst)))
        (if (consp obj-lst)
            (pprogn (print-object$ (car obj-lst) chan state)
                    (write-objects-to-channel (cdr obj-lst) chan state)
                    state)
          state)))

     #+after-writes-okp-fix
     (defttag :writes-okp)

     (local
      (defun write-objects-to-file (obj-lst filename state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (and (stringp filename)
                                    (true-listp obj-lst))))
        (mv-let (chan state)
                #-after-writes-okp-fix
                (open-output-channel filename :object state)
                #+after-writes-okp-fix
                (open-output-channel! filename :object state)
                (if chan
                    (pprogn (write-objects-to-channel obj-lst chan state)
                            (close-output-channel chan state)
                            (value :done))
                  (er soft 'write-object-to-file
                      "Could not open for writing: ~x0"
                      filename)))))

     (local
      (defconst *nil.lisp*
        '((in-package "ACL2")
          (defthm bad nil :rule-classes nil))))

     (local
      (defconst *nil.cert*
        '((IN-PACKAGE "ACL2")
          "ACL2 Version 3.1"
          :BEGIN-PORTCULLIS-CMDS
          :END-PORTCULLIS-CMDS
          NIL
          (("/home/peterd/test/nil.lisp" "nil" "nil"
            ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134094174))
          62589544
          )))

     (local
      (make-event (er-progn
                   (write-objects-to-file *nil.lisp* "nil.lisp" state)
                   (write-objects-to-file *nil.cert* "nil.cert" state)
                   (value '(value-triple :invisible)))))

     (local (include-book
             "nil" :load-compiled-file nil))

     (defthm bad nil :rule-classes nil)

PRINC$    print a string

Use princ$ to print a string, without the surrounding double-quotes.
Princ$ returns state.

     Examples:
     ACL2 !>(princ$ "Howdy ho" (standard-co state) state)
     Howdy ho<state>
     ACL2 !>(pprogn (princ$ "Howdy ho" (standard-co state) state)
                    (newline (standard-co state) state))
     Howdy ho
     <state>
     ACL2 !>

See FMT for more sophisticated printing routines, and see
IO for general information about input and output.

PRINT-CONTROL    advanced controls of ACL2 printing

See IO for a summary of printing in ACL2.  Here we document
some advanced ways to control what is printed by ACL2's primary
printing routines.

See SET-PRINT-BASE and see SET-PRINT-CASE for
discussions of the most common ways to control what is printed.
Indeed, these are the only ways to control the behavior of princ$ and
prin1$.

The rest of this topic is for advanced users of ACL2.  We refer to
Common Lisp behavior, as described in any good Common Lisp
documentation.

*Print-control variables*.  Set-print-base and set-print-case assign to
corresponding so-called "state global variables" 'print-base and
'print-case, which can be accessed using the expressions (@ print-base)
and (@ print-case), respectively; see ASSIGN.  Here is a table
showing all print-control variables, their setters, and their defaults.

     print-base          set-print-base          10
     print-case          set-print-case          :upcase
     print-circle        set-print-circle        nil
       [but see remark on print-circle-files, below]
     print-escape        set-print-escape        t
     print-length        set-print-length        nil
     print-level         set-print-level         nil
     print-lines         set-print-lines         nil
     print-pretty        set-print-pretty        nil
     print-radix         set-print-radix         nil
     print-readably      set-print-readably      nil
     print-right-margin  set-print-right-margin  nil

Each ACL2 print-control variable print-xxx can correspond in function to
Common Lisp variable *PRINT-XXX*.  Specifically, the evaluation of forms
(set-print-base t) and (set-print-case t) affects ACL2 printing
functions in much the same way that setting to t Common Lisp variables
*PRINT-BASE* and *PRINT-CASE*, respectively, affects Common Lisp
printing.  The same is true for print-escape, except that this does not
affect princ$ or prin1$, which correspond to Common Lisp functions
princ and prin1: princ treats *PRINT-ESCAPE* as nil while prin1 treats
*PRINT-ESCAPE* as t.  Moreover, all print-control variables not
mentioned in this paragraph are set to their defaults in princ$ and
prin1$, as indicated by ACL2 constant *print-control-defaults*, except
that print-readably is set to nil in princ$.

Fmt and its related functions are sensitive to state globals
'print-base, 'print-case, 'print-escape, and 'print-readably, in
analogy with Common Lisp functions that don't fix *PRINT-ESCAPE* or
*PRINT-READABLY*.  But the fmt functions do not respect settings of
other print-control variables; for example, they act as though
'print-circle is nil.  Since ACL2 output is produced using the same
underlying print routines as the fmt functions, it also is insensitive
to all print-control variables except for the four above.  To control
the print-level and print-length used for producing ACL2 output, see
SET-EVISC-TUPLE.

Print-object$ is sensitive to all of the print-control variables.

Remark on print-circle-files: ACL2 typically binds 'print-circle to t
before writing certificate files, or auxiliary files that are compiled
when make-event forms are present in a book, or files in support of
:comp commands.  This binding allows for structure sharing that can
keep these files from growing large.  However, this behavior is
defeated in GCL (Gnu Common Lisp), because of the small number of
indices n available by default (1024) for the #n= reader macro.  For the
files described above, what actually happens is that 'print-circle is
bound to the value of 'print-circle-files, which by default is t unless
the underlying Lisp is GCL, in which case it is set to nil.  See
ASSIGN for how to set state globals such as 'print-circle-files.  For
example, if you build GCL with a larger number of #n= indices
available, you may wish to restore the print-circle behavior for
certificate files by following these instructions from Camm Maguire:

     This can trivially be revised to any larger constant by editing the
     following line of read.d and recompiling:

     #ifndef SHARP_EQ_CONTEXT_SIZE
     #define SHARP_EQ_CONTEXT_SIZE 500
     #endif

End of Remark.

Evaluate (reset-print-control) to restore all print-control variables to
their original settings, as stored in constant *print-control-defaults*.

(Remark for those using ACL2 built on Gnu Common Lisp (GCL) versions
that are non-ANSI, which as of October 2008 is all GCL versions
recommended for ACL2: Note that Common Lisp variables *PRINT-LINES*,
*PRINT-MISER-WIDTH*, *PRINT-READABLY*, *PRINT-PPRINT-DISPATCH*, and
*PRINT-RIGHT-MARGIN* do not have any effect for such GCL versions.)

RESET-PRINT-CONTROL    See PRINT-CONTROL.

SET-EVISC-TUPLE    control suppression of details when printing

ACL2 output is generally printed in full.  However, ACL2 can be
directed to abbreviate, or "eviscerate", objects before printing them,
though the use of a so-called "evisc-tuple".  See EVISC-TUPLE
for a discussion of evisc-tuples.  The utility set-evisc-tuple modifies
certain global evisc-tuples, as explained below, to affect the extent
to which ACL2 eviscerates objects during printing, for example during
proof output or when printing top-level evaluation results.

     General Form:
     (set-evisc-tuple evisc-tuple ; a legal evisc-tuple, or :DEFAULT
                     :iprint val  ; one of *iprint-actions*
                     :sites sites ; either :ALL, or an element or a subset of the
                                  ;   list (:TERM :LD :TRACE :ABBREV)

where the value of :iprint is passed to set-iprint, :sites :all
abbreviates :sites '(:TERM :LD :TRACE :ABBREV), and other documentation
is provided below.  Note that all arguments are evaluated.

See WITHOUT-EVISC for how to avoid evisceration for ACL2 output.

The following example illustrates an invocation of set-evisc-tuple that
limits the print-level to 3 -- only three descents into list structures
are permitted before eviscerating a subterm -- and limits the
print-length to 4 -- only the first four elements of any list structure
will be printed.

     ACL2 !>(set-evisc-tuple (evisc-tuple 3   ; print-level
                                          4   ; print-length
                                          nil ; alist
                                          nil ; hiding-cars
                                          )
                             :iprint :same ; better yet, T
                             :sites :all)
      (:TERM :LD :TRACE :ABBREV)
     ACL2 !>'((a b ((c d)) e f g) u v w x y)
     ((A B (#) E ...) U V W ...)
     ACL2 !>

We recommend however using :iprint t so that eviscerated terms may be
read back in; see SET-IPRINT.  Indeed, the :iprint argument is
required as a reminder to the user to consider that issue, unless
iprinting has been enabled at least once.  If :sites or a required
:iprint argument is omitted, however, ACL2 will query the user for the
missing arguments rather than causing an error.

ACL2 eviscerates by default only in a few cases, primarily in
informational messages for errors, warnings, and queries (i.e., in the
:EVISC case below).  Users can modify the default behavior by supplying
a suitable argument to set-evisc-tuple.  The argument may be :default,
which denotes the evisceration provided when ACL2 starts up.  Otherwise
that argument is an evisc-tuple, which is either nil (no evisceration)
or as described above.  Moreover, there are four evisc-tuple
"evisceration contexts", each with its own evisceration control.  The
value returned by set-evisc-tuple indicates the evisceration contexts
whose evisc-tuple has been set.  The evisceration contexts are as
follows, all of which use a default value of nil for the hiding-cars.
Accessors are also shown for retrieving the corresponding evisc-tuple.

     o :TERM -- used for printing terms.  The accessor is
     (term-evisc-tuple flg state), where flg is ignored if
     set-evisc-tuple has been called for :term with value other than
     :default, and otherwise (hence initially): a flg of nil indicates
     an evisc-tuple of nil, and otherwise the term-evisc-tuple has a
     print-level of 3 and print-length of 4.

     o :ABBREV -- used for printing informational messages for errors,
     warnings, and queries.  Initially, the alist abbreviates the ACL2
     world, print-level is 5, and print-level is 7.  The accessor is
     (abbrev-evisc-tuple state).

     o :LD -- used by the ACL2 read-eval-print loop.  The accessor is
     (ld-evisc-tuple state).

     o :TRACE -- used for printing trace output.  No accessor is
     available (though in raw Lisp, (trace-evisc-tuple) returns the
     trace-evisc-tuple).

Each context ectx also has an updater, (set-ectx-evisc-tuple val
state), where val is a legal value for set-evisc-tuple as described
above: :default or an evisc-tuple (possibly nil).

Note that the proof-checker generally does its printing using the
term-evisc-tuple.

SET-FMT-HARD-RIGHT-MARGIN    set the hard right margin for formatted output

Fmt and related functions insert linebreaks when lines get too long.  A
linebreaks is inserted at an aesthetically appropriate points once the
column exceeds the value of state global fmt-soft-right-margin, i.e.,
the result of evaluating (@ fmt-soft-right-margin).  If however the
column exceeds the value of state global fmt-hard-right-margin, i.e.,
the result of evaluating (@ fmt-hard-right-margin), then a linebreak is
soon inserted.  Such a "hard" linebreak follows the insertion of a
backslash (\) character unless fmt!, fms!, or fmt1! is used, or state
global write-for-read is true.

SET-FMT-SOFT-RIGHT-MARGIN    set the soft right margin for formatted output

See SET-FMT-HARD-RIGHT-MARGIN for a discussion of the soft and
hard right margin for formatted output.

SET-IPRINT    control whether abbreviated output can be read back in

When ACL2 pretty-prints large expressions using formatted printing (see
FMT), it may save time and space by printing tokens `#' or
`...' in place of certain subexpressions.  By default this only happens
for a few settings such as error and warning messages; see
SET-EVISC-TUPLE for controlling such elision in general.  The full
expression is unavailable to the user when `#' or `...' is printed, but
that is easily solved by evaluating the form

       (set-iprint t)

to enable a mode called "iprinting".  Then, instead of printing `#' or
`...', ACL2 prints `#@i#' for i = 1,2,3,... -- all in base 10.  ACL2
can read back in such `#@i#' because under the hood, i is associated
with its corresponding elided form.  Thus the term "iprint" can be
viewed as suggesting "interactive print" or "index print".  We also
think of "iprint" as suggesting "i printing", to suggest the printing
of token `#@i#'.  We call i the "iprint index" of that token.

The following example should suffice to illustrate how to recover elided
subexpressions.  (Below this example we provide details that may be of
interest only to advanced users.)  Here we cause an error by defining a
macro of one argument and then calling it with two arguments.  By
default, error messages abbreviate subexpressions deeper than level 5
with `#' and past the 7th element of a list with `...'.  We see this
behavior below.

     ACL2 !>(defmacro foo (x) x)

     Summary
     Form:  ( DEFMACRO FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
      FOO
     ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D #))) H I J K L ...)).  (See :DOC set-iprint
     to be able to see elided values in this message.)

     ACL2 !>(set-iprint t)

     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)).

     ACL2 !>(acl2-count '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
     23
     ACL2 !>

Sometimes you may want to supply the abbreviated form not to compute
with it, as in the acl2-count example just above, but so that you can
see it.  The macro without-evisc eliminates elision during printing.
Below we show two ways to use this utility: first, we use it to print
the elided form, and then, we use it instead on the original input form
to print the entire error message.

     ACL2 !>(without-evisc '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
     (FOO ARG1
          (A (B (C (D (E (F (G))))))
             H I J K L M N))
     ACL2 !>(without-evisc (foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n)))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D (E (F (G)))))) H I J K L M N)).

     ACL2 !>

The documentation above probably suffices for most users.  For those
who want more details, below we detail all the ways to use the
set-iprint utility.

     Example Forms:
     (set-iprint t)   ; enable iprinting (elision with #@i@)
     (set-iprint nil) ; disable iprinting

     General Form:
     (set-iprint action        ; t, nil, :reset, :reset-enable, or :same
                 :soft-bound s ; initially  1000
                 :hard-bound h ; initially 10000)

where all arguments are optional, but ACL2 queries for action if it is
omitted.   We defer the explanations of :soft-bound and :hard-bound.
The values for action are as follows:

     T -- Enable iprinting.

     NIL -- Disable iprinting.

     :RESET -- Reset iprinting so that when enabled, the first index i
     for which `#@i# is printed will be 1.  Note that all stored
     information for existing iprint indices will be erased.

     :RESET-ENABLE -- Reset iprinting as with :reset, and then enable
     iprinting.

     :SAME -- Make no change to the iprinting state (other than setting
     the :soft-bound and/or :hard-bound if specified, as explained
     below).

Immediately after a top-level form is read, hence before it is
evaluated, a check is made for whether the latest iprint index exceeds
a certain bound, (iprint-soft-bound state) -- 1000, by default.  If so,
then the (iprint-last-index state) is set back to 0.  This soft bound
can be changed to any positive integer k by calling set-iprint with
:soft-bound k, typically (set-iprint :same :soft-bound k)].

The above "soft bound" is applied once for each top-level form, but you
may want finer control by applying a bound after the pretty-printing of
each individual form (since many forms may be pretty-printed between
successive evaluations of top-level forms).  That bound is
(iprint-hard-bound state), and can be set with the :hard-bound argument
in analogy to how :soft-bound is set, as described above.

A "rollover" is the detection that the soft or hard bound has been
exceeded, along with a state update so that the next iprint index will
be 1.  When a rollover occurs, any index beyond the latest iprint index
is no longer available for reading.  At the top level of the ACL2
read-eval-print loop, this works as follows: ACL2 reads the next
top-level form according to the current iprint state, then handles a
rollover if the latest iprint index exceeded the current soft bound.
The following log illustrates a rollover, which follows the description
above.

     ACL2 !>(set-iprint t :soft-bound 3)

     ACL2 Observation in SET-IPRINT:  The soft-bound for iprinting has been
     set to 3.

     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>(set-evisc-tuple (evisc-tuple 2 3 nil nil) :sites :ld)
      (:LD)
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@1#) (A B C . #@2#) (A B C . #@3#))
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@4#) (A B C . #@5#) (A B C . #@6#))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
     ((A B C D E F G)
      (A B C D E F G)
      (A B C D E F G))
     ACL2 !>'(1 2 3 4 5)
     (1 2 3 . #@1#)
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@2#) (A B C . #@3#) (A B C . #@4#))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
     ((A B C D E F G)
      (A B C D E F G)
      (A B C D E F G))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  Out-of-bounds index in #@5#.  See :DOC set-iprint.
     ***********************************************

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

We conclude by mentioning two cases where iprinting and evisc-tuples are
ignored.  (1) This is typically the case when printing results in raw
Lisp outside the ACL2 loop.  To use iprinting and evisc-tuples in raw
Lisp, use raw-mode; see SET-RAW-MODE.  In raw-mode, results
that are ACL2 objects will be printed in the same way that ACL2 would
print those results if not in raw-mode.  (2) Iprinting and evisc-tuples
are ignored by print-object$, which however is sensitive to many
settings that do not affect formatted (fmt etc.) printing; see
PRINT-CONTROL.

The reader interested in design and implementation issues considered
during the addition of iprinting to ACL2 is invited to read the paper
"Abbreviated Output for Input in ACL2: An Implementation Case Study";
see the proceedings of ACL2 Workshop 2009,
`http://www.cs.utexas.edu/users/sandip/acl2-09/'.

SET-PRINT-BASE    control radix in which number are printed

By default, integers and ratios are printed in base 10.  ACL2 also
supports printing in radix 2, 8, or 16 by calling set-print-base with
the desired radix (base).

       (set-print-base 10 state) ; Default printing
       (set-print-base 16 state) ; Print integers and ratios in hex, e.g., #x3A

Also see PRINT-CONTROL for other user-settable print controls.

Note: ACL2 events and some other top-level commands (for example, thm,
verify, and history commands such as :pe and :pbt) set the print base
to 10 during their evaluation.  So set-print-base has no effect while
these forms are being processed.

SET-PRINT-CASE    control whether symbols are printed in upper case or in lower case

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  As with Common Lisp, ACL2
supports printing in a "downcase" mode, where symbols are printed in
lower case.  Many printing functions (some details below) print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  (Thus, this state global functions
in complete analogy to the Common Lisp global *print-case*.)  The value
print-case is returned by (print-case), and may be set using the
function set-print-case as follows.

       (set-print-case :upcase   state) ; Default printing
       (set-print-case :downcase state) ; Print symbols in lower case when
                                        ; vertical bars are not required

The ACL2 user can expect that the :downcase setting will have an effect
for formatted output (see FMT and see FMS) when the
directives are ~p, ~P, ~q, or ~Q, for built-in functions princ$ and
prin1$, and the ppr family of functions, and _not_ for built-in
function print-object$.  For other printing functions, the effect of
:downcase is unspecified.

Also see PRINT-CONTROL for other user-settable print controls.

SET-PRINT-CIRCLE    See PRINT-CONTROL.

SET-PRINT-ESCAPE    See PRINT-CONTROL.

SET-PRINT-LENGTH    See PRINT-CONTROL.

SET-PRINT-LEVEL    See PRINT-CONTROL.

SET-PRINT-LINES    See PRINT-CONTROL.

SET-PRINT-RADIX    See PRINT-CONTROL.

SET-PRINT-READABLY    See PRINT-CONTROL.

SET-PRINT-RIGHT-MARGIN    See PRINT-CONTROL.

WITHOUT-EVISC    print output in full

     General Form:
     (without-evisc form)

where form is any expression to evaluate.  The effect is to evaluate
form as though the without-evisc wrapper were absent, except that
expressions are printed in full for the ensuing output, regardless of
the current evisc-tuples (see SET-EVISC-TUPLE).  See
SET-IPRINT for an example.

More precisely, without-evisc binds the term-evisc-tuple,
ld-evisc-tuple, and abbrev-evisc-tuple to nil (see
SET-EVISC-TUPLE).  It does not modify the trace evisc-tuple, so trace
output is not modified by without-evisc.  Also note that calls of
printing functions such as fmt that include explicit evisc-tuples will
not have those evisc-tuples overridden.  The following example
illustrates this point.

     ACL2 !>(without-evisc
             (fms "~x0~%"
                  (list (cons #0 '((a b ((c d)) e f g) u v w x y)))
                  *standard-co*
                  state
                  (evisc-tuple 2 3 nil nil)))

     ((A B # ...) U V ...)
     <state>
     ACL2 !>

We conclude with two remarks.  (1) A call of without-evisc on expression
exp actually invokes a specialized call of ld on a one-element list
containing exp, which prints the value returned by evaluation of exp
but actually returns the useless value (mv nil :invisible state).  So do
not use without-evisc in programs; just use it at the top level of the
ACL2 read-eval-print loop, or at least the top level of ld.  (2) Even
when using without-evisc, if the ACL2 logical world is part of the value
returned, it will be printed in abbreviated form because the ACL2
read-eval-print loop always arranges for this to be the case,
regardless of the ld-evisc-tuple.  For example:

     ACL2 !>(without-evisc (w state))
     <world>
     ACL2 !>

An alternative to the use of without-evisc is to explore large objects
using the ACL2 function (walkabout object state).  Some brief
documentation is printed when you enter an interactive loop upon
evaluating a call of walkabout.  We may add documentation for walkabout
if that is requested.

MISCELLANEOUS    a miscellany of documented functions and concepts
               (often cited in more accessible documentation)

Perhaps as the system matures this section will become more structured.

A!    to return to the top-level of ACL2's command loop

When (a!) is evaluated inside of ACL2's command loop, the current
computation is aborted and control returns to the top of the command
loop, exactly as though the user had interrupted and aborted the current
computation.  (Note: Versions of ACL2 up to Version_3.4 provided `#.'
for this purpose, but no longer; see SHARP-DOT-READER.)

Logically speaking, (a!) = nil.  But imagine that it is defined in such
a way that it causes a stack overflow or other resource exhaustion when
called.

ABORT!    to return to the top-level of ACL2's command loop

This is an alias for a!; see A!.

ACKNOWLEDGMENTS    some contributors to the well-being of ACL2

The development of ACL2 was initially made possible by funding from the
U. S. Department of Defense, including ARPA and ONR.  We thank all the
organizations that have contributed support, including the following (in
alphabetical order).

     o AMD, for providing significant time over several years for Matt
     Kaufmann to carry out ACL2 research, support, and development
     o Computational Logic, Inc. and its president, Don Good, where the
     first eight years of ACL2 development occurred
     o DARPA
     o Digital Equipment Corporation
     o EDS, which provided some time for Matt Kaufmann's ACL2 work
     1998-1999
     o ForrestHunt and, more generally, financial support provided for
     or arranged by Warren A. Hunt, Jr.
     o IBM
     o NSF
     o ONR
     o Rockwell Collins
     o SRC
     o Sun Microsystems
     o University of Texas at Austin (in particular support to J Moore
     through the Admiral B. R.  Inman Chair of Computing Theory)

ACL2 was started in August, 1989 by Boyer and Moore working together.
They co-authored the first versions of axioms.lisp and basis.lisp, with
Boyer taking the lead in the formalization of "state" and the most
primitive io functions.  Boyer also had a significant hand in the
development of the early versions of the files interface-raw.lisp and
translate.lisp.  For several years, Moore alone was responsible for
developing the ACL2 system code, though he consulted often with both
Boyer and Kaufmann.  In August, 1993, Kaufmann became jointly
responsible with Moore for developing the system.  Boyer has continued
to provide valuable consulting on an informal basis.

Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements.  In particular, the :cases and :restrict
hints were his idea; he developed an early version of congruence-based
reasoning for Nqthm; and he helped in the development of some early
books about arithmetic.  In a demonstration of his courage and faith in
us, he pushed for Computational Logic, Inc., to agree to the Motorola
CAP contract - which required formalizing a commercial DSP in the
untested ACL2 - and moved to Scottsdale, AZ, to do the work with the
Motorola design team.  His demonstration of ACL2's utility was an
inspiration, even to those of us designing ACL2.

John Cowles also helped in the development of some early books about
arithmetic, and also provided valuable feedback and bug reports.

Other early users of ACL2 at Computational Logic, Inc. helped influence
its development.  In particular, Warren Hunt helped with the port to
Macintosh Common Lisp, and Art Flatau and Mike Smith provided useful
general feedback.

Mike Smith helped develop the Emacs portion of the implementation of
proof trees.

Bill Schelter made some enhancements to akcl (now gcl) that helped to
enhance ACL2 performance in that Common Lisp implementation, and more
generally, responded helpfully to our bug reports.  Camm Maguire has
since provided wonderful gcl support, and has created a Debian package
for ACL2 built on GCL.  We are also grateful to developers of other
Common Lisp implementations.

Kent Pitman helped in our interaction with the ANSI Common Lisp
standardization committee, X3J13.

John Cowles helped with the port to Windows (98) by answering questions
and running tests.

Ruben Gamboa created a modification of ACL2 to allow reasoning about
the real numbers using non-standard analysis.  His work has been
incorporated into the ACL2 distribution; see REAL.

Rob Sumners has made numerous useful suggestions.  In particular, he has
designed and implemented improvements for stobjs and been key in our
development of locally-bound stobjs; see NOTE-2-6.

Robert Krug has designed and implemented many changes in the vicinity
of the linear arithmetic package and its connection to type-set and
rewrite.  He was also instrumental in the development of
extended-metafunctions.

Pete Manolios has made numerous useful suggestions.  In particular, Pete
helped us to organize the first workshop and was a wonderful equal
partner with the two of us (Kaufmann and Moore) in producing the books
that arose from that workshop.  Pete and his student, Daron Vroon,
provided the current implementation of ordinals.

Jared Davis and Sol Swords have our gratitude for starting the
acl2-books repository, `http://acl2-books.googlecode.com/'.

We thank David L. Rager for contributing an initial version of the
support for parallelism in an experimental extension of ACL2.

Bob Boyer and Warren A. Hunt, Jr. developed a canonical representation
for ACL2 data objects and a function memoization mechanism to
facilitate reuse of previously computed results.  We thank them for
their extensive efforts for the corresponding experimental (as of 2008
and 2009) extension of ACL2; see HONS-AND-MEMOIZATION.

We also thank the contributors to the ACL2 workshops for some suggested
improvements and for the extensive collection of publicly distributed
benchmark problems.  And we thank participants at the ACL2 seminar at
the University of Texas for useful feedback.  More generally, we thank
the ACL2 community for feedback, contributed books, and their interest
in the ACL2 project.

_Regarding the documentation:_

     Bill Young wrote significant portions of the ACL2-TUTORIAL section
     of the ACL2 documentation, an important task for which we are
     grateful.  He, Bishop Brock, Rich Cohen, and Noah Friedman read
     over considerable amounts of the documentation, and made many
     useful comments.  Others, particularly Bill Bevier and John
     Cowles, have also made useful comments on the documentation.

     Art Flatau helped develop the ACL2 markup language and translators
     from that language to Texinfo and HTML.  Michael "Bogo" Bogomolny
     created a search engine, beginning with Version 2.6, and for that
     purpose modified the HTML translator to create one file per topic
     (a good idea in any case).

     Laura Lawless provided many hours of help in marking up
     appropriate parts of the documentation in typewriter font.

     Noah Friedman developed an Emacs tool that helped us insert
     "invisible links" into the documentation, which improve the
     usability of that documentation under HTML readers such as Mosaic.

     Richard Stallman contributed a texinfo patch, to be found in the
     file doc/texinfo.tex.

ACL2-COUNT    a commonly used measure for justifying recursion

(Acl2-count x) returns a nonnegative integer that indicates the "size"
of its argument x.

All characters and symbols have acl2-count 0.  The acl2-count of a
string is the number of characters in it, i.e., its length.  The
acl2-count of a cons is one greater than the sum of the acl2-counts of
the car and cdr.  The acl2-count of an integer is its absolute value.
The acl2-count of a rational is the sum of the acl2-counts of the
numerator and denominator.  The acl2-count of a complex rational is one
greater than the sum of the acl2-counts of the real and imaginary parts.

ACL2S    See ACL2-SEDAN.

APROPOS    searching the documentation online

The :docs command allows you to search the documentation at the
terminal.  See DOCS.

ARRAYS    an introduction to ACL2 arrays

Below we begin a detailed presentation of ACL2 arrays.  ACL2's
single-threaded objects (see STOBJ) provide a similar
functionality that is generally more efficient when there are updates
(writes), but is also more restrictive.

Related topics:

See ARRAYS-EXAMPLE for a brief introduction illustrating the use
of ACL2 arrays.

ACL2 provides relatively efficient 1- and 2-dimensional arrays.  Arrays
are awkward to provide efficiently in an applicative language because
the programmer rightly expects to be able to "modify" an array object
with the effect of changing the behavior of the element accessing
function on that object.  This, of course, does not make any sense in
an applicative setting.  The element accessing function is, after all,
a function, and its behavior on a given object is immutable.  To
"modify" an array object in an applicative setting we must actually
produce a new array object.  Arranging for this to be done efficiently
is a challenge to the implementors of the language.  In addition, the
programmer accustomed to the von Neumann view of arrays must learn how
to use immutable applicative arrays efficiently.

In this note we explain 1-dimensional arrays.  In particular, we
explain briefly how to create, access, and "modify" them, how they are
implemented, and how to program with them.  2-dimensional arrays are
dealt with by analogy.

_The Logical Description of ACL2 Arrays_

An ACL2 1-dimensional array is an object that associates arbitrary
objects with certain integers, called "indices." Every array has a
dimension, dim, which is a positive integer.  The indices of an array
are the consecutive integers from 0 through dim-1.  To obtain the
object associated with the index i in an array a, one uses (aref1 name
a i).  Name is a symbol that is irrelevant to the semantics of aref1
but affects the speed with which it computes.  We will talk more about
array "names" later.  To produce a new array object that is like a but
which associates val with index i, one uses (aset1 name a i val).

An ACL2 1-dimensional array is actually an alist.  There is no special
ACL2 function for creating arrays; they are generally built with the
standard list processing functions list and cons.  However, there is a
special ACL2 function, called compress1, for speeding up access to the
elements of such an alist.  We discuss compress1 later.

One element of the alist must be the "header" of the array.  The header
of a 1-dimensional array with dimension dim is of the form:

     (:HEADER :DIMENSIONS (dim)
              :MAXIMUM-LENGTH max
              :DEFAULT obj ; optional
              :NAME name   ; optional
              :ORDER order ; optional values are < (the default), >, or :none/nil
              ).

Obj may be any object and is called the "default value" of the array.
Max must be an integer greater than dim.  Name must be a symbol.  The
:default and :name entries are optional; if :default is omitted, the
default value is nil.  The function header, when given a name and a 1-
or 2-dimensional array, returns the header of the array.  The functions
dimensions, maximum-length, and default are similar and return the
corresponding fields of the header of the array.  The role of the
:dimensions field is obvious: it specifies the legal indices into the
array.  The roles played by the :maximum-length and :default fields are
described below.

Aside from the header, the other elements of the alist must each be of
the form (i . val), where i is an integer and 0 <= i < dim, and val is
an arbitrary object.

The :order field of the header is ignored for 2-dimensional arrays.  For
1-dimensional arrays, it specifies the order of keys (i, above) when the
array is compressed as with compress1, as described below.  An :order
of :none or nil specifies no reordering of the alist by compress1, and
an order of > specifies reordering by compress1 so that keys are in
descending order.  Otherwise, the alist is reordered by compress1 so
that keys are in ascending order.

(Aref1 name a i) is guarded so that name must be a symbol, a must be an
array and i must be an index into a.  The value of (aref1 name a i) is
either (cdr (assoc i a)) or else is the default value of a, depending
on whether there is a pair in a whose car is i.  Note that name is
irrelevant to the value of an aref1 expression.  You might :pe aref1 to
see how simple the definition is.

(Aset1 name a i val) is guarded analogously to the aref1 expression.
The value of the aset1 expression is essentially (cons (cons i val) a).
Again, name is irrelevant.  Note (aset1 name a i val) is an array, a',
with the property that (aref1 name a' i) is val and, except for index
i, all other indices into a' produce the same value as in a.  Note also
that if a is viewed as an alist (which it is) the pair "binding" i to
its old value is in a' but "covered up" by the new pair.  Thus, the
length of an array grows by one when aset1 is done.

Because aset1 covers old values with new ones, an array produced by a
sequence of aset1 calls may have many irrelevant pairs in it.  The
function compress1 can remove these irrelevant pairs.  Thus, (compress1
name a) returns an array that is equivalent (vis-a-vis aref1) to a but
which may be shorter.  For technical reasons, the alist returned by
compress1 may also list the pairs in a different order than listed in a.

To prevent arrays from growing excessively long due to repeated aset1
operations, aset1 actually calls compress1 on the new alist whenever
the length of the new alist exceeds the :maximum-length entry, max, in
the header of the array.  See the definition of aset1 (for example by
using :pe).  This is primarily just a mechanism for freeing up cons
space consumed while doing aset1 operations.  Note however that this
compress1 call is replaced by a hard error if the header specifies an
:order of :none or nil.

This completes the logical description of 1-dimensional arrays.
2-dimensional arrays are analogous.  The :dimensions entry of the
header of a 2-dimensional array should be (dim1 dim2).  A pair of
indices, i and j, is legal iff 0 <= i < dim1 and 0 <= j < dim2.  The
:maximum-length must be greater than dim1*dim2.  Aref2, aset2, and
compress2 are like their counterparts but take an additional index
argument.  Finally, the pairs in a 2-dimensional array are of the form
((i . j) . val).

_The Implementation of ACL2 Arrays_

Very informally speaking, the function compress1 "creates" an ACL2
array that provides fast access, while the function aref1 "maintains"
fast access.  We now describe this informal idea more carefully.

Aref1 is essentially assoc.  If aref1 were implemented naively the time
taken to access an array element would be linear in the dimension of
the array and the number of "assignments" to it (the number of aset1
calls done to create the array from the initial alist).  This is
intolerable; arrays are "supposed" to provide constant-time access and
change.

The apparently irrelevant names associated with ACL2 arrays allow us to
provide constant-time access and change when arrays are used in
"conventional" ways.  The implementation of arrays makes it clear what
we mean by "conventional."

Recall that array names are symbols.  Behind the scenes, ACL2
associates two objects with each ACL2 array name.  The first object is
called the "semantic value" of the name and is an alist.  The second
object is called the "raw lisp array" and is a Common Lisp array.

When (compress1 name alist) builds a new alist, a', it sets the
semantic value of name to that new alist.  Furthermore, it creates a
Common Lisp array and writes into it all of the index/value pairs of
a', initializing unassigned indices with the default value.  This array
becomes the raw lisp array of name.  Compress1 then returns a', the
semantic value, as its result, as required by the definition of
compress1.

When (aref1 name a i) is invoked, aref1 first determines whether the
semantic value of name is a (i.e., is eq to the alist a).  If so, aref1
can determine the ith element of a by invoking Common Lisp's aref
function on the raw lisp array associated with name.  Note that no
linear search of the alist a is required; the operation is done in
constant time and involves retrieval of two global variables, an eq
test and jump, and a raw lisp array access.  In fact, an ACL2 array
access of this sort is about 5 times slower than a C array access.  On
the other hand, if name has no semantic value or if it is different
from a, then aref1 determines the answer by linear search of a as
suggested by the assoc-like definition of aref1.  Thus, aref1 always
returns the axiomatically specified result.  It returns in constant
time if the array being accessed is the current semantic value of the
name used.  The ramifications of this are discussed after we deal with
aset1.

When (aset1 name a i val) is invoked, aset1 does two conses to create
the new array.  Call that array a'.  It will be returned as the answer.
(In this discussion we ignore the case in which aset1 does a
compress1.)  However, before returning, aset1 determines if name's
semantic value is a.  If so, it makes the new semantic value of name be
a' and it smashes the raw lisp array of name with val at index i,
before returning a' as the result.  Thus, after doing an aset1 and
obtaining a new semantic value a', all aref1s on that new array will be
fast.  Any aref1s on the old semantic value, a, will be slow.

To understand the performance implications of this design, consider the
chronological sequence in which ACL2 (Common Lisp) evaluates
expressions:  basically inner-most first, left-to-right, call-by-value.
An array use, such as (aref1 name a i), is "fast" (constant-time) if
the alist supplied, a, is the value returned by the most recently
executed compress1 or aset1 on the name supplied.  In the functional
expression of "conventional" array processing, all uses of an array are
fast.

The :name field of the header of an array is completely irrelevant.
Our convention is to store in that field the symbol we mean to use as
the name of the raw lisp array.  But no ACL2 function inspects :name
and its primary value is that it allows the user, by inspecting the
semantic value of the array -- the alist -- to recall the name of the
raw array that probably holds that value.  We say "probably" since
there is no enforcement that the alist was compressed under the name in
the header or that all asets used that name.  Such enforcement would be
inefficient.

_Some Programming Examples_

In the following examples we will use ACL2 "global variables" to hold
several arrays.  See @, and see ASSIGN.

Let the state global variable a be the 1-dimensional compressed array
of dimension 5 constructed below.

     ACL2 !>(assign a (compress1 'demo
                                 '((:header :dimensions (5)
                                            :maximum-length 15
                                            :default uninitialized
                                            :name demo)
                                   (0 . zero))))

Then (aref1 'demo (@ a) 0) is zero and (aref1 'demo (@ a) 1) is
uninitialized.

Now execute

     ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

Then (aref1 'demo (@ b) 0) is zero and (aref1 'demo (@ b) 1) is one.

All of the aref1s done so far have been "fast."

Note that we now have two array objects, one in the global variable a
and one in the global variable b.  B was obtained by assigning to a.
That assignment does not affect the alist a because this is an
applicative language.  Thus, (aref1 'demo (@ a) 1) must *still* be
uninitialized.  And if you execute that expression in ACL2 you will see
that indeed it is.  However, a rather ugly comment is printed, namely
that this array access is "slow."  The reason it is slow is that the
raw lisp array associated with the name demo is the array we are
calling b.  To access the elements of a, aref1 must now do a linear
search.  Any reference to a as an array is now "unconventional;" in a
conventional language like Ada or Common Lisp it would simply be
impossible to refer to the value of the array before the assignment
that produced our b.

Now let us define a function that counts how many times a given object,
x, occurs in an array.  For simplicity, we will pass in the name and
highest index of the array:

     ACL2 !>(defun cnt (name a i x)
              (declare (xargs :guard
                              (and (array1p name a)
                                   (integerp i)
                                   (>= i -1)
                                   (< i (car (dimensions name a))))
                              :mode :logic
                              :measure (nfix (+ 1 i))))
              (cond ((zp (1+ i)) 0) ; return 0 if i is at most -1
                    ((equal x (aref1 name a i))
                     (1+ (cnt name a (1- i) x)))
                    (t (cnt name a (1- i) x))))

To determine how many times zero appears in (@ b) we can execute:

     ACL2 !>(cnt 'demo (@ b) 4 'zero)

The answer is 1.  How many times does uninitialized appear in (@ b)?

     ACL2 !>(cnt 'demo (@ b) 4 'uninitialized)

The answer is 3, because positions 2, 3 and 4 of the array contain that
default value.

Now imagine that we want to assign 'two to index 2 and then count how
many times the 2nd element of the array occurs in the array.  This
specification is actually ambiguous.  In assigning to b we produce a
new array, which we might call c.  Do we mean to count the occurrences
in c of the 2nd element of b or the 2nd element of c?  That is, do we
count the occurrences of uninitialized or the occurrences of two?  If
we mean the former the correct answer is 2 (positions 3 and 4 are
uninitialized in c); if we mean the latter, the correct answer is 1
(there is only one occurrence of two in c).

Below are ACL2 renderings of the two meanings, which we call [former]
and [latter].  (Warning:  Our description of these examples, and of an
example [fast former] that follows, assumes that only one of these
three examples is actually executed; for example, they are not executed
in sequence.  See "A Word of Warning" below for more about this issue.)

     (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 (aref1 'demo (@ b) 2))  ; [former]

     (let ((c (aset1 'demo (@ b) 2 'two)))                           ; [latter]
       (cnt 'demo c 4 (aref1 'demo c 2)))

Note that in [former] we create c in the second argument of the call to
cnt (although we do not give it a name) and then refer to b in the
fourth argument.  This is unconventional because the second reference
to b in [former] is no longer the semantic value of demo.  While ACL2
computes the correct answer, namely 2, the execution of the aref1
expression in [former] is done slowly.

A conventional rendering with the same meaning is

     (let ((x (aref1 'demo (@ b) 2)))                           ; [fast former]
       (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 x))

which fetches the 2nd element of b before creating c by assignment.  It
is important to understand that [former] and [fast former] mean exactly
the same thing: both count the number of occurrences of uninitialized
in c.  Both are legal ACL2 and both compute the same answer, 2.
Indeed, we can symbolically transform [fast former] into [former]
merely by substituting the binding of x for x in the body of the let.
But [fast former] can be evaluated faster than [former] because all of
the references to demo use the then-current semantic value of demo,
which is b in the first line and c throughout the execution of the cnt
in the second line.  [Fast former] is the preferred form, both because
of its execution speed and its clarity.  If you were writing in a
conventional language you would have to write something like [fast
former] because there is no way to refer to the 2nd element of the old
value of b after smashing b unless it had been saved first.

We turn now to [latter].  It is both clear and efficient.  It creates c
by assignment to b and then it fetches the 2nd element of c, two, and
proceeds to count the number of occurrences in c.  The answer is 1.
[Latter] is a good example of typical ACL2 array manipulation: after
the assignment to b that creates c, c is used throughout.

It takes a while to get used to this because most of us have grown
accustomed to the peculiar semantics of arrays in conventional
languages.  For example, in raw lisp we might have written something
like the following, treating b as a "global variable":

     (cnt 'demo (aset 'demo b 2 'two) 4 (aref 'demo b 2))

which sort of resembles [former] but actually has the semantics of
[latter] because the b from which aref fetches the 2nd element is not
the same b used in the aset!  The array b is destroyed by the aset and
b henceforth refers to the array produced by the aset, as written more
clearly in [latter].

A Word of Warning:  Users must exercise care when experimenting with
[former], [latter] and [fast former].  Suppose you have just created b
with the assignment shown above,

     ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

If you then evaluate [former] in ACL2 it will complain that the aref1
is slow and compute the answer, as discussed.  Then suppose you
evaluate [latter] in ACL2.  From our discussion you might expect it to
execute fast -- i.e., issue no complaint.  But in fact you will find
that it complains repeatedly.  The problem is that the evaluation of
[former] changed the semantic value of demo so that it is no longer b.
To try the experiment correctly you must make b be the semantic value
of demo again before the next example is evaluated.  One way to do that
is to execute

     ACL2 !>(assign b (compress1 'demo (@ b)))

before each expression.  Because of issues like this it is often hard
to experiment with ACL2 arrays at the top-level.  We find it easier to
write functions that use arrays correctly and efficiently than to so
use them interactively.

This last assignment also illustrates a very common use of compress1.
While it was introduced as a means of removing irrelevant pairs from an
array built up by repeated assignments, it is actually most useful as a
way of insuring fast access to the elements of an array.

Many array processing tasks can be divided into two parts.  During the
first part the array is built.  During the second part the array is
used extensively but not modified.  If your programming task can be so
divided, it might be appropriate to construct the array entirely with
list processing, thereby saving the cost of maintaining the semantic
value of the name while few references are being made.  Once the alist
has stabilized, it might be worthwhile to treat it as an array by
calling compress1, thereby gaining constant time access to it.

ACL2's theorem prover uses this technique in connection with its
implementation of the notion of whether a rune is disabled or not.
Associated with every rune is a unique integer index, called its
"nume."  When each rule is stored, the corresponding nume is stored as
a component of the rule.  Theories are lists of runes and membership in
the "current theory" indicates that the corresponding rule is enabled.
But these lists are very long and membership is a linear-time
operation.  So just before a proof begins we map the list of runes in
the current theory into an alist that pairs the corresponding numes
with t.  Then we compress this alist into an array.  Thus, given a rule
we can obtain its nume (because it is a component) and then determine
in constant time whether it is enabled.  The array is never modified
during the proof, i.e., aset1 is never used in this example.  From the
logical perspective this code looks quite odd:  we have replaced a
linear-time membership test with an apparently linear-time assoc after
going to the trouble of mapping from a list of runes to an alist of
numes.  But because the alist of numes is an array, the "apparently
linear-time assoc" is more apparent than real; the operation is
constant-time.

AREF1    access the elements of a 1-dimensional array

     Example Form:
     (aref1 'delta1 a (+ i k))

     General Form:
     (aref1 name alist index)

where name is a symbol, alist is a 1-dimensional array and index is a
legal index into alist.  This function returns the value associated
with index in alist, or else the default value of the array.  See
ARRAYS for details.

This function executes in virtually constant time if alist is in fact
the "semantic value" associated with name (see ARRAYS).  When
it is not, aref1 must do a linear search through alist.  In that case
the correct answer is returned but a *slow array* comment is printed to
the comment window.  See SLOW-ARRAY-WARNING.

AREF2    access the elements of a 2-dimensional array

     Example Form:
     (aref2 'delta1 a i j)

     General Form:
     (aref2 name alist i j)

where name is a symbol, alist is a 2-dimensional array and i and j are
legal indices into alist.  This function returns the value associated
with (i . j) in alist, or else the default value of the array.  See
ARRAYS for details.

This function executes in virtually constant time if alist is in fact
the "semantic value" associated with name (see ARRAYS).  When
it is not, aref2 must do a linear search through alist.  In that case
the correct answer is returned but a *slow array* comment is printed to
the comment window.  See SLOW-ARRAY-WARNING.

ARRAY1P    recognize a 1-dimensional array

     Example Form:
     (array1p 'delta1 a)

     General Form:
     (array1p name alist)

where name and alist are arbitrary objects.  This function returns t if
alist is a 1-dimensional ACL2 array.  Otherwise it returns nil.  The
function operates in constant time if alist is the semantic value of
name.  See ARRAYS.

ARRAY2P    recognize a 2-dimensional array

     Example Form:
     (array2p 'delta1 a)

     General Form:
     (array2p name alist)

where name and alist are arbitrary objects.  This function returns t if
alist is a 2-dimensional ACL2 array.  Otherwise it returns nil.  The
function operates in constant time if alist is the semantic value of
name.  See ARRAYS.

ARRAYS-EXAMPLE    an example illustrating ACL2 arrays

The example below illustrates the use of ACL2 arrays.  It is not, of
course, a substitute for the detailed explanations provided elsewhere
(see ARRAYS, including subtopics).

     ACL2 !>(defun defarray (name size initial-element)
              (compress1 name
                         (cons (list :HEADER
                                     :DIMENSIONS (list size)
                                     :MAXIMUM-LENGTH (1+ size)
                                     :DEFAULT initial-element
                                     :NAME name)
                               nil)))

     Since DEFARRAY is non-recursive, its admission is trivial.  We observe
     that the type of DEFARRAY is described by the theorem
     (AND (CONSP (DEFARRAY NAME SIZE INITIAL-ELEMENT))
          (TRUE-LISTP (DEFARRAY NAME SIZE INITIAL-ELEMENT))).
     We used the :type-prescription rule COMPRESS1.

     Summary
     Form:  ( DEFUN DEFARRAY ...)
     Rules: ((:TYPE-PRESCRIPTION COMPRESS1))
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.02, other: 0.00)
      DEFARRAY
     ACL2 !>(assign my-ar (defarray 'a1 5 17))
      ((:HEADER :DIMENSIONS (5)
                :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
     ACL2 !>(aref1 'a1 (@ my-ar) 3)
     17
     ACL2 !>(aref1 'a1 (@ my-ar) 8)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol AREF1,
     which is
     (AND (ARRAY1P NAME L) (INTEGERP N) (>= N 0) (< N (CAR (DIMENSIONS NAME L)))),
     is violated by the arguments in the call (AREF1 'A1 '(#) 8).

     ACL2 !>(assign my-ar (aset1 'a1 (@ my-ar) 3 'xxx))
      ((3 . XXX)
       (:HEADER :DIMENSIONS (5)
                :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
     ACL2 !>(aref1 'a1 (@ my-ar) 3)
     XXX
     ACL2 !>(aset1 'a1 (@ my-ar) 3 'yyy) ; BAD: (@ my-ar) now points to
                                         ;      an old copy of the array!
     ((3 . YYY)
      (3 . XXX)
      (:HEADER :DIMENSIONS (5)
               :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
     ACL2 !>(aref1 'a1 (@ my-ar) 3) ; Because of "BAD" above, the array
                                    ; access is done using assoc rather
                                    ; than Lisp aref, hence is slower;
                                    ; but the answer is still correct,
                                    ; reflecting the value in (@ my-ar),
                                    ; which was not changed above.

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

     XXX
     ACL2 !>

ASET1    set the elements of a 1-dimensional array

     Example Form:
     (aset1 'delta1 a (+ i k) 27)

     General Form:
     (aset1 name alist index val)

where name is a symbol, alist is a 1-dimensional array named name,
index is a legal index into alist, and val is an arbitrary object.  See
ARRAYS for details.  Roughly speaking this function "modifies"
alist so that the value associated with index is val.  More precisely,
it returns a new array, alist', of the same name and dimension as alist
that, under aref1, is everywhere equal to alist except at index where
the result is val.  That is, (aref1 name alist' i) is (aref1 name alist
i) for all legal indices i except index, where (aref1 name alist' i) is
val.

In order to "modify" alist, aset1 conses a new pair onto the front.  If
the length of the resulting alist exceeds the :maximum-length entry in
the array header, aset1 compresses the array as with compress1.

It is generally expected that the "semantic value" of name will be
alist (see ARRAYS).  This function operates in virtually
constant time whether this condition is true or not (unless the
compress1 operation is required).  But the value returned by this
function cannot be used efficiently by subsequent aset1 operations
unless alist is the semantic value of name when aset1 is executed.
Thus, if the condition is not true, aset1 prints a *slow array* warning
to the comment window.  See SLOW-ARRAY-WARNING.

ASET2    set the elements of a 2-dimensional array

     Example Form:
     (aset2 'delta1 a i j 27)

     General Form:
     (aset2 name alist i j val)

where name is a symbol, alist is a 2-dimensional array named name, i
and j are legal indices into alist, and val is an arbitrary object.
See ARRAYS for details.  Roughly speaking this function
"modifies" alist so that the value associated with (i . j) is val.
More precisely, it returns a new array, alist', of the same name and
dimension as alist that, under aref2, is everywhere equal to alist
except at (i . j) where the result is val.  That is, (aref2 name alist'
x y) is (aref2 name alist x y) for all legal indices x y except i and j
where (aref2 name alist' i j) is val.

In order to "modify" alist, aset2 conses a new pair onto the front.  If
the length of the resulting alist exceeds the :maximum-length entry in
the array header, aset2 compresses the array as with compress2.

It is generally expected that the "semantic value" of name will be
alist (see ARRAYS).  This function operates in virtually
constant time whether this condition is true or not (unless the
compress2 operation is required).  But the value returned by this
function cannot be used efficiently by subsequent aset2 operations
unless alist is the semantic value of name when aset2 is executed.
Thus, if the condition is not true, aset2 prints a *slow array* warning
to the comment window.  See SLOW-ARRAY-WARNING.

COMPRESS1    remove irrelevant pairs from a 1-dimensional array

     Example Form:
     (compress1 'delta1 a)

     General Form:
     (compress1 name alist)

where name is a symbol and alist is a 1-dimensional array named name.
See ARRAYS for details.  Logically speaking, this function
removes irrelevant pairs from alist, possibly shortening it.  The
function returns a new array, alist', of the same name and dimension as
alist, that, under aref1, is everywhere equal to alist.  That is,
(aref1 name alist' i) is (aref1 name alist i), for all legal indices i.
Alist' may be shorter than alist and the non-irrelevant pairs may
occur in a different order than in alist.

Practically speaking, this function plays an important role in the
efficient implementation of aref1.  In addition to creating the new
array, alist', compress1 makes that array the "semantic value" of name
and allocates a raw lisp array to name.  For each legal index, i, that
raw lisp array contains (aref1 name alist' i) in slot i.  Thus,
subsequent aref1 operations can be executed in virtually constant time
provided they are given name and the alist' returned by the most
recently executed compress1 or aset1 on name.  See ARRAYS.

In general, compress1 returns an alist whose cdr is an association list
whose keys are nonnegative integers in ascending order.  However, if the
header specifies an :order of > then the keys will occur in descending
order, and if the :order is :none or nil then the keys will not be
sorted, i.e., compress1 is logically the identity function (though it
still attaches an array under the hood).  Note however that a compress1
call is replaced by a hard error if the header specifies an :order of
:none or nil and the array's length exceeds the maximum-length field of
its header.

COMPRESS2    remove irrelevant pairs from a 2-dimensional array

     Example Form:
     (compress2 'delta1 a)

     General Form:
     (compress2 name alist)

where name is a symbol and alist is a 2-dimensional array named name.
See ARRAYS for details.  Logically speaking, this function
removes irrelevant pairs from alist, possibly shortening it.  The
function returns a new array, alist', of the same name and dimension as
alist, that, under aref2, is everywhere equal to alist.  That is,
(aref2 name alist' i j) is (aref2 name alist i j), for all legal
indices i and j.  Alist' may be shorter than alist and the
non-irrelevant pairs may occur in a different order in alist' than in
alist.

Practically speaking, this function plays an important role in the
efficient implementation of aref2.  In addition to creating the new
array, alist', compress2 makes that array the "semantic value" of name
and allocates a raw lisp array to name.  For all legal indices, i and
j, that raw lisp array contains (aref2 name alist' i j) in slot i,j.
Thus, subsequent aref2 operations can be executed in virtually constant
time provided they are given name and the alist' returned by the most
recently executed compress2 or aset2 on name.  See ARRAYS.

DEFAULT    return the :default from the header of a 1- or 2-dimensional array

     Example Form:
     (default 'delta1 a)

     General Form:
     (default name alist)

where name is an arbitrary object and alist is a 1- or 2-dimensional
array.  This function returns the contents of the :default field of the
header of alist.  When aref1 or aref2 is used to obtain a value for an
index (or index pair) not bound in alist, the default value is returned
instead.  Thus, the array alist may be thought of as having been
initialized with the default value.  default operates in virtually
constant time if alist is the semantic value of name.  See
ARRAYS.

DIMENSIONS    return the :dimensions from the header of a 1- or 2-dimensional array

     Example Form:
     (dimensions 'delta1 a)

     General Form:
     (dimensions name alist)

where name is arbitrary and alist is a 1- or 2-dimensional array.  This
function returns the dimensions list of the array alist.  That list
will either be of the form (dim1) or (dim1 dim2), depending on whether
alist is a 1- or 2-dimensional array.  Dim1 and dim2 will be integers
and each exceed by 1 the maximum legal corresponding index.  Thus, if
dimensions returns, say, '(100) for an array a named 'delta1, then
(aref1 'delta1 a 99) is legal but (aref1 'delta1 a 100) violates the
guards on aref1.  Dimensions operates in virtually constant time if
alist is the semantic value of name.  See ARRAYS.

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

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

     General Form:
     (flush-compress name)

where name is a symbol.

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

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

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

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

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

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

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

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

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

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

     Example Form:
     (header 'delta1 a)

     General Form:
     (header name alist)

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

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

     Example Form:
     (maximum-length 'delta1 a)

     General Form:
     (maximum-length name alist)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Of course, this may not mean the same thing.

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

BACKCHAIN-LIMIT    limiting the effort expended on relieving hypotheses

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

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

Moreover, the user may set a global backchain-limit that limits the
total backchaining depth.  See SET-BACKCHAIN-LIMIT.  Below we
lay out the precise sense in which this global backchain-limit interacts
with the backchain-limits of individual rules in order to limit
backchaining.  But first we note that when further backchaining is
disallowed, ACL2 can still prove a hypothesis in a given context by
using that contextual information.  This process is sometimes called
"type-set reasoning," an appropriate term since rules of class
:type-prescription may be used.  So, for example, the relieving of
hypotheses may be limited to the use of contextual information (without
backchaining, i.e., without recursively rewriting hypotheses) by
executing :set-backchain-limit 0.

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

We illustrate with the following examples.

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

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

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

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

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

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

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

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

     ; We set the default-backchain-limit to 1.

     :set-default-backchain-limit 1

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

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

     ; This theorem will succeed:

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

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

     :set-default-backchain-limit nil

     ; Here is our last axiom.

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

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

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

BACKTRACK    hints keyword :BACKTRACK

See HINTS.

BIBLIOGRAPHY    reports about ACL2

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

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

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

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

General Forms:

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

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

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

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

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

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

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

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

Consider the following definitions and theorem:

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

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

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

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

How is this rule applied to the following term?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

EXAMPLE 1:  Cancel a common factor.

     (defun bind-divisor (a b)

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

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

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

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

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

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

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

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

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

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

     (in-theory (disable fl))

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

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

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

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

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

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

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

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

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

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

BREAKS    Common Lisp breaks

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

     ACL2 !>

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

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

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

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

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

BY    hints keyword :BY

See HINTS.

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

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

For example, given the rule

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

then an attempt to prove

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

can give rise to a single subgoal:

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

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

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

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

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

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

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

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

CASES    hints keyword :CASES

See HINTS.

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

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

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

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

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

CLAUSE-IDENTIFIER    the internal form of a goal-spec

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

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

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

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

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

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

                  parse-clause-id
                        -->

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

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

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

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

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

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

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

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

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

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

     Examples:

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

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

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

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

      command                   command
     descriptor                described

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

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

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

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

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

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

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

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

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

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

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

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

For example, suppose you make the following defun:

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

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

     ACL2 !>(crash 7)

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

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

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

Furthermore

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

Finally,

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

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

GENERALIZED-BOOLEANS    potential soundness issues related to ACL2 predicates

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

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

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

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

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

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

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

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

COMPUTED-HINTS    computing advice to the theorem proving process

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

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

A common hint is of the form

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

CONSTRAINT    restrictions on certain functions introduced in encapsulate events

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

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

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

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

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

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

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

Finally, before we start our "first cut," we note that constrained
functions always have guards of T.  This makes sense when one considers
that a constrained function's "guard" only appears in the context of a
local defun, which is skipped.  Note also that any information you want
"exported" outside an encapsulate event must be there as an explicit
definition or theorem.  For example, even if a function foo has output
type (mv t t) in its signature, the system will not know (true-listp
(foo x)) merely on account of this information.  Thus, if you are using
functions like foo (constrained mv functions) in a context where you
are verifying guards, then you should probably provide a
:type-prescription rule for the constrained function, for example, the
:type-prescription rule (true-listp (foo x)).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      (defun before2 (x)
        (before1 x))

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

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

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

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

Only the functions sig-fn and during receive extra constraints.  The
functions before1 and before2 are viewed as moving in front of the
encapsulate, as is the theorem before2-prop.  The functions after1 and
after2 are viewed as being moved past the encapsulate.  Notice that the
formula (consp (during x)) is a conjunct of the constraint.  It comes
from the :type-prescription rule deduced during the definition of the
function during.  The implementation reports the following.

     (SIG-FN X) is axiomatized to return one result.

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

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

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

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

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

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

     ; The following event is not admissible in ACL2.

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

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

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

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

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

     ; The following event is not admissible in ACL2.

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

COPYRIGHT    ACL2 copyright, license, sponsorship

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

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

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

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

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

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

Please also see ACKNOWLEDGMENTS.

COROLLARY    the corollary formula of a rune

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

CURRENT-PACKAGE    the package used for reading and printing

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

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

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

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

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

CUSTOM-KEYWORD-HINTS    user-defined hints

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

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

See BACKCHAIN-LIMIT.

The initial value is nil.

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

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

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

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

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

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

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

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

DEFAULT-PRINT-PROMPT    the default prompt printed by ld

     Example prompt:
     ACL2 p!s>

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

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

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

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

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

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

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

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

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

     ACL2 P>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     ACL2 !>(fact 3)

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

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

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

     (verify-termination fact)

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

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

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

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

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

DEFUNS    an alternative to mutual-recursion

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

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

is equivalent to

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

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

DISABLE-FORCING    to disallow forced case-splits

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

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

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

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

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

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

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

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

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

DISABLEDP    determine whether a given name or rune is disabled

     Examples:

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

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

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

DO-NOT    hints keyword :DO-NOT

See HINTS.

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

See HINTS.

DOUBLE-REWRITE    cause a term to be rewritten twice

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*Suggesting congruence rules.*

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

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

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

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

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

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

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

*Details on double-rewrite.*

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

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

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

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

     (g (h1 a))

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

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

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

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

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

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

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

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

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

     (thm (foo (bar y)))

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

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

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

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

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

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

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

     x is of the form (WITH-OUTPUT ... x1) where x1 is an   embedded
     event form;

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

     x macroexpands to one of the forms above; or

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

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

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

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

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

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

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

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

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

_Discussion:_

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

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

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

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

followed by

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

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

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

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

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

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

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

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

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

ENABLE-FORCING    to allow forced splits

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

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

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

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

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

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

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

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

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

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

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

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

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

ESCAPE-TO-COMMON-LISP    escaping to Common Lisp

     Example:
     ACL2 !>:Q

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