doc-src/Logics/Old_HOL.tex
 changeset 9695 ec7d7f877712 parent 2975 230f456956a2
     1.1 --- a/doc-src/Logics/Old_HOL.tex	Mon Aug 28 13:50:24 2000 +0200
1.2 +++ b/doc-src/Logics/Old_HOL.tex	Mon Aug 28 13:52:38 2000 +0200
1.3 @@ -3,33 +3,32 @@
1.4  \index{higher-order logic|(}
1.5  \index{HOL system@{\sc hol} system}
1.6
1.7 -The theory~\thydx{HOL} implements higher-order logic.
1.8 -It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
1.9 -based on Church's original paper~\cite{church40}.  Andrews's
1.10 -book~\cite{andrews86} is a full description of higher-order logic.
1.11 -Experience with the {\sc hol} system has demonstrated that higher-order
1.12 -logic is useful for hardware verification; beyond this, it is widely
1.13 -applicable in many areas of mathematics.  It is weaker than {\ZF} set
1.14 -theory but for most applications this does not matter.  If you prefer {\ML}
1.15 -to Lisp, you will probably prefer \HOL\ to~{\ZF}.
1.16 +The theory~\thydx{HOL} implements higher-order logic.  It is based on
1.17 +Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
1.18 +Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a
1.19 +full description of higher-order logic.  Experience with the {\sc hol} system
1.20 +has demonstrated that higher-order logic is useful for hardware verification;
1.21 +beyond this, it is widely applicable in many areas of mathematics.  It is
1.22 +weaker than ZF set theory but for most applications this does not matter.  If
1.23 +you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
1.24
1.25 -Previous releases of Isabelle included a different version of~\HOL, with
1.26 +Previous releases of Isabelle included a different version of~HOL, with
1.27  explicit type inference rules~\cite{paulson-COLOG}.  This version no longer
1.28  exists, but \thydx{ZF} supports a similar style of reasoning.
1.29
1.30 -\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
1.31 -identifies object-level types with meta-level types, taking advantage of
1.32 -Isabelle's built-in type checker.  It identifies object-level functions
1.33 -with meta-level functions, so it uses Isabelle's operations for abstraction
1.34 -and application.  There is no apply' operator: function applications are
1.35 -written as simply~$f(a)$ rather than $f{\tt}a$.
1.36 +HOL has a distinct feel, compared with ZF and CTT.  It identifies object-level
1.37 +types with meta-level types, taking advantage of Isabelle's built-in type
1.38 +checker.  It identifies object-level functions with meta-level functions, so
1.39 +it uses Isabelle's operations for abstraction and application.  There is no
1.40 +apply' operator: function applications are written as simply~$f(a)$ rather
1.41 +than $f{\tt}a$.
1.42
1.43 -These identifications allow Isabelle to support \HOL\ particularly nicely,
1.44 -but they also mean that \HOL\ requires more sophistication from the user
1.45 ---- in particular, an understanding of Isabelle's type system.  Beginners
1.46 -should work with {\tt show_types} set to {\tt true}.  Gain experience by
1.47 -working in first-order logic before attempting to use higher-order logic.
1.48 -This chapter assumes familiarity with~{\FOL{}}.
1.49 +These identifications allow Isabelle to support HOL particularly nicely, but
1.50 +they also mean that HOL requires more sophistication from the user --- in
1.51 +particular, an understanding of Isabelle's type system.  Beginners should work
1.52 +with {\tt show_types} set to {\tt true}.  Gain experience by working in
1.53 +first-order logic before attempting to use higher-order logic.  This chapter
1.54 +assumes familiarity with~FOL.
1.55
1.56
1.57  \begin{figure}
1.58 @@ -115,7 +114,7 @@
1.59           & | & "EX!~" id~id^* " . " formula
1.60    \end{array}
1.61  \]
1.62 -\caption{Full grammar for \HOL} \label{hol-grammar}
1.63 +\caption{Full grammar for HOL} \label{hol-grammar}
1.64  \end{figure}
1.65
1.66
1.67 @@ -140,7 +139,7 @@
1.68  $\neg(a=b)$.
1.69
1.70  \begin{warn}
1.71 -  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.72 +  HOL has no if-and-only-if connective; logical equivalence is expressed
1.73    using equality.  But equality has a high priority, as befitting a
1.74    relation, while if-and-only-if typically has the lowest priority.  Thus,
1.75    $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
1.76 @@ -155,7 +154,7 @@
1.77  belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
1.78  over functions.
1.79
1.80 -Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.81 +Types in HOL must be non-empty; otherwise the quantifier rules would be
1.82  unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
1.83
1.84  \index{type definitions}
1.85 @@ -178,11 +177,10 @@
1.86
1.87  \subsection{Binders}
1.88  Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
1.89 -satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
1.90 -something, a description is always meaningful, but we do not know its value
1.91 -unless $P[x]$ defines it uniquely.  We may write descriptions as
1.92 -\cdx{Eps}($P$) or use the syntax
1.93 -\hbox{\tt \at $x$.$P[x]$}.
1.94 +satisfying~$P[a]$, if such exists.  Since all terms in HOL denote something, a
1.95 +description is always meaningful, but we do not know its value unless $P[x]$
1.96 +defines it uniquely.  We may write descriptions as \cdx{Eps}($P$) or use the
1.97 +syntax \hbox{\tt \at $x$.$P[x]$}.
1.98
1.99  Existential quantification is defined by
1.100  $\exists x.P(x) \;\equiv\; P(\epsilon x.P(x)).$
1.101 @@ -193,14 +191,14 @@
1.102  exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
1.103
1.104  \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
1.105 -Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
1.106 +Quantifiers have two notations.  As in Gordon's {\sc hol} system, HOL
1.107  uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
1.108  existential quantifier must be followed by a space; thus {\tt?x} is an
1.109  unknown, while \verb'? x.f(x)=y' is a quantification.  Isabelle's usual
1.110 -notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
1.111 -available.  Both notations are accepted for input.  The {\ML} reference
1.112 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available.  Both
1.113 +notations are accepted for input.  The {\ML} reference
1.114  \ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
1.115 -true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
1.116 +  true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
1.117  to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
1.118
1.119  All these binders have priority 10.
1.120 @@ -212,7 +210,7 @@
1.121  the constant~\cdx{Let}.  It can be expanded by rewriting with its
1.122  definition, \tdx{Let_def}.
1.123
1.124 -\HOL\ also defines the basic syntax
1.125 +HOL also defines the basic syntax
1.126  $\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n$
1.127  as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
1.128    case} and \sdx{of} are reserved words.  However, so far this is mere
1.129 @@ -259,8 +257,8 @@
1.130
1.131
1.132  \section{Rules of inference}
1.133 -Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
1.135 +Figure~\ref{hol-rules} shows the inference rules of~HOL, with their~{\ML}
1.137  \begin{ttdescription}
1.138  \item[\tdx{ext}] expresses extensionality of functions.
1.139  \item[\tdx{iff}] asserts that logically equivalent formulae are
1.140 @@ -273,14 +271,14 @@
1.141      shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
1.142  \end{ttdescription}
1.143
1.144 -\HOL{} follows standard practice in higher-order logic: only a few
1.145 -connectives are taken as primitive, with the remainder defined obscurely
1.146 +HOL follows standard practice in higher-order logic: only a few connectives
1.147 +are taken as primitive, with the remainder defined obscurely
1.148  (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
1.149  corresponding definitions \cite[page~270]{mgordon-hol} using
1.150 -object-equality~({\tt=}), which is possible because equality in
1.151 -higher-order logic may equate formulae and even functions over formulae.
1.152 -But theory~\HOL{}, like all other Isabelle theories, uses
1.153 -meta-equality~({\tt==}) for definitions.
1.154 +object-equality~({\tt=}), which is possible because equality in higher-order
1.155 +logic may equate formulae and even functions over formulae.  But theory~HOL,
1.156 +like all other Isabelle theories, uses meta-equality~({\tt==}) for
1.157 +definitions.
1.158
1.159  Some of the rules mention type variables; for
1.160  example, {\tt refl} mentions the type variable~{\tt'a}.  This allows you to
1.161 @@ -344,7 +342,7 @@
1.162  \subcaption{Logical equivalence}
1.163
1.164  \end{ttbox}
1.165 -\caption{Derived rules for \HOL} \label{hol-lemmas1}
1.166 +\caption{Derived rules for HOL} \label{hol-lemmas1}
1.167  \end{figure}
1.168
1.169
1.170 @@ -521,8 +519,8 @@
1.171  \section{A formulation of set theory}
1.172  Historically, higher-order logic gives a foundation for Russell and
1.173  Whitehead's theory of classes.  Let us use modern terminology and call them
1.174 -{\bf sets}, but note that these sets are distinct from those of {\ZF} set
1.175 -theory, and behave more like {\ZF} classes.
1.176 +{\bf sets}, but note that these sets are distinct from those of ZF set theory,
1.177 +and behave more like ZF classes.
1.178  \begin{itemize}
1.179  \item
1.180  Sets are given by predicates over some type~$\sigma$.  Types serve to
1.181 @@ -534,20 +532,19 @@
1.182  Although sets may contain other sets as elements, the containing set must
1.183  have a more complex type.
1.184  \end{itemize}
1.185 -Finite unions and intersections have the same behaviour in \HOL\ as they
1.186 -do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
1.187 -denoting the universal set for the given type.
1.188 +Finite unions and intersections have the same behaviour in HOL as they do
1.189 +in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
1.190 +universal set for the given type.
1.191
1.192
1.193  \subsection{Syntax of set theory}\index{*set type}
1.194 -\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
1.195 -essentially the same as $\alpha\To bool$.  The new type is defined for
1.196 -clarity and to avoid complications involving function types in unification.
1.197 -Since Isabelle does not support type definitions (as mentioned in
1.198 -\S\ref{HOL-types}), the isomorphisms between the two types are declared
1.199 -explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
1.200 -$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
1.201 -argument order).
1.202 +HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially
1.203 +the same as $\alpha\To bool$.  The new type is defined for clarity and to
1.204 +avoid complications involving function types in unification.  Since Isabelle
1.205 +does not support type definitions (as mentioned in \S\ref{HOL-types}), the
1.206 +isomorphisms between the two types are declared explicitly.  Here they are
1.207 +natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt
1.208 +  op :} maps in the other direction (ignoring argument order).
1.209
1.210  Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
1.211  translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
1.212 @@ -563,11 +560,11 @@
1.213    {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
1.214  \end{eqnarray*}
1.215
1.216 -The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
1.217 -that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
1.218 -occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda 1.219 -x.P[x])$.  It defines sets by absolute comprehension, which is impossible
1.220 -in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
1.221 +The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) that
1.222 +satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences
1.223 +of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.P[x])$.  It defines
1.224 +sets by absolute comprehension, which is impossible in~ZF; the type of~$x$
1.225 +implicitly restricts the comprehension.
1.226
1.227  The set theory defines two {\bf bounded quantifiers}:
1.228  \begin{eqnarray*}
1.229 @@ -811,14 +808,13 @@
1.230
1.231
1.232  Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
1.233 -obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
1.234 -such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
1.235 -are designed for classical reasoning; the rules \tdx{subsetD},
1.236 -\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
1.237 -strictly necessary but yield more natural proofs.  Similarly,
1.238 -\tdx{equalityCE} supports classical reasoning about extensionality,
1.239 -after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
1.240 -proofs pertaining to set theory.
1.241 +obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
1.242 +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
1.243 +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
1.244 +not strictly necessary but yield more natural proofs.  Similarly,
1.245 +\tdx{equalityCE} supports classical reasoning about extensionality, after the
1.246 +fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for proofs pertaining
1.247 +to set theory.
1.248
1.249  Figure~\ref{hol-fun} presents derived inference rules involving functions.
1.250  They also include rules for \cdx{Inv}, which is defined in theory~{\tt
1.251 @@ -905,13 +901,12 @@
1.252
1.253
1.254  \section{Generic packages and classical reasoning}
1.255 -\HOL\ instantiates most of Isabelle's generic packages;
1.256 -see {\tt HOL/ROOT.ML} for details.
1.257 +HOL instantiates most of Isabelle's generic packages; see {\tt HOL/ROOT.ML}
1.258 +for details.
1.259  \begin{itemize}
1.260 -\item
1.261 -Because it includes a general substitution rule, \HOL\ instantiates the
1.262 -tactic {\tt hyp_subst_tac}, which substitutes for an equality
1.263 -throughout a subgoal and its hypotheses.
1.264 +\item Because it includes a general substitution rule, HOL instantiates the
1.265 +  tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
1.266 +  subgoal and its hypotheses.
1.267  \item
1.268  It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
1.269  simplification set for higher-order logic.  Equality~($=$), which also
1.270 @@ -921,14 +916,14 @@
1.271  \item
1.272  It instantiates the classical reasoner, as described below.
1.273  \end{itemize}
1.274 -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1.275 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1.276 -rule; recall Fig.\ts\ref{hol-lemmas2} above.
1.277 +HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
1.278 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
1.279 +Fig.\ts\ref{hol-lemmas2} above.
1.280
1.281 -The classical reasoner is set up as the structure
1.282 -{\tt Classical}.  This structure is open, so {\ML} identifiers such
1.283 -as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
1.284 -\HOL\ defines the following classical rule sets:
1.285 +The classical reasoner is set up as the structure {\tt Classical}.  This
1.286 +structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt
1.287 +  fast_tac}, {\tt best_tac}, etc., refer to it.  HOL defines the following
1.288 +classical rule sets:
1.289  \begin{ttbox}
1.290  prop_cs    : claset
1.291  HOL_cs     : claset
1.292 @@ -1075,13 +1070,12 @@
1.293  called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
1.294  similar constructions in the context of set theory~\cite{paulson-set-II}.
1.295
1.296 -Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
1.297 -overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
1.298 -Isabelle provides no means of verifying that such overloading is sensible;
1.299 -there is no means of specifying the operators' properties and verifying
1.300 -that instances of the operators satisfy those properties.  To be safe, the
1.301 -\HOL\ theory includes no polymorphic axioms asserting general properties of
1.302 -$<$ and~$\leq$.
1.303 +Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which overloads
1.304 +$<$ and $\leq$ on the natural numbers.  As of this writing, Isabelle provides
1.305 +no means of verifying that such overloading is sensible; there is no means of
1.306 +specifying the operators' properties and verifying that instances of the
1.307 +operators satisfy those properties.  To be safe, the HOL theory includes no
1.308 +polymorphic axioms asserting general properties of $<$ and~$\leq$.
1.309
1.310  Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
1.311  defines addition, multiplication, subtraction, division, and remainder.
1.312 @@ -1190,9 +1184,9 @@
1.313  \subsection{The type constructor for lists, {\tt list}}
1.314  \index{*list type}
1.315
1.316 -\HOL's definition of lists is an example of an experimental method for
1.317 -handling recursive data types.  Figure~\ref{hol-list} presents the theory
1.318 -\thydx{List}: the basic list operations with their types and properties.
1.319 +HOL's definition of lists is an example of an experimental method for handling
1.320 +recursive data types.  Figure~\ref{hol-list} presents the theory \thydx{List}:
1.321 +the basic list operations with their types and properties.
1.322
1.323  The \sdx{case} construct is defined by the following translation:
1.324  {\dquotes
1.325 @@ -1740,8 +1734,8 @@
1.326  proves the two equivalent.  It contains several datatype and inductive
1.327  definitions, and demonstrates their use.
1.328
1.329 -Directory {\tt HOL/ex} contains other examples and experimental proofs in
1.330 -{\HOL}.  Here is an overview of the more interesting files.
1.331 +Directory {\tt HOL/ex} contains other examples and experimental proofs in HOL.
1.332 +Here is an overview of the more interesting files.
1.333  \begin{itemize}
1.334  \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
1.335    predicate calculus theorems, ranging from simple tautologies to
1.336 @@ -1770,12 +1764,12 @@
1.337    as filter, which can compute indefinitely before yielding the next
1.338    element (if any!) of the lazy list.  A coinduction principle is defined
1.339    for proving equations on lazy lists.
1.340 -
1.341 -\item Theory {\tt PropLog} proves the soundness and completeness of
1.342 -  classical propositional logic, given a truth table semantics.  The only
1.343 -  connective is $\imp$.  A Hilbert-style axiom system is specified, and its
1.344 -  set of theorems defined inductively.  A similar proof in \ZF{} is
1.345 -  described elsewhere~\cite{paulson-set-II}.
1.346 +
1.347 +\item Theory {\tt PropLog} proves the soundness and completeness of classical
1.348 +  propositional logic, given a truth table semantics.  The only connective is
1.349 +  $\imp$.  A Hilbert-style axiom system is specified, and its set of theorems
1.350 +  defined inductively.  A similar proof in ZF is described
1.351 +  elsewhere~\cite{paulson-set-II}.
1.352
1.353  \item Theory {\tt Term} develops an experimental recursive type definition;
1.354    the recursion goes through the type constructor~\tydx{list}.
1.355 @@ -1804,8 +1798,8 @@
1.356  of~$\alpha$.  This version states that for every function from $\alpha$ to
1.357  its powerset, some subset is outside its range.
1.358
1.359 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1.360 -the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
1.361 +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and the
1.362 +operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
1.363  quantified variable so that we may inspect the subset found by the proof.
1.364  \begin{ttbox}
1.365  goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1.366 @@ -1870,12 +1864,11 @@
1.367  {\out No subgoals!}
1.368  \end{ttbox}
1.369  How much creativity is required?  As it happens, Isabelle can prove this
1.370 -theorem automatically.  The classical set \ttindex{set_cs} contains rules
1.371 -for most of the constructs of \HOL's set theory.  We must augment it with
1.372 -\tdx{equalityCE} to break up set equalities, and then apply best-first
1.373 -search.  Depth-first search would diverge, but best-first search
1.374 -successfully navigates through the large search space.
1.375 -\index{search!best-first}
1.376 +theorem automatically.  The classical set \ttindex{set_cs} contains rules for
1.377 +most of the constructs of HOL's set theory.  We must augment it with
1.378 +\tdx{equalityCE} to break up set equalities, and then apply best-first search.
1.379 +Depth-first search would diverge, but best-first search successfully navigates
1.380 +through the large search space.  \index{search!best-first}
1.381  \begin{ttbox}
1.382  choplev 0;
1.383  {\out Level 0}