wneuper/isa: comparison doc-src/HOL/HOL.tex

equal deleted inserted replaced

-:13f3aaf12be2
+:ec7d7f877712
 \index{higher-order logic|(}
 \index{HOL system@{\sc hol} system}
 The theory~\thydx{HOL} implements higher-order logic.  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
+Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a
-book~\cite{andrews86} is a full description of the original
+full description of the original Church-style higher-order logic.  Experience
-Church-style higher-order logic.  Experience with the {\sc hol} system
+with the {\sc hol} system has demonstrated that higher-order logic is widely
-has demonstrated that higher-order logic is widely applicable in many
+applicable in many areas of mathematics and computer science, not just
-areas of mathematics and computer science, not just hardware
+hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It
-verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It is
+is weaker than ZF set theory but for most applications this does not matter.
-weaker than {\ZF} set theory but for most applications this does not
+If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
-matter.  If you prefer {\ML} to Lisp, you will probably prefer \HOL\
-to~{\ZF}.
+The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different
+syntax.  Ancient releases of Isabelle included still another version of~HOL,
-The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
+with explicit type inference rules~\cite{paulson-COLOG}.  This version no
-different syntax.  Ancient releases of Isabelle included still another version
+longer exists, but \thydx{ZF} supports a similar style of reasoning.}
-of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}.  This
+follows $\lambda$-calculus and functional programming.  Function application
-version no longer exists, but \thydx{ZF} supports a similar style of
+is curried.  To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to
-reasoning.} follows $\lambda$-calculus and functional programming.  Function
+the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$.  There is no
-application is curried.  To apply the function~$f$ of type
+`apply' operator as in \thydx{ZF}.  Note that $f(a,b)$ means ``$f$ applied to
-$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
+the pair $(a,b)$'' in HOL.  We write ordered pairs as $(a,b)$, not $\langle
-write $f\,a\,b$.  There is no `apply' operator as in \thydx{ZF}.  Note that
+a,b\rangle$ as in ZF.
-$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL.  We write ordered
-pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
+HOL has a distinct feel, compared with ZF and CTT.  It identifies object-level
+types with meta-level types, taking advantage of Isabelle's built-in
-\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
+type-checker.  It identifies object-level functions with meta-level functions,
-identifies object-level types with meta-level types, taking advantage of
+so it uses Isabelle's operations for abstraction and application.
-Isabelle's built-in type-checker.  It identifies object-level functions
-with meta-level functions, so it uses Isabelle's operations for abstraction
+These identifications allow Isabelle to support HOL particularly nicely, but
-and application.
+they also mean that HOL requires more sophistication from the user --- in
+particular, an understanding of Isabelle's type system.  Beginners should work
-These identifications allow Isabelle to support \HOL\ particularly
+with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.
-nicely, but they also mean that \HOL\ requires more sophistication
-from the user --- in particular, an understanding of Isabelle's type
-system.  Beginners should work with \texttt{show_types} (or even
-\texttt{show_sorts}) set to \texttt{true}.
-%  Gain experience by
-%working in first-order logic before attempting to use higher-order logic.
-%This chapter assumes familiarity with~{\FOL{}}.
 \begin{figure}
 \begin{constants}
 \it name      &\it meta-type  & \it description \\
 & | & "?~~~" id~id^* " . " formula \\
 & | & "EX!~" id~id^* " . " formula
 & | & "?!~~" id~id^* " . " formula \\
 \end{array}
 \]
-\caption{Full grammar for \HOL} \label{hol-grammar}
+\caption{Full grammar for HOL} \label{hol-grammar}
 \end{figure}
 \section{Syntax}
 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
 higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
 $\lnot(a=b)$.
 \begin{warn}
-\HOL\ has no if-and-only-if connective; logical equivalence is expressed
+HOL has no if-and-only-if connective; logical equivalence is expressed using
-using equality.  But equality has a high priority, as befitting a
+equality.  But equality has a high priority, as befitting a relation, while
-relation, while if-and-only-if typically has the lowest priority.  Thus,
+if-and-only-if typically has the lowest priority.  Thus, $\lnot\lnot P=P$
-$\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.
+abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.  When using $=$
-When using $=$ to mean logical equivalence, enclose both operands in
+to mean logical equivalence, enclose both operands in parentheses.
-parentheses.
 \end{warn}
 \subsection{Types and overloading}
 The universal type class of higher-order terms is called~\cldx{term}.
 By default, explicit type variables have class \cldx{term}.  In
 function types, is overloaded with arity {\tt(term,\thinspace
 term)\thinspace term}.  Thus, $\sigma\To\tau$ belongs to class~{\tt
 term} if $\sigma$ and~$\tau$ do, allowing quantification over
 functions.
