3167

1 


2 
\input{style}


3 


4 
\begin{document}


5 


6 
\title{Using Axiomatic Type Classes in Isabelle \\ a tutorial}


7 
\author{Markus Wenzel}


8 
%\date{29 August 1995}


9 
\maketitle


10 


11 
\Isa\ features a \Haskelllike type system with ordered type classes


12 
already since 1991 (see \cite{Nipkow93}). Initially, classes mainly


13 
served as a \E{syntactic tool} to formulate polymorphic object logics


14 
in a clean way (like manysorted \FOL, see


15 
\cite[\S1.1.21.1.3]{Paulson94}).


16 


17 
Applying classes at the \E{logical level} to provide a simple notion


18 
of abstract theories and instantiations to concrete ones, has also


19 
been long proposed (see \cite{Nipkowslides} and


20 
\cite[\S4]{Nipkow93}). At that time, \Isa\ still lacked builtin


21 
support for these \E{axiomatic type classes}. More importantly, their


22 
semantics was not yet fully fleshed out and unnecessarily complicated.


23 


24 
How simple things really are has been shown in \cite[esp.\


25 
\S4]{Wenzel94} which also provided an implementation of the axclass


26 
package that was eventually released with \Isa94. Unfortunately there


27 
was a snag: That version of \Isa\ still contained an old conceptual


28 
bug in the core machinery which caused theories to become inconsistent


29 
after introducing empty sorts. Note that empty intersections of


30 
axiomatic type classes easily occur, unless all basic classes are very


31 
trivial.


32 


33 
These problems prevented the axclass package to be used seriously 

4009

34 
they have been fixed in \Isa942.

3167

35 


36 


37 
\section{Some simple examples} \label{sec:ex}


38 


39 
Axiomatic type classes are a concept of \Isa's metalogic. They may


40 
be applied to any objectlogic that directly uses the meta type


41 
system. Subsequently, we present various examples that are formulated


42 
within \Isa/\HOL\footnote{See also directory


43 
\TT{HOL/AxClasses/Tutorial}.}, except the one of


44 
\secref{sec:exnatclass} which is in \Isa/\FOL\footnote{See also files


45 
\TT{FOL/ex/NatClass.thy} and \TT{FOL/ex/NatClass.ML}.}.


46 


47 


48 
\subsection{Semigroups}


49 


50 
An axiomatic type class is simply a class of types that all meet


51 
certain \E{axioms}. Thus, type classes may be also understood as type


52 
predicates  i.e.\ abstractions over a single type argument


53 
$\alpha$. Class axioms typically contain polymorphic constants that


54 
depend on this type $\alpha$. These \E{characteristic constants}


55 
behave like operations associated with the ``carrier'' $\alpha$.


56 


57 
We illustrate these basic concepts with the following theory


58 
\TT{Semigroup}:


59 


60 
\begin{ascbox}


61 
Semigroup = HOL +\medskip


62 
consts


63 
"<*>" :: "['a, 'a] => 'a" (infixl 70)\medskip


64 
axclass


65 
semigroup < term


66 
assoc "(x <*> y) <*> z = x <*> (y <*> z)"\medskip


67 
end


68 
\end{ascbox}


69 


70 
\TT{Semigroup} first declares a polymorphic constant $\TIMES ::


71 
[\alpha, \alpha] \To \alpha$ and then defines the class \TT{semigroup}


72 
of all those types $\tau$ such that $\TIMES :: [\tau, \tau] \To \tau$


73 
is an associative operator\footnote{Note that $\TIMES$ is used here


74 
instead of $*$, because the latter is already declared in theory


75 
\TT{HOL} in a slightly different way.}. The axiom \TT{assoc}


76 
contains exactly one type variable, which is invisible in the above


77 
presentation, though. Also note that free term variables (like $x$,


78 
$y$, $z$) are allowed for user convenience  conceptually all of


79 
these are bound by outermost universal quantifiers.


80 


81 
\medskip


82 


83 
In general, type classes may be used to describe \E{structures} with


84 
exactly one carrier $\alpha$ and a fixed \E{signature}. Different


85 
signatures require different classes. In the following theory


86 
\TT{Semigroups}, class \TT{plus\_sg} represents semigroups of the form


87 
$(\tau, \PLUS^\tau)$ while \TT{times\_sg} represents semigroups


