[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.