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:

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

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.

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