*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".*From*: Sigurd Torkel Meldgaard <stm at cs.au.dk>*Date*: Thu, 10 Sep 2009 11:26:22 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <cc2478ab0909090810n3aca44abr73950b86ce6ce0b4@mail.gmail.com>*References*: <392528d30909080733k75c9bebeib350047fc82a3d46@mail.gmail.com> <cc2478ab0909090810n3aca44abr73950b86ce6ce0b4@mail.gmail.com>*Sender*: yogurth at gmail.com

Thanks for the pointers, I think I have a better understanding now. Maybe metalogic connectives should be disallowed in subgoals of Isar proofs? Or trigger some warning... Anyways thanks again for the help! Sigurd On Wed, Sep 9, 2009 at 5:10 PM, Brian Huffman<brianh at cs.pdx.edu> wrote: > 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 >> >> >

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

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

- Previous by Date: [isabelle] Deadline extended: Software Verification and Testing at ACM SAC 2010
- Next by Date: [isabelle] implementation of SSL?
- Previous by Thread: Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
- Next by Thread: [isabelle] New AFP entry: Ordinals and Cardinals by Andrei Popescu
- 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