Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
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.
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
> 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
> definition "C a b ≡ b < a"
> lemma a:
> shows "⟦C u u⟧ ⟹ True"
> and "⟦True⟧ ⟹ C u u"
> proof -
> show "⟦C u u⟧ ⟹ True"
> show "⟦True⟧ ⟹ C u u"
> I hope somebody sees what I or Isabelle is doing wrong ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and