Re: [isabelle] Locale interpretations and imported theories



Quoting Brian Huffman <brianh at cs.pdx.edu>:

On Thu, Jul 9, 2009 at 9:11 AM, Peter
Lammich<peter.lammich at 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 inst

The 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.

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





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