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

[Tjark Weber]

I've recently worked on an algebraic hierarchy, ranging from semi-groups
to Kleene algebras and related structures, in Isabelle/HOL.  It goes
without saying that Isabelle's local specification mechanisms were well
suited for the task.  However, using classes and locales more
extensively for the first time, I noticed some (possibly well-known)
shortcomings.

Perhaps by sharing my initial observations and the pitfalls that I ran
into, I can provide some inspiration for further improvement.  My
intention is not to tread on someone's toes in the process; apologies if
I do.  Anyway, here we go (all based on Isabelle 2009-2):


* The documentation for local specification mechanisms is not very
homogeneous.  The tutorials on type classes and locales are valuable.
>From a user's perspective, however, a unifying discussion (with guidance
on when to use which) is missing.  (This is probably a natural
consequence of the fact that Isabelle's local specification mechanisms
were developed by several people and over a long period of time.)

* The previous point extends to the Isabelle/HOL library, which contains
several approaches to defining algebraic hierarchies.  Presumably, there
is a certain amount of bit rot, and some theories that should use
classes nowadays simply haven't been updated yet.

* "Duplicate parameter(s) in superclasses", as in

  class A = fixes x :: 'a
  class B = fixes x :: 'a
  class C = A + B

are disallowed.  The usual work-around (I believe) is to introduce a
syntactic super-class X that fixes the duplicate parameter:

  class X = fixes x :: 'a
  class A = X
  class B = X
  class C = A + B

This is artificial when compared to common mathematical practice, and it
means that one must anticipate the entire class hierarchy whenever one
introduces fixed parameters.

* Class assumptions must mention the class type: e.g.,

  class X = fixes x::'a assumes True

is rejected because there is "No type variable in part of specification
element."  Is there a technical reason for this requirement?

* Cyclic sublocale relationships can lead to "Duplicate fact
declaration" errors that are hard to understand: e.g.,

  class X = fixes x :: 'a
  class A = X + assumes xxx: "x = x"
  class B = X + assumes xxx: "x = x"
  sublocale X < A sorry

is rejected, while

  class X = fixes x :: 'a
  class A = X + assumes xxx: "x = x"
  sublocale X < A sorry
  class B = X + assumes xxx: "x = x"

is accepted.  Also,

  class X = fixes x :: 'a
  sublocale X < X undefined .
  definition (in X) "y == x"

is rejected (but accepted when the sublocale statement is qualified, as
in sublocale X < foo: X undefined).  The error message could probably be
improved.

* "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

This means that one must again anticipate the entire hierarchy when
naming facts.  (Using a qualifier avoids the problem here, as does the
use of locales instead of classes.)

* 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.  Moreover, the work-around

  lemma "class.X (undefined x)" sorry

exposes what I would consider an implementation detail (namely the class
predicate).  It might be an idea to give the user explicit control over
how many instantiation levels he wants from a sublocale command.

Ceterum censeo: a bug/feature tracker would be nice to have.

Kind regards,
Tjark