# Defpun

Define a tail-recursive function symbol

Defpun is a macro developed by Pete Manolios and J Moore that
allows tail-recursive definitions, as well as some other ``partial''
definitions. Related utilities are discussed at the end of this topic.

General Form:
(defpun g (v1 ... vk)
dcl ; optional
body
:kwd1 val1 :kwd2 val2 ... :kwdn valn)

where dcl is an optional `declare` form and the pairs :kwdi
vali are optional (that is n can be 0). If the optional arguments are
omitted, then ACL2 will introduce a constrained function g with this
exported event:

(DEFTHM g-DEF
(EQUAL (g v1 ... vk)
body)
:RULE-CLASSES :DEFINITION)

First suppose that dcl is not present. Then the proposed definition
must have a simple tail-recursive structure (see the discussion of
defp below for a workaround if this is not the case).

If dcl is present, then the definition need not be tail-recursive, and
dcl must have one of the following three forms.

(DECLARE (XARGS :witness defpun-fn))
(DECLARE (XARGS :domain dom-expr :measure m . rest))
(DECLARE (XARGS :gdomain dom-expr :measure m . rest)).

You are encouraged to experiment by using :`trans1` to see the
expansions of defpun forms that use these `declare` forms; but here
is a summary of what is generated.

The first form specifies a function, defpun-fn, and instructs ACL2 to
use that function as a witness for the function g to be introduced, as
follows.

(ENCAPSULATE
((g (v1 ... vk) t))
(LOCAL (DEFUN-NONEXEC g (v1 ... vk) (defpun-fn v1 ... vk)))
(DEFTHM g-DEF
(EQUAL (g v1 ... vk))
body)
:RULE-CLASSES :DEFINITION)

The remaining two declare forms introduce a function, defined
recursively, with the given measure and with a modified body:

(THE-g v1 ... vk)
=
(IF dom-expr body 'UNDEF)

The following theorem is exported.

(defthm g-DEF
(IMPLIES domain-expr
(EQUAL (g v1 ... vk)
body))
:RULE-CLASSES :DEFINITION)

If :gdomain is used (as opposed to :domain), then the following
events are also introduced, where body\{g:=THE-g} denotes the result of
replacing each call of g in body with the corresponding call of
THE-g.

(DEFUN THE-g (v1 ... vk)
(DECLARE (XARGS :MEASURE (IF dom-expr m 0)
:GUARD domain-expr
:VERIFY-GUARDS NIL))
(IF dom-expr body 'UNDEF))
(DEFTHM g-IS-UNIQUE
(IMPLIES domain-expr
(EQUAL (g v1 ... vk) (THE-g v1 ... vk))))

The optional keyword alist :kwd1 val1 :kwd2 val2 ... :kwdn valn is
attached to the end of the generated `defthm` event. If the
:`rule-classes` keyword is not specified by the keyword alist,
:`definition` is used.

Details of defpun are provided by Manolios and Moore in the chapter
``Partial Functions in ACL2'' published with the ACL2 2000
workshop. Also see Partial
Functions in ACL2.

### Variants of defpun

A variant, defp, allows more general forms of tail recursion. If
defpun doesn't work for you, try defp by first executing the
following event.

(include-book "misc/defp" :dir :system)

Sandip Ray has contributed a variant of defpun, defpun-exec, that
supports executability. See community book
books/defexec/defpun-exec/defpun-exec.lisp:

(include-book "defexec/defpun-exec/defpun-exec" :dir :system)

He has also contributed community book
books/misc/misc2/defpun-exec-domain-example.lisp, for functions that are
uniquely defined in a particular domain.

Finally, it is possible to avoid termination proofs even for functions that
are not tail-recursive. See def-partial-measure.