presume does not make Isar more expressive, because you can rearrange every proof with presume only to assume . However, there are at least two (more or less common) use cases:
Firstly, presume sometimes leads to more natural evidence, because you can use presume as a cut.
For example, suppose your proof has two goals A ==> C and B ==> C , and you can prove that some E follows from A and B , given the facts in the current context and E and the facts in the current context mean 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 assume it looks like this:
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 structure of the proof is clearer: apparently, we need only E show the results, and this can be an interesting part of the proof. Moreover, in the style of assume we must prove that E implies C twice. Of course, this can always be taken into account in the lemma, but if proof requires a lot of facts from the context, it can become ugly.
Secondly, you can use presume while you write the proof to find input errors in assume and show s. Suppose you have
fix x assume A and B and C and D and E show F
but Isabelle tells you that show will not solve any goal, i.e. you probably have a typo in assumptions or statement of purpose. Now turn assume into presume . If show still fails, the error will be somewhere in the target declaration. Otherwise, it is probably somewhere in the assumptions. End the show proof with sorry and try to fulfill the assumptions with apply_end(assumption)+ . He will stop on the assumption that he cannot unite. This is probably not true.