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:
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 in.tum.de
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 http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and