# HG changeset patch # User wenzelm # Date 1304456485 -7200 # Node ID 43766deefc16ae0db5e05261aaa10a4db3f9e84e # Parent d34154b085797bb86f841eb6c1c0629143f215e4 removed odd historical material; diff -r d34154b08579 -r 43766deefc16 doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Tue May 03 22:28:19 2011 +0200 +++ b/doc-src/HOL/HOL.tex Tue May 03 23:01:25 2011 +0200 @@ -2718,124 +2718,11 @@ end \end{ttbox} -The Isabelle distribution contains many other inductive definitions. Simple -examples are collected on subdirectory \texttt{HOL/Induct}. The theory -\texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples -may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP}, -\texttt{Lambda} and \texttt{Auth}. +The Isabelle distribution contains many other inductive definitions. \index{*coinductive|)} \index{*inductive|)} -\section{The examples directories} - -Directory \texttt{HOL/Auth} contains theories for proving the correctness of -cryptographic protocols~\cite{paulson-jcs}. The approach is based upon -operational semantics rather than the more usual belief logics. On the same -directory are proofs for some standard examples, such as the Needham-Schroeder -public-key authentication protocol and the Otway-Rees -protocol. - -Directory \texttt{HOL/IMP} contains a formalization of various denotational, -operational and axiomatic semantics of a simple while-language, the necessary -equivalence proofs, soundness and completeness of the Hoare rules with -respect to the denotational semantics, and soundness and completeness of a -verification condition generator. Much of development is taken from -Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}. - -Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare -logic, including a tactic for generating verification-conditions. - -Directory \texttt{HOL/MiniML} contains a formalization of the type system of -the core functional language Mini-ML and a correctness proof for its type -inference algorithm $\cal W$~\cite{milner78,nipkow-W}. - -Directory \texttt{HOL/Lambda} contains a formalization of untyped -$\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$ -and $\eta$ reduction~\cite{Nipkow-CR}. - -Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory -of substitutions and unifiers. It is based on Paulson's previous -mechanisation in LCF~\cite{paulson85} of Manna and Waldinger's -theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef}, -with nested recursion. - -Directory \texttt{HOL/Induct} presents simple examples of (co)inductive -definitions and datatypes. -\begin{itemize} -\item Theory \texttt{PropLog} proves the soundness and completeness of - classical propositional logic, given a truth table semantics. The only - connective is $\imp$. A Hilbert-style axiom system is specified, and its - set of theorems defined inductively. A similar proof in ZF is described - elsewhere~\cite{paulson-set-II}. - -\item Theory \texttt{Term} defines the datatype \texttt{term}. - -\item Theory \texttt{ABexp} defines arithmetic and boolean expressions - as mutually recursive datatypes. - -\item The definition of lazy lists demonstrates methods for handling - infinite data structures and coinduction in higher-order - logic~\cite{paulson-coind}.% -\footnote{To be precise, these lists are \emph{potentially infinite} rather - than lazy. Lazy implies a particular operational semantics.} - Theory \thydx{LList} defines an operator for - corecursion on lazy lists, which is used to define a few simple functions - such as map and append. A coinduction principle is defined - for proving equations on lazy lists. - -\item Theory \thydx{LFilter} defines the filter functional for lazy lists. - This functional is notoriously difficult to define because finding the next - element meeting the predicate requires possibly unlimited search. It is not - computable, but can be expressed using a combination of induction and - corecursion. - -\item Theory \thydx{Exp} illustrates the use of iterated inductive definitions - to express a programming language semantics that appears to require mutual - induction. Iterated induction allows greater modularity. -\end{itemize} - -Directory \texttt{HOL/ex} contains other examples and experimental proofs in -HOL. -\begin{itemize} -\item Theory \texttt{Recdef} presents many examples of using \texttt{recdef} - to define recursive functions. Another example is \texttt{Fib}, which - defines the Fibonacci function. - -\item Theory \texttt{Primes} defines the Greatest Common Divisor of two - natural numbers and proves a key lemma of the Fundamental Theorem of - Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$ - or $p$ divides~$n$. - -\item Theory \texttt{Primrec} develops some computation theory. It - inductively defines the set of primitive recursive functions and presents a - proof that Ackermann's function is not primitive recursive. - -\item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty - predicate calculus theorems, ranging from simple tautologies to - moderately difficult problems involving equality and quantifiers. - -\item File \texttt{meson.ML} contains an experimental implementation of the {\sc - meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is - much more powerful than Isabelle's classical reasoner. But it is less - useful in practice because it works only for pure logic; it does not - accept derived rules for the set theory primitives, for example. - -\item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof - procedure. These are mostly taken from Pelletier \cite{pelletier86}. - -\item File \texttt{set.ML} proves Cantor's Theorem, which is presented in - {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem. - -\item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of - Milner and Tofte's coinduction example~\cite{milner-coind}. This - substantial proof concerns the soundness of a type system for a simple - functional language. The semantics of recursion is given by a cyclic - environment, which makes a coinductive argument appropriate. -\end{itemize} - - -\goodbreak \section{Example: Cantor's Theorem}\label{sec:hol-cantor} Cantor's Theorem states that every set has more subsets than it has elements. It has become a favourite example in higher-order logic since