ENCAPSULATE

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

The following example illustrates the idea of encapsulate. 

(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:

(IMPLIES (CONSP X) (CONSP (FOO X)))

We turn now to more complete documentation.

Other Examples:
(encapsulate (((an-element *) => *))

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

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

(encapsulate
 () ; empty signature: no constrained functions indicated

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

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

General Form:
(encapsulate (signature ... signature)
  ev1
  ...
  evn)
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.

To be well-formed, an encapsulate event must have the properties that each event in the body (including the local ones) can be successfully executed in sequence and that in the resulting theory, each function mentioned among the signatures was introduced via a local event and has the signature listed. (A utility is provided to assist in debugging failures of such execution; see redo-flat.) In addition, the body may contain no ``local incompatibilities'' which, roughly stated, means that the events that are not local must not syntactically require symbols defined by local events, except for the functions listed in the signatures. See local-incompatibility. Finally, no non-local recursive definition in the body may involve in its suggested induction scheme any function symbol listed among the signatures. See subversive-recursions.

The result of an encapsulate event is an extension of the logic in which, roughly speaking, the functions listed in the signatures are constrained to have the signatures listed and to satisfy the non-local theorems proved about them. In fact, other functions introduced in the encapsulate event may be considered to have ``constraints'' as well. (See constraint for details, which are only relevant to functional instantiation.) Since the constraints were all theorems in the ``ephemeral'' or ``local'' theory, we are assured that the extension produced by encapsulate is sound. In essence, the local definitions of the constrained functions are just ``witness functions'' that establish the consistency of the constraints. Because those definitions are local, they are not present in the theory produced by encapsulation. Encapsulate also exports all rules generated by its non-local events, but rules generated by local events are not exported.

The default-defun-mode for the first event in an encapsulation is the default defun-mode ``outside'' the encapsulation. But since events changing the defun-mode are permitted within the body of an encapsulate, the default defun-mode may be changed. However, defun-mode changes occurring within the body of the encapsulate are not exported. In particular, the acl2-defaults-table after an encapsulate is always the same as it was before the encapsulate, even though the encapsulate body might contain defun-mode changing events, :program and :logic. See defun-mode. More generally, after execution of an encapsulate event, the value of acl2-defaults-table is restored to what it was immediately before that event was executed. See acl2-defaults-table.

Theorems about the constrained function symbols may then be proved -- theorems whose proofs necessarily employ only the constraints. Thus, those theorems may be later functionally instantiated, as with the :functional-instance lemma instance (see lemma-instance), to derive analogous theorems about different functions, provided the constraints (see constraint) can be proved about the new functions.

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. 

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

Observe that if the signatures list is empty, encapsulate may still be useful for deriving theorems to be exported whose proofs require lemmas you prefer to hide (i.e., made local).

The order of the events in the vicinity of an encapsulate is confusing. We discuss it in some detail here because when logical names are being used with theory functions to compute sets of rules, it is sometimes important to know the order in which events were executed. (See logical-name and see theory-functions.) What, for example, is the set of function names extant in the middle of an encapsulation?

If the most recent event is previous and then you execute an encapsulate constraining an-element with two non-local events in its body, thm1 and thm2, then the order of the events after the encapsulation is (reading chronologically forward): previous, thm1, thm2, an-element (the encapsulate itself). Actually, between previous and thm1 certain extensions were made to the world by the superior encapsulate, to permit an-element to be used as a function symbol in thm1.

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.