author clasohm Thu, 29 Jun 1995 12:08:44 +0200 changeset 1162 7be0684950a3 parent 1161 1831ba01c90c child 1163 c080ff36d24e
 doc-src/Logics/CHOL.tex file | annotate | diff | comparison | revisions doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Logics/CHOL.tex	Thu Jun 29 10:43:07 1995 +0200
+++ b/doc-src/Logics/CHOL.tex	Thu Jun 29 12:08:44 1995 +0200
@@ -1,37 +1,36 @@
%% $Id$
\chapter{Higher-Order Logic}
\index{higher-order logic|(}
-\index{CHOL system@{\sc chol} system}
+\index{HOL system@{\sc chol} 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 book~\cite{andrews86} is a
+full description of higher-order logic.  Experience with the {\sc hol} system
+has demonstrated that higher-order logic is useful for hardware verification;
+beyond this, it is widely applicable in many areas of mathematics.  It is
+weaker than {\ZF} set theory but for most applications this does not matter.
+If you prefer {\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.

-The theory~\thydx{CHOL} implements higher-order logic with curried
-function application.  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 logic is useful for hardware
-verification; beyond this, it is widely applicable in many areas of
-mathematics.  It is weaker than {\ZF} set theory but for most
-applications this does not matter.  If you prefer {\ML} to Lisp, you
-will probably prefer \CHOL\ to~{\ZF}.
+The syntax of Isabelle's \HOL\ has recently been changed to look more like the
+traditional syntax of higher-order logic.  Function application is now
+curried.  To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you
+must write $f\,a\,b$.  Note that $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} and earlier versions of \HOL.  Early releases of
+Isabelle included still another version of~\HOL, with explicit type inference
+rules~\cite{paulson-COLOG}.  This version no longer exists, but \thydx{ZF}
+supports a similar style of reasoning.

-\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function
-application. Therefore the expression $f(a,b)$ (which in \HOL\ means
-f applied to the two arguments $a$ and $b$'') means f applied to
-the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as
-$<a,b>$ while in \CHOL\ the syntax $(a,b)$ is used.  Previous
-releases of Isabelle also included a different version of~\HOL, with
-explicit type inference rules~\cite{paulson-COLOG}.  This version no
-longer exists, but \thydx{ZF} supports a similar style of reasoning.
-
-\CHOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
+\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 type checker.  It identifies object-level functions
with meta-level functions, so it uses Isabelle's operations for abstraction
and application.  There is no apply' operator: function applications are
written as simply~$f~a$ rather than $f{\tt}a$.

-These identifications allow Isabelle to support \CHOL\ particularly nicely,
-but they also mean that \CHOL\ requires more sophistication from the user
+These identifications allow Isabelle to support \HOL\ particularly 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 {\tt show_types} set to {\tt true}.  Gain experience by
working in first-order logic before attempting to use higher-order logic.
@@ -122,7 +121,7 @@
& | & "EX!~" id~id^* " . " formula
\end{array}
\]
-\caption{Full grammar for \CHOL} \label{chol-grammar}
+\caption{Full grammar for \HOL} \label{chol-grammar}
\end{figure}

@@ -147,7 +146,7 @@
$\neg(a=b)$.

\begin{warn}
-  \CHOL\ has no if-and-only-if connective; logical equivalence is expressed
+  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
using equality.  But equality has a high priority, as befitting a
relation, while if-and-only-if typically has the lowest priority.  Thus,
$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
@@ -155,14 +154,14 @@
parentheses.
\end{warn}

-\subsection{Types}\label{CHOL-types}
+\subsection{Types}\label{HOL-types}
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
formulae are terms.  The built-in type~\tydx{fun}, which constructs function
types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
over functions.

-Types in \CHOL\ must be non-empty; otherwise the quantifier rules would be
+Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.

\index{type definitions}
@@ -185,7 +184,7 @@

\subsection{Binders}
Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
-satisfying~$P[a]$, if such exists.  Since all terms in \CHOL\ denote
+satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
something, a description is always meaningful, but we do not know its value
unless $P[x]$ defines it uniquely.  We may write descriptions as
\cdx{Eps}($P$) or use the syntax
@@ -199,8 +198,8 @@
$\exists!x. \exists!y.P~x~y$; note that this does not mean that there
exists a unique pair $(x,y)$ satisfying~$P~x~y$.

-\index{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system}
-Quantifiers have two notations.  As in Gordon's {\sc hol} system, \CHOL\
+\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
+Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
existential quantifier must be followed by a space; thus {\tt?x} is an
unknown, while \verb'? x.f x=y' is a quantification.  Isabelle's usual
@@ -219,7 +218,7 @@
the constant~\cdx{Let}.  It can be expanded by rewriting with its
definition, \tdx{Let_def}.

-\CHOL\ 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 {\tt case} constructs.  Therefore {\tt
case} and \sdx{of} are reserved words.  However, so far this is mere
@@ -240,7 +239,7 @@
\tdx{selectI}        P(x::'a) ==> P(@x.P x)
\tdx{True_or_False}  (P=True) | (P=False)
\end{ttbox}
-\caption{The {\tt CHOL} rules} \label{chol-rules}
+\caption{The {\tt HOL} rules} \label{chol-rules}
\end{figure}

@@ -260,12 +259,12 @@
\tdx{if_def}     If P x y == (\%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 CHOL} definitions} \label{chol-defs}
+\caption{The {\tt HOL} definitions} \label{chol-defs}
\end{figure}

\section{Rules of inference}
-Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, with
+Figure~\ref{chol-rules} shows the inference rules of~\HOL{}, with
\begin{ttdescription}
\item[\tdx{ext}] expresses extensionality of functions.
@@ -279,13 +278,13 @@
shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
\end{ttdescription}

-\CHOL{} follows standard practice in higher-order logic: only a few
+\HOL{} follows standard practice in higher-order logic: only a few
connectives are taken as primitive, with the remainder defined obscurely
(Fig.\ts\ref{chol-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~\CHOL{}, like all other Isabelle theories, uses
+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}
@@ -350,7 +349,7 @@
\subcaption{Logical equivalence}

\end{ttbox}
-\caption{Derived rules for \CHOL} \label{chol-lemmas1}
+\caption{Derived rules for \HOL} \label{chol-lemmas1}
\end{figure}

@@ -540,17 +539,17 @@
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 \CHOL\ as they
-do in~{\ZF}.  In \CHOL\ the intersection of the empty set is well-defined,
+Finite unions and intersections have the same behaviour in \HOL\ as they
+do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
denoting the universal set for the given type.

\subsection{Syntax of set theory}\index{*set type}
-\CHOL'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 the same as $\alpha\To bool$.  The new type is defined for
clarity and to avoid complications involving function types in unification.
Since Isabelle does not support type definitions (as mentioned in
-\S\ref{CHOL-types}), the isomorphisms between the two types are declared
+\S\ref{HOL-types}), the isomorphisms between the two types are declared
explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
argument order).
@@ -823,27 +822,27 @@
\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 CHOL/Set.ML} for
+after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
proofs pertaining to set theory.

