Define some mutually recursive functions

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 `defun`, `defund`, `defun-nx`, or

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 `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 `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` `defun`s
specifies the `defun-nx` or

Technical Note: Each `defun`,
`defund`, `defun-nx`, or `defun` form. This is because

Suppose you have defined your own `defun`-like macro and wish to use
it in a `defun`-like form. Here is an example. Suppose you define

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

where `defun` form. As noted above, you are not allowed
to write

(my-mutual-recursion (my-defun ...) ... (my-defun ...))

expands into

(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))).

- Defines
- A very fine alternative to mutual-recursion.
- Make-flag
- Create a flag-based ACL2::induction scheme for a mutual-recursion.
- Mutual-recursion-proof-example
- A small proof about mutually recursive functions
- Def-doublevar-induction
- Create an induction scheme that adds a duplicate variable to the substitution.
- Set-bogus-mutual-recursion-ok
- Allow unnecessary ``mutual recursion''
- Defuns
- An alternative to
`mutual-recursion`