src/HOL/Lattice/document/root.tex
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 10157 6d3987f3aad9
child 36862 952b2b102a0a
permissions -rw-r--r--
Name.uu, Name.aT;
wenzelm@10157
     1
wenzelm@10157
     2
% $Id$
wenzelm@10157
     3
wenzelm@10157
     4
\documentclass[11pt,a4paper]{article}
wenzelm@10157
     5
\usepackage{isabelle,isabellesym,pdfsetup}
wenzelm@10157
     6
\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@10157
     7
wenzelm@10157
     8
\urlstyle{rm}\isabellestyle{it}
wenzelm@10157
     9
\pagestyle{headings}
wenzelm@10157
    10
wenzelm@10157
    11
\hyphenation{Isabelle}
wenzelm@10157
    12
\hyphenation{Isar}
wenzelm@10157
    13
wenzelm@10157
    14
wenzelm@10157
    15
\begin{document}
wenzelm@10157
    16
wenzelm@10157
    17
\title{Lattices and Orders in Isabelle/HOL}
wenzelm@10157
    18
\author{Markus Wenzel \\ TU M\"unchen}
wenzelm@10157
    19
\maketitle
wenzelm@10157
    20
wenzelm@10157
    21
\begin{abstract}
wenzelm@10157
    22
  We consider abstract structures of orders and lattices.  Many fundamental
wenzelm@10157
    23
  concepts of lattice theory are developed, including dual structures,
wenzelm@10157
    24
  properties of bounds versus algebraic laws, lattice operations versus
wenzelm@10157
    25
  set-theoretic ones etc.  We also give example instantiations of lattices and
wenzelm@10157
    26
  orders, such as direct products and function spaces.  Well-known properties
wenzelm@10157
    27
  are demonstrated, like the Knaster-Tarski Theorem for complete lattices.
wenzelm@10157
    28
  
wenzelm@10157
    29
  This formal theory development may serve as an example of applying
wenzelm@10157
    30
  Isabelle/HOL to the domain of mathematical reasoning about ``axiomatic''
wenzelm@10157
    31
  structures.  Apart from the simply-typed classical set-theory of HOL, we
wenzelm@10157
    32
  employ Isabelle's system of axiomatic type classes for expressing structures
wenzelm@10157
    33
  and functors in a light-weight manner.  Proofs are expressed in the Isar
wenzelm@10157
    34
  language for readable formal proof, while aiming at its ``best-style'' of
wenzelm@10157
    35
  representing formal reasoning.
wenzelm@10157
    36
\end{abstract}
wenzelm@10157
    37
wenzelm@10157
    38
\tableofcontents
wenzelm@10157
    39
wenzelm@10157
    40
\newpage
wenzelm@10157
    41
{
wenzelm@10157
    42
  \parindent 0pt\parskip 0.7ex
wenzelm@10157
    43
  \pagestyle{myheadings}
wenzelm@10157
    44
  \renewcommand{\isamarkupheader}[1]{\markright{THEORY~``\isabellecontext''}\section{#1}}
wenzelm@10157
    45
  \input{session}
wenzelm@10157
    46
}
wenzelm@10157
    47
wenzelm@10157
    48
\nocite{Wenzel:1999:TPHOL}
wenzelm@10157
    49
\nocite{Wenzel:2000:isar-ref}
wenzelm@10157
    50
\nocite{Wenzel:2000:axclass}
wenzelm@10157
    51
\nocite{Bauer-Wenzel:2000:HB}
wenzelm@10157
    52
wenzelm@10157
    53
\bibliographystyle{abbrv}
wenzelm@10157
    54
\bibliography{root}
wenzelm@10157
    55
wenzelm@10157
    56
\end{document}