[isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

The reason for the continued existence of recdef is that function can cause a 
combinatorial explosion the way it compiles pattern matches. I just tried 
Cooper.thy and changing one of the recdefs to function makes Isabelle go blue 
(purple) in the face until one gives up. Hardware alone will not solve that one.

Now one could argue that since we need recdef, we should also keep the special 
variant defer_recdef, but if nobody speaks up for it, we don't have a proof that 
we really need it and it should go.

Tobias

On 06/06/2015 13:23, Makarius wrote:
> On Sat, 6 Jun 2015, Larry Paulson wrote:
>
>> I’d be happy to see the complete phasing out of TFL. It’s had its day. It was
>> always a tricky thing to maintain. I’m amazed that it still works despite all
>> of the many fundamental changes to system APIs.
>
> There are actually two remaining parts of TFL:
>
>    (1) 'recdef' which is still used in Isabelle + AFP applications, but
>      very rarely and some effort could be made to get rid of it.
>
>    (2) 'defer_recdef' which is unused in the directly visible Isabelle
>      universe.  So it could be deleted today.
>
> This mailing list thread is an opportunity to point out dark matter in the
> Isabelle universe, where 'defer_recdef' still occurs.  Otherwise I will remove
> it soon, lets say within 1-2 weeks.
>
>
> Apart from that we should also work on (1) eventually.  It has become a ritual
> to ask about the purpose of old 'recdef', and it usually leads to the result as
> "still needed" for odd reasons that I then forget immediately.  So I have
> developed a reluctance to ask again.
>
>
>      Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150606/dc5bf9ba/attachment.bin>