` `

auxiliary toxae THEN
Major Section: PROOF-CHECKER

See documentation for `then`

.

` `

auxiliary to `then`

Major Section: PROOF-CHECKER

See documentation for `then`

.

` `

simplify the current subterm
Major Section: PROOF-CHECKER

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

Examples: (retrieve associativity-of-permutationp) retrieveSee acl2-pc::retrieve, or useGeneral Form: (retrieve &optional name)

`(help retrieve)`

inside the
interactive proof-checker loop. Also see unsave.
Major Section: PROOF-CHECKER

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, or else there is no change.
Major Section: PROOF-CHECKER

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

`name`

.
See unsave or see acl2-pc::unsave.
Also see acl2-pc::save and see retrieve.

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