summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.134 -their~{\ML} names. Some of the rules deserve additional comments: 1.135 +Figure~\ref{hol-rules} shows the inference rules of~HOL, with their~{\ML} 1.136 +names. Some of the rules deserve additional comments: 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}