[isabelle] Definitions of Superlocale Cannot be Accessed in Assumptions



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

Attachment: DefAssumption.thy
Description: Binary data



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