Hi Tjark,
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
terminating.
Moreover, the work-around
lemma "class.X (undefined x)" sorry
exposes what I would consider an implementation detail (namely the class
predicate).
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.
Clemens
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
