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 form)
where form is processed as usual except that the proof obligations
usually generated are merely assumed.
Normally form is an event; see events. If you want to put
skip-proofs around more than one event, consider the following
(see progn): (skip-proofs (progn event1 event2 ... eventk)).
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 four 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 undoing
(see ubt) and then paying the price of its admission. Note however
that you might still have to supply a measure. The set of formals
used in some valid measure, known as the ``measured subset'' of the
set of formals, is used by ACL2's induction heuristics and therefore
needs to be suitably specified. You may wish to specify the special
measure of (:? v1 ... vk), where (v1 ... vk) enumerates the
measured subset.
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.
4. You are constructing a proof top-down and wish to defer the proof
of a defthm until you are convinced of its utility. You can
embed the defthm in a skip-proofs. Of cou href="DEFINITION.html">definition, in particular the discussion of ``body'' there,
and see hints for a discussion of the :expand hint. Also see set-body
for how to change which of the available definitions (among the original
definition and appropriate :definition rules) is the one that
provides the body. The show-bodies command displays the available such
bodies in an appropriate format, starting with the one that is currently used
as the body.
General Forms: (show-bodies function-symbol) :show-bodies function-symbol