Re: [isabelle] Auto has to be invoked twice to succeed



apply auto+ also works (the + repeats the given command until it no longer succeeds).

On 07/14/2015 05:27 PM, Joachim Breitner wrote:
Hi Julian,

Am Dienstag, den 14.07.2015, 14:55 +0000 schrieb Julian Brunner:
Dear all,

I came across some interesting behavior with respect to the auto proof
method. In the attached theory, auto has to be applied twice in a row in
order to solve the goal. The first invocation solves the first subgoal and
transforms the second, with the second invocation solving what remains of
the second subgoal. So far, I was under the impression that when invoking
auto, it solves/transforms the subgoals until it cannot do anything else,
guaranteeing that a second invocation fails immediately. Any clues on what
is happening here?

auto has a limit as to how deeply it searches for proofs, and with a
complicated goal, you might well hit that limit, leaving the proof
state in a semi-proven goal a second invocation of auto can solve.

auto has some parameters whose semantics I do not know, but from
experience (auto 4 4), works in these cases. Or try something like
fastforce+.

Greetings,
Joachim





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