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

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

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe

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