Re: [isabelle] Locales: Interpretation changes behaviour of locale expression

Hi Peter,

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 identical to, which it shouldn't:

  term (* yields "" *)

As a consequence, the reference in B, which gets expanded to ends up picking

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> wrote:

> Hi,
> I ran into the following unexpected behaviour with locales:
> theory Scratch
> imports Main
> begin
>   locale A begin
>     definition "name â True"
>   end
>   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*)
> end
> 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?
> Questions:
>   1. Is this the correct behaviour?
>   2. How to correctly reference "name" from A, in the definition of B?
> --
>   Peter

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