Re: [isabelle] primrec of datatype containing fset



And I agree with Andreiâs agreement to Manuelâs disagreement. :)

The question of using primrec or fun shows up every now and then on this mailing list, e.g., here https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00037.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00037.html>.

Next to the reasons brought up by Manuel before, I also particularly agree with Florianâs advice to use the least powerful command as a means of documentation: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00044.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-May/msg00044.html>

Dmitriy


> On 9 Jul 2017, at 16:10, Andrei Popescu <a.popescu at mdx.ac.uk> wrote:
> 
> 
> 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.