[isabelle] Primrec


I have a polymorphic datatype as follows

datatype 'a form:
| Cpd 'a ('a form list)

I also have a function which, given a list of naturals, returns the largest, called max_list. I want to define a function on my datatype as follows:

primrec depth  :: 'a form => nat
  depth ff = 0
  depth Cpd f fs = max_list (map depth fs) + 1

Isabelle doesn't like it, giving me the error message

*** Entity to be defined occurs on rhs
*** The error(s) above occurred in definition "depth_form_def":
*** "depth =_ form_rec_1 (\ i. 0) (\ f fs fsa. max_list (map depth fs) + 1) 0 undefined undefined"
*** At command "primrec".

(where =_ is the identity symbol, and \ is a lambda). Is this not a proper recursive call? I think it should be. For instance, if it is written as

depth Cpd f [p,...q] = max_list [depth p,..., depth q]

then I think it is a recursive call. Can anyone point out how to fix this, or why I am wrong in my belief?



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