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



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"
and
AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"

I then use the following definition of the size funciton (directly derived from your email):
consts
 AppSrcStmtSize :: "AppSrcStmt => nat"
 AppSrcOpSize :: "AppSrcOp => nat"
 AppSrcOpListSize :: "(AppSrcOp list) => nat"
 AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat"
 AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat"

primrec
"AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp"

"AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y"

"AppSrcOpPairSize (x, y) = AppSrcStmtSize y"

"AppSrcOpListSize [] = 0"
"AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize opList)"

"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + (AppSrcOpListSize aTrue) + (AppSrcOpListSize aFalse)"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)"

When I do this, I get the following error:
*** Primrec definition error:
*** inconsistent functions for datatype "List.list"
*** in
*** "AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + AppSrcOpListSize aTrue"
*** At command "primrec".

After playing around with it, I see that the problem comes from the fact that AppSrcOpListSize appears on the right hand side of AppSrcStmtSize in three spots. If I comment out any two of the references to AppSrcOpListSize then the definition goes through without a problem. However, if there is more than one such reference, I get the above error. Any ideas?

--
                            Greg Bronevetsky

Stefan Berghofer wrote:

Greg Bronevetsky wrote:

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

Unfortunately, I get the following error: [...]


Dear Greg,

the problem is that not only the list datatype, but also the triple type
is unfolded (into two pair types). As a consequence, you need two more
size functions, one on type "FuncMark * TypeMark * AppSrcStmt" and one
on type "FuncMark * TypeMark * AppSrcStmt". The following definition should
work:

consts
  AppSrcStmtSize :: "AppSrcStmt => nat"
  AppSrcOpSize :: "AppSrcOp => nat"
  AppSrcOpListSize :: "(AppSrcOp list) => nat"
  AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat"
  AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat"

primrec
 "AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp"

 "AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y"

 "AppSrcOpPairSize (x, y) = AppSrcStmtSize y"

 "AppSrcOpListSize [] = 0"
 "AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp)"

 "AppSrcStmtSize skip = 1"
 "AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)"

See also the theorems AppSrcStmt_AppSrcOp.size provided by the datatype
package, which follow a similar scheme.

Greetings,
Stefan








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