[isabelle-dev] changeset 31457: class replaces axclass

[Brian Huffman]

Hi Florian,

I'm just wondering about why the "class" command is an improvement
over "axclass" in this situation:

http://isabelle.in.tum.de/repos/isabelle/rev/d1cb222438d8

Actually, it would be nice to hear a summary of how "class" is
supposed to be an improvement over "axclass" in general.

>From my point of view, here is the main visible benefit of "class"
over "axclass": When using axclass, it was often necessary to define a
"syntactic" type class for constants, and then a separate axiomatic
class that asserted properties of them. The "class" and
"instantiation" commands now make it possible to have just a single
class in those situations, since we can combine constant definitions
and instance proofs nicely with one "instantiation".

However, I also see some drawbacks to using "class" and related
commands. One example is the "subclass" command: When doing a subclass
proof, only theorems that were proved within a begin/end block for the
class are available to be used. I have tried to use "subclass" to
prove some of the subclass relationships in RealVector.thy (for no
reason except that "subclass" now seems to be the favored style of
doing things) but eventually gave up in despair. Within the class
context, many of the proofs simply no longer work, since many lemmas
and simprocs (especially lemmas about fields) are not available.

Another problem is that many lemmas about class real_vector are
generated by instantiating a generic vector-space locale, but locale
instantiations are not allowed within a class context. I'm not sure
how I can get these lemmas into a real_vector context without
duplicating a lot of code.

One more problem: When defining a subclass of existing classes using
the "class" command, the assumptions are only allowed to mention
constants defined within the begin/end context of the parent classes.
In many cases, it is not difficult to move the relevant constant
definitions into the appropriate class context. But what about
constants that involve more than one type? In particular, I am
thinking of "cont :: ('a::cpo => 'b::cpo) => bool" from HOLCF, and
"LIM :: ('a::metric_space => 'b::metric_space) => 'a => 'b => bool"
from Lim.thy.  There is no way to put these definitions inside a
single class context, so any subclass of "cpo" will never be able to
refer to the "cont" predicate, for example.

Yes, I know about the new feature (used by class bifinite in HOLCF and
also the new t0, t1, t2_space classes now) where the new class is not
really a subclass in the usual sense. But can you explain which
benefits of the "class" system still apply in this case? I suspect
that declaring a class in this way would break code generation for
that class, which I think was supposed to be one of the main reasons
for the new class system in the first place.

Finally, there are also some performance problems with the class
system that I have pointed out before: Opening a class context can be
*really* slow in some cases.

Basically, I am hoping that "axclass" continues to be supported as
long as all these problems with "class" still exist.

- Brian