Re: [isabelle] Raw proof blocks



On 19.10.2014 18:35, 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.'

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




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