When would you use `presume` in an Isar proof?

Question

Isar has, besides assume, also the command presume to introduce facts in an Isar proof block. From what I can see and read in the docs, it does not require the assumption (presumption?) to be explicitly listed in the goal, and seems to add a case to show that the presumed statement follows from the other goals.

So the question is: When would I use presume instead of assume, and what nice tricks can I do with presume?

Coe

Note that even assume does not require the assumption to be explicit in the goal premises. What counts is that the exported rule from the subproof can be resolved with some goal in the manner that is explained in the isar-ref manual section 2.1.2 Reasoning with rules (refinement). These principles are more general than most people expect, e.g. the goal might be schematic and the application than invents suitable premises via unification. – Irrepressible

Answer 1

presume does not make the Isar language more expressive, because you can restructure every proof with presume into one with assume only. Nevertheless, there are at least two (more or less common) use cases:

First, presume sometimes leads to more natural proofs, because you can use presume like a cut.

For example, suppose that you your proof state has two goals A ==> C and B ==> C, and you can proof that some E follows from A and from B given the facts in the current context and E and the facts in the current context imply C. With presume, you can structure the proof as follows:

   presume E
   show C <proof using E and facts>
   thus C .
 next
   assume A
   thus E <proof using A and facts>
   thus E .
 next
   assume B
   thus E <proof using A and facts>
   thus E .

In assume style, this looks as follows:

   assume A
   hence E <proof using A and facts>
   show C <proof using E and facts>
 next
   assume B
   hence E <proof using B and facts>
   show C <proof using E and facts>

With presume, the structure of the proof is more explicit: Apparently, we only need E to show the results and this might be the interesting part of the proof. Moreover, in assume style, we have to do the proof that E implies C twice. Of course, this can always be factored out into a lemma, but if the proof needs a lot of facts from the context, that can become ugly.

Second, you can use presume while you write a proof to locate typing errors in assumes and shows. Suppose you have

 fix x
 assume A and B and C and D and E
 show F

but Isabelle tells you that the show will not solve any goal, i.e., you probably have some typo in the assumptions or the goal statement. Now, turn assume into presume. If show still fails, then the mistake is somewhere in the goal statement. Otherwise, it is probably somewhere in the assumptions. Close the show proof with sorry and try to discharge the assumptions with apply_end(assumption)+. It will stop at the assumption that it cannot unify. Probably, this is the one that is wrong.

Stateroom

I knew I can expect a good and generally useful answer from you! :-) – Coe

Even with assume, you can extract the proof E ==> C by doing: { assume E have C} first and the nesting the proofs of A ==> C and B ==> C` into proof blocks: { assume A show E } { assume B show E}. You still might find the presume style nicer. – Gainful