Major Section: PROOF-CHECKER

Example: (define-pc-help pp () (if (goals t) (io? proof-checker nil state (fms0 "~|~y0~|" (list (cons #0 (fetch-term (conc t) (current-addr t)))))) (print-all-goals-proved-message state)))This defines a macro command namedGeneral Form: (define-pc-help name args &rest body)

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

).

Major Section: PROOF-CHECKER

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.

Major Section: PROOF-CHECKER

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.

Major Section: 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`

.

Major Section: PROOF-CHECKER

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

More documentation will be written on the proof-checker. For now,
we simply point out that there are lots of examples of the use of
`define-pc-macro`

and `define-pc-atomic-macro`

in the ACL2 source file
`"proof-checker-b.lisp"`

. The former is used to create macro
commands, which can be submitted to the interactive loop
(see verify) and will ``expand'' into zero or more commands.
The latter is similar, except that the undoing mechanism
(see acl2-pc::undo) understands atomic macro commands to
represent single interactive commands. Also see acl2-pc::comm
and see acl2-pc::commands for a discussion of the display of
interactive commands.

Also see toggle-pc-macro for how to change a macro command to
an atomic macro command, and vice versa.

Major Section: 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`

.

### ACL2-PC::= -- (atomic macro)

### ACL2-PC::ACL2-WRAP -- (macro)

`(lisp x)`

### ACL2-PC::ADD-ABBREVIATION -- (primitive)

### ACL2-PC::BASH -- (atomic macro)

### ACL2-PC::BDD -- (atomic macro)

### ACL2-PC::BK -- (atomic macro)

### ACL2-PC::BOOKMARK -- (macro)

### ACL2-PC::CASESPLIT -- (primitive)

### ACL2-PC::CG -- (macro)

### ACL2-PC::CHANGE-GOAL -- (primitive)

### ACL2-PC::CLAIM -- (atomic macro)

### ACL2-PC::COMM -- (macro)

### ACL2-PC::COMMANDS -- (macro)

### ACL2-PC::COMMENT -- (primitive)

### ACL2-PC::CONTRADICT -- (macro)

`contrapose`

### ACL2-PC::CONTRAPOSE -- (primitive)

### ACL2-PC::DEMOTE -- (primitive)

### ACL2-PC::DIVE -- (primitive)

### ACL2-PC::DO-ALL -- (macro)

### ACL2-PC::DO-ALL-NO-PROMPT -- (macro)

### ACL2-PC::DO-STRICT -- (macro)

### ACL2-PC::DROP -- (primitive)

### ACL2-PC::DV -- (atomic macro)

### ACL2-PC::ELIM -- (atomic macro)

### ACL2-PC::EQUIV -- (primitive)

### ACL2-PC::EX -- (macro)

### ACL2-PC::EXIT -- (meta)

### ACL2-PC::EXPAND -- (primitive)

### ACL2-PC::FAIL -- (macro)

### ACL2-PC::FORWARDCHAIN -- (atomic macro)

### ACL2-PC::FREE -- (atomic macro)

### ACL2-PC::GENERALIZE -- (primitive)

### ACL2-PC::GOALS -- (macro)

### ACL2-PC::HELP -- (macro)

### ACL2-PC::HELP! -- (macro)

### ACL2-PC::HELP-LONG -- (macro)

`help!`

### ACL2-PC::HYPS -- (macro)

### ACL2-PC::ILLEGAL -- (macro)

### ACL2-PC::IN-THEORY -- (primitive)

### ACL2-PC::INDUCT -- (atomic macro)

### ACL2-PC::LISP -- (meta)

### ACL2-PC::MORE -- (macro)

### ACL2-PC::MORE! -- (macro)

### ACL2-PC::NEGATE -- (macro)

### ACL2-PC::NIL -- (macro)

`control-d`

### ACL2-PC::NOISE -- (meta)

### ACL2-PC::NX -- (atomic macro)

### ACL2-PC::ORELSE -- (macro)

### ACL2-PC::P -- (macro)

### ACL2-PC::P-TOP -- (macro)

### ACL2-PC::PP -- (macro)

### ACL2-PC::PRINT -- (macro)

### ACL2-PC::PRINT-ALL-GOALS -- (macro)

### ACL2-PC::PRINT-MAIN -- (macro)

### ACL2-PC::PRO -- (atomic macro)

### ACL2-PC::PROMOTE -- (primitive)

`implies`

term to top-level### ACL2-PC::PROTECT -- (macro)

### ACL2-PC::PROVE -- (primitive)

### ACL2-PC::PUT -- (macro)

### ACL2-PC::QUIET -- (meta)

### ACL2-PC::R -- (macro)

### ACL2-PC::REDUCE -- (atomic macro)

### ACL2-PC::REDUCE-BY-INDUCTION -- (macro)

### ACL2-PC::REMOVE-ABBREVIATIONS -- (primitive)

### ACL2-PC::REPEAT -- (macro)

### ACL2-PC::REPEAT-REC -- (macro)

`repeat`

### ACL2-PC::REPLAY -- (macro)

### ACL2-PC::RESTORE -- (meta)

### ACL2-PC::RETAIN -- (atomic macro)

**but**the indicated top-level hypotheses### ACL2-PC::RETRIEVE -- (macro)

### ACL2-PC::REWRITE -- (primitive)

### ACL2-PC::RUN-INSTR-ON-GOAL -- (macro)

### ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)

`then`

### ACL2-PC::S -- (primitive)

### ACL2-PC::S-PROP -- (atomic macro)

### ACL2-PC::SAVE -- (macro)

### ACL2-PC::SEQUENCE -- (meta)

### ACL2-PC::SHOW-ABBREVIATIONS -- (macro)

### ACL2-PC::SHOW-REWRITES -- (macro)

### ACL2-PC::SKIP -- (macro)

### ACL2-PC::SL -- (atomic macro)

### ACL2-PC::SPLIT -- (atomic macro)

### ACL2-PC::SR -- (macro)

### ACL2-PC::SUCCEED -- (macro)

### ACL2-PC::TH -- (macro)

### ACL2-PC::THEN -- (macro)

### ACL2-PC::TOP -- (atomic macro)

### ACL2-PC::TYPE-ALIST -- (macro)

### ACL2-PC::UNDO -- (meta)

### ACL2-PC::UNSAVE -- (macro)

### ACL2-PC::UP -- (primitive)

### ACL2-PC::USE -- (atomic macro)

### ACL2-PC::X -- (atomic macro)

### ACL2-PC::X-DUMB -- (atomic macro)

` `

attempt an equality (or equivalence) substitution
Major Section: PROOF-CHECKER-COMMANDS

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)If termsGeneral Form: (= &optional x y &rest keyword-args)

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

` `

same as `(lisp x)`

Major Section: PROOF-CHECKER-COMMANDS

Example: (acl2-wrap (pe :here))Same asGeneral Form: (acl2-wrap form)

`(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)`

.
` `

add an abbreviation
Major Section: PROOF-CHECKER-COMMANDS

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`

.

` `

call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS

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 hintsCall the theorem prover's simplifier, creating a subgoal for each resulting goal.General Form: (bash &rest hints)

Notice that unlike `prove`

, the arguments to `bash`

are spread out, and
are all hints.

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

` `

prove the current goal using bdds
Major Section: PROOF-CHECKER-COMMANDS

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.

` `

move backward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: bkFor 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`

.

` `

insert matching ``bookends'' comments
Major Section: PROOF-CHECKER-COMMANDS

Example: (bookmark final-goal)Run the instructions inGeneral Form: (bookmark name &rest instruction-list)

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

split into two cases
Major Section: PROOF-CHECKER-COMMANDS

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 hypothesisWhen the current subterm is the entire conclusion, this instruction addsGeneral Form: (casesplit expr &optional use-hyps-flag do-not-flatten-flag)

`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 `claim`

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

` `

change to another goal.
Major Section: PROOF-CHECKER-COMMANDS

Examples: (cg (main . 1)) -- change to the goal (main . 1) cg -- change to the next-to-top goalSame asGeneral Form: (CG &OPTIONAL goal-name)

`(change-goal goal-name t)`

, i.e. change to the indicated
and move the current goal to the end of the goal stack.
` `

change to another goal.
Major Section: PROOF-CHECKER-COMMANDS

Examples: (change-goal (main . 1)) -- change to the goal (main . 1) change-goal -- change to the next-to-top goalChange to the goal with the nameGeneral Form: (change-goal &optional goal-name end-flg)

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

.
` `

add a new hypothesis
Major Section: PROOF-CHECKER-COMMANDS

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 aboveThis command creates a new subgoal with the same top-level hypotheses as the current goal but with a conclusion ofGeneral Form: (claim expr &rest rest-args)

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

` `

display instructions from the current interactive session
Major Section: PROOF-CHECKER-COMMANDS

Examples: comm (comm 10)Prints out instructions in reverse order. This is actually the same asGeneral Form: (comm &optional n)

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

` `

display instructions from the current interactive session
Major Section: PROOF-CHECKER-COMMANDS

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.

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

).
` `

insert a comment
Major Section: PROOF-CHECKER-COMMANDS

Example: (comment now begin difficult final goal)This instruction makes no change in the state except to insert theGeneral Form: (comment &rest x)

`comment`

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

.

` `

same as `contrapose`

Major Section: PROOF-CHECKER-COMMANDS

see documentation for `contrapose`

` `

switch a hypothesis with the conclusion, negating both
Major Section: PROOF-CHECKER-COMMANDS

Example: (contrapose 3)The (optional) argumentGeneral Form: (contrapose &optional n)

`n`

should be a positive integer that does
not exceed the number of hypotheses. Negate the current conclusion
and make it the `n`

th hypothesis, while negating the current `n`

th
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)`

.

` `

move top-level hypotheses to the conclusion
Major Section: PROOF-CHECKER-COMMANDS

Examples: demote -- demote all top-level hypotheses (demote 3 5) -- demote hypotheses 3 and 5For 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.

` `

move to the indicated subterm
Major Section: PROOF-CHECKER-COMMANDS

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 thatFor 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`

.

` `

run the given instructions
Major Section: PROOF-CHECKER-COMMANDS

Example: (do-all induct p prove)Run the indicated instructions until there is a hard ``failure''. The instruction ``succeeds'' if and only if each instruction inGeneral Form: (do-all &rest instruction-list)

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

.

` `

run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER-COMMANDS

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`

.
` `

run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER-COMMANDS

Example: (do-strict induct p prove)Run the indicated instructions until there is a (hard or soft) ``failure''. In factGeneral Form: (do-strict &rest instruction-list)

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

.
` `

drop top-level hypotheses
Major Section: PROOF-CHECKER-COMMANDS

Examples: (drop 2 3) -- drop the second and third hypotheses drop -- drop all top-level hypothesesGeneral Forms: (drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.

drop -- Drop all the top-level hypotheses.

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

move to the indicated subterm
Major Section: PROOF-CHECKER-COMMANDS

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 thatFor 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`

.

` `

call the ACL2 theorem prover's elimination process
Major Section: PROOF-CHECKER-COMMANDS

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!

` `

attempt an equality (or congruence-based) substitution
Major Section: PROOF-CHECKER-COMMANDS

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 xSubstitute 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 isGeneral form: (equiv old new &optional relation)

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

` `

exit after possibly saving the state
Major Section: PROOF-CHECKER-COMMANDS

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.

` `

exit the interactive proof-checker
Major Section: PROOF-CHECKER-COMMANDS

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

exit -- Exit without storing an event.

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

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

` `

expand the current function call without simplification
Major Section: PROOF-CHECKER-COMMANDS

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 new-goals-flg keep-all-guards-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 expressionSee alsonew-goals-flg: default of nil means to introduce APPLY for guards

keep-all-guards-flg: default of nil means that the system should make a weak attempt to prove the guards from the current context

`x`

, which allows simplification.
` `

cause a failure
Major Section: PROOF-CHECKER-COMMANDS

Examples: fail (fail t)This is probably only of interest to writers of macro commands. The only function ofGeneral Form: (fail &optional hard)

`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-flag`

is not `nil`

. See also `do-strict`

, `do-all`

, and `sequence`

.

` `

forward chain from an implication in the hyps
Major Section: PROOF-CHECKER-COMMANDS

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`

.

` `

create a ``free variable''
Major Section: PROOF-CHECKER-COMMANDS

Example: (free x)MarkGeneral Form: (free var)

`var`

as a ``free variable''. Free variables are only of
interest for the `put`

command; see its documentation for an
explanation.
` `

perform a generalization
Major Section: PROOF-CHECKER-COMMANDS

Example: (generalize ((and (true-listp x) (true-listp y)) 0) ((append x y) w))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 formGeneral Form: (generalize &rest substitution)

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

` `

list the names of goals on the stack
Major Section: PROOF-CHECKER-COMMANDS

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.

` `

proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS

Examples:The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type(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!

(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)`

.

` `

proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS

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.

` `

same as `help!`

Major Section: PROOF-CHECKER-COMMANDS

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

` `

print the hypotheses
Major Section: PROOF-CHECKER-COMMANDS

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 governorsPrint the indicated top-level hypotheses and governors. (The notion of ``governors'' is defined below.) Here,General Form: (hyps &optional hyps-indices govs-indices)

`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 `cons`

ing `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 `cons`

ing `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 `n`

th 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`

).

` `

illegal instruction
Major Section: PROOF-CHECKER-COMMANDS

Example: (illegal -3)Probably not of interest to most users; always ``fails'' since it expands to theGeneral Form: (illegal instruction)

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

` `

set the current proof-checker theory
Major Section: PROOF-CHECKER-COMMANDS

Example: (in-theory (union-theories *s-prop-theory* '(true-listp binary-append)))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.General Form: (in-theory &optional atom-or-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. However, `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.

` `

generate subgoals using induction
Major Section: PROOF-CHECKER-COMMANDS

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 goalInduct as in the correspondingGeneral Form: (induct &optional term)

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

` `

evaluate the given form in Lisp
Major Section: PROOF-CHECKER-COMMANDS

Example: (lisp (assign xxx 3))EvaluateGeneral Form: (lisp form)

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

` `

proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS

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

.

Invoke `help`

for documentation about the proof-checker help
facility.

` `

proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS

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.

` `

run the given instructions, and ``succeed'' if and only if they ``fail''
Major Section: PROOF-CHECKER-COMMANDS

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

` `

used for interpreting `control-d`

Major Section: PROOF-CHECKER-COMMANDS

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.

` `

run instructions with output
Major Section: PROOF-CHECKER-COMMANDS

Example: (noise induct prove)Run theGeneral Form: (noise &rest instruction-list)

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

.

` `

move forward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: nxFor 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`

.

` `

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

second
Major Section: PROOF-CHECKER-COMMANDS

Example: (orelse top (print "Couldn't move to the top"))Run the first instruction. Then if it ``fails'', run the second instruction also; otherwise, stop after the first.General form: (orelse instr1 instr2)

This instruction ``succeeds'' if and only if either `instr1`

``succeeds'', or else `instr2`

``succeeds''. If it ``fails'', then
the failure is soft.

` `

prettyprint the current term
Major Section: PROOF-CHECKER-COMMANDS

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`

!).

` `

prettyprint the conclusion, highlighting the current term
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: p-topFor 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.

` `

prettyprint the current term
Major Section: PROOF-CHECKER-COMMANDS

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`

.

` `

print the result of evaluating the given form
Major Section: PROOF-CHECKER-COMMANDS

Example: (print (append '(a b) '(c d))) Print the list (a b c d) to the terminalPrettyprints the result of evaluating form. The evaluation ofGeneral Form: (print form)

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

.

` `

print all the (as yet unproved) goals
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: print-all-goals

Prints all the goals that remain to be proved, in a pleasant
format.

` `

print the original goal
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: print-main

Prints the goal as originally entered.

` `

repeatedly apply promote
Major Section: PROOF-CHECKER-COMMANDS

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.

` `

move antecedents of conclusion's `implies`

term to top-level
` `

hypotheses
Major Section: PROOF-CHECKER-COMMANDS

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`

.

` `

run the given instructions, reverting to existing state upon
` `

failure
Major Section: PROOF-CHECKER-COMMANDS

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`

.
` `

call the ACL2 theorem prover to prove the current goal
Major Section: PROOF-CHECKER-COMMANDS

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 setAttempt to prove the current goal, whereGeneral Form: (prove &rest rest-args)

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

` `

substitute for a ``free variable''
Major Section: PROOF-CHECKER-COMMANDS

Example: (put x 17)SubstituteGeneral Form: (put var expr)

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

` `

run instructions without output
Major Section: PROOF-CHECKER-COMMANDS

Example: (quiet induct prove)Run theGeneral Form: (quiet &rest instruction-list)

`instruction-list`

through the top-level loop with no output.` `

same as rewrite
Major Section: PROOF-CHECKER-COMMANDS

Example: (r 3)See the documentation forGeneral Form: (rewrite &optional rule-id substitution ;; below are rare arguments, used for disambiguation: target-lhs target-rhs target-hyps target-equiv)

`rewrite`

, as `r`

and `rewrite`

are identical.
` `

call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS

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 by without using induction, with the indicated hintsAttempt 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.General Form: (reduce &rest hints)

Notice that unlike `prove`

, the arguments to `reduce`

are spread out,
and are all hints.

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

` `

call the ACL2 prover without induction, after going into
` `

induction
Major Section: PROOF-CHECKER-COMMANDS

Examples: reduce-by-induction -- attempt to prove the current goal after going into induction, with no further inductionsA 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.(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)

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.

` `

remove one or more abbreviations
Major Section: PROOF-CHECKER-COMMANDS

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 termsIf vars is not empty (i.e., notGeneral Forms: (remove-abbreviations &rest vars)

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

.

` `

repeat the given instruction until it ``fails''
Major Section: PROOF-CHECKER-COMMANDS

Example: (repeat promote)The givenGeneral Form: (repeat instruction)

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

` `

auxiliary to `repeat`

Major Section: PROOF-CHECKER-COMMANDS

See documentation for `repeat`

.

` `

replay one or more instructions
Major Section: PROOF-CHECKER-COMMANDS

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 instructionsReplay the lastGeneral Form: (REPLAY &OPTIONAL n replacement-instruction)

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

` `

remove the effect of an UNDO command
Major Section: PROOF-CHECKER-COMMANDS

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

.

` `

drop all Major Section: PROOF-CHECKER-COMMANDS

Example: (RETAIN 2 3) -- keep the second and third hypotheses, and drop the restDrop all top-level hypothesesGeneral Form: (retain &rest args)

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

` `

re-enter the proof-checker
Major Section: PROOF-CHECKER-COMMANDS

Examples: (retrieve associativity-of-permutationp) retrieveMust be used fromGeneral Form: (retrieve &optional name)

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

.
` `

apply a rewrite rule
Major Section: PROOF-CHECKER-COMMANDS

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'' yReplace the current subterm with a new term by applying a rewrite rule. IfGeneral Form: (rewrite &optional rule-id substitution)

`rule-id`

is a positive integer `n`

, then the `n`

th 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. More explanation of all of these points follows 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.
A rather important point is that 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 above under
``General Form'' above. The ``disambiguating rare arguments'' will
rarely be of interest to the user; as explained just above, the
stored instruction always contains the name of the rewrite rule, so
if there is more than one rule of that name then the system creates
and stores these extra arguments in order to make the resulting
instruction unambiguous, i.e., so that only one rewrite rule
applies. For what it's worth, they correspond respectively to the
fields of a rewrite rule record named `lhs`

, `rhs`

, `hyps`

, and `equiv`

.

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 matching fails, then the
instruction fails.

Now an attempt is made to relieve the hypotheses, in much the same
sense as the theorem prover relieves hypotheses except that there is
no call to the rewriter. Essentially, this means that the
substitution `unify-subst`

is applied to the hypotheses and the system
then checks whether all hypotheses are ``clearly'' true in the
current context. If there are variables in the hypotheses of the
rewrite rule that do not occur in the left-hand side of the
conclusion even after the user-supplied substitution (default: `nil`

)
is applied, then a weak attempt is made to extend that substitution
so that even those hypotheses can be relieved. However, if even one
hypothesis remains unrelieved, then no automatic extension of the
substitution is made, and in fact hypotheses that contain even one
uninstantiated variable will remain unrelieved.

Finally, the instruction is applied as follows. The current subterm
is replaced by applying the final substitution, i.e., the extension
of `unify-subst`

by the user-supplied substitution which may in turn
be extended by the system (as explained above) in order to relieve
all hypotheses, 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.

` `

auxiliary toxae THEN
Major Section: PROOF-CHECKER-COMMANDS

See documentation for `then`

.

` `

auxiliary to `then`

Major Section: PROOF-CHECKER-COMMANDS

See documentation for `then`

.

` `

simplify the current subterm
Major Section: PROOF-CHECKER-COMMANDS

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 processSimplify the current subterm according to the keyword parameters supplied. First if-normalization is applied (unless theGeneral Form: (s &key rewrite normalize backchain-limit repeat in-theory hands-off expand)

`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 tWhen non-

`nil`

, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.
:normalize -- default tWhen non-

`nil`

, instructs the system to use if-normalization (as
described above) during simplification.
:backchain-limit -- default 0Sets 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 0Sets 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, :expandThese 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.

` `

simplify propositionally
Major Section: PROOF-CHECKER-COMMANDS

Example: s-propSimplify, using the default settings forGeneral Form: (s-prop &rest names)

`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 `*s-prop-theory*`

), together with the names (or parenthesized
names) in the `&rest`

argument `names`

, are enabled.
See also the documentation for `s`

.

` `

save the proof-checker state (state-stack)
Major Section: PROOF-CHECKER-COMMANDS

Example: (save lemma3-attemptSaves the current proof-checker state by ``associating'' it with the given name. SubmitGeneral Form: (save &optional name do-it-flg)

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

.

` `

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

options
Major Section: PROOF-CHECKER-COMMANDS

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

.

` `

display the current abbreviations
Major Section: PROOF-CHECKER-COMMANDS

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 abbreviationsSee 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`

.

` `

display the applicable rewrite rules
Major Section: PROOF-CHECKER-COMMANDS

Example: show-rewritesDisplay rewrite rules whose left-hand side matches the current subterm. This command is useful in conjunction withGeneral Form: (show-rewrites &optional rule-id enabled-only-flg)

`rewrite`

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

th 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, the
free variables of any rule (those occurring in the rule that do not
occur in the left-hand side of its conclusion) will be displayed.
See also the documentation for `rewrite`

.
` `

``succeed'' without doing anything
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: skip

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

.

` `

simplify with lemmas
Major Section: PROOF-CHECKER-COMMANDS

Examples: sl (sl 3)Simplify, but with all function definitions disabled (see function-theory in the top-level ACL2 loop), except for a few basic functions (the ones inGeneral Form: (sl &optional backchain-limit)

`*s-prop-theory*`

). If
`backchain-limit`

is supplied and not `nil`

, then it should be a
nonnegative integer; see `(help s)`

.
` `

split the current goal into cases
Major Section: PROOF-CHECKER-COMMANDS

Example: splitFor 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.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.General Form: 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 `*s-prop-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`

.

` `

same as SHOW-REWRITES
Major Section: PROOF-CHECKER-COMMANDS

Example: srSee the documentation forGeneral Form: (sr &optional rule-id)

`show-rewrites`

, as `sr`

and `show-rewrites`

are identical.
` `

run the given instructions, and ``succeed''
Major Section: PROOF-CHECKER-COMMANDS

Example: (succeed induct p prove)Run the indicated instructions until there is a hard ``failure'', and ``succeed''. (See the documentation forGeneral Form: (succeed &rest instruction-list)

`sequence`

for an
explanation of ``success'' and ``failure''.)
` `

print the top-level hypotheses and the current subterm
Major Section: PROOF-CHECKER-COMMANDS

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 subtermPrint hypotheses and the current subterm. The printing of hypotheses (and perhaps governors) are controlled as in theGeneral Form: (th &optional hyps-indices govs-indices)

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

` `

apply one instruction to current goal and another to new subgoals
Major Section: PROOF-CHECKER-COMMANDS

Example: (then induct prove)RunGeneral Form: (then first-instruction &optional completion must-succeed-flg)

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

move to the top of the goal
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: topFor 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`

.

` `

display the type-alist from the current context
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: type-alist

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

` `

undo some instructions
Major Section: PROOF-CHECKER-COMMANDS

Examples: (undo 7) undoGeneral Forms:

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

undo -- Same as (undo 1).

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

` `

remove a proof-checker state
Major Section: PROOF-CHECKER-COMMANDS

Example: (unsave assoc-of-append)Eliminates the association of a proof-checker state withGeneral Form: (unsave &optional name)

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

.

` `

move to the parent (or some ancestor) of the current subterm
Major Section: PROOF-CHECKER-COMMANDS

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 levelsMove upGeneral Form: (up &optional n)

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

.

` `

use a lemma instance
Major Section: PROOF-CHECKER-COMMANDS

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.Add the given lemma instances to the list of top-level hypotheses. See hints for the syntax ofGeneral Form: (use &rest args)

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

` `

expand and (maybe) simplify function call at the current subterm
Major Section: PROOF-CHECKER-COMMANDS

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))).Expand the function call at the current subterm, and simplify using the same conventions as with theGeneral Form: (X &key rewrite normalize backchain-limit in-theory hands-off expand)

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

.

` `

expand function call at the current subterm, without simplifying
Major Section: PROOF-CHECKER-COMMANDS

Example: x-dumb: expand without simplification.Same asGeneral Form: (x-dumb &optional new-goals-flg keep-all-guards-flg)

`(expand t new-goals-flg keep-all-guards-flg)`

. See
documentation for `expand`

.
See also `x`

, which allows simplification.