doc-src/AxClass/body.tex

snapshot of new Isar'ized version;

\chapter{Introduction}

A Haskell-style type-system \cite{haskell-report} with ordered type-classes
has been present in Isabelle since 1991 \cite{nipkow-sorts93}.  Initially,
classes have mainly served as a \emph{purely syntactic} tool to formulate
polymorphic object-logics in a clean way, such as the standard Isabelle
formulation of many-sorted FOL \cite{paulson-isa-book}.

Applying classes at the \emph{logical level} to provide a simple notion of
abstract theories and instantiations to concrete ones, has been long proposed
as well \cite{nipkow-types93,nipkow-sorts93}).  At that time, Isabelle still
lacked built-in support for these \emph{axiomatic type classes}. More
importantly, their semantics was not yet fully fleshed out (and unnecessarily
complicated, too).

Since the Isabelle94 releases, actual axiomatic type classes have been an
integral part of Isabelle's meta-logic.  This very simple implementation is
based on a straight-forward extension of traditional simple-typed Higher-Order
Logic, including types qualified by logical predicates and overloaded constant
definitions; see \cite{Wenzel:1997:TPHOL} for further details.

Yet until Isabelle99, there used to be still a fundamental methodological
problem in using axiomatic type classes conveniently, due to the traditional
distinction of Isabelle theory files vs.\ ML proof scripts.  This has been
finally overcome with the advent of Isabelle/Isar theories
\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
This nicely accommodates the usual procedure of defining axiomatic type
classes, proving abstract properties, defining operations on concrete types,
proving concrete properties for instantiation of classes etc.

\medskip

So to cut a long story short, the present version of axiomatic type classes
(Isabelle99 or later) now provides an even more useful and convenient
mechanism for light-weight abstract theories, without any special provisions
to be observed by the user.


\chapter{Examples}\label{sec:ex}

Axiomatic type classes are a concept of Isabelle's meta-logic
\cite{paulson-isa-book,Wenzel:1997:TPHOL}.  They may be applied to any
object-logic that directly uses the meta type system, such as Isabelle/HOL
\cite{isabelle-HOL}.  Subsequently, we present various examples that are all
formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
FOL.

\section{Semigroups}

