[isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

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.