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



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

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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