Defret-mutual
Prove additional theorems about a mutual-recursion created using defines, implicitly binding the return variables.
defret-mutual uses flag-function-based induction to prove
theorems about a mutual recursion created using defines. See also ACL2::make-flag for information about the approach.
defret-mutual is mostly just a wrapper around the flag defthm macro
created for the mutual recursion. It generates the individual theorems within
the mutual induction using defret, so the main features are inherited
from defret, such as automatic binding of return value names and support for
the :hyp keyword.
Syntax:
Using the following mutual recursion as an example:
(defines pseudo-term-vars
(define pseudo-term-vars ((x pseudo-termp))
:returns (vars)
...)
(define pseudo-term-list-vars ((x pseudo-term-listp))
:returns (vars)
...))
Then we can use defret-mutual as follows:
(defret-mutual symbol-listp-of-pseudo-term-vars
(defret symbol-listp-of-pseudo-term-vars
(symbol-listp vars)
:hints ...
:fn pseudo-term-vars)
(defret symbol-listp-of-pseudo-term-list-vars
(symbol-listp vars)
:hints ...
:fn pseudo-term-list-vars)
:mutual-recursion pseudo-term-vars
...)
If the :mutual-recursion keyword is omitted, then the last mutual
recursion introduced with defines is assumed to be the subject.
defret-mutual supports all of the top-level options of flag defthm macros such as:
:hints
:no-induction-hint
:skip-others
:instructions
:otf-flg
The individual defret forms inside the mutual recursion support all the
options supported by defret, plus the :skip option from the flag
defthm macro, which if set to nonnil uses the theorem only as an inductive
lemma for the overall mutually recursive proof, and doesn't export it.
