[isabelle-dev] changeset 31457: class replaces axclass

[Florian Haftmann]

Hi Brian,

> 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

Perhaps not "improvement", but "replacement";  before Isabelle 2009,
there were still situations which "class" could not cope with, as mentioned:

> 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.

> 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.

> But what about
> constants that involve more than one type?

With the improved version of "class" in Isabelle 2009, it is possible to
 use "class" as mere replacement for "axclass", with derived constants
defined globally on the theory level, using simple instance _ < _
instead of subclass etc.  The "locale" part of the class specification
is not really relevant in such situations.  There is no need to localize
or adapt abstract specifications, though in many cases this is possible
and desirable.  So nothing is imposed on the user in addition to
conventional axclass specifications.

This is achieved by type inference: in the class body, the sort of the
class type variable 'a is inferred and mixed into the super sort of the
newly defined class.

The reason to defavour "axclass" is simply that one user interface is
better than two.

Hope this helps
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090605/676ad816/attachment.sig>