88 
$(\tau, \TIMES^\tau)$:


89 


90 
\begin{ascbox}


91 
Semigroups = HOL +\medskip


92 
consts


93 
"<+>" :: "['a, 'a] => 'a" (infixl 65)


94 
"<*>" :: "['a, 'a] => 'a" (infixl 70)


95 
assoc :: "(['a, 'a] => 'a) => bool"\medskip


96 
defs


97 
assoc_def "assoc f == ALL x y z. f (f x y) z = f x (f y z)"\medskip


98 
axclass


99 
plus_sg < term


100 
plus_assoc "assoc (op <+>)"\medskip


101 
axclass


102 
times_sg < term


103 
times_assoc "assoc (op <*>)"\medskip


104 
end


105 
\end{ascbox}


106 


107 
Even if both classes \TT{plus\_sg} and \TT{times\_sg} represent


108 
semigroups in a sense, they are not the same!


109 


110 


111 
\subsection{Basic group theory}


112 


113 
The meta type system of \Isa\ supports \E{intersections} and


114 
\E{inclusions} of type classes. These directly correspond to


115 
intersections and inclusions of type predicates in a purely set


116 
theoretic sense. This is sufficient as a means to describe simple


117 
hierarchies of structures. As an illustration, we use the wellknown


118 
example of semigroups, monoids, general groups and abelian groups.


119 


120 


121 
\subsubsection{Monoids and Groups}


122 


123 
First a small theory that provides some polymorphic constants to be


124 
used later for the signature parts:


125 


126 
\begin{ascbox}


127 
Sigs = HOL +\medskip


128 
consts


129 
"<*>" :: "['a, 'a] => 'a" (infixl 70)


130 
inverse :: "'a => 'a"


131 
"1" :: "'a" ("1")\medskip


132 
end


133 
\end{ascbox}


134 


135 
Next comes the theory \TT{Monoid} which defines class


136 
\TT{monoid}\footnote{Note that multiple class axioms are allowed for


137 
user convenience  they simply represent the conjunction of their


138 
respective universal closures.}:


139 


140 
\begin{ascbox}


141 
Monoid = Sigs +\medskip


142 
axclass


143 
monoid < term


144 
assoc "(x <*> y) <*> z = x <*> (y <*> z)"


145 
left_unit "1 <*> x = x"


146 
right_unit "x <*> 1 = x"\medskip


147 
end


148 
\end{ascbox}


149 


150 
So class \TT{monoid} contains exactly those types $\tau$ where $\TIMES


151 
:: [\tau, \tau] \To \tau$ and $\TT{1} :: \tau$ are specified


152 
appropriately, such that $\TIMES$ is associative and $\TT{1}$ is a


153 
left and right unit for $\TIMES$.


154 


155 
\medskip


156 


157 
Independently of \TT{Monoid}, we now define theory \TT{Group} which


158 
introduces a linear hierarchy of semigroups, general groups and


159 
abelian groups:


160 


161 
\begin{ascbox}


162 
Group = Sigs +\medskip


163 
axclass


164 
semigroup < term


165 
assoc "(x <*> y) <*> z = x <*> (y <*> z)"\brk


166 
axclass


167 
group < semigroup


168 
left_unit "1 <*> x = x"


169 
left_inverse "inverse x <*> x = 1"\medskip


170 
axclass


171 
agroup < group


172 
commut "x <*> y = y <*> x"\medskip


173 
end


174 
\end{ascbox}


175 


176 
Class \TT{group} inherits associativity of $\TIMES$ from


177 
\TT{semigroup} and adds the other two group axioms. Similarly,


178 
\TT{agroup} is defined as the subset of \TT{group} such that for all


179 
of its elements $\tau$, the operation $\TIMES :: [\tau, \tau] \To


180 
\tau$ is even commutative.


181 


182 


183 
\subsubsection{Abstract reasoning}


184 


185 
In a sense, axiomatic type classes may be viewed as \E{abstract


186 
theories}. Above class definitions internally generate the


187 
following abstract axioms:


188 


189 
\begin{ascbox}


190 
assoc: (?x::?'a::semigroup) <*> (?y::?'a::semigroup)


191 
<*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip


192 
left_unit: 1 <*> (?x::?'a::group) = ?x


193 
left_inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip


194 
commut: (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x


195 
\end{ascbox}


196 


197 
All of these contain type variables $\alpha :: c$ that are restricted


198 
to types of some class $c$. These \E{sort constraints} express a


199 
logical precondition for the whole formula. For example, \TT{assoc}


200 
states that for all $\tau$, provided that $\tau :: \TT{semigroup}$,


201 
the operation $\TIMES :: [\tau, \tau] \To \tau$ is associative.


202 


203 
\medskip


204 


205 
From a purely technical point of view, abstract axioms are just


206 
ordinary \Isatheorems (of \MLtype \TT{thm}). They may be used for


207 
\Isaproofs without special treatment. Such ``abstract proofs''


208 
usually yield new abstract theorems. For example, in theory \TT{Group}


209 
we may derive:


210 


211 
\begin{ascbox}


212 
right_unit: (?x::?'a::group) <*> 1 = ?x


213 
right_inverse: (?x::?'a::group) <*> inverse ?x = 1


214 
inverse_product: inverse ((?x::?'a::group) <*> (?y::?'a::group)) =


215 
inverse ?y <*> inverse ?x


216 
inverse_inv: inverse (inverse (?x::?'a::group)) = ?x


217 
ex1_inverse: ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1


218 
\end{ascbox}


219 


220 
Abstract theorems (which include abstract axioms, of course) may be


221 
instantiated to only those types $\tau$ where the appropriate class


222 
membership $\tau :: c$ is known at \Isa's type signature level. Since


223 
we have $\TT{agroup} \subseteq \TT{group} \subseteq \TT{semigroup}$ by


224 
definition, all theorems of \TT{semigroup} and \TT{group} are


225 
automatically inherited by \TT{group} and \TT{agroup}.


226 


227 


228 
\subsubsection{Abstract instantiation}


229 


230 
Until now, theories \TT{Monoid} and \TT{Group} were independent.


231 
Forming their union $\TT{Monoid} + \TT{Group}$ we get the following


232 
class hierarchy at the type signature level (left hand side):


233 


234 
\begin{center}


235 
\small


236 
\unitlength 0.75mm


237 
\begin{picture}(65,90)(0,10)


238 
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}


239 
\put(15,50){\line(1,1){10}} \put(35,60){\line(1,1){10}}


240 
\put(15,5){\makebox(0,0){\tt agroup}}


241 
\put(15,25){\makebox(0,0){\tt group}}


242 
\put(15,45){\makebox(0,0){\tt semigroup}}


243 
\put(30,65){\makebox(0,0){\tt term}} \put(50,45){\makebox(0,0){\tt


244 
monoid}}


245 
\end{picture}


246 
\hspace{4em}


247 
\begin{picture}(30,90)(0,0)


248 
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}


249 
\put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}


250 
\put(15,5){\makebox(0,0){\tt agroup}}


251 
\put(15,25){\makebox(0,0){\tt group}}


252 
\put(15,45){\makebox(0,0){\tt monoid}}


253 
\put(15,65){\makebox(0,0){\tt semigroup}}


254 
\put(15,85){\makebox(0,0){\tt term}}


255 
\end{picture}


256 
\end{center}


257 


258 
We know by definition that $\TIMES$ is associative for monoids, i.e.\


259 
$\TT{monoid} \subseteq \TT{semigroup}$. Furthermore we have


260 
\TT{assoc}, \TT{left\_unit} and \TT{right\_unit} for groups (where


261 
\TT{right\_unit} is derivable from the group axioms), that is


262 
$\TT{group} \subseteq \TT{monoid}$. This way we get the refined class


263 
hierarchy shown above at the right hand side.


264 


265 
The additional inclusions $\TT{monoid} \subseteq \TT{semigroup}$ and


266 
$\TT{group} \subseteq \TT{monoid}$ are established by logical means


267 
and have to be explicitly made known at the type signature level. This


268 
is what the theory section \TT{instance} does. So we define


269 
\TT{MonoidGroupInsts} as follows:


270 


271 
\begin{ascbox}


272 
MonoidGroupInsts = Monoid + Group +\medskip


273 
instance


274 
monoid < semigroup (Monoid.assoc)\medskip


275 
instance


276 
group < monoid (assoc, left_unit, right_unit)\medskip


277 
end


278 
\end{ascbox}


279 


280 
The \TT{instance} section does really check that the class inclusions


281 
(or type arities) to be added are derivable. To this end, it sets up a


282 
suitable goal and attempts a proof with the help of some internal


283 
axioms and user supplied theorems. These latter \E{witnesses} usually


284 
should be appropriate type instances of the class axioms (as are


285 
\TT{Monoid.assoc} and \TT{assoc}, \TT{left\_unit}, \TT{right\_unit}


286 
above).


287 


288 
The most important internal tool for instantiation proofs is the class


289 
introduction rule that is automatically generated by \TT{axclass}. For


290 
class \TT{group} this is axiom \TT{groupI}:


291 


292 
\begin{ascbox}


293 
groupI: [ OFCLASS(?'a::term, semigroup_class);


294 
!!x::?'a::term. 1 <*> x = x;


295 
!!x::?'a::term. inverse x <*> x = 1 ]


296 
==> OFCLASS(?'a::term, group_class)


297 
\end{ascbox}


298 


299 
There are also axioms \TT{monoidI}, \TT{semigroupI} and \TT{agroupI}


300 
of a similar form. Note that $\TT{OFCLASS}(\tau, c \TT{\_class})$


301 
expresses class membership $\tau :: c$ as a proposition of the


302 
metalogic.


303 


304 


305 
\subsubsection{Concrete instantiation}


306 


307 
So far we have covered the case of \TT{instance $c_1$ < $c_2$} that


308 
could be described as \E{abstract instantiation}  $c_1$ is more


309 
special than $c_2$ and thus an instance of $c_2$. Even more


310 
interesting for practical applications are \E{concrete instantiations}


311 
of axiomatic type classes. That is, certain simple schemes $(\alpha_1,


312 
\ldots, \alpha_n)t :: c$ of class membership may be transferred to


313 
\Isa's type signature level. This form of \TT{instance} is a ``safe''


314 
variant of the oldstyle \TT{arities} theory section.


315 


316 
As an example, we show that type \TT{bool} with exclusiveor as


317 
operation $\TIMES$, identity as \TT{inverse}, and \TT{False} as \TT{1}


318 
forms an abelian group. We first define theory \TT{Xor}:


319 


320 
\begin{ascbox}


321 
Xor = Group +\medskip


322 
defs


323 
prod_bool_def "x <*> y == x ~= (y::bool)"


324 
inverse_bool_def "inverse x == x::bool"


325 
unit_bool_def "1 == False"\medskip


326 
end


327 
\end{ascbox}


328 


329 
It is important to note that above \TT{defs} are just overloaded


330 
metalevel constant definitions. In particular, type classes are not


331 
yet involved at all! This form of constant definition with overloading


332 
(and optional primitive recursion over types) would be also possible


333 
in traditional versions of \HOL\ that lack type classes.


334 
% (see FIXME <foundation> for more details)


335 
Nonetheless, such definitions are best applied in the context of


336 
classes.


337 


338 
\medskip


339 


340 
Since we chose the \TT{defs} of theory \TT{Xor} suitably, the class


341 
membership $\TT{bool} :: \TT{agroup}$ is now derivable as follows:


342 


343 
\begin{ascbox}


344 
open AxClass;


345 
goal_arity Xor.thy ("bool", [], "agroup");


346 
\out{Level 0}


347 
\out{OFCLASS(bool, agroup_class)}


348 
\out{ 1. OFCLASS(bool, agroup_class)}\brk

6387

349 
by (axclass_tac []);

3167

350 
\out{Level 1}


351 
\out{OFCLASS(bool, agroup_class)}


352 
\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)}


353 
\out{ 2. !!x::bool. 1 <*> x = x}


354 
\out{ 3. !!x::bool. inverse x <*> x = 1}


355 
\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x}


356 
\end{ascbox}


357 


358 
The tactic \TT{axclass\_tac} has applied \TT{agroupI} internally to


359 
expand the class definition. It now remains to be shown that the


360 
\TT{agroup} axioms hold for bool. To this end, we expand the


361 
definitions of \TT{Xor} and solve the new subgoals by \TT{fast\_tac}


362 
of \HOL:


363 


364 
\begin{ascbox}


365 
by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inverse_bool_def,


366 
Xor.unit_bool_def]);


367 
\out{Level 2}


368 
\out{OFCLASS(bool, agroup_class)}


369 
\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))}


370 
\out{ 2. !!x::bool. False ~= x = x}


371 
\out{ 3. !!x::bool. x ~= x = False}


372 
\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)}


373 
by (ALLGOALS (fast_tac HOL_cs));


374 
\out{Level 3}


375 
\out{OFCLASS(bool, agroup_class)}


376 
\out{No subgoals!}


377 
qed "bool_in_agroup";


378 
\out{val bool_in_agroup = "OFCLASS(bool, agroup_class)"}


379 
\end{ascbox}


380 


381 
The result is theorem $\TT{OFCLASS}(\TT{bool}, \TT{agroup\_class})$


382 
which expresses $\TT{bool} :: \TT{agroup}$ as a metaproposition. This


383 
is not yet known at the type signature level, though.


384 


385 
\medskip


386 


387 
What we have done here by hand, can be also performed via


388 
\TT{instance} in a similar way behind the scenes. This may look as


389 
follows\footnote{Subsequently, theory \TT{Xor} is no longer


390 
required.}:


391 


392 
\begin{ascbox}


393 
BoolGroupInsts = Group +\medskip


394 
defs


395 
prod_bool_def "x <*> y == x ~= (y::bool)"


396 
inverse_bool_def "inverse x == x::bool"


397 
unit_bool_def "1 == False"\medskip


