*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Slow rule application in case of many parameters?*From*: Dennis Walter <dennis.walter at gmail.com>*Date*: Mon, 16 Mar 2009 18:14:34 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.0903161448390.8214@atbroy100.informatik.tu-muenchen.de>*References*: <7a5c95d30903151332q3d819484y7108034b365b65e7@mail.gmail.com> <alpine.LNX.1.10.0903161448390.8214@atbroy100.informatik.tu-muenchen.de>

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. Dennis On Mon, Mar 16, 2009 at 2:53 PM, Makarius <makarius at sketis.net> 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 >

**References**:**[isabelle] Slow rule application in case of many parameters?***From:*Dennis Walter

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

- Previous by Date: [isabelle] Displaying some element of a list of facts
- Next by Date: [isabelle] A set is not its own member
- Previous by Thread: Re: [isabelle] Slow rule application in case of many parameters?
- Next by Thread: [isabelle] Proof failed using rules
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list