doc-src/HOL/HOL.tex

   intrs
     accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
 
 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
 it is so easily expressed:
 \[  \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.