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 ... = ... & ...

instead of

  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.


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