*Subject*: Re: [isabelle] primrec on nested mutually-recursive datatype*From*: Greg Bronevetsky <greg at bronevetsky.com>*Date*: Fri, 20 Jan 2006 03:33:49 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43CFB0AF.2000204@in.tum.de>*References*: <43C84BD7.7060301@bronevetsky.com> <43CB7BF4.7010100@in.tum.de> <43CC2203.9000603@bronevetsky.com> <43CFB0AF.2000204@in.tum.de>*User-agent*: Mozilla Thunderbird 1.0 (Windows/20041206)

-- Greg Bronevetsky Stefan Berghofer wrote:

The problem is that each occurrence of "AppSrcOp list" is unfolded. Consequently, you have to give a separate size function for each of these occurrences, even though they happen to behave in the same way. The following definition should work: consts AppSrcStmtSize :: "AppSrcStmt => nat" AppSrcOpSize :: "AppSrcOp => nat" AppSrcOpListSize1 :: "(AppSrcOp list) => nat" AppSrcOpListSize2 :: "(AppSrcOp list) => nat" AppSrcOpListSize3 :: "(AppSrcOp list) => nat" AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat" AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat" primrec "AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp" "AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y" "AppSrcOpPairSize (x, y) = AppSrcStmtSize y" "AppSrcOpListSize1 [] = 0""AppSrcOpListSize1 (asOp # opList) = (AppSrcOpSize asOp) +(AppSrcOpListSize1 opList)""AppSrcOpListSize2 [] = 0""AppSrcOpListSize2 (asOp # opList) = (AppSrcOpSize asOp) +(AppSrcOpListSize2 opList)""AppSrcOpListSize3 [] = 0""AppSrcOpListSize3 (asOp # opList) = (AppSrcOpSize asOp) +(AppSrcOpListSize3 opList)""AppSrcStmtSize skip = 1""AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + (AppSrcOpListSize1aTrue) + (AppSrcOpListSize2 aFalse)""AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize3 aW)" Again, a quick look at the theorems AppSrcStmt_AppSrcOp.size reveals how the scheme works. Greetings, Stefan

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

**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

- Previous by Date: Re: [isabelle] primrec on nested mutually-recursive datatype
- Next by Date: [isabelle] European Master's Program in Computational Logic
- Previous by Thread: Re: [isabelle] primrec on nested mutually-recursive datatype
- Next by Thread: Re: [isabelle] primrec on nested mutually-recursive datatype
- 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