An axiomatic type class is simply a class of types that all meet certain
\emph{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 \emph{characteristic constants} behave like operations associated with
the ``carrier'' type $\alpha$.

We illustrate these basic concepts by the following theory of semi-groups.

\bigskip
\input{generated/Semigroup}
\bigskip

\noindent
Above we have first declared a polymorphic constant $\TIMES :: \alpha \To
\alpha \To \alpha$ and then defined the class $semigroup$ of all types $\tau$
such that $\TIMES :: \tau \To \tau \To \tau$ is indeed an associative
operator.  The $assoc$ axiom 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 \emph{structures} with
exactly one carrier $\alpha$ and a fixed \emph{signature}.  Different
signatures require different classes. In the following theory, class
$plus_semigroup$ represents semigroups of the form $(\tau, \PLUS^\tau)$ while
$times_semigroup$ represents semigroups $(\tau, \TIMES^\tau)$.

\bigskip
\input{generated/Semigroups}
\bigskip

\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both represent
semigroups in a sense, they are not the same!


\section{Basic group theory}

\input{generated/Group}


The meta type system of Isabelle supports \emph{intersections} and
\emph{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.


\subsection{Monoids and Groups}

First we declare some polymorphic constants required later for the signature
parts of our structures.


Next we define class $monoid$ of monoids of the form $(\alpha,
{\TIMES}^\alpha)$.  Note that multiple class axioms are allowed for user
convenience --- they simply represent the conjunction of their respective
universal closures.


So class $monoid$ contains exactly those types $\tau$ where $\TIMES :: \tau
\To \tau \To \tau$ and $1 :: \tau$ are specified appropriately, such that
$\TIMES$ is associative and $1$ is a left and right unit for $\TIMES$.


Independently of $monoid$, we now define a linear hierarchy of semigroups,
general groups and abelian groups.  Note that the names of class axioms are
automatically qualified with the class name; thus we may re-use common names
such as $assoc$.


Class $group$ inherits associativity of $\TIMES$ from $semigroup$ and adds the
other two group axioms. Similarly, $agroup$ is defined as the subset of
$group$ such that for all of its elements $\tau$, the operation $\TIMES ::
\tau \To \tau \To \tau$ is even commutative.


\subsection{Abstract reasoning}

In a sense, axiomatic type classes may be viewed as \emph{abstract theories}.
Above class definitions internally generate the following abstract axioms:

%FIXME
% \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
% \emphnd{ascbox}

All of these contain type variables $\alpha :: c$ that are restricted to types
of some class $c$. These \emph{sort constraints} express a logical
precondition for the whole formula. For example, $assoc$ states that for all
$\tau$, provided that $\tau :: semigroup$, the operation $\TIMES :: \tau \To
\tau \To \tau$ is associative.

\medskip

From a purely technical point of view, abstract axioms are just ordinary
Isabelle theorems; they may be used for proofs without special treatment.
Such ``abstract proofs'' usually yield new abstract theorems.  For example, we
may now derive the following laws of general groups.



Abstract theorems may be instantiated to only those types $\tau$ where the
appropriate class membership $\tau :: c$ is known at Isabelle's type signature
level.  Since we have $agroup \subseteq group \subseteq semigroup$ by
definition, all theorems of $semigroup$ and $group$ are automatically
inherited by $group$ and $agroup$.


\subsection{Abstract instantiation}

From the definition, the $monoid$ and $group$ classes have been independent.
Note that for monoids, $right_unit$ had to be included as an axiom, but for
groups both $right_unit$ and $right_inverse$ are derivable from the other
axioms.  With $group_right_unit$ derived as a theorem of group theory (see
page~\pageref{thm:group-right-unit}), we may now instantiate $group \subset
monoid$ properly as follows (cf.\ \figref{fig:monoid-group}).

\begin{figure}[htbp]
  \begin{center}
    \small
%    \unitlength 0.75mm
    \unitlength 0.6mm
    \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){$agroup$}}
      \put(15,25){\makebox(0,0){$group$}}
      \put(15,45){\makebox(0,0){$semigroup$}}
      \put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$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){$agroup$}}
      \put(15,25){\makebox(0,0){$group$}}
      \put(15,45){\makebox(0,0){$monoid$}}
      \put(15,65){\makebox(0,0){$semigroup$}}
      \put(15,85){\makebox(0,0){$term$}}
    \end{picture}
    \caption{Monoids and groups: according to definition, and by proof}
    \label{fig:monoid-group}
  \end{center}
\end{figure}


\endinput

We know by definition that $\TIMES$ is associative for monoids, i.e.\ $monoid
\subseteq semigroup$. Furthermore we have $assoc$, $left_unit$ and
$right_unit$ for groups (where $right_unit$ is derivable from the group
axioms), that is $group \subseteq monoid$.  Thus we may establish the
following class instantiations.

\endinput