398 
instance


399 
bool :: agroup \{ ALLGOALS (fast_tac HOL_cs) \}\medskip


400 
end


401 
\end{ascbox}


402 


403 
This way, we have $\TT{bool} :: \TT{agroup}$ in the type signature of


404 
\TT{BoolGroupInsts}, and all abstract group theorems are transferred


405 
to \TT{bool} for free.


406 


407 
Similarly, we could now also instantiate our group theory classes to


408 
many other concrete types. For example, $\TT{int} :: \TT{agroup}$ (by


409 
defining $\TIMES$ as addition, \TT{inverse} as negation and \TT{1} as


410 
zero, say) or $\TT{list} :: (\TT{term})\TT{semigroup}$ (e.g.\ if


411 
$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,


412 
\TT{inverse}, \TT{1} really become overloaded, i.e.\ have different


413 
meanings on different types.


414 


415 


416 
\subsubsection{Lifting and Functors}


417 


418 
As already mentioned above, \HOLlike systems not only support


419 
overloaded definitions of polymorphic constants (without requiring


420 
type classes), but even primitive recursion over types. That is,


421 
definitional equations $c^\tau \Eq t$ may also contain constants of


422 
name $c$ on the RHS  provided that these have types that are


423 
strictly simpler (structurally) than $\tau$.


424 


425 
This feature enables us to \E{lift operations}, e.g.\ to Cartesian


426 
products, direct sums or function spaces. Below, theory


427 
\TT{ProdGroupInsts} lifts $\TIMES$ componentwise to twoplace


428 
Cartesian products $\alpha \times \beta$:


429 


430 
\begin{ascbox}


431 
ProdGroupInsts = Prod + Group +\medskip


432 
defs


433 
prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip


434 
instance


435 
"*" :: (semigroup, semigroup) semigroup


436 
\{ simp_tac (prod_ss addsimps [assoc]) 1 \}


437 
end


438 
\end{ascbox}


439 


440 
Note that \TT{prod\_prod\_def} basically has the form $\edrv


441 
{\TIMES}^{\alpha \times \beta} \Eq \ldots {\TIMES}^\alpha \ldots


442 
{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences


443 
$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types.


444 


445 
It is very easy to see that associativity of $\TIMES^\alpha$,


446 
$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence


447 
the twoplace type constructor $\times$ maps semigroups into


448 
semigroups. This fact is proven and put into \Isa's type signature by


449 
above \TT{instance} section.


450 


451 
\medskip


452 


453 
Thus, if we view class instances as ``structures'', overloaded


454 
constant definitions with primitive recursion over types indirectly


455 
provide some kind of ``functors'' (mappings between abstract theories,


456 
that is).


457 


458 


459 
\subsection{Syntactic classes}


460 


461 
There is still a feature of \Isa's type system left that we have not


462 
yet used: When declaring polymorphic constants $c :: \tau$, the type


463 
variables occurring in $\tau$ may be constrained by type classes (or


464 
even general sorts). Note that by default, in \Isa/\HOL\ the


465 
declaration:


466 


467 
\begin{ascbox}


468 
<*> :: ['a, 'a] => 'a


469 
\end{ascbox}


470 


471 
is actually an abbreviation for:


472 


473 
\begin{ascbox}


474 
<*> :: ['a::term, 'a::term] => 'a::term


475 
\end{ascbox}


476 


477 
Since class \TT{term} is the universal class of \HOL, this is not


478 
really a restriction at all. A less trivial example is the following


479 
theory \TT{Product}:


480 


481 
\begin{ascbox}


482 
Product = HOL +\medskip


483 
axclass


484 
product < term\medskip


485 
consts


486 
"<*>" :: "['a::product, 'a] => 'a" (infixl 70)\medskip


487 
end


488 
\end{ascbox}


489 


490 
Here class \TT{product} is defined as subclass of \TT{term}, but


491 
without any additional axioms. This effects in logical equivalence of


492 
\TT{product} and \TT{term}, since \TT{productI} is as follows:


493 


494 
\begin{ascbox}


495 
productI: OFCLASS(?'a::logic, term_class) ==>


496 
OFCLASS(?'a::logic, product_class)


497 
\end{ascbox}


498 


499 
I.e.\ $\TT{term} \subseteq \TT{product}$. The converse inclusion is


500 
already contained in the type signature of theory \TT{Product}.


501 


502 
Now, what is the difference of declaring $\TIMES :: [\alpha ::


503 
\TT{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::


504 
\TT{term}, \alpha] \To \alpha$? In this special case (where


505 
$\TT{product} \Eq \TT{term}$), it should be obvious that both


506 
declarations are the same from the logic's point of view. It is even


507 
most sensible in the general case not to attach any \E{logical}


508 
meaning to sort constraints occurring in constant \E{declarations}


509 
(see \cite[page 79]{Wenzel94} for more details).


510 


511 
On the other hand there are syntactic differences, of course.

6170

512 
Constants $\TIMES^\tau$ are rejected by the typechecker, unless $\tau

3167

513 
:: \TT{product}$ is part of the type signature. In our example, this


514 
arity may be always added when required by means of a trivial


515 
\TT{instance}.


516 


517 
Thus, we can follow this discipline: Overloaded polymorphic constants


518 
have their type arguments restricted to an associated (logically


519 
trivial) class $c$. Only immediately before \E{specifying} these


520 
constants on a certain type $\tau$ do we instantiate $\tau :: c$.


521 


522 
This is done for class \TT{product} and type \TT{bool} in theory


523 
\TT{ProductInsts} below:


524 


525 
\begin{ascbox}


526 
ProductInsts = Product +\medskip


527 
instance


528 
bool :: product\medskip


529 
defs


530 
prod_bool_def "x <*> y == x & y::bool"\medskip


531 
end


532 
\end{ascbox}


533 


534 
Note that \TT{instance bool ::\ product} does not require any


535 
witnesses, since this statement is logically trivial. Nonetheless,


536 
\TT{instance} really performs a proof.


537 


538 
Only after $\TT{bool} :: \TT{product}$ is made known to the type


539 
checker, does \TT{prod\_bool\_def} become syntactically wellformed.


540 


541 
\medskip


542 


543 
It is very important to see that above \TT{defs} are not directly


544 
connected with \TT{instance} at all! We were just following our


545 
convention to specify $\TIMES$ on \TT{bool} after having instantiated


546 
$\TT{bool} :: \TT{product}$. \Isa\ does not require these definitions,


547 
which is in contrast to programming languages like \Haskell.


548 


549 
\medskip


550 


551 
While \Isa\ type classes and those of \Haskell\ are almost the same as

6170

552 
far as typechecking and type inference are concerned, there are major

3167

553 
semantic differences. \Haskell\ classes require their instances to


554 
\E{provide operations} of certain \E{names}. Therefore, its


555 
\TT{instance} has a \TT{where} part that tells the system what these


556 
``member functions'' should be.


557 


558 
This style of \TT{instance} won't make much sense in \Isa, because its


559 
metalogic has no corresponding notion of ``providing operations'' or


560 
``names''.


561 


562 

6623

563 
\subsection{Defining natural numbers in FOL}

3167

564 
\label{sec:exnatclass}


565 


566 
Axiomatic type classes abstract over exactly one type argument. Thus,


567 
any \E{axiomatic} theory extension where each axiom refers to at most


568 
one type variable, may be trivially turned into a \E{definitional}


569 
one.


570 


571 
We illustrate this with the natural numbers in \Isa/\FOL:


572 


573 
\begin{ascbox}


574 
NatClass = FOL +\medskip


575 
consts


576 
"0" :: "'a" ("0")


577 
Suc :: "'a => 'a"


578 
rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip


579 
axclass


580 
nat < term


581 
induct "[ P(0); !!x. P(x) ==> P(Suc(x)) ] ==> P(n)"


582 
Suc_inject "Suc(m) = Suc(n) ==> m = n"


583 
Suc_neq_0 "Suc(m) = 0 ==> R"


584 
rec_0 "rec(0, a, f) = a"


585 
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip


586 
consts


587 
"+" :: "['a::nat, 'a] => 'a" (infixl 60)\medskip


588 
defs


589 
add_def "m + n == rec(m, n, %x y. Suc(y))"\medskip


590 
end


591 
\end{ascbox}


592 


593 
\TT{NatClass} is an abstract version of \TT{Nat}\footnote{See


594 
directory \TT{FOL/ex}.}. Basically, we have just replaced all


595 
occurrences of \E{type} \TT{nat} by $\alpha$ and used the natural


596 
number axioms to define \E{class} \TT{nat}\footnote{There's a snag:


597 
The original recursion operator \TT{rec} had to be made monomorphic,


598 
in a sense.}. Thus class \TT{nat} contains exactly those types


599 
$\tau$ that are isomorphic to ``the'' natural numbers (with signature


600 
\TT{0}, \TT{Suc}, \TT{rec}).


601 


602 
Furthermore, theory \TT{NatClass} defines an ``abstract constant'' $+$


603 
based on class \TT{nat}.


604 


605 
\medskip


606 


607 
What we have done here can be also viewed as \E{type specification}.


608 
Of course, it still remains open if there is some type at all that


609 
meets the class axioms. Now a very nice property of axiomatic type


610 
classes is, that abstract reasoning is always possible  independent


611 
of satisfiability. The metalogic won't break, even if some class (or


612 
general sort) turns out to be empty (``inconsistent'')


613 
later\footnote{As a consequence of an old bug, this is \E{not} true

4009

614 
for pre\Isa942 versions.}.

3167

615 


616 
For example, we may derive the following abstract natural numbers


617 
theorems:


618 


619 
\begin{ascbox}


620 
add_0: 0 + (?n::?'a::nat) = ?n


621 
add_Suc: Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n)


622 
\end{ascbox}


623 


624 
See also file \TT{FOL/ex/NatClass.ML}. Note that this required only


625 
some trivial modifications of the original \TT{Nat.ML}.


626 


627 

6623

628 
\section{The user interface of Isabelle's axclass package}

3167

629 


630 
The actual axiomatic type class package of \Isa/\Pure\ mainly consists


631 
of two new theory sections: \TT{axclass} and \TT{instance}. Some


632 
typical applications of these have already been demonstrated in


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


634 
completely.


635 


636 

6623

637 
\subsection{The axclass section}

3167

638 


639 
Within theory files, \TT{axclass} introduces an axiomatic type class


640 
definition. Its concrete syntax is:


641 


642 
\begin{matharray}{l}


643 
\TT{axclass} \\


644 
\ \ c \TT{ < } c_1\TT, \ldots\TT, c_n \\


645 
\ \ \idt{id}_1\ \idt{axm}_1 \\


646 
\ \ \vdots \\


647 
\ \ \idt{id}_m\ \idt{axm}_m


648 
\end{matharray}


649 


650 
Where $c, c_1, \ldots, c_n$ are classes (category $\idt{id}$ or


651 
$\idt{string}$) and $\idt{axm}_1, \ldots, \idt{axm}_m$ (with $m \ge


652 
0$) are formulas (category $\idt{string}$).


653 


654 
Class $c$ has to be new, and sort $\{c_1, \ldots, c_n\}$ a subsort of


655 
\TT{logic}. Each class axiom $\idt{axm}_j$ may contain any term


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


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


658 
of $\{c_1, \ldots, c_n\}$.


659 


660 
\medskip


661 


662 
The \TT{axclass} section declares $c$ as subclass of $c_1, \ldots,


663 
c_n$ to the type signature.


664 


665 
Furthermore, $\idt{axm}_1, \ldots, \idt{axm}_m$ are turned into the


666 
``abstract axioms'' of $c$ with names $\idt{id}_1, \ldots,


667 
\idt{id}_m$. This is done by replacing all occurring type variables


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


669 
variable will be prefixed by the logical precondition


670 
$\TT{OFCLASS}(\alpha :: \TT{logic}, c\TT{\_class})$.


671 


672 
Another axiom of name $c\TT{I}$  the ``class $c$ introduction


673 
rule''  is built from the respective universal closures of


674 
$\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately.


675 


676 

6623

677 
\subsection{The instance section}

3167

678 


679 
Section \TT{instance} proves class inclusions or type arities at the


680 
logical level and then transfers these into the type signature.


681 


682 
Its concrete syntax is:


683 


684 
\begin{matharray}{l}


685 
\TT{instance} \\


686 
\ \ [\ c_1 \TT{ < } c_2 \ \


687 
t \TT{ ::\ (}\idt{sort}_1\TT, \ldots \TT, \idt{sort}_n\TT) \idt{sort}\ ] \\


688 
\ \ [\ \TT(\idt{name}_1 \TT, \ldots\TT, \idt{name}_m\TT)\ ] \\


689 
\ \ [\ \TT{\{} \idt{text} \TT{\}}\ ]


690 
\end{matharray}


691 


692 
Where $c_1, c_2$ are classes and $t$ is an $n$place type constructor


693 
(all of category $\idt{id}$ or $\idt{string})$. Furthermore,


694 
$\idt{sort}_i$ are sorts in the usual \Isasyntax.


695 


696 
\medskip


697 


698 
Internally, \TT{instance} first sets up an appropriate goal that


699 
expresses the class inclusion or type arity as a metaproposition.


700 
Then tactic \TT{AxClass.axclass\_tac} is applied with all preceding


701 
metadefinitions of the current theory file and the usersupplied


702 
witnesses. The latter are $\idt{name}_1, \ldots, \idt{name}_m$, where


703 
$\idt{id}$ refers to an \MLname of a theorem, and $\idt{string}$ to an


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


705 
axioms from above this \TT{instance} in the theory file. Note


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


707 
processed completely.}.


708 


709 
Tactic \TT{AxClass.axclass\_tac} first unfolds the class definition by


710 
resolving with rule $c\TT{I}$, and then applies the witnesses


711 
according to their form: Metadefinitions are unfolded, all other


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


713 
enables proper object\E{rules} to be used as witnesses for


714 
corresponding class axioms.} with.


715 


716 
The final optional argument $\idt{text}$ is \MLcode of an arbitrary


717 
user tactic which is applied last to any remaining goals.


718 


719 
\medskip


720 


721 
Because of the complexity of \TT{instance}'s witnessing mechanisms,


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


723 
form $\TT{instance}\ \ldots\ (\idt{id}_1, \ldots, \idt{id}_m)$, where


724 
the identifiers refer to theorems that are appropriate type instances


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


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


727 


728 


729 
\begin{thebibliography}{}


730 


731 
\bibitem[Nipkow, 1993a]{Nipkowslides} T. Nipkow. Axiomatic Type


732 
Classes (in Isabelle). Presentation at the workshop \E{Types for


733 
Proof and Programs}, Nijmegen, 1993.


734 


735 
\bibitem[Nipkow, 1993b]{Nipkow93} T. Nipkow. OrderSorted Polymorphism


736 
in Isabelle. In G. Huet, G. Plotkin, editors, \E{Logical


737 
Environments}, pp.\ 164188, Cambridge University Press, 1993.


738 


739 
\bibitem[Paulson, 1994]{Paulson94} L.C. Paulson. \E{Isabelle  A


740 
Generic Theorem Prover}. LNCS 828, 1994.


741 


742 
\bibitem[Wenzel, 1994]{Wenzel94} M. Wenzel. \E{Axiomatische


743 
TypKlassen in Isabelle}. Diplom\arbeit, TU München, 1994.


744 


745 
\end{thebibliography}


746 


747 
\end{document}
