diff -r 419116f1157a -r e23770bc97c8 doc-src/AxClass/body.tex --- a/doc-src/AxClass/body.tex Thu Feb 26 08:44:44 2009 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ - -\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