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