Restrictions on certain functions introduced in `encapsulate` events

Suppose that a given theorem, `defaxiom` or (ii)
`defaxiom`. Here, a function symbol is
``ancestral'' in

The remainder of this note explains what we mean by ``constraint'' in the words above. For a utility that obtains the constraint for a given function symbol, see constraint-info.

In a certain sense, function symbols are introduced in essentially two
ways. The most common way is to use `defun` (or when there is mutual
recursion, `mutual-recursion` or `defuns`). There is also a
mechanism for introducing ``witness functions''; see defchoose. The
documentation for these events describes the axioms they introduce,
which we will call here their ``definitional axioms.'' These definitional
axioms are generally the constraints on the function symbols that these axioms
introduce.

However, when a function symbol is introduced in the scope of an `encapsulate` event, its constraints may differ from the definitional axioms
introduced for it. For example, suppose that a function's definition is
`local` to the `encapsulate`; that is, suppose the function is
introduced in the signature of the `encapsulate`. Then its
constraints include, at the least, those non-`local` theorems and
definitions in the `encapsulate` that mention the function symbol.

Actually, it will follow from the discussion below that if the signature is empty for an `encapsulate`, then the constraint on each of
its new function symbols is exactly the definitional axiom introduced for it.
Intuitively, we view such `include-book` events. But the general case, where the signature
is not empty, is more complicated.

In the discussion that follows we describe in detail exactly which
constraints are associated with which function symbols that are introduced in
the scope of an `encapsulate` event. In order to simplify the
exposition we make two cuts at it. In the first cut we present an
over-simplified explanation that nevertheless captures the main ideas. In the
second cut we complete our explanation by explaining how we view certain events as being ``lifted'' out of the `encapsulate`, resulting in a
possibly smaller `encapsulate`, which becomes the target of the
algorithm described in the first cut.

At the end of this note we present an example showing why a more naive approach is unsound.

Finally, before we start our ``first cut,'' we note that any information
you want ``exported'' outside an `encapsulate` event must be there as an
explicit definition or theorem. For example, even if a function `mv` functions), then you
may find it useful to prove (inside the `type-prescription` rule for the constrained function, for
example, the `type-prescription` rule

*First cut at constraint-assigning algorithm.* Consider the set of
formulas introduced by all events in the scope of an `encapsulate`:

- for every
`defthm`and`defaxiom`event, include its formula as well as the formulas of all its corollaries; - for every
`defun`event, include the formula that equates the body with the application of the function applied to the formals; - for every
defchoose event, include the axiom that it adds (see defchoose); - and so on, including axioms added by
`defpkg`and (recursively) any subsidiaryencapsulate events.

Then quite simply, all such formulas are conjoined, and each function
symbol introduced by the `encapsulate` is assigned that conjunction as
its constraint.

Clearly this is a rather severe algorithm. Let us consider two possible optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below. The function

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

We would like to imagine moving the definition of `encapsulate`, as follows.

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

Thus, we will only assign the constraint

More generally, suppose an event in an `encapsulate` event does not
mention any function symbol in the signature of the `encapsulate`, nor any function symbol that mentions any such function symbol,
and so on. (We might say that no function symbol from the signature is
an ``ancestor'' of any function symbol occurring in the event.) Then we
imagine moving the event, so that it appears in front of the `encapsulate`. We don't actually move it, but we pretend we do when it comes
time to assign constraints. Thus, such definitions only introduce
definitional axioms as the constraints on the function symbols being defined.
In the example above, the event

Once this first optimization is performed, we have in mind a set of
``constrained functions.'' These are the functions introduced in the `encapsulate` that would remain after moving some of them in front, as
indicated above. Consider the collection of all formulas introduced by the
`encapsulate`, except the definitional axioms, that mention these
constrained functions. So for example, in the event below, no such formula
mentions the function symbol

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

We can see that there is really no harm in imagining that we move the
definition of `encapsulate`, to just after the
`encapsulate`.

Many subtle aspects of this rearrangement process have been omitted. For
example, suppose the function

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (declare (ignore x)) 0)) (defun fn (lst) (if (endp lst) t (and (integerp (sig-fn (car lst))) (fn (cdr lst))))) (defthm fn-always-true (fn lst)))

In this example, there are no `defthm` events that mention

This is a pathological example that illustrate a trap into which one may
easily fall: rather than identify the key properties of the constrained
function the user has foreshadowed its intended application and constrained
those notions. Clearly, the user wishing to introduce the

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (declare (ignore x)) 0)) (defthm integerp-sig-fn (integerp (sig-fn x)))) (defun fn (lst) (if (endp lst) t (and (integerp (sig-fn (car lst))) (fn (cdr lst))))) (defthm fn-always-true (fn lst)))

Note that

Sometimes it is necessary to introduce a function such as

