summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/AxClass/body.tex

author | aspinall |

Sun Dec 31 15:34:21 2006 +0100 (2006-12-31) | |

changeset 21973 | e7c9b0d3ce82 |

parent 17133 | 096792bdc58e |

permissions | -rw-r--r-- |

Quote arguments in PGIP exceptions. Tune comment.

2 \chapter{Introduction}

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

15 complicated, too).

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.

32 \medskip

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

37 the user.

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{Group/document/Semigroups}

52 \input{Group/document/Group}

54 \input{Group/document/Product}

56 \input{Nat/document/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

67 % completely.

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}

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}

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\}$.

93 % \medskip

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{|\}}\ ]

123 % \emphnd{matharray}

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.

129 % \medskip

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.

152 % \medskip

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.

162 %%% Local Variables:

163 %%% mode: latex

164 %%% TeX-master: "axclass"

165 %%% End:

166 % LocalWords: Isabelle FOL