Major Section: EVENTS

Example: (mutual-recursion (defun evenlp (x) (if (consp x) (oddlp (cdr x)) t)) (defun oddlp (x) (if (consp x) (evenlp (cdr x)) nil))) General Form: (mutual-recursion def1 ... defn) where eachWhen mutually recursive functions are introduced it is necessary to do the termination analysis on the entire clique of definitions. Each`defi`

is a call of`defun`

,`defund`

,`defun-nx`

, or`defund-nx`

.

`defun`

form specifies its own measure, either with the `:measure`

keyword `xarg`

(see xargs) or by default to `acl2-count`

. When a
function in the clique calls a function in the clique, the measure
of the callee's actuals must be smaller than the measure of the
caller's formals -- just as in the case of a simply recursive
function. But with mutual recursion, the callee's actuals are
measured as specified by the callee's `defun`

while the caller's
formals are measured as specified by the caller's `defun`

. These two
measures may be different but must be comparable in the sense that
`o<`

decreases through calls.If you want to specify `:`

`hints`

or `:guard-hints`

(see xargs), you
can put them in the `xargs`

declaration of any of the `defun`

forms,
as the `:`

`hints`

from each form will be appended together, as will the
`guard-hints`

from each form.

You may find it helpful to use a lexicographic order, the idea being to have a measure that returns a list of two arguments, where the first takes priority over the second. Here is an example.

(include-book "ordinals/lexicographic-ordering" :dir :system) (encapsulate () (set-well-founded-relation l<) ; will be treated as LOCAL (mutual-recursion (defun foo (x) (declare (xargs :measure (list (acl2-count x) 1))) (bar x)) (defun bar (y) (declare (xargs :measure (list (acl2-count y) 0))) (if (zp y) y (foo (1- y))))))

The `guard`

analysis must also be done for all of the functions at the
same time. If any one of the `defun`

s specifies the
`:`

`verify-guards`

`xarg`

to be `nil`

, then guard verification
is omitted for all of the functions. Similarly, if any one of the
`defun`

s specifies the `:non-executable`

`xarg`

to be `t`

, or if
any of the definitions uses `defun-nx`

or `defund-nx`

, then every one
of the definitions will be treated as though it specifies a
`:non-executable`

`xarg`

of `t`

.

Technical Note: Each `defi`

above must be a call of `defun`

,
`defund`

, `defun-nx`

, or `defund-nx`

. In particular, it is not
permitted for a `defi`

to be an arbitrary form that macroexpands into a
`defun`

form. This is because `mutual-recursion`

is itself a macro,
and since macroexpansion occurs from the outside in, at the time
`(mutual-recursion def1 ... defk)`

is expanded the `defi`

have not yet
been macroexpanded.

Suppose you have defined your own `defun`

-like macro and wish to use
it in a `mutual-recursion`

expression. Well, you can't. (!) But you
can define your own version of `mutual-recursion`

that allows your
`defun`

-like form. Here is an example. Suppose you define

(defmacro my-defun (&rest args) (my-defun-fn args))where

`my-defun-fn`

takes the arguments of the `my-defun`

form and
produces from them a `defun`

form. As noted above, you are not
allowed to write `(mutual-recursion (my-defun ...) ...)`

. But you can
define the macro `my-mutual-recursion`

so that
(my-mutual-recursion (my-defun ...) ... (my-defun ...))expands into

`(mutual-recursion (defun ...) ... (defun ...))`

by
applying `my-defun-fn`

to each of the arguments of
`my-mutual-recursion`

.
(defun my-mutual-recursion-fn (lst) (declare (xargs :guard (alistp lst))) ; Each element of lst must be a consp (whose car, we assume, is always ; MY-DEFUN). We apply my-defun-fn to the arguments of each element and ; collect the resulting list of DEFUNs. (cond ((atom lst) nil) (t (cons (my-defun-fn (cdr (car lst))) (my-mutual-recursion-fn (cdr lst)))))) (defmacro my-mutual-recursion (&rest lst) ; Each element of lst must be a consp (whose car, we assume, is always ; MY-DEFUN). We obtain the DEFUN corresponding to each and list them ; all inside a MUTUAL-RECURSION form. (declare (xargs :guard (alistp lst))) (cons 'mutual-recursion (my-mutual-recursion-fn lst))).