doc-src/AxClass/body.tex
 author nipkow Sun Mar 02 15:02:06 2008 +0100 (2008-03-02) changeset 26191 ae537f315b34 parent 17133 096792bdc58e permissions -rw-r--r--
Generalized Zorn and added well-ordering theorem
     1

     2 \chapter{Introduction}

     3

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

     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

    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).

    16

    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).

    22

    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.

    31

    32 \medskip

    33

    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.

    38

    39

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

    41

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

    49

    50 \input{Group/document/Semigroups}

    51

    52 \input{Group/document/Group}

    53

    54 \input{Group/document/Product}

    55

    56 \input{Nat/document/NatClass}

    57

    58

    59 %% FIXME move some parts to ref or isar-ref 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

    84 % $string$) and $axm@1, \ldots, axm@m$ (with $m \geq   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 Isabelle-syntax.

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

   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: 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.

   148

   149 % The final optional argument $text$ is \ML-code 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 %%% TeX-master: "axclass"

   165 %%% End:

   166 % LocalWords:  Isabelle FOL