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