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



That was also Manuel's first idea when I told him about it. However, it
doesn't seem to have any effect here, as even (auto 100 100) doesn't solve
the goal. Also, my interest here is less about finding a convenient proof
(auto+ does it just fine, after all), and more about figuring out what is
going on.

On Tue, Jul 14, 2015 at 5:29 PM Joachim Breitner <breitner at kit.edu> 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
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner
>



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