Re: [isabelle] A sorry qed
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:
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.
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,
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
(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
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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