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 defun form or a defund form.
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 defuns specifies the :verify-guards xarg to be nil, then guard verification is omitted for all of the functions.

Technical Note: Each defi above must be of the form (defun ...). In particular, it is not permitted for a defi to be a form that will macroexpand 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. But mutual-recursion must decompose the defi. We therefore insist that they be explicitly presented as defuns or defunds (or a mixture of these).

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