[isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

A frequent use case is this: you have 5-10 interesting patterns where stuff 
happens and an otherwise pattern with a simple rhs. In that case you do want to 
write those 5-10 patterns explicitly and let the definition facility take care 
of the hundreds of patterns that the default case expands to. You don't really 
care that the induction has hundreds of cases because they are trivial. In 
contrast, rewriting such a definition to avoid the blowup is a pain in the 
backside and is not guaranteed to make proofs simpler.

Tobias

On 07/06/2015 21:46, Larry Paulson wrote:
> I suggest looking for ways for users to avoid exponential blowup. Presumably this means avoiding deeply nested patterns in favour of conditional expressions in some cases. Such a formalisation might be easier to reason with too, who wants an induction rule with hundreds of cases?
>
> But coming up with simple guidelines for users might be tricky.
>
> Larry
>
>> On 7 Jun 2015, at 20:33, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>
>> As far as I know, this is due to layered architecture of the function
>> package.  »recdef« does everything in one bunch and can hence optimize
>> for sequential pattern matching.  Each layer of »function« must feed its
>> result to its successor in a standardized form, and since there is no
>> overall concept of sequential pattern matching, it has to be compiled
>> away once and for all from the very beginning. (roughly spoken)
>>
>> An optimization would require a modified architecture.
>
> _______________________________________________
> 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/20150608/820ed425/attachment.bin>