*To*: Sigurd Torkel Meldgaard <stm at cs.au.dk>*Subject*: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 9 Sep 2009 08:10:38 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <392528d30909080733k75c9bebeib350047fc82a3d46@mail.gmail.com>*References*: <392528d30909080733k75c9bebeib350047fc82a3d46@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

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 > >

**Follow-Ups**:**Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".***From:*Sigurd Torkel Meldgaard

**References**:**[isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".***From:*Sigurd Torkel Meldgaard

- Previous by Date: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Next by Date: [isabelle] New AFP entry: Ordinals and Cardinals by Andrei Popescu
- Previous by Thread: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Next by Thread: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list