Re: [isabelle] primrec of datatype containing fset



Hi Manuel,


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


Best,


Andrei


________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Manuel Eberl <eberlm at in.tum.de>
Sent: 09 July 2017 12:54:12
To: cl-isabelle-users at lists.cam.ac.uk
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.

Manuel


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 in.tum.de> 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.