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

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

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

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

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

THE    run-time type check

(The typ val) checks that val satisfies the type specification typ (see
TYPE-SPEC).  An error is caused if the check fails, and
otherwise, val is the value of this expression.  Here are some examples.

     (the integer 3)       ; returns 3
     (the (integer 0 6) 3) ; returns 3
     (the (integer 0 6) 7) ; causes an error

See TYPE-SPEC for a discussion of the legal type specifications.

The following remark is for those who verify guards for their functions
(see GUARD and see VERIFY-GUARDS).  We remark that a
call of (the TYPE EXPR) in the body of a function definition generates
a guard proof obligation that the type, TYPE, holds for the value of the
expression, EXPR.  Consider the following example.

     (defun f (x)
       (declare (xargs :guard (p1 x)))
       (if (p2 x)
           (the integer x)
         17))

The guard proof obligation generated for the THE expression above is as
follows.

     (implies (and (p1 x) (p2 x))
              (integerp x))

THE is defined in Common Lisp.  See any Common Lisp documentation for
more information.

THIRD    third member of the list

See any Common Lisp documentation for details.

TIME$    time an evaluation

Semantically, (time$ x ...) equals x.  However, its evaluation may
write timing output to the trace output (which is usually the
terminal), as explained further below.

     Examples:

     ; Basic examples:

     (time$ (foo 3 4))
     (time$ (mini-proveall))
     (defun bar (x) (time$ (f x)))

     ; Custom examples, which use a custom timing message rather than a built-in
     ; message from Lisp:

     ; Report only if real time is at least 1/2 second (two equivalent forms).
     (time$ (foo) :mintime 1/2)
     (time$ (foo) :real-mintime 1/2)

     ; Report only if allocation is at least 1000 bytes (and if the Lisp supports
     ; :minalloc).
     (time$ (foo) :minalloc 1000)

     ; Report only if real time is at least 1/2 second and (if the Lisp supports
     ; :minalloc) allocation is at least 931 bytes.
     (time$ (foo) :real-mintime 1/2 :minalloc 931)

     ; Print "Hello Moon, Goodbye World" instead of any timing data.
     (time$ (foo)
            :msg "Hello ~s0, ~s1 World."
            :args (list "Moon" "Goodbye"))

     ; Print default custom timing message (same as omitting :mintime 0):
     (time$ (foo)
            :mintime 0)

     ; Print supplied custom timing message.
     (let ((bar ...))
       (time$ (foo)
              :msg "The execution of ~xf took ~st seconds of real ~
                    time and ~sc seconds of run time (cpu time), and ~
                    allocated ~sa bytes.  In an unrelated note, bar ~
                    currently has the value ~x0.~%"
              :args (list bar)))

     General Forms:
     (time$ form)
     (time$ form ; arguments below are optional
            :real-mintime  <rational number of seconds>
            :run-mintime   <rational number of seconds>
            :minalloc      <number of bytes>
            :msg           <fmt string>
            :args          <list of arguments for msg>
            )
     ; Note: :real-mintime can be replaced by :mintime

where form is processed as usual except that the host Common Lisp times
its evaluation.

The simplest form is (time$ x), which will call the time utility in the
underlying Lisp, and will print a small default message.  If you want to
see a message printed by the host Lisp, use (time$ x :mintime nil)
instead, which may provide detailed, implementation-specific data such
as the amounts of time spent in user and system mode, the gc time, the
number of page faults encountered, and so on.  Of you can create a
custom message, configured using the :msg and :args parameters.  Time$
can also be made to report timing information only conditionally: the
:real-mintime (or equivalently, :mintime), :run-mintime, and :minalloc
arguments can be used to avoid reporting timing information for
computations that take a small amount of time (perhaps as might be
expected in ordinary cases), but to draw the user's attention to
computations that take longer or allocate more memory than expected.

We next document the keyword arguments in some detail.

     Keyword arguments :real-mintime (or :mintime) and :run-mintime can
     be used to specify a minimum time threshold for time reporting.
     That is, no timing information will be printed if the execution of
     form takes less than the specified number of seconds of real
     (total) time or run (cpu) time, respectively.  Note that rational
     numbers like 1/2 may be used to specify a fractional amount of
     seconds.  It is an error to specify both :real-mintime and its
     synonym, :mintime.

     Keyword argument :minalloc is not supported on all Lisps.  When it
     is not supported, it is ignored.  But on supported Lisps,
     :minalloc can be used to specify a minimum memory allocation
     threshold.  If form results in fewer than this many bytes being
     allocated, then no timing information will be reported.

     Keyword argument :msg, when provided, should be a string accepted
     by the fmt family of functions (see FMT), and it may refer
     to the elements of :args by their positions, just as for cw (see
     CW).

The following directives allow you to report timing information using
the :msg string.  The examples at the top of this documentation topic
illustrate the use of these directives.

     ~xf -- the form that was executed

     ~sa -- the amount of memory allocated, in bytes (in supported
     Lisps)

     ~st -- the real time taken, in seconds

     ~sc -- the run time (cpu time) taken, in seconds

We turn now to an example that illustrates how time$ can be called in
function bodies.  Consider the following definition of the Fibonacci
function, followed by the definition of a function that times k calls of
this function.

     (defun fib (n)
       (if (zp n)
           1
         (if (= n 1)
             1
           (+ (fib (- n 1))
              (fib (- n 2))))))

     (defun time-fib (k)
       (if (zp k)
           nil
         (prog2$
          (time$ (fib k)
                 :mintime 1/2
                 :msg "(fib ~x0) took ~st seconds, ~sa bytes allocated.~%"
                 :args (list k))
          (time-fib (1- k)))))

The following log shows a sample execution of the function defined just
above.

     ACL2 !>(time-fib 36)
     (fib 36) took 3.19 seconds, 1280 bytes allocated.
     (fib 35) took 1.97 seconds, 1280 bytes allocated.
     (fib 34) took 1.21 seconds, 1280 bytes allocated.
     (fib 33) took 0.75 seconds, 1280 bytes allocated.
     NIL
     ACL2 !>

Notes:

(1) Common Lisp specifies that the time utility prints to "trace
output", and time$ follows this convention.  Thus, if you have opened a
trace file (see OPEN-TRACE-FILE), then you can expect to find
the time$ output there.

(2) Unless the :msg argument is supplied, an explicit call of time$ in
the top-level loop will show that the form being timed is a call of the
ACL2 evaluator function ev-rec.  This is normal; the curious are
invited, at their own risk, to see RETURN-LAST for an
explanation.

TRUE-LIST-LISTP    recognizer for true (proper) lists of true lists

True-list-listp is the function that checks whether its argument is a
list that ends in, or equals, nil, and furthermore, all of its elements
have that property.  Also see TRUE-LISTP.

To see the ACL2 definition of this function, see PF.

TRUE-LISTP    recognizer for proper (null-terminated) lists

True-listp is the function that checks whether its argument is a list
that ends in, or equals, nil.

To see the ACL2 definition of this function, see PF.

TRUNCATE    division returning an integer by truncating toward 0

     Example Forms:
     ACL2 !>(truncate 14 3)
     4
     ACL2 !>(truncate -14 3)
     -4
     ACL2 !>(truncate 14 -3)
     -4
     ACL2 !>(truncate -14 -3)
     4
     ACL2 !>(truncate -15 -3)
     5
     ACL2 !>(truncate 10/4 3/4)
     3

(Truncate i j) is the result of taking the quotient of i and j and
dropping the fraction.  For example, the quotient of -14 by 3 is -4
2/3, so dropping the fraction 2/3, we obtain a result for (truncate -14
3) of -4.

The guard for (truncate i j) requires that i and j are rational (real,
in ACL2(r)) numbers and j is non-zero.

Truncate is a Common Lisp function.  However, note that unlike Common
Lisp, the ACL2 truncate function returns only a single value,  Also see
NONNEGATIVE-INTEGER-QUOTIENT, which is appropriate for integers
and may simplify reasoning, unless a suitable arithmetic library is
loaded, but be less efficient for evaluation on concrete objects.

To see the ACL2 definition of this function, see PF.

UNARY-    arithmetic negation function

Completion Axiom (completion-of-unary-minus):

     (equal (unary-- x)
            (if (acl2-numberp x)
                (unary-- x)
              0))

Guard for (unary- x):

     (acl2-numberp x)

Notice that like all arithmetic functions, unary- treats non-numeric
inputs as 0.

Calls of the macro - on one argument expand to calls of unary-; see
-.

UNARY-/    reciprocal function

Completion Axiom (completion-of-unary-/):

     (equal (unary-/ x)
            (if (and (acl2-numberp x)
                     (not (equal x 0)))
                (unary-/ x)
              0))

Guard for (unary-/ x):

     (and (acl2-numberp x)
          (not (equal x 0)))

Notice that like all arithmetic functions, unary-/ treats non-numeric
inputs as 0.

Calls of the macro / on one argument expand to calls of unary-/; see
/.

