\chapter{Introduction}A Haskell-style type-system \cite{haskell-report} with ordered type-classeshas been present in Isabelle since 1991 already \cite{nipkow-sorts93}.Initially, classes have mainly served as a \emph{purely syntactic} tool toformulate polymorphic object-logics in a clean way, such as the standardIsabelle formulation of many-sorted FOL \cite{paulson-isa-book}.Applying classes at the \emph{logical level} to provide a simple notion ofabstract theories and instantiations to concrete ones, has been long proposedas well \cite{nipkow-types93,nipkow-sorts93}. At that time, Isabelle stilllacked built-in support for these \emph{axiomatic type classes}. Moreimportantly, their semantics was not yet fully fleshed out (and unnecessarilycomplicated, too).Since Isabelle94, actual axiomatic type classes have been an integral part ofIsabelle's meta-logic. This very simple implementation is based on astraight-forward extension of traditional simply-typed Higher-Order Logic, byincluding types qualified by logical predicates and overloaded constantdefinitions (see \cite{Wenzel:1997:TPHOL} for further details).Yet even until Isabelle99, there used to be still a fundamental methodologicalproblem in using axiomatic type classes conveniently, due to the traditionaldistinction of Isabelle theory files vs.\ ML proof scripts. This has beenfinally 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 typeclasses, proving abstract properties, defining operations on concrete types,proving concrete properties for instantiation of classes etc.\medskipSo to cut a long story short, the present version of axiomatic type classesnow provides an even more useful and convenient mechanism for light-weightabstract theories, without any special technical provisions to be observed bythe 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 anyobject-logic that directly uses the meta type system, such as Isabelle/HOL\cite{isabelle-HOL}. Subsequently, we present various examples that are allformulated within HOL, except the one of \secref{sec:ex-natclass} which is inFOL. 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