Email Gateway (Aug 22 2022 at 09:08): Email Gateway (Aug 22 2022 at 09:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Julian,
find attached a more minimal example.
Your suspicion might be true. Parsing locale specifications is a
notoriously difficult business. It will need further rounds of
investigation to see what is really going on here.
Cheers,
Florian
Locale_Read.thy
signature.asc
Email Gateway (Aug 22 2022 at 09:28):From: Julian Brunner <julianbrunner@gmail.com>
Dear all,
I recently stumbled upon the following behavior in Isabelle which I
find surprising and which affects me negatively. In the attached
theory, the locale "bar" is interpreted as "baz", using a 'for' clause
to retain the parameter "x" of the superlocale "foo". When declaring
another sublocale "test" of "foo", it is now impossible to use the
definitions made in "foo" in the assumptions of "test". However, it is
possible to use the definitions made in "foo" in the body of "test".
My guess is that this has something to do with the fact that the
locale "foo" is already interpreted in its most general form as part
of "baz", so the constants do not get interpreted again when declaring
"test" can and only be accessed using the prefix "baz" (although the
parameter "x" is not yet applied there). However, I do not understand
why they can be accessed in the body of the locale "test", but not
while declaring its assumptions.
What's happening here and how can I access these definitions in the
assumptions without using the locale prefix and reapplying all the
parameters?
Regards,
Julian
DefAssumption.thy
Email Gateway (Aug 22 2022 at 10:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Julian,
after having a second look, the reason is quite obvious: the pervasive
interpretation has the consequence that the syntax declarations to
establish z as local constant are not re-issued while setting up the
context for the locale specification.
I don't understand whether this is an inherent necessity or just an
accident.
Cheers,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC