Re: [isabelle] Primrec

Peter Chapman wrote:
> Hi
> I have a polymorphic datatype as follows
> datatype 'a form:
>   ff
> | 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

Hi Peter,

unfortunately, the primrec command is rather restrictive as far as the recursion
scheme of the function is concerned. More precisely, it requires that the recursion
scheme of the function exactly matches the recursion scheme of the datatype. Since
the datatype "'a form" involves nested recursion through the list type constructor,
the type of lists is "unfolded" when constructing the datatype, as can be seen
from the induction rule

  [| P1 ff; !!list. P2 list ==> P1 (Cpd a list); P2 [];
   !!form list. [| P1 form; P2 list |] ==> P2 (form # list) |] ==>
   P1 form & P2 list

which involves two predicates P1 and P2. Consequently, primrec also expects you
to define your depth function as two mutually recursive functions, where one of
the functions is on "'a form", while the other one is on "'a form list":

primrec depth :: "'a form => nat" and depth_list :: "'a form list => nat list" where
  "depth ff = 0"
| "depth (Cpd f fs) = max_list (depth_list fs) + 1"
| "depth_list [] = []"
| "depth_list (f # fs) = depth f # depth_list fs"

Alternatively, you can also use the more general "fun" command for defining
functions by well-founded recursion, which accepts your definition right away:

fun depth :: "'a form => nat" where
  "depth ff = 0"
| "depth (Cpd f fs) = max_list (map depth fs) + 1"


Dr. Stefan Berghofer               E-Mail: berghofe at
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  

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