Hide some events and/or constrain some functions

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

For example, the following trivial encapsulation exports a single event,

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

Note that trivial encapsulates must introduce at least one sub-event, or else they are treated as no-ops, with no effect on the logical world. Consider the following example.

ACL2 !>(encapsulate nil (local (defun f (x) x))) To verify that the encapsulated event correctly extends the current theory we will evaluate it. The theory thus constructed is only ephemeral. Encapsulated Event: ACL2 !>>(LOCAL (DEFUN F (X) X)) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (EQUAL (F X) X). Summary Form: ( DEFUN F ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F End of Encapsulated Event. ACL2 Observation in ( ENCAPSULATE NIL (LOCAL ...) ...): The submitted encapsulate event has created no new ACL2 events, and thus is leaving the ACL2 logical world unchanged. See :DOC encapsulate. Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :EMPTY-ENCAPSULATE ACL2 !>

After the above evaluation, we are left in the world with which we began. For example, if you evaluate the above form in the initial ACL2 world, you can see the following both before and after that evaluation.

ACL2 !>:pbt 0 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>

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,

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

If any event fails while evaluating a call of

We now provide detailed documentation. But discussion of redundancy for

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
`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 `include-book` events that are among
the `local` `include-book` event
is permitted in the scope of any

To be well-formed, an `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'' `local`). Whether trivial or not (i.e., whether the signature is empty or
not), `local`
events, but its `local` events are ignored for the
resulting logical world.

The result of a non-trivial `local` theorems proved about them. In fact, other
functions introduced in 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

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
`ACL2-defaults-table` after an
`program` and `logic`. See defun-mode. More generally, after execution of an `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 beyond what is required for a legal signature other than that all of the guard's 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 `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

If the most recent event is `local` events in its body,

Remark on return value. As with all events, a call of

- If the
encapsulate event is redundant, thenval is:redundant . - Otherwise, if no new events are introduced, then
val is:empty-encapsulate . - Otherwise, if the last sub-event in the final pass of the
encapsulate form evaluates to(mv nil '(:return-value x) ) for somex ,val isx . Note that this can be accomplished by placing the form(value-triple '(:return-value x) :on-skip-proofs t) as the final form in theencapsulate , but since proofs are skipped during that pass, the argument:on-skip-proofs t is necessary forval to bex . - Otherwise, if the list of signatures is
nil thenval ist . - Otherwise, if there is a single signature introducing the function symbol,
fn , thenval isfn . - Otherwise,
val is the list of function symbols introduced in the list of signatures.

Remark on implicit constraints (unknown-constraints). See partial-encapsulate for a related utility that allows some of the constraints to be unspecified. This is an advanced capability that is useful when one installs special-purpose code, possibly in raw Lisp, using a trust tag (see defttag).

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.

- Signature
- How to specify the arity of a constrained function
- Constraint
- Restrictions on certain functions introduced in
`encapsulate`events - Partial-encapsulate
- Introduce functions with some constraints unspecified
- Redundant-encapsulate
- Redundancy of
`encapsulate`events - Infected-constraints
`Events`affecting constraints of`encapsulate`s- Functional-instantiation
- An analogue in ACL2 of higher-order logical reasoning. Functional instantiation allows you to prove theorems ``by analogy'' with previous theorems. See hints and see lemma-instance.