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
 wenzelm@8890  1 wenzelm@8890  2 \chapter{Introduction}  wenzelm@8890  3 wenzelm@8890  4 A Haskell-style type-system \cite{haskell-report} with ordered type-classes  wenzelm@8907  5 has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.  wenzelm@8907  6 Initially, classes have mainly served as a \emph{purely syntactic} tool to  wenzelm@8907  7 formulate polymorphic object-logics in a clean way, such as the standard  wenzelm@8907  8 Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.  wenzelm@8890  9 wenzelm@8890  10 Applying classes at the \emph{logical level} to provide a simple notion of  wenzelm@8890  11 abstract theories and instantiations to concrete ones, has been long proposed  wenzelm@8907  12 as well \cite{nipkow-types93,nipkow-sorts93}. At that time, Isabelle still  wenzelm@8890  13 lacked built-in support for these \emph{axiomatic type classes}. More  wenzelm@8890  14 importantly, their semantics was not yet fully fleshed out (and unnecessarily  wenzelm@8890  15 complicated, too).  wenzelm@8890  16 wenzelm@8907  17 Since Isabelle94, actual axiomatic type classes have been an integral part of  wenzelm@8907  18 Isabelle's meta-logic. This very simple implementation is based on a  wenzelm@8907  19 straight-forward extension of traditional simply-typed Higher-Order Logic, by  wenzelm@8907  20 including types qualified by logical predicates and overloaded constant  wenzelm@8907  21 definitions (see \cite{Wenzel:1997:TPHOL} for further details).  wenzelm@8890  22 wenzelm@8907  23 Yet even until Isabelle99, there used to be still a fundamental methodological  wenzelm@8890  24 problem in using axiomatic type classes conveniently, due to the traditional  wenzelm@8890  25 distinction of Isabelle theory files vs.\ ML proof scripts. This has been  wenzelm@8890  26 finally overcome with the advent of Isabelle/Isar theories  wenzelm@8890  27 \cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.  wenzelm@8890  28 This nicely accommodates the usual procedure of defining axiomatic type  wenzelm@8890  29 classes, proving abstract properties, defining operations on concrete types,  wenzelm@8890  30 proving concrete properties for instantiation of classes etc.  wenzelm@8890  31 wenzelm@8890  32 \medskip  wenzelm@8890  33 wenzelm@8890  34 So to cut a long story short, the present version of axiomatic type classes  wenzelm@8907  35 now provides an even more useful and convenient mechanism for light-weight  wenzelm@8907  36 abstract theories, without any special technical provisions to be observed by  wenzelm@8907  37 the user.  wenzelm@8890  38 wenzelm@8890  39 wenzelm@8890  40 \chapter{Examples}\label{sec:ex}  wenzelm@8890  41 wenzelm@8890  42 Axiomatic type classes are a concept of Isabelle's meta-logic  wenzelm@8890  43 \cite{paulson-isa-book,Wenzel:1997:TPHOL}. They may be applied to any  wenzelm@8890  44 object-logic that directly uses the meta type system, such as Isabelle/HOL  wenzelm@8890  45 \cite{isabelle-HOL}. Subsequently, we present various examples that are all  wenzelm@8890  46 formulated within HOL, except the one of \secref{sec:ex-natclass} which is in  wenzelm@10140  47 FOL. See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and  wenzelm@8922  48 \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.  wenzelm@8890  49 wenzelm@17133  50 \input{Group/document/Semigroups}  wenzelm@8890  51 wenzelm@17133  52 \input{Group/document/Group}  wenzelm@8890  53 wenzelm@17133  54 \input{Group/document/Product}  wenzelm@8890  55 wenzelm@17133  56 \input{Nat/document/NatClass}  wenzelm@8890  57 wenzelm@8890  58 wenzelm@8890  59 %% FIXME move some parts to ref or isar-ref manual (!?);  wenzelm@8890  60 wenzelm@8890  61 % \chapter{The user interface of Isabelle's axclass package}  wenzelm@8890  62 wenzelm@8890  63 % The actual axiomatic type class package of Isabelle/Pure mainly consists  wenzelm@8890  64 % of two new theory sections: \texttt{axclass} and \texttt{instance}. Some  wenzelm@8890  65 % typical applications of these have already been demonstrated in  wenzelm@8890  66 % \secref{sec:ex}, below their syntax and semantics are presented more  wenzelm@8890  67 % completely.  wenzelm@8890  68 wenzelm@8890  69 wenzelm@8890  70 % \section{The axclass section}  wenzelm@8890  71 wenzelm@8890  72 % Within theory files, \texttt{axclass} introduces an axiomatic type class  wenzelm@8890  73 % definition. Its concrete syntax is:  wenzelm@8890  74 wenzelm@8890  75 % \begin{matharray}{l}  wenzelm@8890  76 % \texttt{axclass} \\  wenzelm@8890  77 % \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\  wenzelm@8890  78 % \ \ id@1\ axm@1 \\  wenzelm@8890  79 % \ \ \vdots \\  wenzelm@8890  80 % \ \ id@m\ axm@m  wenzelm@8890  81 % \emphnd{matharray}  wenzelm@8890  82 wenzelm@8890  83 % Where $c, c@1, \ldots, c@n$ are classes (category $id$ or  wenzelm@8906  84 % $string$) and $axm@1, \ldots, axm@m$ (with $m \geq  wenzelm@8890  85 % 0$) are formulas (category $string$).  wenzelm@8890  86 wenzelm@8890  87 % Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of  wenzelm@8890  88 % \texttt{logic}. Each class axiom $axm@j$ may contain any term  wenzelm@8890  89 % variables, but at most one type variable (which need not be the same  wenzelm@8890  90 % for all axioms). The sort of this type variable has to be a supersort  wenzelm@8890  91 % of $\{c@1, \ldots, c@n\}$.  wenzelm@8890  92 wenzelm@8890  93 % \medskip  wenzelm@8890  94 wenzelm@8890  95 % The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,  wenzelm@8890  96 % c@n$ to the type signature.  wenzelm@8890  97 wenzelm@8890  98 % Furthermore, $axm@1, \ldots, axm@m$ are turned into the  wenzelm@8890  99 % abstract axioms'' of $c$ with names $id@1, \ldots,  wenzelm@8890  100 % id@m$. This is done by replacing all occurring type variables  wenzelm@8890  101 % by $\alpha :: c$. Original axioms that do not contain any type  wenzelm@8890  102 % variable will be prefixed by the logical precondition  wenzelm@8890  103 % $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.  wenzelm@8890  104 wenzelm@8890  105 % Another axiom of name $c\texttt{I}$ --- the class $c$ introduction  wenzelm@8890  106 % rule'' --- is built from the respective universal closures of  wenzelm@8890  107 % $axm@1, \ldots, axm@m$ appropriately.  wenzelm@8890  108 wenzelm@8890  109 wenzelm@8890  110 % \section{The instance section}  wenzelm@8890  111 wenzelm@8890  112 % Section \texttt{instance} proves class inclusions or type arities at the  wenzelm@8890  113 % logical level and then transfers these into the type signature.  wenzelm@8890  114 wenzelm@8890  115 % Its concrete syntax is:  wenzelm@8890  116 wenzelm@8890  117 % \begin{matharray}{l}  wenzelm@8890  118 % \texttt{instance} \\  wenzelm@8890  119 % \ \ [\ c@1 \texttt{ < } c@2 \ |\  wenzelm@8890  120 % t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\  wenzelm@8890  121 % \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\  wenzelm@8890  122 % \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]  wenzelm@8890  123 % \emphnd{matharray}  wenzelm@8890  124 wenzelm@8890  125 % Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor  wenzelm@8890  126 % (all of category $id$ or $string)$. Furthermore,  wenzelm@8890  127 % $sort@i$ are sorts in the usual Isabelle-syntax.  wenzelm@8890  128 wenzelm@8890  129 % \medskip  wenzelm@8890  130 wenzelm@8890  131 % Internally, \texttt{instance} first sets up an appropriate goal that  wenzelm@8890  132 % expresses the class inclusion or type arity as a meta-proposition.  wenzelm@8890  133 % Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding  wenzelm@8890  134 % meta-definitions of the current theory file and the user-supplied  wenzelm@8890  135 % witnesses. The latter are $name@1, \ldots, name@m$, where  wenzelm@8890  136 % $id$ refers to an \ML-name of a theorem, and $string$ to an  wenzelm@8890  137 % axiom of the current theory node\footnote{Thus, the user may reference  wenzelm@8890  138 % axioms from above this \texttt{instance} in the theory file. Note  wenzelm@8890  139 % that new axioms appear at the \ML-toplevel only after the file is  wenzelm@8890  140 % processed completely.}.  wenzelm@8890  141 wenzelm@8890  142 % Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by  wenzelm@8890  143 % resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses  wenzelm@8890  144 % according to their form: Meta-definitions are unfolded, all other  wenzelm@8890  145 % formulas are repeatedly resolved\footnote{This is done in a way that  wenzelm@8890  146 % enables proper object-\emph{rules} to be used as witnesses for  wenzelm@8890  147 % corresponding class axioms.} with.  wenzelm@8890  148 wenzelm@8890  149 % The final optional argument $text$ is \ML-code of an arbitrary  wenzelm@8890  150 % user tactic which is applied last to any remaining goals.  wenzelm@8890  151 wenzelm@8890  152 % \medskip  wenzelm@8890  153 wenzelm@8890  154 % Because of the complexity of \texttt{instance}'s witnessing mechanisms,  wenzelm@8890  155 % new users of the axclass package are advised to only use the simple  wenzelm@8890  156 % form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where  wenzelm@8890  157 % the identifiers refer to theorems that are appropriate type instances  wenzelm@8890  158 % of the class axioms. This typically requires an auxiliary theory,  wenzelm@8890  159 % though, which defines some constants and then proves these witnesses.  wenzelm@8890  160 wenzelm@8890  161 wenzelm@8890  162 %%% Local Variables:  wenzelm@8890  163 %%% mode: latex  wenzelm@8890  164 %%% TeX-master: "axclass"  wenzelm@8890  165 %%% End:  wenzelm@8890  166 % LocalWords: Isabelle FOL