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: