# Re: [isabelle] Problem with mutual recursive primrecs

```Sven,

```
```datatype phi2 =
Fin
| Con "phi2 option"
```
```
```
Your datatype has nested recursion: The recursive occurrence occurs under the "option" type. Isabelle internally expresses this with a mutual recursion and requires you to express your primrecs with mutual recursion of a certain fixed form. The funny error messages you are getting are because you are not following that schema.
```
```
Section 3.4.2 in the Tutorial describes nested recursion of datatypes, and primrecs about such types.
```
```
The "fun" command is much more liberal about the form of the definitions, but proving termination can be an issue.
```
```
section {* 3: f1,f2 call each other but they are not mutually recursive (primrecs).*}
```(*
consts
f1 :: "phi2 \<Rightarrow> phi2"
f2 :: "phi2 option \<Rightarrow> phi2 option"
primrec
"f1 Fin = Fin"
```
"f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x \<Rightarrow> f2 (Some x))"
```  "f2 None = None"
"f2 (Some a) = Some (f1 a)"
```
```
```
Obviously they *are* mutually recursive, but primrec is confused because you are not following the schema: "f1 (Con f)" should call "f2 f".
```
```
section {* 4: f1,f2 call each other, they are not mutually recursive but there is a circular dependency between them.*}
```
```
The same, but the confusion is slightly different, so you get a different error (from a different component of the system).
```
```
```section {* 5: f1,f2 call each other but no termination argument is found.*}
(*
fun
f1 :: "phi2 \<Rightarrow> phi2"
and  f2 :: "phi2 option \<Rightarrow> phi2 option"
where
"f1 Fin = Fin"
```
| "f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x \<Rightarrow> f2 (Some x))"
```|  "f2 None = None"
|  "f2 (Some a) = Some (f1 a)"
*)
```
```
```
The automatic termination prover does not deal very well with nested datatypes yet. Section 4 of the (separate) tutorial on functions explains how to do termination proofs manually. You should also read Section 5 about mutual recursive functions.
```
Hope this helps

Alex

```

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