*Subject*: Re: [isabelle] primrec on nested mutually-recursive datatype*From*: Greg Bronevetsky <greg at bronevetsky.com>*Date*: Tue, 24 Jan 2006 13:59:16 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43D606E5.8010503@in.tum.de>*References*: <43C84BD7.7060301@bronevetsky.com> <43CB7BF4.7010100@in.tum.de> <43CC2203.9000603@bronevetsky.com> <43CFB0AF.2000204@in.tum.de> <43D0A06D.10603@bronevetsky.com> <43D51E64.50804@in.tum.de> <43D5628F.3050703@bronevetsky.com> <43D606E5.8010503@in.tum.de>*User-agent*: Mozilla Thunderbird 1.0 (Windows/20041206)

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 complainsthatyou 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 toogeneric forproving the termination of the above function. For this to work, you haveto use one of the specific size functions produced by the datatypepackage, e.g.recdef func "measure AppSrcOp_list_size1"The termination proof relies on the fact that the three specific sizefunctionsare 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

**References**:**[isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] primrec on nested mutually-recursive datatype
- Next by Date: [isabelle] PhD positions available
- Previous by Thread: Re: [isabelle] primrec on nested mutually-recursive datatype
- Next by Thread: [isabelle] proof term request
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list