Re: [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.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

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev