# Re: [isabelle] mutual recdefs

```I think the only mutual recursion we currently support is for mutually
recursive datatypes. Mutual recursion in general is in the pipeline...

Below you find a higher-order encoding of mutual recursion. It avoids having
to mess around with pairs but requires its own tricks. I had never tried this
before and it was a valuable exercise.

Tobias

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_val2 :: "(exp => bool) => exp => bool"
is_exp :: "exp => bool"

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

recdef is_exp "measure size"
"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_val2 is_exp val"

(* The real thing: *)
constdefs is_val :: "exp => bool"
"is_val == is_val2 is_exp"

(* Deriving the real eqns: *)
lemma [simp]:
"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"

(* A complication: the final is_exp rule is more complicated than one
may naively expect. *)
thm is_exp.simps(6)

lemma is_val2_cong:
"(!!e'. size e' < size e ==> f e' = g e') ==> is_val2 f e = is_val2 g e"
by (induct e) simp_all

lemma is_exp_foo[simp]: "is_exp (Exp_foo e) = is_val e"