Major Section: EVENTS

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

(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 (see signature), each
`signature`

describes a different function symbol, and each `evi`

is an
embedded event form (See embedded-event-form). 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.

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`

.

Finally, we note that an `encapsulate`

event is redundant if and
only if a syntactically identical `encapsulate`

has already been
executed under the same `default-defun-mode`

.
See redundant-events.