Re: [isabelle] A sorry qed

Hi Joachim,

you can exploit one of Isar's features. When you do a fix-assume-show, Isar merely tries to unify this sequence with one of the goals. You do not need to state the precise goal. Hence, you can do something like the following:

  fix P
  show P P P P P P P P P P sorry

where the number of P's in the show statement equals the number of unproven cases. Although this is not as concise as a sorry qed, it should be doable.


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:

Right now I was in the middle for a multi-case induction proof,
something like

        have "foo"
        proof(induct ...)
        case (A ...)
          show ?case by ...
        case (B ...)
          show ?case by ...

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

        show "foo" sorry

but of course "foo" is not the current goal any more. Things like

        qed sorry




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


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 - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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