[isabelle] Locales: Interpretation changes behaviour of locale expression

[Peter Lammich]

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

[Peter Lammich]

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.<br><br>Enviado através de Huawei Mobile<div class="quote" style="line-height: 1.5"><br><br>-------- Originalnachricht --------<br>Betreff: Re: [isabelle] Locales: Interpretation changes behaviour of locale expression<br>Von: Clemens Ballarin <***@in.tum.de><br>An: Peter Lammich <***@in.tum.de><br>Cc: isabelle-users <isabelle-***@cl.cam.ac.uk><br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Peter,<br><br>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).<br><br>The defect occurs also for the following less pathological example, where the locale has a parameter:<br><br> locale A = fixes x :: 'a begin<br> definition "name ≡ x"<br> end<br><br>
interpretation foo!: A x for x by (unfold_locales)<br><br>This interpretation appears to make the global A.name identical to foo.name, which it shouldn't:<br><br> term A.name (* yields "foo.name" *)<br><br>As a consequence, the reference in B, which gets expanded to A.name ends up picking foo.name.<br><br>This doesn't happen if the interpretation is along a morphism that is a proper instantiation, for example when mapping 'a to bool:<br><br> interpretation foo!: A x for x :: bool by (unfold_locales).<br><br>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.<br><br>Clemens<br><br><br><br>On 23 October, 2015 17:12 CEST, Peter Lammich <***@in.tum.de> wrote:<br><br>> Hi,<br>><br>> I ran into the following unexpected behaviour with locales:<br>><br>> theor
y Scratch<br>> imports Main<br>> begin<br>><br>> locale A begin<br>> definition "name ≡ True"<br>> end<br>><br>> interpretation foo!: A by (unfold_locales) (* If this line is<br>> removed, everything works as expected. *)<br>><br>> locale B = A +<br>> assumes "name" (* Name is a FREE VARIABLE here*)<br>><br>> end<br>><br>><br>> When defining locale B, I would have expected "name" to reference to the<br>> 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<br>> to access "name" from A?<br>><br>> Questions:<br>> 1. Is this the correct behaviour?<br>> 2. How to correctly reference "name" from A, in the definition of B?<br>><br>> --<br>> Peter<br>><br>><br>><br>><br>><br><br><br><br><br><br><br><br></blockquote></div>