| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Lattice/document/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle root.tex Sprache: Latech |
|||||||||
|
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc} \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} ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28