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

Greg Bronevetsky wrote:
Thank you. What you suggests works. However, when I apply it to my full example I'm still getting errors. The problem is that my language has if statements as well as while statements. Adding them to my type definition, produces the following:
AppSrcStmt =
  skip |
  ifStmt PvtAddr "AppSrcOp list" "AppSrcOp list"
  while PvtAddr "AppSrcOp list"
AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"

I then use the following definition of the size funciton (directly derived from your email): [...]

When I do this, I get the following error:
*** Primrec definition error:
*** inconsistent functions for datatype "List.list"

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:

 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"

"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 + (AppSrcOpListSize1 aTrue) + (AppSrcOpListSize2 aFalse)"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize3 aW)"

Again, a quick look at the theorems AppSrcStmt_AppSrcOp.size reveals
how the scheme works.


Dr. Stefan Berghofer               E-Mail: berghofe at
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  

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