The \texttt{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 \emph{witnesses} usually
should be appropriate type instances of the class axioms (as are
\texttt{Monoid.assoc} and \texttt{assoc}, \texttt{left_unit}, \texttt{right_unit}
above).

The most important internal tool for instantiation proofs is the class
introduction rule that is automatically generated by \texttt{axclass}. For
class \texttt{group} this is axiom \texttt{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)
\emphnd{ascbox}

There are also axioms \texttt{monoidI}, \texttt{semigroupI} and \texttt{agroupI}
of a similar form.  Note that $\texttt{OFCLASS}(\tau, c \texttt{_class})$
expresses class membership $\tau :: c$ as a proposition of the
meta-logic.


\subsection{Concrete instantiation}

So far we have covered the case of \texttt{instance $c@1$ < $c@2$} that
could be described as \emph{abstract instantiation} --- $c@1$ is more
special than $c@2$ and thus an instance of $c@2$. Even more
interesting for practical applications are \emph{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
Isabelle's type signature level. This form of \texttt{instance} is a ``safe''
variant of the old-style \texttt{arities} theory section.

As an example, we show that type \texttt{bool} with exclusive-or as
operation $\TIMES$, identity as \texttt{inverse}, and \texttt{False} as \texttt{1}
forms an abelian group. We first define theory \texttt{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
\emphnd{ascbox}

It is important to note that above \texttt{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 \texttt{defs} of theory \texttt{Xor} suitably, the class
membership $\texttt{bool} :: \texttt{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 []);
\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}
\emphnd{ascbox}

The tactic \texttt{axclass_tac} has applied \texttt{agroupI} internally to
expand the class definition. It now remains to be shown that the
\texttt{agroup} axioms hold for bool. To this end, we expand the
definitions of \texttt{Xor} and solve the new subgoals by \texttt{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)"}
\emphnd{ascbox}

The result is theorem $\texttt{OFCLASS}(\texttt{bool}, \texttt{agroup_class})$
which expresses $\texttt{bool} :: \texttt{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
\texttt{instance} in a similar way behind the scenes. This may look as
follows\footnote{Subsequently, theory \texttt{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
\emphnd{ascbox}

This way, we have $\texttt{bool} :: \texttt{agroup}$ in the type signature of
\texttt{BoolGroupInsts}, and all abstract group theorems are transferred
to \texttt{bool} for free.

Similarly, we could now also instantiate our group theory classes to
many other concrete types. For example, $\texttt{int} :: \texttt{agroup}$ (by
defining $\TIMES$ as addition, \texttt{inverse} as negation and \texttt{1} as
zero, say) or $\texttt{list} :: (\texttt{term})\texttt{semigroup}$ (e.g.\ if
$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,
\texttt{inverse}, \texttt{1} really become overloaded, i.e.\ have different
meanings on different types.


\subsection{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 \emphq 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 \emph{lift operations}, e.g.\ to Cartesian
products, direct sums or function spaces. Below, theory
\texttt{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
\emphnd{ascbox}

Note that \texttt{prod_prod_def} basically has the form $\emphdrv
{\TIMES}^{\alpha \times \beta} \emphq \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 Isabelle's type signature by
above \texttt{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).




%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "axclass"
%%% End: 


\section{Syntactic classes}

There is still a feature of Isabelle's type system left that we have not yet
used: when declaring polymorphic constants $c :: \sigma$, the type variables
occurring in $\sigma$ may be constrained by type classes (or even general
sorts) in an arbitrary way.  Note that by default, in Isabelle/HOL the
declaration:  FIXME

\input{generated/Product}
\input{generated/NatClass}



\endinput


%\section

\begin{ascbox}
  <*> :: ['a, 'a] => 'a
\emphnd{ascbox}

is actually an abbreviation for:

\begin{ascbox}
  <*> :: ['a::term, 'a::term] => 'a::term
\emphnd{ascbox}

Since class \texttt{term} is the universal class of \HOL, this is not
really a restriction at all. A less trivial example is the following
theory \texttt{Product}:

\begin{ascbox}
Product = HOL +\medskip
axclass
  product < term\medskip
consts
  "<*>" :: "['a::product, 'a] => 'a"      (infixl 70)\medskip
end
\emphnd{ascbox}

Here class \texttt{product} is defined as subclass of \texttt{term}, but
without any additional axioms. This effects in logical equivalence of
\texttt{product} and \texttt{term}, since \texttt{productI} is as follows:

\begin{ascbox}
productI: OFCLASS(?'a::logic, term@class) ==>
            OFCLASS(?'a::logic, product@class)
\emphnd{ascbox}

I.e.\ $\texttt{term} \subseteq \texttt{product}$. The converse inclusion is
already contained in the type signature of theory \texttt{Product}.

Now, what is the difference of declaring $\TIMES :: [\alpha ::
\texttt{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::
\texttt{term}, \alpha] \To \alpha$? In this special case (where
$\texttt{product} \emphq \texttt{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 \emph{logical}
meaning to sort constraints occurring in constant \emph{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
:: \texttt{product}$ is part of the type signature.  In our example, this
arity may be always added when required by means of a trivial
\texttt{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 \emph{specifying} these
constants on a certain type $\tau$ do we instantiate $\tau :: c$.

This is done for class \texttt{product} and type \texttt{bool} in theory
\texttt{ProductInsts} below:

\begin{ascbox}
ProductInsts = Product +\medskip
instance
  bool :: product\medskip
defs
  prod@bool@def "x <*> y  == x & y::bool"\medskip
end
\emphnd{ascbox}

Note that \texttt{instance bool ::\ product} does not require any
witnesses, since this statement is logically trivial. Nonetheless,
\texttt{instance} really performs a proof.

Only after $\texttt{bool} :: \texttt{product}$ is made known to the type
checker, does \texttt{prod_bool_def} become syntactically well-formed.

\medskip

It is very important to see that above \texttt{defs} are not directly
connected with \texttt{instance} at all! We were just following our
convention to specify $\TIMES$ on \texttt{bool} after having instantiated
$\texttt{bool} :: \texttt{product}$. Isabelle does not require these definitions,
which is in contrast to programming languages like Haskell.

\medskip

While Isabelle 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
\emph{provide operations} of certain \emph{names}. Therefore, its
\texttt{instance} has a \texttt{where} part that tells the system what these
``member functions'' should be.

This style of \texttt{instance} won't make much sense in Isabelle, because its
meta-logic has no corresponding notion of ``providing operations'' or
``names''.


\section{Defining natural numbers in FOL}
\label{sec:ex-natclass}

Axiomatic type classes abstract over exactly one type argument. Thus,
any \emph{axiomatic} theory extension where each axiom refers to at most
one type variable, may be trivially turned into a \emph{definitional}
one.

We illustrate this with the natural numbers in Isabelle/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
\emphnd{ascbox}

\texttt{NatClass} is an abstract version of \texttt{Nat}\footnote{See
  directory \texttt{FOL/ex}.}. Basically, we have just replaced all
occurrences of \emph{type} \texttt{nat} by $\alpha$ and used the natural
number axioms to define \emph{class} \texttt{nat}\footnote{There's a snag:
  The original recursion operator \texttt{rec} had to be made monomorphic,
  in a sense.}. Thus class \texttt{nat} contains exactly those types
$\tau$ that are isomorphic to ``the'' natural numbers (with signature
\texttt{0}, \texttt{Suc}, \texttt{rec}).

Furthermore, theory \texttt{NatClass} defines an ``abstract constant'' $+$
based on class \texttt{nat}.

\medskip

What we have done here can be also viewed as \emph{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 \emph{not} true
  for pre-Isabelle94-2 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)
\emphnd{ascbox}

See also file \texttt{FOL/ex/NatClass.ML}. Note that this required only
some trivial modifications of the original \texttt{Nat.ML}.


%% FIXME move some parts to ref or isar-ref manual (!?);

% \chapter{The user interface of Isabelle's axclass package}

% The actual axiomatic type class package of Isabelle/Pure mainly consists
% of two new theory sections: \texttt{axclass} and \texttt{instance}.  Some
% typical applications of these have already been demonstrated in
% \secref{sec:ex}, below their syntax and semantics are presented more
% completely.


% \section{The axclass section}

% Within theory files, \texttt{axclass} introduces an axiomatic type class
% definition. Its concrete syntax is:

% \begin{matharray}{l}
%   \texttt{axclass} \\
%   \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
%   \ \ id@1\ axm@1 \\
%   \ \ \vdots \\
%   \ \ id@m\ axm@m
% \emphnd{matharray}

% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
% $string$) and $axm@1, \ldots, axm@m$ (with $m \ge
% 0$) are formulas (category $string$).

% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
% \texttt{logic}. Each class axiom $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 \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
% c@n$ to the type signature.

% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
% ``abstract axioms'' of $c$ with names $id@1, \ldots,
% 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
% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.

% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
% rule'' --- is built from the respective universal closures of
% $axm@1, \ldots, axm@m$ appropriately.


% \section{The instance section}

% Section \texttt{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}
%   \texttt{instance} \\
%   \ \ [\ c@1 \texttt{ < } c@2 \ |\
%       t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
%   \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
%   \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
% \emphnd{matharray}

% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
% (all of category $id$ or $string)$. Furthermore,
% $sort@i$ are sorts in the usual Isabelle-syntax.

% \medskip

% Internally, \texttt{instance} first sets up an appropriate goal that
% expresses the class inclusion or type arity as a meta-proposition.
% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
% meta-definitions of the current theory file and the user-supplied
% witnesses. The latter are $name@1, \ldots, name@m$, where
% $id$ refers to an \ML-name of a theorem, and $string$ to an
% axiom of the current theory node\footnote{Thus, the user may reference
%   axioms from above this \texttt{instance} in the theory file. Note
%   that new axioms appear at the \ML-toplevel only after the file is
%   processed completely.}.

% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
% resolving with rule $c\texttt\texttt{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-\emph{rules} to be used as witnesses for
%   corresponding class axioms.} with.

% The final optional argument $text$ is \ML-code of an arbitrary
% user tactic which is applied last to any remaining goals.

% \medskip

% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
% new users of the axclass package are advised to only use the simple
% form $\texttt{instance}\ \ldots\ (id@1, \ldots, 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.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "axclass"
%%% End: 
% LocalWords:  Isabelle FOL