# [isabelle] primrec on nested mutually-recursive datatype

`I'm trying to do use primrec to define a function that is applied to a
``nested mutually-recursive datatype. The relevant portion of the datatype
``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:
`consts AppSrcStmtSize :: "AppSrcStmt => nat"
AppSrcOpSize :: "AppSrcOp => nat"
AppSrcOpListSize :: "(AppSrcOp list) => nat"
primrec
"AppSrcOpSize (opTriple asOp) = (AppSrcStmtSize (snd (snd asOp)))"
"AppSrcOpListSize [] = 0"
"AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp)"
"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)"
Unfortunately, I get the following error:
*** Constant to be defined occurs on rhs

`*** The error(s) above occurred in definition
``"AppSrcStmtSize_AppSrcStmt_def":
`*** "AppSrcStmtSize ==

`*** AppSrcStmt_AppSrcOp_rec_1 (1::nat) (%(pv::nat) aW::AppSrcOp list.
``op + (1::nat))
``*** (%(asOp::nat * nat * AppSrcStmt) asOpa::unit. AppSrcStmtSize
``(snd (snd asOp))) (0::nat)
``*** (%(asOp::AppSrcOp) (opList::AppSrcOp list) (asOpa::nat)
``opLista::nat. asOpa) arbitrary arbitrary"
`*** At command "primrec".

`I think I'm following the directions from section 3.4 of the tutorial
``but I apparenly I'm missing something. Any thoughts on what the problem
``might be?
`
--
Greg Bronevetsky

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