doc-src/AxClass/axclass.tex
 author wenzelm Sat, 01 Jul 2000 19:49:20 +0200 changeset 9226 cbe6144f0f15 parent 8907 813fabceec00 child 10140 ba9297b71897 permissions -rw-r--r--
tuned;


\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{graphicx,../iman,../extra,../isar,../pdfsetup}
\usepackage{generated/isabelle,generated/isabellesym}

\newcommand{\TIMES}{\cdot}
\newcommand{\PLUS}{\oplus}
\newcommand{\isasymOtimes}{\emph{$\cdot$}}
\newcommand{\isasymOplus}{\emph{$\oplus$}}
\newcommand{\isasyminv}{\emph{${}^{-1}$}}
\newcommand{\isasymunit}{\emph{$1$}}

\newcommand{\secref}[1]{\S\ref{#1}}
\newcommand{\figref}[1]{figure~\ref{#1}}

\hyphenation{Isabelle}
\hyphenation{Isar}

\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Using Axiomatic Type Classes in Isabelle}
\author{\emph{Markus Wenzel} \\ TU M\"unchen}

\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

\sloppy
\binperiod     %%%treat . like a binary operator

\begin{document}

\underscoreoff

\maketitle

\begin{abstract}
Isabelle offers order-sorted type classes on top of the simple types of
plain Higher-Order Logic.  The resulting type system is similar to that of
the programming language Haskell.  Its interpretation within the logic
enables further application, though, apart from restricting polymorphism
syntactically.  In particular, the concept of \emph{Axiomatic Type Classes}
provides a useful light-weight mechanism for hierarchically-structured
abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
axiomatic type classes to model basic algebraic structures.

This document describes axiomatic type classes using Isabelle/Isar theories,
with proofs expressed via Isar proof language elements.  The new theory
format greatly simplifies the arrangement of the overall development, since
definitions and proofs may be freely intermixed.  Users who prefer tactic
scripts over structured proofs do not need to fall back on separate ML
scripts, though, but may refer to Isar's tactic emulation commands.
\end{abstract}

\pagenumbering{roman} \tableofcontents \clearfirst

\include{body}

%FIXME
\nocite{nipkow-types93}
\nocite{nipkow-sorts93}
\nocite{Wenzel:1997:TPHOL}
\nocite{paulson-isa-book}
\nocite{isabelle-isar-ref}
\nocite{Wenzel:1999:TPHOL}

\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
% LocalWords:  Isabelle FIXME