[isabelle] Fwd: Sledgehammer all subgoals?



(resend, after sending from wrong email address)

On 15 September 2015 at 11:34, Larry Paulson <lp15 at cam.ac.uk> wrote:

> On 15 Sep 2015, at 11:05, Tom Ridge <tom.j.ridge at googlemail.com> wrote:
>
> If it is not too much effort to add, this feature would be quite useful to
> me (and to others?). Presumably the implementation is easy - conjunct-up
> the goals and feed them to sledgehammer?
>
>
> This particular suggestion would not work. You would get nothing unless
> all the goals could be solved, and forming the conjunction of two problems
> is particularly damaging for resolution (to see why, consider the details
> of the translation into clause form).
>

Do you really mean the approach won't work? Yes, if one of the goals cannot
be solved, you get nothing, but that is OK for my use case, and is one
possible interpretation of what "sledgehammer all goals" should mean (the
other being that those goals that can be solved, are solved, and the others
are untouched). Surely the approach of "conjuncting-up" is not worse than
invoking sledgehammer twice? (My expectation is that if there is shared
structure between the proofs, the performance might even be better.)


>
> Canât you identify the difficult case simply by looking at it? And
> possibly the simp_all method could be of use here.
>

In this case, given the lack of this feature, I have indeed manually proved
the goals (by invoking various procedures several times). But I'm looking
for functionality that allows me to avoid doing this.

BTW happy birthday!

T



>
>
> Larry Paulson
>
>
>
>



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