Re: [isabelle] Raw proof blocks

On Sun, 19 Oct 2014, W. Douglas Maurer wrote:

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?

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.



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