author lcp Mon, 25 Apr 1994 11:20:25 +0200 changeset 344 753b50b07c46 parent 343 8d77f767bd26 child 345 7007562172b1
final Springer copy
--- a/doc-src/Logics/Old_HOL.tex	Mon Apr 25 11:05:58 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Mon Apr 25 11:20:25 1994 +0200
@@ -4,7 +4,7 @@
\index{HOL system@{\sc hol} system}

The theory~\thydx{HOL} implements higher-order logic.
-It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is
+It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
based on Church's original paper~\cite{church40}.  Andrews's
book~\cite{andrews86} is a full description of higher-order logic.
Experience with the {\sc hol} system has demonstrated that higher-order
@@ -167,7 +167,8 @@
between the new type and the subset.  If type~$\sigma$ involves type
variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
-type.
+type.  Melham~\cite{melham89} discusses type definitions at length, with
+examples.

Isabelle does not support type definitions at present.  Instead, they are
mimicked by explicit definitions of isomorphism functions.  The definitions
@@ -237,21 +238,21 @@
\end{figure}

-\begin{figure}
+\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
\begin{ttbox}\makeatother
-\tdx{True_def}   True  = ((\%x.x)=(\%x.x))
-\tdx{All_def}    All   = (\%P. P = (\%x.True))
-\tdx{Ex_def}     Ex    = (\%P. P(@x.P(x)))
-\tdx{False_def}  False = (!P.P)
-\tdx{not_def}    not   = (\%P. P-->False)
-\tdx{and_def}    op &  = (\%P Q. !R. (P-->Q-->R) --> R)
-\tdx{or_def}     op |  = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
-\tdx{Ex1_def}    Ex1   = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
+\tdx{True_def}   True  == ((\%x.x)=(\%x.x))
+\tdx{All_def}    All   == (\%P. P = (\%x.True))
+\tdx{Ex_def}     Ex    == (\%P. P(@x.P(x)))
+\tdx{False_def}  False == (!P.P)
+\tdx{not_def}    not   == (\%P. P-->False)
+\tdx{and_def}    op &  == (\%P Q. !R. (P-->Q-->R) --> R)
+\tdx{or_def}     op |  == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
+\tdx{Ex1_def}    Ex1   == (\%P. ? x. P(x) & (! y. P(y) --> y=x))

