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?
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:
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) +
"AppSrcOpListSize2  = 0"
"AppSrcOpListSize2 (asOp # opList) = (AppSrcOpSize asOp) +
"AppSrcOpListSize3  = 0"
"AppSrcOpListSize3 (asOp # opList) = (AppSrcOpSize asOp) +
"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