\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}
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
