src/HOL/Lattice/document/root.tex
author paulson <lp15@cam.ac.uk>
Tue, 10 Nov 2015 14:18:41 +0000
changeset 61609 77b453bd616f
parent 58879 143c85e3cdb5
child 73404 299f6a8faccc
permissions -rw-r--r--
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
\usepackage[only,bigsqcap]{stmaryrd}

\urlstyle{rm}\isabellestyle{it}
\pagestyle{headings}

\hyphenation{Isabelle}
\hyphenation{Isar}


\begin{document}

\title{Lattices and Orders in Isabelle/HOL}
\author{Markus Wenzel \\ TU M\"unchen}
\maketitle

\begin{abstract}
  We consider abstract structures of orders and lattices.  Many fundamental
  concepts of lattice theory are developed, including dual structures,
  properties of bounds versus algebraic laws, lattice operations versus
  set-theoretic ones etc.  We also give example instantiations of lattices and
  orders, such as direct products and function spaces.  Well-known properties
  are demonstrated, like the Knaster-Tarski Theorem for complete lattices.
  
  This formal theory development may serve as an example of applying
  Isabelle/HOL to the domain of mathematical reasoning about ``axiomatic''
  structures.  Apart from the simply-typed classical set-theory of HOL, we
  employ Isabelle's system of axiomatic type classes for expressing structures
  and functors in a light-weight manner.  Proofs are expressed in the Isar
  language for readable formal proof, while aiming at its ``best-style'' of
  representing formal reasoning.
\end{abstract}

\tableofcontents

\newpage
{
  \parindent 0pt\parskip 0.7ex
  \pagestyle{myheadings}
  \renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
  \input{session}
}

\nocite{Wenzel:1999:TPHOL}
\nocite{Wenzel:2000:isar-ref}
\nocite{Wenzel:2000:axclass}
\nocite{Bauer-Wenzel:2000:HB}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}