# Re: [isabelle] primrec on nested mutually-recursive datatype

```Great! That worked perfectly. My recursive definitions go through now.

--
Greg Bronevetsky

Stefan Berghofer wrote:

```
```Greg Bronevetsky wrote:

```
```I'm not using size because it seems to be too generic. [...]

The size function created for this datatype is:
[...]
AppSrcOp_list_size1 [] = 0
AppSrcOp_list_size1 (?AppSrcOp # ?list) = size ?AppSrcOp + [...]

The core of function definition is as follows:
consts func :: "(AppSrcOp list) => bool"
recdef func "measure size"
"func [] = True"
"func (asOp # asList) =
(case asOp of
opTriple triple =>
(case (snd(snd triple)) of
(ifStmt pv aTrue aFalse) =>
((func aTrue) &
(func aFals)) |
(while pv aW) =>
(func aW) |
_ => True) &
(func asList)
)
"
This produces the following error from Isabelle:
"*** recursion equations must use the = relation
*** At command "recdef"."
```
```

```
The above function definition works fine for me. If Isabelle complains that
```you have not used the = relation, then this usually due to missing
parentheses on the right-hand side of some equation, e.g. if you write

f ... = ... & ...

f ... = (... & ...)

```
However, you are right that the "size" function on lists is too generic for
```proving the termination of the above function. For this to work, you have
```
to use one of the specific size functions produced by the datatype package, e.g.
```
recdef func "measure AppSrcOp_list_size1"

```
The termination proof relies on the fact that the three specific size functions
```are equal, i.e. you have to prove

lemma [recdef_simp]: "AppSrcOp_list_size2 xs = AppSrcOp_list_size1 xs"
by (induct xs) simp_all

lemma [recdef_simp]: "AppSrcOp_list_size3 xs = AppSrcOp_list_size1 xs"
by (induct xs) simp_all

before invoking recdef.

Greetings,
Stefan

```
```

```

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