Re-use an existing termination proof automatically.

**NOTE**: THIS UTILITY HAS BEEN LARGELY SUPERSEDED BY

The following (admittedly, contrived) example shows how to use this utility. First define:

(defund my-dec (x) (1- x)) (defun my-max (x y) (declare (xargs :measure (+ (nfix x) (nfix y)) :hints (("Goal" :in-theory (enable my-dec))))) (cond ((zp x) y) ((zp y) x) (t (1+ (my-max (my-dec x) (my-dec y))))))

Now consider the following definition. Its recursion pattern resembles
that of the function above: we recur on the application of

ACL2 !>(with-auto-termination (defun my-sum (a b) (cond ((and (posp a) (posp b)) (+ 2 (my-sum (my-dec a) (my-dec b)))) ((zp b) a) (t b)))) MY-SUM ACL2 !>

We see that the function has been successfully admitted, since the function
name is returned and there is no error message. How did this happen? We can
evaluate `pe`

ACL2 !>:u L 3:x(DEFUN MY-MAX (X Y) ...) ACL2 !>(with-auto-termination (defun my-sum (a b) (cond ((and (posp a) (posp b)) (+ 2 (my-sum (my-dec a) (my-dec b)))) ((zp b) a) (t b))) :show :event) (DEFUN MY-SUM (A B) (DECLARE (XARGS :MEASURE (BINARY-+ (NFIX A) (NFIX B)) :HINTS (("Goal" :USE (:INSTANCE (:TERMINATION-THEOREM MY-MAX) (Y B) (X A)) :IN-THEORY (THEORY 'AUTO-TERMINATION-THEORY))))) (COND ((AND (POSP A) (POSP B)) (+ 2 (MY-SUM (MY-DEC A) (MY-DEC B)))) ((ZP B) A) (T B))) ACL2 !>

We see that ACL2 found a function in the logical world whose
termination argument justifies the termination of `measure` and
`hints` were generated in order to admit the new event.

General Form: (with-auto-termination form :theory th ; default (theory 'auto-termination-theory) :expand ex ; default nil :show s ; default nil :verbose v ; default :minimal )

where `defun` or `defund`, and keyword
arguments, which are not evaluated, have the defaults shown above. If this
event is successful, then the input definition is modified by adding a
generated

We now describe the keyword arguments.

:theory and:expand — These are probably only necessary in the case of defining a reflexive function (one with a recursive call within a recursive call, such as(f (f x)) ). These are passed along as: `in-theory`and`expand`hints, respectively, on"Goal" in the generateddeclare form. A convenient special value for:theory is:current , which is equivalent to supplying the value(current-theory :here) .:show — If this isnil then ACL2 will attempt to admit the resulting definition. Otherwise,:show should be either:event or:dcl , in which case an error-triple is returned without changing the ACL2 world. If:show is:event , then the resulting value will be the generated definition, while if:show is:dcl , then the resulting value will be just the generateddeclare form.:verbose — By default, if adeclare form is successfully generated, then the resulting event will be processed without output from the prover. To see output from the prover, use:verbose t . To avoid even the little messages about ``Searching'' and ``Reusing'', use:verbose nil .

See community book