what's the distinction between `shows` and `obtains` in Isabelle Isar?

0
votes

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?

1
isabelleisar
obtains is the version of obtain that works right after lemmas, like shows/show or assumes/assume. Makarius did not pick the names by accident. Do you understand the explanation of obtain in the prog-prove? – Mathias Fleury
@MathiasFleury Thanks for the hints. The examples of obtain in prog-prove (among others) are the first thing I read. I couldn't understand because they are somewhat magical. The examples themselves work but I often couldn't get it to work on other data. There is usually no further analysis than the working examples. I guess the example set isn't large enough to cover all the combinations in practice. Hence the questions about its grammar, e.g. whether obtains translate to existential quantification etc., so that I can understand the semantics in ordinary mathematical sense. – tinlyx

1 Answers

0
votes

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.