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
