Re: [isabelle] Locales: Interpretation changes behaviour of locale expression
This is a defect. "name" is the correct reference in B to the definition of "name" in A (since the import of A into B is not qualified).
The defect occurs also for the following less pathological example, where the locale has a parameter:
locale A = fixes x :: 'a begin
definition "name â x"
interpretation foo!: A x for x by (unfold_locales)
This interpretation appears to make the global A.name identical to foo.name, which it shouldn't:
term A.name (* yields "foo.name" *)
As a consequence, the reference in B, which gets expanded to A.name ends up picking foo.name.
This doesn't happen if the interpretation is along a morphism that is a proper instantiation, for example when mapping 'a to bool:
interpretation foo!: A x for x :: bool by (unfold_locales).
Users tend not to make interpretations into theories along renamings or identity morphisms, which might explain why this hasn't been noticed before. In the original example there are no locale parameters and so there's no way to get a morphism other than the identity morphism.
On 23 October, 2015 17:12 CEST, Peter Lammich <lammich at in.tum.de> wrote:
> I ran into the following unexpected behaviour with locales:
> theory Scratch
> imports Main
> locale A begin
> definition "name â True"
> interpretation foo!: A by (unfold_locales) (* If this line is
> removed, everything works as expected. *)
> locale B = A +
> assumes "name" (* Name is a FREE VARIABLE here*)
> When defining locale B, I would have expected "name" to reference to the
> definition in A. However, if there is an interpretation of A before,> "name" is a free variable in the definition of B, and I have no idea how
> to access "name" from A?
> 1. Is this the correct behaviour?
> 2. How to correctly reference "name" from A, in the definition of B?
This archive was generated by a fusion of
Pipermail (Mailman edition) and