Another subtle aspect of encapsulation that has been brushed over so far
has to do with exactly how functions defined within the encapsulation use the
signature functions. For example, above we say ``Consider the collection of
all formulas introduced by the encapsulate, *except the definitional
axioms*, that mention these constrained functions.'' We seem to suggest
that a definitional axiom which mentions a constrained function can be moved
out of the encapsulation and considered part of the ``post-encapsulation''
extension of the logical world, if the defined function is not used in
any non-definitional formula proved in the encapsulation. For example, in the
encapsulation above that constrained *admission* used properties of the witnesses! In particular, we say a
function is ``subversive'' if any of its governing tests or the actuals in any
recursive call involve a function in which the signature functions are
ancestral. See infected-constraints and see subversive-recursions.

(Aside: The definition of `and` expands to a call of

(defun fn (lst) (if (endp lst) t (if (integerp (sig-fn (car lst))) (fn (cdr lst)) nil))).

If we switch the order of conjuncts in

Another aspect we have not discussed is what happens to nested
encapsulations when each introduces constrained functions. We say an

From the foregoing discussion we see we are interested in exactly how we can ``rearrange'' the events in a non-trivial encapsulation — moving some ``before'' the encapsulation and others ``after'' the encapsulation. We are also interested in which functions introduced by the encapsulation are ``constrained'' and what the ``constraints'' on each are. We may summarize the observations above as follows, after which we conclude with a more elaborate example.

*Second cut at constraint-assigning algorithm.* First, we focus only
on non-trivial encapsulations that neither contain nor are contained in
non-trivial encapsulations. (Nested non-trivial encapsulations are not
rearranged at all: do not put anything in such a nest unless you mean for it
to become part of the constraints generated.) Second, in what follows we only
consider the non-`encapsulate` other than
definitional axioms. Add to this set any of those definitional equations that
is either subversive or defines a function used in a formula in the set. The
conjunction of the resulting set of formulas is called the ``constraint'' and
the set of all the signature functions of the

Implementation note. In the implementation we do not actually move events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm. It builds on the preceding examples.

(encapsulate (((sig-fn *) => *)) (defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) (defun during (x) (if (consp x) x (cons (car (sig-fn x)) 17))) (defun before2 (x) (before1 x)) (defthm before2-prop (atom (before2 x))) (defthm during-prop (implies (and (atom x) (before2 x)) (equal (car (during x)) (car (sig-fn x))))) (defun after1 (x) (sig-fn x)) (defchoose after2 (x) (u) (and (< u x) (during x))) )

Only the functions `encapsulate`, as is the theorem `encapsulate`. The implementation reports the following.

In addition to SIG-FN, we export AFTER2, AFTER1, BEFORE2, DURING and BEFORE1. The following constraint is associated with both of the functions DURING and SIG-FN: (AND (EQUAL (DURING X) (IF (CONSP X) X (CONS (CAR (SIG-FN X)) 17))) (CONSP (SIG-FN X)) (IMPLIES (AND (ATOM X) (BEFORE2 X)) (EQUAL (CAR (DURING X)) (CAR (SIG-FN X)))))

Notice that the formula `type-prescription` rule deduced during the definition
of the function

We conclude by asking (and to a certain extent, answering) the following
question: Isn't there an approach to assigning constraints that avoids
over-constraining more simply than our ``second cut'' above? Perhaps it seems
that given an `encapsulate`, we should simply assign to each locally
defined function the theorems exported about that function. If we adopted
that simple approach the events below would be admissible.

(encapsulate (((foo *) => *)) (local (defun foo (x) x)) (defun bar (x) (foo x)) (defthm bar-prop (equal (bar x) x) :rule-classes nil)) (defthm foo-id (equal (foo x) x) :hints (("Goal" :use bar-prop))) ; The following event is not admissible in ACL2. (defthm ouch! nil :rule-classes nil :hints (("Goal" :use ((:functional-instance foo-id (foo (lambda (x) (cons x x))))))))

Under the simple approach we have in mind,

It's tempting to think we can fix this by including definitions, not just
theorems, in constraints. But consider the following slightly more elaborate
example. The problem is that we need to include as a constraint on

(encapsulate (((foo *) => *)) (local (defun foo (x) x)) (local (defthm foo-prop (equal (foo x) x))) (defun bar (x) (foo x)) (defun abc (x) (bar x)) (defthm abc-prop (equal (abc x) x) :rule-classes nil)) (defthm foo-id (equal (foo x) x) :hints (("Goal" :use abc-prop))) ; The following event is not admissible in ACL2. (defthm ouch! nil :rule-classes nil :hints (("Goal" :use ((:functional-instance foo-id (foo (lambda (x) (cons x x))) (bar (lambda (x) (cons x x))))))))

- Constraint-info
- Obtaining the constraint on a function symbol