-\tdx{Inv_def}    Inv   = (\%(f::'a=>'b) y. @x. f(x)=y)
-\tdx{o_def}      op o  = (\%(f::'b=>'c) g (x::'a). f(g(x)))
-\tdx{if_def}     if    = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
-\tdx{Let_def}    Let(s,f) = f(s)
+\tdx{Inv_def}    Inv   == (\%(f::'a=>'b) y. @x. f(x)=y)
+\tdx{o_def}      op o  == (\%(f::'b=>'c) g (x::'a). f(g(x)))
+\tdx{if_def}     if    == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
+\tdx{Let_def}    Let(s,f) == f(s)
\end{ttbox}
\caption{The {\tt HOL} definitions} \label{hol-defs}
\end{figure}
@@ -274,17 +275,17 @@

\HOL{} follows standard practice in higher-order logic: only a few
connectives are taken as primitive, with the remainder defined obscurely
-(Fig.\ts\ref{hol-defs}).  Unusually, the definitions are expressed using
-object-equality~({\tt=}) rather than meta-equality~({\tt==}).  This is
-possible because equality in higher-order logic may equate formulae and
-even functions over formulae.  On the other hand, meta-equality is
-Isabelle's usual symbol for making definitions.  Take care to note which
-form of equality is used before attempting a proof.
+(Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
+corresponding definitions \cite[page~270]{mgordon-hol} using
+object-equality~({\tt=}), which is possible because equality in
+higher-order logic may equate formulae and even functions over formulae.
+But theory~\HOL{}, like all other Isabelle theories, uses
+meta-equality~({\tt==}) for definitions.

-Some of the rules mention type variables; for example, {\tt refl} mentions
-the type variable~{\tt'a}.  This allows you to instantiate type variables
-explicitly by calling {\tt res_inst_tac}.  By default, explicit type
-variables have class \cldx{term}.
+Some of the rules mention type variables; for
+example, {\tt refl} mentions the type variable~{\tt'a}.  This allows you to
+instantiate type variables explicitly by calling {\tt res_inst_tac}.  By
+default, explicit type variables have class \cldx{term}.

Include type constraints whenever you state a polymorphic goal.  Type
inference may otherwise make the goal more polymorphic than you intended,
@@ -396,30 +397,6 @@
backward proofs, while \tdx{box_equals} supports reasoning by
simplifying both sides of an equation.

-See the files {\tt HOL/hol.thy} and
-{\tt HOL/hol.ML} for complete listings of the rules and
-derived rules.
-
-
-\section{Generic packages}
-\HOL\ instantiates most of Isabelle's generic packages;
-see {\tt HOL/ROOT.ML} for details.
-\begin{itemize}
-\item
-Because it includes a general substitution rule, \HOL\ instantiates the
-tactic {\tt hyp_subst_tac}, which substitutes for an equality
-throughout a subgoal and its hypotheses.
-\item
-It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
-simplification set for higher-order logic.  Equality~($=$), which also
-expresses logical equivalence, may be used for rewriting.  See the file
-{\tt HOL/simpdata.ML} for a complete listing of the simplification
-rules.
-\item
-It instantiates the classical reasoning module.  See~\S\ref{hol-cla-prover}
-for details.
-\end{itemize}
-

\begin{figure}
\begin{center}
@@ -835,7 +812,7 @@
\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
strictly necessary but yield more natural proofs.  Similarly,
\tdx{equalityCE} supports classical reasoning about extensionality,
-after the fashion of \tdx{iffCE}.  See the file {\tt HOL/set.ML} for
+after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
proofs pertaining to set theory.

Figure~\ref{hol-fun} presents derived inference rules involving functions.
@@ -860,6 +837,7 @@

\begin{figure}
\begin{constants}
+  \it symbol    & \it meta-type &           & \it description \\
\cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
& & ordered pairs $\langle a,b\rangle$ \\
\cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
@@ -895,6 +873,7 @@

\begin{figure}
\begin{constants}
+  \it symbol    & \it meta-type &           & \it description \\
\cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
\cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
\cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
@@ -920,6 +899,65 @@
\end{figure}

+\section{Generic packages and classical reasoning}
+\HOL\ instantiates most of Isabelle's generic packages;
+see {\tt HOL/ROOT.ML} for details.
+\begin{itemize}
+\item
+Because it includes a general substitution rule, \HOL\ instantiates the
+tactic {\tt hyp_subst_tac}, which substitutes for an equality
+throughout a subgoal and its hypotheses.
+\item
+It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
+simplification set for higher-order logic.  Equality~($=$), which also
+expresses logical equivalence, may be used for rewriting.  See the file
+{\tt HOL/simpdata.ML} for a complete listing of the simplification
+rules.
+\item
+It instantiates the classical reasoner, as described below.
+\end{itemize}
+\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
+well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
+rule; recall Fig.\ts\ref{hol-lemmas2} above.
+
+The classical reasoner is set up as the structure
+{\tt Classical}.  This structure is open, so {\ML} identifiers such
+as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
+\HOL\ defines the following classical rule sets:
+\begin{ttbox}
+prop_cs    : claset
+HOL_cs     : claset
+HOL_dup_cs : claset
+set_cs     : claset
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
+those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
+along with the rule~{\tt refl}.
+
+\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
+  {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
+  and~{\tt exI}, as well as rules for unique existence.  Search using
+  this classical set is incomplete: quantified formulae are used at most
+  once.
+
+\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
+  {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
+  and~\tdx{exCI}, as well as rules for unique existence.  Search using
+  this is complete --- quantified formulae may be duplicated --- but
+  frequently fails to terminate.  It is generally unsuitable for
+  depth-first search.
+
+\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
+  quantifiers, subsets, comprehensions, unions and intersections,
+  complements, finite sets, images and ranges.
+\end{ttdescription}
+\noindent
+See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+        {Chap.\ts\ref{chap:classical}}
+for more discussion of classical proof methods.
+
+
\section{Types}
The basic higher-order logic is augmented with a tremendous amount of
material, including support for recursive function and type definitions.  A
@@ -938,14 +976,13 @@

Most of the definitions are suppressed, but observe that the projections
and conditionals are defined as descriptions.  Their properties are easily
-proved using \tdx{select_equality}.  See {\tt HOL/prod.thy} and
-{\tt HOL/sum.thy} for details.
+proved using \tdx{select_equality}.

\begin{figure}
\index{*"< symbol}
\index{*"* symbol}
-\index{/@{\tt/} symbol}
-\index{//@{\tt//} symbol}
+\index{*div symbol}
+\index{*mod symbol}
\index{*"+ symbol}
\index{*"- symbol}
\begin{constants}
@@ -958,8 +995,8 @@
& & primitive recursor\\
\cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
\tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\
-  \tt /         & $[nat,nat]\To nat$    &  Left 70      & division\\
-  \tt //        & $[nat,nat]\To nat$    &  Left 70      & modulus\\
+  \tt div       & $[nat,nat]\To nat$    &  Left 70      & division\\
+  \tt mod       & $[nat,nat]\To nat$    &  Left 70      & modulus\\
\tt +         & $[nat,nat]\To nat$    &  Left 65      & addition\\
\tt -         & $[nat,nat]\To nat$    &  Left 65      & subtraction
\end{constants}
@@ -967,17 +1004,17 @@

\begin{ttbox}\makeatother
\tdx{nat_case_def}  nat_case == (\%n a f. @z. (n=0 --> z=a) &
-                                        (!x. n=Suc(x) --> z=f(x)))
+                                       (!x. n=Suc(x) --> z=f(x)))
\tdx{pred_nat_def}  pred_nat == \{p. ? n. p = <n, Suc(n)>\}
\tdx{less_def}      m<n      == <m,n>:pred_nat^+
\tdx{nat_rec_def}   nat_rec(n,c,d) ==
wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))

-\tdx{add_def}   m+n  == nat_rec(m, n, \%u v.Suc(v))
-\tdx{diff_def}  m-n  == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
-\tdx{mult_def}  m*n  == nat_rec(m, 0, \%u v. n + v)
-\tdx{mod_def}   m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
-\tdx{quo_def}   m/n  == wfrec(trancl(pred_nat),
+\tdx{add_def}   m+n     == nat_rec(m, n, \%u v.Suc(v))
+\tdx{diff_def}  m-n     == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
+\tdx{mult_def}  m*n     == nat_rec(m, 0, \%u v. n + v)
+\tdx{mod_def}   m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
+\tdx{quo_def}   m div n == wfrec(trancl(pred_nat),
m, \%j f. if(j<n,0,Suc(f(j-n))))
\subcaption{Definitions}
\end{ttbox}
@@ -1020,7 +1057,7 @@
\tdx{less_linear}    m<n | m=n | n<m
\subcaption{The less-than relation}
\end{ttbox}
-\caption{Derived rules for~$nat$} \label{hol-nat2}
+\caption{Derived rules for {\tt nat}} \label{hol-nat2}
\end{figure}

@@ -1030,7 +1067,7 @@
individuals, which is non-empty and closed under an injective operation.
The natural numbers are inductively generated by choosing an arbitrary
individual for~0 and using the injective operation to take successors.  As
-usual, the isomorphisms between~$nat$ and its representation are made
+usual, the isomorphisms between~\tydx{nat} and its representation are made
explicitly.

The definition makes use of a least fixed point operator \cdx{lfp},
@@ -1077,7 +1114,7 @@
\cdx{Nil}     & $\alpha list$ & & empty list\\
\tt \#   & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
list constructor \\
-  \cdx{null}    & $\alpha list \To bool$ & & emptyness test\\
+  \cdx{null}    & $\alpha list \To bool$ & & emptiness test\\
\cdx{hd}      & $\alpha list \To \alpha$ & & head \\
\cdx{tl}      & $\alpha list \To \alpha list$ & & tail \\
\cdx{ttl}     & $\alpha list \To \alpha list$ & & total tail \\
@@ -1101,7 +1138,7 @@
\sdx{[]}            & Nil           & \rm empty list \\{}
[$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &
\rm finite list \\{}
-  [$x$:$l$. $P[x]$]  & filter($\lambda x.P[x]$, $l$) &
+  [$x$:$l$. $P$]  & filter($\lambda x{.}P$, $l$) &
\rm list comprehension
\end{tabular}
\end{center}
@@ -1160,17 +1197,16 @@
handling recursive data types.  Figure~\ref{hol-list} presents the theory
\thydx{List}: the basic list operations with their types and properties.

-The \sdx{case} construct is defined by the following translation
-(omitted from the figure due to lack of space):
+The \sdx{case} construct is defined by the following translation:
{\dquotes
\begin{eqnarray*}
-  \begin{array}[t]{r@{\;}l@{}l}
+  \begin{array}{r@{\;}l@{}l}
"case " e " of" & "[]"    & " => " a\\
"|" & x"\#"xs & " => " b
\end{array}
& \equiv &
-  "list_case"(e, a, \lambda x\;xs.b[x,xs])
-\end{eqnarray*}}
+  "list_case"(e, a, \lambda x\;xs.b)
+\end{eqnarray*}}%
The theory includes \cdx{list_rec}, a primitive recursion operator
for lists.  It is derived from well-founded recursion, a general principle
that can express arbitrary total recursive functions.
@@ -1186,71 +1222,30 @@
\index{*llist type}

The definition of lazy lists demonstrates methods for handling infinite
-data structures and coinduction in higher-order logic.  It defines an
-operator for corecursion on lazy lists, which is used to define a few
-simple functions such as map and append.  Corecursion cannot easily define
-operations such as filter, which can compute indefinitely before yielding
-the next element (if any!) of the lazy list.  A coinduction principle is
-defined for proving equations on lazy lists.  See the files {\tt
-  HOL/llist.thy} and {\tt HOL/llist.ML} for the formal derivations.
+data structures and coinduction in higher-order logic.  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.  Corecursion
+cannot easily define operations such as filter, which can compute
+indefinitely before yielding the next element (if any!) of the lazy list.
+A coinduction principle is defined for proving equations on lazy lists.

I have written a paper discussing the treatment of lazy lists; it also
covers finite lists~\cite{paulson-coind}.

-\section{Classical proof procedures} \label{hol-cla-prover}
-\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
-well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
-rule; recall Fig.\ts\ref{hol-lemmas2} above.
-
-The classical reasoner is set up for \HOL, as the structure
-{\tt Classical}.  This structure is open, so {\ML} identifiers such
-as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
-
-\HOL\ defines the following classical rule sets:
-\begin{ttbox}
-prop_cs    : claset
-HOL_cs     : claset
-HOL_dup_cs : claset
-set_cs     : claset
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
-those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
-along with the rule~{\tt refl}.
-
-\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
-  {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
-  and~{\tt exI}, as well as rules for unique existence.  Search using
-  this classical set is incomplete: quantified formulae are used at most
-  once.
-
-\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
-  {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
-  and~\tdx{exCI}, as well as rules for unique existence.  Search using
-  this is complete --- quantified formulae may be duplicated --- but
-  frequently fails to terminate.  It is generally unsuitable for
-  depth-first search.
-
-\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
-  quantifiers, subsets, comprehensions, unions and intersections,
-  complements, finite sets, images and ranges.
-\end{ttdescription}
-\noindent
-See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
-        {Chap.\ts\ref{chap:classical}}
-for more discussion of classical proof methods.
-
-
\section{The examples directories}
-Directory {\tt HOL/Subst} contains Martin Coen's mechanization of a theory of
+Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
substitutions and unifiers.  It is based on Paulson's previous
-mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's
+mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
theory~\cite{mw81}.

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
+  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
meson} proof procedure, inspired by Plaisted~\cite{plaisted90}.  It is
much more powerful than Isabelle's classical reasoner.  But it is less
@@ -1263,24 +1258,25 @@
\item[HOL/ex/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
+\item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
proofs about insertion sort and quick sort.

-\item[HOL/ex/pl.ML] proves the soundness and completeness of classical
+\item[HOL/ex/PL.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.
+  theorems defined inductively.  A similar proof in \ZF{} is described
+  elsewhere~\cite{paulson-set-II}.

-\item[HOL/ex/term.ML]
+\item[HOL/ex/Term.ML]
contains proofs about 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
+\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[HOL/ex/mt.ML] contains Jacob Frost's formalization~\cite{frost93} of
+\item[HOL/ex/MT.ML] 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
@@ -1288,120 +1284,7 @@
\end{ttdescription}

-\section{Example: deriving the conjunction rules}
-The theory {\HOL} comes with a body of derived rules, ranging from simple
-properties of the logical constants and set theory to well-founded
-recursion.  Many of them are worth studying.
-
-Deriving natural deduction rules for the logical constants from their
-definitions is an archetypal example of higher-order reasoning.  Let us
-verify two conjunction rules:
-$\infer[({\conj}I)]{P\conj Q}{P & Q} \qquad\qquad - \infer[({\conj}E1)]{P}{P\conj Q} -$
-
-\subsection{The introduction rule}
-We begin by stating the rule as the goal.  The list of premises $[P,Q]$ is
-bound to the {\ML} variable~{\tt prems}.
-\begin{ttbox}
-val prems = goal HOL.thy "[| P; Q |] ==> P&Q";
-{\out Level 0}
-{\out P & Q}
-{\out  1. P & Q}
-{\out val prems = ["P [P]",  "Q [Q]"] : thm list}
-\end{ttbox}
-The next step is to unfold the definition of conjunction.  But
-\tdx{and_def} uses \HOL's internal equality, so
-\ttindex{rewrite_goals_tac} is unsuitable.
-Instead, we perform substitution using the rule \tdx{ssubst}:
-\begin{ttbox}
-by (resolve_tac [and_def RS ssubst] 1);
-{\out Level 1}
-{\out P & Q}
-{\out  1. ! R. (P --> Q --> R) --> R}
-\end{ttbox}
-We now apply $(\forall I)$ and $({\imp}I)$:
-\begin{ttbox}
-by (resolve_tac [allI] 1);
-{\out Level 2}
-{\out P & Q}
-{\out  1. !!R. (P --> Q --> R) --> R}
-\ttbreak
-by (resolve_tac [impI] 1);
-{\out Level 3}
-{\out P & Q}
-{\out  1. !!R. P --> Q --> R ==> R}
-\end{ttbox}
-The assumption is a nested implication, which may be eliminated
-using~\tdx{mp} resolved with itself.  Elim-resolution, here, performs
-backwards chaining.  More straightforward would be to use~\tdx{impE}
-twice.
-\index{*RS}
-\begin{ttbox}
-by (eresolve_tac [mp RS mp] 1);
-{\out Level 4}
-{\out P & Q}
-{\out  1. !!R. P}
-{\out  2. !!R. Q}
-\end{ttbox}
-These two subgoals are simply the premises:
-\begin{ttbox}
-by (REPEAT (resolve_tac prems 1));
-{\out Level 5}
-{\out P & Q}
-{\out No subgoals!}
-\end{ttbox}
-
-
-\subsection{The elimination rule}
-Again, we bind the list of premises (in this case $[P\conj Q]$)
-to~{\tt prems}.
-\begin{ttbox}
-val prems = goal HOL.thy "[| P & Q |] ==> P";
-{\out Level 0}
-{\out P}
-{\out  1. P}
-{\out val prems = ["P & Q  [P & Q]"] : thm list}
-\end{ttbox}
-Working with premises that involve defined constants can be tricky.  We
-must expand the definition of conjunction in the meta-assumption $P\conj -Q$.  The rule \tdx{subst} performs substitution in forward proofs.
-We get {\it two\/} resolvents since the vacuous substitution is valid:
-\begin{ttbox}
-prems RL [and_def RS subst];
-{\out val it = ["! R. (P --> Q --> R) --> R  [P & Q]",}
-{\out           "P & Q  [P & Q]"] : thm list}
-\end{ttbox}
-By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of
-the vacuous one and put the other into a convenient form:\footnote {Why use
-  {\tt [spec] RL [mp]} instead of {\tt [spec RS mp]} to join the rules?  In
-  higher-order logic, {\tt spec RS mp} fails because the resolution yields
-  two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall - x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$.  In first-order logic, the
-  resolution yields only the latter result because $\forall x.x$ is not a
-  first-order formula; in fact, it is equivalent to falsity.} \index{*RL}
-\begin{ttbox}
-prems RL [and_def RS subst] RL [spec] RL [mp];
-{\out val it = ["P --> Q --> ?Q ==> ?Q  [P & Q]"] : thm list}
-\end{ttbox}
-This is a list containing a single rule, which is directly applicable to
-our goal:
-\begin{ttbox}
-by (resolve_tac it 1);
-{\out Level 1}
-{\out P}
-{\out  1. P --> Q --> P}
-\end{ttbox}
-The subgoal is a trivial implication.  Recall that \ttindex{ares_tac} is a
-combination of {\tt assume_tac} and {\tt resolve_tac}.
-\begin{ttbox}
-by (REPEAT (ares_tac [impI] 1));
-{\out Level 2}
-{\out P}
-{\out No subgoals!}
-\end{ttbox}
-
-
+\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
@@ -1412,9 +1295,10 @@
%
Viewing types as sets, $\alpha\To bool$ represents the powerset
of~$\alpha$.  This version states that for every function from $\alpha$ to
-its powerset, some subset is outside its range.  The Isabelle proof uses
-\HOL's set theory, with the type $\alpha\,set$ and the operator
-\cdx{range}.  The set~$S$ is given as an unknown instead of a
+its powerset, some subset is outside its range.
+
+The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
+the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
quantified variable so that we may inspect the subset found by the proof.
\begin{ttbox}
goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
@@ -1457,8 +1341,8 @@
{\out  2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
\end{ttbox}
Forcing a contradiction between the two assumptions of subgoal~1 completes
-the instantiation of~$S$.  It is now the set $\{x. x\not\in f(x)\}$, the
-standard diagonal construction.
+the instantiation of~$S$.  It is now the set $\{x. x\not\in f(x)\}$, which
+is the standard diagonal construction.
\begin{ttbox}
by (contr_tac 1);
{\out Level 5}