
diff -r d4c6e2bdde59 -r 33a6bdb62a18 doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Fri Sep 09 11:40:40 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Fri Sep 09 11:45:44 1994 +0200
@@ -414,10 +414,12 @@
         & intersection over a set\\
   \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
         & union over a set\\
-  \cdx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
+  \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
         &set of sets intersection \\
-  \cdx{Union} & $((\alpha\,set)set)\To\alpha\,set$
+  \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
         &set of sets union \\
+  \cdx{Pow}   & $\alpha\,set \To (\alpha\,set)set$
+        & powerset \\[1ex]
   \cdx{range}   & $(\alpha\To\beta )\To\beta\,set$
         & range of a function \\[1ex]
   \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
@@ -616,7 +618,8 @@
 \tdx{INTER1_def}        INTER1(B)   == INTER(\{x.True\}, B)
 \tdx{UNION1_def}        UNION1(B)   == UNION(\{x.True\}, B)
 \tdx{Inter_def}         Inter(S)    == (INT x:S. x)
-\tdx{Union_def}         Union(S)    ==  (UN x:S. x)
+\tdx{Union_def}         Union(S)    == (UN  x:S. x)
+\tdx{Pow_def}           Pow(A)      == \{B. B <= A\}
 \tdx{image_def}         f``A        == \{y. ? x:A. y=f(x)\}
 \tdx{range_def}         range(f)    == \{y. ? x. y=f(x)\}
 \tdx{mono_def}          mono(f)     == !A B. A <= B --> f(A) <= f(B)
@@ -698,6 +701,9 @@
 \tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter(C)
 \tdx{InterD}   [| A : Inter(C);  X:C |] ==> A:X
 \tdx{InterE}   [| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R
+
+\tdx{PowI}     A<=B ==> A: Pow(B)
+\tdx{PowD}     A: Pow(B) ==> A<=B
 \end{ttbox}
 \caption{Further derived rules for set theory} \label{hol-set2}
 \end{figure}
@@ -1344,7 +1350,7 @@
          ;
 typ      : typevarlist id
            | tid
-	 ;
+         ;
 typevarlist : () | tid | '(' (tid + ',') ')'
          ;
 \end{rail}
@@ -1528,8 +1534,174 @@
 because the simplifier will dispose of them automatically.
 
 \index{*datatype|)}
