--- 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
their~{\ML} names. Some of the rules deserve additional comments:
\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 @@
Isabelle provides no means of verifying that such overloading is sensible;
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
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 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.