7135
|
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
|
7141
|
31 |
characteristic theorems of the type classes involved. After finishing the
|
|
32 |
proof the theory will be augmented by a type signature declaration
|
7135
|
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:
|