		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Defunt

Variant of defun that re-uses existing termination theorems automatically.

General Form:

(defunt fn (var1 ... varn) doc-string dcl ... dcl body)

where the arguments are the same as for defun, but without any xargs that specify :measure, :hints, or :well-founded-relation. Those will be inserted automatically into a corresponding defun event, as necessary, by using a database of termination theorems from the community-books.

To use this utility, first evaluate the following event.

(include-book "kestrel/auto-termination/defunt-top" :dir :system)

Examples may be found in the community book, books/kestrel/auto-termination/defunt-tests.lisp. Here is a log showing one such example.

ACL2 !>(defunt f0 (x y)
         (if (endp x)
             y
           (list (f0 (cddr x) (cons 23 y)) 100)))

*Defunt note*: Using termination theorem for EVENS.

 F0
ACL2 !>:pe f0
           2:x(DEFUNT F0 (X Y) ...)
              
>L             (DEFUN
                F0 (X Y)
                (DECLARE
                 (XARGS
                    :MEASURE (ACL2-COUNT X)
                    :HINTS
                    (("Goal" :BY (:FUNCTIONAL-INSTANCE F0-TERMINATION-LEMMA-3
                                                       (TD-STUB-2 F0))))))
                (IF (ENDP X)
                    Y (LIST (F0 (CDDR X) (CONS 23 Y)) 100)))
ACL2 !>

Defunt works by consulting a book that contains a database of information for generating hints based on :termination-theorem lemma-instances. Information about the implementation, which is not necessary for using this utility, may be found (for those who are interested) in community-books file books/kestrel/auto-termination/README.