Re: [isabelle] A sorry qed



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.