constrain some functions and/or hide some events
Major Section:  EVENTS

The following example illustrates the idea of encapsulate.


; Introduce a function foo of one argument that returns one value:
 ( ((foo *) => *) )

; Introduce a ``witness'' (example) for foo, marked as local so that
; it is not exported:
 (local (defun foo (x) x))

; Introduce a non-local property to be exported:
 (defthm foo-preserves-consp
   (implies (consp x)
            (consp (foo x))))
The form above introduces a new function symbol, foo, with the indicated property and no definition. In fact, the output from ACL2 concludes as follows.

The following constraint is associated with the function FOO:


We turn now to more complete documentation.

Other Examples:

; The list of signatures above could also be written
;            ((an-element (lst) t))

  (local (defun an-element (lst)
  (local (defthm member-equal-car
            (implies (and lst (true-listp lst))
  (defthm thm1
  (defthm thm2
     (implies (and (true-listp lst)
                   (not (null lst)))

 () ; empty signature: no constrained functions indicated

 (local (defthm hack
          (implies (and (syntaxp (quotep x))
                        (syntaxp (quotep y)))
                   (equal (+ x y z)

 (defthm nthcdr-add1-conditional
            (equal (nthcdr (1+ n) x)
                   (nthcdr n (cdr x))))))

General Form:
(encapsulate (signature ... signature)
where each signature is a well-formed signature, each signature describes a different function symbol, and each evi is an embedded event form (See embedded-event-form). Also see signature, in particular for a discussion of how a signature can assign a guard to a function symbol. There must be at least one evi. The evi inside local special forms are called ``local'' events below. Events that are not local are sometimes said to be ``exported'' by the encapsulation. We make the further restriction that no defaxiom event may be introduced in the scope of an encapsulate (not even by encapsulate or include-book events that are among the evi). Furthermore, no non-local include-book event is permitted in the scope of any encapsulate with a non-empty list of signatures.





We make some remarks on guards and evaluation. Calls of functions introduced in the signatures list cannot be evaluated in the ACL2 read-eval-print loop. See defattach for a way to overcome this limitation. Moreover, any :guard supplied in the signature is automatically associated in the world with its corresponding function symbol, with no requirement other than that the guard is a legal term all of whose function symbols are in :logic mode with their guards verified. In particular, there need not be any relationship between a guard in a signature and the guard in a local witness function. Finally, note that for functions introduced non-locally inside an encapsulate event, guard verification is illegal unless ACL2 determines that the proof obligations hold outside the encapsulate event as well.

 ((f (x) t))
 (local (defun f (x) (declare (xargs :guard t)) (consp x)))
 ;; ERROR!
 (defun g (x)
   (declare (xargs :guard (f x)))
   (car x)))




The typical way for an encapsulate event to be redundant is when a syntactically identical encapsulate has already been executed under the same default-defun-mode, default-ruler-extenders, and default-verify-guards-eagerness. More generally, the encapsulate events need not be syntactically identical, but rather, need only to correspond in the following sense: they contain the same number of top-level events -- let k be that number -- and for each i < k, the ith top-level events E1 and E2 from the earlier and current encapsulates have one of the following properties.

o E1 and E2 are equal; or

o E1 is of the form (record-expansion E2 ...); or else

o E1 and E2 are equal after replacing each local sub-event by (local (value-triple :elided)), where a sub-event of an event E is either E itself, or a sub-event of a constituent event of E in the case that E is a call of with-output, with-prover-time-limit, with-prover-step-limit, record-expansion, time$, progn, progn!, or encapsulate itself.

Remark for ACL2(r) (see real). For ACL2(r), encapsulate can be used to introduce classical and non-classical functions, as determined by the signatures; see signature. Those marked as classical (respectively non-classical) must have classical (respectively, non-classical) local witness functions. A related requirement applies to functional instantiation; see lemma-instance.