[isabelle] any way to increase force search depth?



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.

Any ideas?
-Andrei





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