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:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-April/msg00052.html

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 cs.au.dk> 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.