*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Slow rule application in case of many parameters?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 18 Mar 2009 09:18:20 +1100*Cc*: isabelle-users at cl.cam.ac.uk, Dennis Walter <dennis.walter at gmail.com>*In-reply-to*: <DB2AEA81-5E48-4F07-B4DD-57F9D26CBC8D@cam.ac.uk>*References*: <7a5c95d30903151332q3d819484y7108034b365b65e7@mail.gmail.com> <DB2AEA81-5E48-4F07-B4DD-57F9D26CBC8D@cam.ac.uk>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Lawrence Paulson wrote:

It looks like you are working on rather large problems! Still I don'tthink such runtimes should be normal. Are you using Poly/ML? Does yourmachine have ample memory?Larry Paulson On 15 Mar 2009, at 20:32, Dennis Walter wrote:Hi all, 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? Thanks a lot, Dennis

REPEAT (rtac allI 1 ORELSE rtac impI 1 ORELSE etac conjE 1) (or perhaps REPEAT1) so try instead REPEAT_DETERM (rtac allI 1 ORELSE rtac impI 1 ORELSE etac conjE 1)

Jeremy

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

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

- Previous by Date: [isabelle] Brilliant but broken theory
- Next by Date: [isabelle] INRIA post-doc position on proof reconstruction from SMT solvers
- Previous by Thread: Re: [isabelle] Slow rule application in case of many parameters?
- Next by Thread: Re: [isabelle] Slow rule application in case of many parameters?
- 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