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