-\HOL\ allows new types to be declared as subsets of existing types;
+HOL allows new types to be declared as subsets of existing types;
 see~{\S}\ref{sec:HOL:Types}.  ML-like datatypes can also be declared; see
 ~{\S}\ref{sec:HOL:datatype}.
 Several syntactic type classes --- \cldx{plus}, \cldx{minus},
 \cldx{times} and
 \end{warn}
 \subsection{Binders}
-Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
+Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$
-some~$x$ satisfying~$P$, if such exists.  Since all terms in \HOL\
+satisfying~$P$, if such exists.  Since all terms in HOL denote something, a
-denote something, a description is always meaningful, but we do not
+description is always meaningful, but we do not know its value unless $P$
-know its value unless $P$ defines it uniquely.  We may write
+defines it uniquely.  We may write descriptions as \cdx{Eps}($\lambda x.
-descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
+P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.
-\hbox{\tt SOME~$x$.~$P[x]$}.
 Existential quantification is defined by
 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
 The unique existence quantifier, $\exists!x. P$, is defined in terms
 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
 Local abbreviations can be introduced by a \texttt{let} construct whose
 syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into
 the constant~\cdx{Let}.  It can be expanded by rewriting with its
 definition, \tdx{Let_def}.
-\HOL\ also defines the basic syntax
+HOL also defines the basic syntax
 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
 as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}
 and \sdx{of} are reserved words.  Initially, this is mere syntax and has no
 logical meaning.  By declaring translations, you can cause instances of the
 \texttt{case} construct to denote applications of particular case operators.
 \tdx{True_or_False} (P=True) | (P=False)
 \end{ttbox}
 \caption{The \texttt{HOL} rules} \label{hol-rules}
 \end{figure}
-Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
+Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
-with their~{\ML} names.  Some of the rules deserve additional
+their~{\ML} names.  Some of the rules deserve additional comments:
-comments:
 \begin{ttdescription}
 \item[\tdx{ext}] expresses extensionality of functions.
 \item[\tdx{iff}] asserts that logically equivalent formulae are
 equal.
 \item[\tdx{selectI}] gives the defining property of the Hilbert
 \end{ttbox}
 \caption{The \texttt{HOL} definitions} \label{hol-defs}
 \end{figure}
-\HOL{} follows standard practice in higher-order logic: only a few
+HOL follows standard practice in higher-order logic: only a few connectives
-connectives are taken as primitive, with the remainder defined obscurely
+are taken as primitive, with the remainder defined obscurely
 (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
+object-equality~({\tt=}), which is possible because equality in higher-order
-higher-order logic may equate formulae and even functions over formulae.
+logic may equate formulae and even functions over formulae.  But theory~HOL,
-But theory~\HOL{}, like all other Isabelle theories, uses
+like all other Isabelle theories, uses meta-equality~({\tt==}) for
-meta-equality~({\tt==}) for definitions.
+definitions.
 \begin{warn}
 The definitions above should never be expanded and are shown for completeness
 only.  Instead users should reason in terms of the derived rules shown below
 or, better still, using high-level tactics
 (see~{\S}\ref{sec:HOL:generic-packages}).
 %\tdx{eqTrueI}     P ==> P=True
 %\tdx{eqTrueE}     P=True ==> P
 \subcaption{Logical equivalence}
 \end{ttbox}
-\caption{Derived rules for \HOL} \label{hol-lemmas1}
+\caption{Derived rules for HOL} \label{hol-lemmas1}
 \end{figure}
 \begin{figure}
 \begin{ttbox}\makeatother
 \section{A formulation of set theory}
 Historically, higher-order logic gives a foundation for Russell and
 Whitehead's theory of classes.  Let us use modern terminology and call them
-{\bf sets}, but note that these sets are distinct from those of {\ZF} set
+{\bf sets}, but note that these sets are distinct from those of ZF set theory,
-theory, and behave more like {\ZF} classes.
+and behave more like ZF classes.
 \begin{itemize}
 \item
 Sets are given by predicates over some type~$\sigma$.  Types serve to
 define universes for sets, but type-checking is still significant.
 \item
 may be defined by absolute comprehension.
 \item
 Although sets may contain other sets as elements, the containing set must
 have a more complex type.
 \end{itemize}
-Finite unions and intersections have the same behaviour in \HOL\ as they
+Finite unions and intersections have the same behaviour in HOL as they do
-do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
+in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
-denoting the universal set for the given type.
+universal set for the given type.
 \subsection{Syntax of set theory}\index{*set type}
-\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
+HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially
-essentially the same as $\alpha\To bool$.  The new type is defined for
+the same as $\alpha\To bool$.  The new type is defined for clarity and to
-clarity and to avoid complications involving function types in unification.
+avoid complications involving function types in unification.  The isomorphisms
-The isomorphisms between the two types are declared explicitly.  They are
+between the two types are declared explicitly.  They are very natural:
-very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
+\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
-\hbox{\tt op :} maps in the other direction (ignoring argument order).
+maps in the other direction (ignoring argument order).
 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
 translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
 constructs.  Infix operators include union and intersection ($A\un B$
 and $A\int B$), the subset and membership relations, and the image
 \begin{eqnarray*}
 \{a, b, c\} & \equiv &
 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
 \end{eqnarray*}
-The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
+The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of
-that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
+suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain
-occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
+free occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.
-x. P[x])$.  It defines sets by absolute comprehension, which is impossible
+P[x])$.  It defines sets by absolute comprehension, which is impossible in~ZF;
-in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
+the type of~$x$ implicitly restricts the comprehension.
 The set theory defines two {\bf bounded quantifiers}:
 \begin{eqnarray*}
 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
 \caption{Set equalities} \label{hol-equalities}
 \end{figure}
 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
-obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
+obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
-such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
+as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
-are designed for classical reasoning; the rules \tdx{subsetD},
+reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
-\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
+not strictly necessary but yield more natural proofs.  Similarly,
-strictly necessary but yield more natural proofs.  Similarly,
+\tdx{equalityCE} supports classical reasoning about extensionality, after the
-\tdx{equalityCE} supports classical reasoning about extensionality,
+fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs
-after the fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for
+pertaining to set theory.
-proofs pertaining to set theory.
 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
 Unions form least upper bounds; non-empty intersections form greatest lower
 bounds.  Reasoning directly about subsets often yields clearer proofs than
 reasoning about the membership relation.  See the file \texttt{HOL/subset.ML}.
 \section{Generic packages}
 \label{sec:HOL:generic-packages}
-\HOL\ instantiates most of Isabelle's generic packages, making available the
+HOL instantiates most of Isabelle's generic packages, making available the
 simplifier and the classical reasoner.
 \subsection{Simplification and substitution}
 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
 If $thm$ is a conditional equality, the instantiated condition becomes an
 additional (first) subgoal.
 \end{ttdescription}
-\HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
+HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
-for an equality throughout a subgoal and its hypotheses.  This tactic uses
+equality throughout a subgoal and its hypotheses.  This tactic uses HOL's
-\HOL's general substitution rule.
+general substitution rule.
 \subsubsection{Case splitting}
 \label{subsec:HOL:case:splitting}
-\HOL{} also provides convenient means for case splitting during
+HOL also provides convenient means for case splitting during rewriting. Goals
-rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
+containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
-then\dots else\dots} often require a case distinction on $b$. This is
+often require a case distinction on $b$. This is expressed by the theorem
-expressed by the theorem \tdx{split_if}:
+\tdx{split_if}:
 $$
 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
 \eqno{(*)}
 $$
 \end{ttbox}
 for adding splitting rules to, and deleting them from the current simpset.
 \subsection{Classical reasoning}
-\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
+HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
-well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
+classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
-rule; recall Fig.\ts\ref{hol-lemmas2} above.
+Fig.\ts\ref{hol-lemmas2} above.
 The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and
 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
 for most purposes.  Named clasets include \ttindexbold{prop_cs}, which
 includes the propositional rules, and \ttindexbold{HOL_cs}, which also
 \section{Types}\label{sec:HOL:Types}
-This section describes \HOL's basic predefined types ($\alpha \times
+This section describes HOL's basic predefined types ($\alpha \times \beta$,
-\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
+$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new
-introducing new types in general.  The most important type
+types in general.  The most important type construction, the
-construction, the \texttt{datatype}, is treated separately in
+\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.
-{\S}\ref{sec:HOL:datatype}.
 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
 \label{subsec:prod-sum}
 \end{ttbox}
 \subsection{Numerical types and numerical reasoning}
-The integers (type \tdx{int}) are also available in \HOL, and the reals (type
+The integers (type \tdx{int}) are also available in HOL, and the reals (type
 \tdx{real}) are available in the logic image \texttt{HOL-Real}.  They support
 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
 multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the
 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real
 division and other operations.  Both types belong to class \cldx{linorder}, so
 \index{list@{\textit{list}} type|)}
 \subsection{Introducing new types} \label{sec:typedef}
