Email Gateway (Aug 18 2022 at 20:08): Email Gateway (Aug 18 2022 at 20:08):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 20:28):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Email Gateway (Aug 18 2022 at 20:28):From: Johannes Hölzl <hoelzl@in.tum.de>
You can use "oops". The theorem is not proved, but you are back to the
top level and you can start a new theorem.
Email Gateway (Aug 18 2022 at 20:28):From: John Wickerson <jpw48@cam.ac.uk>
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.
Last updated: Apr 19 2024 at 20:15 UTC