-\underscoreoff
+
+
+\section{Inductive and coinductive definitions}
+\index{*inductive|(}
+\index{*coinductive|(}
+
+An {\bf inductive definition} specifies the least set closed under given
+rules.  For example, a structural operational semantics is an inductive
+definition of an evaluation relation.  Dually, a {\bf coinductive
+  definition} specifies the greatest set closed under given rules.  An
+important example is using bisimulation relations to formalize equivalence
+of processes and infinite data structures.
+
+A theory file may contain any number of inductive and coinductive
+definitions.  They may be intermixed with other declarations; in
+particular, the (co)inductive sets {\bf must} be declared separately as
+constants, and may have mixfix syntax or be subject to syntax translations.
+
+Each (co)inductive definition adds definitions to the theory and also
+proves some theorems.  Each definition creates an ML structure, which is a
+substructure of the main theory structure.
+
+This package is derived from the ZF one, described in a
+separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
+  longer version is distributed with Isabelle.} which you should refer to
+in case of difficulties.  The package is simpler than ZF's, thanks to HOL's
+automatic type-checking.  The type of the (co)inductive determines the
+domain of the fixedpoint definition, and the package does not use inference
+rules for type-checking.
+
+
+\subsection{The result structure}
+Many of the result structure's components have been discussed in the paper;
+others are self-explanatory.
+\begin{description}
+\item[\tt thy] is the new theory containing the recursive sets.
+
+\item[\tt defs] is the list of definitions of the recursive sets.
+
+\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
+
+\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
+the recursive sets, in the case of mutual recursion).
+
+\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
+the recursive sets.  The rules are also available individually, using the
+names given them in the theory file. 
+
+\item[\tt elim] is the elimination rule.
+
+\item[\tt mk\_cases] is a function to create simplified instances of {\tt
+elim}, using freeness reasoning on some underlying datatype.
+\end{description}
+
+For an inductive definition, the result structure contains two induction rules,
+{\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it
+contains the rule \verb|coinduct|.
+
+Figure~\ref{def-result-fig} summarizes the two result signatures,
+specifying the types of all these components.
+
+\begin{figure}
+\begin{ttbox}
+sig
+val thy          : theory
+val defs         : thm list
+val mono         : thm
+val unfold       : thm
+val intrs        : thm list
+val elim         : thm
+val mk_cases     : thm list -> string -> thm
+{\it(Inductive definitions only)} 
+val induct       : thm
+val mutual_induct: thm
+{\it(Coinductive definitions only)}
+val coinduct    : thm
+end
+\end{ttbox}
+\hrule
+\caption{The result of a (co)inductive definition} \label{def-result-fig}
+\end{figure}
 
+\subsection{The syntax of a (co)inductive definition}
+An inductive definition has the form
+\begin{ttbox}
+inductive    {\it inductive sets}
+  intrs      {\it introduction rules}
+  monos      {\it monotonicity theorems}
+  con_defs   {\it constructor definitions}
+\end{ttbox}
+A coinductive definition is identical, except that it starts with the keyword
+{\tt coinductive}.  
+
+The {\tt monos} and {\tt con\_defs} sections are optional.  If present,
+each is specified as a string, which must be a valid ML expression of type
+{\tt thm list}.  It is simply inserted into the {\tt .thy.ML} file; if it
+is ill-formed, it will trigger ML error messages.  You can then inspect the
+file on your directory.
+
+\begin{itemize}
+\item The {\it inductive sets} are specified by one or more strings.
+
+\item The {\it introduction rules} specify one or more introduction rules in
+  the form {\it ident\/}~{\it string}, where the identifier gives the name of
+  the rule in the result structure.
+
+\item The {\it monotonicity theorems} are required for each operator
+  applied to a recursive set in the introduction rules.  There {\bf must}
+  be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
+  premise $t\in M(R_i)$ in an introduction rule!
+
+\item The {\it constructor definitions} contain definitions of constants
+  appearing in the introduction rules.  In most cases it can be omitted.
+\end{itemize}
+
+The package has a few notable restrictions:
+\begin{itemize}
+\item The theory must separately declare the recursive sets as
+  constants.
+
+\item The names of the recursive sets must be identifiers, not infix
+operators.  
+
+\item Side-conditions must not be conjunctions.  However, an introduction rule
+may contain any number of side-conditions.
+
+\item Side-conditions of the form $x=t$, where the variable~$x$ does not
+  occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
+\end{itemize}
+
+
+\subsection{Example of an inductive definition}
+Two declarations, included in a theory file, define the finite powerset
+operator.  First we declare the constant~{\tt Fin}.  Then we declare it
+inductively, with two introduction rules:
+\begin{ttbox}
+consts Fin :: "'a set => 'a set set"
+inductive "Fin(A)"
+  intrs
+    emptyI  "{} : Fin(A)"
+    insertI "[| a: A;  b: Fin(A) |] ==> insert(a,b) : Fin(A)"
+\end{ttbox}
+The resulting theory structure contains a substructure, called~{\tt Fin}.
+It contains the {\tt Fin}$(A)$ introduction rules as the list {\tt Fin.intrs},
+and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction
+rule is {\tt Fin.induct}.
+
+For another example, here is a theory file defining the accessible part of a
+relation.  The main thing to note is the use of~{\tt Pow} in the sole
+introduction rule, and the corresponding mention of the rule
+\verb|Pow_mono| in the {\tt monos} list.  The paper discusses a ZF version
+of this example in more detail.
+\begin{ttbox}
+Acc = WF + 
+consts pred :: "['b, ('a * 'b)set] => 'a set"   (*Set of predecessors*)
+       acc  :: "('a * 'a)set => 'a set"         (*Accessible part*)
+defs   pred_def  "pred(x,r) == {y. <y,x>:r}"
+inductive "acc(r)"
+  intrs
+     pred "pred(a,r): Pow(acc(r)) ==> a: acc(r)"
+  monos   "[Pow_mono]"
+end
+\end{ttbox}
+The HOL distribution contains many other inductive definitions, such as the
+theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The
+theory {\tt HOL/LList.thy} contains coinductive definitions.
+
+\index{*coinductive|)} \index{*inductive|)} \underscoreoff
 
 
 \section{The examples directories}
@@ -1538,49 +1710,52 @@
 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
 theory~\cite{mw81}. 
 
+Directory {\tt HOL/IMP} contains a mechanised version of a semantic
+equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the
+denotational and operational semantics of a simple while-language, then
+proves the two equivalent.  It contains several datatype and inductive
+definitions, and demonstrates their use.
+
 Directory {\tt HOL/ex} contains other examples and experimental proofs in
 {\HOL}.  Here is an overview of the more interesting files.
-\begin{ttdescription}
-\item[HOL/ex/cla.ML] demonstrates the classical reasoner on over sixty
+\begin{itemize}
+\item File {\tt 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[HOL/ex/meson.ML] contains an experimental implementation of the {\sc
+\item File {\tt 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[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof
+\item File {\tt mesontest.ML} contains test data for the {\sc meson} proof
   procedure.  These are mostly taken from Pelletier \cite{pelletier86}.
 
-\item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in
+\item File {\tt set.ML} proves Cantor's Theorem, which is presented in
   \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
 
-\item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
-  proofs about insertion sort and quick sort.
+\item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
+  insertion sort and quick sort.
 
-\item[HOL/ex/PropLog.ML] 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 {\tt 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[HOL/ex/Term.ML] 
-  contains proofs about an experimental recursive type definition;
+\item Theory {\tt Term} develops an experimental recursive type definition;
   the recursion goes through the type constructor~\tydx{list}.
 
-\item[HOL/ex/Simult.ML] defines primitives for solving mutually recursive
-  equations over sets.  It constructs sets of trees and forests as an
-  example, including induction and recursion rules that handle the mutual
-  recursion.
+\item Theory {\tt Simult} constructs mutually recursive sets of trees and
+  forests, including induction and recursion rules.
 
-\item[HOL/ex/MT.ML] contains Jacob Frost's formalization~\cite{frost93} of
+\item Theory {\tt 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{ttdescription}
+\end{itemize}
 
 
 \goodbreak




