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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
