doc-src/AxClass/axclass.tex
 author nipkow Sun Mar 02 15:02:06 2008 +0100 (2008-03-02) changeset 26191 ae537f315b34 parent 17133 096792bdc58e child 26913 67040326ab7a permissions -rw-r--r--
Generalized Zorn and added well-ordering theorem
     1

     2 \documentclass[12pt,a4paper,fleqn]{report}

     3 \usepackage{graphicx,../iman,../extra,../isar}

     4 \usepackage{Group/document/isabelle,Group/document/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