[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Clemens Ballarin]

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