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