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 lightweight 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 the final


32 
$\QED{}$, 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 
%%% TeXmaster: "isarref"


60 
%%% End:
