Re: [isabelle] primrec of datatype containing fset

Hi Manuel,

Sorry, I had missed your message. I fully agree with your disagreement.  :-)



From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Manuel Eberl <eberlm at>
Sent: 09 July 2017 12:54:12
To: cl-isabelle-users at
Subject: Re: [isabelle] primrec of datatype containing fset

I don't fully agree.

There are some cases, like infinitely-branching datatypes, where
"primrec" works without problems, but "function" requires considerable
additional work (because there is no usable "size" function).

Also, for datatypes with many constructors, I think "function" can be
quite slow due to the huge number of things it does and theorems that it
proves. "primrec" is a good light-weight alternative then.

Personally, I tend to use primrec rather than fun whenever it is
possible to do so without significant effort.


On 2017-07-09 11:49, Lawrence Paulson wrote:
> These days, users should regard "primrec" as an internal feature necessary for bootstrapping the system but for implementers only.
> Larry Paulson
>> On 9 Jul 2017, at 11:15, Lars Hupel <hupel at> wrote:
>> this is a restriction of "primrec". What you're writing is not in fact a
>> primitive recursive specification. There are two ways around that:
>> 1) Rewrite it as primitive recursive
>> 2) Use the "fun"/"function" command

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