Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".

Hi Sigurd,

There was a discussion of a similar problem on the list back in April:

In the follow-up comments you will find some explanations of what is
going on behind the scenes. It turns out that low-level proof-state
manipulations like "prefer 2" might make your proof script work, but
the recommended solution is to avoid "==>" in subgoals and use
assume/fix instead, as Florian suggested.

- Brian

On Tue, Sep 8, 2009 at 7:33 AM, Sigurd Torkel Meldgaard<stm at> wrote:
> It seems that sometimes it is not enough to show all goals for qed to
> finish the proof.
> The smallest example I have been able to make is the following (the
> lemma is not true, but because of "sorry" it should be accepted
> anyways.)
> In proof general all lines before qed are accepted, but when I try
> next-step, it gives me: *** Failed to finish proof
> *** At command "qed".
> theory T
> imports Main
> begin
> definition "C a b ≡ b < a"
> lemma a:
> shows "⟦C u u⟧ ⟹ True"
>  and "⟦True⟧ ⟹ C u u"
> proof -
>  show "⟦C u u⟧ ⟹ True"
>    sorry
>  show "⟦True⟧ ⟹ C u u"
>    sorry
> qed
> end
> I hope somebody sees what I or Isabelle is doing wrong ;)
> Sigurd

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