*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] any way to increase force search depth?*From*: Andrei Borac <zerosum42 at gmail.com>*Date*: Mon, 31 May 2010 17:00:03 -0700*In-reply-to*: <3B570047-8C68-4E3E-B7AB-DAEF679F9FC6@cam.ac.uk>*References*: <AANLkTilIS1IVhHdyVUvEe3tgJUdNSOJIGlZbKX8-I402@mail.gmail.com> <3B570047-8C68-4E3E-B7AB-DAEF679F9FC6@cam.ac.uk>

Well, if it is doing a best-first search, which I take to be exhaustive, it does not seem as if the search is over all possible UIs. Applying force to the unrefined subgoal gives up (rather quickly) ... manually instantiating the quantifiers is not really an option, as there are 269 subgoals ... I got here because I assumed that force can find the instantiation that works (and it has been able to do similar proofs, this one just has slightly more complex stuff under the quantifier). Additionally, I found that simp is sufficient to solve the subgoal after manual instantiation: apply(erule_tac x="..." in meta_allE) apply(erule_tac x="..." in meta_allE) apply(erule_tac x="..." in meta_allE) apply(simp) So, my speculation at this point is that force does not blindly try UIs, but looks for some correlation between the stuff in the UI and the other facts in the assumption block. What I am thinking is the best option at this point is to write some kind of control program that will interact with Isabelle, first inserting the thy file up the current point and then try all possible (type-sane) instantiations followed by force until one succeeds ... after a long time, I will have a long script that can be cut & paste into the thy file ... perhaps it would even be possible to run regular expressions on the assumption facts to make good guesses at the required UI. At this point, it would sorta help me out if I knew the incantation to turn on "quick and dirty mode" in the Isabelle shell. Or perhaps someone can give me few pointers to places in Isabelle's source or code samples that are relevant to writing such a trial and error tactic in ML? -Andrei On Mon, May 31, 2010 at 11:49 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > Looking at the code, I see that force has no search depth, but performs a best-first search. You haven't stated whether it gives up or runs forever, but I would expect the latter. If you can make it work by instantiating a couple of quantifiers, that's probably the simplest thing to do. Tuning a reasoning tactic to your specific requirements would probably take quite a long time. > > Larry Paulson > > > On 30 May 2010, at 23:33, Andrei Borac wrote: > >> First off, sorry for not posting the actual real problem at hand, but >> there quite a number of definitions that would have to be brought in. >> >> I have a subgoal that can be solved by "force" if I first specify a >> universal instantiation (UI) of an expression with three variables: >> >> apply(erule_tac x="..." in meta_allE) >> apply(erule_tac x="..." in meta_allE) >> apply(erule_tac x="..." in meta_allE) >> apply(force) >> >> "force" has been able to do universal instantiation in the past ... >> however, this time: >> (1) there is a lot of stuff in the assumptions block >> (2) some amount of simplification is required after UI including >> following the appropriate branch of nested case expressions >> >> Is there a way to get force to try harder, or use some other kind of >> automated method? Note that I have tried ATPs but it seems as they >> have difficulty doing the simplifications required after UI (just a >> guess, I don't actually know how these tools work). To split the >> case/options before instantiation cannot be done by simp split and >> would have to be done semi-manually (to split into multiple >> universally quantified expressions) which I might try but looks >> tedious at best and might not even help. > >

**Follow-Ups**:**Re: [isabelle] any way to increase force search depth?***From:*Jeremy Dawson

**Re: [isabelle] any way to increase force search depth?***From:*Lawrence Paulson

- Next by Date: [isabelle] is it right?
- Next by Thread: Re: [isabelle] any way to increase force search depth?
- Cl-isabelle-users June 2010 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