Email Gateway (Aug 22 2022 at 20:24): Email Gateway (Aug 22 2022 at 20:24):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Dear Isabelle Users,
I have another question about locales, mostly orthogonal to my last one.
As part of a project on trying to describe semantics of certain kinds of
syntax trees in a modular way, I am in a situation where I am trying to do
a few nested levels of locale interpretation. Based on my understanding of
Isabelle locales, I think that I should be able to achieve this by simply
writing an "interpretation" statement (interpreting an "inner" locale)
inside of a ("outer") locale body.
What I expect to happen is that when I interpret the outer locale (say,
into a theory) the definitions from the inner locale also get pulled in,
because they should have been included in the outer locale by virtue of the
interpretation included in that locale's body definition.
Specifically (making reference to the attached .thy file, which is very
contrived but showcases the behavior that I find confusing)
I define a locale called Inner, which takes a function called denote,
which has type " 'a => nat"
Inside inner, I define a function isGood, which sees of the denotation of
a 'a is equal to 0
After closing Inner, I define a locale called Outer, which is almost the
same as Inner except that it takes as a parameter a function called
denote2, which has type " 'a => wrapnat", where wrapnat is isomorphic to
(but distinct from) nat
Inside of Outer, I define a function called denote' that runs denote2 and
"unwraps" the natural number it returns
Finally, still in Outer, I define an interpretation of Inner, InnerInt1,
passing in denote' as the implementation of denote
After closing Outer, I attempt to interpret Outer into the theory. The
command appears to succeed, but the constant OuterInt.InnerInt1.isGood does
not seem to have been introduced into the theory. I would have expected it
to be, since I interpreted Outer into the theory, which in turn interpreted
Inner into the theory, which contains isGood.
Intuitively I had expected that using interpretation inside a locale
context would achieve this, but it seems like there is something I don't
fully understand going on here. I have considered whether sublocales could
be used for this purpose, but I am not sure they are what I want. I don't
want to change the locale hierarchy, I just want to interpret the
definitions from one locale into another locale.
I've included a very contrived example of the kind of behavior that I find
surprising in the attached .thy file. (As with my last message, I wrote and
checked this using Isabelle2018).
Thanks again for your help!
--Mario
Locale_Interp_Example.thy
Email Gateway (Aug 22 2022 at 20:24):From: "lammich@in.tum.de" <lammich@in.tum.de>
Hi
Try using the sublocale command, instead of interpretation.
Peter
Email Gateway (Aug 22 2022 at 20:24):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Hi Peter,
Thanks for the tip. I think I misunderstood the purpose of sublocales, but
after experimenting with them a bit earlier today I think I see how they
can be used to do what I wanted to do.
Best,
Mario
Last updated: Apr 23 2024 at 08:19 UTC