1 |
|
2 \documentclass[12pt,a4paper,fleqn]{report} |
|
3 \usepackage{graphicx,../iman,../extra,../isar} |
|
4 \usepackage{../isabelle,../isabellesym} |
|
5 \usepackage{../pdfsetup} % last one! |
|
6 |
|
7 \isabellestyle{it} |
|
8 \newcommand{\isasyminv}{\isamath{{}^{-1}}} |
|
9 \renewcommand{\isasymzero}{\isamath{0}} |
|
10 \renewcommand{\isasymone}{\isamath{1}} |
|
11 |
|
12 \newcommand{\secref}[1]{\S\ref{#1}} |
|
13 \newcommand{\figref}[1]{figure~\ref{#1}} |
|
14 |
|
15 \hyphenation{Isabelle} |
|
16 \hyphenation{Isar} |
|
17 \hyphenation{Haskell} |
|
18 |
|
19 \title{\includegraphics[scale=0.5]{isabelle_isar} |
|
20 \\[4ex] Using Axiomatic Type Classes in Isabelle} |
|
21 \author{\emph{Markus Wenzel} \\ TU M\"unchen} |
|
22 |
|
23 |
|
24 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
|
25 |
|
26 \pagestyle{headings} |
|
27 \sloppy |
|
28 \binperiod %%%treat . like a binary operator |
|
29 |
|
30 |
|
31 \begin{document} |
|
32 |
|
33 \underscoreoff |
|
34 |
|
35 \maketitle |
|
36 |
|
37 \begin{abstract} |
|
38 Isabelle offers order-sorted type classes on top of the simple types of |
|
39 plain Higher-Order Logic. The resulting type system is similar to that of |
|
40 the programming language Haskell. Its interpretation within the logic |
|
41 enables further application, though, apart from restricting polymorphism |
|
42 syntactically. In particular, the concept of \emph{Axiomatic Type Classes} |
|
43 provides a useful light-weight mechanism for hierarchically-structured |
|
44 abstract theories. Subsequently, we demonstrate typical uses of Isabelle's |
|
45 axiomatic type classes to model basic algebraic structures. |
|
46 |
|
47 This document describes axiomatic type classes using Isabelle/Isar theories, |
|
48 with proofs expressed via Isar proof language elements. The new theory |
|
49 format greatly simplifies the arrangement of the overall development, since |
|
50 definitions and proofs may be freely intermixed. Users who prefer tactic |
|
51 scripts over structured proofs do not need to fall back on separate ML |
|
52 scripts, though, but may refer to Isar's tactic emulation commands. |
|
53 \end{abstract} |
|
54 |
|
55 |
|
56 \pagenumbering{roman} \tableofcontents \clearfirst |
|
57 |
|
58 \include{body} |
|
59 |
|
60 %FIXME |
|
61 \nocite{nipkow-types93} |
|
62 \nocite{nipkow-sorts93} |
|
63 \nocite{Wenzel:1997:TPHOL} |
|
64 \nocite{paulson-isa-book} |
|
65 \nocite{isabelle-isar-ref} |
|
66 \nocite{Wenzel:1999:TPHOL} |
|
67 |
|
68 \begingroup |
|
69 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
70 \bibliography{../manual} |
|
71 \endgroup |
|
72 |
|
73 \end{document} |
|
74 |
|
75 |
|
76 %%% Local Variables: |
|
77 %%% mode: latex |
|
78 %%% TeX-master: t |
|
79 %%% End: |
|
80 % LocalWords: Isabelle FIXME |
|