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!

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.