*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] A sorry qed*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 20 Jun 2012 08:39:00 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <BC97D36E-2D56-4457-A25D-AD5C3C8249D4@cam.ac.uk>*References*: <1340029953.19975.3.camel@kirk> <1340092988.28571.19.camel@macbroy12.informatik.tu-muenchen.de> <BC97D36E-2D56-4457-A25D-AD5C3C8249D4@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Hi Joachim,

next fix P show P P P P P P P P P P sorry qed

Andreas Am 19.06.2012 12:26, schrieb John Wickerson:

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

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] A sorry qed***From:*Joachim Breitner

**Re: [isabelle] A sorry qed***From:*Johannes Hölzl

**Re: [isabelle] A sorry qed***From:*John Wickerson

- Previous by Date: [isabelle] Phd Positions available
- Next by Date: Re: [isabelle] code-relect features
- Previous by Thread: Re: [isabelle] A sorry qed
- Next by Thread: [isabelle] code-relect features
- Cl-isabelle-users June 2012 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