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

I tried to, but failed in the amount of time I've got right now. The
concrete problem is a little too large (and dependent on other
theories) to show here.

The structure of the subgoal is sth like this:

! n1 n2 n3 n4 n5 n6 n7 n8 n9.
[| P1 n1 ... n9 & P2 n2 ... n9 & P3 n3 ... n9 & ...|] ==>
ALL S. f S' = S -->
(ALL S1. f S = S1 -->
(ALL S2. f S2 = S1 -->
 (... -->
(let v = g S in
  ALL S'. f S = S' -->
    (let v = g S' in
      ALL S. f S' = S -->
          in P n1 n2 n3 n4 n5 n6 n7 n8 n9)...)

where the P_i aren't just constants / free variables, but complex
terms referring to the n_i. When I do "apply (rule allI, rule impI,
erule conjE)" with about 30 possible rule applications, it takes
around one minute.

I'll try to come up with a concrete example later.


On Mon, Mar 16, 2009 at 2:53 PM, Makarius <makarius at> wrote:
> 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?
>        Makarius

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