Re: [isabelle] A sorry qed



Hm, but the problem there is that with "sorry" you can use the unsafe theorem in later lemmas, but with "oops" the theorem can't be used later.

On 19 Jun 2012, at 09:03, Johannes Hölzl wrote:

> You can use "oops". The theorem is not proved, but you are back to the
> top level and you can start a new theorem.
> 
> - Johannes
> 
> Am Montag, den 18.06.2012, 16:32 +0200 schrieb Joachim Breitner:
>> Hi,
>> 
>> Right now I was in the middle for a multi-case induction proof,
>> something like
>> 
>>        have "foo"
>>        proof(induct ...)
>>        case (A ...)
>>          ...
>>          show ?case by ...
>>        next
>>        case (B ...)
>>          ...
>>          show ?case by ...
>>        next
>> 
>> with many cases remaining. At this point, I wanted to stop working on
>> this proof and do something else. With apply-scripts I’d just write
>> "sorry" instead of "done" and be done with it. But what can I do here,
>> besides writing down each missing case and solving it with "sorry"? I
>> tried
>> 
>>        show "foo" sorry
>>        qed
>> 
>> but of course "foo" is not the current goal any more. Things like
>> 
>>        qed sorry
>> 
>> or
>> 
>>        apply_end(sorry)
>>        qed
>> 
>> or
>>     qed(cheating)
>> 
>> (the “cheating” coming from A.1.3 of isar-ref, but seemingly not meant
>> literarly) of course don’t make sense either. Is there a clean way to
>> stop the proof here?
>> 
>> Thanks,
>> Joachim
>> 
>> 
> 
> 
> 






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