Re: [isabelle] Primrec



Hi Peter,

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

the problem is that Cpd does not take a parameter of type "'a form", but the "'a form" is nested inside the list type constructor. Internally, such nested datatypes are converted into mutually recursive datatypes, which becomes visible when you try to use primrec.

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
If you want to use primrec, you must define mutually recursive functions, i.e. the following should work:

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

Then, you can later on prove a lemma saying
"depth Cpd f fs = max_list (map depth fs)"
by induction on fs.

Alternatively, you can use the function package instead of primrec, which allows arbitrary pattern matchings and recursion. Since Isabelle 2008, the termination prover usually handles such primitive recursion for nested datatypes.

Andreas





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