Email Gateway (Aug 18 2022 at 13:44): Email Gateway (Aug 18 2022 at 13:44):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I encountered a problem/bug(?) with locales and imported theories.
I have four theories:
def: Defines a locale
add: Adds some lemma to the locale
inst: Interprets the locale, but does not import add
use: Imports add and inst
The problem is, that I need to use the added lemma in the
interpretation. However, it is not visible in the theory "use".
Even more strange things happen, if I try to reinterpret the locale in
theory "use": The re-interpretation (done with a different prefix name)
adds no lemmas, neither the ones originally defined in the locale, nor the
ones added by the theory "add".
The only workarounds that I can currently figure out is instantiating
the missing lemmas by hand, i.e. lemmas xyz_lem = locale_name.lem[OF
xyz_is_interp] or trying to change the structure of the imports-graph.
Is there some better method how to get the desired lemmas, especially
the ones that are declared as [simp] and hence should be filled into the
simpset?
Regards,
Peter
Here follows a boiled-down example: (I also attached a tgz with the four
thy-files)
theory "use"
imports inst add
begin
thm int.orig -- "Works"
thm l.added -- "The theorem is in the locale"
(* thm int.added -- "Does not work ... ok, would have to be merged on
import" *)
interpretation xxx: l .
-- "The namespace below xxx seems to be empty ?"
thm xxx.orig -- "Does not work"
thm xxx.added -- "Does not work"
end
theory "def"
imports Main
begin
locale l
begin
lemma orig: True ..
end
end
theory add
imports "def"
begin
context l begin
lemma added: "x=x" ..
end
end
theory inst
imports "def"
begin
interpretation int: l .
thm int.orig
end
Email Gateway (Aug 18 2022 at 13:44):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Jul 9, 2009 at 9:11 AM, Peter
Lammich<peter.lammich@uni-muenster.de> wrote:
Hi all,
I encountered a problem/bug(?) with locales and imported theories.
I have four theories:
def: Defines a locale
add: Adds some lemma to the locale
inst: Interprets the locale, but does not import add
use: Imports add and instThe problem is, that I need to use the added lemma in the
interpretation. However, it is not visible in the theory "use".
Hi Peter,
This is a long-standing bug in Isabelle's implementation of locales.
It was discussed briefly on the mailing list in February 2008:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-February/msg00001.html
The only workarounds that I can currently figure out is instantiating
the missing lemmas by hand, i.e. lemmas xyz_lem = locale_name.lem[OF
xyz_is_interp] or trying to change the structure of the imports-graph.
Those are exactly the two workarounds that Clemens Ballarin suggested
on the list last February. I'm afraid the situation with the locale
package has not changed, so one of those workarounds will still be
necessary. Of the two, making the import structure more linear is
probably the easiest one to use. The drawback is that it introduces a
lot of extra theory dependencies that shouldn't be there. (For much of
Isabelle's history, import graphs were required to be totally-ordered,
and most of the packages were apparently designed with this in mind.
The locale package is not the only package in Isabelle that doesn't
handle theory merges very well.)
Email Gateway (Aug 18 2022 at 13:44):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Brian Huffman <brianh@cs.pdx.edu>:
I would like to point out that calling this behaviour a bug is jumping
to conclusions.
It is conceivable to "round up" interpretations at theory merges, but
note that this will not only populate the new theory with additional
theorems but also with syntax and other declarations. Enabling this
has to be thought through very carefully. I expect it to cause many
more "surprising" effects that will confuse users, hence I'm very
hesitant to provide this.
Clemens
Email Gateway (Aug 18 2022 at 13:44):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Peter,
I encountered a problem/bug(?) with locales and imported theories.
I have four theories:
def: Defines a locale
add: Adds some lemma to the locale
inst: Interprets the locale, but does not import add
use: Imports add and inst
Brian was so kind to dig out my answer to an earlier enquiry of the
same kind, so I can refer to his e-mail.
Even more strange things happen, if I try to reinterpret the locale in
theory "use": The re-interpretation (done with a different prefix name)
adds no lemmas, neither the ones originally defined in the locale, nor the
ones added by the theory "add".
It is not possible to force the re-interpretation of a locale
instance. In fact, the interpretation does not take place for any
locale fragments that are subsumed by existing interpretations (also
indirect ones created by sublocale).
The only workarounds that I can currently figure out is instantiating
the missing lemmas by hand, i.e. lemmas xyz_lem = locale_name.lem[OF
xyz_is_interp] or trying to change the structure of the imports-graph.
Is there some better method how to get the desired lemmas, especially
the ones that are declared as [simp] and hence should be filled into the
simpset?
If you want too keep the diamond theory hierarchy because "inst"
contains a lengthy proof of the interpretation theorem, you might
consider leaving the proof in "inst" but move the interpretation to
"use". This is, however, not going to work very well if you have a
hierarchy of locales.
Clemens
Email Gateway (Aug 18 2022 at 13:44):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Jul 9, 2009 at 12:33 PM, Clemens Ballarin<ballarin@in.tum.de> wrote:
Quoting Brian Huffman <brianh@cs.pdx.edu>:
On Thu, Jul 9, 2009 at 9:11 AM, Peter
Lammich<peter.lammich@uni-muenster.de> wrote:
Hi all,
I encountered a problem/bug(?) with locales and imported theories.
I have four theories:
def: Defines a locale
add: Adds some lemma to the locale
inst: Interprets the locale, but does not import add
use: Imports add and instThe problem is, that I need to use the added lemma in the
interpretation. However, it is not visible in the theory "use".Hi Peter,
This is a long-standing bug in Isabelle's implementation of locales.
It was discussed briefly on the mailing list in February 2008:...
I would like to point out that calling this behaviour a bug is jumping to
conclusions.
At the very least, I think I can safely say that when locales and
interpretations are used together with theory merges, the result is
often not what users expect.
The issue stems from the interaction between two Isabelle features
(locales and theory-merging), so I guess I shouldn't have called it a
bug in the locale package; it could just as well be called a bug in
Isabelle's theory-merging feature.
It is conceivable to "round up" interpretations at theory merges, but note
that this will not only populate the new theory with additional theorems but
also with syntax and other declarations. Enabling this has to be thought
through very carefully. I expect it to cause many more "surprising" effects
that will confuse users, hence I'm very hesitant to provide this.Clemens
After thinking about this a bit more, I now see a situation where
"rounding up" interpretations during merges could cause problems. The
problem is that the same "merge" could happen in more than one place.
Here's an example:
theory A (defines locale "foo")
theory B imports A (proves lemma "bar" in locale 'foo")
theory C imports A (interpretation "baz" of locale "foo")
theory D imports B C (merge creates lemma "baz.bar")
theory D' imports B C (merge creates another lemma "baz.bar")
theory E imports D D' (???)
Maybe the duplicate lemmas aren't such a big problem, but as you
pointed out, the locales could have syntax or other declarations that
operate on the theory context in arbitrary ways.
If there is not a good solution to the locale/theory-merge issue, then
I think it should be made clear in the documentation that using
locales together with theory-merges is not supported.
Email Gateway (Aug 18 2022 at 13:44):From: Makarius <makarius@sketis.net>
Theory merge does nothing more than delegate the actual merge operation to
theory data provided in user space (here the locale mechanism). So there
cannot be a bug "in" Isabelle's theory merge feature, but you could call
the whole feature a bug, because it raises delicate questions (which is a
well-known fact). But then, "feature" and "bug" are really synonyms, and
life can be generally simplified by deleting both words from one's
dictionary (which I have done many years ago).
BTW, the locale mechanism is properly called a "target" (of the local
theory framework). A "package" is something that implements a
specification mechanism that lives within such a target, e.g. 'inductive',
'function', 'primrec'.
Makarius
Last updated: May 03 2024 at 04:19 UTC