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



This was a boiled down example. The original example had a parameter, and i used the interpretation to get code theorems for the constants defined in this locale.

Enviado atravÃs de Huawei Mobile


-------- Originalnachricht --------
Betreff: Re: [isabelle] Locales: Interpretation changes behaviour of locale _expression_
Von: Clemens Ballarin
An: Peter Lammich
Cc: isabelle-users


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"
end

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.

Clemens



On 23 October, 2015 17:12 CEST, Peter Lammich 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.