doc-src/AxClass/body.tex
author nipkow
Thu, 11 Jul 2002 09:17:01 +0200
changeset 13343 3b2b18c58d80
parent 10140 ba9297b71897
child 17133 096792bdc58e
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     1
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     2
\chapter{Introduction}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     3
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     4
A Haskell-style type-system \cite{haskell-report} with ordered type-classes
8907
wenzelm
parents: 8906
diff changeset
     5
has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
wenzelm
parents: 8906
diff changeset
     6
Initially, classes have mainly served as a \emph{purely syntactic} tool to
wenzelm
parents: 8906
diff changeset
     7
formulate polymorphic object-logics in a clean way, such as the standard
wenzelm
parents: 8906
diff changeset
     8
Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     9
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    10
Applying classes at the \emph{logical level} to provide a simple notion of
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    11
abstract theories and instantiations to concrete ones, has been long proposed
8907
wenzelm
parents: 8906
diff changeset
    12
as well \cite{nipkow-types93,nipkow-sorts93}.  At that time, Isabelle still
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    13
lacked built-in support for these \emph{axiomatic type classes}. More
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    14
importantly, their semantics was not yet fully fleshed out (and unnecessarily
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    15
complicated, too).
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    16
8907
wenzelm
parents: 8906
diff changeset
    17
Since Isabelle94, actual axiomatic type classes have been an integral part of
wenzelm
parents: 8906
diff changeset
    18
Isabelle's meta-logic.  This very simple implementation is based on a
wenzelm
parents: 8906
diff changeset
    19
straight-forward extension of traditional simply-typed Higher-Order Logic, by
wenzelm
parents: 8906
diff changeset
    20
including types qualified by logical predicates and overloaded constant
wenzelm
parents: 8906
diff changeset
    21
definitions (see \cite{Wenzel:1997:TPHOL} for further details).
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    22
8907
wenzelm
parents: 8906
diff changeset
    23
Yet even until Isabelle99, there used to be still a fundamental methodological
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    24
problem in using axiomatic type classes conveniently, due to the traditional
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    25
distinction of Isabelle theory files vs.\ ML proof scripts.  This has been
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    26
finally overcome with the advent of Isabelle/Isar theories
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    27
\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    28
This nicely accommodates the usual procedure of defining axiomatic type
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    29
classes, proving abstract properties, defining operations on concrete types,
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    30
proving concrete properties for instantiation of classes etc.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    31
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    32
\medskip
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    33
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    34
So to cut a long story short, the present version of axiomatic type classes
8907
wenzelm
parents: 8906
diff changeset
    35
now provides an even more useful and convenient mechanism for light-weight
wenzelm
parents: 8906
diff changeset
    36
abstract theories, without any special technical provisions to be observed by
wenzelm
parents: 8906
diff changeset
    37
the user.
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    38
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    39
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    40
\chapter{Examples}\label{sec:ex}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    41
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    42
Axiomatic type classes are a concept of Isabelle's meta-logic
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    43
\cite{paulson-isa-book,Wenzel:1997:TPHOL}.  They may be applied to any
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    44
object-logic that directly uses the meta type system, such as Isabelle/HOL
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    45
\cite{isabelle-HOL}.  Subsequently, we present various examples that are all
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    46
formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
10140
ba9297b71897 major cleanup -- improved typesetting;
wenzelm
parents: 8922
diff changeset
    47
FOL.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
8922
wenzelm
parents: 8907
diff changeset
    48
\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    49
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    50
\input{generated/Semigroups}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    51
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    52
\input{generated/Group}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    53
8903
78d6e47469e4 new Isar version;
wenzelm
parents: 8890
diff changeset
    54
\input{generated/Product}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    55
8903
78d6e47469e4 new Isar version;
wenzelm
parents: 8890
diff changeset
    56
\input{generated/NatClass}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    57
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    58
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    59
%% FIXME move some parts to ref or isar-ref manual (!?);
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    60
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    61
% \chapter{The user interface of Isabelle's axclass package}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    62
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    63
% The actual axiomatic type class package of Isabelle/Pure mainly consists
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    64
% of two new theory sections: \texttt{axclass} and \texttt{instance}.  Some
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    65
% typical applications of these have already been demonstrated in
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    66
% \secref{sec:ex}, below their syntax and semantics are presented more
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    67
% completely.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    68
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    69
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    70
% \section{The axclass section}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    71
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    72
% Within theory files, \texttt{axclass} introduces an axiomatic type class
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    73
% definition. Its concrete syntax is:
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    74
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    75
% \begin{matharray}{l}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    76
%   \texttt{axclass} \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    77
%   \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    78
%   \ \ id@1\ axm@1 \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    79
%   \ \ \vdots \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    80
%   \ \ id@m\ axm@m
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    81
% \emphnd{matharray}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    82
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    83
% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
8906
wenzelm
parents: 8903
diff changeset
    84
% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    85
% 0$) are formulas (category $string$).
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    86
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    87
% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    88
% \texttt{logic}. Each class axiom $axm@j$ may contain any term
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    89
% variables, but at most one type variable (which need not be the same
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    90
% for all axioms). The sort of this type variable has to be a supersort
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    91
% of $\{c@1, \ldots, c@n\}$.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    92
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    93
% \medskip
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    94
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    95
% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    96
% c@n$ to the type signature.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    97
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    98
% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    99
% ``abstract axioms'' of $c$ with names $id@1, \ldots,
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   100
% id@m$.  This is done by replacing all occurring type variables
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   101
% by $\alpha :: c$. Original axioms that do not contain any type
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   102
% variable will be prefixed by the logical precondition
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   103
% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   104
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   105
% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   106
% rule'' --- is built from the respective universal closures of
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   107
% $axm@1, \ldots, axm@m$ appropriately.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   108
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   109
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   110
% \section{The instance section}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   111
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   112
% Section \texttt{instance} proves class inclusions or type arities at the
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   113
% logical level and then transfers these into the type signature.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   114
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   115
% Its concrete syntax is:
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   116
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   117
% \begin{matharray}{l}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   118
%   \texttt{instance} \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   119
%   \ \ [\ c@1 \texttt{ < } c@2 \ |\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   120
%       t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   121
%   \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   122
%   \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   123
% \emphnd{matharray}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   124
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   125
% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   126
% (all of category $id$ or $string)$. Furthermore,
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   127
% $sort@i$ are sorts in the usual Isabelle-syntax.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   128
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   129
% \medskip
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   130
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   131
% Internally, \texttt{instance} first sets up an appropriate goal that
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   132
% expresses the class inclusion or type arity as a meta-proposition.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   133
% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   134
% meta-definitions of the current theory file and the user-supplied
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   135
% witnesses. The latter are $name@1, \ldots, name@m$, where
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   136
% $id$ refers to an \ML-name of a theorem, and $string$ to an
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   137
% axiom of the current theory node\footnote{Thus, the user may reference
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   138
%   axioms from above this \texttt{instance} in the theory file. Note
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   139
%   that new axioms appear at the \ML-toplevel only after the file is
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   140
%   processed completely.}.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   141
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   142
% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   143
% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   144
% according to their form: Meta-definitions are unfolded, all other
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   145
% formulas are repeatedly resolved\footnote{This is done in a way that
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   146
%   enables proper object-\emph{rules} to be used as witnesses for
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   147
%   corresponding class axioms.} with.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   148
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   149
% The final optional argument $text$ is \ML-code of an arbitrary
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   150
% user tactic which is applied last to any remaining goals.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   151
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   152
% \medskip
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   153
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   154
% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   155
% new users of the axclass package are advised to only use the simple
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   156
% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   157
% the identifiers refer to theorems that are appropriate type instances
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   158
% of the class axioms. This typically requires an auxiliary theory,
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   159
% though, which defines some constants and then proves these witnesses.
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   160
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   161
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   162
%%% Local Variables: 
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   163
%%% mode: latex
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   164
%%% TeX-master: "axclass"
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   165
%%% End: 
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   166
% LocalWords:  Isabelle FOL