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

[Tjark Weber]

Clemens,

Thanks for your quick reply!

On Thu, 2010-12-16 at 20:37 +0100, Clemens Ballarin wrote: 
> Suggestions?  The message also says that the relation is probably not  
> terminating.

Well, "roundup bound" is developer jargon.  "Sublocale relation probably
not terminating" points into the right direction, but is not very
precise (because cyclic sublocale relations are, in general, permitted).
Most importantly, any indication on how to resolve the problem is
missing.  So here's an attempt:

| Sorry, Isabelle cannot establish the requested sublocale relationship
| because the effected chain of interpretations would be too long.
|
| Please try to establish a different sublocale relationship.
| Section 7.1 of the Tutorial to Locales and Locale Interpretation
| provides further information on how to avoid infinite chains of
| interpretations.

(With a more closely integrated help system, further information would
be only one click away.  Moreover, Isabelle could automatically suggest
a sublocale statement that breaks the cycle.  But I'm dreaming; other
features are more important, of course.)

> >   lemma "class.X (undefined x)" sorry
> 
> I'm afraid I don't understand why this is a workaround.

It establishes the logical content of the sublocale relationship (i.e.,
the corresponding proof obligation), without providing any
interpretations however.

Kind regards,
Tjark