[isabelle-dev] Remaining uses of defer_recdef?
nipkow at in.tum.de
Mon Jun 8 13:52:46 CEST 2015
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.
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.
>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev