1.1 --- a/doc-src/AxClass/body.tex Wed Mar 04 11:05:02 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,166 +0,0 @@
1.4 -
1.5 -\chapter{Introduction}
1.6 -
1.7 -A Haskell-style type-system \cite{haskell-report} with ordered type-classes
1.8 -has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
1.9 -Initially, classes have mainly served as a \emph{purely syntactic} tool to
1.10 -formulate polymorphic object-logics in a clean way, such as the standard
1.11 -Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
1.12 -
1.13 -Applying classes at the \emph{logical level} to provide a simple notion of
1.14 -abstract theories and instantiations to concrete ones, has been long proposed
1.15 -as well \cite{nipkow-types93,nipkow-sorts93}. At that time, Isabelle still
1.16 -lacked built-in support for these \emph{axiomatic type classes}. More
1.17 -importantly, their semantics was not yet fully fleshed out (and unnecessarily
1.18 -complicated, too).
1.19 -
1.20 -Since Isabelle94, actual axiomatic type classes have been an integral part of
1.21 -Isabelle's meta-logic. This very simple implementation is based on a
1.22 -straight-forward extension of traditional simply-typed Higher-Order Logic, by
1.23 -including types qualified by logical predicates and overloaded constant
1.24 -definitions (see \cite{Wenzel:1997:TPHOL} for further details).
1.25 -
1.26 -Yet even until Isabelle99, there used to be still a fundamental methodological
1.27 -problem in using axiomatic type classes conveniently, due to the traditional
1.28 -distinction of Isabelle theory files vs.\ ML proof scripts. This has been
1.29 -finally overcome with the advent of Isabelle/Isar theories
1.30 -\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
1.31 -This nicely accommodates the usual procedure of defining axiomatic type
1.32 -classes, proving abstract properties, defining operations on concrete types,
1.33 -proving concrete properties for instantiation of classes etc.
1.34 -
1.35 -\medskip
1.36 -
1.37 -So to cut a long story short, the present version of axiomatic type classes
1.38 -now provides an even more useful and convenient mechanism for light-weight
1.39 -abstract theories, without any special technical provisions to be observed by
1.40 -the user.
1.41 -
1.42 -
1.43 -\chapter{Examples}\label{sec:ex}
1.44 -
1.45 -Axiomatic type classes are a concept of Isabelle's meta-logic
1.46 -\cite{paulson-isa-book,Wenzel:1997:TPHOL}. They may be applied to any
1.47 -object-logic that directly uses the meta type system, such as Isabelle/HOL
1.48 -\cite{isabelle-HOL}. Subsequently, we present various examples that are all
1.49 -formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
1.50 -FOL. See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
1.51 -\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
1.52 -
1.53 -\input{Group/document/Semigroups}
1.54 -
1.55 -\input{Group/document/Group}
1.56 -
1.57 -\input{Group/document/Product}
1.58 -
1.59 -\input{Nat/document/NatClass}
1.60 -
1.61 -
1.62 -%% FIXME move some parts to ref or isar-ref manual (!?);
1.63 -
1.64 -% \chapter{The user interface of Isabelle's axclass package}
1.65 -
1.66 -% The actual axiomatic type class package of Isabelle/Pure mainly consists
1.67 -% of two new theory sections: \texttt{axclass} and \texttt{instance}. Some
1.68 -% typical applications of these have already been demonstrated in
1.69 -% \secref{sec:ex}, below their syntax and semantics are presented more
1.70 -% completely.
1.71 -
1.72 -
1.73 -% \section{The axclass section}
1.74 -
1.75 -% Within theory files, \texttt{axclass} introduces an axiomatic type class
1.76 -% definition. Its concrete syntax is:
1.77 -
1.78 -% \begin{matharray}{l}
1.79 -% \texttt{axclass} \\
1.80 -% \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
1.81 -% \ \ id@1\ axm@1 \\
1.82 -% \ \ \vdots \\
1.83 -% \ \ id@m\ axm@m
1.84 -% \emphnd{matharray}
1.85 -
1.86 -% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
1.87 -% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
1.88 -% 0$) are formulas (category $string$).
1.89 -
1.90 -% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
1.91 -% \texttt{logic}. Each class axiom $axm@j$ may contain any term
1.92 -% variables, but at most one type variable (which need not be the same
1.93 -% for all axioms). The sort of this type variable has to be a supersort
1.94 -% of $\{c@1, \ldots, c@n\}$.
1.95 -
1.96 -% \medskip
1.97 -
1.98 -% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
1.99 -% c@n$ to the type signature.
1.100 -
1.101 -% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
1.102 -% ``abstract axioms'' of $c$ with names $id@1, \ldots,
1.103 -% id@m$. This is done by replacing all occurring type variables
1.104 -% by $\alpha :: c$. Original axioms that do not contain any type
1.105 -% variable will be prefixed by the logical precondition
1.106 -% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
1.107 -
1.108 -% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
1.109 -% rule'' --- is built from the respective universal closures of
1.110 -% $axm@1, \ldots, axm@m$ appropriately.
1.111 -
1.112 -
1.113 -% \section{The instance section}
1.114 -
1.115 -% Section \texttt{instance} proves class inclusions or type arities at the
1.116 -% logical level and then transfers these into the type signature.
1.117 -
1.118 -% Its concrete syntax is:
1.119 -
1.120 -% \begin{matharray}{l}
1.121 -% \texttt{instance} \\
1.122 -% \ \ [\ c@1 \texttt{ < } c@2 \ |\
1.123 -% t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
1.124 -% \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
1.125 -% \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
1.126 -% \emphnd{matharray}
1.127 -
1.128 -% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
1.129 -% (all of category $id$ or $string)$. Furthermore,
1.130 -% $sort@i$ are sorts in the usual Isabelle-syntax.
1.131 -
1.132 -% \medskip
1.133 -
1.134 -% Internally, \texttt{instance} first sets up an appropriate goal that
1.135 -% expresses the class inclusion or type arity as a meta-proposition.
1.136 -% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
1.137 -% meta-definitions of the current theory file and the user-supplied
1.138 -% witnesses. The latter are $name@1, \ldots, name@m$, where
1.139 -% $id$ refers to an \ML-name of a theorem, and $string$ to an
1.140 -% axiom of the current theory node\footnote{Thus, the user may reference
1.141 -% axioms from above this \texttt{instance} in the theory file. Note
1.142 -% that new axioms appear at the \ML-toplevel only after the file is
1.143 -% processed completely.}.
1.144 -
1.145 -% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
1.146 -% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
1.147 -% according to their form: Meta-definitions are unfolded, all other
1.148 -% formulas are repeatedly resolved\footnote{This is done in a way that
1.149 -% enables proper object-\emph{rules} to be used as witnesses for
1.150 -% corresponding class axioms.} with.
1.151 -
1.152 -% The final optional argument $text$ is \ML-code of an arbitrary
1.153 -% user tactic which is applied last to any remaining goals.
1.154 -
1.155 -% \medskip
1.156 -
1.157 -% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
1.158 -% new users of the axclass package are advised to only use the simple
1.159 -% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
1.160 -% the identifiers refer to theorems that are appropriate type instances
1.161 -% of the class axioms. This typically requires an auxiliary theory,
1.162 -% though, which defines some constants and then proves these witnesses.
1.163 -
1.164 -
1.165 -%%% Local Variables:
1.166 -%%% mode: latex
1.167 -%%% TeX-master: "axclass"
1.168 -%%% End:
1.169 -% LocalWords: Isabelle FOL