This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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||REPLAY    (macro)
replay one or more instructions

     Examples:
     REPLAY     -- replay all instructions in the current session
                   (i.e., state-stack)
     (REPLAY 5) -- replay the most recent 5 instructions
     (REPLAY 5
             (COMMENT deleted dive command here))
                -- replace the 5th most recent instruction with the
                   indicated comment instruction, and then replay it
                   followed by the remaining 4 instructions

     General Form:
     (REPLAY &OPTIONAL n replacement-instruction)

Replay the last n instructions if n is a positive integer; else n
should be nil or not supplied, and replay all instructions.  However,
if replacement-instruction is supplied and not nil, then before the
replay, replace the nth instruction (from the most recent, as shown by
commands) with replacement-instruction.

If this command "fails", then the restore command will revert the
state-stack to its value present before the replay instruction was
executed.

ACL2-PC||RESTORE    (meta)
remove the effect of an UNDO command

     Example and General Form:
     restore

Restore removes the effect of an undo command.  This always works as
expected if restore is invoked immediately after undo, without
intervening instructions.  However, other commands may also interact
with restore, notably "sequencing" commands such as do-all, do-strict,
protect, and more generally, sequence.

*Note:*  Another way to control the saving of proof-checker state is
with the save command; see the documentation for save.

The restore command always "succeeds"; it returns (mv nil t state).

ACL2-PC||RETAIN    (atomic macro)
drop all *but* the indicated top-level hypotheses

     Example:
     (RETAIN 2 3) -- keep the second and third hypotheses, and drop
                     the rest

     General Form:
     (retain &rest args)

Drop all top-level hypotheses *except* those with the indicated indices.

There must be at least one argument, and all must be in range (i.e.
integers between one and the number of top-level hypotheses, inclusive).

ACL2-PC||RETRIEVE    (macro)
re-enter the proof-checker

     Examples:
     (retrieve associativity-of-permutationp)
     retrieve

     General Form:
     (retrieve &optional name)

Must be used from outside the interactive proof-checker loop.  If name
is supplied and not nil, this causes re-entry to the interactive
proof-checker loop in the state at which save was last executed for the
indicated name.  (See documentation for save.)  If name is nil or is
not supplied, then the user is queried regarding which proof-checker
state to re-enter.  The query is omitted, however, if there only one
proof-checker state is present that was saved with save, in which case
that is the one that is used.  See also unsave.

ACL2-PC||REWRITE    (primitive)
apply a rewrite rule

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

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

Replace the current subterm with a new term by applying a rewrite rule.
The replacement will be done according to the information provided by
the show-rewrites (sr) command.

If rule-id is a positive integer n, then the nth rewrite rule as
displayed by show-rewrites is the one that is applied.  If rule-id is
nil or is not supplied, then it is treated as the number 1.  Otherwise,
rule-id should be either a rune of or name of a rewrite rule.  If a
name is supplied, then any rule of that name may be used.  We say more
about this, and describe the other optional arguments, below.

Consider first the following example.  Suppose that the current subterm
is (reverse (reverse y)) and that there is a rewrite rule called
reverse-reverse of the form

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

Then the instruction (rewrite reverse-reverse) would cause the current
subterm to be replaced by y and would create a new goal with conclusion
(true-listp y).  An exception is that if the top-level hypotheses imply
(true-listp y) using only "trivial reasoning" (more on this below),
then no new goal is created.

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

Speaking in general, then, a rewrite instruction works as follows:

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

Next, the left-hand side of the rule is matched with the current
subterm, i.e., a substitution unify-subst is found such that if one
instantiates the left-hand side of the rule with unify-subst, then one
obtains the current subterm.  If this match fails, then the instruction
fails.

Next, an attempt is made to relieve (discharge) the hypotheses, much as
the theorem prover relieves hypotheses except that there is no call to
the rewriter.  First, the substitution unify-subst is extended with the
substitution argument, which may bind free variables (see
FREE-VARIABLES).  Each hypothesis of the rewrite rule is then
considered in turn, from first to last.  For each hypothesis, first the
current substitution is applied, and then the system checks whether the
hypothesis is "clearly" true in the current context.  If there are
variables in the hypotheses of the rewrite rule that are not bound by
the current substitution, then a weak attempt is made to extend that
substitution so that the hypothesis is present in the current context
(see the documentation for the proof-checker hyps command under
proof-checker-commands), much as would be done by the theorem prover's
rewriter.

