Re: [isabelle] Syntax diagram for obtains allows "is" bindings



On Thu, 9 Apr 2015, Andreas Lochbihler wrote:

The syntax diagrams in the isar-ref manual (section 6.2.4) for obtains allow is-bindings for the propositions in where clauses - at least that is how I understand them. Unfortunately, I get syntax errors at "(" when I try to use them as in

lemma obtains y ys where "x = y # ys" (is "?foo y ys")

Apparently, the documentation and the system do not agree in this case. Also, the syntax diagram for "case" misses the possibility of not binding variables and omitting the where part.

I will change the documentation to fit better to the implementation.


PS: Two unanswered posts are related:
https: //lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-November/msg00002.html https: //lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-June/msg00050.html

This is all about "is" within the hypothetical context of 'obtain' or 'obtains'. It is in principle possible to get this right, but when these elements where first implemented, many reforms of Isabelle syntax (parse, check, term export) where not yet there. Today it should probably work out smoothly.

For the past 5 releases or so, I always tried to re-open this can, but never got back to it on time. The reason why it is both important and dangerous to be revisited is that there are some fundamental improvements in the pipeline that want to get out, but will take quite some efforts. E.g. 'obtain' with multiple branches inside a proof, like 'obtains' already does for statements, and a notation for "eigen contexts" (like the sporadic 'for' declarations that have popped up here and there).


	Makarius




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