control output
Parent topic: OTHER Home
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 output
It 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.
skip proofs for an event -- a quick way to introduce unsoundness
Parent topic: OTHER Home
Example Form:
(skip-proofs
(defun foo (x)
(if (atom x) nil (cons (car x) (foo (reverse (cdr x)))))))
General Form:
(skip-proofs event)
where 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.
prove a theorem
Parent topic: OTHER Home
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.
print the macroexpansion of a form
Parent topic: OTHER Home
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 ``multiplicity'' and ``state-out'' for the translated term. The
multiplicity indicates how many values are returned (in the mv
sense) and is always 1 or greater. State-out indicates whether and
where a state is returned. If state-out is nil, the form does not
return a state (either as its value or among its multiple values).
If t, the form returns one value and it is a state. Otherwise,
state-out is a number which indicates which of its multiple values
is a state.
For more, see term.
print the one-step macroexpansion of a form
Parent topic: OTHER Home
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.