Major Section: EVENTS
Example Forms:
(defattach f g) ; call g in place of calling constrained function f
(defattach (f g)) ; same as just above
(defattach (f g :hints (("Goal" :in-theory (enable foo)))))
; equivalent to first form above, except with hints for the
; proof that the guard of f implies the guard of g
(defattach (f g :hints (("Goal" :in-theory (enable foo))))
:hints (("Goal" :use my-thm)))
; equivalent to first form above, except with hints for the
; proof that the constraints on f hold for g
(defattach (f g :hints (("Goal" :in-theory (enable foo))))
(h j :hints (("Goal" :in-theory (enable bar))))
:hints (("Goal" :use my-thm)))
; as above, except attach g to f and attach j to h, with
; the following hints:
; - For proving that the guard of f implies the guard of g,
; enable foo;
; - For proving that the guard of h implies the guard of j,
; enable bar; and
; - For proving that the constraints on f and h hold for
; g and j (respectively), use theorem my-thm.
(defattach f nil) ; remove the attachment of f, if any (e.g., g above)
(defattach (f nil)) ; same as just above
General Forms:
(defattach f g) ; single attach or, if g is nil, unattach
(defattach (f1 g1 :hints hints1)
(f2 g2 :hints hints2)
...
(fk gk :hints hintsk)
:hints hints)
; where all :hints are optional, and if any gi is nil, then
; all gi are nil and all :hints are omitted
The first General Form above is simply an abbreviation for the form
(defattach (f g)), which is an instance of the second General Form above,
described in detail below; but here we give a brief introduction in the case
that g is not nil. This form arranges that during evaluation, with
an exception noted below, every call of the constrained function symbol f
will in essence be replaced by a call of the function symbol g on the
same arguments. We may then refer to g as the ``attachment of'' f,
or say that ``g is attached to f.'' The exception promised above is
that attachments are not called when the theorem prover is simplifying terms.
Consider for example:
(defstub f (x) t) (defun g (x) (+ 3 x)) (defattach f g)If the form
(f 2) is submitted at the ACL2 prompt, the result will be
5 because the attachment g of f is called on the argument,
2. However, during a proof the term (f 2) will not be simplified to
5, which of course would be unsound since there are no axioms about f
that would justify such a simplification.
For the case that g is nil in the first General Form above, we simply
have an abbreviation for the form (defattach (f nil)). This form results
in removal of the existing attachment of f, if any. After this removal,
calls of f will once again cause errors saying that ``ACL2 cannot ev the
call of undefined function ...''.
The rest of this documentation describes the second General Form above, which
is the most general. All hints are optional; their role is described below.
However, i must be at least 1. The fi must be distinct constrained
function symbols, that is, function symbols all introduced in signatures
of encapsulate events (or macros such as defstub that
generate encapsulate events). If any gi is nil then all gi
must be nil, in which case no hintsi is allowed. Assume otherwise.
Then each gi is a :logic-mode function symbol that has had its
guards verified, with the same signature as fi. However, an
exception is that each fi or gi may be the name of a macro that is
associated with a suitable function symbol (see macro-aliases-table); in
that case, references to fi or gi throughout this discussion will
implicitly refer to the corresponding function symbol. This event generates
proof obligations, as described below. If all proofs succeed, then the
effect of this event is first to remove any existing attachments of all the
function symbols fi, and then to attach each gi to fi, in the
sense described above for the first General Form. We may refer to the set of
fi (still assuming each gi is non-nil as the ``attachment nest''
of those fi.
It is legal to redefine attachments, but only after unattaching any
previously-defined attachment (by ``attaching'' nil, as described
above). Whenever a function symbol's attachment is removed, so are all
function symbols that received attachments from the same defattach
event.
Proofs must in general be performed before making attachments. For this
discussion we assume that each gi is non-nil. ACL2 first proves, for
each i (in order), that the guard of fi implies the guard of gi.
If this sequence of proofs succeeds, then the remaining formula to prove is
formed by first taking the conjunction of the constraints on the symbols
fi, and then replacing each fi by gi. This latter proof
obligation is thus similar to that done on behalf of functional
instantiation; see constraint for a discussion of constraints. As with
functional instantiation, ACL2 stores the fact that such proofs have been
done so that they are avoided in future events (see lemma-instance).
How do we determine the status of a function symbol, fn, with respect to
attachment? The form (attachment-alist fn (w state))) evaluates to t
if it is legal to attach a function to (the value of) fn, but there is
not currently any such attachment. It evaluates to nil if it is not
legal to attach to fn. Otherwise, this form evaluates to a non-empty
list of pairs (fi gi) such that fi ranges over the elements of the
attachment nest of f, and for each i, gi is the attachment of
fi.
