doc-src/IsarRef/generic.tex
 author wenzelm Fri Jul 30 18:27:25 1999 +0200 (1999-07-30) changeset 7141 a67dde8820c0 parent 7135 8eabfd7e6b9b child 7167 0b2e3ef1d8f4 permissions -rw-r--r--
even more stuff;
     1

     2 \chapter{Generic Tools and Packages}

     3

     4 \section{Axiomatic Type Classes}\label{sec:axclass}

     5

     6 \indexisarcmd{axclass}\indexisarcmd{instance}

     7 \begin{matharray}{rcl}

     8   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\

     9   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\

    10 \end{matharray}

    11

    12 Axiomatic type classes are provided by Isabelle/Pure as a purely

    13 \emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus

    14 any object logic may make use of this light-weight mechanism for abstract

    15 theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a

    16 tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of

    17 the standard Isabelle documentation.

    18

    19 \begin{rail}

    20   'axclass' classdecl (axmdecl prop comment? +)

    21   ;

    22   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?

    23   ;

    24 \end{rail}

    25

    26 \begin{description}

    27 \item [$\isarkeyword{axclass}~$] FIXME

    28 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <   29 c@2$] setup up a goal stating the class relation or type arity.  The proof

    30   would usually proceed by the $expand_classes$ method, and then establish the

    31   characteristic theorems of the type classes involved.  After finishing the

    32   proof the theory will be augmented by a type signature declaration

    33   corresponding to the resulting theorem.

    34 \end{description}

    35

    36

    37

    38 \section{The Simplifier}

    39

    40 \section{The Classical Reasoner}

    41

    42

    43 %\indexisarcmd{}

    44 %\begin{matharray}{rcl}

    45 %  \isarcmd{} & : & \isartrans{}{} \\

    46 %\end{matharray}

    47

    48 %\begin{rail}

    49

    50 %\end{rail}

    51

    52 %\begin{description}

    53 %\item []

    54 %\end{description}

    55

    56

    57 %%% Local Variables:

    58 %%% mode: latex

    59 %%% TeX-master: "isar-ref"

    60 %%% End: