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.haftm...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev