doc-src/AxClass/body.tex

new Isar 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 semigroups.

\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!


\input{generated/Group}

\input{generated/Product}


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

\bigskip
\input{generated/NatClass}
\bigskip

This is an abstract version of the plain $Nat$ theory in
FOL.\footnote{See \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}

Basically, we have just replaced all occurrences of type $nat$ by $\alpha$ and
used the natural number axioms to define class $nat$.  There is only a minor
snag, that the original recursion operator $rec$ had to be made monomorphic,
in a sense.  Thus class $nat$ contains exactly those types $\tau$ that are
isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, $rec$).

\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 classes (or general sorts) turns out to
be empty (``inconsistent'') later.

Theorems of the abstract natural numbers may be derived in the same way as for
the concrete version.  The original proof scripts may be used with some
trivial changes only (mostly adding some type constraints).


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