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

AppSrcStmt = skip | ifStmt PvtAddr "AppSrcOp list" "AppSrcOp list" while PvtAddr "AppSrcOp list" and AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"

consts AppSrcStmtSize :: "AppSrcStmt => nat" AppSrcOpSize :: "AppSrcOp => nat" AppSrcOpListSize :: "(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" "AppSrcOpListSize [] = 0"

"AppSrcStmtSize skip = 1"

"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)" When I do this, I get the following error: *** Primrec definition error: *** inconsistent functions for datatype "List.list" *** in *** "AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + AppSrcOpListSize aTrue" *** At command "primrec".

-- Greg Bronevetsky Stefan Berghofer wrote:

Greg Bronevetsky wrote:I'm trying to do use primrec to define a function that is applied toa nested mutually-recursive datatype. The relevant portion of thedatatype definition is below:datatype AppSrcStmt = skip | while PvtAddr "AppSrcOp list" and AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"The primrec in question is a measure function on this datatype,defined as follows: [...]Unfortunately, I get the following error: [...]Dear Greg, the problem is that not only the list datatype, but also the triple type is unfolded (into two pair types). As a consequence, you need two more size functions, one on type "FuncMark * TypeMark * AppSrcStmt" and oneon type "FuncMark * TypeMark * AppSrcStmt". The following definitionshouldwork: consts AppSrcStmtSize :: "AppSrcStmt => nat" AppSrcOpSize :: "AppSrcOp => nat" AppSrcOpListSize :: "(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" "AppSrcOpListSize [] = 0" "AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp)" "AppSrcStmtSize skip = 1" "AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)" See also the theorems AppSrcStmt_AppSrcOp.size provided by the datatype package, which follow a similar scheme. 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

- Previous by Date: Re: [isabelle] proof term request
- Next by Date: [isabelle] PhD-Position (Mitarbeiterstelle) in Coalgebra, Algebra, Formal Methods
- 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