Re: [isabelle] Slow rule application in case of many parameters?

On Sun, 15 Mar 2009, Dennis Walter wrote:

I'm having problems solving large structured goals involving many parameters. Even rule applications like apply (rule allI | rule impI | erule conjE)+ take several minutes. I've experienced this slowdown in cases where the number of parameters (bound meta-variables) is > 30, and these repeatedly occur in various places within the goal (~2000 lines, no abbreviations). I suspect that Isabelle's lifting of rules over parameters is to blame, but I can't see why this should be the case. Can anybody explain this phenomenon to me?

Incidently, I've come across a similar situation just 2 weeks ago, with approx. 10 parameters and 10 premises in the goal, but the same numbers in the rule being applied. It took several minutes to apply the rules.

Can you produce a selfcontained example of your application, so that we can get check if this is really the same hot spot?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.