Email Gateway (Feb 01 2023 at 08:01): Email Gateway (Feb 01 2023 at 08:01):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I have noticed some some peculiar behaviour with global locale interpretations and a theory import diamond.
Consider a diamond in a theory import graph:
Base
/ \
Extend Interpret
\ /
Use
We define a locale in theory Base and extend it (adding definitions and lemmas) in theory Extend.
Moreover, we provide a global interpretation of the locale in theory Interprete.
As expected within theory Interpret the extensions to the locale are not available for the interpretation.
But also after merging Extend and Interpret into theory Use the extensions are not made available for the interpretation.
I have an idea why this happens in the current implementation. But is this the expected behaviour?
Note that when providing a (global) interpretation in theory Use, all extensions are available.
Regards,
Norbert
Base.thy
Extend.thy
Interpret.thy
Use.thy
Email Gateway (Feb 01 2023 at 17:41):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Norbert,
the behaviour you observe is intended. It is even documented (towards
the end of section 5.7.3 Locale interpretation in the Isar Ref Manual):
If a global theory inherits declarations (body elements) for a locale
from one parent and an interpretation of that locale from another
parent, the interpretation will not be applied to the declarations.
Clemens
Email Gateway (Feb 02 2023 at 08:36):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Hi Clemens,
Ok. Then it would be nice to have a mechanism to update (or redo) the interpretation in the merged theory.
Reworking the import graph (e.g. by putting theory Interpret after theory Extend) might not be a good option, e.g. in case theories Extend and Interpret come from different libraries.
Regards,
Norbert
Last updated: Apr 20 2024 at 08:16 UTC