[isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

>> So are there any experience reports that the combinatorial explosion in
>> pattern matching in fun/function had to be worked around somehow?  Or do
>> we have to conclude that the pattern complexity of the applications in
>> src/HOL/Decision_Procs is indeed domain-specific?
> I have some experience with the combinatorial explosion in fun. You
> don't need much: just take extended regular expressions (~10
> constructors) and define binary normalizing constructors (by some
> sequential pattern matching on both arguments). The AFP entry
> MSO_Regex_Equivalence is full of ~30 sec fun declarations.
> 
> While this is still on the edge of being bearable, try to add one more
> constructor... (I've seen examples where fun from 10 lines of
> specification produced something like 10^5 simp equations.) In a
> different formalization (AFP entry Formula_Derivatives) where I needed
> to have more then 10 constructors, I had to work around the function
> package by separating the datatype into two and defining the functions
> separately. (In the end, the separation had also positive effects, but
> still it felt like fighting the system when doing it.)

OK, the dragons are still there and not just a historic relic.

> Note that the domain is quite similar to Cooper---syntactic
> manipulations of expressions/formulas---but isn't it what we do quite
> often in Isabelle? Orthogonally, I have no idea, whether recdef would
> have helped me.

I would definitely not suggest to use recdef for any new application…
the open question is whether we have to think about a refinement or
extension of function.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150607/f6904017/attachment.sig>