Re: [isabelle] Primrec
> datatype 'a form:
> | 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
If you want to use primrec, you must define mutually recursive
functions, i.e. the following should work:
primrec depth :: 'a form => nat
depth ff = 0
depth Cpd f fs = max_list (map depth fs) + 1
primrec depth :: 'a form => nat and depths :: 'a form list => nat list
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and