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:
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
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and