doc-src/AxClass/body.tex

-
-\chapter{Introduction}
-
-A Haskell-style type-system \cite{haskell-report} with ordered type-classes
-has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
-Initially, classes have mainly served as a \emph{purely syntactic} tool to
-formulate polymorphic object-logics in a clean way, such as the standard
-Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
-
-Applying classes at the \emph{logical level} to provide a simple notion of
-abstract theories and instantiations to concrete ones, has been long proposed
-as well \cite{nipkow-types93,nipkow-sorts93}.  At that time, Isabelle still
-lacked built-in support for these \emph{axiomatic type classes}. More
-importantly, their semantics was not yet fully fleshed out (and unnecessarily
-complicated, too).
-
-Since Isabelle94, actual axiomatic type classes have been an integral part of
-Isabelle's meta-logic.  This very simple implementation is based on a
-straight-forward extension of traditional simply-typed Higher-Order Logic, by
-including types qualified by logical predicates and overloaded constant
-definitions (see \cite{Wenzel:1997:TPHOL} for further details).
-
-Yet even until Isabelle99, there used to be still a fundamental methodological
-problem in using axiomatic type classes conveniently, due to the traditional
-distinction of Isabelle theory files vs.\ ML proof scripts.  This has been
-finally overcome with the advent of Isabelle/Isar theories
-\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
-This nicely accommodates the usual procedure of defining axiomatic type
-classes, proving abstract properties, defining operations on concrete types,
-proving concrete properties for instantiation of classes etc.
-
-\medskip
-
-So to cut a long story short, the present version of axiomatic type classes
-now provides an even more useful and convenient mechanism for light-weight
-abstract theories, without any special technical provisions to be observed by
-the user.
-
-
-\chapter{Examples}\label{sec:ex}
-
-Axiomatic type classes are a concept of Isabelle's meta-logic
-\cite{paulson-isa-book,Wenzel:1997:TPHOL}.  They may be applied to any
-object-logic that directly uses the meta type system, such as Isabelle/HOL
-\cite{isabelle-HOL}.  Subsequently, we present various examples that are all
-formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
-FOL.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
-\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
-
-\input{Group/document/Semigroups}
-
-\input{Group/document/Group}
-
-\input{Group/document/Product}
-
-\input{Nat/document/NatClass}
-
-
-%% FIXME move some parts to ref or isar-ref manual (!?);
-
-% \chapter{The user interface of Isabelle's axclass package}
-
-% The actual axiomatic type class package of Isabelle/Pure mainly consists
-% of two new theory sections: \texttt{axclass} and \texttt{instance}.  Some
-% typical applications of these have already been demonstrated in
-% \secref{sec:ex}, below their syntax and semantics are presented more
-% completely.
-
-
-% \section{The axclass section}
-
-% Within theory files, \texttt{axclass} introduces an axiomatic type class
-% definition. Its concrete syntax is:
-
-% \begin{matharray}{l}
-%   \texttt{axclass} \\
-%   \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
-%   \ \ id@1\ axm@1 \\
-%   \ \ \vdots \\
-%   \ \ id@m\ axm@m
-% \emphnd{matharray}
-
-% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
-% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
-% 0$) are formulas (category $string$).
-
-% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
-% \texttt{logic}. Each class axiom $axm@j$ may contain any term
-% variables, but at most one type variable (which need not be the same
-% for all axioms). The sort of this type variable has to be a supersort
-% of $\{c@1, \ldots, c@n\}$.
-
-% \medskip
-
-% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
-% c@n$ to the type signature.
-
-% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
-% ``abstract axioms'' of $c$ with names $id@1, \ldots,
-% id@m$.  This is done by replacing all occurring type variables
-% by $\alpha :: c$. Original axioms that do not contain any type
-% variable will be prefixed by the logical precondition
-% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
-
-% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
-% rule'' --- is built from the respective universal closures of
-% $axm@1, \ldots, axm@m$ appropriately.
-
-
-% \section{The instance section}
-
-% Section \texttt{instance} proves class inclusions or type arities at the
-% logical level and then transfers these into the type signature.
-
-% Its concrete syntax is:
-
-% \begin{matharray}{l}
-%   \texttt{instance} \\
-%   \ \ [\ c@1 \texttt{ < } c@2 \ |\
-%       t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
-%   \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
-%   \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
-% \emphnd{matharray}
-
-% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
-% (all of category $id$ or $string)$. Furthermore,
-% $sort@i$ are sorts in the usual Isabelle-syntax.
-
-% \medskip
-
-% Internally, \texttt{instance} first sets up an appropriate goal that
-% expresses the class inclusion or type arity as a meta-proposition.
-% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
-% meta-definitions of the current theory file and the user-supplied
-% witnesses. The latter are $name@1, \ldots, name@m$, where
-% $id$ refers to an \ML-name of a theorem, and $string$ to an
-% axiom of the current theory node\footnote{Thus, the user may reference
-%   axioms from above this \texttt{instance} in the theory file. Note
-%   that new axioms appear at the \ML-toplevel only after the file is
-%   processed completely.}.
-
-% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
-% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
-% according to their form: Meta-definitions are unfolded, all other
-% formulas are repeatedly resolved\footnote{This is done in a way that
-%   enables proper object-\emph{rules} to be used as witnesses for
-%   corresponding class axioms.} with.
-
-% The final optional argument $text$ is \ML-code of an arbitrary
-% user tactic which is applied last to any remaining goals.
-
-% \medskip
-
-% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
-% new users of the axclass package are advised to only use the simple
-% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
-% the identifiers refer to theorems that are appropriate type instances
-% of the class axioms. This typically requires an auxiliary theory,
-% though, which defines some constants and then proves these witnesses.
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "axclass"
-%%% End: 
-% LocalWords:  Isabelle FOL