This is documentation for ACL2 Version 4.3
Copyright (C) 2011  University of Texas at Austin

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

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

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

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

FMT1    :(str alist col co-channel state evisc) => (mv col state)

See FMT for further explanation, including documentation of the
tilde-directives.

FMT1!    :(str alist col channel state evisc) => (mv col state)

This function is nearly identical to fmt1; see FMT1.  The only
difference is that fmt1 may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fmt1! instead if you want to be able to read
the forms back in.

FMT1!-TO-STRING    See PRINTING-TO-STRINGS.

FMT1-TO-STRING    See PRINTING-TO-STRINGS.

FOURTH    fourth member of the list

See any Common Lisp documentation for details.

GET-OUTPUT-STREAM-STRING$    See IO.

GETENV$    read an environment variable

(Getenv$ str state), where str is a string, reads the value of
environment variable str, returning nil if none is found or if the read
fails.  The formal story is that getenv$ reads its value from the
oracle field of the ACL2 state.  The return value is thus a triple of
the form (mv erp val state), where erp will always be nil in practice,
val is the value that has been read, and state is the new state, which
is obtained by popping val from the top of the state's oracle.

     Example:
     (getenv$ "PWD" state) ==> (mv nil "/u/joe/work" state)

Also see SETENV$.

GETPROP    access fast property lists

     General form:
     (getprop symb key default world-name world-alist)

See books/misc/getprop.lisp for an example that illustrates the use of
ACL2 utilities getprop and putprop to take advantage of under-the-hood
Lisp (hashed) property lists.

GOOD-ATOM-LISTP    recognizer for a true list of "good" atoms

The predicate good-atom-listp tests whether its argument is a
true-listp of "good" atoms, i.e., where each element is a number, a
symbol, a character, or a string.

Also see ATOM-LISTP.

HARD-ERROR    print an error message and stop execution

(Hard-error ctx str alist) causes evaluation to halt with a short
message using the "context" ctx.  An error message is first printed
using the string str and alist alist that are of the same kind as
expected by fmt.  See FMT.  Also see ER for a macro
that provides a unified way of signaling errors.

Hard-error has a guard of t.  Also see ILLEGAL for a similar
capability which however has a guard of nil that supports static
checking using guard verification, rather than using dynamic (run-time)
checking.   This distinction is illustrated elsewhere: see
PROG2$ for examples.

Semantically, hard-error ignores its arguments and always returns nil.
But if a call (hard-error ctx str alist) is encountered during
evaluation, then the string str is printed using the association list
alist (as in fmt), after which evaluation halts immediately.  Here is a
trivial, contrived example.

     ACL2 !>(cons 3 (hard-error 'my-context
                                 "Printing 4: ~n0"
                                 (list (cons #\0 4))))

     HARD ACL2 ERROR in MY-CONTEXT:  Printing 4: four

     ACL2 Error in TOP-LEVEL:  Evaluation aborted.

     ACL2 !>

IDENTITY    the identity function

(Identity x) equals x; what else can we say?

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

IF    if-then-else function

(if x y z) is equal to y if x is any value other than nil, and is equal
to z if x is nil.

Only one of y, z is evaluated when (if x y z) is evaluated.

If has a guard of t.

If is part of Common Lisp.  See any Common Lisp documentation for more
information.

IFF    logical "if and only if"

Iff is the ACL2 biconditional, "if and only if".  (iff P Q) means that
either P and Q are both false (i.e., nil) or both true (i.e., not nil).

IFIX    coerce to an integer

Ifix simply returns any integer argument unchanged, returning 0 on a
non-integer argument.  Also see NFIX, see RFIX, see
REALFIX and see FIX for analogous functions that coerce
to a natural number, a rational number, a real, and a number,
respectively.

Ifix has a guard of t.

IGNORABLE    See DECLARE.

IGNORE    See DECLARE.

ILLEGAL    print an error message and stop execution

(Illegal ctx str alist) causes evaluation to halt with a short message
using the "context" ctx.  An error message is first printed using the
string str and alist alist that are of the same kind as expected by
fmt.  See FMT, and see PROG2$ for an example of how to
use a related function, hard-error (see HARD-ERROR).  Also see
ER for a macro that provides a unified way of signaling errors.

The difference between illegal and hard-error is that the former has a
guard of nil while the latter has a guard of t.  Thus, you may want to
use illegal rather than hard-error when you intend to do guard
verification at some point, and you expect the guard to guarantee that
the illegal call is never executed.  See PROG2$ for an example.

IMAGPART    imaginary part of a complex number

Completion Axiom (completion-of-imagpart):

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

Guard for (imagpart x):

     (acl2-numberp x)

IMPLIES    logical implication

Implies is the ACL2 implication function.  (implies P Q) means that
either P is false (i.e., nil) or Q is true (i.e., not nil).

IMPROPER-CONSP    recognizer for improper (non-null-terminated) non-empty lists

Improper-consp is the function that checks whether its argument is a
non-empty list that ends in other than nil.  See PROPER-CONSP
and also see TRUE-LISTP.

INT=    test equality of two integers

(int= x y) is logically equivalent to (equal x y).

Unlike equal, int= requires its arguments to be numbers (or else causes
a guard violation; see GUARD).  Generally, int= is executed
more efficiently than equal or = on integers.

INTEGER-LENGTH    number of bits in two's complement integer representation

For non-negative integers, (integer-length i) is the minimum number of
bits needed to represent the integer.  Any integer can be represented
as a signed two's complement field with a minimum of (+ (integer-length
i) 1) bits.

The guard for integer-length requires its argument to be an integer.
Integer-length is defined in Common Lisp.  See any Common Lisp
documentation for more information.

INTEGER-LISTP    recognizer for a true list of integers

The predicate integer-listp tests whether its argument is a true list
of integers.

INTEGERP    recognizer for whole numbers

(integerp x) is true if and only if x is an integer.

INTERN    create a new symbol in a given package

(intern symbol-name symbol-package-name) returns a symbol with the
given symbol-name and the given symbol-package-name.  We restrict
Common Lisp's intern so that the second argument is either the symbol
*main-lisp-package-name*, the value of that constant, or is one of
"ACL2", "ACL2-INPUT-CHANNEL", "ACL2-OUTPUT-CHANNEL", or "KEYWORD".  To
avoid that restriction, see INTERN$.

In ACL2 intern is actually implemented as a macro that expands to a
call of a similar function whose second argument is a symbol.  Invoke
:pe intern to see the definition, or see
INTERN-IN-PACKAGE-OF-SYMBOL.

To see why is intern so restricted consider (intern "X" "P").  In
particular, is it a symbol and if so, what is its symbol-package-name?
One is tempted to say "yes, it is a symbol in the package "P"."  But if
package "P" has not yet been defined, that would be premature because
the imports to the package are unknown.  For example, if "P" were
introduced with

     (defpkg "P" '(LISP::X))

then in Common Lisp (symbol-package-name (intern "X" "P")) returns
"LISP".

The obvious restriction on intern is that its second argument be the
name of a package known to ACL2.  We cannot express such a restriction
(except, for example, by limiting it to those packages known at some
fixed time, as we do).  Instead, we provide intern-in-package-of-symbol
which requires a "witness symbol" for the package instead of the
package.  The witness symbol is any symbol (expressible in ACL2) and
uniquely specifies a package necessarily known to ACL2.

INTERN$    create a new symbol in a given package

Intern$ is a macro that behaves the same as the macro intern, except
for weakening the restriction to a fixed set of package names so that
any package name other than "" is legal.  See INTERN.  Note
that if you evaluate a call (intern$ x y) for which there is no package
with name y that is known to ACL2, you will get an error.

(Intern$ x y) expands to:

     (intern-in-package-of-symbol x (pkg-witness y))

See INTERN-IN-PACKAGE-OF-SYMBOL and see PKG-WITNESS.

INTERN-IN-PACKAGE-OF-SYMBOL    create a symbol with a given name

Completion Axiom (completion-of-intern-in-package-of-symbol):

     (equal (intern-in-package-of-symbol x y)
            (if (and (stringp x)
                     (symbolp y))
                (intern-in-package-of-symbol x y)
              nil))

Guard for (intern-in-package-of-symbol x y):

     (and (stringp x) (symbolp y))

Intuitively, (intern-in-package-of-symbol x y) creates a symbol with
symbol-name x interned in the package containing y.  More precisely,
suppose x is a string, y is a symbol with symbol-package-name pkg and
that the defpkg event creating pkg had the list of symbols imports as
the value of its second argument.  Then (intern-in-package-of-symbol x
y) returns a symbol, ans, the symbol-name of ans is x, and the
symbol-package-name of ans is pkg, unless x is the symbol-name of some
member of imports with symbol-package-name ipkg, in which case the
symbol-package-name of ans is ipkg.  Because defpkg requires that there
be no duplications among the symbol-names of the imports,
intern-in-package-of-symbol is uniquely defined.

For example, suppose "MY-PKG" was created by

     (defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).

Let w be 'my-pkg::witness.  Observe that

     (symbolp w) is t                     ; w is a symbol
     (symbol-name w) is "WITNESS"         ; w's name is "WITNESS"
     (symbol-package-name w) is "MY-PKG"  ; w is in the package "MY-PKG"

The construction of w illustrates one way to obtain a symbol in a given
package:  write it down as a constant using the double-colon notation.

But another way to obtain a symbol in a given package is to create it
with intern-in-package-of-symbol.

     (intern-in-package-of-symbol "XYZ" w) is MY-PKG::XYZ

     (intern-in-package-of-symbol "ABC" w) is ACL2::ABC

     (intern-in-package-of-symbol "CAR" w) is LISP::CAR

     (intern-in-package-of-symbol "car" w) is MY-PKG::|car|

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

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

(Intersection$ x y) equals a list that contains the members of x that
are also members of y.  More precisely, the resulting list is the
result of deleting from x those members that that are not members of y.
The optional keyword, :TEST, has no effect logically, but provides the
test (default eql) used for comparing members of the two lists.

Intersection$ need not take exactly two arguments, though it must take
at least one argument: (intersection$ x) is x,  (intersection$ x y z
... :test test) is (intersection$ x (intersection$ y z ... :test test)
:test test), and if :TEST is not supplied, then (intersection$ x y z
...)  is (intersection$ x (intersection$ y z ...)).  For the discussion
below we restrict ourselves, then, to the cases (intersection$ x y) and
(intersection$ x y :test test).

The guard for a call of intersection$ (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
intersection$ and its variants:

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

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

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

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

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

INTERSECTION-EQ    See INTERSECTION$.

INTERSECTION-EQUAL    See INTERSECTION$.

INTERSECTP    test whether two lists intersect

     General Forms:
     (set-difference$ l1 l2)
     (set-difference$ l1 l2 :test 'eql)   ; same as above (eql as equality test)
     (set-difference$ l1 l2 :test 'eq)    ; same, but eq is equality test
     (set-difference$ l1 l2 :test 'equal) ; same, but equal is equality test

(Intersectp l1 l2) returns t if l1 and l2 have a member in common, else
it returns nil.  The optional keyword, :TEST, has no effect logically,
but provides the test (default eql) used for comparing members of the
two lists.

The guard for a call of intersectp 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
intersectp and its variants:

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

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

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

INTERSECTP-EQ    See INTERSECTP.

INTERSECTP-EQUAL    See INTERSECTP.

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.

KEYWORD-VALUE-LISTP    recognizer for true lists whose even-position elements are keywords

(keyword-value-listp l) is true if and only if l is a list of even
length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword.

KEYWORDP    recognizer for keywords

(Keywordp x) is true if and only if x is a keyword, i.e., a symbol in
the "KEYWORD" package.  Such symbols are typically printed using a colon
(:) followed by the symbol-name of the symbol.

Keywordp has a guard of t.

Keywordp is a Common Lisp function.  See any Common Lisp documentation
for more information.  The following log may be illuminating.

     ACL2 !>(intern "ABC" "KEYWORD")
     :ABC
     ACL2 !>(symbol-name ':ABC)
     "ABC"
     ACL2 !>(symbol-package-name ':ABC)
     "KEYWORD"
     ACL2 !>

KWOTE    quote an arbitrary object

For any object x, (kwote x) returns the two-element list whose elements
are the symbol quote and the given x, respectively.  The guard of
(kwote x) is t.

KWOTE-LST    quote an arbitrary true list of objects

The function kwote-lst applies the function kwote to each element of a
given list.  The guard of (kwote-lst lst) is (true-listp lst).

LAST    the last cons (not element) of a list

(Last l) is the last cons of a list.  Here are examples.

     ACL2 !>(last '(a b . c))
     (B . C)
     ACL2 !>(last '(a b c))
     (C)

(Last l) has a guard of (listp l); thus, l need not be a true-listp.

Last is a Common Lisp function.  See any Common Lisp documentation for
more information.  Unlike Common Lisp, we do not allow an optional
second argument for last.

LEN    length of a list

Len returns the length of a list.

A Common Lisp function that is appropriate for both strings and proper
lists is length; see LENGTH.  The guard for len is t.

(Low-level implementation note.  ACL2 provides a highly-optimized
implementation of len, which is tail-recursive and fixnum-aware, that
differs from its simple ACL2 definition.)

LENGTH    length of a string or proper list

Length is the function for determining the length of a sequence.  In
ACL2, the argument is required to be either a true-listp or a string.

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

LET    binding of lexically scoped (local) variables

     Example LET Form:
     (let ((x (* x x))
           (y (* 2 x)))
      (list x y))

If the form above is executed in an environment in which x has the
value -2, then the result is '(4 -4).

Let expressions bind variables so that their "local" values, the values
they have when the "body" of the let is evaluated, are possibly
different than their "global" values, the values they have in the
context in which the let expression appears.  In the let expression
above, the local variables bound by the let are x and y.  They are
locally bound to the values delivered by the two forms (* x x) and (* 2
x), respectively, that appear in the "bindings" of the let.  The body
of the let is (list x y).

Suppose that the let expression above occurs in a context in which x
has the value -2.  (The global value of y is irrelevant to this
example.)  For example, one might imagine that the let form above
occurs as the body of some function, fn, with the formal parameter x
and we are evaluating (fn -2).

To evaluate the let above in a context in which x is -2, we first
evaluate the two forms specifying the local values of the variables.
Thus, (* x x) is evaluated and produces 4 (because x is -2) and (* 2 x)
is evaluated and produces -4 (because x is -2).  Then x and y are bound
to these values and the body of the let is evaluated.  Thus, when the
body, (list x y) is evaluated, x is 4 and y is -4.  Thus, the body
produces '(4 -4).

Note that the binding of y, which is written after the binding of x and
which mentions x, nevertheless uses the global value of x, not the new
local value.  That is, the local variables of the let are bound "in
parallel" rather than "sequentially." In contrast, if the

     Example LET* Form:
     (let* ((x (* x x))
            (y (* 2 x)))
      (list x y))

is evaluated when the global value of x is -2, then the result is '(4
8), because the local value of y is computed after x has been bound to
4.  Let* binds its local variables "sequentially."

     General LET Forms:
     (let ((var1 term1) ... (varn termn)) body)
     and
     (let ((var1 term1) ... (varn termn))
      (declare ...) ... (declare ...)
      body)

where the vari are distinct variables, the termi are terms involving
only variables bound in the environment containing the let, and body is
a term involving only the vari plus the variables bound in the
environment containing the let.  Each vari must be used in body or else
declared ignored.

A let form is evaluated by first evaluating each of the termi,
obtaining for each a vali.  Then, each vari is bound to the
corresponding vali and body is evaluated.

Actually, let forms are just abbreviations for certain uses of lambda
notation.  In particular

     (let ((var1 term1) ... (varn termn)) (declare ...) body)

is equivalent to

     ((lambda (var1 ... varn)
        (declare ...)
        body)
      term1 ... termn).

Let* forms are used when it is desired to bind the vari sequentially,
i.e., when the local values of preceding varj are to be used in the
computation of the local value for vari.

     General LET* Forms:
     (let* ((var1 term1) ... (varn termn)) body)
     and
     (let* ((var1 term1) ... (varn termn))
      (declare (ignore x1 ... xm))
      body)

where the vari are variables (not necessarily distinct), the termi are
terms involving only variables bound in the environment containing the
let* and those varj such that j<i, and body is a term involving only
the vari plus the variables bound in the environment containing the
let*.  Each vari must be used either in some subsequent termj or in
body, except that in the second form above we make an exception when
vari is among the xk, in which case vari must not be thus used.  Note
that let* does not permit the inclusion of any declare forms other than
one as shown above.  In the second general form above, every xk must be
among the vari, and furthermore, xk may not equal vari and varj for
distinct i, j.

The first let* above is equivalent to

     (let ((var1 term1))
      ...
      (let ((varn termn)) body)...)

Thus, the termi are evaluated successively and after each evaluation
the corresponding vali is bound to the value of termi.  The second let*
is similarly expanded, except that each for each vari that is among the
(x1 ... xm), the form (declare (ignore vari)) is inserted immediately
after (vari termi).

Each (vari termi) pair in a let or let* form is called a "binding" of
vari and the vari are called the "local variables" of the let or let*.
The common use of let and let* is to save the values of certain
expressions (the termi) so that they may be referenced several times in
the body without suggesting their recomputation.

Let is part of Common Lisp.  See any Common Lisp documentation for more
information.

LET*    binding of lexically scoped (local) variables

     Example LET* Forms:
     (let* ((x (* x x))
            (y (* 2 x)))
      (list x y))

     (let* ((x (* x x))
            (y (* 2 x))
            (x (* x y))
            (a (* x x)))
      (declare (ignore a))
      (list x y))

If the forms above are executed in an environment in which x has the
value -2, then the respective results are '(4 8) and '(32 8).  See
LET for a discussion of both let and let*, or read on for a
briefer discussion.

The difference between let and let* is that the former binds its local
variables in parallel while the latter binds them sequentially.  Thus,
in let*, the term evaluated to produce the local value of one of the
locally bound variables is permitted to reference any locally bound
variable occurring earlier in the binding list and the value so
obtained is the newly computed local value of that variable.  See
LET.

In ACL2 the only declare forms allowed for a let* form are ignore,
ignorable, and type.  See DECLARE.  Moreover, no variable
declared ignored or ignorable may be bound more than once.  A variable
with a type declaration may be bound more than once, in which case the
type declaration is treated by ACL2 as applying to each binding
occurrence of that variable.  It seems unclear from the Common Lisp spec
whether the underlying Lisp implementation is expected to apply such a
declaration to more than one binding occurrence, however, so
performance in such cases may depend on the underlying Lisp.

Let* is a Common Lisp macro.  See any Common Lisp documentation for
more information.

LEXORDER    total order on ACL2 objects

Lexorder is a non-strict total order, a "less than or equal," on ACL2
objects.  Also see ALPHORDER, the restriction of lexorder to
atoms; the notion of "non-strict total order" is defined there.

Lexorder has a guard of t.

For lexorder, an atom and a cons are ordered so that the atom comes
first, and two conses are ordered so that the one with the recursively
smaller car comes first, with the cdrs being compared only if the cars
are equal.   Lexorder compares two atoms by using alphorder.

LIST    build a list

List is the macro for building a list of objects.  For example, (list 5
6 7) returns a list of length 3 whose elements are 5, 6, and 7
respectively.  Also see LIST*.

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

LIST*    build a list

List* is the Common Lisp macro for building a list of objects from
given elements and a tail.  For example, (list* 5 6 '(7 8 9)) equals
the list '(5 6 7 8 9).  Also see LIST.

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

LISTP    recognizer for (not necessarily proper) lists

(listp x) is true when x is either a cons pair or is nil.

Listp has no guard, i.e., its guard is t.

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

LOGAND    bitwise logical `and' of zero or more integers

When integers are viewed in their two's complement representation,
logand returns their bitwise logical `and'.  In ACL2 logand is a macro
that expands into calls of the binary function binary-logand, except
that (logand) expands to -1 and (logand x) expands to x.

The guard for binary-logand requires its arguments to be integers.
Logand is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOGANDC1    bitwise logical `and' of two ints, complementing the first

When integers are viewed in their two's complement representation,
logandc1 returns the bitwise logical `and' of the second with the
bitwise logical `not' of the first.

The guard for logandc1 requires its arguments to be integers.  Logandc1
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGANDC2    bitwise logical `and' of two ints, complementing the second

When integers are viewed in their two's complement representation,
logandc2 returns the bitwise logical `and' of the first with the
bitwise logical `not' of the second.

The guard for logandc2 requires its arguments to be integers.  Logandc2
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGBITP    the ith bit of an integer

For a nonnegative integer i and an integer j, (logbitp i j) is the
value of the ith bit in the two's complement representation of j.

(Logbitp i j) has a guard that i is a nonnegative integer and j is an
integer.

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

LOGCOUNT    number of "on" bits in a two's complement number

(Logcount x) is the number of "on" bits in the two's complement
representation of x.

(Logcount x) has a guard of (integerp x).

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

LOGEQV    bitwise logical equivalence of zero or more integers

When integers are viewed in their two's complement representation,
logeqv returns their bitwise logical equivalence.  In ACL2 logeqv is a
macro that expands into calls of the binary function binary-logeqv,
except that (logeqv) expands to -1 and (logeqv x) expands to x.

The guard for binary-logeqv requires its arguments to be integers.
Logeqv is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOGIOR    bitwise logical inclusive or of zero or more integers

When integers are viewed in their two's complement representation,
logior returns their bitwise logical inclusive or.  In ACL2 logior is a
macro that expands into calls of the binary function binary-logior,
except that (logior) expands to 0 and (logior x) expands to x.

The guard for binary-logior requires its arguments to be integers.
Logior is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOGNAND    bitwise logical `nand' of two integers

When integers are viewed in their two's complement representation,
lognand returns their bitwise logical `nand'.

The guard for lognand requires its arguments to be integers.  Lognand
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGNOR    bitwise logical `nor' of two integers

When integers are viewed in their two's complement representation,
lognor returns the bitwise logical `nor' of the first with the second.

The guard for lognor requires its arguments to be integers.  Lognor is
defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGNOT    bitwise not of a two's complement number

(lognot i) is the two's complement bitwise `not' of the integer i.

Lognot is actually defined by coercing its argument to an integer (see
IFIX), negating the result, and then subtracting 1.

The guard for lognot requires its argument to be an integer.

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

LOGORC1    bitwise logical inclusive or of two ints, complementing the first

When integers are viewed in their two's complement representation,
logorc1 returns the bitwise logical inclusive or of the second with the
bitwise logical `not' of the first.

The guard for logorc1 requires its arguments to be integers.  Logorc1
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGORC2    bitwise logical inclusive or of two ints, complementing the second

When integers are viewed in their two's complement representation,
logorc2 returns the bitwise logical inclusive or of the first with the
bitwise logical `not' of the second.

The guard for logorc2 requires its arguments to be integers.  Logorc2
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGTEST    test if two integers share a `1' bit

When integers x and y are viewed in their two's complement
representation, (logtest x y) is true if and only if there is some
position for which both x and y have a `1' bit in that position.

The guard for logtest requires its arguments to be integers.  Logtest
is defined in Common Lisp.  See any Common Lisp documentation for more
information.

LOGXOR    bitwise logical exclusive or of zero or more integers

When integers are viewed in their two's complement representation,
logxor returns their bitwise logical exclusive or.  In ACL2 logxor is a
macro that expands into calls of the binary function binary-logxor,
except that (logxor) expands to 0 and (logxor x) expands to x.

The guard for binary-logxor requires its arguments to be integers.
Logxor is defined in Common Lisp.  See any Common Lisp documentation
for more information.

LOWER-CASE-P    recognizer for lower case characters

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

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

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

MAKE-CHARACTER-LIST    coerce to a list of characters

Non-characters in the given list are coerced to the character with code
0.

MAKE-LIST    make a list of a given size

For a nonnegative integer size, (Make-list size) is a list of elements
of length size, each of which is initialized to the :initial-element
(which defaults to nil).

Make-list is a macro in ACL2, defined in terms of a tail recursive
function make-list-ac whose guard requires size to be a nonnegative
integer.  Make-list is a Common Lisp function.  See any Common Lisp
documentation for more information.

MAKE-ORD    a constructor for ordinals.

Make-ord is the ordinal constructor.  Its use is recommended instead of
using cons to make ordinals.  For a discussion of ordinals, see
ORDINALS.

For any ordinal, alpha < epsilon-0, there exist natural numbers p and
n, positive integers x1, x2, ..., xn and ordinals a1 > a2 > ... > an >
0 such that alpha > a1 and alpha = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn
+ p.  We call a1 the "first exponent", x1 the "first coefficient", and
the remainder (w^(a2)x2 + ... + w^(an)xn + p) the "rest" of alpha.

(Make-ord fe fco rst) corresponds to the ordinal (w^fe)fco + rst.  Thus
the first infinite ordinal, w (omega), is constructed by

     (make-ord 1 1 0)

and, for example, the ordinal (w^2)5 + w2 + 7 is constructed by:

     (make-ord 2 5 (make-ord 1 2 7)) .

The reason make-ord is used rather than cons is that it allows us to
reason more abstractly about the ordinals, without having to worry
about the underlying representation.

MAX    the larger of two numbers

(Max x y) is the larger of the numbers x and y.

The guard for max requires its arguments to be rational (real, in
ACL2(r)) numbers.

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

MBE    attach code for execution

The macro mbe ("must be equal") can be used in function definitions in
order to cause evaluation to use alternate code to that provided for the
logic.  An example is given below.  However, the use of mbe can lead to
non-terminating computations.  See DEFEXEC, perhaps after
reading the present documentation, for a way to guarantee termination
(at least theoretically).

In the ACL2 logic, (mbe :exec exec-code :logic logic-code) equals
logic-code; the value of exec-code is ignored.  However, in raw Lisp it
is the other way around:  this form macroexpands simply to exec-code.
ACL2's guard verification mechanism ensures that the raw Lisp code is
only evaluated when appropriate, since the guard proof obligations
generated for this call of mbe are (equal exec-code logic-code)
together with the guard proof obligations from exec-code.  See
VERIFY-GUARDS and, for general discussion of guards, see
GUARD.

Warning for nested mbe calls: The equality of :exec and :logic code is
not checked in the scope of superior :logic code, as for the equality
of x and y in the following.

     (mbe :logic
          (mbe :logic x :exec y)
          :exec
          z)

The form (mbe :exec exec-code :logic logic-code) macroexpands in ACL2 to
a form that generates the guard proof obligation (equal logic-code
exec-code).  The c[:exec and the :logic code in an mbe call must have
the same return type; for example, one cannot return (mv * *) while the
other returns just a single value.

Also see MBT, which stands for "must be true."  You may find it
more natural to use mbt for certain applications, as described in its
documentation.

Related topics other than immediate subtopics:

Here is an example of the use of mbe.  Suppose that you want to define
factorial in the usual recursive manner, as follows.

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

But perhaps you want to be able to execute calls of fact on large
arguments that cause stack overflows, perhaps during proofs.  (This
isn't a particularly realistic example, but it should serve.)  So,
instead you can define this tail-recursive version of factorial:

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

We are now ready to define fact using mbe.  Our intention is that
logically, fact is as shown in the first definition above, but that
fact should be executed by calling fact1.  Notice that we defer guard
verification, since we are not ready to prove the correspondence
between fact1 and fact.

     (defun fact (n)
       (declare (xargs :guard (and (integerp n) (>= n 0))
                       :verify-guards nil))
       (mbe :exec  (fact1 n 1)
            :logic (if (zp n)
                       1
                     (* n (fact (1- n))))))

Next, we prove the necessary correspondence lemmas.  Notice the
inclusion of a standard book to help with the arithmetic reasoning.

     (include-book "books/arithmetic/top-with-meta")

     (defthm fact1-fact
       (implies (integerp acc)
                (equal (fact1 n acc)
                       (* acc (fact n)))))

We may now do guard verification for fact, which will allow the
execution of the raw Lisp fact function, where the above mbe call
expands simply to (fact1 n 1).

     (verify-guards fact)

Now that guards have been verified, a trace of function calls
illustrates that the evaluation of calls of fact is passed to
evaluation of calls of fact1.  The outermost call below is of the
logical function stored for the definition of fact; all the others are
of actual raw Common Lisp functions.

     ACL2 !>(trace$ fact fact1)
     NIL
     ACL2 !>(fact 3)
     1> (ACL2_*1*_ACL2::FACT 3)
       2> (FACT 3)
         3> (FACT1 3 1)
           4> (FACT1 2 3)
             5> (FACT1 1 6)
               6> (FACT1 0 6)
               <6 (FACT1 6)
             <5 (FACT1 6)
           <4 (FACT1 6)
         <3 (FACT1 6)
       <2 (FACT 6)
     <1 (ACL2_*1*_ACL2::FACT 6)
     6
     ACL2 !>

You may occasionally get warnings when you compile functions defined
using mbe.  (For commands that invoke the compiler, see
COMPILATION.)  These can be inhibited by using an ignorable declare
form.  Here is a simple but illustrative example.  Note that the
declarations can optionally be separated into two declare forms.

     (defun foo (x y)
       (declare (ignorable x)
                (xargs :guard (equal x y)))
       (mbe :logic x :exec y))

Finally, we observe that when the body of a function contains a term of
the form (mbe :exec exec-code :logic logic-code), the user is very
unlikely to see any logical difference than if this were replaced by
logic-code.  ACL2 takes various steps to ensure this.  For example, the
proof obligations generated for admitting a function treat the above
mbe term simply as logic-code.  Function expansion, :use hints,
:definition rules, generation of constraints for functional
instantiation, and creation of rules of class :rewrite and
:forward-chaining also treat mbe calls as their :logic code.

MBE1    attach code for execution

The form (mbe1 exec logic) is equivalent to the forms (mbe :logic logic
:exec exec) and (must-be-equal logic exec).  See MBE.

MBT    introduce a test not to be evaluated

The macro mbt ("must be true") can be used in order to add code in
order to admit function definitions in :logic mode, without paying a
cost in execution efficiency.  Examples below illustrate its intended
use.

Semantically, (mbt x) equals x.  However, in raw Lisp (mbt x) ignores x
entirely, and macroexpands to t.  ACL2's guard verification mechanism
ensures that the raw Lisp code is only evaluated when appropriate,
since a guard proof obligation (equal x t) is generated.  See
VERIFY-GUARDS and, for general discussion of guards, see
GUARD.

Also see MBE, which stands for "must be equal."  Although mbt
is more natural in many cases, mbe has more general applicability.  In
fact, (mbt x) is essentially defined to be (mbe :logic x :exec t).

We can illustrate the use of mbt on the following generic example, where
<g>, <test>, <rec-x>, and <base> are intended to be terms involving
only the variable x.

     (defun foo (x)
       (declare (xargs :guard <g>))
       (if <test>
           (foo <rec-x>)
         <base>))

In order to admit this function, ACL2 needs to discharge the proof
obligation that <rec-x> is smaller than x, namely:

     (implies <test>
              (o< (acl2-count <rec-x>)
                   (acl2-count x)))

But suppose we need to know that <g> is true in order to prove this.
Since <g> is only the guard, it is not part of the logical definition
of foo.  A solution is to add the guard to the definition of foo, as
follows.

     (defun foo (x)
       (declare (xargs :guard <g>))
       (if (mbt <g>)
           (if <test>
               (foo <rec-x>)
             <base>)
         nil))

If we do this using <g> rather than (mbt <g>), then evaluation of every
recursive call of foo will cause the evaluation of (the appropriate
instance of) <g>.  But since (mbt <g>) expands to t in raw Lisp, then
once we verify the guards of foo, the evaluations of <g> will be
avoided (except at the top level, when we check the guard before
allowing evaluation to take place in Common Lisp).

Other times, the guard isn't the issue, but rather, the problem is that
a recursive call has an argument that itself is a recursive call.  For
example, suppose that <rec-x> is of the form (foo <expr>).  There is no
way we can hope to discharge the termination proof obligation shown
above.  A standard solution is to add some version of this test:

     (mbt (o< (acl2-count <rec-x>) (acl2-count x)))

Here is a specific example based on one sent by Vernon Austel.

     (defun recurX2 (n)
       (declare (xargs :guard (and (integerp n) (<= 0 n))
                       :verify-guards nil))
       (cond ((zp n) 0)
             (t (let ((call (recurX2 (1- n))))
                  (if (mbt (< (acl2-count call) n))
                      (recurX2 call)
                    1 ;; this branch is never actually taken
                    )))))

     (defthm recurX2-0
      (equal (recurX2 n) 0))

     (verify-guards recurX2)

If you (trace$ acl2-count), you will see that evaluation of (recurX2 2)
causes several calls of acl2-count before the verify-guards.  But this
evaluation does not call acl2-count after the verify-guards, because
the ACL2 evaluation mechanism uses raw Lisp to do the evaluation, and
the form (mbt (< (acl2-count call) n)) macroexpands to t in Common Lisp.

You may occasionally get warnings when you compile functions defined
using mbt.  (For commands that invoke the compiler, see
COMPILATION.)  These can be inhibited by using an ignorable declare
form.  Here is a simple but illustrative example.  Note that the
declarations can optionally be separated into two declare forms.

     (defun foo (x y)
       (declare (ignorable x)
                (xargs :guard (equal x t)))
       (and (mbt x) y))

MEMBER    membership predicate

     General Forms:
     (member x lst)
     (member x lst :test 'eql)   ; same as above (eql as equality test)
     (member x lst :test 'eq)    ; same, but eq is equality test
     (member x lst :test 'equal) ; same, but equal is equality test

(Member x lst) equals the longest tail of the list lst that begins with
x, or else nil if no such tail exists.  The optional keyword, :TEST,
has no effect logically, but provides the test (default eql) used for
comparing x with successive elements of lst.

The guard for a call of member depends on the test.  In all cases, the
second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

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

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

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

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

Member is defined by Common Lisp.  See any Common Lisp documentation for
more information.

MEMBER-EQ    See MEMBER.

MEMBER-EQUAL    See MEMBER.

MIN    the smaller of two numbers

(Min x y) is the smaller of the numbers x and y.

The guard for min requires its arguments to be rational (real, in
ACL2(r)) numbers.

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

MINUSP    test whether a number is negative

(Minusp x) is true if and only if x < 0.

The guard of minusp requires its argument to be a rational (real, in
ACL2(r)) number.

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

MOD    remainder using floor

     ACL2 !>(mod 14 3)
     2
     ACL2 !>(mod -14 3)
     1
     ACL2 !>(mod 14 -3)
     -1
     ACL2 !>(mod -14 -3)
     -2
     ACL2 !>(mod -15 -3)
     0
     ACL2 !>

(Mod i j) is that number k that (* j (floor i j)) added to k equals i.

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

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

MOD-EXPT    exponential function

(mod-expt r i m) is the result of raising the number r to the integer
power i and then taking the residue mod m.  That is, (mod-expt r i m)
is equal to (mod (expt r i) m).

The guard for (mod-expt r i m) is that r is a rational number and i is
an integer; if r is 0 then i is nonnegative; and m is a non-zero
rational number.

In some implementations (GCL Version 2.7.0 as of this writing), this
function is highly optimized when r and i are natural numbers, not both
zero, and m is a positive integer.  For other Lisp implementations,
consider using function mod-expt-fast, defined in the book
arithmetic-3/floor-mod/mod-expt-fast.lisp, which should still provide
significantly improved performance over this function.

MUST-BE-EQUAL    attach code for execution

The form (must-be-equal logic exec) evaluates to logic in the ACL2
logic but evaluates to exec in raw Lisp.  The point is to be able to
write one definition to reason about logically but another for
evaluation.  Please see MBE and see MBT for appropriate
macros to use, rather than calling must-be-equal directly, since it is
easy to commute the arguments of must-be-equal by accident.

In essence, the guard for (must-be-equal x y) is (equal x y).  However,
note that must-be-equal is a macro: (must-be-equal logic exec) expands
to (mbe1 exec logic), which expands to a call of return-last.

MV    returning a multiple value

Mv is the mechanism provided by ACL2 for returning two or more values.
Logically, (mv x1 x2 ... xn) is the same as (list x1 x2 ... xn), a list
of the indicated values.  However, ACL2 avoids the cost of building
this list structure, with the cost that mv may only be used in a
certain style in definitions:  if a function ever returns using mv
(either directly, or by calling another function that returns a
multiple value), then this function must always return the same number
of values.

For more explanation of the multiple value mechanism, see
MV-LET.

ACL2 does not support the Common Lisp construct values, whose logical
meaning seems difficult to characterize.  Mv is the ACL2 analogue of
that construct.

MV-LET    calling multi-valued ACL2 functions

     Example Form:
     (mv-let (x y z)              ; local variables
             (mv 1 2 3)           ; multi-valued expression
             (declare (ignore y)) ; optional declarations
             (cons x z))          ; body

The form above binds the three "local variables," x, y, and z, to the
three results returned by the multi-valued expression and then
evaluates the body.  The result is '(1 . 3).  The second local, y, is
declared ignored.  The multi-valued expression can be any ACL2
expression that returns k results, where k is the number of local
variables listed.  Often however it is simply the application of a
k-valued function.  Mv-let is the standard way to invoke a multi-valued
function when the caller must manipulate the vector of results returned.

     General Form:
     (mv-let (var1 ... vark)
             term
             body)
     or
     (mv-let (var1 ... vark)
             term
             (declare ...) ... (declare ...)
             body)

where the vari are distinct variables, term is a term that returns k
results and mentions only variables bound in the environment containing
the mv-let expression, and body is a term mentioning only the vari and
variables bound in the environment containing the mv-let.  Each vari
must occur in body unless it is declared ignored or ignorable in one of
the optional declare forms, unless this requirement is turned off; see
SET-IGNORE-OK.  The value of the mv-let term is the result of
evaluating body in an environment in which the vari are bound, in
order, to the k results obtained by evaluating term in the environment
containing the mv-let.

Here is an extended example that illustrates both the definition of a
multi-valued function and the use of mv-let to call it.  Consider a
simple binary tree whose interior nodes are conses and whose leaves are
non-conses.  Suppose we often need to know the number, n, of interior
nodes of such a tree; the list, syms, of symbols that occur as leaves;
and the list, ints, of integers that occur as leaves.  (Observe that
there may be leaves that are neither symbols nor integers.)  Using a
multi-valued function we can collect all three results in one pass.

Here is the first of two definitions of the desired function.  This
definition is "primitive recursive" in that it has only one argument
and that argument is reduced in size on every recursion.

     (defun count-and-collect (x)

     ; We return three results, (mv n syms ints) as described above.

       (cond ((atom x)

     ; X is a leaf.  Thus, there are 0 interior nodes, and depending on
     ; whether x is a symbol, an integer, or something else, we return
     ; the list containing x in as the appropriate result.

              (cond ((symbolp x) (mv 0 (list x) nil))
                    ((integerp x)(mv 0 nil      (list x)))
                    (t           (mv 0 nil      nil))))
             (t

     ; X is an interior node.  First we process the car, binding n1, syms1, and
     ; ints1 to the answers.

                (mv-let (n1 syms1 ints1)
                        (count-and-collect (car x))

     ; Next we process the cdr, binding n2, syms2, and ints2.

                        (mv-let (n2 syms2 ints2)
                                (count-and-collect (car x))

     ; Finally, we compute the answer for x from those obtained for its car
     ; and cdr, remembering to increment the node count by one for x itself.

                                (mv (1+ (+ n1 n2))
                                    (append syms1 syms2)
                                    (append ints1 ints2)))))))

This use of a multiple value to "do several things at once" is very
common in ACL2.  However, the function above is inefficient because it
appends syms1 to syms2 and ints1 to ints2, copying the list structures
of syms1 and ints1 in the process.  By adding "accumulators" to the
function, we can make the code more efficient.

     (defun count-and-collect1 (x n syms ints)
       (cond ((atom x)
              (cond ((symbolp x) (mv n (cons x syms) ints))
                    ((integerp x) (mv n syms (cons x ints)))
                    (t (mv n syms ints))))
             (t (mv-let (n2 syms2 ints2)
                        (count-and-collect1 (cdr x) (1+ n) syms ints)
                        (count-and-collect1 (car x) n2 syms2 ints2)))))

We claim that (count-and-collect x) returns the same triple of results
as (count-and-collect1 x 0 nil nil).  The reader is urged to study this
claim until convinced that it is true and that the latter method of
computing the results is more efficient.  One might try proving the
theorem

     (defthm count-and-collect-theorem
       (equal (count-and-collect1 x 0 nil nil) (count-and-collect x))).

Hint:  the inductive proof requires attacking a more general theorem.

ACL2 does not support the Common Lisp construct multiple-value-bind,
whose logical meaning seems difficult to characterize.  Mv-let is the
ACL2 analogue of that construct.

MV-LIST    converting multiple-valued result to a single-valued list

     Example Forms:
     ; Returns the list (3 4):
     (mv-list 2 (mv 3 4))

     ; Returns a list containing the three values returned by var-fn-count:
     (mv-list 3 (var-fn-count '(cons (binary-+ x y) z) nil))

     General form:
     (mv-list n term)

Logically, (mv-list n term) is just term; that is, in the logic mv-list
simply returns its second argument.  However, the evaluation of a call
of mv-list on explicit values always results in a single value, which
is a (null-terminated) list.  For evaluation, the term n above (the
first argument to an mv-list call) must "essentially" (see below) be an
integer not less than 2, where that integer is the number of values
returned by the evaluation of term (the second argument to that mv-list
call).

We say "essentially" above because it suffices that the translation of
n to a term (see TRANS) be of the form (quote k), where k is an
integer greater than 1.  So for example, if term above returns three
values, then n can be the expression 3, or (quote 3), or even (mac 3)
if mac is a macro defined by (defmacro mac (x) x).  But n cannot be (+
1 2), because even though that expression evaluates to 3, nevertheless
it translates to (binary-+ '1 '2), not to (quote 3).

Mv-list is the ACL2 analogue of the Common Lisp construct
multiple-value-list.

MV-NTH    the mv-nth element (zero-based) of a list

(Mv-nth n l) is the nth element of l, zero-based.  If n is greater than
or equal to the length of l, then mv-nth returns nil.

(Mv-nth n l) has a guard that n is a non-negative integer.

Mv-nth is equivalent to the Common Lisp function nth (although without
the guard condition that the list is a true-listp), but is used by ACL2
to access the nth value returned by a multiply valued expression.  For
an example of the use of mv-nth, try

     ACL2 !>:trans1 (mv-let (erp val state)
                            (read-object ch state)
                            (value (list erp val)))

MV?    returning a single value

Mv? is designed to work with mv?-let, generalizing how mv works with
mv-let by allowing the binding of a single variable.  For example, the
following form is legal.

     (mv?-let (y)
              (mv? (f x))
              (declare (type integer y))
              (g x y z))

The expression above is equivalent to the following expression, because
(mv? form) expands to form for any expression, form.

     (let ((y (f x)))
       (declare (type integer y))
       (g x y z))

Logically, (mv? x) is the same as x, while (mv? v1 v2 ...) is the same
as (list v1 v2 ...).  Also see MV and see MV?-LET.

MV?-LET    calling possibly multi-valued ACL2 functions

Mv?-let is a macro that extends the macro mv-let by allowing a single
variable to be bound.  Thus, the syntax is the same as that of mv-let
except that mv?-let is permitted to bind a single variable to a form
that produces a single value.  The macros mv?-let and mv?  are provided
to facilitate the writing of macros that traffic in expressions that
could return one or more (multiple) values.

For example, the form

     (mv?-let (y)
              (f x)
              (declare (type integer y))
              (g x y z))

is equivalent to the following form.

     (let ((y (f x)))
       (declare (type integer y))
       (g x y z))

Calls of mv?-let and of mv-let are equivalent when the first argument
contains at least two variables; see MV-LET for documentation.
In the case of binding a single variable, the general form is

     (mv?-let (var)
              term
              (declare ...) ... (declare ...)
              body)

and this is equivalent to the following form (see LET).

     (let ((var term))
       (declare ...) ... (declare ...)
       body)

Also see MV?.

NATP    a recognizer for the natural numbers

The natural numbers is the set of all non-negative integers,
{0,1,2,3,...}.  Natp returns t if and only its argument is a   natural
number, and nil otherwise.  We recommend the file
books/arithmetic/natp-posp.lisp as a book for reasoning about posp
and natp.  This book is included in books/arithmetic/top and
books/arithmetic/top-with-meta.

NFIX    coerce to a natural number

Nfix simply returns any natural number argument unchanged, returning 0
on an argument that is not a natural number.  Also see IFIX,
see RFIX, see REALFIX, and see FIX for
analogous functions that coerce to an integer, a rational number, a
real, and a number, respectively.

Nfix has a guard of t.

NINTH    ninth member of the list

See any Common Lisp documentation for details.

NO-DUPLICATESP    check for duplicates in a list

     General Forms:
     (no-duplicatesp x)
     (no-duplicatesp x :test 'eql)   ; same as above (eql as equality test)
     (no-duplicatesp x :test 'eq)    ; same, but eq is equality test
     (no-duplicatesp x :test 'equal) ; same, but equal is equality test

(no-duplicatesp lst) is true if and only if no member of lst occurs
twice in lst.  The optional keyword, :TEST, has no effect logically,
but provides the test (default eql) used for comparing elements of lst.

The guard for a call of no-duplicatesp depends on the test.  In all
cases, the argument must satisfy true-listp.  If the test is eql, then
the argument must satisfy eqlable-listp.  If the test is eq, then the
argument must satisfy symbol-listp.

See EQUALITY-VARIANTS for a discussion of the relation between
no-duplicatesp and its variants:

     (no-duplicatesp-eq x lst) is equivalent to (no-duplicatesp x lst
     :test 'eq);

     (no-duplicatesp-equal x lst) is equivalent to (no-duplicatesp x
     lst :test 'equal).

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

NO-DUPLICATESP-EQ    See NO-DUPLICATESP.

NO-DUPLICATESP-EQUAL    See NO-DUPLICATESP.

NONNEGATIVE-INTEGER-QUOTIENT    natural number division function

     Example Forms:
     (nonnegative-integer-quotient 14 3) ; equals 4
     (nonnegative-integer-quotient 15 3) ; equals 5

(nonnegative-integer-quotient i j) returns the integer quotient of the
integers i and (non-zero) j, i.e., the largest k such that (* j k) is
less than or equal to i.  Also see FLOOR, see CEILING
and see TRUNCATE, which are derived from this function and
apply to rational numbers.

The guard of (nonnegative-integer-quotient i j) requires that i is a
nonnegative integer and j is a positive integer.

NOT    logical negation

Not is the ACL2 negation function.  The negation of nil is t and the
negation of anything else is nil.

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

NTH    the nth element (zero-based) of a list

(Nth n l) is the nth element of l, zero-based.  If n is greater than or
equal to the length of l, then nth returns nil.

(Nth n l) has a guard that n is a non-negative integer and l is a
true-listp.

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

NTHCDR    final segment of a list

(Nthcdr n l) removes the first n elements from the list l.

The following is a theorem.

     (implies (and (integerp n)
                   (<= 0 n)
                   (true-listp l))
              (equal (length (nthcdr n l))
                     (if (<= n (length l))
                         (- (length l) n)
                       0)))

For related functions, see TAKE and see BUTLAST.

The guard of (nthcdr n l) requires that n is a nonnegative integer and
l is a true list.

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

NULL    recognizer for the empty list

Null is the function that checks whether its argument is nil.  For
recursive definitions it is often preferable to test for the end of a
list using endp instead of null; see ENDP.

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

NUMERATOR    dividend of a ratio in lowest terms

Completion Axiom (completion-of-numerator):

     (equal (numerator x)
            (if (rationalp x)
                (numerator x)
              0))

Guard for (numerator x):

     (rationalp x)

O-FINP    recognizes if an ordinal is finite

We introduce the function o-finp which returns t for any ordinal that
is finite, else nil.  This function is equivalent to the function atom,
and is introduced so that we can disable its definition when dealing
with ordinals (also see MAKE-ORD).

O-FIRST-COEFF    returns the first coefficient of an ordinal

An ACL2 ordinal is either a natural number or, for an infinite ordinal,
a list whose elements are exponent-coefficient pairs (see O-P).
In the latter case, this function returns the cdr of the first pair in
the list.  In the case of a natural number, this function returns the
ordinal itself (since a natural number, n, can be thought of as (w^0)n).

For the corresponding exponent, see O-FIRST-EXPT.

O-FIRST-EXPT    the first exponent of an ordinal

An ACL2 ordinal is either a natural number or, for an infinite ordinal,
a list whose elements are exponent-coefficient pairs (see O-P).
In the latter case, this function returns the car of the first pair in
the list.  In the case of a natural number, the value returned is 0
(since a natural number, n, can be thought of as (w^0)n).

For the corresponding coefficient, see O-FIRST-COEFF.

O-INFP    recognizes if an ordinal is infinite

O-infp is a macro.  (O-infp x) opens up to (not (o-finp x)) (see
O-FINP).

O-P    a recognizer for the ordinals up to epsilon-0

Using the nonnegative integers and lists we can represent the ordinals
up to epsilon-0. The ordinal representation used in ACL2 has changed as
of Version_2.8 from that of Nqthm-1992, courtesy of Pete Manolios and
Daron Vroon; additional discussion may be found in "Ordinal Arithmetic
in ACL2", proceedings of ACL2 Workshop 2003,
`http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/'.  Previously,
ACL2's notion of ordinal was very similar to the development given in
"New Version of the Consistency Proof for Elementary Number Theory" in
The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland
Publishing Company, Amsterdam, 1969, pp 132-213.

The following essay is intended to provide intuition about ordinals.
The truth, of course, lies simply in the ACL2 definitions of o-p and o<.

Very intuitively, think of each non-zero natural number as by being
denoted by a series of the appropriate number of strokes, i.e.,

     0             0
     1             |
     2             ||
     3             |||
     4             ||||
     ...           ...

Then "omega," here written as w, is the ordinal that might be written as

     w             |||||...,

i.e., an infinite number of strokes.  Addition here is just
concatenation.  Observe that adding one to the front of w in the
picture above produces w again, which gives rise to a standard
definition of w:  w is the least ordinal such that adding another
stroke at the beginning does not change the ordinal.

We denote by w+w or w*2 the "doubly infinite" sequence that we might
write as follows.

     w*2           |||||... |||||...

One way to think of w*2 is that it is obtained by replacing each stroke
in 2 (||) by w.  Thus, one can imagine w*3, w*4, etc., which leads
ultimately to the idea of "w*w," the ordinal obtained by replacing each
stroke in w by w.  This is also written as "omega squared" or w^2, or:

      2
     w             |||||... |||||... |||||... |||||... |||||... ...

We can analogously construct w^3 by replacing each stroke in w by w^2
(which, it turns out, is the same as replacing each stroke in w^2 by
w).  That is, we can construct w^3 as w copies of w^2,

      3              2       2       2       2
     w              w  ...  w  ...  w  ...  w ... ...

Then we can construct w^4 as w copies of w^3, w^5 as w copies of w^4,
etc., ultimately suggesting w^w.  We can then stack omegas, i.e.,
(w^w)^w etc.  Consider the "limit" of all of those stacks, which we
might display as follows.

            .
           .
          .
         w
        w
       w
      w
     w

That is epsilon-0.

Below we begin listing some ordinals up to epsilon-0; the reader can
fill in the gaps at his or her leisure.  We show in the left column the
conventional notation, using w as "omega," and in the right column the
ACL2 object representing the corresponding ordinal.

       ordinal            ACL2 representation

       0                  0
       1                  1
       2                  2
       3                  3
       ...                ...
       w                 '((1 . 1) . 0)
       w+1               '((1 . 1) . 1)
       w+2               '((1 . 1) . 2)
       ...                ...
       w*2               '((1 . 2) . 0)
       (w*2)+1           '((1 . 2) . 1)
       ...                ...
       w*3               '((1 . 3) . 0)
       (w*3)+1           '((1 . 3) . 1)
       ...                ...

        2
       w                 '((2 . 1) . 0)
       ...                ...

        2
       w +w*4+3          '((2 . 1) (1 . 4) . 3)
       ...                ...

        3
       w                 '((3 . 1) . 0)
       ...                ...

        w
       w                 '((((1 . 1) . 0) . 1) . 0)
       ...                ...

        w  99
       w +w  +w4+3       '((((1 . 1) . 0) . 1) (99 . 1) (1 . 4) . 3)
       ...                ...

         2
        w
       w                 '((((2 . 1) . 0) . 1) . 0)

       ...                ...

         w
        w
       w                 '((((((1 . 1) . 0) . 1) . 0) . 1) . 0)
       ...               ...

Observe that the sequence of o-ps starts with the natural numbers
(which are recognized by natp). This is convenient because it means
that if a term, such as a measure expression for justifying a recursive
function (see O<) must produce an o-p, it suffices for it to
produce a natural number.

The ordinals listed above are listed in ascending order.  This is the
ordering tested by o<.

The "epsilon-0 ordinals" of ACL2 are recognized by the recursively
defined function o-p.  The base case of the recursion tells us that
natural numbers are epsilon-0 ordinals.  Otherwise, an epsilon-0
ordinal is a list of cons pairs whose final cdr is a natural number,
((a1 . x1) (a2 . x2) ... (an . xn) . p).  This corresponds to the
ordinal (w^a1)x1 + (w^a2)x2 + ... + (w^an)xn + p.  Each ai is an
ordinal in the ACL2 representation that is not equal to 0.  The
sequence of the ai's is strictly decreasing (as defined by o<). Each xi
is a positive integer (as recognized by posp).

Note that infinite ordinals should generally be created using the
ordinal constructor, make-ord, rather than cons. The functions
o-first-expt, o-first-coeff, and o-rst are ordinals destructors.
Finally, the function o-finp and the macro o-infp tell whether an
ordinal is finite or infinite, respectively.

The function o< compares two epsilon-0 ordinals, x and y.  If both are
integers, (o< x y) is just x<y.  If one is an integer and the other is
a cons, the integer is the smaller.  Otherwise, o< recursively compares
the o-first-expts of the ordinals to determine which is smaller.  If
they are the same, the o-first-coeffs of the ordinals are compared.  If
they are equal, the o-rsts of the ordinals are recursively compared.

Fundamental to ACL2 is the fact that o< is well-founded on epsilon-0
ordinals.  That is, there is no "infinitely descending chain" of such
ordinals.  See PROOF-OF-WELL-FOUNDEDNESS.

O-RST    returns the rest of an infinite ordinal

An ACL2 infinite ordinal is a list whose elements are
exponent-coefficient pairs (see O-P and see O-INFP).
The first exponent and first coefficient of an ordinal can be obtained
by using o-first-expt and o-first-coeff respectively.  To obtain the
rest of the ordinal (for recursive analysis), use the o-rst function.
It returns the rest of the ordinal after the first exponent and
coefficient are removed.

O<    the well-founded less-than relation on ordinals up to epsilon-0

If x and y are both o-ps (see O-P) then (o< x y) is true iff x
is strictly less than y.  o< is well-founded on the o-ps.  When x and y
are both nonnegative integers, o< is just the familiar "less than"
relation (<).

o< plays a key role in the formal underpinnings of the ACL2 logic.  In
order for a recursive definition to be admissible it must be proved to
"terminate."  By terminate we mean that the arguments to the function
"get smaller" as the function recurses and this sense of size
comparison must be such that there is no "infinitely descending"
sequence of ever smaller arguments.  That is, the relation used to
compare successive arguments must be well-founded on the domain being
measured.

The most basic way ACL2 provides to prove termination requires the user
to supply (perhaps implicitly) a mapping of the argument tuples into
the ordinals with some "measure" expression in such a way that the
measures of the successive argument tuples produced by recursion
decrease according to the relation o<.  The validity of this method
rests on the well-foundedness of o< on the o-ps.

Without loss of generality, suppose the definition in question
introduces the function f, with one formal parameter x (which might be
a list of objects).  Then we require that there exist a measure
expression, (m x), that always produces an o-p.  Furthermore, consider
any recursive call, (f (d x)), in the body of the definition.  Let hyps
be the conjunction of terms, each of which is either the test of an if
in the body or else the negation of such a test, describing the path
through the body to the recursive call in question.  Then it must be a
theorem that

       (IMPLIES hyps (O< (m (d x)) (m x))).

When we say o< is "well-founded" on the o-ps we mean that there is no
infinite sequence of o-ps such that each is smaller than its
predecessor in the sequence.  Thus, the theorems that must be proved
about f when it is introduced establish that it cannot recur forever
because each time a recursive call is taken (m x) gets smaller.  From
this, and the syntactic restrictions on definitions, it can be shown
(as on page 44 in "A Computational Logic", Boyer and Moore, Academic
Press, 1979) that there exists a function satisfying the definition;
intuitively, the value assigned to any given x by the alleged function
is that computed by a sufficiently large machine.  Hence, the logic is
consistent if the axiom defining f is added.

See O-P for a discussion of the ordinals and how to compare two
ordinals.

The definitional principle permits the use of relations other than o<
but they must first be proved to be well-founded on some domain.  See
WELL-FOUNDED-RELATION.  Roughly put, alternative relations are
shown well-founded by providing an order-preserving mapping from their
domain into the ordinals.  See DEFUN for details on how to
specify which well-founded relation is to be used.

O<=    the less-than-or-equal relation for the ordinals

o<= is a macro and (o<= x y) expands to (not (o< y x)).  See O<.

O>    the greater-than relation for the ordinals

O> is a macro and (o> x y) expands to (o< y x).  See O<.

O>=    the greater-than-or-equal relation for the ordinals

O>= is a macro and (o>= x y) expands to (not (o< x y)).  See O<.

OBSERVATION    print an observation

Here is a typical application of observation.

     ACL2 !>(let ((ctx 'top-level)
                  (name 'foo))
              (observation ctx
                           "Skipping processing of name ~x0."
                           name))

     ACL2 Observation in TOP-LEVEL:  Skipping processing of name FOO.
     <state>
     ACL2 !>

Observation prints an initial "ACL2 Observation...:  ", and then prints
the indicated message using formatted printing (see FMT).
Notice in the example above that evaluation of a call of observation
returns state.  Indeed, observation is actually a macro whose expansion
takes and returns the ACL2 state.  A similar utility, observation-cw,
is available that does not take or return state; rather, it returns nil
as the suffix "cw" suggests that a "comment window" is the target of
this printing, rather than the state.  For example:

     ACL2 !>(let ((ctx 'top-level)
                  (name 'foo))
              (observation-cw ctx
                              "Skipping processing of name ~x0."
                              name))

     ACL2 Observation in TOP-LEVEL:  Skipping processing of name FOO.
     NIL
     ACL2 !>

Observation-cw takes exactly the same arguments as observation, but
observation-cw does its printing in a so-called "wormhole"; see
WORMHOLE.

     General Forms:
     (observation    ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)
     (observation-cw ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)

where ctx generally evaluates to a symbol (but see below), and
fmt-string together with the fmt-argi are suitable for passing to fmt.
Output begins and ends with a newline.

Recall from the example above that the output from a call of observation
(or observation-cw) begins with "ACL2 Observation" and additional
characters ending in ":  ", for example " in TOP-LEVEL:  ", followed by
formatted output produced from fmt-string with the given fmt-argi.  The
characters printed immediately following the string "ACL2 Observation"
depend on the value of ctx.  If ctx is nil, nothing is printed.  If ctx
is a non-nil symbol, it is printed using fmt directive ~x.  If ctx is a
cons pair whose car is a symbol, formatted printing is applied to the
string "(~x0 ~x1 ...)", where #\0 and #\1 are bound respectively to
that car and cdr.  Otherwise, ctx is printed using fmt directive ~@.

We next discuss situations in which printing is inhibited for
observation and observation-cw.  No printing is done when observation
is among the inhibited output types; see
SET-INHIBIT-OUTPUT-LST.  Moreover, no printing is done by observation
during include-book.  If you want to avoid printing from observation-cw
during include-book, then you need to manage that yourself.

OBSERVATION-CW    See OBSERVATION.

ODDP    test whether an integer is odd

(oddp x) is true if and only if x is odd, i.e., not even in the sense
of evenp.

The guard for oddp requires its argument to be an integer.

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

OPEN-INPUT-CHANNEL    See IO.

OPEN-INPUT-CHANNEL-P    See IO.

OPEN-OUTPUT-CHANNEL    See IO.

OPEN-OUTPUT-CHANNEL-P    See IO.

OPTIMIZE    See DECLARE.

OR    disjunction

Or is the macro for disjunctions.  Or takes any number of arguments and
returns the first that is non-nil, or nil if there is no non-nil
element.

In the ACL2 logic, the macroexpansion of (or x y) is an IF term that
appears to cause x to be evaluated twice:

     ACL2 !>:trans (or x y)

     (IF X X Y)

     => *

     ACL2 !>

If x were replaced by an expression whose evaluation takes a long time,
then such an expansion would be ineffecient.  However, don't be fooled:
you can expect Common Lisp implementations to avoid this problem, say by
generating a new variable, for example:

     ACL2 !>:q ; Exit the ACL2 loop and go into raw Common Lisp

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>(macroexpand '(or x y))

     (LET ((#:G5374 X)) (IF #:G5374 #:G5374 Y))
     T

     ACL2>

Or is a Common Lisp macro.  See any Common Lisp documentation for more
information.

PAIRLIS    See PAIRLIS$

The Common Lisp language allows its pairlis function to construct an
alist in any order!  So we have to define our own version: See
PAIRLIS$.

PAIRLIS$    zipper together two lists

The Common Lisp language allows its pairlis function to construct an
alist in any order!  So we have to define our own version, pairlis$.
It returns the list of pairs obtained by consing together successive
respective members of the given lists until the first list runs out.
(Hence in particular, if the second argument is nil then each element
of the first argument is paired with nil.)

The guard for pairlis$ requires that its arguments are true lists.

PEEK-CHAR$    See IO.

PKG-IMPORTS    list of symbols imported into a given package

Completion Axiom (completion-of-pkg-imports):

     (equal (pkg-imports x)
            (if (stringp x)
                (pkg-imports x)
              nil))

Guard for (pkg-imports x):

     (stringp x)

(Pkg-imports pkg) returns a duplicate-free list of all symbols imported
into pkg, which should be the name of a package known to ACL2.  For
example, suppose "MY-PKG" was created by

     (defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).

Then (pkg-imports "MY-PKG") equals the list (ACL2::ABC LISP::CAR).

If pkg is not a string, then (pkg-imports pkg) is nil.  If pkg is a
string but not the name of a package known to ACL2, then the value of
the form (pkg-imports pkg) is unspecified, and it evaluation will fail
to yield a value.  By "the symbols imported into pkg" we mean the
symbols imported into pkg by the defpkg event that introduced pkg.
There are no imports for built-in packages except for the "ACL2"
package, which imports the symbols in the list value of the constant
*common-lisp-symbols-from-main-lisp-package*.  In particular, this is
the case for the "COMMON-LISP" package.  Users familiar with Common
Lisp may find this surprising, since in actual Common Lisp
implementations it is often the case that many symbols in that package
are imported from other packages.  However, ACL2 treats all symbols in
the constant *common-lisp-symbols-from-main-lisp-package* as having a
symbol-package-name of "COMMON-LISP", as though they were not imported.
ACL2 admits a symbol imported into in the "COMMON-LISP" package only if
it belongs to that list: any attempt to read any other symbol imported
into the "COMMON-LISP" package, or to produce such a symbol with
intern$ or intern-in-package-of-symbol, will cause an error.

The following axioms formalize properties of pkg-imports discussed above
(use :pe to view them).

     symbol-package-name-intern-in-package-of-symbol
     intern-in-package-of-symbol-is-identity
     symbol-listp-pkg-imports
     no-duplicatesp-pkg-imports
     completion-of-pkg-imports

PKG-WITNESS    return a specific symbol in the indicated package

For any string pkg that names a package currently known to ACL2,
(pkg-witness pkg) is a symbol in that package whose symbol-name is the
value of constant *pkg-witness-name*.  Logically, this is the case even
if the package is not currently known to ACL2.  However, if pkg-witness
is called on a string that is not the name of a package known to ACL2,
a hard Lisp error will result.

(Pkg-witness pkg) has a guard of (and (stringp pkg) (not (equal pkg
""))).  If pkg is not a string, then (pkg-witness pkg) is equal to
(pkg-witness "ACL2")

PLUSP    test whether a number is positive

(Plusp x) is true if and only if x > 0.

The guard of plusp requires its argument to be a rational (real, in
ACL2(r)) number.

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

POSITION    position of an item in a string or a list

     General Forms:
     (position x seq)
     (position x seq :test 'eql)   ; same as above (eql as equality test)
     (position x seq :test 'eq)    ; same, but eq is equality test
     (position x seq :test 'equal) ; same, but equal is equality test

(Position x seq) is the least index (zero-based) of the element x in
the string or list seq, if x is an element of seq.  Otherwise (position
x seq) is nil.  The optional keyword, :TEST, has no effect logically,
but provides the test (default eql) used for comparing x with items of
seq.

The guard for a call of position depends on the test.  In all cases,
the second argument must satisfy stringp or true-listp.  If the test is
eql, then either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

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

     (position-eq x seq) is equivalent to (position x seq :test 'eq);

     (position-equal x seq) is equivalent to (position x seq :test
     'equal).

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

Position is defined by Common Lisp.  See any Common Lisp documentation
for more information.

POSITION-EQ    See POSITION.

POSITION-EQUAL    See POSITION.

POSP    a recognizer for the positive integers

(posp x) is logically equivalent to (not (zp x)) (see ZP) and
also   to (and (natp x) (not (equal x 0))).  We recommend the file
books/ordinals/natp-posp as a book for reasoning about posp and   natp.
This book is included in books/arithmetic/top and
books/arithmetic/top-with-meta.

PPROGN    evaluate a sequence of forms that return state

     Example Form:
     (pprogn
      (cond ((or (equal (car l) #\) (equal (car l) slash-char))
             (princ$ #\ channel state))
            (t state))
      (princ$ (car l) channel state)
      (mv (cdr l) state))

The convention for pprogn usage is to give it a non-empty sequence of
forms, each of which (except possibly for the last) returns state (see
STATE) as its only value.  The state returned by each but the
last is passed on to the next.  The value or values of the last form
are returned as the value of the pprogn.

If you are using single-threaded objects you may wish to define an
analogue of this function for your own stobj.

General Form:

     (PPROGN form1
             form2
             ...
             formk
             result-form)

This general form is equivalent, via macro expansion, to:

     (LET ((STATE form1))
          (LET ((STATE form2))
               ...
               (LET ((STATE formk))
                    result-form)))

PRINT-OBJECT$    See IO.

PRINTING-TO-STRINGS    printing to strings instead of files or standard output

Each of ACL2's formatted printing functions, FM*, has an analoguous
macro FM*-TO-STRING indicated below.  These functions do not include a
channel or state as an argument, and FM*-TO-STRING returns the string
that FM* would print to the state, in place of state; see FMT.
The legal keyword arguments are described below.

     General Forms:                                 result
     (fms-to-string string alist &key ...)          ; string
     (fmt-to-string string alist &key ...)          ; (mv col string)
     (fmt1-to-string string alist column &key ...)  ; (mv col string)
     (fms!-to-string string alist &key ...)         ; string
     (fmt!-to-string string alist &key ...)         ; (mv col string)
     (fmt1!-to-string string alist column &key ...) ; (mv col string)

The legal keyword arguments are as follows.  They are all optional with
a default of nil.

     Evisc-tuple is evaluated, and corresponds exactly to the
     evisc-tuple argument of the corresponding FM* function; see
     FMT.

     Fmt-control-alist should typically evaluate to an alist that maps
     print-control variables to values; see PRINT-CONTROL.  Any
     alist mapping variables to values is legal, however.  By default
     the print controls are set according to the value of constant
     *fmt-control-defaults*; fmt-control-alist overrides these defaults.

     Iprint is typically nil, but t is also a legal value.  See
     SET-IPRINT for the effect of value t, which however is local to
     this call of a FM*-TO-STRING function; the behavior if iprinting
     afterwards is not affected by this call.  In particular, you will
     not be able to look at the values of iprint tokens printed by this
     call, so the value t is probably of limited utility at best.

Also see IO for a discussion of the utility
get-output-stream-string$, which allows for accumulating the results of
more than one printing call into a single string but requires the use
of state.

PROG2$    execute two forms and return the value of the second one

See HARD-ERROR, see ILLEGAL, and see CW for
examples of functions to call in the first argument of prog2$.

Semantically, (Prog2$ x y) equals y; the value of x is ignored.
However, x is first evaluated for side effect.  Since the ACL2
programming language is applicative, there can be no logical impact of
evaluating x.  However, x may involve a call of a function such as
hard-error or illegal, which can cause so-called "hard errors", or a
call of cw to perform output.

Here is a simple, contrived example using hard-error.  The intention is
to check at run-time that the input is appropriate before calling
function bar.

     (defun foo-a (x)
       (declare (xargs :guard (consp x)))
       (prog2$
        (or (good-car-p (car x))
            (hard-error 'foo-a
                        "Bad value for x: ~p0"
                        (list (cons #\0 x))))
        (bar x)))

The following similar function uses illegal instead of hard-error.
Since illegal has a guard of nil, guard verification would guarantee
that the call of illegal below will never be made (at least when guard
checking is on; see SET-GUARD-CHECKING).

     (defun foo-b (x)
       (declare (xargs :guard (and (consp x) (good-car-p (car x)))))
       (prog2$
        (or (good-car-p (car x))
            (illegal 'foo-b
                     "Bad value for x: ~p0"
                     (list (cons #\0 x))))
        (bar x)))

We conclude with a simple example using cw from the ACL2 sources.

     (defun print-terms (terms iff-flg wrld)

     ; Print untranslations of the given terms with respect to iff-flg, following
     ; each with a newline.

     ; We use cw instead of the fmt functions because we want to be able to use this
     ; function in print-type-alist-segments (used in brkpt1), which does not return
     ; state.

       (if (endp terms)
           terms
         (prog2$
          (cw "~q0" (untranslate (car terms) iff-flg wrld))
          (print-terms (cdr terms) iff-flg wrld))))

PROGN$    execute a sequence of forms and return the value of the last one

This macro expands to a corresponding nest of calls of prog2$; see
PROG2$.  The examples below show how this works: the first case
below is typical, but we conclude with two special cases.

     ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x))
      (PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X)))
     ACL2 !>:trans1 (progn$ (f1 x) (f2 x))
      (PROG2$ (F1 X) (F2 X))
     ACL2 !>:trans1 (progn$ (f1 x))
      (F1 X)
     ACL2 !>:trans1 (progn$)
      NIL
     ACL2 !>

PROOFS-CO    the proofs character output channel

Proofs-co is an ld special (see LD).  The accessor is
(proofs-co state) and the updater is (set-proofs-co val state).
Proofs-co must be an open character output channel.  It is to this
channel that defun, defthm, and the other event commands print their
commentary.

"Proofs-co" stands for "proofs character output." The initial value of
proofs-co is the same as the value of *standard-co* (see
*STANDARD-CO*).

PROPER-CONSP    recognizer for proper (null-terminated) non-empty lists

Proper-consp is the function that checks whether its argument is a
non-empty list that ends in nil.  Also see TRUE-LISTP.

PUT-ASSOC    modify an association list by associating a value with a key

     General Forms:
     (put-assoc name val alist)
     (put-assoc name val alist :test 'eql)   ; same as above (eql as equality test)
     (put-assoc name val alist :test 'eq)    ; same, but eq is equality test
     (put-assoc name val alist :test 'equal) ; same, but equal is equality test

(Put-assoc name val alist) returns an alist that is the same as the list
alist, except that the first pair in alist with a car of name is
replaced by (cons name val), if there is one.  If there is no such
pair, then (cons name val) is added at the end.  Note that the order of
the keys occurring in alist is unchanged (though a new key may be
added).

The guard for a call of put-assoc depends on the test.  In all cases,
the last argument must satisfy alistp.  If the test is eql, then either
the first argument must be suitable for eql (see EQLABLEP) or
the last argument must satisfy eqlable-alistp.  If the test is eq, then
either the first argument must be a symbol or the last argument must
satisfy symbol-alistp.

See EQUALITY-VARIANTS for a discussion of the relation between
put-assoc and its variants:

     (put-assoc-eq name val alist) is equivalent to (put-assoc name val
     alist :test 'eq);

     (put-assoc-equal name val alist) is equivalent to (put-assoc name
     val alist :test 'equal).

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

PUT-ASSOC-EQ    See PUT-ASSOC.

PUT-ASSOC-EQL    See PUT-ASSOC.

PUT-ASSOC-EQUAL    See PUT-ASSOC.

PUTPROP    update fast property lists

     General form:
     (putprop symbol key value world-alist)

See books/misc/getprop.lisp for an example that illustrates the use of
ACL2 utilities getprop and putprop to take advantage of under-the-hood
Lisp (hashed) property lists.

QUOTE    create a constant

The form (quote x) evaluates to x.  See any Common Lisp documentation.

R-EQLABLE-ALISTP    recognizer for a true list of pairs whose cdrs are suitable for eql

The predicate r-eqlable-alistp tests whether its argument is a
true-listp of consp objects whose cdrs all satisfy eqlablep.

R-SYMBOL-ALISTP    recognizer for association lists with symbols as values

(R-symbol-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where val is a symbolp.

RANDOM$    obtain a random value

     Example:
     (random$ 10 state) ==> (mv 7 <state>)

(Random$ limit state), where limit is a positive integer, returns a
random non-negative integer together with a new state.  Logically, it
simply returns the first element of a list that is a field of the ACL2
state, called the acl2-oracle, together with the new state resulting
from removing that element from that list.  (Except, if that element is
not in range as specified above, then 0 is returned.)  However, random$
actually invokes a Common Lisp function to choose the integer returned.
Quoting from the Common Lisp HyperSpec(TM),
`http://www.lispworks.com/documentation/HyperSpec/Front': "An
approximately uniform choice distribution is used...  each of the
possible results occurs with (approximate) probability 1/limit."

Consider enabling rules natp-random$ and random$-linear if you want to
reason about random$.

RASSOC    look up value in association list

     General Forms:
     (rassoc x alist)
     (rassoc x alist :test 'eql)   ; same as above (eql as equality test)
     (rassoc x alist :test 'eq)    ; same, but eq is equality test
     (rassoc x alist :test 'equal) ; same, but equal is equality test

(Rassoc x alist) is the first member of alist whose cdr is x, or nil if
no such member exists.  (rassoc x alist) is thus similar to (assoc x
alist), the difference being that it looks for the first pair in the
given alist whose cdr, rather than car, is eql to x.  See
ASSOC.  The optional keyword, :TEST, has no effect logically, but
provides the test (default eql) used for comparing x with the cdrs of
successive elements of lst.

The guard for a call of rassoc depends on the test.  In all cases, the
second argument must satisfy alistp.  If the test is eql, then either
the first argument must be suitable for eql (see EQLABLEP) or
the second argument must satisfy r-eqlable-alistp.  If the test is eq,
then either the first argument must be a symbol or the second argument
must satisfy r-symbol-alistp.

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

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

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

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

Rassoc is defined by Common Lisp.  See any Common Lisp documentation for
more information.

RASSOC-EQ    See RASSOC.

RASSOC-EQUAL    See RASSOC.

RATIONAL-LISTP    recognizer for a true list of rational numbers

The predicate rational-listp tests whether its argument is a true list
of rational numbers.

RATIONALP    recognizer for rational numbers (ratios and integers)

(rationalp x) is true if and only if x is an rational number.

READ-BYTE$    See IO.

READ-CHAR$    See IO.

READ-OBJECT    See IO.

REAL/RATIONALP    recognizer for rational numbers (including real number in ACL2(r))

For most ACL2 users, this is a macro abbreviating rationalp.  In
ACL2(r) (see REAL), this macro abbreviates the predicate realp,
which holds for real numbers as well (including rationals).  Most ACL2
users can ignore this macro and use rationalp instead, but many books
in the ACL2 distribution use real/rationalp so that these books will be
suitable for ACL2(r) as well.

REALFIX    coerce to a real number

Realfix simply returns any real number argument unchanged, returning 0
on a non-real argument.  Also see NFIX, see IFIX, see
RFIX, and see FIX for analogous functions that coerce
to a natural number, an integer, a rational, and a number, respectively.

Realfix has a guard of t.

REALPART    real part of a complex number

Completion Axiom (completion-of-realpart):

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

Guard for (realpart x):

     (acl2-numberp x)

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.

REM    remainder using truncate

     ACL2 !>(rem 14 3)
     2
     ACL2 !>(rem -14 3)
     -2
     ACL2 !>(rem 14 -3)
     2
     ACL2 !>(rem -14 -3)
     -2
     ACL2 !>(rem -15 -3)
     0
     ACL2 !>

(Rem i j) is that number k for which (* j (truncate i j)) added to k
equals i.

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

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

REMOVE    remove all occurrences

     General Forms:
     (remove x lst)
     (remove x lst :test 'eql)   ; same as above (eql as equality test)
     (remove x lst :test 'eq)    ; same, but eq is equality test
     (remove x lst :test 'equal) ; same, but equal is equality test

(Remove x lst) is equal to lst if x is not a member of lst, else is the
result of removing all occurrences of x from lst.  The optional
keyword, :TEST, has no effect logically, but provides the test (default
eql) used for comparing x with successive elements of lst.

Also see REMOVE1.

The guard for a call of remove depends on the test.  In all cases, the
second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

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

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

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

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

Remove is defined by Common Lisp.  See any Common Lisp documentation for
more information.

REMOVE-DUPLICATES    remove duplicates from a string or a list

     General Forms:
     (remove-duplicates x)
     (remove-duplicates x :test 'eql)   ; same as above (eql as equality test)
     (remove-duplicates x :test 'eq)    ; same, but eq is equality test
     (remove-duplicates x :test 'equal) ; same, but equal is equality test

(Remove-duplicates x) returns the result of deleting duplicate elements
from the beginning of the list or string x.  For example,
(remove-duplicates '(1 2 3 2 4)) is equal to '(1 3 2 4).  The optional
keyword, :TEST, has no effect logically, but provides the test (default
eql) used for comparing x with successive elements of lst.

The guard for a call of remove-duplicates depends on the test.  In all
cases, the argument must satisfy stringp or true-listp.  If the test is
eql, then the argument must satisfy either stringp or eqlable-listp.
If the test is eq, then the argument must satisfy symbol-listp.

The relation between remove-duplicates and its variants is related to
the usual pattern for equality variants; see EQUALITY-VARIANTS.
However, the possibility of a string argument changes the usual pattern
a bit.  As one might expect:

     (remove-duplicates-eq lst) is equivalent to (remove-duplicates lst
     :test 'eq).

However, remove-duplicates-equal is defined without consideration of
strings, for backward compatibility with versions of ACL2 through
Version_4.2.  The macro remove-duplicates-logic has been introduced to
model the behavior of remove-duplicates even on strings; use :pe if you
wish to see its definition.  So we can say the following.

     (remove-duplicates-logic lst) is equivalent to (remove-duplicates
     lst :test 'equal); and

     (remove-duplicates-logic lst) is equal to (remove-duplicates-equal
     lst) when lst is not a string.

In particular, when the argument is not a string, reasoning about any of
these primitives reduces to reasoning about the function
remove-duplicates-equal.

Remove-duplicates is defined by Common Lisp.  See any Common Lisp
documentation for more information.

REMOVE-DUPLICATES-EQ    See REMOVE-DUPLICATES.

REMOVE-DUPLICATES-EQUAL    See REMOVE-DUPLICATES.

REMOVE-EQ    See REMOVE.

REMOVE-EQUAL    See REMOVE.

REMOVE1    remove first occurrences, testing using eql

     General Forms:
     (remove1 x lst)
     (remove1 x lst :test 'eql)   ; same as above (eql as equality test)
     (remove1 x lst :test 'eq)    ; same, but eq is equality test
     (remove1 x lst :test 'equal) ; same, but equal is equality test

(Remove1 x lst) is equal to lst if x is not a member of lst, else is
the result of removing the first occurrences of x from lst.  The
optional keyword, :TEST, has no effect logically, but provides the test
(default eql) used for comparing x with successive elements of lst.

Also see REMOVE.

The guard for a call of remove1 depends on the test.  In all cases, the
second argument must satisfy true-listp.  If the test is eql, then
either the first argument must be suitable for eql (see
EQLABLEP) or the second argument must satisfy eqlable-listp.  If the
test is eq, then either the first argument must be a symbol or the
second argument must satisfy symbol-listp.

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

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

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

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

REMOVE1-EQ    See REMOVE1.

REMOVE1-EQUAL    See REMOVE1.

REST    rest (cdr) of the list

In the logic, rest is just a macro for cdr.

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

RETURN-LAST    return the last argument, perhaps with side effects

Return-last is an ACL2 function that returns its last argument.  It is
used to implement common utilities such as prog2$ and time$.  For most
users, this may already be more than one needs to know about
return-last; for example, ACL2 tends to avoid printing calls of
return-last in its output, printing calls of prog2$ or time$ (or other
such utilities) instead.

If you encounter a call of return-last during a proof, then you may find
it most useful to consider return-last simply as a function defined by
the following equation.

     (equal (return-last x y z) z)

It may also be useful to know that unlike other ACL2 functions,
return-last can take a multiple value as its last argument, in which
case this multiple value is returned.  The following contrived
definition illustrates this point.

     ACL2 !>(defun foo (fn x y z)
              (return-last fn x (mv y z)))

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

     (FOO * * * *) => (MV * *).

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FOO
     ACL2 !>(foo 'bar 3 4 5)
     (4 5)
     ACL2 !>(mv-let (a b)
                    (foo 'bar 3 4 5)
                    (cons b a))
     (5 . 4)
     ACL2 !>

Most readers would be well served to avoid reading the rest of this
documentation of return-last.  For reference, however, below we document
it in some detail.  We include some discussion of its evaluation, in
particular its behavior in raw Lisp, because we expect that most who
read further are working with raw Lisp code (and trust tags).

Return-last is an ACL2 function that can arise from macroexpansion of
certain utilities that return their last argument, which may be a
multiple value.  Consider for example the simplest of these, prog2$:

     ACL2 !>:trans1 (prog2$ (cw "Some CW printing...~%") (+ 3 4))
      (RETURN-LAST 'PROGN
                   (CW "Some CW printing...~%")
                   (+ 3 4))
     ACL2 !>

Notice that a call of prog2$ macroexpands to a call of return-last in
which the first argument is (quote progn).  Although return-last is a
function in the ACL2 world, it is implemented "under the hood" as a
macro in raw Lisp, as the following log (continuing the example above)
illustrates.

     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ? [RAW LISP] (macroexpand-1 '(RETURN-LAST 'PROGN
                                                (CW "Some CW printing...~%")
                                                (+ 3 4)))
     (PROGN (LET ((*AOKP* T)) (CW "SOME CW PRINTING...~%")) (+ 3 4))
     T
     ? [RAW LISP]

Thus, the original prog2$ call generates a corresponding call of progn
in raw Lisp, which in turn causes evaluation of each argument and
returns whatever is returned by evaluation of the last (second)
argument.

(Remark for those who use defattach.  The binding of *aokp* to t is
always included for the second argument as shown except when the first
argument is of the form (QUOTE M) where M is a macro, or (less
important) when the first argument is a symbol or a cons whose car is
QUOTE.  This binding allows ACL2 to use attachments in the second
argument of return-last (hence, in the first argument of prog2$), even
in contexts such as proofs in which attachments are normally not
allowed.  Those who use the experimental HONS version of ACL2 (see
HONS-AND-MEMOIZATION) will see an additional binding in the
above single-step macroexpansion, which allows the storing of memoized
results even when that would otherwise be prevented because of the use
of attachments.)

In general, a form (return-last (quote F) X Y) macroexpands to (F X Y),
where F is defined in raw Lisp to return its last argument.  The case
that F is progn is a bit misleading, because it is so simple.  More
commonly, macroexpansion produces a call of a macro defined in raw Lisp
that may produce side effects.  Consider for example the ACL2 utility
with-guard-checking, which is intended to change the guard-checking
mode to the indicated value (see WITH-GUARD-CHECKING).

     ACL2 !>(with-guard-checking :none (car 3)) ; no guard violation
     NIL
     ACL2 !>:trans1 (with-guard-checking :none (car 3))
      (WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                            (CAR 3))
     ACL2 !>:trans1 (WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                                          (CAR 3))
      (RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
                   (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                   (CAR 3))
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ? [RAW LISP] (macroexpand-1
                   '(RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
                                  (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                                  (CAR 3)))
     (WITH-GUARD-CHECKING1-RAW (CHK-WITH-GUARD-CHECKING-ARG :NONE) (CAR 3))
     T
     ? [RAW LISP] (pprint
                   (macroexpand-1
                    '(WITH-GUARD-CHECKING1-RAW
                      (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                      (CAR 3))))

     (LET ((ACL2_GLOBAL_ACL2::GUARD-CHECKING-ON
            (CHK-WITH-GUARD-CHECKING-ARG :NONE)))
       (DECLARE (SPECIAL ACL2_GLOBAL_ACL2::GUARD-CHECKING-ON))
       (CAR 3))
     ? [RAW LISP]

The above raw Lisp code binds the state global variable
guard-checking-on to :none, as chk-with-guard-checking-arg is just the
identity function except for causing a hard error for an illegal input.

The intended use of return-last is that the second argument is evaluated
first in a normal manner, and then the third argument is evaluated in an
environment that may depend on the value of the second argument.  (For
example, the macro with-prover-time-limit macroexpands to a call of
return-last with a first argument of 'WITH-PROVER-TIME-LIMIT1-RAW, a
second argument that evaluates to a numeric time limit, and a third
argument that is evaluated in an environment where the theorem prover
is restricted to avoid running longer than that time limit.)  Although
this intended usage model is not strictly enforced, it is useful to
keep in mind in the following description of how calls of return-last
are handled by the ACL2 evaluator.

When a form is submitted in the top-level loop, it is handled by ACL2's
custom evaluator.  That evaluator is specified to respect the semantics
of the expression supplied to it: briefly put, if an expression E
evaluates to a value V, then the equality (equal E (quote V)) should be
a theorem.  Notice that this specification does not discuss the
side-effects that may occur when evaluating a call of return-last, so
we discuss that now.  Suppose that the ACL2 evaluator encounters the
call (return-last 'fn expr1 expr2).  First it evaluates expr1.  If this
evaluation succeeds without error, then it constructs an expression of
the form (fn *x* ev-form), where *x* is a Lisp variable bound to the
result of evaluating expr1 and ev-form is a call of the evaluator for
expr2.  (Those who want implementation details are invited to look at
function ev-rec-return-last in ACL2 source file translate.lisp.)  There
are exceptions if fn is progn, ec-call1-raw, with-guard-checking1-raw,
or mbe1-raw, but the main idea is the same: do a reasonable job
emulating the behavior of a raw-Lisp call of return-last.

The following log shows how a time$ call can generate a call of the
evaluator for the last argument of return-last (arguent expr2, above).
We use :trans1 to show single-step macroexpansions, which indicate how
a call of time$ expands to a call of return-last.  The implementation
actually binds the Lisp variable *RETURN-LAST-ARG3* to expr2 before
calling the ACL2 evaluator, ev-rec.

     ACL2 !>:trans1 (time$ (+ 3 4))
      (TIME$1 (LIST 0 NIL NIL NIL NIL)
              (+ 3 4))
     ACL2 !>:trans1 (TIME$1 (LIST 0 NIL NIL NIL NIL)
                            (+ 3 4))
      (RETURN-LAST 'TIME$1-RAW
                   (LIST 0 NIL NIL NIL NIL)
                   (+ 3 4))
     ACL2 !>(time$ (+ 3 4))
     ; (EV-REC *RETURN-LAST-ARG3* ...) took
     ; 0.00 seconds realtime, 0.00 seconds runtime
     ; (1,120 bytes allocated).
     7
     ACL2 !>

We now show how things can go wrong in other than the "intended use"
case described above.  In the example below, the macro mac-raw is
operating directly on the syntactic representation of its first
argument, which it obtains of course as the second argument of a
return-last call.  Again this "intended use" of return-last requires
that argument to be evaluated and then only its result is relevant; its
syntax is not supposed to matter.  We emphasize that only top-level
evaluation depends on this "intended use"; once evaluation is passed to
Lisp, the issue disappears.  We illustrate below how to use the
top-level utility to avoid this issue; see TOP-LEVEL.  The
example uses the utility defmacro-last to "install" special handling of
the raw-Lisp macro mac-raw by return-last; later below we discuss
defmacro-last.

     ACL2 !>(defttag t)

     TTAG NOTE: Adding ttag T from the top level loop.
      T
     ACL2 !>(progn!
              (set-raw-mode t)
              (defmacro mac-raw (x y)
                `(progn (print (quote ,(cadr x)))
                        (terpri) ; newline
                        ,y)))

     Summary
     Form:  ( PROGN! (SET-RAW-MODE T) ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      NIL
     ACL2 !>(defmacro-last mac)
     [[ ... output omitted ... ]]
      RETURN-LAST-TABLE
     ACL2 !>(return-last 'mac-raw '3 nil)

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  Fault during read of memory address #x120000300006
     ***********************************************

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

     To enable breaks into the debugger (also see :DOC acl2-customization):
     (SET-DEBUGGER-ENABLE T)
     ACL2 !>(top-level (return-last 'mac-raw '3 nil))

     3
     NIL
     ACL2 !>

We next describe how to extend the behavior of return-last.  This
requires an active trust tag (see DEFTTAG), and is accomplished
by extending a table provided by ACL2, see RETURN-LAST-TABLE.
Rather than using table events directly for this purpose, it is
probably more convenient to use a macro, defmacro-last.  We describe
the distributed book books/misc/profiling.lisp in order to illustrate
how this works.  The events in that book include the following, which
are described below.

     (defttag :profiling)

     (progn!
      (set-raw-mode t)
      (load (concatenate 'string (cbd) "profiling-raw.lsp")))

     (defmacro-last with-profiling)

The first event introduces a trust tag.  The second loads a file into
raw Lisp that defines a macro, with-profiling-raw, which can do
profiling for the form to be evaluated.  The third introduces an ACL2
macro with-profiling, whose calls expand into calls of the form
(return-last (quote with-profiling-raw) & &).  The third event also
extends return-last-table so that these calls will expand in raw Lisp
to calls of with-profiling-raw.

The example above illustrates the following methodology for introducing
a macro that returns its last argument but produces useful side-effects
with raw Lisp code.

     (1) Introduce a trust tag (see DEFTTAG).

     (2) Using progn!, load into raw Lisp a file defining a macro,
     RAW-NAME, that takes two arguments, returning its last (second)
     argument but using the first argument to produce desired side
     effects during evaluation of that last argument.

     (3) Evaluate the form (defmacro-last NAME :raw RAW-NAME).  This
     will introduce NAME as an ACL2 macro that expands to a
     corresponding call of RAW-NAME (see (2) above) in raw Lisp.  The
     specification of keyword value of :raw as RAW-NAME may be omitted
     if RAW-NAME is the result of modifying the symbol NAME by
     suffixing the string "-RAW" to the symbol-name of NAME.

It is useful to explore what is done by defmacro-last.

     ACL2 !>:trans1 (defmacro-last with-profiling)
      (PROGN (DEFMACRO WITH-PROFILING (X Y)
                       (LIST 'RETURN-LAST
                             (LIST 'QUOTE 'WITH-PROFILING-RAW)
                             X Y))
             (TABLE RETURN-LAST-TABLE 'WITH-PROFILING-RAW
                    'WITH-PROFILING))
     ACL2 !>:trans1 (with-profiling '(assoc-eq fgetprop rewrite) (mini-proveall))
      (RETURN-LAST 'WITH-PROFILING-RAW
                   '(ASSOC-EQ FGETPROP REWRITE)
                   (MINI-PROVEALL))
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ? [RAW LISP] (macroexpand-1
                   '(RETURN-LAST 'WITH-PROFILING-RAW
                                  '(ASSOC-EQ FGETPROP REWRITE)
                                  (MINI-PROVEALL)))
     (WITH-PROFILING-RAW '(ASSOC-EQ FGETPROP REWRITE) (MINI-PROVEALL))
     T
     ? [RAW LISP]

To understand the macro with-profiling-raw you could look at the
distributed file loaded above: books/misc/profiling-raw.lsp.  If you
wish to automate certification of such a book with makefiles (see
BOOK-MAKEFILES, perhaps contributing such a book to the ACL2 books
repository (see `http://acl2-books.googlecode.com/'), you may also wish
to look at distributed file books/misc/Makefile, where you'll notice
the following extra `make' dependency:

     profiling.cert: profiling-raw.lsp

We mentioned above that ACL2 tends to print calls of prog2$ or time$
(or other such utilities) instead of calls of return-last.  Here we
elaborate that point.  ACL2's `untranslate' utility treats (return-last
(quote F) X Y) as (F X Y) if F is a key in return-last-table.  However,
it is generally rare to encounter such a term during a proof, since
calls of return-last are generally expanded away early during a proof.

Calls of return-last that occur in code -- forms submitted in the
top-level ACL2 loop, and definition bodies other than those marked as
non-executable (see DEFUN-NX) -- have the following
restriction: if the first argument is of the form (quote F), then F
must be an entry in return-last-table.  There are however four
exceptions: the following symbols are considered to be keys of
return-last-table even if they are no longer associated with non-nil
values, say because of a table event with keyword :clear.

     * progn, associated with prog2$
     * mbe1-raw, associated with mbe1, a version of mbe
     * ec-call1-raw, associated with ec-call1 (a variant of ec-call)
     * with-guard-checking1-raw, associated with with-guard-checking1 (a
     variant of with-guard-checking)

Note that because of its special status, it is illegal to trace
return-last.

We conclude by warning that as a user, you take responsibility for not
compromising the soundness or error handling of ACL2 when you define a
macro in raw Lisp and especially when you install it as a key of
return-last-table, either directly or (more likely) using
defmacro-last.  In particular, be sure that you are defining a macro of
two arguments that always returns the value of its last argument,
returning the complete multiple value if that last argument evaluates
to a multiple value.

The following is correct, and illustrates care taken to return multiple
values.

     :q
     (defmacro my-time1-raw (val form)
       (declare (ignore val))
       `(let  ((start-time (get-internal-run-time))
               (result (multiple-value-list ,form))
               (end-time (get-internal-run-time)))
          (format t "Total time: ~s~%"
                  (float (/ (- end-time start-time)
                            internal-time-units-per-second)))
          (values-list result)))
     (lp)
     (defttag t)
     (defmacro-last my-time1)
     (defmacro my-time (form)
       `(my-time1 nil ,form))

Then for example:

     ACL2 !>(my-time (equal (make-list 1000000) (make-list 1000000)))
     Total time: 0.12
     T
     ACL2 !>

But if instead we provide the following more naive implementation, of
the above raw Lisp macro, the above evaluation can produce an error,
for example if the host Lisp is CCL.

     (defmacro my-time1-raw (val form)
         (declare (ignore val))
         `(let  ((start-time (get-internal-run-time))
                 (result ,form)
                 (end-time (get-internal-run-time)))
            (format t "Total time: ~s~%"
                    (float (/ (- end-time start-time)
                              internal-time-units-per-second)))
            result)) ; WRONG -- need multiple values returned!

Here is a second, similar example.  This time we'll start with the
error; can you spot it?

     (defttag t)
     (progn!
      (set-raw-mode t)
      (defmacro foo-raw (x y)
        `(prog1
             ,y
           (cw "Message showing argument 1: ~x0~%" ,x))))
     (defmacro-last foo)

We then can wind up with a hard Lisp error:

     ACL2 !>(foo 3 (mv 4 5))
     Message showing argument 1: 3

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  value NIL is not of the expected type REAL.
     ***********************************************

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

     To enable breaks into the debugger (also see :DOC acl2-customization):
     (SET-DEBUGGER-ENABLE T)
     ACL2 !>

Here is a corrected version of the above macro.  The point here is that
prog1 returns a single value, while our-multiple-value-prog1 returns
all the values that are returned by its first argument.

     (progn!
      (set-raw-mode t)
      (defmacro foo-raw (x y)
        `(our-multiple-value-prog1 ;; better
          ,y
          (cw "Message showing argument 1: ~x0~%" ,x))))

REVAPPEND    concatentate the reverse of one list to another

(Revappend x y) concatenates the reverse of the list x to y, which is
also typically a list.

The following theorem characterizes this English description.

     (equal (revappend x y)
            (append (reverse x) y))

Hint:  This lemma follows immediately from the definition of reverse
and the following lemma.

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

The guard for (revappend x y) requires that x is a true list.

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

REVERSE    reverse a list or string

(Reverse x) is the result of reversing the order of the elements of the
list or string x.

The guard for reverse requires that its argument is a true list or a
string.

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

RFIX    coerce to a rational number

Rfix simply returns any rational number argument unchanged, returning 0
on a non-rational argument.  Also see NFIX, see IFIX,
see REALFIX, and see FIX for analogous functions that
coerce to a natural number, an integer, a real, and a number,
respectively.

Rfix has a guard of t.

ROUND    division returning an integer by rounding off

     Example Forms:
     ACL2 !>(round 14 3)
     5
     ACL2 !>(round -14 3)
     -5
     ACL2 !>(round 14 -3)
     -5
     ACL2 !>(round -14 -3)
     5
     ACL2 !>(round 13 3)
     4
     ACL2 !>(round -13 3)
     -4
     ACL2 !>(round 13 -3)
     -4
     ACL2 !>(round -13 -3)
     4
     ACL2 !>(round -15 -3)
     5
     ACL2 !>(round 15 -2)
     -8

(Round i j) is the result of taking the quotient of i and j and
rounding off to the nearest integer.  When the quotient is exactly
halfway between consecutive integers, it rounds to the even one.

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

Round is a Common Lisp function.  See any Common Lisp documentation for
more information.  However, note that unlike Common Lisp, the ACL2 round
function returns only a single value,

SEARCH    search for a string or list in another string or list

     Example Forms:
     (search "cd" "Cdabcdefcde")                   ; = 4, index of first match
     (search "cd" "Cdabcdefcde" :test 'equal)      ; same as above
     (search "cd" "Cdabcdefcde" :from-end t)       ; = 8, index of last match
     (search "cd" "Cdabcdefcde" :start1 1)         ; = 1
     (search "cd" "Cdabcdefcde" :start2 5)         ; = 8
     (search "cd" "Cdabcdefcde" :test 'char-equal) ; = 0 (case-insensitive)
     (search "ac" "Cdabcdefcde")                   ; = nil
     (search '(a b) '(9 8 a b 7 6))                    ; = 2

     General Form:
     (search seq1 seq2 &key from-end test start1 start2 end1 end2)

Search indicates whether one string or list occurs as a (contiguous)
subsequence of another string or list, respectively.  It returns nil if
no such match is found; otherwise it returns the (zero-based) index of
the first match by default, but a non-nil value of keyword argument
:from-end causes it to return the last match.  The :test is equal by
default.  The other legal value for :test is char-equal, which can be
given only for two strings, in which case the match is case-insensitive.
Finally, values of :start1 and :end1 for the first sequence, and of
:start2 and :end2 for the second sequence, bound the portion of the
respective sequence used for deciding on a match, though the index
returned is always an index into the second sequence as a whole.

The guard for calls of search is given by a function, search-fn-guard,
which has the following requirements.

     o The two arguments much both satisfy true-listp or else must both
     be strings, which must consist of standard characters (see
     STANDARD-CHAR-P) if the :test is char-equal.

     o The :test must evaluate to one of the symbols equal or
     char-equal, where the latter is only allowed if the (first) two
     arguments are strings.

     o The values of :start1, :start2, :end1, and :end2 must all be
     natural numbers, where if omitted they default to 0, 0, the length
     len1 of the first argument, and the length len2 of the second
     argument, respectively.

     o If start1 is the value of :start1, defaulting as described just
     above, and similarly for the other start and end keywords and for
     lengths len1 and len2 as described just above, then: start1 <=
     end1 <= len1 and start2 <= end2 <= len2.

Search is a Common Lisp function (actually, a macro in ACL2).  See any
Common Lisp documentation for more information.

SECOND    second member of the list

See any Common Lisp documentation for details.

SET-DIFFERENCE$    elements of one list that are not elements of another

     General Forms:
     (set-difference$ l1 l2)
     (set-difference$ l1 l2 :test 'eql)   ; same as above (eql as equality test)
     (set-difference$ l1 l2 :test 'eq)    ; same, but eq is equality test
     (set-difference$ l1 l2 :test 'equal) ; same, but equal is equality test

(Set-difference$ l1 l2) equals a list that contains the members of x
that are not members of y.  More precisely, the resulting list is the
same as one gets by deleting the members of y from x, leaving the
remaining elements in the same order as in x.  The optional keyword,
:TEST, has no effect logically, but provides the test (default eql)
used for comparing members of the two lists.

The guard for a call of set-difference$ 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
set-difference$ and its variants:

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

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

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

Set-difference$ is similar to the Common Lisp primitive set-difference.
However, Common Lisp does not specify the order of elements in the
result of a call of set-difference.

SET-DIFFERENCE-EQ    See SET-DIFFERENCE$.

SET-DIFFERENCE-EQUAL    See SET-DIFFERENCE$.

SETENV$    set an environment variable

(Setenv$ str val), where str and val are strings, sets the environment
variable str to have value val, for subsequent read by getenv$ (see
GETENV$), and returns nil.  Or, if this operation is not
implemented for the host Common Lisp, an error will occur.

     Example:
     (setenv$ "FOO" "BAR")

SEVENTH    seventh member of the list

See any Common Lisp documentation for details.

SIGNUM    indicator for positive, negative, or zero

(Signum x) is 0 if x is 0, -1 if x is negative, and is 1 otherwise.

The guard for signum requires its argument to be rational (real, in
ACL2(r)) number.

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

From "Common Lisp the Language" page 206, we see a definition of signum
in terms of abs.  As explained elsewhere (see ABS), the guard
for abs requires its argument to be a rational (real, in ACL2(r))
number; hence, we make the same restriction for signum.

SIXTH    sixth member of the list

See any Common Lisp documentation for details.

STANDARD-CHAR-LISTP    recognizer for a true list of standard characters

(standard-char-listp x) is true if and only if x is a null-terminated
list all of whose members are standard characters.  See
STANDARD-CHAR-P.

Standard-char-listp has a guard of t.

STANDARD-CHAR-P    recognizer for standard characters

(Standard-char-p x) is true if and only if x is a "standard" character,
i.e., a member of the list *standard-chars*.  This list includes
#Newline and #Space characters, as well as the usual punctuation and
alphanumeric characters.

Standard-char-p has a guard requiring its argument to be a character.

Standard-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

STANDARD-CO    the character output channel to which ld prints

Standard-co is an ld special (see LD).  The accessor is
(standard-co state) and the updater is (set-standard-co val state).
Standard-co must be an open character output channel.  It is to this
channel that ld prints the prompt, the form to be evaluated, and the
results.  The event commands such as defun, defthm, etc., which print
extensive commentary do not print to standard-co but rather to a
different channel, proofs-co, so that you may redirect this commentary
while still interacting via standard-co.  See PROOFS-CO.

"Standard-co" stands for "standard character output." The initial value
of standard-co is the same as the value of *standard-co* (see
*STANDARD-CO*).

STANDARD-OI    the standard object input "channel"

Standard-oi is an ld special (see LD).  The accessor is
(standard-oi state) and the updater is (set-standard-oi val state).
Standard-oi must be an open object input channel, a true list of
objects, or a list of objects whose last cdr is an open object input
channel.  It is from this source that ld takes the input forms to
process.  When ld is called, if the value specified for standard-oi is
a string or a list of objects whose last cdr is a string, then ld
treats the string as a file name and opens an object input channel from
that file, where the connected book directory (see CBD) is used
to resolve relative pathnames.  The channel opened by ld is closed by
ld upon termination.

"Standard-oi" stands for "standard object input." The read-eval-print
loop in ld reads the objects in standard-oi and treats them as forms to
be evaluated.  The initial value of standard-oi is the same as the
value of *standard-oi* (see *STANDARD-OI*).

STANDARD-STRING-ALISTP    recognizer for association lists with standard strings as keys

(Standard-string-alistp x) is true if and only if x is a list of pairs
of the form (cons key val) where key is a string all of whose
characters are standard (see STANDARD-CHAR-P).

Standard-string-alistp has a guard of t.

STRING    coerce to a string

(String x) coerces x to a string.  If x is already a string, then it is
returned unchanged; if x is a symbol, then its symbol-name is returned;
and if x is a character, the corresponding one-character string is
returned.

The guard for string requires its argument to be a string, a symbol, or
a character.

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

STRING-APPEND    concatenate two strings

String-append takes two arguments, which are both strings (if the guard
is to be met), and returns a string obtained by concatenating together
the characters in the first string followed by those in the second.
Also see CONCATENATE, noting that the macro call

     (concatenate 'string str1 str2).

expands to the call

     (string-append str1 str2).

STRING-DOWNCASE    in a given string, turn upper-case characters into lower-case

For a string x, (string-downcase x) is the result of applying
char-downcase to each character in x.

The guard for string-downcase requires its argument to be a string
containing only standard characters.

String-downcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

STRING-EQUAL    string equality without regard to case

For strings str1 and str2, (string-equal str1 str2) is true if and only
str1 and str2 are the same except perhaps for the cases of their
characters.

The guard on string-equal requires that its arguments are strings
consisting of standard characters (see STANDARD-CHAR-LISTP).

String-equal is a Common Lisp function.  See any Common Lisp
documentation for more information.

STRING-LISTP    recognizer for a true list of strings

The predicate string-listp tests whether its argument is a true-listp
of strings.

STRING-UPCASE    in a given string, turn lower-case characters into upper-case

For a string x, (string-upcase x) is the result of applying char-upcase
to each character in x.

The guard for string-upcase requires its argument to be a string
containing only standard characters.

String-upcase is a Common Lisp function.  See any Common Lisp
documentation for more information.

STRING<    less-than test for strings

(String< str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically, where character inequalities are
tested using char<.  When non-nil, (string< str1 str2) is the first
position (zero-based) at which the strings differ.  Here are some
examples.

     ACL2 !>(string< "abcd" "abu")
     2
     ACL2 !>(string< "abcd" "Abu")
     NIL
     ACL2 !>(string< "abc" "abcde")
     3
     ACL2 !>(string< "abcde" "abc")
     NIL

The guard for string< specifies that its arguments are strings.

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

STRING<=    less-than-or-equal test for strings

(String<= str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically or the strings are equal.  When
non-nil, (string<= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING<.

The guard for string<= specifies that its arguments are strings.

String<= is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRING>    greater-than test for strings

(String> str1 str2) is non-nil if and only if str2 precedes str1
lexicographically.  When non-nil, (string> str1 str2) is the first
position (zero-based) at which the strings differ.  See STRING<.

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

STRING>=    less-than-or-equal test for strings

(String>= str1 str2) is non-nil if and only if the string str2 precedes
the string str1 lexicographically or the strings are equal.  When
non-nil, (string>= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING>.

The guard for string>= specifies that its arguments are strings.

String>= is a Common Lisp function.  See any Common Lisp documentation
for more information.

STRINGP    recognizer for strings

(stringp x) is true if and only if x is a string.

STRIP-CARS    collect up all first components of pairs in a list

(strip-cars x) is the list obtained by walking through the list x and
collecting up all first components (cars).  This function is
implemented in a tail-recursive way, despite its logical definition.

(strip-cars x) has a guard of (alistp x).

STRIP-CDRS    collect up all second components of pairs in a list

(strip-cdrs x) has a guard of (alistp x), and returns the list obtained
by walking through the list x and collecting up all second components
(cdrs).  This function is implemented in a tail-recursive way, despite
its logical definition.

SUBLIS    substitute an alist into a tree

(Sublis alist tree) is obtained by replacing every leaf of tree with
the result of looking that leaf up in the association list alist.
However, a leaf is left unchanged if it is not found as a key in alist.

Leaves are looked up using the function assoc.  The guard for (sublis
alist tree) requires (eqlable-alistp alist).  This guard ensures that
the guard for assoc will be met for each lookup generated by sublis.

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

SUBSEQ    subsequence of a string or list

For any natural numbers start and end, where start <= end <= (length
seq), (subseq seq start end) is the subsequence of seq from index start
up to, but not including, index end.  End may be nil, which which case
it is treated as though it is (length seq), i.e., we obtain the
subsequence of seq from index start all the way to the end.

The guard for (subseq seq start end) is that seq is a true list or a
string, start and end are integers (except, end may be nil, in which
case it is treated as (length seq) for the rest of this discussion),
and 0 <= start <= end <= (length seq).

Subseq is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the third argument of
subseq is optional, but in ACL2 it is required, though it may be nil as
explained above.

SUBSETP    test if every member of one list is a member of the other

     General Forms:
     (subsetp x y)
     (subsetp x y :test 'eql)   ; same as above (eql as equality test)
     (subsetp x y :test 'eq)    ; same, but eq is equality test
     (subsetp x y :test 'equal) ; same, but equal is equality test

(Subsetp x y) is true if and only if every member of the list x is a
member of the list y.  The optional keyword, :TEST, has no effect
logically, but provides the test (default eql) used for comparing
members of the two lists.

The guard for a call of subsetp 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
subsetp and its variants:

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

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

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

Subsetp is defined by Common Lisp.  See any Common Lisp documentation
for more information.

SUBSETP-EQ    See SUBSETP.

SUBSETP-EQUAL    See SUBSETP.

SUBST    a single substitution into a tree

(Subst new old tree) is obtained by substituting new for every
occurence of old in the given tree.

Equality to old is determined using the function eql.  The guard for
(subst new old tree) requires (eqlablep old), which ensures that the
guard for eql will be met for each comparison generated by subst.

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

SUBSTITUTE    substitute into a string or a list, using eql as test

(Substitute new old seq) is the result of replacing each occurrence of
old in seq, which is a list or a string, with new.

The guard for substitute requires that either seq is a string and new
is a character, or else:  seq is a true-listp such that either all of
its members are eqlablep or old is eqlablep.

Substitute is a Common Lisp function.  See any Common Lisp
documentation for more information.  Since ACL2 functions cannot take
keyword arguments (though macros can), the test used in substitute is
eql.

SYMBOL-<    less-than test for symbols

(symbol-< x y) is non-nil if and only if either the symbol-name of the
symbol x lexicographially precedes the symbol-name of the symbol y (in
the sense of string<) or else the symbol-names are equal and the
symbol-package-name of x lexicographically precedes that of y (in the
same sense).  So for example, (symbol-< 'abcd 'abce) and (symbol-<
'acl2::abcd 'foo::abce) are true.

The guard for symbol specifies that its arguments are symbols.

SYMBOL-ALISTP    recognizer for association lists with symbols as keys

(Symbol-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a symbolp.

SYMBOL-LISTP    recognizer for a true list of symbols

The predicate symbol-listp tests whether its argument is a true list of
symbols.

SYMBOL-NAME    the name of a symbol (a string)

Completion Axiom (completion-of-symbol-name):

     (equal (symbol-name x)
            (if (symbolp x)
                (symbol-name x)
              ""))

Guard for (symbol-name x):

     (symbolp x)

SYMBOL-PACKAGE-NAME    the name of the package of a symbol (a string)

WARNING: While symbol-package-name behaves properly on all ACL2 objects,
it may give surprising results when called in raw Lisp.  More details
see PKG-IMPORTS, in particula the discussion there of the
"COMMON-LISP" package.

Completion Axiom (completion-of-symbol-package-name):

     (equal (symbol-package-name x)
            (if (symbolp x)
                (symbol-package-name x)
              ""))

Guard for (symbol-package-name x):

     (symbolp x)

Note:  If the ACL2 image is built on GCL, then symbol-package-name
diverges from the name of the symbol's package in raw Lisp, in the case
that this package is the main Lisp package.  For example,
(symbol-package-name 'car) evaluates to "COMMON-LISP" regardless of of
the underlying Lisp implementation, even though the name of the main
Lisp package in GCL is "LISP".

SYMBOLP    recognizer for symbols

(symbolp x) is true if and only if x is a symbol.

SYS-CALL    make a system call to the host operating system

     Example Forms:
     (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
     (prog2$ (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
             (sys-call-status state))

The first argument of sys-call is a command for the host operating
system, and the second argument is a list of strings that are the
arguments for that command.  In GCL and perhaps other lisps, you can
put the arguments with the command; but this is not the case, for
example, in Allegro CL running on Linux.

The use of prog2$ above is optional, but illustrates a typical sort of
use when one wishes to get the return status.  See
SYS-CALL-STATUS.

     General Form:
     (sys-call cmd args)

This function logically returns nil.  However, it makes the indicated
call to the host operating system, as described above, using a function
supplied "under the hood" by the underlying Lisp system.  On occasions
where one wishes to obtain the numeric status returned by the host
operating system (or more precisely, by the Lisp function under the
hood that passes the system call to the host operating system), one may
do so;  see SYS-CALL-STATUS.  The status value is the value
returned by that Lisp function, which may well be the same numeric
value returned by the host operating system for the underlying system
call.

Note that sys-call does not touch the ACL2 state; however,
sys-call-status updates the file-clock field of the state.  One may
view that update as modifying the fileclock to be at least as recent as
the time of the most recent sys-call.

Be careful if you use sys-call!  It can be used for example to overwrite
files, or worse!  We view a use of sys-call as a call to the operating
system that is made outside ACL2.  The following example from Bob Boyer
shows how to use sys-call to execute, in effect, arbitrary Lisp forms.
ACL2 provides a "trust tag" mechanism that requires execution of a
defttag form before you can use sys-call; see DEFTTAG.  (Note:
The setting of the raw Lisp variable *features* below is just to
illustrate that any such mischief is possible.  Normally *features* is
a list with more than a few elements.)

     % cat foo
     print *0x85d2064=0x838E920
     detach
     q
     % acl2
     ... boilerplate deleted
     ACL2 !>(sys-call "gdb -p $PPID -w < foo >& /dev/null " nil)
     NIL
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>*features*

     (:AKCL-SET-MV)

     ACL2>

Finally, we make a comment about output redirection, which also applies
to other related features that one may expect of a shell.  Sys-call
does not directly support output redirection.  If you want to run a
program, P, and redirect its output, we suggest that you create a
wrapper script, W to call instead.  Thus W might be a shell script
containing the line:

     P $* >& foo.out

If this sort of solution proves inadequate, please contact the ACL2
implementors and perhaps we can come up with a solution.

SYS-CALL-STATUS    exit status from the preceding system call

This function returns two values, (mv status state).  The first is the
status returned by the most recent invocation of function sys-call; see
SYS-CALL.  The second is the ACL2 state object, which is also
the input to this function.

The function sys-call makes a system call to the host operating system
using a function supplied "under the hood" by the underlying Lisp
system.  The status value is the value returned by that Lisp function,
which may well be the same numeric value returned by the host operating
system for the underlying system call.  For more information, see
SYS-CALL.

TAKE    initial segment of a list

For any natural number n not exceeding the length of l, (take n l)
collects the first n elements of the list l.

The following is a theorem (though it takes some effort, including
lemmas, to get ACL2 to prove it):

     (equal (length (take n l)) (nfix n))

If n is an integer greater than the length of l, then take pads the
list with the appropriate number of nil elements.  Thus, the following
is also a theorem.

     (implies (and (integerp n)
                   (true-listp l)
                   (<= (length l) n))
              (equal (take n l)
                     (append l (make-list (- n (length l))))))

For related functions, see NTHCDR and see BUTLAST.

The guard for (take n l) is that n is a nonnegative integer and l is a
true list.

TENTH    tenth member of the list

See any Common Lisp documentation for details.

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

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.

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.

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.

TYPE    See DECLARE.

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.

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

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.

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.

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

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

     General form:
     (with-live-state form)

where form is an arbitrary form that mentions state.

Most users will not need with-live-state.  If for some reason a form
that mentions the variable state might be executed in raw Lisp, outside
the ACL2 loop, then the use of with-live-state is recommended in order
to avoid potential warnings or (less likely) errors.

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

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

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.

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.

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 ACL2 "error triple," i.e., have 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

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

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

prettyprint the current term

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 rewrite rules

display the applicable type-prescription rules

``succeed'' without doing anything

simplify with lemmas

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||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 file
     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||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" 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||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||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!.