• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Macro-libraries

With-supporters-after

Automatically define necessary redundant definitions from after a specified event

When local include-book forms are used in support of definitions and theorems, the resulting book or encapsulate event may be ill-formed because of missing definitions. The macro, with-supporters-after, is intended to avoid this problem.

See with-supporters for a related utility. (However, with-supporters-after does not support keyword arguments; they may be straightforward to add.) The documentation below assumes familiarity with with-supporters.

General form:

(with-supporters-after name event-1 ... event-k)

where name is the name of an event and event-i are events. The effect is the same as

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

where EXTRA includes redundant definitions and other events introduced after name, as necessary, in order to avoid undefined function errors when processing this encapsulate event, as is the case for with-supporters, in particular, including in-theory events so that the rules introduced by the EXTRA definitions are suitably enabled or disabled. Consider the following example.

(in-package "ACL2")

(include-book "tools/with-supporters" :dir :system)

(deflabel my-label)

(local (include-book "std/lists/duplicity" :dir :system))

(with-supporters-after
 my-label
 (defthm duplicity-append
   (equal (duplicity a (append x y))
          (+ (duplicity a x) (duplicity a y)))))

The form above is equivalent to the following. Again, see with-supporters for relevant background.

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