UNION$    elements of one list that are not elements of another

     General Forms:
     (union$ l1 l2 ... lk)
     (union$ l1 l2 ... lk :test 'eql) ; same as above
     (union$ l1 l2 ... lk :test 'eq)    ; same, but eq is equality test
     (union$ l1 l2 ... lk :test 'equal) ; same, but equal is equality test

(Union$ x y) equals a list that contains both the members of x and the
members of y.  More precisely, the resulting list is the same as one
would get by first deleting the members of y from x, and then
concatenating the result to the front of y.  The optional keyword,
:TEST, has no effect logically, but provides the test (default eql)
used for comparing members of the two lists.

Union$ need not take exactly two arguments: (union$) is nil, (union$ x)
is x, (union$ x y z ... :test test) is (union$ x (union$ y z ... :test
test) :test test), and if :TEST is not supplied, then (union$ x y z
...) is (union$ x (union$ y z ...)).  For the discussion below we
restrict ourselves, then, to the cases (union$ x y) and (union$ x y
:test test).

The guard for a call of union$ (in the two cases just above) depends on
the test.  In all cases, both arguments must satisfy true-listp.  If
the test is eql, then one of the arguments must satisfy eqlable-listp.
If the test is eq, then one of the arguments must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
union$ and its variants:

     (union-eq x lst) is equivalent to (union$ x lst :test 'eq);

     (union-equal x lst) is equivalent to (union$ x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to
reasoning about the function union-equal.

Note that union-eq can take any number of arguments, in analogy to
union$; indeed, (union-eq ...) expands to (union$ ... :test 'eq).
However, union-equal is a function, not a macro, and takes exactly two
arguments.

Union$ is similar to the Common Lisp primitive union.  However, Common
Lisp does not specify the order of elements in the result of a call of
union.

UNION-EQ    See UNION$.

UNION-EQUAL    See UNION$.

UNTRANSLATE    See USER-DEFINED-FUNCTIONS-TABLE.

UPDATE-NTH    modify a list by putting the given value at the given position

(Update-nth key val l) returns a list that is the same as the list l,
except that the value at the 0-based position key (a natural number) is
val.

If key is an integer at least as large as the length of l, then l will
be padded with the appropriate number of nil elements, as illustrated
by the following example.

     ACL2 !>(update-nth 8 'z '(a b c d e))
     (A B C D E NIL NIL NIL Z)

We have the following theorem.

     (implies (and (true-listp l)
                   (integerp key)
                   (<= 0 key))
              (equal (length (update-nth key val l))
                     (if (< key (length l))
                         (length l)
                       (+ 1 key))))

The guard of update-nth requires that its first (position) argument is
a natural number and its last (list) argument is a true list.

To see the ACL2 definition of this function, see PF.

UPPER-CASE-P    recognizer for upper case characters

(Upper-case-p x) is true if and only if x is an upper case character,
i.e., a member of the list #\A, #\B, ..., #\Z.

The guard for upper-case-p requires its argument to be a standard
character (see STANDARD-CHAR-P).

Upper-case-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

To see the ACL2 definition of this function, see PF.

WITH-LIVE-STATE    allow a reference to state in raw Lisp

The macro with-live-state is an advanced feature that very few users
will need (basically, only system hackers).  Indeed, it is untouchable;
see REMOVE-UNTOUCHABLE for how to enable calling
with-live-state in the ACL2 loop.

     Example Form:
     (with-live-state (assign y 3))

     General form:
     (with-live-state form)

where form is an arbitrary form with a free reference to the variable
state.

Logically, (with-live-state FORM) macroexpands to FORM.  However, in
raw Lisp it expands to:

     (let ((state *the-live-state*))
       FORM)

If a form that mentions the variable state might be executed in raw
Lisp -- that is, either outside the ACL2 loop or in raw mode (see
SET-RAW-MODE) -- then the surrounding the form with with-live-state
as shown above can avoid potential warnings or (much less likely)
errors.  Note however that if state is lexically bound to a state other
than the usual "live" state, surprising behavior may occur when
evaluating a call of with-live-state in raw Lisp or raw mode (either
directly by evaluation or at compile time), because with-live-state will
override that lexical binding of state by a lexical binding of state to
the usual "live" state.

WRITE-BYTE$    See IO.

XOR    logical "exclusive or"

Xor is the ACL2 exclusive-or function.  (xor P Q) means that either P
or Q, but not both, is false (i.e., nil).

To see the ACL2 definition of this function, see PF.

ZEROP    test an acl2-number against 0

(zerop x) is t if x is 0 and is nil otherwise.  Thus, it is logically
equivalent to (equal x 0).

(Zerop x) has a guard requiring x to be numeric and can be expected to
execute more efficiently than (equal x 0) in properly guarded compiled
code.

In recursions down the natural numbers, (zp x) is preferred over (zerop
x) because the former coerces x to a natural and allows the termination
proof.  In recursions through the integers, (zip x) is preferred.  See
ZERO-TEST-IDIOMS.

Zerop is a Common Lisp function.  See any Common Lisp documentation for
more information.

To see the ACL2 definition of this function, see PF.

ZIP    testing an "integer" against 0

(Zip i) is logically equivalent to (equal (ifix i) 0) and is the
preferred termination test for recursion through the integers.  (Zip i)
returns t if i is 0 or not an integer; it returns nil otherwise.  Thus,

        i         (zip i)
        3         nil
        0         t
        -2        nil
        5/2       t
        #c(1 3)   t
        'abc      t

(Zip i) has a guard requiring i to be an integer.

For a discussion of the various idioms for testing against 0, see
ZERO-TEST-IDIOMS.

Zip is typically used as the termination test in recursions through the
integers.  It has the advantage of "coercing" its argument to an
integer and hence allows the definition to be admitted without an
explicit type check in the body.  Guard verification allows zip to be
compiled as a direct =-comparision with 0.

ZP    testing a "natural" against 0

(Zp n) is logically equivalent to (equal (nfix n) 0) and is the
preferred termination test for recursion down the natural numbers. (Zp
n) returns t if n is 0 or not a natural number; it returns nil
otherwise.  Thus, in the ACL2 logic (ignoring the issue of guards):

         n       (zp n)
        3         nil
        0         t
        -1        t
        5/2       t
        #c(1 3)   t
        'abc      t

(Zp n) has a guard requiring n to be a natural number.

For a discussion of the various idioms for testing against 0, see
ZERO-TEST-IDIOMS.

Zp is typically used as the termination test in recursions down the
natural numbers.  It has the advantage of "coercing" its argument to a
natural and hence allows the definition to be admitted without an
explicit type check in the body.  Guard verification allows zp to be
compiled as a direct =-comparision with 0.

ZPF    testing a nonnegative fixnum against 0

Zpf is exactly the same as zp, except that zpf is intended for, and
faster for, fixnum arguments.  Its guard is specified with a type
declaration, (type (unsigned-byte 29) x).  (See DECLARE and see
TYPE-SPEC.)  Also see ZP.

To see the ACL2 definition of this function, see PF.

ACL2-USER    a package the ACL2 user may prefer

This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are commonly
used when interacting with ACL2.  You may prefer to select this as your
current package so as to avoid colliding with ACL2 system names.

This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains hundreds
of CLTL function and macro names including those supported by ACL2 such
as cons, car, and cdr.  It also imports the symbols in *acl2-exports*,
which contains a few symbols that are frequently used while interacting
with the ACL2 system, such as implies, defthm, and rewrite.  It imports
nothing else.

Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here.  If you find
yourself frequently colliding with names that are defined in "ACL2" you
might consider selecting "ACL2-USER" as your current package (see
IN-PACKAGE).  If you select "ACL2-USER" as the current package, you
may then simply type member-equal to refer to acl2-user::member-equal,
which you may define as you see fit.  Of course, should you desire to
refer to the "ACL2" version of member-equal, you will have to use the
"ACL2::" prefix, e.g., acl2::member-equal.

If, while using "ACL2-USER" as the current package, you find that there
are symbols from "ACL2" that you wish we had imported into it (because
they are frequently used in interaction), please bring those symbols to
our attention.  For example, should union-theories and universal-theory
be imported?  Except for stabilizing on the "frequently used" names
from "ACL2", we intend never to define a symbol whose
symbol-package-name is "ACL2-USER".

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.

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, generally
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', with the same header
(including 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, generally
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', with the same header
(including 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 it 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.

COMPILATION    compiling ACL2 functions

ACL2 has several mechanisms to speed up the evaluation of function
calls by _compiling_ functions: see COMP, see
SET-COMPILE-FNS, and see CERTIFY-BOOK.  The intention is that
compilation never changes the value returned by a function call, though
it could cause the call to succeed rather than fail, for example by
avoiding a stack overflow.

The state global variable 'compiler-enabled is set automatically when
the system is built, and may depend on the underlying Lisp
implementation.  (In order to disable the compiler at build time, which
will defeat the speed-up but usually be pretty harmless when the host
Lisp is CCL or SBCL, see the discussion of ACL2_COMPILER_DISABLED in
distributed file GNUmakefile.)  The value of 'compiler-enabled, as
returned by (@ compiler-enabled), can be t, :books, or nil.  If the
value is nil, then include-book and certify-book coerce their arguments
:load-compile-file and compile-flg arguments (respectively) to nil.
Otherwise, the value is :books or t and there is no such coercion; but
if the value is not t, then comp and set-compile-fns are no-ops, which
is probably desirable for Lisps such as CCL and SBCL that compile
on-the-fly even when the compiler is not explicitly invoked.

However, you may have reason to want to change the above (default)
behavior.  To enable compilation by default for certify-book and
include-book but not for comp or set-compile-fns:

     (set-compiler-enabled :books state)

To enable compilation not only as above but also for comp and
set-compile-fns:

     (set-compiler-enabled t state)

To suppress compilation and loading of compiled files by include-book:

     (set-compiler-enabled nil state)

See BOOK-COMPILED-FILE for more discussion about compilation and
books.

DECLARE    declarations

     Examples:
     (declare (ignore x y z))
     (declare (ignorable x y z)
              (type integer i j k)
              (type (satisfies integerp) m1 m2))
     (declare (xargs :guard (and (integerp i)
                                 (<= 0 i))
                     :guard-hints (("Goal" :use (:instance lemma3
                                                   (x (+ i j)))))))

     * Menu:

     * TYPE-SPEC:: type specifiers in declarations

     General Form:
     (declare d1 ... dn)
     where, in ACL2, each di is of one of the following forms:

       (ignore v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables must not
       occur free in the scope of the declaration.

       (ignorable v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables need not
       occur free in the scope of the declaration.  This declaration can be useful
       for inhibiting compiler warnings.

       (type type-spec v1 ... vn) -- where each vi is a variable introduced in the
       immediately superior lexical environment and type-spec is a type specifier
       (as described in the documentation for type-spec).

       (xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's
       and their respective vali's are described in the documentation for
       xargs.

       (optimize ...) -- for example, (optimize (safety 3)).  This is allowed
       only at the top level of defun forms.  See any Common Lisp
       documentation for more information.

Declarations in ACL2 may occur only where dcl occurs below:

       (DEFUN name args doc-string dcl ... dcl body)
       (DEFMACRO name args doc-string dcl ... dcl body)
       (LET ((v1 t1) ...) dcl ... dcl body)
       (MV-LET (v1 ...) term dcl ... dcl body)

Of course, if a form macroexpands into one of these (as let* expands
into nested lets and our er-let* expands into nested mv-lets) then
declarations are permitted as handled by the macros involved.

Declare is defined in Common Lisp.  See any Common Lisp documentation
for more information.

TYPE-SPEC    type specifiers in declarations

     Examples:
     The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec.  Other
     type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127),
     (RATIONAL 1 *), CHARACTER, and ATOM.

The type-specs and their meanings (when applied to the variable x as in
(declare (type type-spec x)) are given below.

     type-spec              meaning
     (AND type1 ... typek)  (AND (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     ATOM                   (ATOM X)
     BIT                    (OR (EQUAL X 1) (EQUAL X 0))
     CHARACTER              (CHARACTERP X)
     COMPLEX                (AND (COMPLEX-RATIONALP X)
                                 (RATIONALP (REALPART X))
                                 (RATIONALP (IMAGPART X)))
     (COMPLEX RATIONAL)     same as COMPLEX, above
     (COMPLEX type)         (AND (COMPLEX-RATIONALP X)
                                 (p (REALPART X))
                                 (p (IMAGPART X)))
                            where (p x) is the meaning for type-spec type
     CONS                   (CONSP X)
     INTEGER                (INTEGERP X)
     (INTEGER i j)          (AND (INTEGERP X)   ; See notes below
                                 (<= i X)
                                 (<= X j))
     (MEMBER x1 ... xn)     (MEMBER X '(x1 ... xn))
     (MOD i)                same as (INTEGER 0 i-1)
     NIL                    NIL
     (NOT type)             (NOT (p X))
                            where (p x) is the meaning for type-spec type
     NULL                   (EQ X NIL)
     (OR type1 ... typek)   (OR (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     RATIO                  (AND (RATIONALP X) (NOT (INTEGERP X)))
     RATIONAL               (RATIONALP X)
     (RATIONAL i j)         (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     REAL                   (RATIONALP X)       ; (REALP X) in ACL2(r)
     (REAL i j)             (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     (SATISFIES pred)       (pred X) ; Lisp requires a unary function, not a macro
     SIGNED-BYTE            (INTEGERP X)
     (SIGNED-BYTE i)        same as (INTEGER k m) where k=-2^(i-1), m=2^(i-1)-1
     STANDARD-CHAR          (STANDARD-CHARP X)
     STRING                 (STRINGP X)
     (STRING max)           (AND (STRINGP X) (EQUAL (LENGTH X) max))
     SYMBOL                 (SYMBOLP X)
     T                      T
     UNSIGNED-BYTE          same as (INTEGER 0 *)
     (UNSIGNED-BYTE i)      same as (INTEGER 0 (2^i)-1)

_Notes:_

In general, (integer i j) means

          (AND (INTEGERP X)
               (<= i X)
               (<= X j)).

But if i is the symbol *, the first inequality is omitted.  If j is the
symbol *, the second inequality is omitted.  If instead of being an
integer, the second element of the type specification is a list
containing an integer, (i), then the first inequality is made strict.
An analogous remark holds for the (j) case.  The RATIONAL and REAL type
specifiers are similarly generalized.

EQUALITY-VARIANTS    versions of a function using different equality tests

The ACL2 environment includes not only a logic but also a programming
language, which is based on Common Lisp.  Execution efficiency may be
increased by using fast equality tests: eq for symbols and eql for
numbers, symbols, and characters (see EQLABLEP).  Several
list-processing functions built into ACL2 thus have three variants,
depending on whether the equality function used is eq, eql, or equal; a
list is provided below.  ACL2 has taken measures to ensure that one can
reason about a single logical function even when one uses these
different variants.

Consider for example the case of list membership.  Common Lisp provides
a utility for this purposes, member, which can take a :TEST keyword
argument, default eql.  So for example, one might write

     (member a x :TEST 'eq)

if either a is a symbol or x is a list of symbols, so that the fastest
equality test (eq) may be used when comparing a to successive elements
of the list, x.  One might elsewhere write (member b (foo y)), which is
equivalent to (member b (foo y) :TEST 'eql), for example if b is a
number.  If one wants to reason about both (member a x :TEST 'eq) and
(member b y), it might be helpful for both calls of member to be the
same logically, even though Common Lisp will execute them differently
(using eq or eql, respectively).  ACL2 arranges that in fact, both
references to member generate calls of member-equal in the theorem
prover.

In fact, since member can take the optional :TEST keyword argument,
then in ACl2 it must be defined as a macro, not a function (see
DEFUN).  ACL2 arranges that a call of member generates a
corresponding call of the function member-equal, regardless of the
value of TEST, in a manner that produces member-equal in prover output.
More generally, you can expect ACL2 to treat your use of member as
though you had written member-equal, for example in the way it stores
rewrite rules and other kinds of rules as well (see
RULE-CLASSES).  We say little here about how this is all arranged by
ACL2, other than to mention that mbe is utilized (so, you might see
mention in proof logs) of the function return-last that implements mbe.
Such details, which probably can be ignored by most users, may be found
elsewhere; see EQUALITY-VARIANTS-DETAILS.

As a convenience to the user, the macro member-eq is provided that
expands to a corresponding call of member with :TEST 'eq, as follows.

     ACL2 !>:trans1 (member-eq (foo x) (bar y))
      (MEMBER (FOO X) (BAR Y) :TEST 'EQ)
     ACL2 !>

For efficiency we recommend using the -equal equality variant, for
example member-equal or ... :TEST 'equal, in certain contexts:
defmacro, defpkg, defconst, and value-triple forms.  However, the
implementation of equality variants has been designed so that when
defining a function, one may choose freely in a definition an equality
variant of primitive F, to get efficient execution but where subsequent
reasoning is about F-equal.  For details about the above recommendation
and for a discussion of the implementation, see
EQUALITY-VARIANTS-DETAILS.

The following alphabetical list includes all primitives that have
equality variants.  Each macro F listed below takes an optional :TEST
keyword argument of 'eq, 'eql, or 'equal, where 'eql is the default.
For each such F, a function F-equal is defined such that for logical
purposes (in particular theorem proving), each call of F expands to a
corresponding call of F-equal.  For convenience, a macro F-eq is also
defined, so that a call of F-eq expands to a corresponding call of F
with :TEST 'eq.

     add-to-set
     assoc
     delete-assoc
     intersection$ ; (see Note below)
     intersectp
     member
     no-duplicatesp
     position-ac
     position
     put-assoc
     rassoc
     remove-duplicates
     remove1
     remove
     set-difference$ ; (see Note below)
     subsetp
     union$ ; (see Note below)

Note: Three of the macros above have names ending with the character,
`$': intersection$, set-difference$, and union$.  In each case there is
a corresponding Common Lisp primitive without the trailing `$':
intersection, set-difference, and union.  However, Common Lisp does not
specify the order of elements in the list returned by those primitives,
so ACL2 has its own.  Nevertheless, the only use of the trailing `$' is
to distinguish the primitives; associated functions and macros, for
example union-eq and intersection-equal, do not include the `$'
character in their names.

EQUALITY-VARIANTS-DETAILS    details about equality-variants

Here we present details about equality variants, none of which is likely
to be important to the majority of ACL2 users.  Please see
EQUALITY-VARIANTS for relevant background.

We begin by presenting events that implement the equality variants for
member, as these illustrate the events introduced for all macros having
equality variants.  The definition of member, just below, calls the
macro let-mbe, which in turn is just an abbreviation for a combination
of let and mbe.

     (defmacro let-mbe (bindings &key logic exec)
       `(let ,bindings
          (mbe :logic ,logic
               :exec ,exec)))

This use of let arranges that each argument of a call of member is
evaluated only once.

     (defmacro member (x l &key (test ''eql))
       (declare (xargs :guard (or (equal test ''eq)
                                  (equal test ''eql)
                                  (equal test ''equal))))
       (cond
        ((equal test ''eq)
         `(let-mbe ((x ,x) (l ,l))
                   :logic (member-equal x l)
                   :exec  (member-eq-exec x l)))
        ((equal test ''eql)
         `(let-mbe ((x ,x) (l ,l))
                   :logic (member-equal x l)
                   :exec  (member-eql-exec x l)))
        (t ; (equal test 'equal)
         `(member-equal ,x ,l))))

Inspection of the definition above shows that every call of member
expands to one that is logically equivalent to the corresponding call of
member-equal, which is defined as follows.

     (defun member-equal (x lst)
       (declare (xargs :guard (true-listp lst)))
       (cond ((endp lst) nil)
             ((equal x (car lst)) lst)
             (t (member-equal x (cdr lst)))))

The following two definitions model equality variants of member for
tests eq and eql, respectively.

     (defun member-eq-exec (x lst)
       (declare (xargs :guard (if (symbolp x)
                                  (true-listp lst)
                                (symbol-listp lst))))
       (cond ((endp lst) nil)
             ((eq x (car lst)) lst)
             (t (member-eq-exec x (cdr lst)))))

     (defun member-eql-exec (x lst)
       (declare (xargs :guard (if (eqlablep x)
                                  (true-listp lst)
                                (eqlable-listp lst))))
       (cond ((endp lst) nil)
             ((eql x (car lst)) lst)
             (t (member-eql-exec x (cdr lst)))))

At this point the user can write (member x y) or (member-equal x y) to
call equality variants of member with test eql or equal, respectively.
We thus provide the following macro for the eq variant.

     (defmacro member-eq (x lst)
       `(member ,x ,lst :test 'eq))

Guard proof obligations generated by calls of member will include those
based on its use of mbe, and are supported by the following two lemmas.

     (defthm member-eq-exec-is-member-equal
       (equal (member-eq-exec x l)
              (member-equal x l)))

     (defthm member-eql-exec-is-member-equal
       (equal (member-eql-exec x l)
              (member-equal x l)))

Finally, the following two events arrange that in certain contexts such
as theories (including the use of in-theory in events and hints),
member-eq and member are treated as references to member-equal.

     (add-macro-alias member-eq member-equal)
     (add-macro-alias member member-equal)

We conclude this topic by exploring the following recommendation made
in the documentation for equality-variants.

     For efficiency we recommend using the -equal equality variant, for
     example member-equal or ... :TEST 'equal, in certain contexts:
     defmacro, defpkg, defconst, and value-triple forms.

ACL2 reliies on the underlying Common Lisp for evaluation.  It also
processes events in the ACL2 logic.  In order to guarantee consistency
of its logical and Common Lisp evaluations, ACL2 uses a "safe mode" to
avoid ill-guarded calls.  In particular, consider the use of mbe in
execution of a call of an equality variant of a primitive, F, other
than its F-equal variant.  The mbe call discussed above requires a
connection to be established between the :logic and :exec forms.  For
example, if F is called with :TEST 'eql (either explicitly or as the
default), then ACL2 will call both F-eql-exec and F-equal, and check
that the two results are equal.

The following partial log illustrates the point above.  We define a
macro that calls member, and when a call of this macro is expanded
during processing of a subsequent definition, we see that two
membership functions are called on the same arguments.

     ACL2 !>(defmacro mac (lst)
              (list 'quote (and (true-listp lst)
                                (member 'c lst :test 'eq))))

     Summary
     Form:  ( DEFMACRO MAC ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      MAC
     ACL2 !>(trace$ member-equal member-eq-exec)
      ((MEMBER-EQUAL) (MEMBER-EQ-EXEC))
     ACL2 !>(defun f () (mac (a b c d)))
     1> (ACL2_*1*_ACL2::MEMBER-EQ-EXEC C (A B C D))
       2> (MEMBER-EQ-EXEC C (A B C D))
       <2 (MEMBER-EQ-EXEC (C D))
     <1 (ACL2_*1*_ACL2::MEMBER-EQ-EXEC (C D))
     1> (ACL2_*1*_ACL2::MEMBER-EQUAL C (A B C D))
       2> (MEMBER-EQUAL C (A B C D))
       <2 (MEMBER-EQUAL (C D))
     <1 (ACL2_*1*_ACL2::MEMBER-EQUAL (C D))

     Since F is non-recursive, its admission is trivial.

If performance is an issue then we can avoid such a problem, for
example as follows.  In a fresh session, let us define a suitable
wrapper for calling member with :TEST 'eq.  This time, the trace in our
partial log shows that we have avoided calling two membership functions.

     ACL2 !>(defun mem-eq (x lst)
              (declare (xargs :guard (if (symbolp x)
                                         (true-listp lst)
                                       (symbol-listp lst))))
              (member x lst :test 'eq))
     [[ ... output omitted here ... ]]
      MEM-EQ
     ACL2 !>(defmacro mac (lst)
              (list 'quote (and (true-listp lst)
                                (mem-eq 'c lst))))

     Summary
     Form:  ( DEFMACRO MAC ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      MAC
     ACL2 !>(trace$ member-equal member-eq-exec mem-eq)
      ((MEMBER-EQUAL)
       (MEMBER-EQ-EXEC)
       (MEM-EQ))
     ACL2 !>(defun f () (mac (a b c d)))
     1> (ACL2_*1*_ACL2::MEM-EQ C (A B C D))
       2> (MEM-EQ C (A B C D))
       <2 (MEM-EQ (C D))
     <1 (ACL2_*1*_ACL2::MEM-EQ (C D))

     Since F is non-recursive, its admission is trivial.

IGNORABLE    See DECLARE.

IGNORE    See DECLARE.

IRRELEVANT-FORMALS    formals that are used but only insignificantly

Let fn be a function of n arguments.  Let x be the ith formal of fn.
We say x is "irrelevant in fn" if x is not involved in either the guard
or the measure for fn, x is used in the body, but the value of (fn
a1...ai...an) is independent of ai.

The easiest way to define a function with an irrelevant formal is
simply not to use the formal in the body of the function.  Such formals
are said to be "ignored" by Common Lisp and a special declaration is
provided to allow ignored formals.  ACL2 makes a distinction between
ignored and irrelevant formals.  Note however that if a variable is
declared ignored or ignorable, then it will not be reported as
irrelevant.

An example of an irrelevant formal is x in the definition of fact below.

     (defun fact (i x)
       (declare (xargs :guard (and (integerp i) (<= 0 i))))
       (if (zerop i) 0 (* i (fact (1- i) (cons i x))))).

Observe that x is only used in recursive calls of fact; it never "gets
out" into the result.  ACL2 can detect some irrelevant formals by a
closure analysis on how the formals are used.  For example, if the ith
formal is only used in the ith argument position of recursive calls,
then it is irrelevant.  This is how x is used above.

It is possible for a formal to appear only in recursive calls but still
be relevant.  For example, x is *not* irrelevant below, even though it
only appears in the recursive call.

     (defun fn (i x) (if (zerop i) 0 (fn x (1- i))))

The key observation above is that while x only appears in a recursive
call, it appears in an argument position, namely i's, that is relevant.
(The function above can be admitted with a :guard requiring both
arguments to be nonnegative integers and the :measure (+ i x).)

Establishing that a formal is irrelevant, in the sense defined above,
can be an arbitrarily hard problem because it requires theorem proving.
For example, is x irrelevant below?

     (defun test (i j k x) (if (p i j k) 0 x))

Note that the value of (test i j k x) is independent of x -- thus
making x irrelevant -- precisely if (p i j k) is a theorem.  ACL2's
syntactic analysis of a definition does not guarantee to notice all
irrelevant formals.

We regard the presence of irrelevant formals as an indication that
something is wrong with the definition.  We cause an error on such
definitions and suggest that you recode the definition so as to
eliminate the irrelevant formals.  If you must have an irrelevant
formal, one way to "trick" ACL2 into accepting the definition, without
slowing down the execution of your function, is to use the formal in an
irrelevant way in the guard.  For example, to admit fact, above, with
its irrelevant x one might use

     (defun fact (i x)
       (declare (xargs :guard (and (integerp i) (<= 0 i) (equal x x))))
       (if (zerop i) 0 (* i (fact (1- i) (cons i x)))))

For those who really want to turn off this feature, we have provided a
way to use the acl2-defaults-table for this purpose; see
SET-IRRELEVANT-FORMALS-OK.

OPTIMIZE    See DECLARE.

REDEFINING-PROGRAMS    an explanation of why we restrict redefinitions

ACL2 does not in general allow the redefinition of functions because
logical inconsistency can result:  previously stored theorems can be
rendered invalid if the axioms defining the functions involved are
changed.  However, to permit prototyping of both :program and :logic
mode systems, ACL2 permits redefinition if the user has accepted
logical responsibility for the consequences by setting
ld-redefinition-action to an appropriate non-nil value.  The refusal of
ACL2 to support the unrestricted redefinition of :program mode
functions may appear somewhat capricious.  After all, what are the
logical consequences of changing a definition if no axioms are involved?

Three important points should be made before we discuss redefinition
further.

The first is that ACL2 does support redefinition (of both :program and
:logic functions) when ld-redefinition-action is non-nil.

The second is that a "redefinition" that does not change the mode,
formals, guards, type declarations, stobjs, or body of a function is
considered redundant and is permitted even when ld-redefinition-action
is nil.  We recognize and permit redundant definitions because it is not
uncommon for two distinct books to share identical function
definitions.  When determining whether the body of a function is
changed by a proposed redefinition, we actually compare the
untranslated versions of the two bodies.  See TERM.  For
example, redundancy is not recognized if the old body is (list a b) and
the new body is (cons a (cons b nil)).  We use the untranslated bodies
because of the difficulty of translating the new body in the presence
of the old syntactic information, given the possibility that the
redefinition might attempt to change the signature of the function,
i.e., the number of formals, the number of results, or the position of
single-threaded objects in either.

The third important point is that a "redefinition" that preserves the
formals, guard, types, stobjs, and body but changes the mode from
:program to :logic is permitted even when ld-redefinition-action is
nil.  That is what verify-termination does.

This note addresses the temptation to allow redefinition of :program
functions in situations other than the three described above.
Therefore, suppose ld-redefinition-action is nil and consider the cases.

Case 1.  Suppose the new definition attempts to change the formals or
more generally the signature of the function.  Accepting such a
redefinition would render ill-formed other :program functions which
call the redefined function.  Subsequent attempts to evaluate those
callers could arbitrarily damage the Common Lisp image.  Thus,
redefinition of :program functions under these circumstances requires
the user's active approval, as would be sought with
ld-redefinition-action '(:query . :overwrite).

Case 2.  Suppose the new definition attempts to change the body (even
though it preserves the signature).  At one time we believed this was
acceptable and ACL2 supported the quiet redefinition of :program mode
functions in this circumstance.  However, because such functions can be
used in macros and redundancy checking is based on untranslated bodies,
this turns out to be unsound!  (Aside: Perhaps this is not an issue if
the function takes state or a user-defined stobj argument; but we do
not further consider this distinction.)  Such redefinition is therefore
now prohibited.  We illustrate such an unsoundness below.  Let
foo-thm1.lisp be a book with the following contents.

     (in-package "ACL2")
     (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil))
     (defmacro p (x) (p1 x))
     (defun foo (x) (p x))
     (defthm foo-thm1 (iff (foo x) x) :rule-classes nil)

Note that the macro form (p x) translates to (if x t nil).  The
:program function p1 is used to generate this translation.  The
function foo is defined so that (foo x) is (p x) and a theorem about
foo is proved, namely, that (foo x) is true iff x is true.

Now let foo-thm2.lisp be a book with the following contents.

     (in-package "ACL2")
     (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't))
     (defmacro p (x) (p1 x))
     (defun foo (x) (p x))
     (defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)

In this book, the :program function p1 is defined so that (p x) means
just the negation of what it meant in the first book, namely, (if x nil
t).  The function foo is defined identically -- more precisely, the
untranslated body of foo is identical in the two books, but because of
the difference between the two versions of the :program function p1 the
axioms defining the two foos are different.  In the second book we prove
the theorem that (foo x) is true iff x is nil.

Now consider what would happen if the signature-preserving redefinition
of :program functions were permitted and these two books were included.
When the second book is included the redefinition of p1 would be
permitted since the signature is preserved and p1 is just a :program.
But then when the redefinition of foo is processed it would be
considered redundant and thus be permitted.  The result would be a
logic in which it was possible to prove that (foo x) is equivalent to
both x and (not x).  In particular, the following sequence leads to a
proof of nil:

     (include-book "foo-thm1")
     (include-book "foo-thm2")
     (thm nil :hints (("Goal" :use (foo-thm1 foo-thm2))))

It might be possible to loosen the restrictions on the redefinition of
:program functions by allowing signature-preserving redefinition of
:program functions not involved in macro definitions.  Alternatively,
we could implement definition redundancy checking based on the
translated bodies of functions (though that is quite problematic).
Barring those two changes, we believe it is necessary simply to impose
the same restrictions on the redefinition of :program mode functions as
we do on :logic mode functions.

STATE    the von Neumannesque ACL2 state object

Note: If you are interested in programming with state, see
PROGRAMMING-WITH-STATE after reading the information below.

The ACL2 state object is used extensively in programming the ACL2
system, and has been used in other ACL2 programs as well.  However,
most users, especially those interested in specification and
verification (as opposed to programming per se), need not be aware of
the role of the state object in ACL2, and will not write functions that
use it explicitly.  We say more about this point at the end of this
documentation topic.

The ACL2 state object is an example of a single-threaded object or
stobj.  ACL2 allows the user to define new single-threaded objects.
Generally, ACL2 may need to access the ACL2 state but should not
(cannot) change it except via a certain set of approved functions such
as defun and defthm.  If you need a state-like object to which you have
complete rights, you may want a stobj.

Key to the idea of our state is the notion of single-threadedness.  For
an explanation, see STOBJ.  The upshot of it is that state is a
variable symbol with severe restrictions on its use, so that it can be
passed into only certain functions in certain slots, and must be
returned by those functions that "modify" it.  Henceforth, we do not
discuss single-threaded objects in general (which the user can introduce
with defstobj and defabsstobj) but one in particular, namely ACL2's
state object.

The global table is perhaps the most visible portion of the state
object.  Using the interface functions @ and assign, a user may bind
global variables to the results of function evaluations (much as an
Nqthm user exploits the Nqthm utility r-loop).  See @,
and see ASSIGN.

ACL2 supports several facilities of a truly von Neumannesque state
machine character, including file io and global variables.  Logically
speaking, the state is a true list of the 14 components described
below.  There is a "current" state object at the top-level of the ACL2
command loop.  This object is understood to be the value of what would
otherwise be the free variable state appearing in top-level input.
When any command returns a state object as one of its values, that
object becomes the new current state.  But ACL2 provides von Neumann
style speed for state operations by maintaining only one physical (as
opposed to logical) state object.  Operations on the state are in fact
destructive.  This implementation does not violate the applicative
semantics because we enforce certain draconian syntactic rules
regarding the use of state objects.  For example, one cannot "hold on"
to an old state, access the components of a state arbitrarily, or
"modify" a state object without passing it on to subsequent
state-sensitive functions.

Every routine that uses the state facilities (e.g. does io, or calls a
routine that does io), must be passed a "state object." And a routine
must return a state object if the routine modifies the state in any
way.  Rigid syntactic rules governing the use of state objects are
enforced by the function translate, through which all ACL2 user input
first passes.  State objects can only be "held" in the formal parameter
state, never in any other formal parameter and never in any structure
(excepting a multiple-value return list field which is always a state
object).  State objects can only be accessed with the primitives we
specifically permit.  Thus, for example, one cannot ask, in code to be
executed, for the length of state or the car of state.  In the
statement and proof of theorems, there are no syntactic rules
prohibiting arbitrary treatment of state objects.

Logically speaking, a state object is a true list whose members are as
follows:

     Open-input-channels, an alist with keys that are symbols in
     package "ACL2-INPUT-CHANNEL".  The value (cdr) of each pair has
     the form ((:header type file-name open-time) . elements), where
     type is one of :character, :byte, or :object and elements is a
     list of things of the corresponding type, i.e. characters,
     integers of type (mod 255), or lisp objects in our theory.
     File-name is a string.  Open-time is an integer.  See IO.

     Open-output-channels, an alist with keys that are symbols in
     package "ACL2-OUTPUT-CHANNEL".  The value of a pair has the form
     ((:header type file-name open-time) .  current-contents).  See
     IO.

     Global-table, an alist associating symbols (to be used as "global
     variables") with values.  See @, and see
     ASSIGN.

     T-stack, a list of arbitrary objects accessed and changed by the
     functions aref-t-stack and aset-t-stack.

     32-bit-integer-stack, a list of arbitrary 32-bit-integers accessed
     and changed by the functions aref-32-bit-integer-stack and
     aset-32-bit-integer-stack.

     Big-clock-entry, an integer, that is used logically to bound the
     amount of effort spent to evaluate a quoted form.

     Idates, a list of dates and times, used to implement the function
     print-current-idate, which prints the date and time.

     Acl2-oracle, a list of objects, used for example to implement the
     functions that let ACL2 report how much time was used, but
     inaccessible to the user.  Also see WITH-PROVER-TIME-LIMIT.

     File-clock, an integer that is increased on every file opening and
     closing, and on each call of sys-call, and is used to maintain the
     consistency of the io primitives.

     Readable-files, an alist whose keys have the form (string type
     time), where string is a file name and time is an integer.  The
     value associated with such a key is a list of characters, bytes,
     or objects, according to type.  The time field is used in the
     following way:  when it comes time to open a file for input, we
     will only look for a file of the specified name and type whose
     time field is that of file-clock.  This permits us to have a
     "probe-file" aspect to open-file: one can ask for a file, find it
     does not exist, but come back later and find that it does now
     exist.

     Written-files, an alist whose keys have the form (string type
     time1 time2), where string is a file name, type is one of
     :character, :byte or :object, and time1 and time2 are integers.
     Time1 and time2 correspond to the file-clock time at which the
     channel for the file was opened and closed.  This field is
     write-only; the only operation that affects this field is
     close-output-channel, which conses a new entry on the front.

     Read-files, a list of the form (string type time1 time2), where
     string is a file name and time1 and time2 were the times at which
     the file was opened for reading and closed.  This field is write
     only.

     Writeable-files, an alist whose keys have the form (string type
     time).  To open a file for output, we require that the name, type,
     and time be on this list.

     List-all-package-names-lst, a list of true-listps.  Roughly
     speaking, the car of this list is the list of all package names
     known to this Common Lisp right now and the cdr of this list is
     the value of this state variable after you look at its car.  The
     function, list-all-package-names, which takes the state as an
     argument, returns the car and cdrs the list (returning a new state
     too).  This essentially gives ACL2 access to what is provided by
     CLTL's list-all-packages.  Defpkg uses this feature to ensure that
     the about-to-be-created package is new in this lisp.  Thus, for
     example, in akcl it is impossible to create the package "COMPILER"
     with defpkg because it is on the list, while in Lucid that package
     name is not initially on the list.

     User-stobj-alist, an alist which associates user-defined
     single-threaded objects (see STOBJ) with their values.

We recommend avoiding the use of the state object when writing ACL2
code intended to be used as a formal model of some system, for several
reasons.  First, the state object is complicated and contains many
components that are oriented toward implementation and are likely to be
irrelevant to the model in question.  Second, there is currently not
much support for reasoning about ACL2 functions that manipulate the
state object, beyond their logical definitions.  Third, the
documentation about state is not as complete as one might wish.

User-defined single-threaded objects offer the speed of state while
giving the user complete access to all the fields.  See STOBJ.

Again, if you are interested in programming with state see
PROGRAMMING-WITH-STATE.

ERROR-TRIPLES    a common ACL2 programming idiom

When evaluation returns three values, where the first two are ordinary
(non-stobj) objects and the third is the ACL2 state, the result may be
called an "error triple".  If an error triple is (mv erp val state), we
think of erp as an error flag and val as the returned value.  By
default, if the result of evaluating a top-level form is an error triple
(mv erp val state), then that result is not printed if erp is non-nil
or if val is the keyword :INVISIBLE, and otherwise val is printed with
a preceding space.  For example:

     ACL2 !>(+ 3 4) ; ordinary value
     7
     ACL2 !>(mv nil (+ 3 4) state) ; error triple, error component of nil
      7
     ACL2 !>(mv t (+ 3 4) state) ; error triple, non-nil error component
     ACL2 !>(mv nil :invisible state) ; special case for :INVISIBLE
     ACL2 !>

See PROGRAMMING-WITH-STATE for a discussion of error triples
and how to program with them.  Also see LD-ERROR-TRIPLES and
see LD for a discussion of the value :COMMAND-CONVENTIONS for
keyword :LD-POST-EVAL-PRINT.

PROGRAMMING-WITH-STATE    programming using the von Neumannesque ACL2 state object

This documentation section introduces some common techniques for
programming using the ACL2 state object.  A prerequisite is thus a basic
understanding of that object; see STATE.  We hope this section
is useful, and we invite suggestions for improvements and additions.

A supplement to this section is the ACL2 source code, which uses most
(and probably all) of the techniques discussed here.  That code is thus
a source of many examples, which can serve as "templates" to guide
one's own programming with state.

Recall that "ACL2" stands for "A Computational Logic for Applicative
Common Lisp".  In particular, the language is applicative: there are no
global variables or side effects.  For many purposes this does not feel
restrictive; for example, an ACL2 user who is programming in raw Lisp
may well be more comfortable coding a factorial function applicatively,
using recursion, rather than using iteration with repeated assignment
to the same variable.

However, there are situations that call for reading or modifying the
system state, such as performing input and output, signalling errors,
saving information from one computation for use in a later one, or
reading and updating system-level or environmental data.  This section
provides an introductory guide for writing functions that traffic in
state.  We emphasize that this guide is intended as an introduction;
more complete documentation may often be found by following links to
documentation of individual utilities, and again, more examples may be
found by searching the ACL2 source code for uses of the functions and
macros mentioned below.  The rest of this section is organized as
follows.

     ENABLING PROGRAMMING WITH STATE
     STATE GLOBALS
     A REMARK ON GUARDS
     ERRORS AND ERROR TRIPLES
     SEQUENTIAL PROGRAMMING
     BINDING VARIABLES USING ERROR TRIPLES
     BINDING STATE GLOBAL VARIABLES
     INPUT AND OUTPUT
     TIMINGS
     ENVIRONMENT AND SYSTEM
     REMARKS ON EVENTS AND LD
     ADVANCED TOPICS

ENABLING PROGRAMMING WITH STATE

In order to submit a definition that takes state as a formal parameter,
you must either declare state as a :stobj (see XARGS) or first
evaluate the following form at the top level: (set-state-ok t).

Consider for example the following trivial definition.

     (defun foo (state)
       (mv 3 state))

If you submit the above definition in a fresh ACL2 session, you will
get this error message.

       ACL2 Error in ( DEFUN FOO ...):  The variable symbol STATE should not
       be used as a formal parameter of a defined function unless you are
       aware of its unusual status and the restrictions enforced on its use.
       See :DOC set-state-ok.

If first you evaluate (set-state-ok t), you can admit the above
definition.  Alternatively, you can declare state as a :stobj, as
follows.

     (defun foo (state)
       (declare (xargs :stobjs state))
       (mv 3 state))

A difference in the two approaches is that for the latter, a guard proof
obligation is generated by default.  See the section below entitled "A
remark on guards".

STATE GLOBALS

Recall (see STATE) that one of the fields of the ACL2 state
object is the global-table, which logically is an alist associating
symbols, known as "state globals" or "state global variables", with
values.  But no such alist actually exists in the implementation.
Instead, ACL2 provides utilities for reading state globals -- see
@ and see F-GET-GLOBAL -- and utilities for writing
them -- see ASSIGN and see F-PUT-GLOBAL.  The following
log shows how they work; further explanation follows below.

     ACL2 !>(assign my-var (+ 3 4))
      7
     ACL2 !>(@ my-var)
     7
     ACL2 !>(f-put-global 'my-var (+ 1 5) state)
     <state>
     ACL2 !>(f-get-global 'my-var state)
     6
     ACL2 !>

Note that the first result is indented by one space.  This is ACL2's
way to indicate that the assign expression returned an "error triple"
and that no error was signalled.  We discuss error triples in more
detail below; also see ERROR-TRIPLES.

As illustrated above, the output signatures of the utilities for
assigning to state globals differ from each other as follows:
f-put-global returns state, but assign returns an error triple (mv nil
val state) where val is the value assigned to the state global.  The
output signatures of the utilities for reading, @ and f-get-global, are
identical.  In fact, the form (f-get-global 'my-var state) is the
single-step macroexpansion of the form (@ my-var), as can be confirmed
using trans1.

     ACL2 !>:trans1 (@ my-var)
      (F-GET-GLOBAL 'MY-VAR STATE)
     ACL2 !>

State globals are useful for conveying persistent state information.
Consider for example the utility set-inhibit-output-lst.  The form
(set-inhibit-output-lst '(prove proof-tree)) is approximately equivalent
to (assign inhibit-output-lst '(prove proof-tree)).  We say
"approximately" because set-inhibit-output-lst additionally does some
error checking to insure that all the tokens in the new list are legal.
When deciding whether to print output, the ACL2 system reads the value
of state global variable inhibit-output-lst.

A REMARK ON GUARDS

For a function definition (see DEFUN), if state is specified as
a stobj as with the form (declare (xargs :stobjs state)), then the
guard for that function is considered to include the condition (state-p
state).  By default, guard verification will then be performed.

We can illustrate this point by modifying the example above as follows,
to read the value of state global gag-mode.

     (defun foo (state)
       (declare (xargs :stobjs state))
       (f-get-global 'gag-mode state))

If you try this in a fresh ACL2 session, the proof will fail with the
following key checkpoint, which says that the state global gag-mode is
bound in the global-table of the state.

       (IMPLIES (STATE-P1 STATE)
                (ASSOC-EQUAL 'GAG-MODE (NTH 2 STATE)))

How can we deal with this proof failure?   One way is simply to ignore
the issue by defining the function in :program mode, as follows.

     (defun foo (state)
       (declare (xargs :stobjs state
                       :mode :program))
       (f-get-global 'gag-mode state))

Perhaps a better way is to strengthen the guard to assert that the
indicated state global is bound, as follows.

     (defun foo (state)
       (declare (xargs :guard (boundp-global 'gag-mode state)
                       :stobjs state))
       (f-get-global 'gag-mode state))

Also see GUARD-MISCELLANY for a discussion of how guards are
generated from xargs fields of declare forms, specifically, for keywords
:guard and :stobjs.

ERRORS AND ERROR TRIPLES

When evaluation returns three values, where the first two are ordinary
objects and the third is the ACL2 state, the result may be called an
"error triple".  (Whether it is treated as an error triple depends on
the programmer.)  Error triples are often denoted (mv erp val state),
and common ACL2 programming idioms treat erp as a flag indicating
whether an error is being signalled and val as the "value" computed.
Also see ERROR-TRIPLES.

Even ACL2 users who are not programmers encounter error triples, because
these are the values returned by evaluation of ACL2 events.  Consider
the following log, where the only user input is the defun form
following the prompt.

     ACL2 !>(defun foo (x) x)

     Since FOO is non-recursive, its admission is trivial.  We observe that
     the type of FOO is described by the theorem (EQUAL (FOO X) X).

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>

All output above results from explicit calls of output functions,
except for the next-to-last line, which contains FOO.  Notice the
single-space indentation preceding FOO.  That space indicates that in
fact, the value returned by evaluation of the defun form is the error
triple whose error flag is nil and whose computed value is FOO.  By
default, ACL2 prints any error triple (mv nil val state) by inserting a
space before printing val.  You can change the default by setting state
global ld-post-eval-print to t; notice how the same result is printed
below.

     ACL2 !>:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 !>(set-ld-post-eval-print t state)
     (NIL T <state>)
     ACL2 !>(defun foo (x) x)

     Since FOO is non-recursive, its admission is trivial.  We observe that
     the type of FOO is described by the theorem (EQUAL (FOO X) X).

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
     (NIL FOO <state>)
     ACL2 !>

The way error triples are printed by ld is controlled not only by state
global ld-post-eval-print, but also by state global ld-error-triples.
These are examples of "ld specials"; see LD, see
LD-POST-EVAL-PRINT, and see LD-ERROR-TRIPLES.

It is so common to produce an error triple whose first (error flag)
component is nil that ACL2 provides a handy macro, value, for this
purpose.  Thus, (value <expression>) is equivalent to (mv nil
<expression> state).  Also see VALUE-TRIPLE for a similar
construct that is a legal event form.

We turn now to the topic of errors.  The macro ER "causes" an error,
but there are really two quite different kinds of errors: "soft" and
"hard" errors.  We use the term "soft error" to refer to a form that
returns an error triple (mv erp val state) for which erp is non-nil.
Soft errors do not interrupt the normal flow of evaluation: the error
triple is returned to the caller which interprets the erp flag and val
as directed by the programmer.  Macros discussed below make it
convenient to think about soft errors as short-circuiting the
computation.  Hard errors, on the other hand, do actually rip control
away from the current evaluation and return it to the top-level loop.
Logically speaking, expressions that cause hard errors return nil in
the error case, but the nil is never seen in actual evaluation because
control does not return to the caller.

Note that the function abort!, which you can invoke by typing :a!,
always returns to the top level.  Note that ACL2 can prove that
(abort!) returns nil but that this cannot be confirmed by computation.

     ACL2 !>(thm (equal (abort!) nil))

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION ABORT!))
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Proof succeeded.
     ACL2 !>(equal (abort!) nil)
     Abort to ACL2 top-level
     ...
     ACL2 !>

(What actually happens with a hard error, including non-default cases,
is a bit subtle; most readers will probably want to skip this
paragraph.  The read-eval-print loop implemented by ld is implemented
by a call of the ACL2 evaluator function, trans-eval, on each input
form.  If a hard error occurs during evaluation of an input form, its
trans-eval call will return with a soft error.  Ld, in turn handles
that soft error appropriately; see LD-ERROR-ACTION.)

The most common way to signal errors is the macro er, which prints a
formatted error message and returns a soft or hard error as specified
by the call.  Note however that soft errors are signalled using :program
mode functions.

Since the output signatures of soft and hard errors are different --
hard errors "return" a single value while soft errors return a triple --
mixing them in an expression requires embedding the hard error form in
(an irrelevant) triple, as illustrated below.  All branches of the
expression must produce an error triple if any branch does.

     ACL2 !>(defun chk-find-or-abort (e x state)
              (declare (xargs :mode :program))
              (if (endp x)
                  (value                          ; Note use of VALUE!
                    (er hard 'chk-find-or-abort
                        "Did not find ~x0!"
                         e))
                  (if (not (integerp (car x)))
                      (er soft 'chk-find-or-abort
                          "Non-integer, ~x0, in list!"
                          (car x))
                      (if (eql (car x) e)
                          (value x)
                          (chk-find-or-abort e (cdr x) state)))))

     Summary
     Form:  ( DEFUN CHK-FIND-OR-ABORT ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      CHK-FIND-OR-ABORT
     ACL2 !>(chk-find-or-abort 3 '(1 2 3 4 5) state)
      (3 4 5)
     ACL2 !>(chk-find-or-abort 3 '(1 A 3 4 5) state)

     ACL2 Error in CHK-FIND-OR-ABORT:  Non-integer, A, in list!

     ACL2 !>(chk-find-or-abort 3 '(1 2 4 5) state)

     HARD ACL2 ERROR in CHK-FIND-OR-ABORT:  Did not find 3!
     ...
     ACL2 !>

See ER for further discussion of errors.  For some other
individual topics related to errors see ASSERT$, see
BREAK-ON-ERROR, see ERROR1, see HARD-ERROR, see
ILLEGAL, and see LD-ERROR-TRIPLES.

In the next section we discuss soft errors further, in the context of
programming.

SEQUENTIAL PROGRAMMING

This section describes handy ways to modify state in steps, using
macros that implement a sequence of let or mv-let bindings.  For
example, suppose you want to assign the values 1 and 2 to two state
globals one-var and two-var, respectively.  Because of ACL2's syntactic
restrictions on state, it is not legal simply to write (f-put-global
'two-var 2 (f-put-global 'one-var 1 state)).  However, let comes to the
rescue as follows.

     (let ((state (f-put-global 'one-var 1 state)))
       (let ((state (f-put-global 'two-var 2 state)))
         state))

It is so common to bind state successively in such a manner that ACL2
provides a macro, pprogn, for this purpose.  Thus, an equivalent
solution to the problem above is

     (pprogn (f-put-global 'one-var 1 state)
             (f-put-global 'two-var 2 state)
             state)

or, more simply, as follows.

     (pprogn (f-put-global 'one-var 1 state)
             (f-put-global 'two-var 2 state))

See PPROGN.  Note that the last form is allowed to return
multiple values; the only requirement on the last form is that its
value include state.

It is also common to update the state using a sequence of forms such
that each returns an error triple, where the intention is for
evaluation to short-circuit immediately if a soft error is encountered.
Suppose <expr1> and <expr2> are expressions that return error triples,
where the state components of the error triples might be updated, and
one wishes to evaluate <expr1> and then <expr2>, returning the
(multiple) values returned by <expr2> unless the error triple returned
by <expr1> is a soft error, in which case that error triple is returned.
One can of course do so as follows.

     (mv-let (erp val state)
             <expr1>
             (cond (erp (mv erp val state))
                   (t <expr2>)))

But ACL2 provides a handy macro, er-progn, for this purpose.  The
following code is equivalent to the code just above.

     (er-progn <expr1> <expr2>)

See ER-PROGN for more details.  Note that unlike pprogn, the
return signature for the last expression must be the same as that of the
others: an error triple.

Let's consider how to use pprogn and er-progn together.  In the
following example f1 and f2 both return state, while each of g1 and g2
returns an error triple.  The following code modifies state by
executing these in the order f1, g1, f2, and finally g2, returning (mv
nil val state) where val is the value component of the error triple
returned by g2 -- except we return a soft error if g1 or g2 returns a
soft error.

     (pprogn (f1 x state)
             (er-progn (g1 x state)
                       (pprogn (f2 x state)
                               (g2 x state))))

Finally, consider the events progn and progn!.  These have similar
behavior to that of er-progn.  However, progn and progn! may only be
used in event contexts, for example at the top level or immediately
underneath a call of encapsulate or progn, while er-progn has no such
restriction.  So when writing code, use er-progn rather than progn or
progn!.  In particular, the body of a defun must not have any calls of
progn (or of progn!  either), and the same restriction holds for any
code to be executed, such as the body of a make-event form.

BINDING VARIABLES USING ERROR TRIPLES

In this section we discuss the macro er-let*, which is a variant of the
special form, let*, that is useful when programming with state.

The macro er-let* is useful when binding variables to the value
components of error triples.  It is actually quite similar to er-progn,
described above, except that er-let* binds variables.  First consider
the following example.

     (er-let* ((x1 (f1 state))
               (x2 (f2 x1 state)))
       (value (cons x1 x2)))

The code just above is essentially equivalent to writing the following.

     (mv-let (erp x1 state)
             (f1 state)
             (cond (erp (mv erp x1 state))
                   (t (mv-let (erp x2 state)
                              (f2 x1 state)
                              (cond (erp (mv erp x2 state))
                                    (t (value (cons x1 x2))))))))

As suggested by the example above, er-let* has the same syntax as let*,
except that declarations are not supported.  (But note that ignore
declarations are not needed; all variables that are bound are also
used, at least in the error case.  Consider replacing (cons x1 x2) by
nil in the example displayed immediately above, and note that x1 and x2
are still used.)  However, unlike let*, er-let* requires that for each
binding (var expr), the expression expr must evaluate to an error
triple and, moreover, it requires that the second argument (the "body")
of er-let* must evaluate to an error triple.  If one of the variable
expressions (e.g., the f1 and f2 calls above) signals an error, its
error triple is returned as the value of the er-let*.

Of course, soft errors can be "caught" by using mv-let instead of
er-let* and simply ignoring the error flag or, more generally, by
returning a non-erroneous error triple even if the error flag was on.

BINDING STATE GLOBAL VARIABLES

In this section we introduce a utility, state-global-let*, that is an
analogue of let* for state global variables.  Consider the following
example.

     (state-global-let*
      ((inhibit-output-lst (add-to-set-eq 'summary (@ inhibit-output-lst))))
      (thm (equal x x)))

This form binds state global variable inhibit-output-lst to the result
of adding the symbol, summary, to the current value of that state
global.  Thus (see SET-INHIBIT-OUTPUT-LST), the usual summary
is not printed when evaluating this call of thm.

See STATE-GLOBAL-LET* for more complete documentation.

INPUT AND OUTPUT

In ACL2, most input and output involves the ACL2 state.  See IO.

TIMINGS

For how to obtain the runtime elapsed since the start of the ACL2
session, see READ-RUN-TIME.

For a utility for saving times into the ACL2 state and for printing
those saved times, see the community book misc/save-time.lisp.

To time an evaluation (though this really isn't about state), see
TIME$.

ENVIRONMENT AND SYSTEM

Next, we mention briefly some ways in which ACL2 interacts with its
environment using the ACL2 state.

For how to read and write environment variables, see GETENV$ and
see SETENV$.

For how to run a command in the host operating system, see
SYS-CALL.

REMARKS ON EVENTS AND LD

In general, undefined or surprising behavior may occur when using ACL2
events or calling ld in your programs.  In some cases ACL2 enforces
restrictions against these uses.  We strongly discourage using ld in
programs, as it has been designed to be called only at the top level of
a read-eval-print loop.

There is also a restriction on contexts in which make-event may be
called: it may only be called in a context where an event is expected,
such as the top level, in a book, or as an argument of encapsulate or
progn.  The reason is that ACL2 does very subtle and careful tracking
of make-event expansions; and it is only able to do this in event
contexts, where it is able to carry out such tracking accurately.

ADVANCED TOPICS

ACL2 provides the function trans-eval to evaluate an arbitrary form
(after translating it to a term, i.e., into internal form).  For more
information, we refer to reader to comments in the definition of
trans-eval in the ACL2 source code.  There are also many examples of its
use in the ACL2 sources.

For a function that provides the true absolute filename, with soft links
resolved, see CANONICAL-PATHNAME.

For a function that returns a check-sum on the characters in a channel,
see CHECK-SUM.

To obtain a random number, see RANDOM$.

If you are programming in raw-mode (see SET-RAW-MODE) or in raw
Lisp, use the variable *the-live-state* in place of the variable state.

We invite suggestions for additional advanced topics.

TIME-TRACKER    display time spent during specified evaluation

The time-tracker macro is a utility for displaying runtime (cpu time)
spent during specified evaluation.  In general, the user provides this
specification.  However, ACL2 itself uses this utility for tracking
uses of its tau-system reasoning utility (see
TIME-TRACKER-TAU).  We discuss that use as an example before
discussing the general form for calls of time-tracker.

Remark for ACL2(p) users (see PARALLELISM): time-tracker is
merely a no-op in ACL2(p).

During the development of the tau-system, we were concerned about the
possibility that it would slow down proofs without any indication of
how one might avoid the problem.  We wanted a utility that would alert
the user in such situations.  However, the tau-system code does not
return state, so we could not track time spent in the state.  We
developed the time-tracker utility to track time and print messages,
and we did it in a general way so that others can use it in their own
code.  Here is an example of such a message that could be printed
during a proof.

     TIME-TRACKER-NOTE [:TAU]: Elapsed runtime in tau is 2.58 secs; see
     :DOC time-tracker-tau.

And here is an example of such a message that could be printed at the
end of the proof.

     TIME-TRACKER-NOTE [:TAU]: For the proof above, the total time spent
     in the tau system was 20.29 seconds.  See :DOC time-tracker-tau.

The time-tracker utility tracks computation time spent on behalf of a
user-specified "tag".  In the case of the tau-system, we chose the tag,
:tau.  The first argument of time-tracker is the tag, which in our
running example is always :tau.  Note that although all arguments of
time-tracker are evaluated, the first argument is typically a keyword
and the second is always a keyword, and such arguments evaluate to
themselves.

An ACL2 function invoked at the start of a proof includes the following
code.

     (progn$
      (time-tracker :tau :end)
      (time-tracker :tau :init
                    :times '(1 2 3 4 5)
                    :interval 5
                    :msg "Elapsed runtime in tau is ~st secs; see :DOC ~
                          time-tracker-tau.~|~%")
      ...)

The first time-tracker call (above) ends any existing time-tracking for
tag :tau.  One might have expected it be put into code managing the
proof summary, but we decided not to rely on that code being executed,
say, in case of an interrupt.  When a given tag is not already being
time-tracked, then :end is a no-op (rather than an error).

The second time-tracker call (above) initiates time-tracking for the
tag, :tau.  Moreover, it specifies the effect of the :print? keyword.
Consider the following abbreviated definition from the ACL2 source code.

     (defun tau-clausep-lst-rec (clauses ens wrld ans ttree state calist)
       (cond
        ((endp clauses)
         (mv (revappend ans nil) ttree calist))
        (t (mv-let
            (flg1 ttree1 calist)
            (tau-clausep (car clauses) ens wrld state calist)
            (prog2$ (time-tracker :tau :print?)
                    (tau-clausep-lst-rec (cdr clauses) ...))))))

Notice that (time-tracker :tau :print?) is executed immediately after
tau-clausep is called.  The idea is to check whether the total time
elapsed inside the tau-system justifies printing a message to the user.
The specification of :times '(1 2 3 4 5) in the :init form above says
that a message should be printed after 1 second, after 2 seconds, ...,
and after 5 seconds.  Thereafter, the specification of :interval 5 in
the :init form above says that each time we print, at least 5 additional
seconds should have been tracked before (time-tracker :tau :print?)
prints again.  Finally, the :msg keyword above specifies just what
should be printed.  If it is omitted, then a reasonable default message
is printed (as discussed below), but in this case we wanted to print a
custom message.  The :msg string above is what is printed using
formatted printing (see FMT), where the character #\t is bound
to a string giving a decimal representation with two decimal points of
the time tracked so far for tag :tau.  (As our general description
below points out, :msg can also be a "message" list rather than a
string.)

But when is time actually tracked for :tau?  Consider the following
definition from the ACL2 source code.

     (defun tau-clausep-lst (clauses ens wrld ans ttree state calist)
       (prog2$ (time-tracker :tau :start)
               (mv-let
                (clauses ttree calist)
                (tau-clausep-lst-rec clauses ens wrld ans ttree state calist)
                (prog2$ (time-tracker :tau :stop)
                        (mv clauses ttree calist)))))

The two calls of time-tracker above first start, and then stop,
time-tracking for the tag, :tau.  Thus, time is tracked during
evaluation of the call of tau-clausep-lst-rec, which is the function
(discussed above) that does the tau-system's work.

Finally, as noted earlier above, ACL2 may print a time-tracking message
for tag :tau at the end of a proof.  The ACL2 function print-summary
contains essentially the following code.

     (time-tracker :tau :print?
                   :min-time 1
                   :msg "For the proof above, the total runtime ~
                         spent in the tau system was ~st seconds.  ~
                         See :DOC time-tracker-tau.~|~%")

The use of :min-time says that we are to ignore the :times and
:interval established by the :init call described above, and instead,
print a message if and only if at least 1 second (since 1 is the value
of keyword :min-time) has been tracked for tag :tau.  Formatted printing
(see FMT) is used for the value of :msg, where the character
#\t is bound to a decimal string representation of the time in seconds,
as described above.

The example above covers all legal values for the second argument of
time-tracker and discusses all the additional legal keyword arguments.
We conclude with a precise discussion of all arguments.  Note that all
arguments are evaluated; thus when we refer to an argument, we are
discussing the value of that argument.  All times discussed are
runtimes, i.e., cpu times.

     General forms:

     (time-tracker t)        ; enable time-tracking (default)

     (time-tracker nil)      ; disable time-tracking

     (time-tracker tag       ; a symbol other than t or nil
                   option    ; :init, :end, :start, :stop, or :print?
                   ;; keyword arguments:
                   :times    ; non-nil if and only if option is :init
                   :interval ; may only be non-nil with :init option
                   :min-time ; may only be non-nil with :print? option
                   :msg      ; may only be non-nil with :init and :print? options

Time-tracking is enabled by default.  If the first argument is t or
nil, then no other arguments are permitted and time-tracking is enabled
or disabled, respectively.  When time-tracking is disabled, nothing
below takes place.  Thus we assume time-tracking is enabled for the
remainder of this discussion.  We also assume below that the first
argument is neither t nor nil.

We introduce some basic notions about time-tracking.  A given tag, such
as :tau in the example above, might or might not currently be "tracked":
:init causes the specified tag to be tracked, while :end causes the
specified tag not to be tracked.  If the tag is being tracked, the tag
might or might not be "active": :start causes the tag to be in an active
state, whie :stop causes the tag not to be active.  Note that only
tracked tags can be in an active or inactive state.  For a tag that is
being tracked, the "accumulated time" is the total time spent in an
active state since the time that the tag most recently started being
tracked, and the "checkpoint list" is a non-empty list of rational
numbers specifying when printing may take place, as described below.

We now consider each legal value for the second argument, or "option",
for a call of time-tracker on a given tag.

:Init specifies that the tag is to be tracked.  It also establishes
defaults for the operation of :print?, as described below, using the
:times, :interval, and :msg keywords.  Of these three, only :times is
required, and its value must be a non-empty list of rational numbers
specifying the initial checkpoint list for the tag.  It is an error to
specify :init if the tag is already being tracked.  (So if you don't
care whether or not the tag is already being tracked and you want to
initiate tracking for that tag, use :end first.)

:End specifies that if the tag is being tracked, then it should nstop
being tracked.  If the tag is not being tracked, then :end has no
effect.

:Start specifies that the tag is to be active.  It is an error to
specify :start if the tag is not being tracked or is already active.

:Stop specifies that the tag is to stop being active.  It is an error to
specify :stop if the tag is not being tracked or is not active.

:Print? specifies that if the tag is being tracked (not necessarily
active), then a message should be printed if a suitable condition is
met.  The nature of that message and that condition depend on the
keyword options supplied with :print? as well as those supplied with
the :init option that most recently initiated tracking.  :Print? has no
effect if the tag is not being tracked, except that if certain keyword
values are checked if supplied with :print?: :min-time must be a
rational number or nil, and :msg must be either a string, a true-list
whose car is a string, or nil.  The remainder of this documentation
describes the :print? option in detail under the assumption that the
tag is being tracked: first, giving the conditions under which it
causes a message to be printed, and second, explaining what is printed.

When :print? is supplied a non-nil value of :min-time, that value must
be a rational number, in which case a message is printed if the
accumulated time for the tag is at least that value.  Otherwise a
message is printed if the accumulated time is greater than or equal to
the car of the checkpoint list for the tag.  In that case, the tracking
state for the tag is updated in the following two ways.  First, the
checkpoint list is scanned from the front and as long as the
accumulated time is greater than or equal to the car of the remaining
checkpoint list, that car is popped off the checkpoint list.  Second,
if the checkpoint list has been completely emptied and a non-nil
:interval was supplied when tracking was most recently initiated with
the :init option, then the checkpoint list is set to contain a single
element, namely the sum of the accumulated time with that value of
:interval.

Finally, suppose the above criteria are met, so that :print? results in
printing of a message.  We describe below the message, msg, that is
printed.  Here is how it is printed (see FMT), where
seconds-as-decimal-string is a string denoting the number of seconds of
accumulated time for the tag, with two digits after the decimal point.

     (fms "TIME-TRACKER-NOTE [~x0]: ~@1~|"
          (list (cons #0 tag)
                (cons #1 msg)
                (cons #t seconds-as-decimal-string))
          (proofs-co state) state nil)

The value of msg is the value of the :msg keyword supplied with
:print?, if non-nil; else, the value of :msg supplied when most
recently initialization with the :init option, if non-nil; and
otherwise, the string "~st s" (the final "s" abbreviating the word
"seconds").  It is convenient to supply :msg as a call (msg str arg-0
arg-1 ... arg-k), where str is a string and each arg-i is the value to
be associated with #\i upon formatted printing (as with fmt) of the
string str.

TYPE    See DECLARE.

ZERO-TEST-IDIOMS    how to test for 0

Below are six commonly used idioms for testing whether x is 0.  Zip and
zp are the preferred termination tests for recursions down the integers
and naturals, respectively.

     idiom       logical              guard                 primary
                 meaning                                 compiled code*

     (equal x 0) (equal x 0)          t                   (equal x 0)

     (eql x 0)   (equal x 0)          t                   (eql x 0)

     (zerop x)   (equal x 0)          x is a number       (= x 0)

     (= x 0)     (equal x 0)          x is a number       (= x 0)

     (zip x)     (equal (ifix x) 0)   x is an integer     (= x 0)

     (zp x)      (equal (nfix x) 0)   x is a natural      (int= x 0)

     (zpf x)     (equal (nfix x) 0)   x is a fixnum >= 0  (eql (the-fixnum x) 0)

*See GUARDS-AND-EVALUATION, especially the subsection titled
"Guards and evaluation V: efficiency issues".  Primary code is relevant
only if guards are verified.  The "compiled code" shown is only
suggestive.

The first four idioms all have the same logical meaning and differ only
with respect to their executability and efficiency.  In the absence of
compiler optimizing, (= x 0) is probably the most efficient, (equal x
0) is probably the least efficient, and (eql x 0) is in between.
However, an optimizing compiler could always choose to compile (equal x
0) as (eql x 0) and, in situations where x is known at compile-time to
be numeric, (eql x 0) as (= x 0).  So efficiency considerations must, of
course, be made in the context of the host compiler.

Note also that (zerop x) and (= x 0) are indistinguishable.  They have
the same meaning and the same guard, and can reasonably be expected to
generate equally efficient code.

Note that (zip x) and (zp x) do not have the same logical meanings as
the others or each other.  They are not simple tests for equality to 0.
They each coerce x into a restricted domain, zip to the integers and zp
to the natural numbers, choosing 0 for x when x is outside the domain.
Thus, 1/2, #c(1 3), and 'abc, for example, are all "recognized" as zero
by both zip and zp.  But zip reports that -1 is different from 0 while
zp reports that -1 "is" 0.  More precisely, (zip -1) is nil while (zp
-1) is t.

Note that the last five idioms all have guards that restrict their
Common Lisp executability.  If these last five are used in situations
in which guards are to be verified, then proof obligations are incurred
as the price of using them.  If guard verification is not involved in
your project, then the first five can be thought of as synonymous.

Zip and zp are not provided by Common Lisp but are ACL2-specific
functions.  Why does ACL2 provide these functions?  The answer has to
do with the admission of recursively defined functions and efficiency.
Zp is provided as the zero-test in situations where the controlling
formal parameter is understood to be a natural number.  Zip is
analogously provided for the integer case.  We illustrate below.

Here is an admissible definition of factorial

     (defun fact (n) (if (zp n) 1 (* n (fact (1- n)))))

Observe the classic recursion scheme: a test against 0 and recursion by
1-.  Note however that the test against 0 is expressed with the zp
idiom.  Note also the absence of a guard making explicit our intention
that n is a natural number.

This definition of factorial is readily admitted because when (zp n)

is false (i.e., nil) then n is a natural number other than 0 and so (1-
n) is less than n.  The base case, where (zp n) is true, handles all
the "unexpected" inputs, such as arise with (fact -1) and (fact 'abc).
When calls of fact are evaluated, (zp n) checks (integerp n) and (> n
0).  Guard verification is unsuccessful for this definition of fact
because zp requires its argument to be a natural number and there is no
guard on fact, above.  Thus the primary raw lisp for fact is
inaccessible and only the :logic definition (which does runtime "type"
checking) is used in computation.  In summary, this definition of
factorial is easily admitted and easily manipulated by the prover but
is not executed as efficiently as it could be.

Runtime efficiency can be improved by adding a guard to the definition.

     (defun fact (n)
       (declare (xargs :guard (and (integerp n) (>= n 0))))
       (if (zp n) 1 (* n (fact (1- n)))))

This guarded definition has the same termination conditions as before -
termination is not sensitive to the guard.  But the guards can be
verified.  This makes the primary raw lisp definition accessible during
execution.  In that definition, the (zp n) above is compiled as (= n
0), because n will always be a natural number when the primary code is
executed.  Thus, by adding a guard and verifying it, the elegant and
easily used definition of factorial is also efficiently executed on
natural numbers.

Now let us consider an alternative definition of factorial in which (=
n 0) is used in place of (zp n).

     (defun fact (n) (if (= n 0) 1 (* n (fact (1- n)))))

This definition does not terminate.  For example (fact -1) gives rise
to a call of (fact -2), etc.  Hence, this alternative is inadmissible.
A plausible response is the addition of a guard restricting n to the
naturals:

     (defun fact (n)
      (declare (xargs :guard (and (integerp n) (>= n 0))))
      (if (= n 0) 1 (* n (fact (1- n)))))

But because the termination argument is not sensitive to the guard, it
is still impossible to admit this definition.  To influence the
termination argument one must change the conditions tested.  Adding a
runtime test that n is a natural number would suffice and allow both
admission and guard verification.  But such a test would slow down the
execution of the compiled function.

The use of (zp n) as the test avoids this dilemma.  Zp provides the
logical equivalent of a runtime test that n is a natural number but the
execution efficiency of a direct = comparison with 0, at the expense of
a guard conjecture to prove.  In addition, if guard verification and
most-efficient execution are not needed, then the use of (zp n) allows
the admission of the function without a guard or other extraneous
verbiage.

While general rules are made to be broken, it is probably a good idea
to get into the habit of using (zp n) as your terminating "0 test"
idiom when recursing down the natural numbers.  It provides the logical
power of testing that n is a non-0 natural number and allows efficient
execution.

We now turn to the analogous function, zip.  Zip is the preferred
0-test idiom when recursing through the integers toward 0.  Zip
considers any non-integer to be 0 and otherwise just recognizes 0.  A
typical use of zip is in the definition of integer-length, shown below.
(ACL2 can actually accept this definition, but only after appropriate
lemmas have been proved.)

     (defun integer-length (i)
       (declare (xargs :guard (integerp i)))
       (if (zip i)
           0
         (if (= i -1)
           0
           (+ 1 (integer-length (floor i 2))))))

Observe that the function recurses by (floor i 2).  Hence, calling the
function on 25 causes calls on 12, 6, 3, 1, and 0, while calling it on
-25 generates calls on -13, -7, -4, -2, and -1.  By making (zip i) the
first test, we terminate the recursion immediately on non-integers.
The guard, if present, can be verified and allows the primary raw lisp
definition to check (= i 0) as the first terminating condition (because
the primary code is executed only on integers).

PROOF-CHECKER    support for low-level interaction

Call this up with (verify ...).

This is an interactive system for checking ACL2 theorems, or at least
exploring their proofs.  One enters it using the VERIFY command (see
VERIFY), and then invokes commands at the resulting prompt to
operate on a stack of goals, starting with the single goal that was
supplied to VERIFY.  The final command (or "instruction") can be an exit
command, which can print out a defthm event if the goal stack is empty;
see PROOF-CHECKER-COMMANDS, in particular the exit command.
That resulting defthm event includes an :instructions parameter, which
directs replay of the proof-checker commands (for example during
certification of a book containing that event; see BOOKS).

If you exit the proof-checker interactive loop, you may re-enter that
session at the same point using the command (verify), i.e., with no
arguments.  The commands save and retrieve may be invoked to manage
more than one session.

The proof-checker can be invoked on a specific subgoal, and the
resulting :instructions can be given as a hint to the theorem prover
for that subgoal.  See INSTRUCTIONS.

A tutorial is available on the world-wide web:
`http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html'.
The tutorial illustrates more than just the proof-checker.  The portion
relevant to the proof-checker may be accessed directly:
`http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29'

See SET-EVISC-TUPLE for how to arrange that output is printed
in abbreviated form.  In general, the proof-checker uses the :TERM
evisc-tuple described in that documentation.

Individual proof-checker commands are documented in subsection
proof-checker-commands.  When inside the interactive loop (i.e., after
executing verify), you may use the help command to get a list of legal
instructions and (help instr) to get help for the instruction instr.

DEFINE-PC-HELP    define a macro command whose purpose is to print something

     Example:
     (define-pc-help pp ()
       (if (goals t)
           (io? proof-checker nil state
                (state-stack)
                (fms0 "~|~y0~|"
                      (list (cons #0
                                  (fetch-term (conc t)
                                              (current-addr t))))))
         (print-all-goals-proved-message state)))

     General Form:
     (define-pc-help name args &rest body)

This defines a macro command named name, as explained further below.
The body should (after removing optional declarations) be a form that
returns state as its single value.   Typically, it will just print
something.

What (define-pc-help name args &rest body) really does is to create a
call of define-pc-macro that defines name to take arguments args, to
have the declarations indicated by all but the last form in body, and
to have a body that (via pprogn) first executes the form in the last
element of body and then returns a call to the command skip (which will
return (mv nil t state)).

DEFINE-PC-MACRO    define a proof-checker macro command

     Example:
     (define-pc-macro ib (&optional term)
       (value
        (if term
            `(then (induct ,term) bash)
          `(then induct bash))))

The example above captures a common paradigm:  one attempts to prove
the current goal by inducting and then simplifying the resulting goals.
(see PROOF-CHECKER-COMMANDS for documentation of the command
then, which is itself a pc-macro command, and commands induct and
bash.)  Rather than issuing (then induct bash), or worse yet issuing
induct and then issuing bash for each resulting goals, the above
definition of ib would let you issue ib and get the same effect.

     General Form:
     (define-pc-macro cmd args doc-string dcl ... dcl body)

where cmd is the name of the pc-macro than you want to define, args is
its list of formal parameters.  Args may include lambda-list keywords
&optional and &rest; see MACRO-ARGS, but note that here, args
may not include &key or &whole.

The value of body should be an error triple (see
ERROR-TRIPLES), of the form (mv erp xxx state) for some erp and xxx.
If erp is nil, then xxx is handed off to the proof-checker's instruction
interpreter.  Otherwise, evaluation typically halts.  We may write more
on the full story later if there is interest in reading it.

DEFINE-PC-META    define a proof-checker meta command

Built-in proof-checker meta commands include undo and restore, and
others (lisp, exit, and sequence); see PROOF-CHECKER-COMMANDS.
The advanced proof-checker user can define these as well.  See ACL2
source file proof-checker-b.lisp for examples, and contact the ACL2
implementors if those examples do not provide sufficient documentation.

INSTRUCTIONS    instructions to the proof checker

See PROOF-CHECKER for an introduction to the interactive
"proof-checker" goal manager, which supports much more direct control
of the proof process than is available by direct calls to the prover
(as are normally made using defthm or thm).  In brief, typical use is
to evaluate the form (verify SOME-GOAL), where SOME-GOAL is a formula
(i.e., term) that you would like to prove.  Various commands
(instructions) are available at the resulting prompt; see
PROOF-CHECKER-COMMANDS.  When the proof is completed, suitable
invocation of the exit command will print out a form containing an
:instructions field that provides the instructions that you gave
interactively, so that this form can be evaluated non-interactively.

Thus, also see DEFTHM for the role of :instructions in place of
:hints.  As illustrated by the following example, the value associated
with :instructions is a list of proof-checker commands.

     Example:
     (defthm associativity-of-append
             (equal (append (append x y) z)
                    (append x (append y z)))
             :instructions
             (:induct (:dv 1) (:dv 1) :x :up :x (:dv 2) := (:drop 2)
              :top (:dv 2) :x :top :s :bash))

When you are inside the interactive loop (i.e., after executing
verify), you may invoke help to get a list of legal instructions and
(help instr) to get help for the instruction instr.

Below, we describe a capability for supplying :instructions as :hints.

The most basic utilities for directing the discharge of a proof
obligation are :hints and (less commonly) :instructions.  Individual
instructions may call the prover with :hints; in that sense, prover
hints may occur inside instructions.  We now describe how, on the other
hand, instructions may occur inside hints.

ACL2 supports :instructions as a hints keyword.  The following example
forms the basis for our running example.  This example does not
actually need hints, but imagine that the inductive step -- which is
"Subgoal *1/2" -- was proving difficult.  You could submit that goal to
verify, do an interactive proof, submit (exit t) to obtain the list of
:instructions (answering with `N' at the prompt, to complete the exit),
and then paste in those instructions.  When you submit the result
event, you might see the following.  Below we'll explain the hint
processing.

     ACL2 !>(thm (equal (append (append x y) z)
                        (append x (append y z)))
                 :hints (("Subgoal *1/2"
                          :instructions
                          (:promote (:dv 1) (:dv 1) :x :up :x (:dv 2) :=
                           (:drop 2) :top (:dv 2) :x :top :s))))

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction schemes are
     suggested by this conjecture.  Subsumption reduces that number to two.
     However, one of these is flawed and so we are left with one viable
     candidate.

     We will induct according to a scheme suggested by (BINARY-APPEND X Y).
     This suggestion was produced using the :induction rule BINARY-APPEND.
     If we let (:P X Y Z) denote *1 above then the induction scheme we'll
     use is
     (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y Z))
                   (:P X Y Z))
          (IMPLIES (ENDP X) (:P X Y Z))).
     This induction is justified by the same argument used to admit BINARY-APPEND.
     When applied to the goal at hand the above induction scheme produces
     two nontautological subgoals.

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

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

     But the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC replaces
     this goal by T.

     Subgoal *1/1
     (IMPLIES (ENDP X)
              (EQUAL (APPEND (APPEND X Y) Z)
                     (APPEND X Y Z))).

     By the simple :definition ENDP we reduce the conjecture to

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP X))
              (EQUAL (APPEND (APPEND X Y) Z)
                     (APPEND X Y Z))).

     But simplification reduces this to T, using the :definition BINARY-APPEND
     and primitive type reasoning.

     That completes the proof of *1.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:DEFINITION BINARY-APPEND)
             (:DEFINITION ENDP)
             (:DEFINITION NOT)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:INDUCTION BINARY-APPEND))
     Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)

     Proof succeeded.
     ACL2 !>

To understand how the :instructions supplied above were processed,
observe proof-checker instruction interpreter may be viewed as a
"clause-processor": a function that takes an input goal and returns a
list of goals (which can be the empty list).  Such a function has the
property that if all goals in that returned list are theorems, then so
is the input goal.  This view of the proof-checker instruction
interpreter as a clause-processor leads to the following crucial
observation.

*IMPORTANT!*.  Each call of the proof-checker instruction interpreter is
treated as a standalone clause-processor that is insensitive to the
surrounding prover environment.  In particular:

     o The proof-checker's theory is not sensitive to :in-theory hints
     already processed in the surrounding proof.  Indeed, the current
     theory for which proof-checker commands are processed is just the
     current theory of the ACL2 logical world, i.e., the value of
     (current-theory :here).  Moreover, references to (current-theory
     :here) in a proof-checker in-theory command, even implicit
     references such as provided by enable and disable expressions, are
     also references to the current theory of the ACL2 logical world.

     o The runes used during an :instructions hint are not tracked
     beyond that hint, hence may not show up in the summary of the
     overall proof.  Again, think of the :instructions hint as a
     clause-processor call, which has some effect not tracked by the
     surrounding proof other than for the child goals that it returns.

We continue now with our discussion of the proof-checker instruction
interpreter as a clause-processor.

In the example above, the input goal ("Subgoal *1/2") was processed by
the proof-checker instruction interpreter.  The result was the empty
goal stack, therefore proving the goal, as reported in the output,
which we repeat here.

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

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

     But the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC replaces
     this goal by T.

*Remark.*  This brief remark can probably be ignored, but we include it
for completeness.  The :CLAUSE-PROCESSOR message above may be
surprising, since the hint attached to "Subgoal *1/2" is an
:instructions hint, not a :clause-processor hint.  But :instructions is
actually a custom keyword hint (see CUSTOM-KEYWORD-HINTS), and
may be thought of as a macro that expands to a :clause-processor hint,
one that specifies proof-checker-cl-proc as the clause-processor
function.  The keen observer may notice that the clause-processor is
referred to as "trusted" in the above output.  Normally one needs a
trust tag (see DEFTTAG) to install a trusted clause-processor,
but that is not the case for the built-in clause-processor,
proof-checker-cl-proc.  Finally, we note that :instructions hints are
"spliced" in: the appropriate :clause-processor hint replaces the
:instructions hint, and the other hints remain intact.  It may seems
surprising that one can thus, for example, use :instructions and
:in-theory together; but although the :in-theory hint will have no
effect on execution of the :instructions (see first bullet above), the
:in-theory hint will apply in the usual manner to any child goes (see
HINTS-AND-THE-WATERFALL).  End of Remark.

Now consider the case that the supplied instructions do not prove the
goal.  That is, suppose that the execution of those instructions
results in a non-empty goal stack.  In that case, the resulting goals
become children of the input goals.  The following edited log provides
an illustration using a modification of the above example, this time
with a single instruction that splits into two cases.

     ACL2 !>(thm (equal (append (append x y) z)
                        (append x (append y z)))
                 :hints (("Subgoal *1/2"
                          :instructions
                          ((:casesplit (equal x y))))))

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

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

     We now apply the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC
     to produce two new subgoals.

     Subgoal *1/2.2

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

     Subgoal *1/2.1

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

We have seen that an :instructions hint may produce zero or more
subgoals.  There may be times where you wish to insist that it produce
zero subgoals, i.e., that it prove the desired goal.  The proof-checker
`finish' command works nicely for this purpose.  For example, the
following form is successfully admitted, but if you delete some of the
commands (for example, the :s command at the end), you will see an
informative error message.

     (thm (equal (append (append x y) z)
                 (append x (append y z)))
          :hints (("Subgoal *1/2"
                   :instructions
                   ((finish :promote (:dv 1) (:dv 1) :x :up :x (:dv 2) :=
                            (:drop 2) :top (:dv 2) :x :top :s)))))

If an :instructions hint of the form ((finish ...)) fails to prove the
goal, the clause-processor is deemed to have caused an error.  Indeed,
any "failure" of a supplied proof-checker instruction will be deemed to
cause an error.  In this case, you should see an error message such as
the following:

     Saving proof-checker error state; see :DOC instructions.  To retrieve:

     (RETRIEVE :ERROR1)

In this case, you can evaluate the indicated retrieve command in the
ACL2 read-eval-print loop, to get to the point of failure.

You may have noticed that there is no output from the proof-checker in
the examples above.  This default behavior prevents confusion that
could arise from use of proof-checker commands that call the theorem
prover such as prove, bash, split, and induct.  These commands produce
output for what amounts to a fresh proof attempt, which could confuse
attempts to understand the surrounding proof log.  You can override the
default behavior by providing a command of the form

     (comment inhibit-output-lst VAL)

where VAL is either the keyword :SAME (indicating that no change should
be made to which output is inhibited) or else is a legal value for
inhibited output; see SET-INHIBIT-OUTPUT-LST.  The following
two variants of the immediately preceding THM form will each produce
output from the proof-checker commands, assuming in the first variant
that output hasn't already been inhibited.

     (thm (equal (append (append x y) z)
                        (append x (append y z)))
                 :hints (("Subgoal *1/2"
                          :instructions
                          ((comment inhibit-output-lst :same)
                           (:casesplit (equal x y))))))

     (thm (equal (append (append x y) z)
                        (append x (append y z)))
                 :hints (("Subgoal *1/2"
                          :instructions
                          ((comment inhibit-output-lst (proof-tree))
                           (:casesplit (equal x y))))))

Note that such a comment instruction must be provided explicitly (i.e.,
not by way of a proof-checker macro-command) as the first instruction,
in order to have the effect on inhibited output that is described above.

The following contrived example gives a sense of how one might want to
use :instructions within :hints.  If you submit the following theorem

     (thm (implies (true-listp x)
                   (equal (reverse (reverse x)) x)))

then you will see the following checkpoint printed with the summary.

     Subgoal *1/3''
     (IMPLIES (AND (CONSP X)
                   (EQUAL (REVAPPEND (REVAPPEND (CDR X) NIL) NIL)
                          (CDR X))
                   (TRUE-LISTP (CDR X)))
              (EQUAL (REVAPPEND (REVAPPEND (CDR X) (LIST (CAR X)))
                                NIL)
                     X))

This suggests proving the following theorem.  Here we state it using
defthmd, so that it is immediately disabled.  Normally disabling would
be unnecessary, but for our contrived example it is useful to imagine
disabling it, say because we are following a methodology that tends to
keep rewrite rules disabled.

     (defthmd revappend-revappend
       (equal (revappend (revappend x y) z)
              (revappend y (append x z))))

We might then enter the proof-checker to prove the original theorem
interactively, as follows.

     ACL2 !>(verify (implies (true-listp x)
                             (equal (reverse (reverse x)) x)))
     ->: bash
     ***** Now entering the theorem prover *****

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

     This simplifies, using the :definition REVERSE and the :type-prescription
     rule REVAPPEND, to

     Goal'
     (IMPLIES (TRUE-LISTP X)
              (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
                     X)).

     But we have been asked to pretend that this goal is subsumed by the
     yet-to-be-proved |PROOF-CHECKER Goal'|.

     Q.E.D.

     Creating one new goal:  (MAIN . 1).

     The proof of the current goal, MAIN, has been completed.  However,
     the following subgoals remain to be proved:
       (MAIN . 1).
     Now proving (MAIN . 1).
     ->: th
     *** Top-level hypotheses:
     1. (TRUE-LISTP X)

     The current subterm is:
     (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
            X)
     ->: 1
     ->: sr ; show-rewrites

     1. REVAPPEND-REVAPPEND (disabled)
       New term: (REVAPPEND NIL (APPEND X NIL))
       Hypotheses: <none>
       Equiv: EQUAL

     2. REVAPPEND
       New term: (AND (CONSP (REVAPPEND X NIL))
                      (REVAPPEND (CDR (REVAPPEND X NIL))
                                 (LIST (CAR (REVAPPEND X NIL)))))
       Hypotheses: <none>
       Equiv: EQUAL
     ->: (r 1) ; rewrite with rule #1 above
     Rewriting with REVAPPEND-REVAPPEND.
     ->: exit
     Exiting....
      NIL
     ACL2 !>(verify (implies (true-listp x)
                             (equal (reverse (reverse x)) x)))
     ->: bash
     ***** Now entering the theorem prover *****

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

     This simplifies, using the :definition REVERSE and the :type-prescription
     rule REVAPPEND, to

     Goal'
     (IMPLIES (TRUE-LISTP X)
              (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
                     X)).

     But we have been asked to pretend that this goal is subsumed by the
     yet-to-be-proved |PROOF-CHECKER Goal'|.

     Q.E.D.

     Creating one new goal:  (MAIN . 1).

     The proof of the current goal, MAIN, has been completed.  However,
     the following subgoals remain to be proved:
       (MAIN . 1).
     Now proving (MAIN . 1).
     ->: th
     *** Top-level hypotheses:
     1. (TRUE-LISTP X)

     The current subterm is:
     (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
            X)
     ->: p
     (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
            X)
     ->: 1
     ->: p
     (REVAPPEND (REVAPPEND X NIL) NIL)
     ->: sr ; show-rewrites

     1. REVAPPEND-REVAPPEND (disabled)
       New term: (REVAPPEND NIL (APPEND X NIL))
       Hypotheses: <none>
       Equiv: EQUAL

     2. REVAPPEND
       New term: (AND (CONSP (REVAPPEND X NIL))
                      (REVAPPEND (CDR (REVAPPEND X NIL))
                                 (LIST (CAR (REVAPPEND X NIL)))))
       Hypotheses: <none>
       Equiv: EQUAL
     ->: (r 1) ; rewrite with rule #1 above
     Rewriting with REVAPPEND-REVAPPEND.
     ->: p
     (REVAPPEND NIL (APPEND X NIL))
     ->: top
     ->: prove ; finish the proof
     ***** Now entering the theorem prover *****

     But simplification reduces this to T, using the :definition REVAPPEND,
     the :executable-counterpart of CONSP, primitive type reasoning and
     the :rewrite rule APPEND-TO-NIL.

     Q.E.D.

     *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!*
     You may wish to exit.
     ->: (exit t) ; to get :instructions; could give name, or (exit t nil t)
     (DEFTHM T
             (IMPLIES (TRUE-LISTP X)
                      (EQUAL (REVERSE (REVERSE X)) X))
             :INSTRUCTIONS (:BASH (:DV 1)
                                  (:REWRITE REVAPPEND-REVAPPEND)
                                  :TOP :PROVE))

     ACL2 Query (ACL2-PC::EXIT):
     Do you want to submit this event?  Possible replies are:
     Y (Yes), R (yes and Replay commands), N (No, but exit), A (Abort exiting).
        (Y, R, N or A):  n
      NIL
     ACL2 !>(thm
             (IMPLIES (TRUE-LISTP X)
                      (EQUAL (REVERSE (REVERSE X)) X))
             :hints (("Goal"
                      :INSTRUCTIONS ; copy what was printed above:
                      (:BASH (:DV 1)
                             (:REWRITE REVAPPEND-REVAPPEND)
                             :TOP :PROVE))))

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

     But the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC replaces
     this goal by T.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Proof succeeded.
     ACL2 !>

Finally we present an even more contrived example, based on the one
above.  This example illustrates that there is actually no limit
imposed on the nesting of :instructions within :hints within
:instructions, and so on.  Notice the indication of nesting levels:
"1>" to "<1" for output from nesting level 1, and "2>" to "<2" for
output from nesting level 2.

     (thm (implies (true-listp x)
                   (equal (reverse (reverse x)) x))
          :hints (("Goal"
                   :instructions
                   ((comment inhibit-output-lst :same)
                    (:prove
                     :hints (("Goal" :in-theory (disable append))
                             ("Subgoal *1/3''"
                              :instructions
                              ((comment inhibit-output-lst :same)
                               :bash
                               (:dv 1)
                               (:rewrite revappend-revappend)))))))))

Here is an edited version of the resulting log.

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

     [[1> Executing proof-checker instructions]]

     ->: (COMMENT INHIBIT-OUTPUT-LST :SAME)
     ->: (:PROVE
              :HINTS
              (("Goal" :IN-THEORY (DISABLE APPEND))
               ("Subgoal *1/3''" :INSTRUCTIONS ((COMMENT INHIBIT-OUTPUT-LST :SAME)
                                                :BASH (:DV 1)
                                                (:REWRITE REVAPPEND-REVAPPEND)))))
     ***** Now entering the theorem prover *****

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

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

     Subgoal *1/3''
     (IMPLIES (AND (CONSP X)
                   (EQUAL (REVAPPEND (REVAPPEND (CDR X) NIL) NIL)
                          (CDR X))
                   (TRUE-LISTP (CDR X)))
              (EQUAL (REVAPPEND (REVAPPEND (CDR X) (LIST (CAR X)))
                                NIL)
                     X)).

     [[2> Executing proof-checker instructions]]

     ->: (COMMENT INHIBIT-OUTPUT-LST :SAME)
     ->: :BASH
     ***** Now entering the theorem prover *****

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

     But we have been asked to pretend that this goal is subsumed by the
     yet-to-be-proved |PROOF-CHECKER Goal|.

     Q.E.D.

     Creating one new goal:  (MAIN . 1).

     The proof of the current goal, MAIN, has been completed.  However,
     the following subgoals remain to be proved:
       (MAIN . 1).
     Now proving (MAIN . 1).
     ->: (:DV 1)
     ->: (:REWRITE REVAPPEND-REVAPPEND)
     Rewriting with REVAPPEND-REVAPPEND.

     [[<2 Completed proof-checker instructions]]

     We now apply the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC
     to produce one new subgoal.

     Subgoal *1/3'''

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

     [[<1 Completed proof-checker instructions]]

The nesting levels are independent of whether or not output is enabled;
for example, if the first (comment ...) form below is omitted, then we
will see only the output bracketed by "2>" to "<2".  Note also that
these levels are part of the error states saved for access by retrieve
(as indicated above); for example, a failure at level 1 would be
associated with symbol :ERROR1 as indicated above, while a failure at
level 2 would be associated with symbol :ERROR2.

MACRO-COMMAND    compound command for the proof-checker

The proof-checker (see PROOF-CHECKER) allows the user to supply
interactive commands.  Compound commands, called macro commands, may be
defined; these expand into zero or more other commands.  Some of these
are "atomic" macro commands; these are viewed as a single command step
when completed successfully.

More documentation will be written on the proof-checker.  For now, we
simply point out that there are lots of examples of the use of
define-pc-macro and define-pc-atomic-macro in the ACL2 source file
"proof-checker-b.lisp".  The former is used to create macro commands,
which can be submitted to the interactive loop (see VERIFY) and
will "expand" into zero or more commands.  The latter is similar,
except that the undoing mechanism (see ACL2-PC||UNDO)
understands atomic macro commands to represent single interactive
commands.  Also see ACL2-PC||COMM and see
ACL2-PC||COMMANDS for a discussion of the display of interactive
commands.

Also see TOGGLE-PC-MACRO for how to change a macro command to
an atomic macro command, and vice versa.

PROOF-CHECKER-COMMANDS    list of commands for the proof-checker

This documentation section contains documentation for individual
commands that can be given inside the interactive proof-checker loop
that is entered using verify.

attempt an equality (or equivalence) substitution

same as (lisp x)

add an abbreviation

same as apply-linear

apply a linear rule

call the ACL2 theorem prover's simplifier

prove the current goal using bdds

move backward one argument in the enclosing term

insert matching ``bookends'' comments

split into two cases

change to another goal.

change to another goal.

same as clause-processor

add a new hypothesis

use a clause-processor

display instructions from the current interactive session

display instructions from the current interactive session

insert a comment

same as contrapose

switch a hypothesis with the conclusion, negating both

move top-level hypotheses to the conclusion

move to the indicated subterm

run the given instructions

run the given instructions, halting once there is a ``failure''

run the given instructions, halting once there is a ``failure''

drop top-level hypotheses

move to the indicated subterm

call the ACL2 theorem prover's elimination process

attempt an equality (or congruence-based) substitution

exit after possibly saving the state

exit the interactive proof-checker

expand the current function call without simplification

cause a failure

require completion of instructions; save error if inside :hints

forward chain from an implication in the hyps

create a ``free variable''

show the generated equivalence relation maintained at the current subterm

perform a generalization

list the names of goals on the stack

proof-checker help facility

proof-checker help facility

same as help!

print the hypotheses

illegal instruction

set the current proof-checker theory

generate subgoals using induction

print the runes (definitions, lemmas, ...) used

evaluate the given form in Lisp

proof-checker help facility

proof-checker help facility

run the given instructions, and ``succeed'' if and only if they ``fail''

used for interpreting control-d

run instructions with output

move forward one argument in the enclosing term

run the first instruction; if (and only if) it ``fails'', run the
second

prettyprint the current term

prettyprint the conclusion, highlighting the current term

print the rules for a given name

prettyprint the current term

print the rules for a given name

print the result of evaluating the given form

print all the conclusions of (as yet unproved) goals

print all the (as yet unproved) goals

print the original goal

repeatedly apply promote

move antecedents of conclusion's implies term to top-level
hypotheses

run the given instructions, reverting to existing state upon
failure

call the ACL2 theorem prover to prove the current goal

print the most recent proof attempt from inside the proof-checker

print the most recent proof attempt from inside the proof-checker

print the most recent proof attempt from inside the proof-checker

substitute for a ``free variable''

run instructions without output

same as rewrite

call the ACL2 theorem prover's simplifier

call the ACL2 prover without induction, after going into
induction

remove one or more abbreviations

repeat the given instruction until it ``fails''

auxiliary to repeat

replay one or more instructions

remove the effect of an UNDO command

drop all *but* the indicated top-level hypotheses

re-enter the proof-checker

apply a rewrite rule

auxiliary to THEN

auxiliary to then

print the runes (definitions, lemmas, ...) used

simplify the current subterm

simplify propositionally

save the proof-checker state (state-stack)

run the given list of instructions according to a multitude of
options

display the current abbreviations

display the applicable linear rules

display the applicable rewrite rules

display the applicable type-prescription rules

``succeed'' without doing anything

simplify with lemmas

same as SHOW-LINEARS

split the current goal into cases

same as SHOW-REWRITES

same as SHOW-TYPE-PRESCRIPTIONS

run the given instructions, and ``succeed''

print the top-level hypotheses and the current subterm

apply one instruction to current goal and another to new subgoals

move to the top of the goal

display the type-alist from the current context

undo some instructions

remove a proof-checker state

move to the parent (or some ancestor) of the current subterm

use a lemma instance

execute the indicated instructions and combine all the new goals

same as induct, but create a single goal

combine goals into a single goal

expand and (maybe) simplify function call at the current subterm

expand function call at the current subterm, without simplifying

ACL2-PC||=    (atomic macro)
attempt an equality (or equivalence) substitution

     Examples:
     =     -- replace the current subterm by a term equated to it in
              one of the hypotheses (if such a term exists)
     (= x) -- replace the current subterm by x, assuming that the prover
              can show that they are equal
     (= (+ x y) z)
           -- replace the term (+ x y) by the term z inside the current
              subterm, assuming that the prover can prove
              (equal (+ x y) z) from the current top-level hypotheses
              or that this term or (equal z (+ x y)) is among the
              current top-level hypotheses or the current governors
     (= & z)
           -- exactly the same as above, if (+ x y) is the current
              subterm
     (= (+ x y) z :hints :none)
           -- same as (= (+ x y) z), except that a new subgoal is
              created with the current goal's hypotheses and governors
              as its top-level hypotheses and (equal (+ x y) z) as its
              conclusion
     (= (+ x y) z 0)
           -- exactly the same as immediately above
     (= (p x)
        (p y)
        :equiv iff
        :otf-flg t
        :hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar)))
           -- same as (= (+ x y) z), except that the prover uses
              the indicated values for otf-flg and hints, and only
              propositional (iff) equivalence is used (however, it
              must be that only propositional equivalence matters at
              the current subterm)

     General Form:
     (= &optional x y &rest keyword-args)

If terms x and y are supplied, then replace x by y inside the current
subterm if they are "known" to be "equal".  Here "known" means the
following:  the prover is called as in the prove command (using
keyword-args) to prove (equal x y), except that a keyword argument
:equiv is allowed, in which case (equiv x y) is proved instead, where
equiv is that argument.  (See below for how governors are handled.)

Actually, keyword-args is either a single non-keyword or is a list of
the form ((kw-1 x-1) ... (kw-n x-n)), where each kw-i is one of the
keywords :equiv, :otf-flg, :hints.  Here :equiv defaults to equal if
the argument is not supplied or is nil, and otherwise should be the
name of an ACL2 equivalence relation.  :Otf-flg and :hints give
directives to the prover, as explained above and in the documentation
for the prove command; however, no prover call is made if :hints is a
non-nil atom or if keyword-args is a single non-keyword (more on this
below).

_Remarks on defaults_

(1) If there is only one argument, say a, then x defaults to the
current subterm, in the sense that x is taken to be the current subterm
and y is taken to be a.

(2) If there are at least two arguments, then x may be the symbol &,
which then represents the current subterm.  Thus, (= a) is equivalent
to (= & a).  (Obscure point:  actually, & can be in any package, except
the keyword package.)

(3) If there are no arguments, then we look for a top-level hypothesis
or a governor of the form (equal c u) or (equal u c), where c is the
current subterm.  In that case we replace the current subterm by u.

As with the prove command, we allow goals to be given "bye"s in the
proof, which may be generated by a :hints keyword argument in
keyword-args.  These result in the creation of new subgoals.

A proof is attempted unless the :hints argument is a non-nil atom other
than :none, or unless there is one element of keyword-args and it is
not a keyword.  In that case, if there are any hypotheses in the
current goal, then what is attempted is a proof of the implication
whose antecedent is the conjunction of the current hypotheses and
governors and whose conclusion is the appropriate equal term.

*Remarks:*  (1) It is allowed to use abbreviations in the hints.  (2)
The keyword :none has the special role as a value of :hints that is
shown clearly in an example above.  (3) If there are governors, then
the new subgoal has as additional hypotheses the current governors.

ACL2-PC||ACL2-WRAP    (macro)
same as (lisp x)

     Example:
     (acl2-wrap (pe :here))

     General Form:
     (acl2-wrap form)

Same as (lisp form).  This is provided for interface tools that want to
be able to execute the same form in raw Lisp, in the proof-checker, or
in the ACL2 top-level loop (lp).

ACL2-PC||ADD-ABBREVIATION    (primitive)
add an abbreviation

Example:  (add-abbreviation v (* x y)) causes future occurrences of (*
x y) to be printed as (? v), until (unless) a corresponding invocation
of remove-abbreviations occurs.  In this case we say that v
"abbreviates" (* x y).

     General Form:
     (add-abbreviation var &optional raw-term)

Let var be an abbreviation for raw-term, if raw-term is supplied, else
for the current subterm.  Note that var must be a variable that does
not already abbreviate some term.

A way to think of abbreviations is as follows.  Imagine that whenever
an abbreviation is added, say v abbreviates expr, an entry associating
v to expr is made in an association list, which we will call
"*abbreviations-alist*".  Then simply imagine that ? is a function
defined by something like:

     (defun ? (v)
       (let ((pair (assoc v *abbreviations-alist*)))
         (if pair (cdr pair)
           (error ...))))

Of course the implementation isn't exactly like that, since the
"constant" *abbreviations-alist* actually changes each time an
add-abbreviation instruction is successfully invoked.  Nevertheless, if
one imagines an appropriate redefinition of the "constant"
*abbreviations-alist* each time an add-abbreviation is invoked, then
one will have a clear model of the meaning of such an instruction.

The effect of abbreviations on output is that before printing a term,
each subterm that is abbreviated by a variable v is first replaced by
(? v).

The effect of abbreviations on input is that every built-in
proof-checker command accepts abbreviations wherever a term is expected
as an argument, i.e., accepts the syntax (? v) whenever v abbreviates a
term.  For example, the second argument of add-abbreviation may itself
use abbreviations that have been defined by previous add-abbreviation
instructions.

See also remove-abbreviations and show-abbreviations.

ACL2-PC||AL    (macro)
same as apply-linear

     Example:
     (al 3)

See the documentation for apply-linear, as al and apply-linear are
identical.

ACL2-PC||APPLY-LINEAR    (primitive)
apply a linear rule

     Examples:
     (apply-linear foo)
        -- apply the linear rule `foo'
     (apply-linear (:linear foo))
        -- same as above
     (apply-linear 2)
        -- apply the second linear rule, as displayed by show-linears
     rewrite
        -- apply the first rewrite rule, as displayed by show-rewrites
     (apply-linear foo ((y 7)))
        -- apply the linear rule foo with the substitution
           that associates 7 to the ``free variable'' y
     (apply-linear foo ((x 2) (y 3)) t)
        -- apply the linear rule foo by substituting 2 and 3 for free
           variables x and y, respectively, and also binding all other
           free variables possible by using the current context
           (hypotheses and governors)

     General Form:
     (apply-linear &optional rule-id substitution instantiate-free)

Add a new top-level hypothesis by applying a linear rule to the current
subterm.  The new hypothesis will be created according to the
information provided by the show-linears (sls) command.

A short name for this command is al.

We assume familiarity with the proof-checker's rewrite (r) command.  In
brief, the apply-linear command is an analogue of the rewrite command,
but for linear rules in place of rewrite rules.  There is a significant
difference: for the apply-linear command, instead of rewriting the
current subterm as is done by the rewrite command, the conclusion of
the applicable linear rule, suitably instantiated, is added as a new
(and last) top-level hypothesis of the goal.  There is another
significant difference: the automatic application of linear rules in
the theorem prover is somewhat more complex than the automatic
application of rewrite rules, so the apply-linear command may not
correspond as closely to the prover's automatic use of a linear rule as
the rewrite command corresponds to the prover's automatic use of a
rewrite rule.

Below, we refer freely to the documentation for the proof-checker's
rewrite command.

The rule-id is treated just as it is by the rewrite command.  If
rule-id is a positive integer n, then the nth rule as displayed by
show-linears is the one that is applied.  If rule-id is nil or is not
supplied, then it is treated as the number 1.  Otherwise, rule-id
should be either a symbol or else a :linear rune.  If a symbol is
supplied, then any linear rule of that name may be used.

Consider the following example.  Suppose that the current subterm is (<
(g (h y)) y) and that foo is the name of the following linear rule.

     (implies (true-listp x)
              (< (g x) 15))

Then the instruction (apply-linear foo) applies foo by adding a new
hypothesis (< (g (h y)) 15).  In addition, a new goal with conclusion
(true-listp y) is created unless the current context (top-level
hypotheses and governors) implies (true-listp y) using only "trivial
reasoning", just as for the rewrite command.

If the rule-id argument is a number or is not supplied, then the system
will store an instruction of the form (apply-linear name ...), where
name is the name of a linear rule; this is in order to make it easier
to replay instructions when there have been changes to the history.
Except: instead of the name (whether the name is supplied or
calculated), the system stores the rune if there is any chance of
ambiguity.  (Formally, "ambiguity" here means that the rune being
applied is of the form (:rewrite name . index), where index is not nil.)

Speaking in general, then, an apply-linear instruction works as follows.

First, a linear rule is selected according to the arguments of the
instruction.  The selection is made as explained under "General Form"
above.

Next, a trigger term of the rule (see LINEAR) is matched with
the current subterm, i.e., a substitution unify-subst is found such
that if one instantiates that trigger term of the rule with
unify-subst, then one obtains the current subterm.  If this match
fails, then the instruction fails.

Next, an attempt is made to relieve (discharge) the hypotheses, possibly
handling free variables (see FREE-VARIABLES), exactly as is
done with hypotheses when applying the proof-checker command, rewrite
(r).

Finally, the instruction is applied exactly as the rewrite instruction
is applied, except instead of replacing the current subterm, the rule's
instantiated conclusion is added to the end of the list of top-level
hypotheses of the goal.

Note that as for the rewrite command, the substitution argument should
be a list whose elements have the form (variable term), where term may
contain abbreviations.

ACL2-PC||BASH    (atomic macro)
call the ACL2 theorem prover's simplifier

     Examples:
     bash -- attempt to prove the current goal by simplification alone
     (bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
          -- attempt to prove the current goal by simplification alone,
             with the indicated hints

     General Form:
     (bash &rest hints)

Call the theorem prover's simplifier, creating a subgoal for each
resulting goal.

Notice that unlike prove, the arguments to bash are spread out, and are
all hints.

Bash is similar to reduce in that neither of these allows induction.
But bash only allows simplification, while reduce allows processes
eliminate-destructors, fertilize, generalize, and eliminate-irrelevance.

*Remark:*  All forcing rounds will be skipped (unless there are more
than 15 subgoals generated in the first forcing round, an injustice
that should be rectified, but might remain unless there is pressure to
fix it).

ACL2-PC||BDD    (atomic macro)
prove the current goal using bdds

     Examples:
     bdd
     (bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)

The general form is as shown in the latter example above, but with any
keyword-value pairs omitted and with values as described for the :bdd
hint; see HINTS.

This command simply calls the theorem prover with the indicated bdd
hint for the top-level goal.  Note that if :prove is t (the default),
then the proof will succeed entirely using bdds or else it will fail
immediately.  See BDD.

ACL2-PC||BK    (atomic macro)
move backward one argument in the enclosing term

     Example and General Form:
     bk

For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is (* (- y) z), then after executing bk, the current subterm
will be x.

Move to the previous argument of the enclosing term.

This is the same as up followed by (dive n-1), where n is the position
of the current subterm in its parent term in the conclusion.  Thus in
particular, the nx command fails if one is already at the top of the
conclusion.

See also up, dive, top, and bk.

ACL2-PC||BOOKMARK    (macro)
insert matching "bookends" comments

     Example:
     (bookmark final-goal)

     General Form:
     (bookmark name &rest instruction-list)

Run the instructions in instruction-list (as though this were a call of
do-all; see the documentation for do-all), but first insert a begin
bookend with the given name and then, when the instructions have been
completed, insert an end bookend with that same name.  See the
documentation of comm for an explanation of bookends and how they can
affect the display of instructions.

ACL2-PC||CASESPLIT    (primitive)
split into two cases

     Example:
     (casesplit (< x y)) -- assuming that we are at the top of the
                            conclusion, add (< x y) as a new top-level
                            hypothesis in the current goal, and create a
                            subgoal identical to the current goal except
                            that it has (not (< x y)) as a new top-level
                            hypothesis

     General Form:
     (casesplit expr &optional use-hyps-flag do-not-flatten-flag)

When the current subterm is the entire conclusion, this instruction
adds expr as a new top-level hypothesis, and create a subgoal identical
to the existing current goal except that it has the negation of expr as
a new top-level hypothesis.  See also claim.  The optional arguments
control the use of governors and the "flattening" of new hypotheses, as
we now explain.

The argument use-hyps-flag is only of interest when there are
governors.  (To read about governors, see the documentation for the
command hyps).  In that case, if use-hyps-flag is not supplied or is
nil, then the description above is correct; but otherwise, it is not
expr but rather it is (implies govs expr) that is added as a new
top-level hypothesis (and whose negation is added as a top-level
hypothesis for the new goal), where govs is the conjunction of the
governors.

If do-not-flatten-flag is supplied and not nil, then that is all there
is to this command.  Otherwise (thus this is the default), when the
claimed term (first argument) is a conjunction (and) of terms and the
claim instruction succeeds, then each (nested) conjunct of the claimed
term is added as a separate new top-level hypothesis.  Consider the
following example, assuming there are no governors.

     (casesplit (and (and (< x y) (integerp a)) (equal r s)) t)

Three new top-level hypotheses are added to the current goal, namely (<
x y), (integerp a), and (equal r s).  In that case, only one hypothesis
is added to create the new goal, namely the negation of (and (< x y)
(integerp a) (equal r s)).  If the negation of this term had been
claimed, then it would be the other way around:  the current goal would
get a single new hypothesis while the new goal would be created by
adding three hypotheses.

*Remark:*  It is allowed to use abbreviations in the hints.

ACL2-PC||CG    (macro)
change to another goal.

     Examples:
     (cg (main . 1)) -- change to the goal (main . 1)
     cg              -- change to the next-to-top goal

     General Form:
     (CG &OPTIONAL goal-name)

Same as (change-goal goal-name t), i.e. change to the indicated and
move the current goal to the end of the goal stack.

ACL2-PC||CHANGE-GOAL    (primitive)
change to another goal.

     Examples:
     (change-goal (main . 1)) -- change to the goal (main . 1)
     change-goal              -- change to the next-to-top goal

     General Form:
     (change-goal &optional goal-name end-flg)

Change to the goal with the name goal-name, i.e. make it the current
goal.  However, if goal-name is nil or is not supplied, then it
defaults to the next-to-top goal, i.e., the second goal in the stack of
goals.  If end-flg is supplied and not nil, then move the current goal
to the end of the goal stack; else merely swap it with the next-to-top
goal.  Also see documentation for cg.

ACL2-PC||CL-PROC    (macro)
same as clause-processor

See the documentation for proof-checker command clause-processor, which
is identical to cl-proc.

ACL2-PC||CLAIM    (atomic macro)
add a new hypothesis

     Examples:
     (claim (< x y))   -- attempt to prove (< x y) from the current
                          top-level hypotheses and if successful, then
                          add (< x y) as a new top-level hypothesis in
                          the current goal
     (claim (< x y)
            :otf-flg t
            :hints (("Goal" :induct t)))
                       -- as above, but call the prover using the
                          indicated values for the otf-flg and hints
     (claim (< x y) 0) -- as above, except instead of attempting to
                          prove (< x y), create a new subgoal with the
                          same top-level hypotheses as the current goal
                          that has (< x y) as its conclusion
     (claim (< x y) :hints :none)
                       -- same as immediately above

     General Form:
     (claim expr &rest rest-args)

This command creates a new subgoal with the same top-level hypotheses
as the current goal but with a conclusion of expr.  If rest-args is a
non-empty list headed by a non-keyword, then there will be no proof
attempted for the new subgoal.  With that possible exception, rest-args
should consist of keyword arguments.  The keyword argument
:do-not-flatten controls the "flattening" of new hypotheses, just as
with the casesplit command (as described in its documentation).  The
remaining rest-args are used with a call the prove command on the new
subgoal, except that if :hints is a non-nil atom, then the prover is
not called -- rather, this is the same as the situation described
above, where rest-args is a non-empty list headed by a non-keyword.

*Remarks:*  (1) Unlike the casesplit command, the claim command is
completely insensitive to governors. (2) It is allowed to use
abbreviations in the hints.  (3) The keyword :none has the special role
as a value of :hints that is shown clearly in an example above.

ACL2-PC||CLAUSE-PROCESSOR    (atomic macro)
use a clause-processor

     Example:
     (cl-proc :function
              note-fact-clause-processor
             :hint
             '(equal a a))
     -- Invoke the indicated clause processor function with the indicated hint
     argument (see the beginning of community book
     books/clause-processors/basic-examples.lisp.

     General Form:
     (cl-proc &rest cl-proc-args)

Invoke a clause-processor as indicated by cl-proc-args, which is a list
of arguments that can serve as the value of a :clause-processor hint;
see HINTS.

This command calls the prove command, and hence should only be used at
the top of the conclusion.

ACL2-PC||COMM    (macro)
display instructions from the current interactive session

     Examples:
     comm
     (comm 10)

     General Form:
     (comm &optional n)

Prints out instructions in reverse order.  This is actually the same as
(commands n t) -- or, (commands nil t) if n is not supplied.  As
explained in the documentation for commands, the final argument of t
causes suppression of instructions occurring between so-called
"matching bookends," which we now explain.

A "begin bookend" is an instruction of the form

     (COMMENT :BEGIN x . y).

Similarly, an "end bookend" is an instruction of the form

     (COMMENT :END x' . y').

The "name" of the first bookend is x and the "name" of the second
bookend is x'.  When such a pair of instructions occurs in the current
state-stack, we call them "matching bookends" provided that they have
the same name (i.e. x equals x') and if no other begin or end bookend
with name x occurs between them.  The idea now is that comm hides
matching bookends together with the instructions they enclose.  Here is
a more precise explanation of this "hiding"; probably there is no value
in reading on!

A comm instruction hides bookends in the following manner.  (So does a
comment instruction when its second optional argument is supplied and
non-nil.)  First, if the first argument n is supplied and not nil, then
we consider only the last n instructions from the state-stack;
otherwise, we consider them all.  Now the resulting list of
instructions is replaced by the result of applying the following
process to each pair of matching bookends:  the pair is removed,
together with everything in between the begin and end bookend of the
pair, and all this is replaced by the "instruction"

     ("***HIDING***" :COMMENT :BEGIN name ...)

where (comment begin name ...) is the begin bookend of the pair.
Finally, after applying this process to each pair of matching bookends,
each begin bookend of the form (comment begin name ...)  that remains
is replaced by

     ("***UNFINISHED***" :COMMENT :BEGIN name ...) .

ACL2-PC||COMMANDS    (macro)
display instructions from the current interactive session

     Examples:
     commands
     (commands 10 t)

     General Forms:

     commands or (commands nil)
     Print out all the instructions (in the current state-stack) in
     reverse order, i.e. from the most recent instruction to the starting
     instruction.

     (commands n) [n a positive integer]
     Print out the most recent n instructions (in the current
     state-stack), in reverse order.

     (commands x abbreviate-flag)
     Same as above, but if abbreviate-flag is non-NIL, then do not
     display commands between ``matching bookends''.  See documentation
     for comm for an explanation of matching bookends.

*Remark*:  If there are more than n instructions in the state-stack,
then (commands n) is the same as commands (and also, (commands n abb)
is the same as (commands nil abb)).

ACL2-PC||COMMENT    (primitive)
insert a comment

     Example:
     (comment now begin difficult final goal)

     General Form:
     (comment &rest x)

This instruction makes no change in the state except to insert the
comment instruction.

Some comments can be used to improve the display of commands; see
documentation for comm.

ACL2-PC||CONTRADICT    (macro)
same as contrapose

see documentation for contrapose

ACL2-PC||CONTRAPOSE    (primitive)
switch a hypothesis with the conclusion, negating both

     Example:
     (contrapose 3)

     General Form:
     (contrapose &optional n)

The (optional) argument n should be a positive integer that does not
exceed the number of hypotheses.  Negate the current conclusion and
make it the nth hypothesis, while negating the current nth hypothesis
and making it the current conclusion.  If no argument is supplied then
the effect is the same as for (contrapose 1).

*Remark:* By "negate" we mean an operation that replaces nil by t, x by
nil for any other explicit value x, (not x) by x, and any other x by
(not x).

ACL2-PC||DEMOTE    (primitive)
move top-level hypotheses to the conclusion

     Examples:
     demote        -- demote all top-level hypotheses
     (demote 3 5)  -- demote hypotheses 3 and 5

For example, if the top-level hypotheses are x and y and the conclusion
is z, then after execution of demote, the conclusion will be (implies
(and x y) z) and there will be no (top-level) hypotheses.

     General Form:
     (demote &rest hyps-indices)

Eliminate the indicated (top-level) hypotheses, but replace the
conclusion conc with (implies hyps conc) where hyps is the conjunction
of the hypotheses that were eliminated.  If no arguments are supplied,
then all hypotheses are demoted, i.e. demote is the same as (demote 1 2
... n) where n is the number of top-level hypotheses.

*Remark*:  You must be at the top of the conclusion in order to use
this command.  Otherwise, first invoke top.  Also, demote fails if
there are no top-level hypotheses or if indices are supplied that are
out of range.

ACL2-PC||DIVE    (primitive)
move to the indicated subterm

     Examples:
     (DIVE 1)    -- assign the new current subterm to be the first
                    argument of the existing current subterm
     (DIVE 1 2)  -- assign the new current subterm to be the result of
                    first taking the 1st argument of the existing
                    current subterm, and then the 2nd argument of that

For example, if the current subterm is

     (* (+ a b) c),

then after (dive 1) it is

     (+ a b).

If after that, then (dive 2) is invoked, the new current subterm will be

     b.

Instead of (dive 1) followed by (dive 2), the same current subterm
could be obtained by instead submitting the single instruction (dive 1
2).

     General Form:
     (dive &rest naturals-list)

If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers,
let the new current subterm be the result of selecting the n_1-st
argument of the current subterm, and then the n_2-th subterm of that,
..., finally the n_k-th subterm.

*Remark:*  Dive is related to the command pp, in that the diving is
done according to raw (translated, internal form) syntax.  Use the
command dv if you want to dive according to the syntax displayed by the
command p.  Note that (dv n) can be abbreviated by simply n.

ACL2-PC||DO-ALL    (macro)
run the given instructions

     Example:
     (do-all induct p prove)

     General Form:
     (do-all &rest instruction-list)

Run the indicated instructions until there is a hard "failure".  The
instruction "succeeds" if and only if each instruction in
instruction-list does.  (See the documentation for sequence for an
explanation of "success" and "failure.")  As each instruction is
executed, the system will print the usual prompt followed by that
instruction, unless the global state variable
pc-print-prompt-and-instr-flg is nil.

*Remark:*  If do-all "fails", then the failure is hard if and only if
the last instruction it runs has a hard "failure".

Obscure point:  For the record, (do-all ins_1 ins_2 ... ins_k) is the
same as (sequence (ins_1 ins_2 ... ins_k)).

ACL2-PC||DO-ALL-NO-PROMPT    (macro)
run the given instructions, halting once there is a "failure"

     Example:
     (do-all-no-prompt induct p prove)

     General Form:
     (do-all-no-prompt &rest instruction-list)

Do-all-no-prompt is the same as do-all, except that the prompt and
instruction are not printed each time, regardless of the value of
pc-print-prompt-and-instr-flg.  Also, restoring is disabled.  See the
documentation for do-all.

ACL2-PC||DO-STRICT    (macro)
run the given instructions, halting once there is a "failure"

     Example:
     (do-strict induct p prove)

     General Form:
     (do-strict &rest instruction-list)

Run the indicated instructions until there is a (hard or soft)
"failure".  In fact do-strict is identical in effect to do-all, except
that do-all only halts once there is a hard "failure".  See the
documentation for do-all.

ACL2-PC||DROP    (primitive)
drop top-level hypotheses

     Examples:
     (drop 2 3) -- drop the second and third hypotheses
     drop       -- drop all top-level hypotheses

     General Forms:
     (drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.

     drop             -- Drop all the top-level hypotheses.

*Remark:*  If there are no top-level hypotheses, then the instruction
drop will fail.  If any of the indices is out of range, i.e. is not an
integer between one and the number of top-level hypotheses (inclusive),
then (drop n1 n2 ...) will fail.

ACL2-PC||DV    (atomic macro)
move to the indicated subterm

     Examples:
     (dv 1)    -- assign the new current subterm to be the first argument
                  of the existing current subterm
     (dv 1 2)  -- assign the new current subterm to be the result of
                  first taking the 1st argument of the existing
                  current subterm, and then the 2nd argument of that

For example, if the current subterm is

     (* (+ a b) c),

then after (dv 1) it is

     (+ a b).

If after that, then (dv 2) is invoked, the new current subterm will be

     b.

Instead of (dv 1) followed by (dv 2), the same current subterm could be
obtained by instead submitting the single instruction (dv 1 2).

     General Form:
     (dv &rest naturals-list)

If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers,
let the new current subterm be the result of selecting the n_1-st
argument of the current subterm, and then the n_2-th subterm of that,
..., finally the n_k-th subterm.

*Remark:*  (dv n) may be abbreviated by simply n, so we could have
typed 1 instead of (dv 1) in the first example above.

*Remark:*  See also dive, which is related to the command pp, in that
the diving is done according to raw (translated, internal form) syntax.
Use the command dv if you want to dive according to the syntax
displayed by the command p.  Thus, the command "up" is the inverse of
dive, not of dv.  The following example illustrates this point.

     ACL2 !>(verify (equal (* a b c) x))
     ->: p ; print user-level term
     (EQUAL (* A B C) X)
     ->: pp ; print internal-form (translated) term
     (EQUAL (BINARY-* A (BINARY-* B C)) X)
     ->: exit
     Exiting....
      NIL
     ACL2 !>(verify (equal (* a b c) x))
     ->: p
     (EQUAL (* A B C) X)
     ->: 1 ; same as (dv 1)
     ->: p ; print user-level term
     (* A B C)
     ->: pp ; print internal-form (translated) term
     (BINARY-* A (BINARY-* B C))
     ->: 3 ; dive to third argument of (* A B C)
     ->: p
     C
     ->: up ; go up one level in (BINARY-* A (BINARY-* B C))
     ->: p
     (* B C)
     ->: pp
     (BINARY-* B C)
     ->:

ACL2-PC||ELIM    (atomic macro)
call the ACL2 theorem prover's elimination process

     Example and General Form:
     elim

Upon running the elim command, the system will create a subgoal will be
created for each goal that would have been pushed for proof by
induction in an ordinary proof, where *only* elimination is used; not
even simplification is used!

ACL2-PC||EQUIV    (primitive)
attempt an equality (or congruence-based) substitution

     Examples:
     (equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
                          current subterm, if their equality is among the
                          top-level hypotheses or the governors
     (equiv x t iff)   -- replace x by t everywhere inside the current
                          subterm, where only propositional equivalence
                          needs to be maintained at each occurrence of x

     General form:
     (equiv old new &optional relation)

Substitute new for old everywhere inside the current subterm, provided
that either (relation old new) or (relation new old) is among the
top-level hypotheses or the governors (possibly by way of backchaining
and/or refinement; see below).  If relation is nil or is not supplied,
then it defaults to equal.  See also the command =, which is much more
flexible.  Note that this command fails if no substitution is actually
made.

*Remark:*  No substitution takes place inside explicit values.  So for
example, the instruction (equiv 3 x) will cause 3 to be replaced by x
if the current subterm is, say, (* 3 y), but not if the current subterm
is (* 4 y) even though 4 = (1+ 3).

The following remarks are quite technical and mostly describe a certain
weak form of "backchaining" that has been implemented for equiv in
order to support the = command.  In fact neither the term (relation old
new) nor the term (relation new old) needs to be *explicitly* among the
current "assumptions", i.e., the top-level hypothesis or the governors.
Rather, there need only be such an assumption that "tells us" (r old
new) or (r new old), for *some* equivalence relation r that *refines*
relation.  Here, "tells us" means that either one of the indicated
terms is among those assumptions, or else there is an assumption that
is an implication whose conclusion is one of the indicated terms and
whose hypotheses (gathered up by appropriately flattening the first
argument of the implies term) are all among the current assumptions.

ACL2-PC||EX    (macro)
exit after possibly saving the state

     Example and General Form:
     ex

Same as exit, except that first the instruction save is executed.

If save queries the user and is answered negatively, then the exit is
aborted.

ACL2-PC||EXIT    (meta)
exit the interactive proof-checker

     Examples:
     exit                        -- exit the interactive proof-checker
     (exit append-associativity) -- exit and create a defthm
                                    event named append-associativity

     General Forms:

     exit --  Exit without storing an event.

     (exit event-name &optional rule-classes do-it-flg)
     Exit, and store an event.

The command exit returns you to the ACL2 loop.  At a later time,
(verify) may be executed to get back into the same proof-checker state,
as long as there hasn't been an intervening use of the proof-checker
(otherwise see save).

When given one or more arguments as shown above, exit still returns you
to the ACL2 loop, but first, if the interactive proof is complete, then
it attempts create a defthm event with the specified event-name and
rule-classes (which defaults to (:rewrite) if not supplied).  The event
will be printed to the terminal, and then normally the user will be
queried whether an event should really be created.  However, if the
final optional argument do-it-flg is supplied and not nil, then an
event will be made without a query.

For example, the form

     (exit top-pop-elim (:elim :rewrite) t)

causes a defthm event named top-pop-elim to be created with
rule-classes (:elim :rewrite), without a query to the user (because of
the argument t).

*Remark:* it is permitted for event-name to be nil.  In that case, the
name of the event will be the name supplied during the original call of
verify.  (See the documentation for verify and commands.)  Also in that
case, if rule-classes is not supplied then it defaults to the
rule-classes supplied in the original call of verify.

Comments on "success" and "failure".  An exit instruction will always
"fail", so for example, if it appears as an argument of a do-strict
instruction then none of the later (instruction) arguments will be
executed.  Moreover, the "failure" will be "hard" if an event is
successfully created or if the instruction is simply exit; otherwise it
will be "soft".  See the documentation for sequence for an explanation
of hard and soft "failures".  An obscure but potentially important fact
is that if the "failure" is hard, then the error signal is a special
signal that the top-level interactive loop can interpret as a request
to exit.  Thus for example, a sequencing command that turns an error
triple (mv erp val state) into (mv t val state) would never cause an
exit from the interactive loop.

If the proof is not complete, then (exit event-name ...) will not cause
an exit from the interactive loop.  However, in that case it will print
out the original user-supplied goal (the one that was supplied with the
call to verify) and the current list of instructions.

ACL2-PC||EXPAND    (primitive)
expand the current function call without simplification

     Examples:
     expand -- expand and do not simplify.

For example, if the current subterm is (append a b), then after (expand
t) the current subterm will be the term:

     (if (true-listp x)
         (if x
             (cons (car x) (append (cdr x) y))
           y)
       (apply 'binary-append (list x y)))

regardless of the top-level hypotheses and the governors.

     General Form:
     (expand &optional do-not-expand-lambda-flg)

Expand the function call at the current subterm, and do not simplify.
The options have the following meanings:

     do-not-expand-lambda-flg:   default is nil; otherwise, the result
                                 should be a lambda expression

See also x, which allows simplification.

ACL2-PC||FAIL    (macro)
cause a failure

     Examples:
     fail
     (fail t)

     General Form:
     (fail &optional hard)

This is probably only of interest to writers of macro commands.  The
only function of fail is to fail to "succeed".

The full story is that fail and (fail nil) simply return (mv nil nil
state), while (fail hard) returns (mv hard nil state) if hard is not
nil.  See also do-strict, do-all, and sequence.

ACL2-PC||FINISH    (macro)
require completion of instructions; save error if inside :hints

     Example:
     (finish induct prove bash)

     General Form:
     (finish &rest instructions)

Run the indicated instructions, stopping at the first failure.  If
there is any failure, or if any new goals are created and remain at the
end of the indicated instructions, then consider the call of finish to
be a failure.  See PROOF-CHECKER-COMMANDS and visit the
documentation for sequence for a discussion of the notion of "failure"
for proof-checker commands.

ACL2-PC||FORWARDCHAIN    (atomic macro)
forward chain from an implication in the hyps

     Example:
     (forwardchain 2) ; Second hypothesis should be of the form
                      ; (IMPLIES hyp concl), and the result is to replace
                      ; that hypothesis with concl.

     General Forms:
     (forwardchain hypothesis-number)
     (forwardchain hypothesis-number hints)
     (forwardchain hypothesis-number hints quiet-flg)

This command replaces the hypothesis corresponding to given index,
which should be of the form (IMPLIES hyp concl), with its consequent
concl.  In fact, the given hypothesis is dropped, and the replacement
hypothesis will appear as the final hypothesis after this command is
executed.

The prover must be able to prove the indicated hypothesis from the
other hypotheses, or else the command will fail.  The :hints argument
is used in this prover call, and should have the usual syntax of hints
to the prover.

Output is suppressed if quiet-flg is supplied and not nil.

ACL2-PC||FREE    (atomic macro)
create a "free variable"

     Example:
     (free x)

     General Form:
     (free var)

Mark var as a "free variable".  Free variables are only of interest for
the put command; see its documentation for an explanation.

ACL2-PC||GENEQV    (macro)
show the generated equivalence relation maintained at the current subterm

     General Forms:
     geneqv     ; show list of equivalence relations being maintained
     (geneqv t) ; as above, but pair each relation with a justifying rune

This is an advanced command, whose effect is to print the so-called
"generated equivalence relation" (or "geneqv") that is maintained at the
current subterm of the conclusion.  That structure is a list of
equivalence relations, representing the transitive closure E of the
union of those relations, such that it suffices to maintain E at the
current subterm: if that subterm, u, is replaced in the goal's
conclusion, G, by another term equivalent to u with respect to E, then
the resulting conclusion is Boolean equivalent to G.  Also see
DEFCONG.

The command `geneqv' prints the above list of equivalence relations, or
more precisely, the list of function symbols for those relations.  If
however geneqv is given a non-nil argument, then a list is printed whose
elements are each of the form (s r), where s is the symbol for an
equivalence relation and r is a :congruence rune justifying the
inclusion of s in the list of equivalence relations being maintained at
the current subterm.

ACL2-PC||GENERALIZE    (primitive)
perform a generalization

     Example:
     (generalize
      ((and (true-listp x) (true-listp y)) 0)
      ((append x y) w))

     General Form:
     (generalize &rest substitution)

Generalize using the indicated substitution, which should be a
non-empty list.  Each element of that list should be a two-element list
of the form (term variable), where term may use abbreviations.  The
effect of the instruction is to replace each such term in the current
goal by the corresponding variable.  This replacement is carried out by
a parallel substitution, outside-in in each hypothesis and in the
conclusion.  More generally, actually, the "variable" (second)
component of each pair may be nil or a number, which causes the system
to generate a new name of the form _ or _n, with n a natural number;
more on this below.  However, when a variable is supplied, it must not
occur in any goal of the current proof-checker state.

When the "variable" above is nil, the system will treat it as the
variable |_| if that variable does not occur in any goal of the current
proof-checker state.  Otherwise it treats it as |_0|, or |_1|, or |_2|,
and so on, until one of these is not among the variables of the current
proof-checker state.  If the "variable" is a non-negative integer n,
then the system treats it as |_n| unless that variable already occurs
among the current goals, in which case it increments n just as above
until it obtains a new variable.

*Remark:*  The same variable may not occur as the variable component of
two different arguments (though nil may occur arbitrarily many times,
as may a positive integer).

ACL2-PC||GOALS    (macro)
list the names of goals on the stack

     Example and General Form:
     goals

Goals lists the names of all goals that remain to be proved.  They are
listed in the order in which they appear on the stack of remaining
goals, which is relevant for example to the effect of a change-goal
instruction.

ACL2-PC||HELP    (macro)
proof-checker help facility

     Examples:

     (help all)     -- list all proof-checker commands
     (help rewrite) -- partial documentation on the rewrite command; the
                       rest is available using more or more!

     (help! rewrite) -- full documentation on the rewrite command

     help, help!     -- this documentation (in part, or in totality,
                        respectively)

     General Forms:
     (help &optional command)
     (help! &optional command)
     more
     more!

The proof checker supports the same kind of documentation as does ACL2
proper.  The main difference is that you need to type

     (help command)

in a list rather than :doc command.  So, to get all the documentation
on command, type (help! command) inside the interactive loop, but to
get only a one-line description of the command together with some
examples, type (help command).  In the latter case, you can get the
rest of the help by typing more!; or type more if you don't necessarily
want all the rest of the help at once.  (Then keep typing more if you
want to keep getting more of the help for that command.)

An exception is (help all), which prints the documentation topic
proof-checker-commands, to show you all possible proof-checker commands.
So for example, when you see ACL2-PC::USE in that list, you can then
submit (help use) or (help! use) to get documentation for the
proof-checker use command.

But summarizing for other than the case of all:  as with ACL2, you can
type either of the following:

     more, more!
     -- to obtain more (or, all the rest of) the documentation last
        requested by help (or, outside the proof-checker's loop, :doc)

It has been arranged that the use of (help command) will tell you just
about everything you could want to know about command, almost always by
way of examples.  For more details about a command, use help!, more, or
more!.

We use the word "command" to refer to the name itself, e.g.  rewrite.
We use the word "instruction" to refer to an input to the interactive
system, e.g. (rewrite foo) or (help split).  Of course, we allow
commands with no arguments as instructions in many cases, e.g. rewrite.
In such cases, command is treated identically to (command).

ACL2-PC||HELP!    (macro)
proof-checker help facility

Same as help, except that the entire help message is printed without
any need to invoke more! or more.

Invoke help for documentation about the proof-checker help facility.

ACL2-PC||HELP-LONG    (macro)
same as help!

See the documentation for help!.

Help-long has been included in addition to help! for historical
reasons.  (Such a command is included in Pc-Nqthm).

ACL2-PC||HYPS    (macro)
print the hypotheses

     Examples:
     hyps               -- print all (top-level) hypotheses
     (hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4
     (hyps (1 3) t)     -- print hypotheses 1 and 3 and all governors

     General Form:
     (hyps &optional hyps-indices govs-indices)

Print the indicated top-level hypotheses and governors.  (The notion of
"governors" is defined below.)  Here, hyps-indices and govs-indices
should be lists of indices of hypotheses and governors (respectively),
except that the atom t may be used to indicate that one wants all
hypotheses or governors (respectively).

The list of "governors" is defined as follows.  Actually, we define
here the notion of the governors for a pair of the form <term,
address>]; we're interested in the special case where the term is the
conclusion and the address is the current address.  If the address is
nil, then there are no governors, i.e., the list of governors is nil.
If the term is of the form (if x y z) and the address is of the form (2
. rest) or (3 . rest), then the list of governors is the result of
consing x or its negation (respectively) onto the list of governors for
the pair <y, rest> or the pair <z, rest> (respectively).  If the term
is of the form (implies x y) and the address is of the form (2 . rest),
then the list of governors is the result of consing x onto the list of
governors for the pair <y, rest>.  Otherwise, the list of governors for
the pair <term, (n .  rest)> is exactly the list of governors for the
pair <argn, rest> where argn is the nth argument of term.

If all goals have been proved, a message saying so will be printed.
(as there will be no current hypotheses or governors!).

The hyps command never causes an error.  It "succeeds" (in fact its
value is t) if the arguments (when supplied) are appropriate, i.e.
either t or lists of indices of hypotheses or governors, respectively.
Otherwise it "fails" (its value is nil).

ACL2-PC||ILLEGAL    (macro)
illegal instruction

     Example:
     (illegal -3)

     General Form:
     (illegal instruction)

Probably not of interest to most users; always "fails" since it expands
to the fail command.

The illegal command is used mainly in the implementation.  For example,
the instruction 0 is "read" as (illegal 0), since dive expects positive
integers.

ACL2-PC||IN-THEORY    (primitive)
set the current proof-checker theory

     Example:
     (in-theory
        (union-theories (theory 'minimal-theory) '(true-listp binary-append)))

     General Form:
     (in-theory &optional atom-or-theory-expression)

If the argument is not supplied, then this command sets the current
proof-checker theory (see below for explanation) to agree with the
current ACL2 theory.  Otherwise, the argument should be a theory
expression, and in that case the proof-checker theory is set to the
value of that theory expression.

The current proof-checker theory is used in all calls to the ACL2
theorem prover and rewriter from inside the proof-checker.  Thus, the
most recent in-theory instruction in the current state-stack has an
effect in the proof-checker totally analogous to the effect caused by
an in-theory hint or event in ACL2.  All in-theory instructions before
the last are ignored, because they refer to the current theory in the
ACL2 state, not to the existing proof-checker theory.  For example:

        ACL2 !>:trans1 (enable bar)
         (UNION-THEORIES (CURRENT-THEORY :HERE)
                         '(BAR))
        ACL2 !>:trans1 (CURRENT-THEORY :HERE)
         (CURRENT-THEORY-FN :HERE WORLD)
        ACL2 !>

Thus (in-theory (enable bar)) modifies the current theory of the current
ACL2 world.  So for example, suppose that foo is disabled outside the
proof checker and you execute the following instructions, in this order.

        (in-theory (enable foo))
        (in-theory (enable bar))

Then after the second of these, bar will be enabled in the
proof-checker, but foo will be disabled.  The reason is that (in-theory
(enable bar)) instructs the proof-checker to modify the current theory
(from outside the proof-checker, not from inside the proof-checker) by
enabling bar.

Note that in-theory instructions in the proof-checker have no effect
outside the proof-checker's interactive loop.

If the most recent in-theory instruction in the current state of the
proof-checker has no arguments, or if there is no in-theory instruction
in the current state of the proof-checker, then the proof-checker will
use the current ACL2 theory.  This is true even if the user has
interrupted the interactive loop by exiting and changing the global
ACL2 theory.  However, if the most recent in-theory instruction in the
current state of the proof-checker had an argument, then global changes
to the current theory will have no effect on the proof-checker state.

ACL2-PC||INDUCT    (atomic macro)
generate subgoals using induction

     Examples:
     induct, (induct t)
        -- induct according to a heuristically-chosen scheme, creating
           a new subgoal for each base and induction step
     (induct (append (reverse x) y))
        -- as above, but choose an induction scheme based on the term
           (append (reverse x) y) rather than on the current goal

     General Form:
     (induct &optional term)

Induct as in the corresponding :induct hint given to the theorem
prover, creating new subgoals for the base and induction steps.  If
term is t or is not supplied, then use the current goal to determine
the induction scheme; otherwise, use that term.

*Remark:*  As usual, abbreviations are allowed in the term.

*Remark:*  Induct actually calls the prove command with all processes
turned off.  Thus, you must be at top of the goal for an induct
instruction.

ACL2-PC||LEMMAS-USED    (macro)
print the runes (definitions, lemmas, ...) used

This is just an alias for runes.

ACL2-PC||LISP    (meta)
evaluate the given form in Lisp

     Example:
     (lisp (assign xxx 3))

     General Form:
     (lisp form)

Evaluate form.  The lisp command is mainly of interest for side
effects.  See also print, skip, and fail.

The rest of the documentation for lisp is of interest only to those who
use it in macro commands.  If the Lisp evaluation (by trans-eval) of
form returns an error triple (see ERROR-TRIPLES) of the form
(mv erp ((NIL NIL STATE) . (erp-1 val-1 &)) state), then the lisp
command returns the appropriate error triple

     (mv (or erp erp-1)
         val-1
         state) .

Otherwise, the trans-eval of form must return an error triple of the
form (mv erp (cons stobjs-out val) &), and the lisp command returns the
appropriate error triple

     (mv erp
         val
         state).

Note that the output signature of the form has been lost.  The user
must know the signature in order to use the output of the lisp command.
Trans-eval, which is undocumented except by comments in the ACL2 source
code, has replaced, in val, any occurrence of the current state or the
current values of stobjs by simple symbols such as REPLACED-STATE.  The
actual values of these objects may be recovered, in principle, from the
state returned and the user-stobj-alist within that state.  However, in
practice, the stobjs cannot be recovered because the user is denied
access to user-stobj-alist.  The moral is: do not try to write macro
commands that manipulate stobjs.  Should the returned val contain
REPLACED-STATE the value may simply be ignored and state used, since
that is what REPLACED-STATE denotes.

ACL2-PC||MORE    (macro)
proof-checker help facility

Continues documentation of last proof-checker command visited with help.

Invoke help for documentation about the proof-checker help facility.

ACL2-PC||MORE!    (macro)
proof-checker help facility

Continues documentation of last proof-checker command visited with
help, until all documentation on that command is printed out.

Invoke help for documentation about the proof-checker help facility.

ACL2-PC||NEGATE    (macro)
run the given instructions, and "succeed" if and only if they "fail"

Example: (negate prove)

     General form:
     (negate &rest instruction-list)

Run the indicated instructions exactly in the sense of do-all, and
"succeed" if and only if they "fail".

*Remark:*  Negate instructions will never produce hard "failures".

ACL2-PC||NIL    (macro)
used for interpreting control-d

     Example and General form:
     nil

(or, control-d).

The whole point of this command is that in some Lisps (including akcl),
if you type control-d then it seems, on occasion, to get interpreted as
nil.  Without this command, one seems to get into an infinite loop.

ACL2-PC||NOISE    (meta)
run instructions with output

     Example:
     (noise induct prove)

     General Form:
     (noise &rest instruction-list)

Run the instruction-list through the top-level loop with output.

In fact, having output is the default.  Noise is useful inside a
surrounding call of quiet, when one temporarily wants output.  For
example, if one wants to see output for a prove command immediately
following an induct command but before an s command, one may want to
submit an instruction like (quiet induct (noise prove) s).  See also
quiet.

ACL2-PC||NX    (atomic macro)
move forward one argument in the enclosing term

     Example and General Form:
     nx

For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is x, then after executing nx, the current subterm will be (*
(- y) z).

This is the same as up followed by (dive n+1), where n is the position
of the current subterm in its parent term in the conclusion.  Thus in
particular, the nx command fails if one is already at the top of the
conclusion.

See also up, dive, top, and bk.

ACL2-PC||ORELSE    (macro)
run the first instruction; if (and only if) it "fails", run the
second

     Example:
     (orelse top (print "Couldn't move to the top"))

     General form:
     (orelse instr1 instr2)

Run the first instruction.  Then if it "fails", run the second
instruction also; otherwise, stop after the first.

This instruction "succeeds" if and only if either instr1 "succeeds", or
else instr2 "succeeds".  If it "fails", then the failure is soft.

ACL2-PC||P    (macro)
prettyprint the current term

     Example and General Form:
     p

Prettyprint the current term.  The usual user syntax is used, so that
for example one would see (and x y) rather than (if x y 'nil).  (See
also pp.)  Also, abbreviations are inserted where appropriate; see
add-abbreviation.

The "current term" is the entire conclusion unless dive commands have
been given, in which case it may be a subterm of the conclusion.

If all goals have been proved, a message saying so will be printed (as
there will be no current term!).

ACL2-PC||P-TOP    (macro)
prettyprint the conclusion, highlighting the current term

     Example and General Form:
     p-top

For example, if the conclusion is (equal (and x (p y)) (foo z)) and the
current subterm is (p y), then p-top will print (equal (and x (*** (p
y) ***)) (foo z)).

Prettyprint the the conclusion, highlighting the current term.  The
usual user syntax is used, as with the command p (as opposed to pp).
This is illustrated in the example above, where one would *not* see
(equal (if x (*** (p y) ***) 'nil) (foo z)).

*Remark* (obscure): In some situations, a term of the form (if x t y)
occurring inside the current subterm will not print as (or x y), when x
isn't a call of a boolean primitive.  There's nothing incorrect about
this, however.

ACL2-PC||PL    (macro)
print the rules for a given name

     Examples:
     pl
     (pl foo)

     General Form:
     (pl &optional x)

This command simply invokes the corresponding command of the top-level
ACL2 loop; see PL.  If no argument is given, or if the argument
is nil, then the current subterm should be a call of a function symbol,
and the argument is taken to be that symbol.

If you want information about applying rewrite rules to the current
subterm, consider the show-rewrites (or equivalently, sr) command.

ACL2-PC||PP    (macro)
prettyprint the current term

     Example and General Form:
     pp

This is the same as p (see its documentation), except that raw syntax
(internal form) is used.  So for example, one would see (if x y 'nil)
rather than (and x y).  Abbreviations are however still inserted, as
with p.

ACL2-PC||PR    (macro)
print the rules for a given name

     Examples:
     pr
     (pr foo)

     General Form:
     (pr &optional x)

This command simply invokes the corresponding command of the top-level
ACL2 loop; see PR.  If no argument is given, or if the argument
is nil, then the current subterm should be a call of a function symbol,
and the argument is taken to be that symbol.

If you want information about applying rewrite rules to the current
subterm, consider the show-rewrites (or equivalently, sr) command.

ACL2-PC||PRINT    (macro)
print the result of evaluating the given form

     Example:
     (print (append '(a b) '(c d)))
     Print the list (a b c d) to the terminal

     General Forms:
     (print form)
     (print form t)

Prettyprints the result of evaluating form.  The evaluation of form
should return a single value that is not state or a single-threaded
object (see STOBJ).  The optional second argument causes
printing to be done without elision (so-called "evisceration"; see
EVISC-TUPLE).

If the form you want to evaluate does not satisfy the criterion above,
you should create an appropriate call of the lisp command instead.
Notice that this command always returns (mv nil nil state) where the
second result will always be REPLACED-STATE.

ACL2-PC||PRINT-ALL-CONCS    (macro)
print all the conclusions of (as yet unproved) goals

Example and General Form: print-all-concs

Prints all the conclusions of goals that remain to be proved, in a
pleasant format.  See also the proof-checker command print-all-goals.

ACL2-PC||PRINT-ALL-GOALS    (macro)
print all the (as yet unproved) goals

Example and General Form: print-all-goals

Prints all the goals that remain to be proved, in a pleasant format.
See also the proof-checker command print-all-concs.

ACL2-PC||PRINT-MAIN    (macro)
print the original goal

     Example and General Form:
     print-main

Print the goal as originally entered.

ACL2-PC||PRO    (atomic macro)
repeatedly apply promote

     Example and General Form:
     pro

Apply the promote command until there is no change.  This command
"succeeds" exactly when at least one call of promote "succeeds".  In
that case, only a single new proof-checker state will be created.

ACL2-PC||PROMOTE    (primitive)
move antecedents of conclusion's implies term to top-level
hypotheses

     Examples:
     promote
     (promote t)

For example, if the conclusion is (implies (and x y) z), then after
execution of promote, the conclusion will be z and the terms x and y
will be new top-level hypotheses.

     General Form:
     (promote &optional do-not-flatten-flag)

Replace conclusion of (implies hyps exp) or (if hyps exp t) with simply
exp, adding hyps to the list of top-level hypotheses.  Moreover, if
hyps is viewed as a conjunction then each conjunct will be added as a
separate top-level hypothesis.  An exception is that if
do-not-flatten-flag is supplied and not nil, then only one top-level
hypothesis will be added, namely hyps.

*Remark*:  You must be at the top of the conclusion in order to use this
command.  Otherwise, first invoke top.

ACL2-PC||PROTECT    (macro)
run the given instructions, reverting to existing state upon
failure

     Example:
     (protect induct p prove)

     General Form:
     (protect &rest instruction-list)

Protect is the same as do-strict, except that as soon as an instruction
"fails", the state-stack reverts to what it was before the protect
instruction began, and restore is given the same meaning that it had
before the protect instruction began.  See the documentation for
do-strict.

ACL2-PC||PROVE    (primitive)
call the ACL2 theorem prover to prove the current goal

     Examples:
     prove -- attempt to prove the current goal
     (prove :otf-flg t
            :hints (("Subgoal 2" :by foo) ("Subgoal 1" :use bar)))
           -- attempt to prove the current goal, with the indicated hints
              and with OTF-FLG set

     General Form:
     (prove &rest rest-args)

Attempt to prove the current goal, where rest-args is as in the keyword
arguments to defthm except that only :hints and :otf-flg are allowed.
The command succeeds exactly when the corresponding defthm would
succeed, except that it is all right for some goals to be given "bye"s.
Each goal given a "bye" will be turned into a new subgoal.  (See
HINTS for an explanation of :by hints.)

*Remark:*  Use (= t) instead if you are not at the top of the
conclusion.  Also note that if there are any hypotheses in the current
goal, then what is actually attempted is a proof of (implies hyps
conc), where hyps is the conjunction of the top-level hypotheses and
conc is the goal's conclusion.

*Remark:*  It is allowed to use abbreviations in the hints.

ACL2-PC||PSO    (macro)
print the most recent proof attempt from inside the proof-checker

     Example and General Form:
     pso

Print the most recent proof attempt from inside the proof-checker
assuming you are in gag-mode or have saved output (see
SET-SAVED-OUTPUT).  This includes all calls to the prover, including
for example proof-checker commands induct, split, and bash, in addition
to prove.  So for example, you can follow (quiet prove) with pso to see
the proof, including proof-tree output, if it failed.

See also documentation for related proof-checker commands psog and pso!.

ACL2-PC||PSO!    (macro)
print the most recent proof attempt from inside the proof-checker

     Example and General Form:
     pso!

Print the most recent proof attempt from inside the proof-checker,
including proof-tree output, assuming you are in gag-mode or have saved
output (see SET-SAVED-OUTPUT).  This includes all calls to the
prover, including for example proof-checker commands induct, split, and
bash, in addition to prove.  So for example, you can follow (quiet
prove) with pso! to see the proof, including proof-tree output, if it
failed.

See also documentation for related proof-checker commands pso and psog.

ACL2-PC||PSOG    (macro)
print the most recent proof attempt from inside the proof-checker

     Example and General Form:
     psog

Print the most recent proof attempt from inside the proof-checker,
including goal names, assuming you are in gag-mode or have saved output
(see SET-SAVED-OUTPUT).  This includes all calls to the prover,
including for example proof-checker commands induct, split, and bash,
in addition to prove.  So for example, you can follow (quiet prove)
with psog to see the proof, including proof-tree output, if it failed.

See also documentation for related proof-checker commands pso and pso!.

ACL2-PC||PUT    (macro)
substitute for a "free variable"

     Example:
     (put x 17)

     General Form:
     (put var expr)

Substitute expr for the "free variable" var, as explained below.

A "free variable" is, for our purposes, a variable var such that the
instruction (free var) has been executed earlier in the state-stack.
What (free var) really does is to let var be an abbreviation for the
term (hide var) (see documentation for add-abbreviation).  What (put
var expr) really does is to unwind the state-stack, replacing that free
instruction with the instruction (add-abbreviation var expr), so that
future references to (? var) become reference to expr rather than to
(hide var), and then to replay all the other instructions that were
unwound.  Because hide was used, the expectation is that in most cases,
the instructions will replay successfully and put will "succeed".
However, if any replayed instruction "fails", then the entire replay
will abort and "fail", and the state-stack will revert to its value
before the put instruction was executed.

If (put var expr) "succeeds", then (remove-abbreviation var) will be
executed at the end.

*Remark*:  The restore command will revert the state-stack to its value
present before the put instruction was executed.

ACL2-PC||QUIET    (meta)
run instructions without output

     Example:
     (quiet induct prove)

     General Form:
     (quiet &rest instruction-list)

Run the instruction-list through the top-level loop with no output.

See also noise.

ACL2-PC||R    (macro)
same as rewrite

     Example:
     (r 3)

See the documentation for rewrite, as r and rewrite are identical.

ACL2-PC||REDUCE    (atomic macro)
call the ACL2 theorem prover's simplifier

     Examples:
     reduce -- attempt to prove the current goal without using induction
     (reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
            -- attempt to prove the current goal without using
               induction, with the indicated hints

     General Form:
     (reduce &rest hints)

Attempt to prove the current goal without using induction, using the
indicated hints (if any).  A subgoal will be created for each goal that
would have been pushed for proof by induction in an ordinary proof.

Notice that unlike prove, the arguments to reduce are spread out, and
are all hints.

Reduce is similar to bash in that neither of these allows induction.
But bash only allows simplification, while reduce allows processes
eliminate-destructors, fertilize, generalize, and eliminate-irrelevance.

*Remark:*  Induction will be used to the extent that it is ordered
explicitly in the hints.

ACL2-PC||REDUCE-BY-INDUCTION    (macro)
call the ACL2 prover without induction, after going into
induction

     Examples:
     reduce-by-induction
       -- attempt to prove the current goal after going into induction,
          with no further inductions

     (reduce-by-induction ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
       -- attempt to prove the current goal after going into induction,
          with no further inductions, using the indicated hints

     General Form:
     (reduce-by-induction &rest hints)

A subgoal will be created for each goal that would have been pushed for
proof by induction in an ordinary proof, except that the proof begins
with a top-level induction.

Notice that unlike prove, the arguments to reduce-by-induction are
spread out, and are all hints.  See also prove, reduce, and bash.

*Remark*:  Induction and the various processes will be used to the
extent that they are ordered explicitly in the :induct and :do-not
hints.

ACL2-PC||REMOVE-ABBREVIATIONS    (primitive)
remove one or more abbreviations

     Examples:
     remove-abbreviations -- remove all abbreviations
     (remove-abbreviations v w)
                          -- assuming that V and W currently abbreviate
                             terms, then they are ``removed'' in the
                             sense that they are no longer considered to
                             abbreviate those terms

     General Forms:
     (remove-abbreviations &rest vars)

If vars is not empty (i.e., not nil), remove the variables in vars from
the current list of abbreviations, in the sense that each variable in
vars will no longer abbreviate a term.

*Remark:*  The instruction fails if at least one of the arguments fails
to be a variable that abbreviates a term.

See also the documentation for add-abbreviation, which contains a
discussion of abbreviations in general, and show-abbreviations.

ACL2-PC||REPEAT    (macro)
repeat the given instruction until it "fails"

     Example:
     (repeat promote)

     General Form:
     (repeat instruction)

The given instruction is run repeatedly until it "fails".

*Remark:*  There is nothing here in general to prevent the instruction
from being run after all goals have been proved, though this is indeed
the case for primitive instructions.

ACL2-PC||REPEAT-REC    (macro)
auxiliary to repeat

See documentation for repeat.

ACL2-PC||REPLAY    (macro)
replay one or more instructions

     Examples:
     REPLAY     -- replay all instructions in the current session
                   (i.e., state-stack)
     (REPLAY 5) -- replay the most recent 5 instructions
     (REPLAY 5
             (COMMENT deleted dive command here))
                -- replace the 5th most recent instruction with the
                   indicated comment instruction, and then replay it
                   followed by the remaining 4 instructions

     General Form:
     (REPLAY &OPTIONAL n replacement-instruction)

Replay the last n instructions if n is a positive integer; else n
should be nil or not supplied, and replay all instructions.  However,
if replacement-instruction is supplied and not nil, then before the
replay, replace the nth instruction (from the most recent, as shown by
commands) with replacement-instruction.

If this command "fails", then the restore command will revert the
state-stack to its value present before the replay instruction was
executed.

ACL2-PC||RESTORE    (meta)
remove the effect of an UNDO command

     Example and General Form:
     restore

Restore removes the effect of an undo command.  This always works as
expected if restore is invoked immediately after undo, without
intervening instructions.  However, other commands may also interact
with restore, notably "sequencing" commands such as do-all, do-strict,
protect, and more generally, sequence.

*Remark:*  Another way to control the saving of proof-checker state is
with the save command; see the documentation for save.

The restore command always "succeeds"; it returns (mv nil t state).

ACL2-PC||RETAIN    (atomic macro)
drop all *but* the indicated top-level hypotheses

     Example:
     (RETAIN 2 3) -- keep the second and third hypotheses, and drop
                     the rest

     General Form:
     (retain &rest args)

Drop all top-level hypotheses *except* those with the indicated indices.

There must be at least one argument, and all must be in range (i.e.
integers between one and the number of top-level hypotheses, inclusive).

ACL2-PC||RETRIEVE    (macro)
re-enter the proof-checker

     Examples:
     (retrieve associativity-of-permutationp)
     retrieve

     General Form:
     (retrieve &optional name)

Must be used from outside the interactive proof-checker loop.  If name
is supplied and not nil, this causes re-entry to the interactive
proof-checker loop in the state at which save was last executed for the
indicated name.  (See documentation for save.)  If name is nil or is
not supplied, then the user is queried regarding which proof-checker
state to re-enter.  The query is omitted, however, if there only one
proof-checker state is present that was saved with save, in which case
that is the one that is used.  See also unsave.

ACL2-PC||REWRITE    (primitive)
apply a rewrite rule

     Examples:
     (rewrite reverse-reverse)
        -- apply the rewrite rule `reverse-reverse'
     (rewrite (:rewrite reverse-reverse))
        -- same as above
     (rewrite 2)
        -- apply the second rewrite rule, as displayed by show-rewrites
     rewrite
        -- apply the first rewrite rule, as displayed by show-rewrites
     (rewrite transitivity-of-< ((y 7)))
        -- apply the rewrite rule transitivity-of-< with the substitution
           that associates 7 to the ``free variable'' y
     (rewrite foo ((x 2) (y 3)) t)
        -- apply the rewrite rule foo by substituting 2 and 3 for free
           variables x and y, respectively, and also binding all other
           free variables possible by using the current context
           (hypotheses and governors)

     General Form:
     (rewrite &optional rule-id substitution instantiate-free)

Replace the current subterm with a new term by applying a rewrite or
definition rule.  The replacement will be done according to the
information provided by the show-rewrites (sr) command.

See also the linear command, for an analogous command to use with
linear rules.

If rule-id is a positive integer n, then the nth rule as displayed by
show-rewrites is the one that is applied.  If rule-id is nil or is not
supplied, then it is treated as the number 1.  Otherwise, rule-id
should be either a symbol or else a :rewrite or :definition rune.  If a
symbol is supplied, then any (:rewrite or :definition) rule of that
name may be used.  We say more about this, and describe the other
optional arguments, below.

Consider first the following example.  Suppose that the current subterm
is (reverse (reverse y)) and that there is a rewrite rule called
reverse-reverse of the form

     (implies (true-listp x)
              (equal (reverse (reverse x)) x)) .

Then the instruction (rewrite reverse-reverse) causes the current
subterm to be replaced by y and creates a new goal with conclusion
(true-listp y).  An exception is that if the top-level hypotheses imply
(true-listp y) using only "trivial reasoning" (more on this below),
then no new goal is created.

If the rule-id argument is a number or is not supplied, then the system
will store an instruction of the form (rewrite name ...), where name is
the name of a rewrite rule; this is in order to make it easier to replay
instructions when there have been changes to the history.  Except:
instead of the name (whether the name is supplied or calculated), the
system stores the rune if there is any chance of ambiguity.  (Formally,
"ambiguity" here means that the rune being applied is of the form
(:rewrite name . index), where index is not nil.)

Speaking in general, then, a rewrite instruction works as follows:

First, a rewrite or definition rule is selected according to the
arguments of the rewrite instruction.  The selection is made as
explained under "General Form" above.

Next, the left-hand side of the rule is matched with the current
subterm, i.e., a substitution unify-subst is found such that if one
instantiates the left-hand side of the rule with unify-subst, then one
obtains the current subterm.  If this match fails, then the instruction
fails.

Next, an attempt is made to relieve (discharge) the hypotheses, much as
the theorem prover relieves hypotheses except that there is no call to
the rewriter.  First, the substitution unify-subst is extended with the
substitution argument, which may bind free variables (see
FREE-VARIABLES).  Each hypothesis of the rule is then considered in
turn, from first to last.  For each hypothesis, first the current
substitution is applied, and then the system checks whether the
hypothesis is "clearly" true in the current context.  If there are
variables in the hypotheses of the rule that are not bound by the
current substitution, then a weak attempt is made to extend that
substitution so that the hypothesis is present in the current context
(see the documentation for the proof-checker hyps command under
proof-checker-commands), much as would be done by the theorem prover's
rewriter.

If in the process above there are free variables (see
FREE-VARIABLES), but the proof-checker can see how to bind them to
relieve all hypotheses, then it will do so in both the show-rewrites
(sr) and rewrite commands.  But normally, if even one hypothesis
remains unrelieved, then no automatic extension of the substitution is
made.  Except, if instantiate-free is not nil, then that extension to
the substitution is kept.

Finally, the instruction is applied as follows.  The current subterm is
replaced by applying the final substitution described above to the
right-hand side of the selected rule.  And, one new subgoal is created
for each unrelieved hypothesis of the rule, whose top-level hypotheses
are the governors and top-level hypotheses of the current goal and
whose conclusion and current subterm are the instance, by that same
final substitution, of that unrelieved hypothesis.

*Remark:*  The substitution argument should be a list whose elements
have the form (variable term), where term may contain abbreviations.

ACL2-PC||RUN-INSTR-ON-GOAL    (macro)
auxiliary to THEN

See documentation for then.

ACL2-PC||RUN-INSTR-ON-NEW-GOALS    (macro)
auxiliary to then

See documentation for then.

ACL2-PC||RUNES    (macro)
print the runes (definitions, lemmas, ...) used

     Examples and general forms:
     (runes t)   ; print all runes used during this interactive proof
     (runes nil) ; print all runes used by the most recent command
     (runes)     ; same as (runes nil)
     runes       ; same as (runes nil)

This command does not change the proof-checker state.  Rather, it
simply reports runes (see RUNE) that have participated in the
interactive proof.

Note that (runes nil) will show the runes used by the most recent
primitive or macro command (as displayed by :comm).

ACL2-PC||S    (primitive)
simplify the current subterm

     Examples:
     S  -- simplify the current subterm
     (S :backchain-limit 2 :normalize t :expand (append x z))
        -- simplify the current subterm, but during the rewriting
           process first ``normalize'' it by pushing IFs to the
           top-level, and also force the term (append x z) to be
           expanded during the rewriting process

     General Form:
     (s &key rewrite normalize backchain-limit repeat in-theory hands-off
             expand)

Simplify the current subterm according to the keyword parameters
supplied.  First if-normalization is applied (unless the normalize
argument is nil), i.e., each subterm of the form (f ... (if test x y)
...)  is replaced by the term (if test (f ... x ...) (f ... y ...))
except, of course, when f is if and the indicated if subterm is in the
second or third argument position.  Then rewriting is applied (unless
the rewrite argument is nil).  Finally this pair of actions is repeated
-- until the rewriting step causes no change in the term.  A
description of each parameter follows.

     :rewrite -- default t

When non-nil, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.

     :normalize -- default t

When non-nil, instructs the system to use if-normalization (as
described above) during simplification.

     :backchain-limit -- default 0

Sets the number of recursive calls to the rewriter that are allowed for
backchaining.  Even with the default of 0, some reasoning is allowed
(technically speaking, type-set reasoning is allowed) in the relieving
of hypotheses.  The value should be nil or a non-negative integer, and
limits backchaining only for rewriting, not for type-set reasoning.

     :repeat -- default 0

Sets the number of times the current term is to be rewritten.  If this
value is t, then the default is used (as specified by the constant
*default-s-repeat-limit*).

     :in-theory, :hands-off, :expand

These have their usual meaning; see HINTS.

*Remark:*  if conditional rewrite rules are used that cause case splits
because of the use of force, then appropriate new subgoals will be
created, i.e., with the same current subterm (and address) but with
each new (forced) hypothesis being negated and then used to create a
corresponding new subgoal.  In that case, the current goal will have
all such new hypotheses added to the list of top-level hypotheses.

ACL2-PC||S-PROP    (atomic macro)
simplify propositionally

     Example:
     s-prop

     General Form:
     (s-prop &rest names)

Simplify, using the default settings for s (which include
if-normalization and rewriting without real backchaining), but with
respect to a theory in which only basic functions and rules (the ones in
(theory 'minimal-theory)), together with the names (or parenthesized
names) in the &rest argument names, are enabled.

See also the documentation for s.

ACL2-PC||SAVE    (macro)
save the proof-checker state (state-stack)

     Example:
     (save lemma3-attempt)

     General Form:
     (save &optional name do-it-flg)

Saves the current proof-checker state by "associating" it with the
given name.  Submit (retrieve name) to Lisp to get back to this
proof-checker state.  If verify was originally supplied with an event
name, then the argument can be omitted in favor of that name as the
default.

*Remark* that if a save has already been done with the indicated name
(or the default event name), then the user will be queried regarding
whether to go ahead with the save -- except, if do-it-flg is supplied
and not nil, then there will be no query and the save will be effected.

See also the documentation for retrieve and unsave.

ACL2-PC||SEQUENCE    (meta)
run the given list of instructions according to a multitude of
options

     Example:
     (sequence (induct p prove) t)

See also the definitions of commands do-all, do-strict, protect, and
succeed.

     General Form:
     (sequence
      instruction-list
      &optional
      strict-flg protect-flg success-expr no-prompt-flg no-restore-flg)

Each instruction in the list instruction-list is run, and the
instruction "succeeds" if every instruction in instruction-list
"succeeds".  However, it might "succeed" even if some instructions in
the list "fail"; more generally, the various arguments control a number
of aspects of the running of the instructions.  All this is explained
in the paragraphs below.  First we embark on a general discussion of
the instruction interpreter, including the notions of "succeed" and
"fail".

*Remark:*  The arguments are *not* evaluated, except (in a sense) for
success-expr, as described below.

Each primitive and meta instruction can be thought of as returning an
error triple, say (erp val state); see ERROR-TRIPLES.  An
instruction (primitive or meta) "succeeds" if erp is nil and val is not
nil; otherwise it "fails".  (When we use the words "succeed" or "fail"
in this technical sense, we'll always include them in double quotes.)
If an instruction "fails," we say that that the failure is "soft" if
erp is nil; otherwise the failure is "hard".  The sequence command
gives the user control over how to treat "success" and "failure" when
sequencing instructions, though we have created a number of handy macro
commands for this purpose, notably do-all, do-strict and protect.

Here is precisely what happens when a sequence instruction is run.  The
instruction interpreter is run on the instructions supplied in the
argument instruction-list (in order).  The interpreter halts the first
time there is a hard "failure." except that if strict-flg is supplied
and not nil, then the interpreter halts the first time there is any
"failure."  The error triple (erp val state) returned by the sequence
instruction is the triple returned by the last instruction executed
(or, the triple (nil t state) if instruction-list is nil), except for
the following provision.  If success-expr is supplied and not nil, then
it is evaluated with the state global variables pc-erp and pc-val (in
the "ACL2" package) bound to the corresponding components of the error
triple returned (as described above).  At least two values should be
returned, and the first two of these will be substituted for erp and
val in the triple finally returned by sequence.  For example, if
success-expr is (mv erp val), then no change will be made to the error
triple, and if instead it is (mv nil t), then the sequence instruction
will "succeed".

That concludes the description of the error triple returned by a
sequence instruction, but it remains to explain the effects of the
arguments protect-flg and no-prompt-flg.

If protect-flg is supplied and not nil and if also the instruction
"fails" (i.e., the error component of the triple is not nil or the
value component is nil), then the state is reverted so that the
proof-checker's state (including the behavior of restore) is set back
to what it was before the sequence instruction was executed.
Otherwise, unless no-restore-flg is set, the state is changed so that
the restore command will now undo the effect of this sequence
instruction (even if there were nested calls to sequence).

Finally, as each instruction in instruction-list is executed, the
prompt and that instruction will be printed, unless the global state
variable pc-print-prompt-and-instr-flg is unbound or nil and the
parameter no-prompt-flg is supplied and not nil.

ACL2-PC||SHOW-ABBREVIATIONS    (macro)
display the current abbreviations

     Examples:
     (show-abbreviations v w)
        -- assuming that v and w currently abbreviate terms,
           then this instruction displays them together with
           the terms they abbreviate
     show-abbreviations
        -- display all abbreviations

See also add-abbreviation and remove-abbreviations.  In particular, the
documentation for add-abbreviation contains a general discussion of
abbreviations.

     General Form:
     (show-abbreviations &rest vars)

Display each argument in vars together with the term it abbreviates (if
any).  If there are no arguments, i.e. the instruction is simply
show-abbreviations, then display all abbreviations together with the
terms they abbreviate.

If the term abbreviated by a variable, say v, contains a proper subterm
that is also abbreviate by (another) variable, then both the
unabbreviated term and the abbreviated term (but not using (? v) to
abbreviate the term) are displayed with together with v.

ACL2-PC||SHOW-LINEARS    (macro)
display the applicable linear rules

     Example:
     show-linears

     General Form:
     (show-linears &optional rule-id enabled-only-flg)

This command displays linear rules with a trigger term that matches the
current subterm, and shows how they can be applied.  This command is
analogous to the show-rewrites proof-checker command; see its
documentation for details.  Also see the documentation for
proof-checker command apply-linear for how to apply linear rules.

ACL2-PC||SHOW-REWRITES    (macro)
display the applicable rewrite rules

     Example:
     show-rewrites

     General Form:
     (show-rewrites &optional rule-id enabled-only-flg)

This command displays rewrite rules whose left-hand side matches the
current subterm, and shows how that command can be applied.  For each
rule displayed, hypotheses are shown that would need to be proved after
the rule is applied.  Note that hypotheses are omitted from the display
when the system can trivially verify that they hold; to see all
hypotheses for each rule in a display that is independent of the
arguments of the current subterm, use the pl or pr command.

Here are details on the arguments and the output.  If rule-id is
supplied and is a name (non-nil symbol) or a :rewrite or :definition
rune, then only the corresponding rewrite rule(s) will be displayed,
while if rule-id is a positive integer n, then only the nth rule that
would be in the list is displayed.  In each case, the display will
point out when a rule is currently disabled (in the interactive
environment), except that if enabled-only-flg is supplied and not nil,
then disabled rules will not be displayed at all.  Finally, among the
free variables of any rule (see FREE-VARIABLES), those that
would remain free if the rule were applied will be displayed.  Also see
REWRITE.

ACL2-PC||SHOW-TYPE-PRESCRIPTIONS    (macro)
display the applicable type-prescription rules

     Example:
     show-type-prescriptions

     General Form:
     (show-type-prescriptions &optional rule-id)

Display type-prescription rules that apply to the current subterm.  If
rule-id is supplied and is a name (non-nil symbol) or a :rewrite or
:definition rune, then only the corresponding rewrite rule(s) will be
displayed.  In each case, the display will point out when a rule is
currently disabled (in the interactive environment).  Also see
TYPE-PRESCRIPTION.

ACL2-PC||SKIP    (macro)
"succeed" without doing anything

     Example and General Form:
     skip

Make no change in the state-stack, but "succeed".  Same as (sequence
nil).

ACL2-PC||SL    (atomic macro)
simplify with lemmas

     Examples:
     sl
     (sl 3)

     General Form:
     (sl &optional backchain-limit)

Simplify, but with all function definitions disabled (see
FUNCTION-THEORY in the top-level ACL2 loop), except for a few basic
functions (the ones in (theory 'minimal-theory)).  The backchain-limit
has a default of 0, but if is supplied and not nil, then it should be a
nonnegative integer; see the documentation for s.

WARNING: This command completely ignores in-theory commands that are
executed inside the proof-checker.

ACL2-PC||SLS    (macro)
same as SHOW-LINEARS

     Example:
     srs

     General Form:
     (srs &optional rule-id enabled-only-flg)

See the documentation for show-linears, as sls and show-linears are
identical.  NOTE: In analogy to the sr abbreviation for show-rewrites,
one might expect this command to be sl; but that name was taken
("simplify with lemmas") before sls was implemented.

ACL2-PC||SPLIT    (atomic macro)
split the current goal into cases

     Example:
     split

For example, if the current goal has one hypothesis (or x y) and a
conclusion of (and a b), then split will create four new goals:

     one with hypothesis X and conclusion A
     one with hypothesis X and conclusion B
     one with hypothesis Y and conclusion A
     one with hypothesis Y and conclusion B.

     General Form:
     SPLIT

Replace the current goal by subgoals whose conjunction is equivalent
(primarily by propositional reasoning) to the original goal, where each
such goal cannot be similarly split.

*Remark:*  The new goals will all have their hypotheses promoted; in
particular, no conclusion will have a top function symbol of implies.
Also note that split will fail if there is exactly one new goal created
and it is the same as the existing current goal.

The way split really works is to call the ACL2 theorem prover with only
simplification (and preprocessing) turned on, and with only a few
built-in functions (especially, propositional ones) enabled, namely,
the ones in the list (theory 'minimal-theory).  However, because the
prover is called, type-set reasoning can be used to eliminate some
cases.  For example, if (true-listp x) is in the hypotheses, then
probably (true-listp (cdr x)) will be reduced to t.

ACL2-PC||SR    (macro)
same as SHOW-REWRITES

     Example:
     sr

     General Form:
     (sr &optional rule-id enabled-only-flg)

See the documentation for show-rewrites, as sr and show-rewrites are
identical.

ACL2-PC||ST    (macro)
same as SHOW-TYPE-PRESCRIPTIONS

     Example:
     sr

     General Form:
     (st &optional rule-id)

See the documentation for show-type-prescriptions, as st and
show-type-prescriptions are identical.

ACL2-PC||SUCCEED    (macro)
run the given instructions, and "succeed"

     Example:
     (succeed induct p prove)

     General Form:
     (succeed &rest instruction-list)

Run the indicated instructions until there is a hard "failure", and
"succeed".  (See the documentation for sequence for an explanation of
"success" and "failure".)

ACL2-PC||TH    (macro)
print the top-level hypotheses and the current subterm

     Examples:
     th               -- print all (top-level) hypotheses and the current
                         subterm
     (th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
                         and the current subterm
     (th (1 3) t)     -- print hypotheses 1 and 3 and all governors, and
                         the current subterm

     General Form:
     (th &optional hyps-indices govs-indices)

Print hypotheses and the current subterm.  The printing of hypotheses
(and perhaps governors) are controlled as in the hyps command; see its
documentation.

Historical note:  The name th is adapted from the Gypsy Verification
Environment, where th abbreviates the command theorem, which says to
print information on the current goal.

ACL2-PC||THEN    (macro)
apply one instruction to current goal and another to new subgoals

     Example:
     (then induct prove)

     General Form:
     (then first-instruction &optional completion must-succeed-flg)

Run first-instruction, and then run completion (another instruction) on
each subgoal created by first-instruction.  If must-succeed-flg is
supplied and not nil, then halt at the first "failure" and remove the
effects of the invocation of completion that "failed".

The default for completion is reduce.

ACL2-PC||TOP    (atomic macro)
move to the top of the goal

     Example and General Form:
     top

For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is y, then after executing top, the current subterm will be the
same as the conclusion, i.e., (= x (* (- y) z)).

Top is the same as (up n), where n is the number of times one needs to
execute up in order to get to the top of the conclusion.  The top
command fails if one is already at the top of the conclusion.

See also up, dive, nx, and bk.

ACL2-PC||TYPE-ALIST    (macro)
display the type-alist from the current context

     Examples:
     (type-alist t t)     ; display type-alist based on conclusion and governors
     (type-alist t t t)   ; as above, but also display forward-chaining report
     type-alist           ; same as (type-alist nil t) -- governors only
     (type-alist nil)     ; same as (type-alist nil t) -- governors only
     (type-alist t)       ; same as (type-alist t nil) -- conclusion only
     (type-alist nil nil) ; display type-alist without considering
                          ; conclusion or governors

     General Form:
     (type-alist &optional concl-flg govs-flg fc-report-flg)

where if govs-flg is omitted then it defaults to (not concl-flg), and
concl-flg and fc-report-flg default to nil.

Display the current assumptions as a type-alist.  Note that this display
includes the result of forward chaining.  When fc-report-flg is supplied
a non-nil value, the display also includes a forward-chaining report;
otherwise,the presence or absence of such a report is controlled by the
usual global settings (see FORWARD-CHAINING-REPORTS).

There are two basic reasons contemplated for using this command.

1. The theorem prover has failed (either outside the proof-checker or
using a proof-checker command such as bash or reduce and you want to
debug by getting an idea of what the prover knows about the context.

     a. You really are interested in the context for the current term.
     Include hypotheses and governors (i.e., accounting for tests of
     surrounding if-expressions that must be true or false) but not the
     current conclusion (which the theorem prover's heuristics would
     generally ignore for contextual information).  Command:
     (type-alist nil t) ; equivalently, type-alist or (type-alist nil)

     b. You are not thinking in particular about the current term; you
     just want to get an idea of the context that the prover would
     build at the top-level, for forward-chaining.  Incorporate the
     conclusion but not the governors.  Command:
     (type-alist t nil) ; equivalently, (type-alist t)

2. You intend to use one of the proof-checker-commands that does
simplification, such as s or x, and you want to see the context.  Then
include the surrounding if-term governors but not the goal's
conclusion.  Command:
(type-alist nil t) ; equivalently, type-alist or (type-alist nil)

See TYPE-SET (also see TYPE-PRESCRIPTION) for
information about ACL2's type system, which can assist in understanding
the output of the type-alist command.

ACL2-PC||UNDO    (meta)
undo some instructions

     Examples:
     (undo 7)
     undo

     General Forms:

     (undo n) -- Undo the last n instructions.  The argument n should be
                 a positive integer.

     undo     -- Same as (undo 1).

*Remark:*  To remove the effect of an undo command, use restore.  See
the documentation for details.

*Remark:*  If the argument n is greater than the total number of
interactive instructions in the current session, then (undo n) will
simply take you back to the start of the session.

The undo meta command always "succeeds"; it returns (mv nil t state)
unless its optional argument is supplied and of the wrong type (i.e.
not a positive integer) or there are no instructions to undo.

ACL2-PC||UNSAVE    (macro)
remove a proof-checker state

     Example:
     (unsave assoc-of-append)

     General Form:
     (unsave &optional name)

Eliminates the association of a proof-checker state with name, if name
is supplied and not nil.  The name may be nil or not supplied, in which
case it defaults to the event name supplied with the original call to
verify (if there is one -- otherwise, the instruction "fails" and there
is no change).  The ACL2 function unsave may also be executed outside
the interactive loop, with the same syntax.

See also documentation for save and retrieve.

ACL2-PC||UP    (primitive)
move to the parent (or some ancestor) of the current subterm

     Examples:  if the conclusion is (= x (* (- y) z)) and the
                current subterm is y, then we have:
     up or (up 1) -- the current subterm becomes (- y)
     (up 2)       -- the current subterm becomes (* (- y) z)
     (up 3)       -- the current subterm becomes the entire conclusion
     (up 4)       -- no change; can't go up that many levels

     General Form:
     (up &optional n)

Move up n levels in the conclusion from the current subterm, where n is
a positive integer.  If n is not supplied or is nil, then move up 1
level, i.e., treat the instruction as (up 1).

See also dive, top, nx, and bk.

ACL2-PC||USE    (atomic macro)
use a lemma instance

     Example:
     (USE true-listp-append
          (:instance assoc-of-append (x a) (y b) (z c)))
     -- Add two top-level hypotheses, one the lemma called
        true-listp-append, and the other an instance of the lemma called
        assoc-of-append by the substitution in which x is assigned a, y
        is assigned b, and z is assigned c.

     General Form:
     (use &rest args)

Add the given lemma instances to the list of top-level hypotheses.  See
HINTS for the syntax of :use hints in defthm, which is
essentially the same as the syntax here (see the example above).

This command calls the prove command, and hence should only be used at
the top of the conclusion.