summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/AxClass/axclass.tex

author | wenzelm |

Tue, 20 May 1997 19:29:50 +0200 | |

changeset 3257 | 4e3724e0659f |

parent 3167 | 4e1eae442821 |

child 4009 | 6d9bec7b0b9e |

permissions | -rw-r--r-- |

README generation;

\input{style} \begin{document} \title{Using Axiomatic Type Classes in Isabelle \\ a tutorial} \author{Markus Wenzel} %\date{29 August 1995} \maketitle \Isa\ features a \Haskell-like type system with ordered type classes already since 1991 (see \cite{Nipkow93}). Initially, classes mainly served as a \E{syntactic tool} to formulate polymorphic object logics in a clean way (like many-sorted \FOL, see \cite[\S1.1.2--1.1.3]{Paulson94}). Applying classes at the \E{logical level} to provide a simple notion of abstract theories and instantiations to concrete ones, has also been long proposed (see \cite{Nipkow-slides} and \cite[\S4]{Nipkow93}). At that time, \Isa\ still lacked built-in support for these \E{axiomatic type classes}. More importantly, their semantics was not yet fully fleshed out and unnecessarily complicated. How simple things really are has been shown in \cite[esp.\ \S4]{Wenzel94} which also provided an implementation of the axclass package that was eventually released with \Isa94. Unfortunately there was a snag: That version of \Isa\ still contained an old conceptual bug in the core machinery which caused theories to become inconsistent after introducing empty sorts. Note that empty intersections of axiomatic type classes easily occur, unless all basic classes are very trivial. These problems prevented the axclass package to be used seriously --- they have been fixed in \Isa95. \section{Some simple examples} \label{sec:ex} Axiomatic type classes are a concept of \Isa's meta-logic. They may be applied to any object-logic that directly uses the meta type system. Subsequently, we present various examples that are formulated within \Isa/\HOL\footnote{See also directory \TT{HOL/AxClasses/Tutorial}.}, except the one of \secref{sec:ex-natclass} which is in \Isa/\FOL\footnote{See also files \TT{FOL/ex/NatClass.thy} and \TT{FOL/ex/NatClass.ML}.}. \subsection{Semigroups} An axiomatic type class is simply a class of types that all meet certain \E{axioms}. Thus, type classes may be also understood as type predicates --- i.e.\ abstractions over a single type argument $\alpha$. Class axioms typically contain polymorphic constants that depend on this type $\alpha$. These \E{characteristic constants} behave like operations associated with the ``carrier'' $\alpha$. We illustrate these basic concepts with the following theory \TT{Semigroup}: \begin{ascbox} Semigroup = HOL +\medskip consts "<*>" :: "['a, 'a] => 'a" (infixl 70)\medskip axclass semigroup < term assoc "(x <*> y) <*> z = x <*> (y <*> z)"\medskip end \end{ascbox} \TT{Semigroup} first declares a polymorphic constant $\TIMES :: [\alpha, \alpha] \To \alpha$ and then defines the class \TT{semigroup} of all those types $\tau$ such that $\TIMES :: [\tau, \tau] \To \tau$ is an associative operator\footnote{Note that $\TIMES$ is used here instead of $*$, because the latter is already declared in theory \TT{HOL} in a slightly different way.}. The axiom \TT{assoc} contains exactly one type variable, which is invisible in the above presentation, though. Also note that free term variables (like $x$, $y$, $z$) are allowed for user convenience --- conceptually all of these are bound by outermost universal quantifiers. \medskip In general, type classes may be used to describe \E{structures} with exactly one carrier $\alpha$ and a fixed \E{signature}. Different signatures require different classes. In the following theory \TT{Semigroups}, class \TT{plus\_sg} represents semigroups of the form $(\tau, \PLUS^\tau)$ while \TT{times\_sg} represents semigroups $(\tau, \TIMES^\tau)$: \begin{ascbox} Semigroups = HOL +\medskip consts "<+>" :: "['a, 'a] => 'a" (infixl 65) "<*>" :: "['a, 'a] => 'a" (infixl 70) assoc :: "(['a, 'a] => 'a) => bool"\medskip defs assoc_def "assoc f == ALL x y z. f (f x y) z = f x (f y z)"\medskip axclass plus_sg < term plus_assoc "assoc (op <+>)"\medskip axclass times_sg < term times_assoc "assoc (op <*>)"\medskip end \end{ascbox} Even if both classes \TT{plus\_sg} and \TT{times\_sg} represent semigroups in a sense, they are not the same! \subsection{Basic group theory} The meta type system of \Isa\ supports \E{intersections} and \E{inclusions} of type classes. These directly correspond to intersections and inclusions of type predicates in a purely set theoretic sense. This is sufficient as a means to describe simple hierarchies of structures. As an illustration, we use the well-known example of semigroups, monoids, general groups and abelian groups. \subsubsection{Monoids and Groups} First a small theory that provides some polymorphic constants to be used later for the signature parts: \begin{ascbox} Sigs = HOL +\medskip consts "<*>" :: "['a, 'a] => 'a" (infixl 70) inverse :: "'a => 'a" "1" :: "'a" ("1")\medskip end \end{ascbox} Next comes the theory \TT{Monoid} which defines class \TT{monoid}\footnote{Note that multiple class axioms are allowed for user convenience --- they simply represent the conjunction of their respective universal closures.}: \begin{ascbox} Monoid = Sigs +\medskip axclass monoid < term assoc "(x <*> y) <*> z = x <*> (y <*> z)" left_unit "1 <*> x = x" right_unit "x <*> 1 = x"\medskip end \end{ascbox} So class \TT{monoid} contains exactly those types $\tau$ where $\TIMES :: [\tau, \tau] \To \tau$ and $\TT{1} :: \tau$ are specified appropriately, such that $\TIMES$ is associative and $\TT{1}$ is a left and right unit for $\TIMES$. \medskip Independently of \TT{Monoid}, we now define theory \TT{Group} which introduces a linear hierarchy of semigroups, general groups and abelian groups: \begin{ascbox} Group = Sigs +\medskip axclass semigroup < term assoc "(x <*> y) <*> z = x <*> (y <*> z)"\brk axclass group < semigroup left_unit "1 <*> x = x" left_inverse "inverse x <*> x = 1"\medskip axclass agroup < group commut "x <*> y = y <*> x"\medskip end \end{ascbox} Class \TT{group} inherits associativity of $\TIMES$ from \TT{semigroup} and adds the other two group axioms. Similarly, \TT{agroup} is defined as the subset of \TT{group} such that for all of its elements $\tau$, the operation $\TIMES :: [\tau, \tau] \To \tau$ is even commutative. \subsubsection{Abstract reasoning} In a sense, axiomatic type classes may be viewed as \E{abstract theories}. Above class definitions internally generate the following abstract axioms: \begin{ascbox} assoc: (?x::?'a::semigroup) <*> (?y::?'a::semigroup) <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip left_unit: 1 <*> (?x::?'a::group) = ?x left_inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip commut: (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x \end{ascbox} All of these contain type variables $\alpha :: c$ that are restricted to types of some class $c$. These \E{sort constraints} express a logical precondition for the whole formula. For example, \TT{assoc} states that for all $\tau$, provided that $\tau :: \TT{semigroup}$, the operation $\TIMES :: [\tau, \tau] \To \tau$ is associative. \medskip From a purely technical point of view, abstract axioms are just ordinary \Isa-theorems (of \ML-type \TT{thm}). They may be used for \Isa-proofs without special treatment. Such ``abstract proofs'' usually yield new abstract theorems. For example, in theory \TT{Group} we may derive: \begin{ascbox} right_unit: (?x::?'a::group) <*> 1 = ?x right_inverse: (?x::?'a::group) <*> inverse ?x = 1 inverse_product: inverse ((?x::?'a::group) <*> (?y::?'a::group)) = inverse ?y <*> inverse ?x inverse_inv: inverse (inverse (?x::?'a::group)) = ?x ex1_inverse: ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1 \end{ascbox} Abstract theorems (which include abstract axioms, of course) may be instantiated to only those types $\tau$ where the appropriate class membership $\tau :: c$ is known at \Isa's type signature level. Since we have $\TT{agroup} \subseteq \TT{group} \subseteq \TT{semigroup}$ by definition, all theorems of \TT{semigroup} and \TT{group} are automatically inherited by \TT{group} and \TT{agroup}. \subsubsection{Abstract instantiation} Until now, theories \TT{Monoid} and \TT{Group} were independent. Forming their union $\TT{Monoid} + \TT{Group}$ we get the following class hierarchy at the type signature level (left hand side): \begin{center} \small \unitlength 0.75mm \begin{picture}(65,90)(0,-10) \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} \put(15,5){\makebox(0,0){\tt agroup}} \put(15,25){\makebox(0,0){\tt group}} \put(15,45){\makebox(0,0){\tt semigroup}} \put(30,65){\makebox(0,0){\tt term}} \put(50,45){\makebox(0,0){\tt monoid}} \end{picture} \hspace{4em} \begin{picture}(30,90)(0,0) \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} \put(15,5){\makebox(0,0){\tt agroup}} \put(15,25){\makebox(0,0){\tt group}} \put(15,45){\makebox(0,0){\tt monoid}} \put(15,65){\makebox(0,0){\tt semigroup}} \put(15,85){\makebox(0,0){\tt term}} \end{picture} \end{center} We know by definition that $\TIMES$ is associative for monoids, i.e.\ $\TT{monoid} \subseteq \TT{semigroup}$. Furthermore we have \TT{assoc}, \TT{left\_unit} and \TT{right\_unit} for groups (where \TT{right\_unit} is derivable from the group axioms), that is $\TT{group} \subseteq \TT{monoid}$. This way we get the refined class hierarchy shown above at the right hand side. The additional inclusions $\TT{monoid} \subseteq \TT{semigroup}$ and $\TT{group} \subseteq \TT{monoid}$ are established by logical means and have to be explicitly made known at the type signature level. This is what the theory section \TT{instance} does. So we define \TT{MonoidGroupInsts} as follows: \begin{ascbox} MonoidGroupInsts = Monoid + Group +\medskip instance monoid < semigroup (Monoid.assoc)\medskip instance group < monoid (assoc, left_unit, right_unit)\medskip end \end{ascbox} The \TT{instance} section does really check that the class inclusions (or type arities) to be added are derivable. To this end, it sets up a suitable goal and attempts a proof with the help of some internal axioms and user supplied theorems. These latter \E{witnesses} usually should be appropriate type instances of the class axioms (as are \TT{Monoid.assoc} and \TT{assoc}, \TT{left\_unit}, \TT{right\_unit} above). The most important internal tool for instantiation proofs is the class introduction rule that is automatically generated by \TT{axclass}. For class \TT{group} this is axiom \TT{groupI}: \begin{ascbox} groupI: [| OFCLASS(?'a::term, semigroup_class); !!x::?'a::term. 1 <*> x = x; !!x::?'a::term. inverse x <*> x = 1 |] ==> OFCLASS(?'a::term, group_class) \end{ascbox} There are also axioms \TT{monoidI}, \TT{semigroupI} and \TT{agroupI} of a similar form. Note that $\TT{OFCLASS}(\tau, c \TT{\_class})$ expresses class membership $\tau :: c$ as a proposition of the meta-logic. \subsubsection{Concrete instantiation} So far we have covered the case of \TT{instance $c_1$ < $c_2$} that could be described as \E{abstract instantiation} --- $c_1$ is more special than $c_2$ and thus an instance of $c_2$. Even more interesting for practical applications are \E{concrete instantiations} of axiomatic type classes. That is, certain simple schemes $(\alpha_1, \ldots, \alpha_n)t :: c$ of class membership may be transferred to \Isa's type signature level. This form of \TT{instance} is a ``safe'' variant of the old-style \TT{arities} theory section. As an example, we show that type \TT{bool} with exclusive-or as operation $\TIMES$, identity as \TT{inverse}, and \TT{False} as \TT{1} forms an abelian group. We first define theory \TT{Xor}: \begin{ascbox} Xor = Group +\medskip defs prod_bool_def "x <*> y == x ~= (y::bool)" inverse_bool_def "inverse x == x::bool" unit_bool_def "1 == False"\medskip end \end{ascbox} It is important to note that above \TT{defs} are just overloaded meta-level constant definitions. In particular, type classes are not yet involved at all! This form of constant definition with overloading (and optional primitive recursion over types) would be also possible in traditional versions of \HOL\ that lack type classes. % (see FIXME <foundation> for more details) Nonetheless, such definitions are best applied in the context of classes. \medskip Since we chose the \TT{defs} of theory \TT{Xor} suitably, the class membership $\TT{bool} :: \TT{agroup}$ is now derivable as follows: \begin{ascbox} open AxClass; goal_arity Xor.thy ("bool", [], "agroup"); \out{Level 0} \out{OFCLASS(bool, agroup_class)} \out{ 1. OFCLASS(bool, agroup_class)}\brk by (axclass_tac Xor.thy []); \out{Level 1} \out{OFCLASS(bool, agroup_class)} \out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)} \out{ 2. !!x::bool. 1 <*> x = x} \out{ 3. !!x::bool. inverse x <*> x = 1} \out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x} \end{ascbox} The tactic \TT{axclass\_tac} has applied \TT{agroupI} internally to expand the class definition. It now remains to be shown that the \TT{agroup} axioms hold for bool. To this end, we expand the definitions of \TT{Xor} and solve the new subgoals by \TT{fast\_tac} of \HOL: \begin{ascbox} by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inverse_bool_def, Xor.unit_bool_def]); \out{Level 2} \out{OFCLASS(bool, agroup_class)} \out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))} \out{ 2. !!x::bool. False ~= x = x} \out{ 3. !!x::bool. x ~= x = False} \out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)} by (ALLGOALS (fast_tac HOL_cs)); \out{Level 3} \out{OFCLASS(bool, agroup_class)} \out{No subgoals!} qed "bool_in_agroup"; \out{val bool_in_agroup = "OFCLASS(bool, agroup_class)"} \end{ascbox} The result is theorem $\TT{OFCLASS}(\TT{bool}, \TT{agroup\_class})$ which expresses $\TT{bool} :: \TT{agroup}$ as a meta-proposition. This is not yet known at the type signature level, though. \medskip What we have done here by hand, can be also performed via \TT{instance} in a similar way behind the scenes. This may look as follows\footnote{Subsequently, theory \TT{Xor} is no longer required.}: \begin{ascbox} BoolGroupInsts = Group +\medskip defs prod_bool_def "x <*> y == x ~= (y::bool)" inverse_bool_def "inverse x == x::bool" unit_bool_def "1 == False"\medskip instance bool :: agroup \{| ALLGOALS (fast_tac HOL_cs) |\}\medskip end \end{ascbox} This way, we have $\TT{bool} :: \TT{agroup}$ in the type signature of \TT{BoolGroupInsts}, and all abstract group theorems are transferred to \TT{bool} for free. Similarly, we could now also instantiate our group theory classes to many other concrete types. For example, $\TT{int} :: \TT{agroup}$ (by defining $\TIMES$ as addition, \TT{inverse} as negation and \TT{1} as zero, say) or $\TT{list} :: (\TT{term})\TT{semigroup}$ (e.g.\ if $\TIMES$ is list append). Thus, the characteristic constants $\TIMES$, \TT{inverse}, \TT{1} really become overloaded, i.e.\ have different meanings on different types. \subsubsection{Lifting and Functors} As already mentioned above, \HOL-like systems not only support overloaded definitions of polymorphic constants (without requiring type classes), but even primitive recursion over types. That is, definitional equations $c^\tau \Eq t$ may also contain constants of name $c$ on the RHS --- provided that these have types that are strictly simpler (structurally) than $\tau$. This feature enables us to \E{lift operations}, e.g.\ to Cartesian products, direct sums or function spaces. Below, theory \TT{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place Cartesian products $\alpha \times \beta$: \begin{ascbox} ProdGroupInsts = Prod + Group +\medskip defs prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip instance "*" :: (semigroup, semigroup) semigroup \{| simp_tac (prod_ss addsimps [assoc]) 1 |\} end \end{ascbox} Note that \TT{prod\_prod\_def} basically has the form $\edrv {\TIMES}^{\alpha \times \beta} \Eq \ldots {\TIMES}^\alpha \ldots {\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences $\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types. It is very easy to see that associativity of $\TIMES^\alpha$, $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence the two-place type constructor $\times$ maps semigroups into semigroups. This fact is proven and put into \Isa's type signature by above \TT{instance} section. \medskip Thus, if we view class instances as ``structures'', overloaded constant definitions with primitive recursion over types indirectly provide some kind of ``functors'' (mappings between abstract theories, that is). \subsection{Syntactic classes} There is still a feature of \Isa's type system left that we have not yet used: When declaring polymorphic constants $c :: \tau$, the type variables occurring in $\tau$ may be constrained by type classes (or even general sorts). Note that by default, in \Isa/\HOL\ the declaration: \begin{ascbox} <*> :: ['a, 'a] => 'a \end{ascbox} is actually an abbreviation for: \begin{ascbox} <*> :: ['a::term, 'a::term] => 'a::term \end{ascbox} Since class \TT{term} is the universal class of \HOL, this is not really a restriction at all. A less trivial example is the following theory \TT{Product}: \begin{ascbox} Product = HOL +\medskip axclass product < term\medskip consts "<*>" :: "['a::product, 'a] => 'a" (infixl 70)\medskip end \end{ascbox} Here class \TT{product} is defined as subclass of \TT{term}, but without any additional axioms. This effects in logical equivalence of \TT{product} and \TT{term}, since \TT{productI} is as follows: \begin{ascbox} productI: OFCLASS(?'a::logic, term_class) ==> OFCLASS(?'a::logic, product_class) \end{ascbox} I.e.\ $\TT{term} \subseteq \TT{product}$. The converse inclusion is already contained in the type signature of theory \TT{Product}. Now, what is the difference of declaring $\TIMES :: [\alpha :: \TT{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha :: \TT{term}, \alpha] \To \alpha$? In this special case (where $\TT{product} \Eq \TT{term}$), it should be obvious that both declarations are the same from the logic's point of view. It is even most sensible in the general case not to attach any \E{logical} meaning to sort constraints occurring in constant \E{declarations} (see \cite[page 79]{Wenzel94} for more details). On the other hand there are syntactic differences, of course. Constants $\TIMES^\tau$ are rejected by the type checker, unless $\tau :: \TT{product}$ is part of the type signature. In our example, this arity may be always added when required by means of a trivial \TT{instance}. Thus, we can follow this discipline: Overloaded polymorphic constants have their type arguments restricted to an associated (logically trivial) class $c$. Only immediately before \E{specifying} these constants on a certain type $\tau$ do we instantiate $\tau :: c$. This is done for class \TT{product} and type \TT{bool} in theory \TT{ProductInsts} below: \begin{ascbox} ProductInsts = Product +\medskip instance bool :: product\medskip defs prod_bool_def "x <*> y == x & y::bool"\medskip end \end{ascbox} Note that \TT{instance bool ::\ product} does not require any witnesses, since this statement is logically trivial. Nonetheless, \TT{instance} really performs a proof. Only after $\TT{bool} :: \TT{product}$ is made known to the type checker, does \TT{prod\_bool\_def} become syntactically well-formed. \medskip It is very important to see that above \TT{defs} are not directly connected with \TT{instance} at all! We were just following our convention to specify $\TIMES$ on \TT{bool} after having instantiated $\TT{bool} :: \TT{product}$. \Isa\ does not require these definitions, which is in contrast to programming languages like \Haskell. \medskip While \Isa\ type classes and those of \Haskell\ are almost the same as far as type checking and type inference are concerned, there are major semantic differences. \Haskell\ classes require their instances to \E{provide operations} of certain \E{names}. Therefore, its \TT{instance} has a \TT{where} part that tells the system what these ``member functions'' should be. This style of \TT{instance} won't make much sense in \Isa, because its meta-logic has no corresponding notion of ``providing operations'' or ``names''. \subsection{Defining natural numbers in \FOL} \label{sec:ex-natclass} Axiomatic type classes abstract over exactly one type argument. Thus, any \E{axiomatic} theory extension where each axiom refers to at most one type variable, may be trivially turned into a \E{definitional} one. We illustrate this with the natural numbers in \Isa/\FOL: \begin{ascbox} NatClass = FOL +\medskip consts "0" :: "'a" ("0") Suc :: "'a => 'a" rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip axclass nat < term induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" Suc_inject "Suc(m) = Suc(n) ==> m = n" Suc_neq_0 "Suc(m) = 0 ==> R" rec_0 "rec(0, a, f) = a" rec_Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip consts "+" :: "['a::nat, 'a] => 'a" (infixl 60)\medskip defs add_def "m + n == rec(m, n, %x y. Suc(y))"\medskip end \end{ascbox} \TT{NatClass} is an abstract version of \TT{Nat}\footnote{See directory \TT{FOL/ex}.}. Basically, we have just replaced all occurrences of \E{type} \TT{nat} by $\alpha$ and used the natural number axioms to define \E{class} \TT{nat}\footnote{There's a snag: The original recursion operator \TT{rec} had to be made monomorphic, in a sense.}. Thus class \TT{nat} contains exactly those types $\tau$ that are isomorphic to ``the'' natural numbers (with signature \TT{0}, \TT{Suc}, \TT{rec}). Furthermore, theory \TT{NatClass} defines an ``abstract constant'' $+$ based on class \TT{nat}. \medskip What we have done here can be also viewed as \E{type specification}. Of course, it still remains open if there is some type at all that meets the class axioms. Now a very nice property of axiomatic type classes is, that abstract reasoning is always possible --- independent of satisfiability. The meta-logic won't break, even if some class (or general sort) turns out to be empty (``inconsistent'') later\footnote{As a consequence of an old bug, this is \E{not} true for pre-\Isa95 versions.}. For example, we may derive the following abstract natural numbers theorems: \begin{ascbox} add_0: 0 + (?n::?'a::nat) = ?n add_Suc: Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n) \end{ascbox} See also file \TT{FOL/ex/NatClass.ML}. Note that this required only some trivial modifications of the original \TT{Nat.ML}. \section{The user interface of \Isa's axclass package} The actual axiomatic type class package of \Isa/\Pure\ mainly consists of two new theory sections: \TT{axclass} and \TT{instance}. Some typical applications of these have already been demonstrated in \secref{sec:ex}, below their syntax and semantics are presented more completely. \subsection{The \TT{axclass} section} Within theory files, \TT{axclass} introduces an axiomatic type class definition. Its concrete syntax is: \begin{matharray}{l} \TT{axclass} \\ \ \ c \TT{ < } c_1\TT, \ldots\TT, c_n \\ \ \ \idt{id}_1\ \idt{axm}_1 \\ \ \ \vdots \\ \ \ \idt{id}_m\ \idt{axm}_m \end{matharray} Where $c, c_1, \ldots, c_n$ are classes (category $\idt{id}$ or $\idt{string}$) and $\idt{axm}_1, \ldots, \idt{axm}_m$ (with $m \ge 0$) are formulas (category $\idt{string}$). Class $c$ has to be new, and sort $\{c_1, \ldots, c_n\}$ a subsort of \TT{logic}. Each class axiom $\idt{axm}_j$ may contain any term variables, but at most one type variable (which need not be the same for all axioms). The sort of this type variable has to be a supersort of $\{c_1, \ldots, c_n\}$. \medskip The \TT{axclass} section declares $c$ as subclass of $c_1, \ldots, c_n$ to the type signature. Furthermore, $\idt{axm}_1, \ldots, \idt{axm}_m$ are turned into the ``abstract axioms'' of $c$ with names $\idt{id}_1, \ldots, \idt{id}_m$. This is done by replacing all occurring type variables by $\alpha :: c$. Original axioms that do not contain any type variable will be prefixed by the logical precondition $\TT{OFCLASS}(\alpha :: \TT{logic}, c\TT{\_class})$. Another axiom of name $c\TT{I}$ --- the ``class $c$ introduction rule'' --- is built from the respective universal closures of $\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately. \subsection{The \TT{instance} section} Section \TT{instance} proves class inclusions or type arities at the logical level and then transfers these into the type signature. Its concrete syntax is: \begin{matharray}{l} \TT{instance} \\ \ \ [\ c_1 \TT{ < } c_2 \ |\ t \TT{ ::\ (}\idt{sort}_1\TT, \ldots \TT, \idt{sort}_n\TT) \idt{sort}\ ] \\ \ \ [\ \TT(\idt{name}_1 \TT, \ldots\TT, \idt{name}_m\TT)\ ] \\ \ \ [\ \TT{\{|} \idt{text} \TT{|\}}\ ] \end{matharray} Where $c_1, c_2$ are classes and $t$ is an $n$-place type constructor (all of category $\idt{id}$ or $\idt{string})$. Furthermore, $\idt{sort}_i$ are sorts in the usual \Isa-syntax. \medskip Internally, \TT{instance} first sets up an appropriate goal that expresses the class inclusion or type arity as a meta-proposition. Then tactic \TT{AxClass.axclass\_tac} is applied with all preceding meta-definitions of the current theory file and the user-supplied witnesses. The latter are $\idt{name}_1, \ldots, \idt{name}_m$, where $\idt{id}$ refers to an \ML-name of a theorem, and $\idt{string}$ to an axiom of the current theory node\footnote{Thus, the user may reference axioms from above this \TT{instance} in the theory file. Note that new axioms appear at the \ML-toplevel only after the file is processed completely.}. Tactic \TT{AxClass.axclass\_tac} first unfolds the class definition by resolving with rule $c\TT{I}$, and then applies the witnesses according to their form: Meta-definitions are unfolded, all other formulas are repeatedly resolved\footnote{This is done in a way that enables proper object-\E{rules} to be used as witnesses for corresponding class axioms.} with. The final optional argument $\idt{text}$ is \ML-code of an arbitrary user tactic which is applied last to any remaining goals. \medskip Because of the complexity of \TT{instance}'s witnessing mechanisms, new users of the axclass package are advised to only use the simple form $\TT{instance}\ \ldots\ (\idt{id}_1, \ldots, \idt{id}_m)$, where the identifiers refer to theorems that are appropriate type instances of the class axioms. This typically requires an auxiliary theory, though, which defines some constants and then proves these witnesses. \begin{thebibliography}{} \bibitem[Nipkow, 1993a]{Nipkow-slides} T. Nipkow. Axiomatic Type Classes (in Isabelle). Presentation at the workshop \E{Types for Proof and Programs}, Nijmegen, 1993. \bibitem[Nipkow, 1993b]{Nipkow93} T. Nipkow. Order-Sorted Polymorphism in Isabelle. In G. Huet, G. Plotkin, editors, \E{Logical Environments}, pp.\ 164--188, Cambridge University Press, 1993. \bibitem[Paulson, 1994]{Paulson94} L.C. Paulson. \E{Isabelle --- A Generic Theorem Prover}. LNCS 828, 1994. \bibitem[Wenzel, 1994]{Wenzel94} M. Wenzel. \E{Axiomatische Typ-Klassen in Isabelle}. Diplom\-arbeit, TU München, 1994. \end{thebibliography} \end{document}