doc-src/AxClass/body.tex

* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution

\chapter{Introduction}

A Haskell-style type-system \cite{haskell-report} with ordered type-classes
has been present in Isabelle since 1991 already \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 Isabelle94, 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 simply-typed Higher-Order Logic, by
including types qualified by logical predicates and overloaded constant
definitions (see \cite{Wenzel:1997:TPHOL} for further details).

Yet even 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
now provides an even more useful and convenient mechanism for light-weight
abstract theories, without any special technical 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.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.

\input{Group/document/Semigroups}

\input{Group/document/Group}

\input{Group/document/Product}

\input{Nat/document/NatClass}


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