Re: [isabelle] any way to increase force search depth?



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.
>
>





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