Re: [isabelle] Locale interpretations and imported theories



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:

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

- Brian





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