Major Section: EVENTS

`Encapsulate`

provides a way to execute a sequence of events and then
hide some of the resulting effects. There are two kinds of encapsulations:
``trivial'' and ``non-trivial''. We discuss these briefly before providing
detailed documentation.

A trivial encapsulation is an event of the following form.

(encapsulate () ; nil here indicates "trivial" <event-1> ... <event-k>)We use the term ``sub-events'' to refer to

`<event-1>`

through
`<event-k>`

. Each sub-event `<event-i>`

may be ``local'', that is,
of the form `(local <event-i'>)`

; the other sub-events are called
``non-local''. When this `encapsulate`

form is submitted to ACL2, it is
processed in two passes. On the first pass, each sub-event is processed in
sequence; admission of the `encapsulate`

fails if any `<event-i>`

fails
to be admitted. Then a second pass is made after rolling back the logical
world to what it was just before executing the `encapsulate`

form. In
the second pass, only the non-local forms `<event-i>`

are evaluated,
again in order, and proofs are skipped.For example, the following trivial encapsulation exports a single event,
`member-equal-reverse`

. The lemma `member-revappend`

is used (as a
rewrite rule) to prove `member-equal-reverse`

on the first pass, but
since `member-revappend`

is local, it is ignored on the second (final)
pass.

(encapsulate () (local (defthm member-revappend (iff (member-equal a (revappend x y)) (or (member-equal a x) (member-equal a y))) :hints (("Goal" :induct (revappend x y))))) (defthm member-equal-reverse (iff (member-equal a (reverse x)) (member-equal a x))))Of course, one might prefer to prove these events at the top level, rather than within an encapsulation; but the point here is to illustrate that you can have local events that do not become part of the logical world. (Such a capability is also provided at the level of books; in particular, see include-book.)

On the other hand, non-trivial encapsulations provide a way to introduce axioms about new function symbols, without introducing inconsistency and without introducing complete definitions. The following example illustrates how that works.

(encapsulate ; The following list has a single signature, introducing a function foo of ; one argument that returns one value. (The list is non-empty, so we call ; this a "non-trivial" encapsulation.) ( ((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)))To understand this example, we consider how non-trivial encapsulations are processed. The same two passes are made as for trivial encapsulations, and the (local) definition of

`foo`

is ignored on the second pass, and
hence does not appear in the resulting ACL2 logical world. But before
the second pass, each signature is stored in the world. Thus, when
the theorem `foo-preserves-consp`

is encountered in the second pass,
`foo`

is a known function symbol with the indicated signature.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.

Observe that if the signatures list is empty, the resulting ``trivial''
`encapsulate`

may still be useful for deriving theorems to be exported
whose proofs require lemmas you prefer to hide (i.e., made `local`

).
Whether trivial or not (i.e., whether the signature is empty or not),
`encapsulate`

exports the results of evaluating its non-`local`

events, but its `local`

events are ignored for the resulting
logical world.

The result of a non-trivial `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. After a non-trivial `encapsulate`

event is admitted,
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.

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.

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 a non-trivial `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)))

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 signatures and the
same number of top-level events -- let `k`

be that number -- and for
each `i < k`

, the `i`

th top-level events `E1`

and `E2`

from the
earlier and current `encapsulate`

s 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.