1.1 --- a/doc-src/Logics/Old_HOL.tex Sun Mar 27 12:33:14 1994 +0200
1.2 +++ b/doc-src/Logics/Old_HOL.tex Wed Mar 30 17:31:18 1994 +0200
1.3 @@ -7,22 +7,22 @@
1.4 higher-order logic is useful for hardware verification; beyond this, it is
1.5 widely applicable in many areas of mathematics. It is weaker than {\ZF}
1.6 set theory but for most applications this does not matter. If you prefer
1.7 -{\ML} to Lisp, you will probably prefer {\HOL} to~{\ZF}.
1.8 +{\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.
1.9
1.10 Previous releases of Isabelle included a completely different version
1.11 -of~{\HOL}, with explicit type inference rules~\cite{paulson-COLOG}. This
1.12 +of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
1.13 version no longer exists, but \ttindex{ZF} supports a similar style of
1.14 reasoning.
1.15
1.16 -{\HOL} has a distinct feel, compared with {\ZF} and {\CTT}. It
1.17 +\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
1.18 identifies object-level types with meta-level types, taking advantage of
1.19 Isabelle's built-in type checker. It identifies object-level functions
1.20 with meta-level functions, so it uses Isabelle's operations for abstraction
1.21 and application. There is no ``apply'' operator: function applications are
1.22 written as simply~$f(a)$ rather than $f{\tt`}a$.
1.23
1.24 -These identifications allow Isabelle to support {\HOL} particularly nicely,
1.25 -but they also mean that {\HOL} requires more sophistication from the user
1.26 +These identifications allow Isabelle to support \HOL\ particularly nicely,
1.27 +but they also mean that \HOL\ requires more sophistication from the user
1.28 --- in particular, an understanding of Isabelle's type system. Beginners
1.29 should gain experience by working in first-order logic, before attempting
1.30 to use higher-order logic. This chapter assumes familiarity with~{\FOL{}}.
1.31 @@ -37,35 +37,39 @@
1.32 \idx{True} & $bool$ & tautology ($\top$) \\
1.33 \idx{False} & $bool$ & absurdity ($\bot$) \\
1.34 \idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
1.35 - \idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion
1.36 + \idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
1.37 + \idx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
1.38 \end{tabular}
1.39 \end{center}
1.40 \subcaption{Constants}
1.41
1.42 -\index{"@@{\tt\at}}
1.43 \begin{center}
1.44 +\index{"@@{\tt\at}|bold}
1.45 +\index{*"!|bold}
1.46 +\index{*"?"!|bold}
1.47 \begin{tabular}{llrrr}
1.48 \it symbol &\it name &\it meta-type & \it prec & \it description \\
1.49 - \tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 &
1.50 + \tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 &
1.51 Hilbert description ($\epsilon$) \\
1.52 - \idx{!} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
1.53 + \tt! & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
1.54 universal quantifier ($\forall$) \\
1.55 \idx{?} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
1.56 existential quantifier ($\exists$) \\
1.57 - \idx{?!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
1.58 + \tt?! & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
1.59 unique existence ($\exists!$)
1.60 \end{tabular}
1.61 \end{center}
1.62 \subcaption{Binders}
1.63
1.64 \begin{center}
1.65 +\index{*"E"X"!|bold}
1.66 \begin{tabular}{llrrr}
1.67 \it symbol &\it name &\it meta-type & \it prec & \it description \\
1.68 \idx{ALL} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
1.69 universal quantifier ($\forall$) \\
1.70 \idx{EX} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
1.71 existential quantifier ($\exists$) \\
1.72 - \idx{EX!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
1.73 + \tt EX! & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
1.74 unique existence ($\exists!$)
1.75 \end{tabular}
1.76 \end{center}
1.77 @@ -94,11 +98,14 @@
1.78 \end{figure}
1.79
1.80
1.81 -\begin{figure}
1.82 +\begin{figure}
1.83 +\indexbold{*let}
1.84 +\indexbold{*in}
1.85 \dquotes
1.86 \[\begin{array}{rcl}
1.87 term & = & \hbox{expression of class~$term$} \\
1.88 - & | & "\at~~" id~id^* " . " formula \\[2ex]
1.89 + & | & "\at~~" id~id^* " . " formula \\
1.90 + & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\[2ex]
1.91 formula & = & \hbox{expression of type~$bool$} \\
1.92 & | & term " = " term \\
1.93 & | & term " \ttilde= " term \\
1.94 @@ -117,7 +124,7 @@
1.95 \end{array}
1.96 \]
1.97 \subcaption{Grammar}
1.98 -\caption{Full grammar for {\HOL}} \label{hol-grammar}
1.99 +\caption{Full grammar for \HOL} \label{hol-grammar}
1.100 \end{figure}
1.101
1.102
1.103 @@ -145,7 +152,7 @@
1.104 formulae are terms. The built-in type~$fun$, which constructs function
1.105 types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
1.106 $\sigma$ and~$\tau$ do; this allows quantification over functions. Types
1.107 -in {\HOL} must be non-empty; otherwise the quantifier rules would be
1.108 +in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.109 unsound~\cite[\S7]{paulson-COLOG}.
1.110
1.111 Gordon's {\sc hol} system supports {\bf type definitions}. A type is
1.112 @@ -166,7 +173,7 @@
1.113
1.114 \subsection{Binders}
1.115 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
1.116 -satisfying~$P[a]$, if such exists. Since all terms in {\HOL} denote
1.117 +satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote
1.118 something, a description is always meaningful, but we do not know its value
1.119 unless $P[x]$ defines it uniquely. We may write descriptions as
1.120 \ttindexbold{Eps}($P$) or use the syntax
1.121 @@ -180,7 +187,7 @@
1.122 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
1.123
1.124 \index{*"!}\index{*"?}
1.125 -Quantifiers have two notations. As in Gordon's {\sc hol} system, {\HOL}
1.126 +Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
1.127 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
1.128 existential quantifier must be followed by a space; thus {\tt?x} is an
1.129 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
1.130 @@ -199,7 +206,21 @@
1.131 \hbox{\tt \at $x\,y$.$P[x,y]$}.
1.132 \end{warn}
1.133
1.134 -\begin{figure}
1.135 +\subsection{\idx{let} and \idx{case}}
1.136 +Local abbreviations can be introduced via a \ttindex{let}-construct whose
1.137 +syntax is shown in Fig.~\ref{hol-grammar}. Internally it is translated into
1.138 +the constant \ttindex{Let} and can be expanded by rewriting with its
1.139 +definition \ttindex{Let_def}.
1.140 +
1.141 +\HOL\ also defines the basic syntax {\dquotes$"case"~e~"of"~c@1~"=>"~e@1~"|"
1.142 + \dots "|"~c@n~"=>"~e@n$} for {\tt case}-constructs, which means that {\tt
1.143 + case} and \ttindex{of} are reserved words. However, so far this is mere
1.144 +syntax and has no logical meaning. In order to be useful it needs to be
1.145 +filled with life by translating certain case constructs into meaningful
1.146 +terms. For an example see the case construct for the type of lists below.
1.147 +
1.148 +
1.149 +\begin{figure}
1.150 \begin{ttbox}\makeatother
1.151 \idx{refl} t = t::'a
1.152 \idx{subst} [| s=t; P(s) |] ==> P(t::'a)
1.153 @@ -224,6 +245,7 @@
1.154 \idx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y)
1.155 \idx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
1.156 \idx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
1.157 +\idx{Let_def} Let(s,f) = f(s)
1.158 \subcaption{Further definitions}
1.159 \end{ttbox}
1.160 \caption{Rules of {\tt HOL}} \label{hol-rules}
1.161 @@ -267,7 +289,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 @@ -358,7 +380,7 @@
1.171 \end{description}
1.172
1.173 \begin{warn}
1.174 -{\HOL} has no if-and-only-if connective; logical equivalence is expressed
1.175 +\HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.176 using equality. But equality has a high precedence, as befitting a
1.177 relation, while if-and-only-if typically has the lowest precedence. Thus,
1.178 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. When
1.179 @@ -381,11 +403,11 @@
1.180
1.181
1.182 \section{Generic packages}
1.183 -{\HOL} instantiates most of Isabelle's generic packages;
1.184 +\HOL\ instantiates most of Isabelle's generic packages;
1.185 see {\tt HOL/ROOT.ML} for details.
1.186 \begin{itemize}
1.187 \item
1.188 -Because it includes a general substitution rule, {\HOL} instantiates the
1.189 +Because it includes a general substitution rule, \HOL\ instantiates the
1.190 tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
1.191 throughout a subgoal and its hypotheses.
1.192 \item
1.193 @@ -464,12 +486,13 @@
1.194 \end{tabular}
1.195 \end{center}
1.196 \subcaption{Infixes}
1.197 -\caption{Syntax of {\HOL}'s set theory} \label{hol-set-syntax}
1.198 +\caption{Syntax of \HOL's set theory} \label{hol-set-syntax}
1.199 \end{figure}
1.200
1.201
1.202 \begin{figure}
1.203 \begin{center} \tt\frenchspacing
1.204 +\index{*"!|bold}
1.205 \begin{tabular}{rrr}
1.206 \it external & \it internal & \it description \\
1.207 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
1.208 @@ -481,7 +504,7 @@
1.209 \rm intersection over a set \\
1.210 \idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
1.211 \rm union over a set \\
1.212 - \idx{!} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
1.213 + \tt ! $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
1.214 \rm bounded $\forall$ \\
1.215 \idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
1.216 \rm bounded $\exists$ \\[1ex]
1.217 @@ -517,7 +540,7 @@
1.218 \end{array}
1.219 \]
1.220 \subcaption{Full Grammar}
1.221 -\caption{Syntax of {\HOL}'s set theory (continued)} \label{hol-set-syntax2}
1.222 +\caption{Syntax of \HOL's set theory (continued)} \label{hol-set-syntax2}
1.223 \end{figure}
1.224
1.225
1.226 @@ -550,7 +573,7 @@
1.227 \idx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
1.228 \subcaption{Definitions}
1.229 \end{ttbox}
1.230 -\caption{Rules of {\HOL}'s set theory} \label{hol-set-rules}
1.231 +\caption{Rules of \HOL's set theory} \label{hol-set-rules}
1.232 \end{figure}
1.233
1.234
1.235 @@ -650,8 +673,8 @@
1.236 Although sets may contain other sets as elements, the containing set must
1.237 have a more complex type.
1.238 \end{itemize}
1.239 -Finite unions and intersections have the same behaviour in {\HOL} as they
1.240 -do in~{\ZF}. In {\HOL} the intersection of the empty set is well-defined,
1.241 +Finite unions and intersections have the same behaviour in \HOL\ as they
1.242 +do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
1.243 denoting the universal set for the given type.
1.244
1.245 \subsection{Syntax of set theory}
1.246 @@ -715,7 +738,7 @@
1.247 These include straightforward properties of functions: image~({\tt``}) and
1.248 {\tt range}, and predicates concerning monotonicity, injectiveness, etc.
1.249
1.250 -{\HOL}'s set theory has the {\ML} identifier \ttindexbold{Set.thy}.
1.251 +\HOL's set theory has the {\ML} identifier \ttindexbold{Set.thy}.
1.252
1.253 \begin{figure} \underscoreon
1.254 \begin{ttbox}
1.255 @@ -876,15 +899,15 @@
1.256 \it name &\it meta-type & \it description \\
1.257 \idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\
1.258 \idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\
1.259 - \idx{case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
1.260 + \idx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
1.261 & conditional
1.262 \end{tabular}
1.263 \end{center}
1.264 \subcaption{Constants}
1.265
1.266 \begin{ttbox}\makeatletter
1.267 -\idx{case_def} case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
1.268 - (!y. p=Inr(y) --> z=g(y)))
1.269 +\idx{sum_case_def} sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
1.270 + (!y. p=Inr(y) --> z=g(y)))
1.271 \subcaption{Definition}
1.272
1.273 \idx{Inl_not_Inr} ~ Inl(a)=Inr(b)
1.274 @@ -894,10 +917,10 @@
1.275
1.276 \idx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
1.277
1.278 -\idx{case_Inl} case(Inl(x), f, g) = f(x)
1.279 -\idx{case_Inr} case(Inr(x), f, g) = g(x)
1.280 +\idx{sum_case_Inl} sum_case(Inl(x), f, g) = f(x)
1.281 +\idx{sum_case_Inr} sum_case(Inr(x), f, g) = g(x)
1.282
1.283 -\idx{surjective_sum} case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
1.284 +\idx{surjective_sum} sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
1.285 \subcaption{Derived rules}
1.286 \end{ttbox}
1.287 \caption{Rules for type $\alpha+\beta$}
1.288 @@ -912,7 +935,7 @@
1.289 product, sum, natural number and list types.
1.290
1.291 \subsection{Product and sum types}
1.292 -{\HOL} defines the product type $\alpha\times\beta$ and the sum type
1.293 +\HOL\ defines the product type $\alpha\times\beta$ and the sum type
1.294 $\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
1.295 standard constructions (Figs.~\ref{hol-prod} and~\ref{hol-sum}). Because
1.296 Isabelle does not support abstract type definitions, the isomorphisms
1.297 @@ -1016,7 +1039,7 @@
1.298
1.299
1.300 \subsection{The type of natural numbers, $nat$}
1.301 -{\HOL} defines the natural numbers in a roundabout but traditional way.
1.302 +\HOL\ defines the natural numbers in a roundabout but traditional way.
1.303 The axiom of infinity postulates an type~$ind$ of individuals, which is
1.304 non-empty and closed under an injective operation. The natural numbers are
1.305 inductively generated by choosing an arbitrary individual for~0 and using
1.306 @@ -1032,7 +1055,7 @@
1.307 Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
1.308 $\leq$ on the natural numbers. As of this writing, Isabelle provides no
1.309 means of verifying that such overloading is sensible. On the other hand,
1.310 -the {\HOL} theory includes no polymorphic axioms stating general properties
1.311 +the \HOL\ theory includes no polymorphic axioms stating general properties
1.312 of $<$ and $\leq$.
1.313
1.314 File {\tt HOL/arith.ML} develops arithmetic on the natural numbers.
1.315 @@ -1047,52 +1070,93 @@
1.316 be well-founded; recursion along this relation is primitive recursion,
1.317 while its transitive closure is~$<$.
1.318
1.319 -
1.320 \begin{figure}
1.321 \begin{center}
1.322 \begin{tabular}{rrr}
1.323 \it symbol & \it meta-type & \it description \\
1.324 - \idx{Nil} & $\alpha list$ & the empty list\\
1.325 - \idx{Cons} & $[\alpha, \alpha list] \To \alpha list$
1.326 - & list constructor\\
1.327 + \idx{Nil} & $\alpha list$ & empty list\\
1.328 + \idx{null} & $\alpha list \To bool$ & emptyness test\\
1.329 + \idx{hd} & $\alpha list \To \alpha$ & head \\
1.330 + \idx{tl} & $\alpha list \To \alpha list$ & tail \\
1.331 + \idx{ttl} & $\alpha list \To \alpha list$ & total tail \\
1.332 + \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1.333 + & mapping functional\\
1.334 + \idx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1.335 + & forall functional\\
1.336 + \idx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1.337 + & filter functional\\
1.338 \idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1.339 \beta]\To\beta] \To \beta$
1.340 - & list recursor\\
1.341 - \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1.342 - & mapping functional
1.343 + & list recursor
1.344 \end{tabular}
1.345 \end{center}
1.346 -\subcaption{Constants}
1.347 +
1.348 +\begin{center}
1.349 +\index{"# @{\tt\#}|bold}
1.350 +\index{"@@{\tt\at}|bold}
1.351 +\begin{tabular}{rrrr}
1.352 + \it symbol & \it meta-type & \it precedence & \it description \\
1.353 + \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & cons \\
1.354 + \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1.355 + \idx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership
1.356 +\end{tabular}
1.357 +\end{center}
1.358 +\subcaption{Constants and infixes}
1.359 +
1.360 +\begin{center} \tt\frenchspacing
1.361 +\begin{tabular}{rrr}
1.362 + \it external & \it internal & \it description \\{}
1.363 + \idx{[]} & Nil & empty list \\{}
1.364 + [$x@1$, $\dots$, $x@n$] & $x@1$\#$\cdots$\#$x@n$\#[] &
1.365 + \rm finite list \\{}
1.366 + [$x$:$xs$ . $P$] & filter(\%$x$.$P$,$xs$) & list comprehension\\
1.367 + \begin{tabular}{r@{}l}
1.368 + \idx{case} $e$ of&\ [] => $a$\\
1.369 + |&\ $x$\#$xs$ => $b$
1.370 + \end{tabular} & list_case($e$,$a$,\%$x~xs$.$b$)
1.371 + & case analysis
1.372 +\end{tabular}
1.373 +\end{center}
1.374 +\subcaption{Translations}
1.375
1.376 \begin{ttbox}
1.377 -\idx{map_def} map(f,xs) == list_rec(xs, Nil, \%x l r. Cons(f(x), r))
1.378 -\subcaption{Definition}
1.379 +\idx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1.380
1.381 -\idx{list_induct}
1.382 - [| P(Nil); !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l)
1.383 -
1.384 -\idx{Cons_not_Nil} ~ Cons(x,xs) = Nil
1.385 -\idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)
1.386 -
1.387 -\idx{list_rec_Nil} list_rec(Nil,c,h) = c
1.388 -\idx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))
1.389 -
1.390 -\idx{map_Nil} map(f,Nil) = Nil
1.391 -\idx{map_Cons} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))
1.392 +\idx{Cons_not_Nil} (x # xs) ~= []
1.393 +\idx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1.394 +\subcaption{Induction and freeness}
1.395 \end{ttbox}
1.396 \caption{The type of lists and its operations} \label{hol-list}
1.397 \end{figure}
1.398
1.399 +\begin{figure}
1.400 +\begin{ttbox}\makeatother
1.401 +list_rec([],c,h) = c list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
1.402 +list_case([],c,h) = c list_case(x # xs, c, h) = h(x, xs)
1.403 +map(f,[]) = [] map(f, x \# xs) = f(x) \# map(f,xs)
1.404 +null([]) = True null(x # xs) = False
1.405 +hd(x # xs) = x tl(x # xs) = xs
1.406 +ttl([]) = [] ttl(x # xs) = xs
1.407 +[] @ ys = ys (x # xs) \at ys = x # xs \at ys
1.408 +x mem [] = False x mem y # ys = if(y = x, True, x mem ys)
1.409 +filter(P, []) = [] filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
1.410 +list_all(P,[]) = True list_all(P, x # xs) = (P(x) & list_all(P, xs))
1.411 +\end{ttbox}
1.412 +\caption{Rewrite rules for lists} \label{hol-list-simps}
1.413 +\end{figure}
1.414
1.415 \subsection{The type constructor for lists, $\alpha\,list$}
1.416 -{\HOL}'s definition of lists is an example of an experimental method for
1.417 -handling recursive data types. The details need not concern us here; see
1.418 -the file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the
1.419 -basic list operations, with their types and properties. In particular,
1.420 +\HOL's definition of lists is an example of an experimental method for
1.421 +handling recursive data types. The details need not concern us here; see the
1.422 +file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the basic list
1.423 +operations, with their types and properties. In particular,
1.424 \ttindexbold{list_rec} is a primitive recursion operator for lists, in the
1.425 style of Martin-L\"of type theory. It is derived from well-founded
1.426 recursion, a general principle that can express arbitrary total recursive
1.427 -functions.
1.428 +functions. The basic rewrite rules shown in Fig.~\ref{hol-list-simps} are
1.429 +contained, together with additional useful lemmas, in the simpset {\tt
1.430 + list_ss}. Induction over the variable $xs$ in subgoal $i$ is performed by
1.431 +{\tt list_ind_tac "$xs$" $i$}.
1.432
1.433
1.434 \subsection{The type constructor for lazy lists, $\alpha\,llist$}
1.435 @@ -1109,7 +1173,7 @@
1.436
1.437
1.438 \section{Classical proof procedures} \label{hol-cla-prover}
1.439 -{\HOL} derives classical introduction rules for $\disj$ and~$\exists$, as
1.440 +\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1.441 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1.442 rule (Fig.~\ref{hol-lemmas2}).
1.443
1.444 @@ -1117,7 +1181,7 @@
1.445 \ttindexbold{Classical}. This structure is open, so {\ML} identifiers such
1.446 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
1.447
1.448 -{\HOL} defines the following classical rule sets:
1.449 +\HOL\ defines the following classical rule sets:
1.450 \begin{ttbox}
1.451 prop_cs : claset
1.452 HOL_cs : claset
1.453 @@ -1159,7 +1223,7 @@
1.454 theory~\cite{mw81}.
1.455
1.456 Directory {\tt ex} contains other examples and experimental proofs in
1.457 -{\HOL}. Here is an overview of the more interesting files.
1.458 +\HOL. Here is an overview of the more interesting files.
1.459 \begin{description}
1.460 \item[{\tt HOL/ex/meson.ML}]
1.461 contains an experimental implementation of the MESON proof procedure,
1.462 @@ -1195,7 +1259,7 @@
1.463
1.464
1.465 \section{Example: deriving the conjunction rules}
1.466 -{\HOL} comes with a body of derived rules, ranging from simple properties
1.467 +\HOL\ comes with a body of derived rules, ranging from simple properties
1.468 of the logical constants and set theory to well-founded recursion. Many of
1.469 them are worth studying.
1.470
1.471 @@ -1217,7 +1281,7 @@
1.472 {\out val prems = ["P [P]", "Q [Q]"] : thm list}
1.473 \end{ttbox}
1.474 The next step is to unfold the definition of conjunction. But
1.475 -\ttindex{and_def} uses {\HOL}'s internal equality, so
1.476 +\ttindex{and_def} uses \HOL's internal equality, so
1.477 \ttindex{rewrite_goals_tac} is unsuitable.
1.478 Instead, we perform substitution using the rule \ttindex{ssubst}:
1.479 \begin{ttbox}
1.480 @@ -1318,7 +1382,7 @@
1.481 Viewing types as sets, $\alpha\To bool$ represents the powerset
1.482 of~$\alpha$. This version states that for every function from $\alpha$ to
1.483 its powerset, some subset is outside its range.
1.484 -The Isabelle proof uses {\HOL}'s set theory, with the type $\alpha\,set$ and
1.485 +The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1.486 the operator \ttindex{range}. Since it avoids quantification, we may
1.487 inspect the subset found by the proof.
1.488 \begin{ttbox}
1.489 @@ -1384,7 +1448,7 @@
1.490 \end{ttbox}
1.491 How much creativity is required? As it happens, Isabelle can prove this
1.492 theorem automatically. The classical set \ttindex{set_cs} contains rules
1.493 -for most of the constructs of {\HOL}'s set theory. We augment it with
1.494 +for most of the constructs of \HOL's set theory. We augment it with
1.495 \ttindex{equalityCE} --- set equalities are not broken up by default ---
1.496 and apply best-first search. Depth-first search would diverge, but
1.497 best-first search successfully navigates through the large search space.