This is documentation for ACL2 Version 3.0
Copyright (C) 2006  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.

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

(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,

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)
     (COMPLEX RATIONAL)          (RATIONALP (REALPART X))
                                 (RATIONALP (IMAGPART X)))
     (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)
     SIGNED-BYTE            (INTEGERP X)
     (SIGNED-BYTE i)        same as (INTEGER -2**i-1 (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:

     (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:

     (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-EQ    union of two lists of symbols

(Union-eq x y) equals a list whose members (see MEMBER-EQ)
contains 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 guard for union-eq requires both arguments to be true lists, but in
fact further requires the first list to contain only symbols, as the
function member-eq is used to test membership (with eq).  See
UNION-EQUAL.

UNION-EQUAL    union of two lists

(Union-equal x y) equals a list whose members (see MEMBER-EQUAL)
contains 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 guard for union-equal requires both arguments to be true lists.
Essentially, union-equal has the same functionality as the Common Lisp
function union, except that it uses the equal function to test
membership rather than eql.  However, we do not include the function
union in ACL2, because the Common Lisp language does not specify the
order of the elements in the list that it returns.

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.

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 28) 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 theorems in ACL2.  One enters
it using VERIFY; see VERIFY.  The result of an interactive
session is a defthm event with an :instructions parameter supplied; see
the documentation for proof-checker command exit (in package "ACL2-PC").
Such an event can be replayed later in a new ACL2 session with the
"proof-checker" loaded.

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

Individual proof-checker commands are documented in subsection
proof-checker-commands.

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

     Example:
     :instructions (induct prove promote (dive 1) x
                           (dive 2) = top (drop 2) prove)

See DEFTHM for the role of :instructions in place of :hints.  As
illustrated by the example above, the value associated with
:instructions is a list of proof-checker commands.  At the moment the
best way to understand the idea of the interactive proof-checker (see
PROOF-CHECKER and see VERIFY) is probably to read the
first 11 pages of CLI Technical Report 19, which describes the
corresponding facility for Nqthm.

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

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

add a new hypothesis

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

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

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

"succeed" without doing anything

simplify with lemmas

split the current goal into cases

same as SHOW-REWRITES

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.

*Notes:* (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.

*Note:* 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 by the next release).

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.

*Note:*  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||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.

*Notes:* (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||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 ...) .