Re: [isabelle] Strange behavior in isabelle 2009, *** Failed to finish proof *** At command "qed".
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!
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:
> 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
>> 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