		Search-engine friendly clone of the ACL2 documentation.

Macro-libraries

With-supporters

Automatically include specified definitions from a specified book

When local include-book forms are used in support of definitions and theorems, the enclosing book or encapsulate event may be ill-formed because of missing definitions. Consider the following example.

(encapsulate
  ()
  (local (include-book "bk")) ; defines function f ;
  (defun g (x) (f x)))

In this example, the definition of f in "bk.lisp" is required in order to admit the definition of g; thus, we say that (the definition of) f is a supporter of (the definition of) g.

With-supporters automatically generates and evaluates definitions, in order to support a given set of names and events. See also with-supporters-after for a related utility.

General forms:

(with-supporters (local ev) ; a local event
                 [optional keyword arguments, including perhaps:]
                 :names (name-1 ... name-m) ; optional keyword argument
                 [other optional keyword arguments]
                 event-1 ... event-k)

where the optional keyword arguments are not evaluated and are described below, and each event-i is an event. The effect is the same as

((encapsulate () (local ev) EXTRA event-1 ... event-k)

where EXTRA is a sequence of events that includes the supporters of the name-i and event-i so that the second pass of that encapsulate call will succeed. (Recall that local events are skipped during that pass; see encapsulate.) More precisely, EXTRA includes the following:

function, macro, and constant definitions that support the supplied :names and event-1 through event-k;
definitions of macros that are aliases for the newly-defined functions (see macro-aliases-table);
defattach and table events; and
in-theory events so that the rules introduced by the EXTRA definitions are suitably enabled or disabled.

Other keywords

Each keyword argument must appear immediately after the initial local event, before the supplied event-i. The keyword :names is discussed above; here we discuss the others. The keyword arguments are not evaluated.

:show (default nil)
This argument must be nil, :only, or t. If it is :only then no event is submitted, but the generated encapsulate is shown by returning it as the value component of an error-triple. If it is t then that encapsulate event is printed, before it is evaluated as usual.
:tables (default nil)
If this value is not nil, then it may be a list of table names, causing the indicated tables to be populated as they were immediately after evaluating the local event, ev. Otherwise the value should be :all, indicating that this should be done for all tables (with the exception, for technical reasons, of pe-table and the xdoc table).
:with-output (default (:off :all :on error))
This value is an alternating list of keywords and values that can be accepted by the with-output utility.

Examples

We now illustrate with examples, starting with one that does not use the :names keyword.

Consider the following event.

(encapsulate
 ()
 (local (include-book "std/lists/duplicity" :dir :system))
 (defthm duplicity-append
   (equal (duplicity a (append x y))
          (+ (duplicity a x) (duplicity a y)))))

This event fails because the function duplicity is defined in the locally included book, and hence that function is undefined when the above defthm form is processed during the second pass of the encapsulate event.

One solution is to move the include-book form so that it appears non-locally in front of the encapsulate event. But we may not want to include other events from that book, out of concern that rules defined in that book could affect our proof development, or perhaps because including the book is slow and we want the superior book to include only what is necessary from that book.

A more suitable solution may thus be to use the macro, with-supporters, in place of encapsulate, as follows.

(with-supporters
 (local (include-book "std/lists/duplicity" :dir :system))
 (defthm duplicity-append
   (equal (duplicity a (append x y))
          (+ (duplicity a x) (duplicity a y)))))

That macro determines automatically that the function duplicity needs to be defined, so it generates an encapsulate event like the original one above but with the definition of duplicity added non-locally. In this example, duplicity is actually defined in terms of another function, duplicity-exec, so its definition is needed as well. The generated event is initially as follows, as we can see using the :show keyword.

ACL2 !>(with-supporters
        (local (include-book "std/lists/duplicity" :dir :system))
        :show :only
        (defthm duplicity-append
          (equal (duplicity a (append x y))
                 (+ (duplicity a x) (duplicity a y)))))

Summary
Form:  ( MAKE-EVENT (WITH-OUTPUT! :OFF ...))
Rules: NIL
Time:  0.13 seconds (prove: 0.00, print: 0.00, other: 0.13)
Prover steps counted:  154
 (WITH-OUTPUT
   :OFF :ALL :ON ERROR
   (ENCAPSULATE
        NIL
        (LOCAL (INCLUDE-BOOK "std/lists/duplicity"
                             :DIR :SYSTEM))
        (SET-ENFORCE-REDUNDANCY T)
        (SET-BOGUS-DEFUN-HINTS-OK T)
        (SET-BOGUS-MUTUAL-RECURSION-OK T)
        (SET-IRRELEVANT-FORMALS-OK T)
        (SET-IGNORE-OK T)
        (PROGN (DEFUN DUPLICITY-EXEC (A X N)
                      (DECLARE (XARGS :GUARD (NATP N)))
                      (IF (ATOM X)
                          N
                          (DUPLICITY-EXEC A (CDR X)
                                          (IF (EQUAL (CAR X) A) (+ 1 N) N))))
               (VERIFY-GUARDS DUPLICITY-EXEC))
        (PROGN (DEFUN DUPLICITY (A X)
                      (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL))
                      (MBE :LOGIC (COND ((ATOM X) 0)
                                        ((EQUAL (CAR X) A)
                                         (+ 1 (DUPLICITY A (CDR X))))
                                        (T (DUPLICITY A (CDR X))))
                           :EXEC (DUPLICITY-EXEC A X 0)))
               (VERIFY-GUARDS DUPLICITY))
        (IN-THEORY (DISABLE (:DEFINITION DUPLICITY-EXEC)
                            (:INDUCTION DUPLICITY-EXEC)
                            (:DEFINITION DUPLICITY)
                            (:INDUCTION DUPLICITY)
                            (:DEFINITION DUPLICITY-EXEC)
                            (:INDUCTION DUPLICITY-EXEC)
                            (:DEFINITION DUPLICITY)
                            (:INDUCTION DUPLICITY)
                            (:DEFINITION DUPLICITY-EXEC)
                            (:INDUCTION DUPLICITY-EXEC)))
        (SET-ENFORCE-REDUNDANCY NIL)
        (DEFTHM DUPLICITY-APPEND
                (EQUAL (DUPLICITY A (APPEND X Y))
                       (+ (DUPLICITY A X) (DUPLICITY A Y))))))
ACL2 !>

Notice that care is taken to preserve the :mode, guard-verification, and enabled status of supporting functions.

For more examples, see community-books file tools/with-supporters-test-top.lisp.