8890

1 


2 
\chapter{Introduction}


3 


4 
A Haskellstyle typesystem \cite{haskellreport} with ordered typeclasses

8907

5 
has been present in Isabelle since 1991 already \cite{nipkowsorts93}.


6 
Initially, classes have mainly served as a \emph{purely syntactic} tool to


7 
formulate polymorphic objectlogics in a clean way, such as the standard


8 
Isabelle formulation of manysorted FOL \cite{paulsonisabook}.

8890

9 


10 
Applying classes at the \emph{logical level} to provide a simple notion of


11 
abstract theories and instantiations to concrete ones, has been long proposed

8907

12 
as well \cite{nipkowtypes93,nipkowsorts93}. At that time, Isabelle still

8890

13 
lacked builtin support for these \emph{axiomatic type classes}. More


14 
importantly, their semantics was not yet fully fleshed out (and unnecessarily


15 
complicated, too).


16 

8907

17 
Since Isabelle94, actual axiomatic type classes have been an integral part of


18 
Isabelle's metalogic. This very simple implementation is based on a


19 
straightforward extension of traditional simplytyped HigherOrder Logic, by


20 
including types qualified by logical predicates and overloaded constant


21 
definitions (see \cite{Wenzel:1997:TPHOL} for further details).

8890

22 

8907

23 
Yet even until Isabelle99, there used to be still a fundamental methodological

8890

24 
problem in using axiomatic type classes conveniently, due to the traditional


25 
distinction of Isabelle theory files vs.\ ML proof scripts. This has been


26 
finally overcome with the advent of Isabelle/Isar theories


27 
\cite{isabelleisarref}: now definitions and proofs may be freely intermixed.


28 
This nicely accommodates the usual procedure of defining axiomatic type


29 
classes, proving abstract properties, defining operations on concrete types,


30 
proving concrete properties for instantiation of classes etc.


31 


32 
\medskip


33 


34 
So to cut a long story short, the present version of axiomatic type classes

8907

35 
now provides an even more useful and convenient mechanism for lightweight


36 
abstract theories, without any special technical provisions to be observed by


37 
the user.

8890

38 


39 


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


41 


42 
Axiomatic type classes are a concept of Isabelle's metalogic


43 
\cite{paulsonisabook,Wenzel:1997:TPHOL}. They may be applied to any


44 
objectlogic that directly uses the meta type system, such as Isabelle/HOL


45 
\cite{isabelleHOL}. Subsequently, we present various examples that are all


46 
formulated within HOL, except the one of \secref{sec:exnatclass} which is in

8922

47 
FOL. See also \url{http://isabelle.in.tum.de/library/HOL/AxClass/} and


48 
\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.

8890

49 


50 
\input{generated/Semigroups}


51 


52 
\input{generated/Group}


53 

8903

54 
\input{generated/Product}

8890

55 

8903

56 
\input{generated/NatClass}

8890

57 


58 


59 
%% FIXME move some parts to ref or isarref manual (!?);


60 


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


62 


63 
% The actual axiomatic type class package of Isabelle/Pure mainly consists


64 
% of two new theory sections: \texttt{axclass} and \texttt{instance}. Some


65 
% typical applications of these have already been demonstrated in


66 
% \secref{sec:ex}, below their syntax and semantics are presented more


67 
% completely.


68 


69 


70 
% \section{The axclass section}


71 


72 
% Within theory files, \texttt{axclass} introduces an axiomatic type class


73 
% definition. Its concrete syntax is:


74 


75 
% \begin{matharray}{l}


76 
% \texttt{axclass} \\


77 
% \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\


78 
% \ \ id@1\ axm@1 \\


79 
% \ \ \vdots \\


80 
% \ \ id@m\ axm@m


81 
% \emphnd{matharray}


82 


83 
% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or

8906

84 
% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq

8890

85 
% 0$) are formulas (category $string$).


86 


87 
% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of


88 
% \texttt{logic}. Each class axiom $axm@j$ may contain any term


89 
% variables, but at most one type variable (which need not be the same


90 
% for all axioms). The sort of this type variable has to be a supersort


91 
% of $\{c@1, \ldots, c@n\}$.


92 


93 
% \medskip


94 


95 
% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,


96 
% c@n$ to the type signature.


97 


98 
% Furthermore, $axm@1, \ldots, axm@m$ are turned into the


99 
% ``abstract axioms'' of $c$ with names $id@1, \ldots,


100 
% id@m$. This is done by replacing all occurring type variables


101 
% by $\alpha :: c$. Original axioms that do not contain any type


102 
% variable will be prefixed by the logical precondition


103 
% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.


104 


105 
% Another axiom of name $c\texttt{I}$  the ``class $c$ introduction


106 
% rule''  is built from the respective universal closures of


107 
% $axm@1, \ldots, axm@m$ appropriately.


108 


109 


110 
% \section{The instance section}


111 


112 
% Section \texttt{instance} proves class inclusions or type arities at the


113 
% logical level and then transfers these into the type signature.


114 


115 
% Its concrete syntax is:


116 


117 
% \begin{matharray}{l}


118 
% \texttt{instance} \\


119 
% \ \ [\ c@1 \texttt{ < } c@2 \ \


120 
% t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\


121 
% \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\


122 
% \ \ [\ \texttt{\{} text \texttt{\}}\ ]


123 
% \emphnd{matharray}


124 


125 
% Where $c@1, c@2$ are classes and $t$ is an $n$place type constructor


126 
% (all of category $id$ or $string)$. Furthermore,


127 
% $sort@i$ are sorts in the usual Isabellesyntax.


128 


129 
% \medskip


130 


131 
% Internally, \texttt{instance} first sets up an appropriate goal that


132 
% expresses the class inclusion or type arity as a metaproposition.


133 
% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding


134 
% metadefinitions of the current theory file and the usersupplied


135 
% witnesses. The latter are $name@1, \ldots, name@m$, where


136 
% $id$ refers to an \MLname of a theorem, and $string$ to an


137 
% axiom of the current theory node\footnote{Thus, the user may reference


138 
% axioms from above this \texttt{instance} in the theory file. Note


139 
% that new axioms appear at the \MLtoplevel only after the file is


140 
% processed completely.}.


141 


142 
% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by


143 
% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses


144 
% according to their form: Metadefinitions are unfolded, all other


145 
% formulas are repeatedly resolved\footnote{This is done in a way that


146 
% enables proper object\emph{rules} to be used as witnesses for


147 
% corresponding class axioms.} with.


148 


149 
% The final optional argument $text$ is \MLcode of an arbitrary


150 
% user tactic which is applied last to any remaining goals.


151 


152 
% \medskip


153 


154 
% Because of the complexity of \texttt{instance}'s witnessing mechanisms,


155 
% new users of the axclass package are advised to only use the simple


156 
% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where


157 
% the identifiers refer to theorems that are appropriate type instances


158 
% of the class axioms. This typically requires an auxiliary theory,


159 
% though, which defines some constants and then proves these witnesses.


160 


161 


162 
%%% Local Variables:


163 
%%% mode: latex


164 
%%% TeXmaster: "axclass"


165 
%%% End:


166 
% LocalWords: Isabelle FOL
