• 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)))))