1 |
1 |
2 \documentclass[12pt,a4paper,fleqn]{report} |
2 \documentclass[12pt,a4paper,fleqn]{report} |
3 \usepackage{graphicx,../iman,../extra,../isar,../pdfsetup} |
3 \usepackage{graphicx,../iman,../extra,../isar,../pdfsetup} |
4 \usepackage{generated/isabelle,generated/isabellesym} |
4 \usepackage{generated/isabelle,generated/isabellesym} |
5 |
5 |
6 \newcommand{\isasymOtimes}{\emph{$\odot$}} |
6 \newcommand{\TIMES}{\cdot} |
|
7 \newcommand{\PLUS}{\oplus} |
|
8 \newcommand{\isasymOtimes}{\emph{$\cdot$}} |
7 \newcommand{\isasymOplus}{\emph{$\oplus$}} |
9 \newcommand{\isasymOplus}{\emph{$\oplus$}} |
8 \newcommand{\isasyminv}{\emph{${}^{-1}$}} |
10 \newcommand{\isasyminv}{\emph{${}^{-1}$}} |
9 \newcommand{\isasymunit}{\emph{$1$}} |
11 \newcommand{\isasymunit}{\emph{$1$}} |
10 \newcommand{\TIMES}{\odot} |
|
11 \newcommand{\PLUS}{\oplus} |
|
12 |
12 |
13 |
13 |
14 \newcommand{\secref}[1]{\S\ref{#1}} |
14 \newcommand{\secref}[1]{\S\ref{#1}} |
15 \newcommand{\figref}[1]{figure~\ref{#1}} |
15 \newcommand{\figref}[1]{figure~\ref{#1}} |
16 |
16 |
44 syntactically. In particular, the concept of \emph{Axiomatic Type Classes} |
44 syntactically. In particular, the concept of \emph{Axiomatic Type Classes} |
45 provides a useful light-weight mechanism for hierarchically-structured |
45 provides a useful light-weight mechanism for hierarchically-structured |
46 abstract theories. Subsequently, we demonstrate typical uses of Isabelle's |
46 abstract theories. Subsequently, we demonstrate typical uses of Isabelle's |
47 axiomatic type classes to model basic algebraic structures. |
47 axiomatic type classes to model basic algebraic structures. |
48 |
48 |
49 Note that this document describes axiomatic type classes using Isabelle/Isar |
49 This document describes axiomatic type classes using Isabelle/Isar theories, |
50 theories, with proofs expressed via Isar proof language elements. The new |
50 with proofs expressed via Isar proof language elements. The new theory |
51 theory format greatly simplifies the arrangement of the overall development, |
51 format greatly simplifies the arrangement of the overall development, since |
52 since definitions and proofs may be freely intermixed. Users who prefer |
52 definitions and proofs may be freely intermixed. Users who prefer tactic |
53 tactic scripts over structured proofs do not need to fall back on separate |
53 scripts over structured proofs do not need to fall back on separate ML |
54 ML scripts, but may refer to Isar's tactic emulation commands. |
54 scripts, though, but may refer to Isar's tactic emulation commands. |
55 \end{abstract} |
55 \end{abstract} |
56 |
56 |
57 |
57 |
58 \pagenumbering{roman} \tableofcontents \clearfirst |
58 \pagenumbering{roman} \tableofcontents \clearfirst |
59 |
59 |