SET-INHIBIT-OUTPUT-LST

control output 
Major Section:  OTHER


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


General Form:
(set-inhibit-output-lst lst)
where 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

skip proofs for an event -- a quick way to introduce unsoundness 
Major Section:  OTHER


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.












































































THM

prove a theorem 
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.












































































TRANS

print the macroexpansion of a form 
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 
=> STATE
and 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.












































































TRANS1

print the one-step macroexpansion of a form 
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.