4 A Haskell-style type-system \cite{haskell-report} with ordered type-classes
5 has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
6 Initially, classes have mainly served as a \emph{purely syntactic} tool to
7 formulate polymorphic object-logics in a clean way, such as the standard
8 Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
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
12 as well \cite{nipkow-types93,nipkow-sorts93}. At that time, Isabelle still
13 lacked built-in support for these \emph{axiomatic type classes}. More
14 importantly, their semantics was not yet fully fleshed out (and unnecessarily
17 Since Isabelle94, actual axiomatic type classes have been an integral part of
18 Isabelle's meta-logic. This very simple implementation is based on a
19 straight-forward extension of traditional simply-typed Higher-Order Logic, by
20 including types qualified by logical predicates and overloaded constant
21 definitions (see \cite{Wenzel:1997:TPHOL} for further details).
23 Yet even until Isabelle99, there used to be still a fundamental methodological
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{isabelle-isar-ref}: 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.
34 So to cut a long story short, the present version of axiomatic type classes
35 now provides an even more useful and convenient mechanism for light-weight
36 abstract theories, without any special technical provisions to be observed by
40 \chapter{Examples}\label{sec:ex}
42 Axiomatic type classes are a concept of Isabelle's meta-logic
43 \cite{paulson-isa-book,Wenzel:1997:TPHOL}. They may be applied to any
44 object-logic that directly uses the meta type system, such as Isabelle/HOL
45 \cite{isabelle-HOL}. Subsequently, we present various examples that are all
46 formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
47 FOL. See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
48 \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
50 \input{generated/Semigroups}
52 \input{generated/Group}
54 \input{generated/Product}
56 \input{generated/NatClass}
59 %% FIXME move some parts to ref or isar-ref manual (!?);
61 % \chapter{The user interface of Isabelle's axclass package}
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
70 % \section{The axclass section}
72 % Within theory files, \texttt{axclass} introduces an axiomatic type class
73 % definition. Its concrete syntax is:
75 % \begin{matharray}{l}
77 % \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
83 % Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
84 % $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
85 % 0$) are formulas (category $string$).
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\}$.
95 % The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
96 % c@n$ to the type signature.
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})$.
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.
110 % \section{The instance section}
112 % Section \texttt{instance} proves class inclusions or type arities at the
113 % logical level and then transfers these into the type signature.
115 % Its concrete syntax is:
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{|\}}\ ]
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 Isabelle-syntax.
131 % Internally, \texttt{instance} first sets up an appropriate goal that
132 % expresses the class inclusion or type arity as a meta-proposition.
133 % Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
134 % meta-definitions of the current theory file and the user-supplied
135 % witnesses. The latter are $name@1, \ldots, name@m$, where
136 % $id$ refers to an \ML-name 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 \ML-toplevel only after the file is
140 % processed completely.}.
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: Meta-definitions 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.
149 % The final optional argument $text$ is \ML-code of an arbitrary
150 % user tactic which is applied last to any remaining goals.
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.
164 %%% TeX-master: "axclass"
166 % LocalWords: Isabelle FOL