--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/axclass.tex Mon May 12 17:53:36 1997 +0200
@@ -0,0 +1,747 @@
+
+\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}