Re: [isabelle] Locale interpretations and imported theories



On Thu, Jul 9, 2009 at 12:33 PM, Clemens Ballarin<ballarin at in.tum.de> wrote:
> 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.

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

- Brian





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