Figure~\ref{chol-fun} presents derived inference rules involving functions.
They also include rules for \cdx{Inv}, which is defined in theory~{\tt
-  CHOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
+  HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
inverse of~$f$.  They also include natural deduction rules for the image
and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
Reasoning about function composition (the operator~\sdx{o}) and the
predicate~\cdx{surj} is done simply by expanding the definitions.  See
-the file {\tt CHOL/fun.ML} for a complete listing of the derived rules.
+the file {\tt HOL/fun.ML} for a complete listing of the derived rules.

Figure~\ref{chol-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 {\tt CHOL/subset.ML}.
+reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.

Figure~\ref{chol-equalities} presents many common set equalities.  They
include commutative, associative and distributive laws involving unions,
intersections and complements.  The proofs are mostly trivial, using the
-classical reasoner; see file {\tt CHOL/equalities.ML}.
+classical reasoner; see file {\tt HOL/equalities.ML}.

\begin{figure}
@@ -911,23 +910,23 @@

\section{Generic packages and classical reasoning}
-\CHOL\ instantiates most of Isabelle's generic packages;
-see {\tt CHOL/ROOT.ML} for details.
+\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, \CHOL\ instantiates the
+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 CHOL/simpdata.ML} for a complete listing of the simplification
+{\tt HOL/simpdata.ML} for a complete listing of the simplification
rules.
\item
It instantiates the classical reasoner, as described below.
\end{itemize}
-\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
+\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{chol-lemmas2} above.

@@ -1087,7 +1086,7 @@
there is no means of specifying the operators' properties and verifying
that instances of the operators satisfy those properties.  To be safe, the
-\CHOL\ theory includes no polymorphic axioms asserting general properties of
+\HOL\ theory includes no polymorphic axioms asserting general properties of
$<$ and~$\leq$.

Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
@@ -1161,22 +1160,22 @@
\begin{figure}
\begin{ttbox}\makeatother
\tdx{list_rec_Nil}    list_rec [] c h = c
-\tdx{list_rec_Cons}   list_rec a#l c h = h a l (list_rec l c h)
+\tdx{list_rec_Cons}   list_rec (a#l) c h = h a l (list_rec l c h)

\tdx{list_case_Nil}   list_case c h [] = c
-\tdx{list_case_Cons}  list_case c h x#xs = h x xs
+\tdx{list_case_Cons}  list_case c h (x#xs) = h x xs

\tdx{map_Nil}         map f [] = []
-\tdx{map_Cons}        map f x \# xs = f x \# map f xs
+\tdx{map_Cons}        map f (x#xs) = f x # map f xs

\tdx{null_Nil}        null [] = True
-\tdx{null_Cons}       null x#xs = False
+\tdx{null_Cons}       null (x#xs) = False

-\tdx{hd_Cons}         hd x#xs = x
-\tdx{tl_Cons}         tl x#xs = xs
+\tdx{hd_Cons}         hd (x#xs) = x
+\tdx{tl_Cons}         tl (x#xs) = xs

\tdx{ttl_Nil}         ttl [] = []
-\tdx{ttl_Cons}        ttl x#xs = xs
+\tdx{ttl_Cons}        ttl (x#xs) = xs

\tdx{append_Nil}      [] @ ys = ys
\tdx{append_Cons}     (x#xs) \at ys = x # xs \at ys
@@ -1185,10 +1184,10 @@
\tdx{mem_Cons}        x mem (y#ys) = if y=x then True else x mem ys

\tdx{filter_Nil}      filter P [] = []
-\tdx{filter_Cons}     filter P x#xs = if P x then x#filter P xs else filter P xs
+\tdx{filter_Cons}     filter P (x#xs) = if P x then x#filter P xs else filter P xs

\tdx{list_all_Nil}    list_all P [] = True
-\tdx{list_all_Cons}   list_all P x#xs = (P x & list_all P xs)
+\tdx{list_all_Cons}   list_all P (x#xs) = (P x & list_all P xs)
\end{ttbox}
\caption{Rewrite rules for lists} \label{chol-list-simps}
\end{figure}
@@ -1197,7 +1196,7 @@
\subsection{The type constructor for lists, {\tt list}}
\index{*list type}

-\CHOL's definition of lists is an example of an experimental method for
+\HOL's definition of lists is an example of an experimental method for
handling recursive data types.  Figure~\ref{chol-list} presents the theory
\thydx{List}: the basic list operations with their types and properties.

@@ -1374,10 +1373,10 @@
\subsubsection{The datatype $\alpha~list$}

We want to define the type $\alpha~list$.\footnote{Of course there is a list
-  type in CHOL already. This is only an example.} To do this we have to build
-a new theory that contains the type definition. We start from {\tt CHOL}.
+  type in HOL already. This is only an example.} To do this we have to build
+a new theory that contains the type definition. We start from {\tt HOL}.
\begin{ttbox}
-MyList = CHOL +
+MyList = HOL +
datatype 'a list = Nil | Cons 'a ('a list)
end
\end{ttbox}
@@ -1431,7 +1430,7 @@
\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
after the constructor declarations as follows:
\begin{ttbox}
-MyList = CHOL +
+MyList = HOL +
datatype 'a list = "[]" ("[]")
| "#" 'a ('a list) (infixr 70)
end
@@ -1473,7 +1472,7 @@
consts app :: "['a list,'a list] => 'a list"
rules
app_Nil   "app [] ys = ys"
-   app_Cons  "app x#xs ys = x#app xs ys"
+   app_Cons  "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
this carries with it the danger of accidentally asserting an inconsistency,
@@ -1484,7 +1483,7 @@
consts app :: "'['a list,'a list] => 'a list"
primrec app MyList.list
app_Nil   "app [] ys = ys"
-   app_Cons  "app x#xs ys = x#app xs ys"
+   app_Cons  "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
The system will now check that the two rules \verb$app_Nil$ and
@@ -1590,7 +1589,7 @@
This package is derived from the ZF one, described in 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 CHOL's
+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.
@@ -1728,27 +1727,27 @@
monos   "[Pow_mono]"
end
\end{ttbox}
-The CHOL distribution contains many other inductive definitions, such as the
-theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}.  The
-theory {\tt CHOL/ex/LList.thy} contains coinductive definitions.
+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/ex/LList.thy} contains coinductive definitions.

\index{*coinductive|)} \index{*inductive|)} \underscoreoff

\section{The examples directories}
-Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation 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
mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
theory~\cite{mw81}.

-Directory {\tt CHOL/IMP} contains a mechanised version of a semantic
+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 CHOL/ex} contains other examples and experimental proofs in
-{\CHOL}.  Here is an overview of the more interesting files.
+Directory {\tt HOL/ex} contains other examples and experimental proofs in
+{\HOL}.  Here is an overview of the more interesting files.
\begin{itemize}
\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
predicate calculus theorems, ranging from simple tautologies to
@@ -1811,7 +1810,7 @@
of~$\alpha$.  This version states that for every function from $\alpha$ to
its powerset, some subset is outside its range.

-The Isabelle proof uses \CHOL'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}.  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}
@@ -1878,7 +1877,7 @@
\end{ttbox}
How much creativity is required?  As it happens, Isabelle can prove this
theorem automatically.  The classical set \ttindex{set_cs} contains rules
-for most of the constructs of \CHOL's set theory.  We must augment it with
+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
search.  Depth-first search would diverge, but best-first search
successfully navigates through the large search space.
--- a/doc-src/Logics/HOL.tex	Thu Jun 29 10:43:07 1995 +0200
+++ b/doc-src/Logics/HOL.tex	Thu Jun 29 12:08:44 1995 +0200
@@ -1,37 +1,36 @@
%% $Id$
\chapter{Higher-Order Logic}
\index{higher-order logic|(}
-\index{CHOL system@{\sc chol} system}
+\index{HOL system@{\sc chol} 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 book~\cite{andrews86} is a
+full description of higher-order logic.  Experience with the {\sc hol} system
+has demonstrated that higher-order logic is useful for hardware verification;
+beyond this, it is widely applicable in many areas of mathematics.  It is
+weaker than {\ZF} set theory but for most applications this does not matter.
+If you prefer {\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.

-The theory~\thydx{CHOL} implements higher-order logic with curried
-function application.  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 logic is useful for hardware
-verification; beyond this, it is widely applicable in many areas of
-mathematics.  It is weaker than {\ZF} set theory but for most
-applications this does not matter.  If you prefer {\ML} to Lisp, you
-will probably prefer \CHOL\ to~{\ZF}.
+The syntax of Isabelle's \HOL\ has recently been changed to look more like the
+traditional syntax of higher-order logic.  Function application is now
+curried.  To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you
+must write $f\,a\,b$.  Note that $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} and earlier versions of \HOL.  Early releases of
+Isabelle included still another version of~\HOL, with explicit type inference
+rules~\cite{paulson-COLOG}.  This version no longer exists, but \thydx{ZF}
+supports a similar style of reasoning.

-\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function
-application. Therefore the expression $f(a,b)$ (which in \HOL\ means
-f applied to the two arguments $a$ and $b$'') means f applied to
-the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as
-$<a,b>$ while in \CHOL\ the syntax $(a,b)$ is used.  Previous
-releases of Isabelle also included a different version of~\HOL, with
-explicit type inference rules~\cite{paulson-COLOG}.  This version no
-longer exists, but \thydx{ZF} supports a similar style of reasoning.
-
-\CHOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
+\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 type checker.  It identifies object-level functions
with meta-level functions, so it uses Isabelle's operations for abstraction
and application.  There is no apply' operator: function applications are
written as simply~$f~a$ rather than $f{\tt}a$.

-These identifications allow Isabelle to support \CHOL\ particularly nicely,
-but they also mean that \CHOL\ requires more sophistication from the user
+These identifications allow Isabelle to support \HOL\ particularly 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 {\tt show_types} set to {\tt true}.  Gain experience by
working in first-order logic before attempting to use higher-order logic.
@@ -122,7 +121,7 @@
& | & "EX!~" id~id^* " . " formula
\end{array}
\]
-\caption{Full grammar for \CHOL} \label{chol-grammar}
+\caption{Full grammar for \HOL} \label{chol-grammar}
\end{figure}

@@ -147,7 +146,7 @@
$\neg(a=b)$.

\begin{warn}
-  \CHOL\ has no if-and-only-if connective; logical equivalence is expressed
+  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
using equality.  But equality has a high priority, as befitting a
relation, while if-and-only-if typically has the lowest priority.  Thus,
$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
@@ -155,14 +154,14 @@
parentheses.
\end{warn}

-\subsection{Types}\label{CHOL-types}
+\subsection{Types}\label{HOL-types}
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
formulae are terms.  The built-in type~\tydx{fun}, which constructs function
types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
over functions.

-Types in \CHOL\ must be non-empty; otherwise the quantifier rules would be
+Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.

\index{type definitions}
@@ -185,7 +184,7 @@

\subsection{Binders}
Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
-satisfying~$P[a]$, if such exists.  Since all terms in \CHOL\ denote
+satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
something, a description is always meaningful, but we do not know its value
unless $P[x]$ defines it uniquely.  We may write descriptions as
\cdx{Eps}($P$) or use the syntax
@@ -199,8 +198,8 @@
$\exists!x. \exists!y.P~x~y$; note that this does not mean that there
exists a unique pair $(x,y)$ satisfying~$P~x~y$.

-\index{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system}
-Quantifiers have two notations.  As in Gordon's {\sc hol} system, \CHOL\
+\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
+Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
existential quantifier must be followed by a space; thus {\tt?x} is an
unknown, while \verb'? x.f x=y' is a quantification.  Isabelle's usual
@@ -219,7 +218,7 @@
the constant~\cdx{Let}.  It can be expanded by rewriting with its
definition, \tdx{Let_def}.

-\CHOL\ 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 {\tt case} constructs.  Therefore {\tt
case} and \sdx{of} are reserved words.  However, so far this is mere
@@ -240,7 +239,7 @@
\tdx{selectI}        P(x::'a) ==> P(@x.P x)
\tdx{True_or_False}  (P=True) | (P=False)
\end{ttbox}
-\caption{The {\tt CHOL} rules} \label{chol-rules}
+\caption{The {\tt HOL} rules} \label{chol-rules}
\end{figure}

@@ -260,12 +259,12 @@
\tdx{if_def}     If P x y == (\%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 CHOL} definitions} \label{chol-defs}
+\caption{The {\tt HOL} definitions} \label{chol-defs}
\end{figure}

\section{Rules of inference}
-Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, with
+Figure~\ref{chol-rules} shows the inference rules of~\HOL{}, with
\begin{ttdescription}
\item[\tdx{ext}] expresses extensionality of functions.
@@ -279,13 +278,13 @@
shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
\end{ttdescription}

-\CHOL{} follows standard practice in higher-order logic: only a few
+\HOL{} follows standard practice in higher-order logic: only a few
connectives are taken as primitive, with the remainder defined obscurely
(Fig.\ts\ref{chol-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~\CHOL{}, like all other Isabelle theories, uses
+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}
@@ -350,7 +349,7 @@
\subcaption{Logical equivalence}

\end{ttbox}
-\caption{Derived rules for \CHOL} \label{chol-lemmas1}
+\caption{Derived rules for \HOL} \label{chol-lemmas1}
\end{figure}

@@ -540,17 +539,17 @@
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 \CHOL\ as they
-do in~{\ZF}.  In \CHOL\ the intersection of the empty set is well-defined,
+Finite unions and intersections have the same behaviour in \HOL\ as they
+do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
denoting the universal set for the given type.

\subsection{Syntax of set theory}\index{*set type}
-\CHOL'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 the same as $\alpha\To bool$.  The new type is defined for
clarity and to avoid complications involving function types in unification.
Since Isabelle does not support type definitions (as mentioned in
-\S\ref{CHOL-types}), the isomorphisms between the two types are declared
+\S\ref{HOL-types}), the isomorphisms between the two types are declared
explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
argument order).
@@ -823,27 +822,27 @@
\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 CHOL/Set.ML} for
+after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
proofs pertaining to set theory.

Figure~\ref{chol-fun} presents derived inference rules involving functions.
They also include rules for \cdx{Inv}, which is defined in theory~{\tt
-  CHOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
+  HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
inverse of~$f$.  They also include natural deduction rules for the image
and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
Reasoning about function composition (the operator~\sdx{o}) and the
predicate~\cdx{surj} is done simply by expanding the definitions.  See
-the file {\tt CHOL/fun.ML} for a complete listing of the derived rules.
+the file {\tt HOL/fun.ML} for a complete listing of the derived rules.

Figure~\ref{chol-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 {\tt CHOL/subset.ML}.
+reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.

Figure~\ref{chol-equalities} presents many common set equalities.  They
include commutative, associative and distributive laws involving unions,
intersections and complements.  The proofs are mostly trivial, using the
-classical reasoner; see file {\tt CHOL/equalities.ML}.
+classical reasoner; see file {\tt HOL/equalities.ML}.

\begin{figure}
@@ -911,23 +910,23 @@

\section{Generic packages and classical reasoning}
-\CHOL\ instantiates most of Isabelle's generic packages;
-see {\tt CHOL/ROOT.ML} for details.
+\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, \CHOL\ instantiates the
+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 CHOL/simpdata.ML} for a complete listing of the simplification
+{\tt HOL/simpdata.ML} for a complete listing of the simplification
rules.
\item
It instantiates the classical reasoner, as described below.
\end{itemize}
-\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
+\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{chol-lemmas2} above.

@@ -1087,7 +1086,7 @@
there is no means of specifying the operators' properties and verifying
that instances of the operators satisfy those properties.  To be safe, the
-\CHOL\ theory includes no polymorphic axioms asserting general properties of
+\HOL\ theory includes no polymorphic axioms asserting general properties of
$<$ and~$\leq$.

Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
@@ -1161,22 +1160,22 @@
\begin{figure}
\begin{ttbox}\makeatother
\tdx{list_rec_Nil}    list_rec [] c h = c
-\tdx{list_rec_Cons}   list_rec a#l c h = h a l (list_rec l c h)
+\tdx{list_rec_Cons}   list_rec (a#l) c h = h a l (list_rec l c h)

\tdx{list_case_Nil}   list_case c h [] = c
-\tdx{list_case_Cons}  list_case c h x#xs = h x xs
+\tdx{list_case_Cons}  list_case c h (x#xs) = h x xs

\tdx{map_Nil}         map f [] = []
-\tdx{map_Cons}        map f x \# xs = f x \# map f xs
+\tdx{map_Cons}        map f (x#xs) = f x # map f xs

\tdx{null_Nil}        null [] = True
-\tdx{null_Cons}       null x#xs = False
+\tdx{null_Cons}       null (x#xs) = False

-\tdx{hd_Cons}         hd x#xs = x
-\tdx{tl_Cons}         tl x#xs = xs
+\tdx{hd_Cons}         hd (x#xs) = x
+\tdx{tl_Cons}         tl (x#xs) = xs

\tdx{ttl_Nil}         ttl [] = []
-\tdx{ttl_Cons}        ttl x#xs = xs
+\tdx{ttl_Cons}        ttl (x#xs) = xs

\tdx{append_Nil}      [] @ ys = ys
\tdx{append_Cons}     (x#xs) \at ys = x # xs \at ys
@@ -1185,10 +1184,10 @@
\tdx{mem_Cons}        x mem (y#ys) = if y=x then True else x mem ys

\tdx{filter_Nil}      filter P [] = []
-\tdx{filter_Cons}     filter P x#xs = if P x then x#filter P xs else filter P xs
+\tdx{filter_Cons}     filter P (x#xs) = if P x then x#filter P xs else filter P xs

\tdx{list_all_Nil}    list_all P [] = True
-\tdx{list_all_Cons}   list_all P x#xs = (P x & list_all P xs)
+\tdx{list_all_Cons}   list_all P (x#xs) = (P x & list_all P xs)
\end{ttbox}
\caption{Rewrite rules for lists} \label{chol-list-simps}
\end{figure}
@@ -1197,7 +1196,7 @@
\subsection{The type constructor for lists, {\tt list}}
\index{*list type}

-\CHOL's definition of lists is an example of an experimental method for
+\HOL's definition of lists is an example of an experimental method for
handling recursive data types.  Figure~\ref{chol-list} presents the theory
\thydx{List}: the basic list operations with their types and properties.

@@ -1374,10 +1373,10 @@
\subsubsection{The datatype $\alpha~list$}

We want to define the type $\alpha~list$.\footnote{Of course there is a list
-  type in CHOL already. This is only an example.} To do this we have to build
-a new theory that contains the type definition. We start from {\tt CHOL}.
+  type in HOL already. This is only an example.} To do this we have to build
+a new theory that contains the type definition. We start from {\tt HOL}.
\begin{ttbox}
-MyList = CHOL +
+MyList = HOL +
datatype 'a list = Nil | Cons 'a ('a list)
end
\end{ttbox}
@@ -1431,7 +1430,7 @@
\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
after the constructor declarations as follows:
\begin{ttbox}
-MyList = CHOL +
+MyList = HOL +
datatype 'a list = "[]" ("[]")
| "#" 'a ('a list) (infixr 70)
end
@@ -1473,7 +1472,7 @@
consts app :: "['a list,'a list] => 'a list"
rules
app_Nil   "app [] ys = ys"
-   app_Cons  "app x#xs ys = x#app xs ys"
+   app_Cons  "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
this carries with it the danger of accidentally asserting an inconsistency,
@@ -1484,7 +1483,7 @@
consts app :: "'['a list,'a list] => 'a list"
primrec app MyList.list
app_Nil   "app [] ys = ys"
-   app_Cons  "app x#xs ys = x#app xs ys"
+   app_Cons  "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
The system will now check that the two rules \verb$app_Nil$ and
@@ -1590,7 +1589,7 @@
This package is derived from the ZF one, described in 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 CHOL's
+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.
@@ -1728,27 +1727,27 @@
monos   "[Pow_mono]"
end
\end{ttbox}
-The CHOL distribution contains many other inductive definitions, such as the
-theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}.  The
-theory {\tt CHOL/ex/LList.thy} contains coinductive definitions.
+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/ex/LList.thy} contains coinductive definitions.

\index{*coinductive|)} \index{*inductive|)} \underscoreoff

\section{The examples directories}
-Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation 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
mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
theory~\cite{mw81}.

-Directory {\tt CHOL/IMP} contains a mechanised version of a semantic
+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 CHOL/ex} contains other examples and experimental proofs in
-{\CHOL}.  Here is an overview of the more interesting files.
+Directory {\tt HOL/ex} contains other examples and experimental proofs in
+{\HOL}.  Here is an overview of the more interesting files.
\begin{itemize}
\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
predicate calculus theorems, ranging from simple tautologies to
@@ -1811,7 +1810,7 @@
of~$\alpha$.  This version states that for every function from $\alpha$ to
its powerset, some subset is outside its range.

-The Isabelle proof uses \CHOL'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}.  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}
@@ -1878,7 +1877,7 @@
\end{ttbox}
How much creativity is required?  As it happens, Isabelle can prove this
theorem automatically.  The classical set \ttindex{set_cs} contains rules
-for most of the constructs of \CHOL's set theory.  We must augment it with
+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
search.  Depth-first search would diverge, but best-first search
successfully navigates through the large search space.