Major Section: OTHER

Examples: (set-inhibit-output-lst '(warning)) (set-inhibit-output-lst '(proof-tree prove)) :set-inhibit-output-lst (proof-tree prove)whereGeneral Form: (set-inhibit-output-lst lst)

`lst`

is a form (which may mention `state`

) that evaluates
to a list of names, each of which is the name of one of the
following ``kinds'' of output produced by ACL2.
error error messages warning warnings observation observations prove commentary produced by the theorem prover event non-proof commentary produced by events such as defun and encapsulate summary the summary at the successful conclusion of an event proof-tree proof-tree outputIt is possible to inhibit each kind of output by putting the corresponding name into

`lst`

. For example, if `'warning`

is
included in (the value of) `lst`

, then no warnings are printed.
Note that proof-tree output is affected by
`set-inhibit-output-lst`

; see proof-tree.
Major Section: OTHER

Example Form: (skip-proofs (defun foo (x) (if (atom x) nil (cons (car x) (foo (reverse (cdr x)))))))whereGeneral Form: (skip-proofs event)

`event`

is an event; see events. `Event`

is processed
as usual except that the proof obligations usually generated are
merely assumed.WARNING: Skip-proofs allows inconsistent events to be admitted to the logic. Use it at your own risk!

Sometimes in the development of a formal model or proof it is
convenient to skip the proofs required by a given event. By
embedding the event in a `skip-proofs`

form, you can avoid the
proof burdens generated by the event, at the risk of introducing
unsoundness. Below we list three illustrative situations in which
you might find `skip-proofs`

useful.

1. The termination argument for a proposed function definition is
complicated. You presume you could admit it, but are not sure that
your definition has the desired properties. By embedding the
`defun`

event in a `skip-proofs`

you can ``admit'' the function
and experiment with theorems about it before you pay the price of
its admission.

2. You intend eventually to verify the guards for a definition but
do not want to take the time now to pursue that. By embedding the
`verify-guards`

event in a `skip-proofs`

you can get the system to
behave as though the guards were verified.

3. You are repeatedly recertifying a book while making many
experimental changes. A certain `defthm`

in the book takes a very
long time to prove and you believe the proof is not affected by the
changes you are making. By embedding the `defthm`

event in a
`skip-proofs`

you allow the theorem to be assumed without proof
during the experimental recertifications.

Unsoundness or Lisp errors may result if the presumptions underlying
a use of `skip-proofs`

are incorrect. Therefore, `skip-proofs`

must be considered a dangerous (though useful) tool in system
development.

Roughly speaking, a `defthm`

embedded in a `skip-proofs`

is
essentially a `defaxiom`

, except that it is not noted as an axiom
for the purposes of functional instantiation
(see lemma-instance). But a skipped `defun`

is much more
subtle since not only is the definitional equation being assumed but
so are formulas relating to termination and type. The situation is
also difficult to characterize if the `skip-proofs`

events are
within the scope of an `encapsulate`

in which constrained functions
are being introduced. In such contexts no clear logical story is
maintained; in particular, constraints aren't properly tracked for
definitions. A proof script involving `skip-proofs`

should be
regarded as work-in-progress, not as a completed proof with some
unproved assumptions. A `skip-proofs`

event represents a promise
by the author to admit the given event without further axioms.

ACL2 allows the certification of books containing `skip-proofs`

events. This is contrary to the spirit of certified books, since
one is supposedly assured by a valid certificate that a book has
been ``blessed.'' But certification, too, takes the view of
`skip-proofs`

as ``work-in-progress'' and so allows the author of
the book to promise to finish. When such books are certified, a
warning to the author is printed, reminding him or her of the
incurred obligation. When books containing `skip-proofs`

are
included into a session, a warning to the user is printed, reminding
the user that the book is in fact incomplete and possibly
inconsistent.

Major Section: OTHER

Example: (thm (equal (app (app a b) c) (app a (app b c))))Also see defthm. Unlike

`defthm`

, `thm`

does not create an
event; it merely causes the theorem prover to attempt a proof.

General Form: (thm term :hints hints :otf-flg otf-flg :doc doc-string)where

`term`

is a term alleged to be a theorem, and `hints`

,
`otf-flg`

and `doc-string`

are as described in the corresponding
`:`

`doc`

entries. The three keyword arguments above are all
optional.
Major Section: OTHER

Examples: :trans (list a b c) :trans (caddr x) :trans (cond (p q) (r))

This function takes one argument, an alleged term, and translates
it, expanding the macros in it completely. Either an error is
caused or the formal meaning of the term is printed. We also print
the ``output signature'' which indicates how many results are returned
and which are single-threaded objects. For example,
a term that returns one ordinary object (e.g., an object other than
`STATE`

or a user-defined single-threaded object (see defstobj))
has the output signature

=> *A term that returns the single-threaded object

`STATE`

has the
output signature
=> STATEand a term that returns four results might have the output signature

=> (MV $MEM * * STATE)This signature indicates that the first result is the (user defined) single-threaded object

`$MEM`

, that the next two results are ordinary,
and that the last result is `STATE`

.
It is sometimes more convenient to use `trans1`

which is like trans
but which only does top-level macroexpansion.

For more, see term.

Major Section: OTHER

Examples: :trans1 (list a b c) :trans1 (caddr x) :trans1 (cond (p q) (r))

This function takes one argument, an alleged term, and expands the
top-level macro in it for one step only. Either an error is caused,
which happens when the form is not a call of a macro, or the result
printed. Also see trans, which translates the given form
completely.