Re: [isabelle] Sledgehammer all subgoals?

On Di, 2015-09-15 at 10:11 +0100, Larry Paulson wrote:
> I don't believe that such an option exists. Even with one goal, you are spawning up to 5 subprocesses on your machine. The idea anyway that you are trying to tackle a particularly tough problem, so it's natural to tackle them one at a time.

> I wonder: is there much demand for this option?

Another use-case of sledgehammer is just to find the necessary theorems to 
easily solve a goal. Sledgehammer will not find hard proofs itself, but 
is very good at deducing proofs from theorems the user did not even know about.

Assuming sufficient computing power is available, a (auto-) sledgehammer
on all sub-goals in the background would imho be useful: Ideally, while
you are trying to prove the first sub-goal manually, sledgehammer
already solves the others for you.


> Larry
> > On 15 Sep 2015, at 09:14, Tom Ridge via Cl-isabelle-users <cl-isabelle-users at> wrote:
> > 
> > Dear All,
> > 
> > Sorry for the easy question, but I couldn't find the answer in the
> > documentation.
> > 
> > How can I apply sledgehammer to solve all subgoals?
> > 
> > e.g.
> > 
> > lemma "True & True"
> > apply(rule)
> > 
> > At this point, if I click on the "Sledgehammer" tab in jedit and click
> > apply, it shows me a solution to the first goal. But I want it to solve all
> > the goals.
> > 
> > Thanks

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