Re: [isabelle] Re-interpretation of locales does not generate abbreviations



Hi Peter,

This feature has been discussed already twice this year on the mailing list:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-September/msg00019.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-February/msg00076.html

Clemens' locale implementation paper describes this as a feature, because it allows certain types of cyclic locale hierarchies, so I would expect that it won't change.

Best,
Andreas

On 13/11/13 19:40, Peter Lammich wrote:
I encountered the following odd behaviour:
When interpreting a locale with a prefix, the expected abbreviations are
only generated if the locale has not been interpreted before with the
same parameters.

This feature is quite confusing, as it makes modular design more
difficult: If you need an instance of a locale for your theory, you must
make sure that none of the theories you are importing has already
instantiated this locale, and otherwise use the other theory's
instantiation.

Is there any workaround, or plans to change this behaviour? [Or good
reasons to keep it as is?]

Example:

locale foo begin
   definition "bar \<equiv> True"
end

interpretation p1!: foo by unfold_locales
interpretation p2!: foo by unfold_locales

term p1.bar
term p2.bar (* Does not exist! *)


Regards
   Peter






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