If in the process above there are free variables, but the proof-checker
can see how to bind them to relieve all hypotheses, then it will do so
in both the show-rewrites (sr) and rewrite commands.  But normally, if
even one hypothesis remains unrelieved, then no automatic extension of
the substitution is made.  Except, if instantiate-free is not nil, then
that extension to the substitution is kept.

Finally, the instruction is applied as follows.  The current subterm is
replaced by applying the final substitution described above to the
right-hand side of the selected rewrite rule.  And, one new subgoal is
created for each unrelieved hypothesis of the rule, whose top-level
hypotheses are the governors and top-level hypotheses of the current
goal and whose conclusion and current subterm are the instance, by that
same final substitution, of that unrelieved hypothesis.

*Note:*  The substitution argument should be a list whose elements have
the form (variable term), where term may contain abbreviations.

ACL2-PC||RUN-INSTR-ON-GOAL    (macro)
auxiliary to THEN

See documentation for then.

ACL2-PC||RUN-INSTR-ON-NEW-GOALS    (macro)
auxiliary to then

See documentation for then.

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

     Examples and general forms:
     (runes t)   ; print all runes used during this interactive proof
     (runes nil) ; print all runes used by the most recent command
     (runes)     ; same as (runes nil)
     runes       ; same as (runes nil)

This command does not change the proof-checker state.  Rather, it
simply reports runes (see RUNE) that have participated in the
interactive proof.

Note that (runes nil) will show the runes used by the most recent
primitive or macro command (as displayed by :comm).

ACL2-PC||S    (primitive)
simplify the current subterm

     Examples:
     S  -- simplify the current subterm
     (S :backchain-limit 2 :normalize t :expand (append x z))
        -- simplify the current subterm, but during the rewriting
           process first ``normalize'' it by pushing IFs to the
           top-level, and also force the term (append x z) to be
           expanded during the rewriting process

     General Form:
     (s &key rewrite normalize backchain-limit repeat in-theory hands-off
             expand)

Simplify the current subterm according to the keyword parameters
supplied.  First if-normalization is applied (unless the normalize
argument is nil), i.e., each subterm of the form (f ... (if test x y)
...)  is replaced by the term (if test (f ... x ...) (f ... y ...))
except, of course, when f is if and the indicated if subterm is in the
second or third argument position.  Then rewriting is applied (unless
the rewrite argument is nil).  Finally this pair of actions is repeated
-- until the rewriting step causes no change in the term.  A
description of each parameter follows.

     :rewrite -- default t

When non-nil, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.

     :normalize -- default t

When non-nil, instructs the system to use if-normalization (as
described above) during simplification.

     :backchain-limit -- default 0

Sets the number of recursive calls to the rewriter that are allowed for
backchaining.  Even with the default of 0, some reasoning is allowed
(technically speaking, type-set reasoning is allowed) in the relieving
of hypotheses.

     :repeat -- default 0

Sets the number of times the current term is to be rewritten.  If this
value is t, then the default is used (as specified by the constant
*default-s-repeat-limit*).

     :in-theory, :hands-off, :expand

These have their usual meaning; see HINTS.

*Note:*  if conditional rewrite rules are used that cause case splits
because of the use of force, then appropriate new subgoals will be
created, i.e., with the same current subterm (and address) but with
each new (forced) hypothesis being negated and then used to create a
corresponding new subgoal.  In that case, the current goal will have
all such new hypotheses added to the list of top-level hypotheses.

ACL2-PC||S-PROP    (atomic macro)
simplify propositionally

     Example:
     s-prop

     General Form:
     (s-prop &rest names)