-The \HOL-methodology dictates that all extensions to a theory should
+The HOL-methodology dictates that all extensions to a theory should be
-be \textbf{definitional}.  The type definition mechanism that
+\textbf{definitional}.  The type definition mechanism that meets this
-meets this criterion is \ttindex{typedef}.  Note that \emph{type synonyms},
+criterion is \ttindex{typedef}.  Note that \emph{type synonyms}, which are
-which are inherited from {\Pure} and described elsewhere, are just
+inherited from Pure and described elsewhere, are just syntactic abbreviations
-syntactic abbreviations that have no logical meaning.
+that have no logical meaning.
 \begin{warn}
-Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
+Types in HOL must be non-empty; otherwise the quantifier rules would be
 unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
 \end{warn}
 A \bfindex{type definition} identifies the new type with a subset of
 an existing type.  More precisely, the new type is defined by
 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
 \end{array}
 \]
 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
 and its inverse $Abs_T$.
 \end{itemize}
-Below are two simple examples of \HOL\ type definitions.  Non-emptiness
+Below are two simple examples of HOL type definitions.  Non-emptiness is
-is proved automatically here.
+proved automatically here.
 \begin{ttbox}
 typedef unit = "{\ttlbrace}True{\ttrbrace}"
 typedef (prod)
 ('a, 'b) "*"    (infixr 20)
 \par
 \begin{ttbox}
 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
 \end{ttbox}
 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
-class of all \HOL\ types.
+class of all HOL types.
 \end{warn}
 \section{Records}
 where
 \begin{itemize}
 \item \textit{function} is the name of the function, either as an \textit{id}
 or a \textit{string}.
-\item \textit{rel} is a {\HOL} expression for the well-founded termination
+\item \textit{rel} is a HOL expression for the well-founded termination
 relation.
 \item \textit{congruence rules} are required only in highly exceptional
 circumstances.
 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 related to the \ZF\ one, described in a separate
+This package is related to the ZF one, described in a separate
 paper,%
 \footnote{It appeared in CADE~\cite{paulson-CADE}; 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 extra-logical automatic type-checking.  The types
+than ZF's thanks to HOL's extra-logical automatic type-checking.  The types of
-of the (co)inductive sets determine the domain of the fixedpoint definition,
+the (co)inductive sets determine the domain of the fixedpoint definition, and
-and the package does not have to use inference rules for type-checking.
+the package does not have to 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.
 The resulting theory structure contains a substructure, called~\texttt{Fin}.
 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}.  The induction
 rule is \texttt{Fin.induct}.
-For another example, here is a theory file defining the accessible
+For another example, here is a theory file defining the accessible part of a
-part of a relation.  The paper
+relation.  The paper \cite{paulson-CADE} discusses a ZF version of this
-\cite{paulson-CADE} discusses a \ZF\ version of this example in more
+example in more detail.
-detail.
 \begin{ttbox}
 Acc = WF + Inductive +
 consts acc :: "('a * 'a)set => 'a set"   (* accessible part *)
 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
+Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory
-substitutions and unifiers.  It is based on Paulson's previous
+of substitutions and unifiers.  It is based on Paulson's previous
-mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
+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
+set of theorems defined inductively.  A similar proof in ZF is described
-described elsewhere~\cite{paulson-set-II}.
+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.
 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}.
+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.
 %
 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 Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and
 the operator \cdx{range}.
 \begin{ttbox}
 context Set.thy;
 \end{ttbox}
 The set~$S$ is given as an unknown instead of a
 {\out Level 7}
 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
 {\out No subgoals!}
 \end{ttbox}
 How much creativity is required?  As it happens, Isabelle can prove this
-theorem automatically.  The default classical set \texttt{claset()} contains rules
+theorem automatically.  The default classical set \texttt{claset()} contains
-for most of the constructs of \HOL's set theory.  We must augment it with
+rules for most of the constructs of HOL's set theory.  We must augment it with
-\tdx{equalityCE} to break up set equalities, and then apply best-first
+\tdx{equalityCE} to break up set equalities, and then apply best-first search.
-search.  Depth-first search would diverge, but best-first search
+Depth-first search would diverge, but best-first search successfully navigates
-successfully navigates through the large search space.
+through the large search space.  \index{search!best-first}
-\index{search!best-first}
 \begin{ttbox}
 choplev 0;
 {\out Level 0}
 {\out ?S ~: range f}
 {\out  1. ?S ~: range f}

changeset 9695	ec7d7f877712
parent 9258	2121ff73a37d
child 9969	4753185f1dd2