• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • 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 the :names argument; that should be straightforward to add, if needed.) 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 of functions introduced after name, as necessary, in order to avoid undefined function errors when processing this encapsulate event. (As with with-supporters, EXTRA may also include macro aliases and their supporters; see with-supporters for details.) EXTRA also includes in-theory events so that the rules introduced by the EXTRA definitions are suitably enable 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. Note that the present macro, like that one, is also implemented using the macro std::defredundant.

(progn
 (encapsulate
  ()
  (set-enforce-redundancy t)
  (logic)
  (defun duplicity-exec (a x n)
    (declare (xargs :mode :logic :verify-guards t))
    (declare (xargs :measure (:? x)))
    (declare (xargs :guard (natp n)))
    (if (atom x)
        n
        (duplicity-exec a (cdr x)
                        (if (equal (car x) a) (+ 1 n) n))))
  (in-theory (e/d ((:type-prescription duplicity-exec)
                   (:executable-counterpart duplicity-exec))
                  ((:induction duplicity-exec)
                   (:definition duplicity-exec))))
  (defun duplicity (a x)
    (declare (xargs :mode :logic :verify-guards t))
    (declare (xargs :measure (:? x)))
    (declare (xargs :guard t))
    (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)))
  (in-theory (e/d ((:type-prescription duplicity)
                   (:executable-counterpart duplicity))
                  ((:induction duplicity)
                   (:definition duplicity)))))
 (defthm duplicity-append
   (equal (duplicity a (append x y))
          (+ (duplicity a x) (duplicity a y)))))