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.

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.

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

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

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

*Note:* 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 print-prompt-and-instr-flg
is nil.

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

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

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

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

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.

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

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

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

To summarize: 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 ACL2 logical world,
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.

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

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

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

*Note* (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 Form:
     (print form)

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

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.

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

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

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

Print the most recent proof attempt from inside the proof-checker,
assuming that you haven't left the proof-checker loop and subsequently
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 if it failed.

See documentation for the similar proof-checker command pso! for
including proof-tree output.  Also see SET-SAVED-OUTPUT for a
general discussion of the output-saving mechanism.

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 that you haven't left the
proof-checker loop and subsequently 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 documentation for the similar proof-checker command pso for
inhibiting proof-tree output.  Also see SET-SAVED-OUTPUT for a
general discussion of the output-saving mechanism.

ACL2-PC||PUT    (macro)
substitute for a "free variable"

     Example:
     (put x 17)

     General Form:
     (put var expr)

Substitute expr for the "free variable" var, as explained below.

A "free variable" is, for our purposes, a variable var such that the
instruction (free var) has been executed earlier in the state-stack.
What (free var) really does is to let var be an abbreviation for the
term (hide var) (see documentation for add-abbreviation).  What (put var
expr) really does is to unwind the state-stack, replacing that free
instruction with the instruction (add-abbreviation var expr), so that
future references to (? var) become reference to expr rather than to
(hide var), and then to replay all the other instructions that were
unwound.  Because hide was used, the expectation is that in most cases,
the instructions will replay successfully and put will "succeed".
However, if any replayed instruction "fails", then the entire replay
will abort and "fail", and the state-stack will revert to its value
before the put instruction was executed.

If (put var expr) "succeeds", then (remove-abbreviation var) will be
executed at the end.

*Note*: The restore command will revert the state-stack to its value
present before the put instruction was executed.

ACL2-PC||QUIET    (meta)
run instructions without output

     Example:
     (quiet induct prove)

     General Form:
     (quiet &rest instruction-list)

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

See also noise.

ACL2-PC||R    (macro)
same as rewrite

     Example:
     (r 3)

     General Form:
     (rewrite &optional rule-id substitution
              ;; below are rare arguments, used for disambiguation:
              target-lhs target-rhs target-hyps target-equiv)

See the documentation for rewrite, as r and rewrite are identical.

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

     Examples:
     reduce -- attempt to prove the current goal without using induction
     (reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
            -- attempt to prove the current goal without using
               induction, with the indicated hints

     General Form:
     (reduce &rest hints)

Attempt to prove the current goal without using induction, using the
indicated hints (if any).  A subgoal will be created for each goal that
would have been pushed for proof by induction in an ordinary proof.

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

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

*Note:* Induction will be used to the extent that it is ordered
explicitly in the hints.

ACL2-PC||REDUCE-BY-INDUCTION    (macro)
call the ACL2 prover without induction, after going into
induction

     Examples:
     reduce-by-induction
       -- attempt to prove the current goal after going into induction,
          with no further inductions

     (reduce-by-induction ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
       -- attempt to prove the current goal after going into induction,
          with no further inductions, using the indicated hints

     General Form:
     (reduce-by-induction &rest hints)

A subgoal will be created for each goal that would have been pushed for
proof by induction in an ordinary proof, except that the proof begins
with a top-level induction.

Notice that unlike prove, the arguments to reduce-by-induction are
spread out, and are all hints.  See also prove, reduce, and bash.

*Note*: Induction and the various processes will be used to the extent
that they are ordered explicitly in the :induct and :do-not hints.

ACL2-PC||REMOVE-ABBREVIATIONS    (primitive)
remove one or more abbreviations

     Examples:
     remove-abbreviations -- remove all abbreviations
     (remove-abbreviations v w)
                          -- assuming that V and W currently abbreviate
                             terms, then they are "removed" in the
                             sense that they are no longer considered to
                             abbreviate those terms

     General Forms:
     (remove-abbreviations &rest vars)

If vars is not empty (i.e., not nil), remove the variables in vars from
the current list of abbreviations, in the sense that each variable in
vars will no longer abbreviate a term.

*Note:* The instruction fails if at least one of the arguments fails to
be a variable that abbreviates a term.

See also the documentation for add-abbreviation, which contains a
discussion of abbreviations in general, and show-abbreviations.

ACL2-PC||REPEAT    (macro)
repeat the given instruction until it "fails"

     Example:
     (repeat promote)

     General Form:
     (repeat instruction)

The given instruction is run repeatedly until it "fails".

*Note:* There is nothing here in general to prevent the instruction from
being run after all goals have been proved, though this is indeed the
case for primitive instructions.