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

Ah, that worked! One final question then. You suggested that I look at the theorem AppSrcStmt_AppSrcOp.size. How do I do that?

                            Greg Bronevetsky

Stefan Berghofer wrote:

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.


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