[isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy?
Larry

> On 6 Jun 2015, at 16:11, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
>> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev