# Re: [isabelle] mutual recdefs

```Brian Huffman writes:
>You could actually define these functions together using primrec: Since
>recursive calls are only made on subterms, you don't really need the full
>power of recdef.

that's true in this case, indeed.

>However, using primrec is complicated by the fact that you have used product
>types as arguments to your constructors. This is actually an instance of
>indirect recursion, which means you would be required to additionally define
>several extra constants which take the product types as arguments. If you
>change your datatype definitions so that the constructors have two separate
>arguments instead of a pair, then primrec should work just fine.

But that seems not to be.  As far as I can tell it's impossible to
define multiple mutually-recursive functions over the same types, eg the

is_val :: "exp => bool"
is_exp :: "exp => bool"

in the example below, using either primrec or recdef.  Is that really the case?
Clearly I could encode, with something like

is_val_is_exp :: "exp => (bool * bool) "

and Tom Ridge points out that I can then prove lemmas characterising
the projections of that that look like my original definition.
But I don't want to do that encoding unless I have to...

thanks,
Peter

(* here is_val and is_exp define two sub-grammars of the free exp *)
theory Out = Main:
types ident = "string"
datatype
exp =
Exp_ident "ident"
| Exp_unit
| Exp_pair "exp" "exp"
| Exp_fun "ident" "exp"
| Exp_app "exp" "exp"
| Exp_foo "exp"

consts
is_val :: "exp => bool"
is_exp :: "exp => bool"

primrec
"is_val ((Exp_ident x)) = (True)"
"is_val (Exp_unit) = (True)"
"is_val ((Exp_pair exp exp')) = (((is_val exp) & (is_val exp')))"
"is_val ((Exp_fun x exp)) = (((is_exp exp)))"
"is_val ((Exp_app exp exp')) = False"
"is_val ((Exp_foo val)) = False"

"is_exp ((Exp_ident x)) = (True)"
"is_exp (Exp_unit) = (True)"
"is_exp ((Exp_pair exp exp')) = (((is_exp exp) & (is_exp exp')))"
"is_exp ((Exp_fun x exp)) = (((is_exp exp)))"
"is_exp ((Exp_app exp exp')) = (((is_exp exp) & (is_exp exp')))"
"is_exp ((Exp_foo val)) = (((is_val val)))"

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.