[isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> The reason for the continued existence of recdef is that function can
> cause a combinatorial explosion the way it compiles pattern matches. I
> just tried Cooper.thy and changing one of the recdefs to function makes
> Isabelle go blue (purple) in the face until one gives up. Hardware alone
> will not solve that one.
> 
> Now one could argue that since we need recdef, we should also keep the
> special variant defer_recdef, but if nobody speaks up for it, we don't
> have a proof that we really need it and it should go.

At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

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?

	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/20150606/32d560c4/attachment.sig>