I am trying to understand the difference between the shows and obtains commands in Isar (as of Isabelle 2020). The documentation in isar-ref.pdf (pp 137.) seems to have some typo and confuses me.
... Moreover, there are two kinds of conclusions: shows states several simultaneous propositions (essentially a big conjunction), while obtains claims several simultaneous simultaneous contexts of (essentially a big disjunction of eliminated parameters and assumptions, cf. §6.6).
shows seems straight forward.
From the limited experience I have so far, it seems that obtains is about proving a conclusion that begins with an existential quantifier, as shown in this question (where the conclusion is existential and then the goal is a obtains).
Is this really the distinction between shows and obtains (universal vs existential)?
If not, what is the proper intended use of obtains?
The lemmas "shows ‹∃x. P x›" and "obtains x where ‹P x›` are very similar, but not entirely identical.
In terms of proofs, the obtain version requires to find an explicit witness (look the fact called that in such a proof). Something similar can be achieved by applying the theorem exI after the shows.
The generated lemmas are different. The obtains version generates an elimination rule instead of a quantified, because there is no existential quantifier in Pure. However, the difference rarely matters when using the theorem.