Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 09:17):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 22 2022 at 09:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isar experts,

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.

Best,
Andreas

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

Email Gateway (Aug 22 2022 at 09:37):

From: Lars Hupel <hupel@in.tum.de>
A quick look into the sources appears to corroborate your thesis. While
propositions following "shows", "assumes" and "defines" are parsed with
'Parse.propp', the ones following "obtains" are parsed with
'Parse.prop'. The former parses "is", the latter doesn't. Looking
through the history of 'parse_spec.ML' I can't find any evidence of it
being any different in the past.

Cheers
Lars
smime.p7s

Last updated: Apr 19 2024 at 01:05 UTC