Email Gateway (Aug 19 2022 at 16:20): Email Gateway (Aug 19 2022 at 16:20):From: "W. Douglas Maurer" <maurer@gwu.edu>
In section 2.6 ("Raw proof blocks") of "A Tutorial Introduction to
Structured Isar Proofs," there appears the following sentence at the
top of page 13: "Note that the conclusion of a raw proof block is
stated with 'have' rather than 'show' because it is not the
conclusion of some pending goal but some independent claim." Yet in
theory Fields, in the section (14.1) on division rings, there is a
proof of the right-inverse-eq lemma that contains a raw proof block
(at least I assume it is a raw proof block -- it is contained in
curly brackets) that ends in 'show.' Is this just a bug, or is it a
version of raw proof blocks that isn't described in the Tutorial
Introduction?
Email Gateway (Aug 19 2022 at 16:20):From: Makarius <makarius@sketis.net>
Whenever the meaningless word "bug" comes up, there is a high chance that
it is a misunderstanding of the user.
A tutorial is not necessarily complete and exhaustive, in contrast to a
reference manual. Isabelle has lots of manuals with different approaches
to explain things. Ultimately the authoritative source for Isar is the
isar-ref manual (and of course the implementation). So if the system
accepts some proof text, it is probably right.
According to the inner workings of Isar, it is of course possible to use
raw proof blocks { } together with fix-assume-show of regular proof
bodies. It is not used very often, but it definitely has its uses. It
allows to manage local contexts with further depth, instead of the
immediate default context of the original goal statement.
You can also use the block separator 'next' within { } even though some
explanations sometimes tell a different story.
Makarius
Email Gateway (Aug 19 2022 at 16:20):From: Makarius <makarius@sketis.net>
It is a reference manual, which means you don't read it from start to end
in one go, but look occasionally if there are relevant bits and pieces.
Taking all that information together, some mental picture of what Isar
actually is should emerge. You should skim through the table of contents
to get an idea of the different areas that are covered.
Chapter 6 is about proofs. Section 6.1 about proof structure. Blocks are
described in 6.1.2 --- some abstract text about that concept. At least it
says something about 'next' and also mentions 'show' in a way that
indicates that it can be used here.
BTW, the current version of Isabelle is from August 2014 and the manual
has the same date. As a habit you should follow the normal Isabelle
release cycle, unless there are special reasons to stick to an older
version.
Makarius
Email Gateway (Aug 19 2022 at 16:21):From: Lars Noschinski <noschinl@in.tum.de>
The difference between show and have is that show uses the proven fact
to discharge a pending proof obligation.
Now, when you open a raw proof block, you don't setup a proof obligation
to be discharged in this block, so there is no need to use show there.
Rather, the last fact mentioned in this block (whether this be by means
of have or e.g. note) is exported, when you close the block.
However, even though you don't setup a proof obligation to be discharged
in a raw proof block, you can still discharge all the pending proof
obligations which were there before you open the proof block -- and for
this you use show, as you would usually do.
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC