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



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

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