`Events` affecting constraints of `encapsulate`s

Here we explain briefly the two kinds of `encapsulate` events. Also see constraint for a more complete
discussion of constraints produced by

An `defun`, but it could be
introduced in a signatures of a subsidiary `defchoose` event. Below we'll discuss the case of

Let's compare the following three examples.

**EXAMPLE 1**.

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (cons x x))) (defun foo (x) (sig-fn x)) (defthm foo-prop (consp (foo x))))

In Example 1 above, ACL2 warns us that the

ACL2 Warning [Infected] in ( ENCAPSULATE (((SIG-FN * ...) ...) ...) ...): Note that the definitional equation for FOO infects the constraint of this encapsulation....

Indeed, just above that warning we see that the definitional equation for

The following constraint is associated with both of the functions FOO and SIG-FN: (AND (EQUAL (FOO X) (SIG-FN X)) (CONSP (FOO X)))

The warning message suggests the desirability of moving the definition out
of the

By contrast, in the next two examples the

**EXAMPLE 2** (moving the definition of

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (cons x x))) (defun foo (x) x) (defthm foo-prop (equal (foo x) (car (sig-fn x)))))

**EXAMPLE 3** (moving the definition of

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (cons x x))) (defun foo (x) (sig-fn x)) (defthm foo-prop (consp (sig-fn x))) )

We now turn to a second kind of

**EXAMPLE 4**.

(encapsulate (((f *) => *)) (local (defun f (x) (cdr x))) (defthm f-prop (equal (f nil) nil)) (defun g (x) (if (consp x) (g (f x)) x)))

As in Example 1 above, the exported constraint is on both function symbols that have been introduced, reported as follows by ACL2.

The following constraint is associated with both of the functions G and F: (AND (EQUAL (F NIL) NIL) (EQUAL (G X) (IF (CONSP X) (G (F X)) X)))

But this time, in addition, no induction scheme is stored for

ACL2 Warning [Infected] in ( ENCAPSULATE (((F * ...) ...) ...) ...): Note that G is ``subversive.'' See :DOC infected-constraints....

Note that if

See subversive-recursions for more details, including criteria for
when this ``subversive'' situation arises and what might be done to address
it. Also see constraint for a general discussion of constraints
introduced by an `encapsulate` event.