--- 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