Simplify, using the default settings for s (which include
if-normalization and rewriting without real backchaining), but with
respect to a theory in which only basic functions and rules (the ones in
(theory 'minimal-theory)), together with the names (or parenthesized
names) in the &rest argument names, are enabled.

See also the documentation for s.

ACL2-PC||SAVE    (macro)
save the proof-checker state (state-stack)

     Example:
     (save lemma3-attempt)

     General Form:
     (save &optional name do-it-flg)

Saves the current proof-checker state by "associating" it with the
given name.  Submit (retrieve name) to Lisp to get back to this
proof-checker state.  If verify was originally supplied with an event
name, then the argument can be omitted in favor of that name as the
default.

*Note* that if a save has already been done with the indicated name (or
the default event name), then the user will be queried regarding
whether to go ahead with the save -- except, if do-it-flg is supplied
and not nil, then there will be no query and the save will be effected.

See also the documentation for retrieve and unsave.

ACL2-PC||SEQUENCE    (meta)
run the given list of instructions according to a multitude of
options

     Example:
     (sequence (induct p prove) t)

See also the definitions of commands do-all, do-strict, protect, and
succeed.

     General Form:
     (sequence
      instruction-list
      &optional
      strict-flg protect-flg success-expr no-prompt-flg no-restore-flg)

Each instruction in the list instruction-list is run, and the
instruction "succeeds" if every instruction in instruction-list
"succeeds".  However, it might "succeed" even if some instructions in
the list "fail"; more generally, the various arguments control a number
of aspects of the running of the instructions.  All this is explained
in the paragraphs below.  First we embark on a general discussion of
the instruction interpreter, including the notions of "succeed" and
"fail".

*Note:*  The arguments are *not* evaluated, except (in a sense) for
success-expr, as described below.

Each primitive and meta instruction can be thought of as returning an
error triple (in the standard ACL2 sense), say (erp val state).  An
instruction (primitive or meta) "succeeds" if erp is nil and val is not
nil; otherwise it "fails".  (When we use the words "succeed" or "fail"
in this technical sense, we'll always include them in double quotes.)
If an instruction "fails," we say that that the failure is "soft" if
erp is nil; otherwise the failure is "hard".  The sequence command
gives the user control over how to treat "success" and "failure" when
sequencing instructions, though we have created a number of handy macro
commands for this purpose, notably do-all, do-strict and protect.

Here is precisely what happens when a sequence instruction is run.  The
instruction interpreter is run on the instructions supplied in the
argument instruction-list (in order).  The interpreter halts the first
time there is a hard "failure." except that if strict-flg is supplied
and not nil, then the interpreter halts the first time there is any
"failure."  The error triple (erp val state) returned by the sequence
instruction is the triple returned by the last instruction executed
(or, the triple (nil t state) if instruction-list is nil), except for
the following provision.  If success-expr is supplied and not nil, then
it is evaluated with the state global variables erp and val (in ACL2
package) bound to the corresponding components of the error triple
returned (as described above).  At least two values should be returned,
and the first two of these will be substituted for erp and val in the
triple finally returned by sequence.  For example, if success-expr is
(mv erp val), then no change will be made to the error triple, and if
instead it is (mv nil t), then the sequence instruction will "succeed".

That concludes the description of the error triple returned by a
sequence instruction, but it remains to explain the effects of the
arguments protect-flg and no-prompt-flg.

If protect-flg is supplied and not nil and if also the instruction
"fails" (i.e., the error component of the triple is not nil or the
value component is nil), then the state is reverted so that the
proof-checker's state (including the behavior of restore) is set back
to what it was before the sequence instruction was executed.
Otherwise, unless no-restore-flg is set, the state is changed so that
the restore command will now undo the effect of this sequence
instruction (even if there were nested calls to sequence).

Finally, as each instruction in instruction-list is executed, the
prompt and that instruction will be printed, unless the global state
variable print-prompt-and-instr-flg is unbound or nil and the parameter
no-prompt-flg is supplied and not nil.

ACL2-PC||SHOW-ABBREVIATIONS    (macro)
display the current abbreviations

     Examples:
     (show-abbreviations v w)
        -- assuming that v and w currently abbreviate terms,
           then this instruction displays them together with
           the terms they abbreviate
     show-abbreviations
        -- display all abbreviations

See also add-abbreviation and remove-abbreviations.  In particular, the
documentation for add-abbreviation contains a general discussion of
abbreviations.

     General Form:
     (show-abbreviations &rest vars)

Display each argument in vars together with the term it abbreviates (if
any).  If there are no arguments, i.e. the instruction is simply
show-abbreviations, then display all abbreviations together with the
terms they abbreviate.

If the term abbreviated by a variable, say v, contains a proper subterm
that is also abbreviate by (another) variable, then both the
unabbreviated term and the abbreviated term (but not using (? v) to
abbreviate the term) are displayed with together with v.

ACL2-PC||SHOW-REWRITES    (macro)
display the applicable rewrite rules

     Example:
     show-rewrites

     General Form:
     (show-rewrites &optional rule-id enabled-only-flg)

Display rewrite rules whose left-hand side matches the current subterm.
This command shows how the rewrite command can be applied.  If rule-id
is supplied and is a name (non-nil symbol) or a rune, then only the
corresponding rewrite rule(s) will be displayed, while if rule-id is a
positive integer n, then only the nth rule that would be in the list is
displayed.  In each case, the display will point out when a rule is
currently disabled (in the interactive environment), except that if
enabled-only-flg is supplied and not nil, then disabled rules will not
be displayed at all.  Finally, among the free variables of any rule
(those occurring in the rule that do not occur in the left-hand side of
its conclusion), those that would remain free if the rule were applied
will be displayed.  See also the documentation for rewrite.

ACL2-PC||SKIP    (macro)
``succeed'' without doing anything

     Example and General Form:
     skip

Make no change in the state-stack, but "succeed".  Same as (sequence
nil).

ACL2-PC||SL    (atomic macro)
simplify with lemmas

     Examples:
     sl
     (sl 3)

     General Form:
     (sl &optional backchain-limit)

Simplify, but with all function definitions disabled (see
FUNCTION-THEORY in the top-level ACL2 loop), except for a few basic
functions (the ones in (theory 'minimal-theory)).  The backchain-limit
has a default of 0, but if is supplied and not nil, then it should be a
nonnegative integer; see the documentation for s.

WARNING: This command completely ignores in-theory commands that are
executed inside the proof-checker.

ACL2-PC||SPLIT    (atomic macro)
split the current goal into cases

     Example:
     split

For example, if the current goal has one hypothesis (or x y) and a
conclusion of (and a b), then split will create four new goals:

     one with hypothesis X and conclusion A
     one with hypothesis X and conclusion B
     one with hypothesis Y and conclusion A
     one with hypothesis Y and conclusion B.

     General Form:
     SPLIT

Replace the current goal by subgoals whose conjunction is equivalent
(primarily by propositional reasoning) to the original goal, where each
such goal cannot be similarly split.

*Note:*  The new goals will all have their hypotheses promoted; in
particular, no conclusion will have a top function symbol of implies.
Also note that split will fail if there is exactly one new goal created
and it is the same as the existing current goal.

The way split really works is to call the ACL2 theorem prover with only
simplification (and preprocessing) turned on, and with only a few
built-in functions (especially, propositional ones) enabled, namely,
the ones in the list (theory 'minimal-theory).  However, because the
prover is called, type-set reasoning can be used to eliminate some
cases.  For example, if (true-listp x) is in the hypotheses, then
probably (true-listp (cdr x)) will be reduced to t.

ACL2-PC||SR    (macro)
same as SHOW-REWRITES

     Example:
     sr

     General Form:
     (sr &optional rule-id)

See the documentation for show-rewrites, as sr and show-rewrites are
identical.

ACL2-PC||SUCCEED    (macro)
run the given instructions, and ``succeed''

     Example:
     (succeed induct p prove)

     General Form:
     (succeed &rest instruction-list)

Run the indicated instructions until there is a hard "failure", and
"succeed".  (See the documentation for sequence for an explanation of
"success" and "failure".)

ACL2-PC||TH    (macro)
print the top-level hypotheses and the current subterm

     Examples:
     th               -- print all (top-level) hypotheses and the current
                         subterm
     (th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
                         and the current subterm
     (th (1 3) t)     -- print hypotheses 1 and 3 and all governors, and
                         the current subterm

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

Print hypotheses and the current subterm.  The printing of hypotheses
(and perhaps governors) are controlled as in the hyps command; see its
documentation.

Historical note:  The name th is adapted from the Gypsy Verification
Environment, where th abbreviates the command theorem, which says to
print information on the current goal.

ACL2-PC||THEN    (macro)
apply one instruction to current goal and another to new subgoals

     Example:
     (then induct prove)

     General Form:
     (then first-instruction &optional completion must-succeed-flg)

Run first-instruction, and then run completion (another instruction) on
each subgoal created by first-instruction.  If must-succeed-flg is
supplied and not nil, then immediately remove the effects of each
invocation of completion that "fails".

The default for completion is reduce.

ACL2-PC||TOP    (atomic macro)
move to the top of the goal

     Example and General Form:
     top

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

Top is the same as (up n), where n is the number of times one needs to
execute up in order to get to the top of the conclusion.  The top
command fails if one is already at the top of the conclusion.

See also up, dive, nx, and bk.

ACL2-PC||TYPE-ALIST    (macro)
display the type-alist from the current context

     Examples:
     (type-alist t t) ; display type-alist based on both conclusion and governors
     type-alist       ; same as (type-alist nil t) -- governors only
     (type-alist nil) ; same as (type-alist nil t) -- governors only
     (type-alist t)   ; same as (type-alist t nil) -- conclusion only
     (type-alist nil nil) ; display type-alist without considering
                          ; conclusion or governors

     General Form:
     (type-alist &optional concl-flg govs-flg)

where if govs-flg is omitted, it defaults to (not concl-flg).

Display the current assumptions as a type-alist.  Note that this
display includes the result of forward chaining.

There are two basic reasons contemplated for using this command.

1. The theorem prover has failed (either outside the proof-checker or
using a proof-checker command such as bash or reduce and you want to
debug by getting an idea of what the prover knows about the context.

     a. You really are interested in the context for the current term.
     Include hypotheses and governors (i.e., accounting for tests of
     surrounding if-expressions that must be true or false) but not the
     current conclusion (which the theorem prover's heuristics would
     generally ignore for contextual information).  Command:
     (type-alist nil t) ; equivalently, type-alist or (type-alist nil)

     b. You are not thinking in particular about the current term; you
     just want to get an idea of the context that the prover would
     build at the top-level, for forward-chaining.  Incorporate the
     conclusion but not the governors.  Command:
     (type-alist t nil) ; equivalently, (type-alist t)

2. You intend to use one of the proof-checker-commands that does
simplification, such as s or x, and you want to see the context.  Then
include the surrounding if-term governors but not the goal's
conclusion.  Command:
(type-alist nil t) ; equivalently, type-alist or (type-alist nil)

See TYPE-SET (also see TYPE-PRESCRIPTION) for
information about ACL2's type system, which can assist in understanding
the output of the type-alist command.

ACL2-PC||UNDO    (meta)
undo some instructions

     Examples:
     (undo 7)
     undo

     General Forms:

     (undo n) -- Undo the last n instructions.  The argument n should be
                 a positive integer.

     undo     -- Same as (undo 1).

*Note:*  To remove the effect of an undo command, use restore.  See the
documentation for details.

*Note:*  If the argument n is greater than the total number of
interactive instructions in the current session, then (undo n) will
simply take you back to the start of the session.

The undo meta command always "succeeds"; it returns (mv nil t state)
unless its optional argument is supplied and of the wrong type (i.e.
not a positive integer) or there are no instructions to undo.

ACL2-PC||UNSAVE    (macro)
remove a proof-checker state

     Example:
     (unsave assoc-of-append)

     General Form:
     (unsave &optional name)

Eliminates the association of a proof-checker state with name, if name
is supplied and not nil.  The name may be nil or not supplied, in which
case it defaults to the event name supplied with the original call to
verify (if there is one -- otherwise, the instruction "fails" and there
is no change).  The ACL2 function unsave may also be executed outside
the interactive loop, with the same syntax.

See also documentation for save and retrieve.

ACL2-PC||UP    (primitive)
move to the parent (or some ancestor) of the current subterm

     Examples:  if the conclusion is (= x (* (- y) z)) and the
                current subterm is y, then we have:
     up or (up 1) -- the current subterm becomes (- y)
     (up 2)       -- the current subterm becomes (* (- y) z)
     (up 3)       -- the current subterm becomes the entire conclusion
     (up 4)       -- no change; can't go up that many levels

     General Form:
     (up &optional n)

Move up n levels in the conclusion from the current subterm, where n is
a positive integer.  If n is not supplied or is nil, then move up 1
level, i.e., treat the instruction as (up 1).

See also dive, top, nx, and bk.

ACL2-PC||USE    (atomic macro)
use a lemma instance

     Example:
     (USE true-listp-append
          (:instance assoc-of-append (x a) (y b) (z c)))
     -- Add two top-level hypotheses, one the lemma called
        true-listp-append, and the other an instance of the lemma called
        assoc-of-append by the substitution in which x is assigned a, y
        is assigned b, and z is assigned c.

     General Form:
     (use &rest args)

Add the given lemma instances to the list of top-level hypotheses.  See
HINTS for the syntax of :use hints in defthm, which is
essentially the same as the syntax here (see the example above).

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

ACL2-PC||WRAP    (atomic macro)
execute the indicated instructions and combine all the new goals

     Example:
     (wrap induct) ; induct, then replace first new goal by the conjunction of all
                   ; the new goals, and drop all new goals after the first

     General Form:
     (wrap &rest instrs)

First the instructions in instrs are executed, as in do-all.  If this
"fails" then no additional action is taken.  Otherwise, the current goal
after execution of instrs is conjoined with all "new" goals, in the
sense that their names are not among the names of goals at the time
instrs was begun.  This conjunction becomes the new current goal and
those "new" goals are dropped.

See the code for the proof-checker command wrap-induct for an example
of the use of wrap.

ACL2-PC||WRAP-INDUCT    (atomic macro)
same as induct, but create a single goal

     Examples:
     wrap-induct
     (wrap-induct t)
     (wrap-induct (append (reverse x) y))

     General Form:
     (wrap-induct &optional term)

The wrap-induct command is identical to the proof-checker induct
command, except that only a single goal is created:  the conjunction of
the base and induction steps.

Note:  The output will generally indicate that more than goal has been
created, e.g.:

     Creating two new goals:  (MAIN . 1) and (MAIN . 2).

However, wrap-induct always creates a unique goal (when it succeeds).  A
subsequent message clarifies this, for example:

     NOTE: Created ONLY one new goal, which is the current goal:
       (MAIN . 1)

ACL2-PC||WRAP1    (primitive)
combine goals into a single goal

     Examples:
     ; Keep (main . 1) and (main . 2) if they exist, as well as the current goal;
     ; and for each other goal, conjoin it into the current goal and delete it:
     (wrap1 ((main . 1) (main . 2)))

     ; As explained below, conjoin all subsequent siblings of the current goal
     ; into the current goal, and then delete them:
     (wrap1)

     General Form:
     (wrap1 &optional kept-goal-names)

If kept-goal-names is not nil, the current goal is replaced by
conjoining it with all goals other than the current goal and those
indicated by kept-goal-names, and those other goals are deleted.  If
kept-goal-names is omitted, then the the current goal must be of the
form (name . n), and the goals to conjoin into the current goal (and
delete) are those with names of the form (name . k) for k >= n.

NOTE: Wrap1 always "succeeds", even if there are no other goals to
conjoin into the current goal (a message is printed in that case), and
it always leaves you with no hypotheses at the top of the current goal's
conclusion (as though top and demote had been executed, if necessary).

Also see proof-checker documentation for wrap (see
PROOF-CHECKER-COMMANDS).

ACL2-PC||X    (atomic macro)
expand and (maybe) simplify function call at the current subterm

     Examples:
     x --  expand and simplify.

For example, if the current subterm is (append a b), then after x the
current subterm will probably be (cons (car a) (append (cdr a) b)) if
(consp a) and (true-listp a) are among the top-level hypotheses and
governors.  If there are no top-level hypotheses and governors, then
after x the current subterm will probably be:

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

     General Form:
     (X &key
        rewrite normalize backchain-limit in-theory hands-off expand)

Expand the function call at the current subterm, and simplify using the
same conventions as with the s command (see documentation for s).

Unlike s, it is permitted to set both :rewrite and :normalize to nil,
which will result in no simplification; see x-dumb.

*Note* (obscure):  On rare occasions the current address may be
affected by the use of x.  For example, suppose we have the definition

     (defun g (x) (if (consp x) x 3))

and then we enter the proof-checker with

     (verify (if (integerp x) (equal (g x) 3) t)) .

Then after invoking the instruction (dive 2 1), so that the current
subterm is (g x), followed by the instruction x, we would expect the
conclusion to be (if (integerp x) (equal 3 3) t).  However, the system
actually replaces (equal 3 3) with t (because we use the ACL2
term-forming primitives), and hence the conclusion is actually (if
(integerp x) (equal 3 3) t).  Therefore, the current address is put at
(2) rather than (2 1).  In such cases, a warning "NOTE" will be printed
to the terminal.

The other primitive commands to which the above "truncation" note
applies are equiv, rewrite, and s.

ACL2-PC||X-DUMB    (atomic macro)
expand function call at the current subterm, without simplifying

     General Form:
     x-dumb:  expand without simplification.

Same as (expand t new-goals-flg keep-all-guards-flg).  See
documentation for expand.

See also x, which allows simplification.

RETRIEVE    re-enter a (specified) proof-checker state

     Examples:
     (retrieve associativity-of-permutationp)
     retrieve

     General Form:
     (retrieve &optional name)

See ACL2-PC||RETRIEVE, or use (help retrieve) inside the
interactive proof-checker loop.  Also see UNSAVE.

TOGGLE-PC-MACRO    change an ordinary macro command to an atomic macro, or vice-versa

     Example:
     (toggle-pc-macro pro)

Change pro from an atomic macro command to an ordinary one (or
vice-versa, if pro happens to be an ordinary macro command)

     General Form:
     (toggle-pc-macro name &optional new-tp)

If name is an atomic macro command then this turns it into an ordinary
one, and vice-versa.  However, if new-tp is supplied and not nil, then
it should be the new type (the symbol macro or atomic-macro, in any
package), or else there is no change.

UNSAVE    remove a proof-checker state

     Example:
     (unsave assoc-of-append)

     General Form:
     (unsave name)

Eliminates the association of a proof-checker state with name.  See
UNSAVE or see ACL2-PC||UNSAVE.

Also see ACL2-PC||SAVE and see RETRIEVE.

VERIFY    enter the interactive proof checker

For proof-checker command summaries, see PROOF-CHECKER.

     Examples:
     (VERIFY (implies (and (true-listp x) (true-listp y))
                           (equal (append (append x y) z)
                                  (append x (append y z)))))
        -- Attempt to prove the given term interactively.

     (VERIFY (p x)
             :event-name p-always-holds
             :rule-classes (:rewrite :generalize)
             :instructions ((rewrite p-always-holds-lemma)
                            change-goal))
        -- Attempt to prove (p x), where the intention is to call the
           resulting DEFTHM event by the name p-always-holds, with
           rule-classes as indicated.  The two indicated instructions
           will be run immediately to start the proof.

     (VERIFY)
        -- Re-enter the proof-checker in the state at which is was last
           left.

     General Form:
     (VERIFY &OPTIONAL raw-term
             &KEY
             event-name
             rule-classes
             instructions)

Verify is the function used for entering the proof-checker's
interactive loop.

PROOF-TREE    proof tree displays

A view of ACL2 proofs may be obtained by way of "proof tree displays."
The emacs environment is easily customized to provide window-based
proof tree displays that assist in traversing and making sense of the
proof transcript; see PROOF-TREE-EMACS.  Proof tree displays
may be turned on with the command :start-proof-tree and may be turned
off with the command :stop-proof-tree; see START-PROOF-TREE and
see STOP-PROOF-TREE.

Here is an example of a proof tree display, with comments.  Lines
marked with "c" are considered "checkpoints," i.e., goals whose
scrutiny may be of particular value.

     ( DEFTHM PLUS-TREE-DEL ...)    ;currently proving PLUS-TREE-DEL
        1 Goal preprocess   ;"Goal" creates 1 subgoal by preprocessing
        2 |  Goal' simp     ;"Goal'" creates 2 subgoals by simplification
     c  0 |  |  Subgoal 2 PUSH *1   ;"Subgoal 2" pushes "*1" for INDUCT
     ++++++++++++++++++++++++++++++ ;first pass thru waterfall completed
     c  6 *1 INDUCT                 ;Proof by induction of "*1" has
          |  <5 more subgoals>      ; created 6 top-level subgoals.  At
                                    ; this point, one of those 6 has been
                                    ; proved, and 5 remain to be proved.
                                    ; We are currently working on the
                                    ; first of those 5 remaining goals.

See PROOF-TREE-EXAMPLES for many examples that contain proof
tree displays.  But first, we summarize the kinds of lines that may
appear in a proof tree display.  The simplest form of a proof tree
display is a header showing the current event, followed by list of
lines, each having one of the following forms.

         n <goal> <process> ...

Says that the indicated goal created n subgoals using the indicated
process.  Here "..." refers to possible additional information.

     c   n <goal> <process> ...

As above, but calls attention to the fact that this goal is a
"checkpoint" in the sense that it may be of particular interest.  Some
displays may overwrite "c" with ">" to indicate the current checkpoint
being shown in the proof transcript.

          |  <goal> ...
          |  |  <k subgoals>

Indicates that the goal just above this line, which is pointed to by the
rightmost vertical bar ("|"), has k subgoals, none of which have yet
been processed.

          |  <goal> ...
          |  |  <k more subgoals>

As above, except that some subgoals have already been processed.

     ++++++++++++++++++++++++++++++

Separates successive passes through the "waterfall".  Thus, this
"fencepost" mark indicates the start of a new proof by induction or of a
new forcing round.

See PROOF-TREE-EXAMPLES for detailed examples.  To learn how to
turn off proof tree displays or to turn them back on again, see
STOP-PROOF-TREE and see START-PROOF-TREE, respectively. See
CHECKPOINT-FORCED-GOALS to learn how to mark goals as
checkpoints that force the creation of goals in forcing rounds.
Finally, see PROOF-TREE-DETAILS for some points not covered
elsewhere.

CHECKPOINT-FORCED-GOALS    Cause forcing goals to be checkpointed in proof trees

     Example forms:
     (checkpoint-forced-goals t)
     (checkpoint-forced-goals nil)

Also see PROOF-TREE.

By default, goals are not marked as checkpoints by a proof tree display
(as described elsewhere; see PROOF-TREE) merely because they
force some hypotheses, thus possibly contributing to a forcing round.
However, some users may want such behavior, which will occur once the
command (checkpoint-forced-goals t) has been executed.  To return to the
default behavior, use the command (checkpoint-forced-goals nil).

PROOF-TREE-DETAILS    proof tree details not covered elsewhere

See PROOF-TREE for an introduction to proof trees, and for a
list of related topics.  Here we present some details not covered
elsewhere.

1.  When proof tree display is enabled (because the command
:stop-proof-tree has not been executed, or has been superseded by a
later :start-proof-tree command), then time summaries will include the
time for proof tree display.  This time includes the time spent
computing with proof trees, such as the pruning process described
briefly above.  Even when proof trees are not displayed, such as when
their display is turned off in the middle of a proof, this time will be
printed if it is not 0.

2.  When a goal is given a :bye in a proof (see HINTS), it is
treated for the purpose of proof tree display just as though it had
been proved.

3.  Several state global variables affect proof tree display.  (@
proof-tree-indent) is initially the string "| ":  it is the string that
is laid down the appropriate number of times to effect indentation.  (@
proof-tree-buffer-width) is initially the value of
(fmt-soft-right-margin state), and is used to prevent printing of the
annotation "(forced ...)" in any greater column than this value.
However, (assign proof-tree-buffer-width nil) to avoid any such
suppression.  Finally, (@ checkpoint-processors) is a list of processors
from the constant list *preprocess-clause-ledge*, together with
:induct.  You may remove elements of (@ checkpoint-processors) to limit
which processes are considered checkpoints, but note that this can
affect what is printed by gag-mode (see SET-GAG-MODE).

4.  When :otf-flg is not set to t in a proof, and the prover then
decides to revert to the original goal and prove it by induction, the
proof tree display will reflect this fact as shown here:

     c  0 |  |  Subgoal 2 PUSH (reverting)

5. The usual failure message is printed as part of the prooftree display
when a proof has failed.

PROOF-TREE-EMACS    using emacs with proof trees

Within emacs, proof trees provide a sort of structure for the linear
proof transcript output by the ACL2 prover.  Below we explain how to
get proof trees set up in your emacs environment.

To get started, it suffices to load the distributed ACL2 emacs file,
which has lots more than just proof tree support (documented near the
top of that file), as follows.  Thus, you can put the following form in
your ~/.emacs file, where DIR refers to your ACL2 source directory
(typically called acl2-sources/).

     (load "DIR/emacs/emacs-acl2.el")

Then you can start the proof tree display by issuing the following emacs
command:  M-x start-proof-tree.

If you prefer not to load the ACL2 emacs file as shown above, you can
instead put the following forms in your ~/.emacs file (where DIR is as
above) and then issue the above M-x command.

     (setq *acl2-interface-dir*
           "DIR/interface/emacs/")

     (autoload 'start-proof-tree
       (concat *acl2-interface-dir* "top-start-shell-acl2")
       "Enable proof tree logging in a prooftree buffer."
       t)

Once the above is taken care of, then to start using proof trees you do
two things.  In emacs, start a shell (meta-x shell) and evaluate:

        M-x start-proof-tree

Also, in your ACL2, evaluate

       :start-proof-tree

If you want to turn off proof trees, evaluate this in emacs

        M-x stop-proof-tree

and evaluate this in your ACL2 session:

       :stop-proof-tree

When you do M-x start-proof-tree for the first time in your emacs
session, you will be prompted for some information.  You can avoid the
prompt by putting the following in your .emacs file.  The defaults are
as shown, but you can of course change them.

       (setq *acl2-proof-tree-height* 17)
       (setq *checkpoint-recenter-line* 3)
       (setq *mfm-buffer* "*shell*")

Alternatively, you can put the following in your ~/.emacs file in order
to start proof trees without any queries.

       (start-proof-tree-noninteractive "*shell*")

Once you start proof trees (meta-x start-proof-tree), you will have
defined the key bindings shown by executing C-z h in emacs.  Also see
PROOF-TREE-BINDINGS for that additional documentation.

If you want proof-trees to be displayed in a separate emacs frame to the
side, then you can put the following forms in your .emacs file above the
load of emacs-acl2.el described above.  But you may wish to edit the
second form, in particular the number 2048.

     (start-proof-tree-noninteractive "*shell*")
     (cond ((and (eq window-system 'x)
                 (fboundp 'x-display-pixel-width)
                 (= (x-display-pixel-width) 2048) ; for a wide monitor
                 )
            (delete-other-windows)
            (if (boundp 'emacs-startup-hook) ; false in xemacs
                (push 'new-prooftree-frame emacs-startup-hook))))

The file interface/emacs/README-mouse.doc discusses an extension of ACL2
proof trees that allows the mouse to be used with menus.  That
extension may well work, but it is no longer supported.  The basic
proof tree interface, however, is supported and is what is described in
detail elsewhere; see PROOF-TREE.  Thanks to Mike Smith for his
major role in providing emacs support for proof trees.