[isabelle-dev] Local Specification Mechanisms: Brief Experience Report
ballarin at in.tum.de
Thu Dec 16 20:37:53 CET 2010
thanks for your observations. When writing documentation, it is not
easy to anticipate what users will try to do, and what advice they
require. A user wiki/faq might be useful. Here are comments on your
locale-related observations. I cannot comment on classes since I
don't actually use them.
> * "Duplicate parameter(s) in superclasses", as in
> class A = fixes x :: 'a
> class B = fixes x :: 'a
> class C = A + B
> are disallowed.
For locales you would use
locale C = A x + B x for x
or one of the shortcuts discussed in the Locale Expressions Section of
the tutorial. I surprised that classes don't accept this syntax.
> * Cyclic sublocale relationships can lead to "Duplicate fact
> declaration" errors that are hard to understand: e.g.,
Indeed. Using a weak (that it, optional) qualifier in the locale
instance usually helps avoid this.
> * "Duplicate fact declaration" errors already show up with acyclic
> sublocale relationships, as in
> class A = fixes x::'a assumes xxx: "x = x"
> class B = fixes x::'a assumes xxx: "x = x"
> sublocale A < B sorry
See above. Using an optional qualifier is never a problem because you
don't need to mention it when quoting the fact. In fact, qualifiers
where introduced to deal with such situations in a pragmatic way.
> * Sublocale relationships that give rise to an infinite chain of
> instantiations, as in
> class X = fixes x::'a assumes "x = x"
> sublocale X < X "undefined x" sorry
> cause a "Roundup bound exceeded" error. The error message could
> probably be improved.
Suggestions? The message also says that the relation is probably not
> Moreover, the work-around
> lemma "class.X (undefined x)" sorry
> exposes what I would consider an implementation detail (namely the class
I'm afraid I don't understand why this is a workaround.
> It might be an idea to give the user explicit control over
> how many instantiation levels he wants from a sublocale command.
First you need to break the cycle. Then you can add sublocale
declarations for as many instantiation levels as you like. For
further information, please see "Avoiding Infinite Chains of
Interpretations" in the locales tutorial. There the idea is
elaborated up to the first level.
More information about the isabelle-dev