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