MUTUAL-RECURSION

define some mutually recursive functions
```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 each `defi` is a call of `defun`, `defund`, `defun-nx`,
or `defund-nx`.
```
When mutually recursive functions are introduced it is necessary to do the termination analysis on the entire clique of definitions. Each `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))).
```