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;
wenzelm@7135
     1
wenzelm@7135
     2
\chapter{Generic Tools and Packages}
wenzelm@7135
     3
wenzelm@7135
     4
\section{Axiomatic Type Classes}\label{sec:axclass}
wenzelm@7135
     5
wenzelm@7135
     6
\indexisarcmd{axclass}\indexisarcmd{instance}
wenzelm@7135
     7
\begin{matharray}{rcl}
wenzelm@7135
     8
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm@7135
     9
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7135
    10
\end{matharray}
wenzelm@7135
    11
wenzelm@7135
    12
Axiomatic type classes are provided by Isabelle/Pure as a purely
wenzelm@7135
    13
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
wenzelm@7135
    14
any object logic may make use of this light-weight mechanism for abstract
wenzelm@7135
    15
theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
wenzelm@7135
    16
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
wenzelm@7135
    17
the standard Isabelle documentation.
wenzelm@7135
    18
wenzelm@7135
    19
\begin{rail}
wenzelm@7135
    20
  'axclass' classdecl (axmdecl prop comment? +)
wenzelm@7135
    21
  ;
wenzelm@7135
    22
  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
wenzelm@7135
    23
  ;
wenzelm@7135
    24
\end{rail}
wenzelm@7135
    25
wenzelm@7135
    26
\begin{description}
wenzelm@7135
    27
\item [$\isarkeyword{axclass}~$] FIXME
wenzelm@7135
    28
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
wenzelm@7135
    29
  c@2$] setup up a goal stating the class relation or type arity.  The proof
wenzelm@7135
    30
  would usually proceed by the $expand_classes$ method, and then establish the
wenzelm@7141
    31
  characteristic theorems of the type classes involved.  After finishing the
wenzelm@7141
    32
  proof the theory will be augmented by a type signature declaration
wenzelm@7135
    33
  corresponding to the resulting theorem.
wenzelm@7135
    34
\end{description}
wenzelm@7135
    35
wenzelm@7135
    36
wenzelm@7135
    37
wenzelm@7135
    38
\section{The Simplifier}
wenzelm@7135
    39
wenzelm@7135
    40
\section{The Classical Reasoner}
wenzelm@7135
    41
wenzelm@7135
    42
wenzelm@7135
    43
%\indexisarcmd{}
wenzelm@7135
    44
%\begin{matharray}{rcl}
wenzelm@7135
    45
%  \isarcmd{} & : & \isartrans{}{} \\
wenzelm@7135
    46
%\end{matharray}
wenzelm@7135
    47
wenzelm@7135
    48
%\begin{rail}
wenzelm@7135
    49
  
wenzelm@7135
    50
%\end{rail}
wenzelm@7135
    51
wenzelm@7135
    52
%\begin{description}
wenzelm@7135
    53
%\item [$ $]
wenzelm@7135
    54
%\end{description}
wenzelm@7135
    55
wenzelm@7135
    56
wenzelm@7135
    57
%%% Local Variables: 
wenzelm@7135
    58
%%% mode: latex
wenzelm@7135
    59
%%% TeX-master: "isar-ref"
wenzelm@7135
    60
%%% End: