2 \chapter{Higher-Order Logic}
3 \index{higher-order logic|(}
4 \index{HOL system@{\sc hol} system}
6 The theory~\thydx{HOL} implements higher-order logic.
7 It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
8 based on Church's original paper~\cite{church40}. Andrews's
9 book~\cite{andrews86} is a full description of higher-order logic.
10 Experience with the {\sc hol} system has demonstrated that higher-order
11 logic is useful for hardware verification; beyond this, it is widely
12 applicable in many areas of mathematics. It is weaker than {\ZF} set
13 theory but for most applications this does not matter. If you prefer {\ML}
14 to Lisp, you will probably prefer \HOL\ to~{\ZF}.
16 Previous releases of Isabelle included a different version of~\HOL, with
17 explicit type inference rules~\cite{paulson-COLOG}. This version no longer
18 exists, but \thydx{ZF} supports a similar style of reasoning.
20 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
21 identifies object-level types with meta-level types, taking advantage of
22 Isabelle's built-in type checker. It identifies object-level functions
23 with meta-level functions, so it uses Isabelle's operations for abstraction
24 and application. There is no `apply' operator: function applications are
25 written as simply~$f(a)$ rather than $f{\tt`}a$.
27 These identifications allow Isabelle to support \HOL\ particularly nicely,
28 but they also mean that \HOL\ requires more sophistication from the user
29 --- in particular, an understanding of Isabelle's type system. Beginners
30 should work with {\tt show_types} set to {\tt true}. Gain experience by
31 working in first-order logic before attempting to use higher-order logic.
32 This chapter assumes familiarity with~{\FOL{}}.
38 \it name &\it meta-type & \it description \\
39 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
40 \cdx{not} & $bool\To bool$ & negation ($\neg$) \\
41 \cdx{True} & $bool$ & tautology ($\top$) \\
42 \cdx{False} & $bool$ & absurdity ($\bot$) \\
43 \cdx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
44 \cdx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
45 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
48 \subcaption{Constants}
51 \index{"@@{\tt\at} symbol}
52 \index{*"! symbol}\index{*"? symbol}
53 \index{*"?"! symbol}\index{*"E"X"! symbol}
54 \begin{tabular}{llrrr}
55 \it symbol &\it name &\it meta-type & \it description \\
56 \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ &
57 Hilbert description ($\epsilon$) \\
58 {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ &
59 universal quantifier ($\forall$) \\
60 {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ &
61 existential quantifier ($\exists$) \\
62 {\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ &
63 unique existence ($\exists!$)
70 \index{&@{\tt\&} symbol}
72 \index{*"-"-"> symbol}
74 \it symbol & \it meta-type & \it priority & \it description \\
75 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
76 Right 50 & composition ($\circ$) \\
77 \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
78 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
79 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
80 less than or equals ($\leq$)\\
81 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
82 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
83 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
87 \caption{Syntax of {\tt HOL}} \label{hol-constants}
95 \[\begin{array}{rclcl}
96 term & = & \hbox{expression of class~$term$} \\
97 & | & "\at~" id~id^* " . " formula \\
99 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term}
101 formula & = & \hbox{expression of type~$bool$} \\
102 & | & term " = " term \\
103 & | & term " \ttilde= " term \\
104 & | & term " < " term \\
105 & | & term " <= " term \\
106 & | & "\ttilde\ " formula \\
107 & | & formula " \& " formula \\
108 & | & formula " | " formula \\
109 & | & formula " --> " formula \\
110 & | & "!~~~" id~id^* " . " formula
111 & | & "ALL~" id~id^* " . " formula \\
112 & | & "?~~~" id~id^* " . " formula
113 & | & "EX~~" id~id^* " . " formula \\
114 & | & "?!~~" id~id^* " . " formula
115 & | & "EX!~" id~id^* " . " formula
118 \caption{Full grammar for \HOL} \label{hol-grammar}
123 The type class of higher-order terms is called~\cldx{term}. Type variables
124 range over this class by default. The equality symbol and quantifiers are
125 polymorphic over class {\tt term}.
127 Class \cldx{ord} consists of all ordered types; the relations $<$ and
128 $\leq$ are polymorphic over this class, as are the functions
129 \cdx{mono}, \cdx{min} and \cdx{max}. Three other
130 type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
131 overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
132 {\tt-} is overloaded for set difference and subtraction.
137 Figure~\ref{hol-constants} lists the constants (including infixes and
138 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
139 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
143 \HOL\ has no if-and-only-if connective; logical equivalence is expressed
144 using equality. But equality has a high priority, as befitting a
145 relation, while if-and-only-if typically has the lowest priority. Thus,
146 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
147 When using $=$ to mean logical equivalence, enclose both operands in
151 \subsection{Types}\label{HOL-types}
152 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
153 formulae are terms. The built-in type~\tydx{fun}, which constructs function
154 types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$
155 belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
158 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
159 unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
161 \index{type definitions}
162 Gordon's {\sc hol} system supports {\bf type definitions}. A type is
163 defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
164 bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$
165 specifies a non-empty subset of~$\sigma$, and the new type denotes this
166 subset. New function constants are generated to establish an isomorphism
167 between the new type and the subset. If type~$\sigma$ involves type
168 variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
169 a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
170 type. Melham~\cite{melham89} discusses type definitions at length, with
173 Isabelle does not support type definitions at present. Instead, they are
174 mimicked by explicit definitions of isomorphism functions. The definitions
175 should be supported by theorems of the form $\exists x::\sigma.P(x)$, but
176 Isabelle cannot enforce this.
180 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
181 satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote
182 something, a description is always meaningful, but we do not know its value
183 unless $P[x]$ defines it uniquely. We may write descriptions as
184 \cdx{Eps}($P$) or use the syntax
185 \hbox{\tt \at $x$.$P[x]$}.
187 Existential quantification is defined by
188 \[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
189 The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
190 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
191 quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
192 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
193 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
195 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
196 Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
197 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
198 existential quantifier must be followed by a space; thus {\tt?x} is an
199 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
200 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
201 available. Both notations are accepted for input. The {\ML} reference
202 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
203 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
204 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
206 All these binders have priority 10.
209 \subsection{The \sdx{let} and \sdx{case} constructions}
210 Local abbreviations can be introduced by a {\tt let} construct whose
211 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
212 the constant~\cdx{Let}. It can be expanded by rewriting with its
213 definition, \tdx{Let_def}.
215 \HOL\ also defines the basic syntax
216 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
217 as a uniform means of expressing {\tt case} constructs. Therefore {\tt
218 case} and \sdx{of} are reserved words. However, so far this is mere
219 syntax and has no logical meaning. By declaring translations, you can
220 cause instances of the {\tt case} construct to denote applications of
221 particular case operators. The patterns supplied for $c@1$,~\ldots,~$c@n$
222 distinguish among the different case operators. For an example, see the
223 case construct for lists on page~\pageref{hol-list} below.
227 \begin{ttbox}\makeatother
228 \tdx{refl} t = (t::'a)
229 \tdx{subst} [| s=t; P(s) |] ==> P(t::'a)
230 \tdx{ext} (!!x::'a. (f(x)::'b) = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
231 \tdx{impI} (P ==> Q) ==> P-->Q
232 \tdx{mp} [| P-->Q; P |] ==> Q
233 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
234 \tdx{selectI} P(x::'a) ==> P(@x.P(x))
235 \tdx{True_or_False} (P=True) | (P=False)
237 \caption{The {\tt HOL} rules} \label{hol-rules}
241 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
242 \begin{ttbox}\makeatother
243 \tdx{True_def} True == ((\%x::bool.x)=(\%x.x))
244 \tdx{All_def} All == (\%P. P = (\%x.True))
245 \tdx{Ex_def} Ex == (\%P. P(@x.P(x)))
246 \tdx{False_def} False == (!P.P)
247 \tdx{not_def} not == (\%P. P-->False)
248 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
249 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
250 \tdx{Ex1_def} Ex1 == (\%P. ? x. P(x) & (! y. P(y) --> y=x))
252 \tdx{Inv_def} Inv == (\%(f::'a=>'b) y. @x. f(x)=y)
253 \tdx{o_def} op o == (\%(f::'b=>'c) g (x::'a). f(g(x)))
254 \tdx{if_def} if == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
255 \tdx{Let_def} Let(s,f) == f(s)
257 \caption{The {\tt HOL} definitions} \label{hol-defs}
261 \section{Rules of inference}
262 Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
263 their~{\ML} names. Some of the rules deserve additional comments:
264 \begin{ttdescription}
265 \item[\tdx{ext}] expresses extensionality of functions.
266 \item[\tdx{iff}] asserts that logically equivalent formulae are
268 \item[\tdx{selectI}] gives the defining property of the Hilbert
269 $\epsilon$-operator. It is a form of the Axiom of Choice. The derived rule
270 \tdx{select_equality} (see below) is often easier to use.
271 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
272 fact, the $\epsilon$-operator already makes the logic classical, as
273 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
276 \HOL{} follows standard practice in higher-order logic: only a few
277 connectives are taken as primitive, with the remainder defined obscurely
278 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
279 corresponding definitions \cite[page~270]{mgordon-hol} using
280 object-equality~({\tt=}), which is possible because equality in
281 higher-order logic may equate formulae and even functions over formulae.
282 But theory~\HOL{}, like all other Isabelle theories, uses
283 meta-equality~({\tt==}) for definitions.
285 Some of the rules mention type variables; for
286 example, {\tt refl} mentions the type variable~{\tt'a}. This allows you to
287 instantiate type variables explicitly by calling {\tt res_inst_tac}. By
288 default, explicit type variables have class \cldx{term}.
290 Include type constraints whenever you state a polymorphic goal. Type
291 inference may otherwise make the goal more polymorphic than you intended,
292 with confusing results.
295 If resolution fails for no obvious reason, try setting
296 \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
297 terms. Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
298 Isabelle to display sorts.
300 \index{unification!incompleteness of}
301 Where function types are involved, Isabelle's unification code does not
302 guarantee to find instantiations for type variables automatically. Be
303 prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
304 possibly instantiating type variables. Setting
305 \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
306 omitted search paths during unification.\index{tracing!of unification}
312 \tdx{sym} s=t ==> t=s
313 \tdx{trans} [| r=s; s=t |] ==> r=t
314 \tdx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
315 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
316 \tdx{arg_cong} x=y ==> f(x)=f(y)
317 \tdx{fun_cong} f=g ==> f(x)=g(x)
318 \subcaption{Equality}
321 \tdx{FalseE} False ==> P
323 \tdx{conjI} [| P; Q |] ==> P&Q
324 \tdx{conjunct1} [| P&Q |] ==> P
325 \tdx{conjunct2} [| P&Q |] ==> Q
326 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
328 \tdx{disjI1} P ==> P|Q
329 \tdx{disjI2} Q ==> P|Q
330 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
332 \tdx{notI} (P ==> False) ==> ~ P
333 \tdx{notE} [| ~ P; P |] ==> R
334 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
335 \subcaption{Propositional logic}
337 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
338 \tdx{iffD1} [| P=Q; P |] ==> Q
339 \tdx{iffD2} [| P=Q; Q |] ==> P
340 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
342 \tdx{eqTrueI} P ==> P=True
343 \tdx{eqTrueE} P=True ==> P
344 \subcaption{Logical equivalence}
347 \caption{Derived rules for \HOL} \label{hol-lemmas1}
352 \begin{ttbox}\makeatother
353 \tdx{allI} (!!x::'a. P(x)) ==> !x. P(x)
354 \tdx{spec} !x::'a.P(x) ==> P(x)
355 \tdx{allE} [| !x.P(x); P(x) ==> R |] ==> R
356 \tdx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
358 \tdx{exI} P(x) ==> ? x::'a.P(x)
359 \tdx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
361 \tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
362 \tdx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
365 \tdx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
366 \subcaption{Quantifiers and descriptions}
368 \tdx{ccontr} (~P ==> False) ==> P
369 \tdx{classical} (~P ==> P) ==> P
370 \tdx{excluded_middle} ~P | P
372 \tdx{disjCI} (~Q ==> P) ==> P|Q
373 \tdx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
374 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
375 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
376 \tdx{notnotD} ~~P ==> P
377 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
378 \subcaption{Classical logic}
380 \tdx{if_True} if(True,x,y) = x
381 \tdx{if_False} if(False,x,y) = y
382 \tdx{if_P} P ==> if(P,x,y) = x
383 \tdx{if_not_P} ~ P ==> if(P,x,y) = y
384 \tdx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
385 \subcaption{Conditionals}
387 \caption{More derived rules} \label{hol-lemmas2}
391 Some derived rules are shown in Figures~\ref{hol-lemmas1}
392 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
393 for the logical connectives, as well as sequent-style elimination rules for
394 conjunctions, implications, and universal quantifiers.
396 Note the equality rules: \tdx{ssubst} performs substitution in
397 backward proofs, while \tdx{box_equals} supports reasoning by
398 simplifying both sides of an equation.
404 \it name &\it meta-type & \it description \\
405 \index{{}@\verb'{}' symbol}
406 \verb|{}| & $\alpha\,set$ & the empty set \\
407 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
408 & insertion of element \\
409 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
411 \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$
413 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
414 & intersection over a set\\
415 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
417 \cdx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
418 &set of sets intersection \\
419 \cdx{Union} & $((\alpha\,set)set)\To\alpha\,set$
420 &set of sets union \\
421 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
422 & range of a function \\[1ex]
423 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
424 & bounded quantifiers \\
425 \cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
427 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
428 & injective/surjective \\
429 \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
430 & injective over subset
433 \subcaption{Constants}
436 \begin{tabular}{llrrr}
437 \it symbol &\it name &\it meta-type & \it priority & \it description \\
438 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
439 intersection over a type\\
440 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
450 \begin{tabular}{rrrr}
451 \it symbol & \it meta-type & \it priority & \it description \\
452 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
454 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
455 & Left 70 & intersection ($\inter$) \\
456 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
457 & Left 65 & union ($\union$) \\
458 \tt: & $[\alpha ,\alpha\,set]\To bool$
459 & Left 50 & membership ($\in$) \\
460 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
461 & Left 50 & subset ($\subseteq$)
465 \caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}
470 \begin{center} \tt\frenchspacing
473 \it external & \it internal & \it description \\
474 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
475 \{$a@1$, $\ldots$\} & insert($a@1$, $\ldots$\{\}) & \rm finite set \\
476 \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
478 \sdx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
480 \sdx{UN}{\tt\ } $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
482 \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ &
483 Ball($A$,$\lambda x.P[x]$) &
484 \rm bounded $\forall$ \\
485 \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ &
486 Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$
489 \subcaption{Translations}
492 \[\begin{array}{rclcl}
493 term & = & \hbox{other terms\ldots} \\
495 & | & "\{ " term\; ("," term)^* " \}" \\
496 & | & "\{ " id " . " formula " \}" \\
497 & | & term " `` " term \\
498 & | & term " Int " term \\
499 & | & term " Un " term \\
500 & | & "INT~~" id ":" term " . " term \\
501 & | & "UN~~~" id ":" term " . " term \\
502 & | & "INT~~" id~id^* " . " term \\
503 & | & "UN~~~" id~id^* " . " term \\[2ex]
504 formula & = & \hbox{other formulae\ldots} \\
505 & | & term " : " term \\
506 & | & term " \ttilde: " term \\
507 & | & term " <= " term \\
508 & | & "!~" id ":" term " . " formula
509 & | & "ALL " id ":" term " . " formula \\
510 & | & "?~" id ":" term " . " formula
511 & | & "EX~~" id ":" term " . " formula
514 \subcaption{Full Grammar}
515 \caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
519 \section{A formulation of set theory}
520 Historically, higher-order logic gives a foundation for Russell and
521 Whitehead's theory of classes. Let us use modern terminology and call them
522 {\bf sets}, but note that these sets are distinct from those of {\ZF} set
523 theory, and behave more like {\ZF} classes.
526 Sets are given by predicates over some type~$\sigma$. Types serve to
527 define universes for sets, but type checking is still significant.
529 There is a universal set (for each type). Thus, sets have complements, and
530 may be defined by absolute comprehension.
532 Although sets may contain other sets as elements, the containing set must
533 have a more complex type.
535 Finite unions and intersections have the same behaviour in \HOL\ as they
536 do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
537 denoting the universal set for the given type.
540 \subsection{Syntax of set theory}\index{*set type}
541 \HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
542 essentially the same as $\alpha\To bool$. The new type is defined for
543 clarity and to avoid complications involving function types in unification.
544 Since Isabelle does not support type definitions (as mentioned in
545 \S\ref{HOL-types}), the isomorphisms between the two types are declared
546 explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
547 $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
550 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
551 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
552 constructs. Infix operators include union and intersection ($A\union B$
553 and $A\inter B$), the subset and membership relations, and the image
554 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
557 The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
558 obvious manner using~{\tt insert} and~$\{\}$:
560 \{a@1, \ldots, a@n\} & \equiv &
561 {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
564 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
565 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
566 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
567 x.P[x])$. It defines sets by absolute comprehension, which is impossible
568 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
570 The set theory defines two {\bf bounded quantifiers}:
572 \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
573 \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
575 The constants~\cdx{Ball} and~\cdx{Bex} are defined
576 accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
577 write\index{*"! symbol}\index{*"? symbol}
578 \index{*ALL symbol}\index{*EX symbol}
580 \hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's
581 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
582 for input. As with the primitive quantifiers, the {\ML} reference
583 \ttindex{HOL_quantifiers} specifies which notation to use for output.
585 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
586 $\bigcap@{x\in A}B[x]$, are written
587 \sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
588 \sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
590 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
591 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
592 \sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous
593 union and intersection operators when $A$ is the universal set.
595 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
596 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
600 \begin{figure} \underscoreon
602 \tdx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
603 \tdx{Collect_mem_eq} \{x.x:A\} = A
605 \tdx{empty_def} \{\} == \{x.x=False\}
606 \tdx{insert_def} insert(a,B) == \{x.x=a\} Un B
607 \tdx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
608 \tdx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
609 \tdx{subset_def} A <= B == ! x:A. x:B
610 \tdx{Un_def} A Un B == \{x.x:A | x:B\}
611 \tdx{Int_def} A Int B == \{x.x:A & x:B\}
612 \tdx{set_diff_def} A - B == \{x.x:A & x~:B\}
613 \tdx{Compl_def} Compl(A) == \{x. ~ x:A\}
614 \tdx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
615 \tdx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
616 \tdx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
617 \tdx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
618 \tdx{Inter_def} Inter(S) == (INT x:S. x)
619 \tdx{Union_def} Union(S) == (UN x:S. x)
620 \tdx{image_def} f``A == \{y. ? x:A. y=f(x)\}
621 \tdx{range_def} range(f) == \{y. ? x. y=f(x)\}
622 \tdx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
623 \tdx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
624 \tdx{surj_def} surj(f) == ! y. ? x. y=f(x)
625 \tdx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
627 \caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
631 \begin{figure} \underscoreon
633 \tdx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
634 \tdx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
635 \tdx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
637 \tdx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
638 \tdx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
639 \tdx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
641 \tdx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
642 \tdx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
643 \tdx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
644 \subcaption{Comprehension and Bounded quantifiers}
646 \tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
647 \tdx{subsetD} [| A <= B; c:A |] ==> c:B
648 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
650 \tdx{subset_refl} A <= A
651 \tdx{subset_antisym} [| A <= B; B <= A |] ==> A = B
652 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
654 \tdx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
655 \tdx{equalityD1} A = B ==> A<=B
656 \tdx{equalityD2} A = B ==> B<=A
657 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
659 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
660 [| ~ c:A; ~ c:B |] ==> P
662 \subcaption{The subset and equality relations}
664 \caption{Derived rules for set theory} \label{hol-set1}
668 \begin{figure} \underscoreon
670 \tdx{emptyE} a : \{\} ==> P
672 \tdx{insertI1} a : insert(a,B)
673 \tdx{insertI2} a : B ==> a : insert(b,B)
674 \tdx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
676 \tdx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
677 \tdx{ComplD} [| c : Compl(A) |] ==> ~ c:A
679 \tdx{UnI1} c:A ==> c : A Un B
680 \tdx{UnI2} c:B ==> c : A Un B
681 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
682 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
684 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B
685 \tdx{IntD1} c : A Int B ==> c:A
686 \tdx{IntD2} c : A Int B ==> c:B
687 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
689 \tdx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
690 \tdx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
692 \tdx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
693 \tdx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
694 \tdx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
696 \tdx{UnionI} [| X:C; A:X |] ==> A : Union(C)
697 \tdx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
699 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
700 \tdx{InterD} [| A : Inter(C); X:C |] ==> A:X
701 \tdx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
703 \caption{Further derived rules for set theory} \label{hol-set2}
707 \subsection{Axioms and rules of set theory}
708 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
709 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
710 that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms. Of
711 course, \hbox{\tt op :} also serves as the membership relation.
713 All the other axioms are definitions. They include the empty set, bounded
714 quantifiers, unions, intersections, complements and the subset relation.
715 They also include straightforward properties of functions: image~({\tt``}) and
716 {\tt range}, and predicates concerning monotonicity, injectiveness and
719 The predicate \cdx{inj_onto} is used for simulating type definitions.
720 The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
721 set~$A$, which specifies a subset of its domain type. In a type
722 definition, $f$ is the abstraction function and $A$ is the set of valid
723 representations; we should not expect $f$ to be injective outside of~$A$.
725 \begin{figure} \underscoreon
727 \tdx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
728 \tdx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
731 % [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
733 \tdx{imageI} [| x:A |] ==> f(x) : f``A
734 \tdx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
736 \tdx{rangeI} f(x) : range(f)
737 \tdx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
739 \tdx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
740 \tdx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
742 \tdx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
743 \tdx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
744 \tdx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
746 \tdx{inj_ontoI} (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
747 \tdx{inj_ontoD} [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
749 \tdx{inj_onto_inverseI}
750 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
751 \tdx{inj_onto_contraD}
752 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
754 \caption{Derived rules involving functions} \label{hol-fun}
758 \begin{figure} \underscoreon
760 \tdx{Union_upper} B:A ==> B <= Union(A)
761 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
763 \tdx{Inter_lower} B:A ==> Inter(A) <= B
764 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
766 \tdx{Un_upper1} A <= A Un B
767 \tdx{Un_upper2} B <= A Un B
768 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
770 \tdx{Int_lower1} A Int B <= A
771 \tdx{Int_lower2} A Int B <= B
772 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
774 \caption{Derived rules involving subsets} \label{hol-subset}
778 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
780 \tdx{Int_absorb} A Int A = A
781 \tdx{Int_commute} A Int B = B Int A
782 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
783 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
785 \tdx{Un_absorb} A Un A = A
786 \tdx{Un_commute} A Un B = B Un A
787 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
788 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
790 \tdx{Compl_disjoint} A Int Compl(A) = \{x.False\}
791 \tdx{Compl_partition} A Un Compl(A) = \{x.True\}
792 \tdx{double_complement} Compl(Compl(A)) = A
793 \tdx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
794 \tdx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
796 \tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
797 \tdx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
798 \tdx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
800 \tdx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
801 \tdx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
802 \tdx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
804 \caption{Set equalities} \label{hol-equalities}
808 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
809 obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
810 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
811 are designed for classical reasoning; the rules \tdx{subsetD},
812 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
813 strictly necessary but yield more natural proofs. Similarly,
814 \tdx{equalityCE} supports classical reasoning about extensionality,
815 after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for
816 proofs pertaining to set theory.
818 Figure~\ref{hol-fun} presents derived inference rules involving functions.
819 They also include rules for \cdx{Inv}, which is defined in theory~{\tt
820 HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
821 inverse of~$f$. They also include natural deduction rules for the image
822 and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
823 Reasoning about function composition (the operator~\sdx{o}) and the
824 predicate~\cdx{surj} is done simply by expanding the definitions. See
825 the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
827 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
828 Unions form least upper bounds; non-empty intersections form greatest lower
829 bounds. Reasoning directly about subsets often yields clearer proofs than
830 reasoning about the membership relation. See the file {\tt HOL/subset.ML}.
832 Figure~\ref{hol-equalities} presents many common set equalities. They
833 include commutative, associative and distributive laws involving unions,
834 intersections and complements. The proofs are mostly trivial, using the
835 classical reasoner; see file {\tt HOL/equalities.ML}.
840 \it symbol & \it meta-type & & \it description \\
841 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
842 & & ordered pairs $\langle a,b\rangle$ \\
843 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
844 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
845 \cdx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
846 & & generalized projection\\
848 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
849 & general sum of sets
851 \begin{ttbox}\makeatletter
852 \tdx{fst_def} fst(p) == @a. ? b. p = <a,b>
853 \tdx{snd_def} snd(p) == @b. ? a. p = <a,b>
854 \tdx{split_def} split(p,c) == c(fst(p),snd(p))
855 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
858 \tdx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
859 \tdx{fst_conv} fst(<a,b>) = a
860 \tdx{snd_conv} snd(<a,b>) = b
861 \tdx{split} split(<a,b>, c) = c(a,b)
863 \tdx{surjective_pairing} p = <fst(p),snd(p)>
865 \tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
867 \tdx{SigmaE} [| c: Sigma(A,B);
868 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
870 \caption{Type $\alpha\times\beta$}\label{hol-prod}
876 \it symbol & \it meta-type & & \it description \\
877 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
878 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
879 \cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
882 \begin{ttbox}\makeatletter
883 \tdx{sum_case_def} sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
884 (!y. p=Inr(y) --> z=g(y)))
886 \tdx{Inl_not_Inr} ~ Inl(a)=Inr(b)
888 \tdx{inj_Inl} inj(Inl)
889 \tdx{inj_Inr} inj(Inr)
891 \tdx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
893 \tdx{sum_case_Inl} sum_case(Inl(x), f, g) = f(x)
894 \tdx{sum_case_Inr} sum_case(Inr(x), f, g) = g(x)
896 \tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)
898 \caption{Type $\alpha+\beta$}\label{hol-sum}
902 \section{Generic packages and classical reasoning}
903 \HOL\ instantiates most of Isabelle's generic packages;
904 see {\tt HOL/ROOT.ML} for details.
907 Because it includes a general substitution rule, \HOL\ instantiates the
908 tactic {\tt hyp_subst_tac}, which substitutes for an equality
909 throughout a subgoal and its hypotheses.
911 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
912 simplification set for higher-order logic. Equality~($=$), which also
913 expresses logical equivalence, may be used for rewriting. See the file
914 {\tt HOL/simpdata.ML} for a complete listing of the simplification
917 It instantiates the classical reasoner, as described below.
919 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
920 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
921 rule; recall Fig.\ts\ref{hol-lemmas2} above.
923 The classical reasoner is set up as the structure
924 {\tt Classical}. This structure is open, so {\ML} identifiers such
925 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
926 \HOL\ defines the following classical rule sets:
933 \begin{ttdescription}
934 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
935 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
936 along with the rule~{\tt refl}.
938 \item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
939 {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
940 and~{\tt exI}, as well as rules for unique existence. Search using
941 this classical set is incomplete: quantified formulae are used at most
944 \item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
945 {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
946 and~\tdx{exCI}, as well as rules for unique existence. Search using
947 this is complete --- quantified formulae may be duplicated --- but
948 frequently fails to terminate. It is generally unsuitable for
951 \item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
952 quantifiers, subsets, comprehensions, unions and intersections,
953 complements, finite sets, images and ranges.
956 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
957 {Chap.\ts\ref{chap:classical}}
958 for more discussion of classical proof methods.
962 The basic higher-order logic is augmented with a tremendous amount of
963 material, including support for recursive function and type definitions. A
964 detailed discussion appears elsewhere~\cite{paulson-coind}. The simpler
965 definitions are the same as those used the {\sc hol} system, but my
966 treatment of recursive types differs from Melham's~\cite{melham89}. The
967 present section describes product, sum, natural number and list types.
969 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
970 Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
971 the ordered pair syntax {\tt<$a$,$b$>}. Theory \thydx{Sum} defines the
972 sum type $\alpha+\beta$. These use fairly standard constructions; see
973 Figs.\ts\ref{hol-prod} and~\ref{hol-sum}. Because Isabelle does not
974 support abstract type definitions, the isomorphisms between these types and
975 their representations are made explicitly.
977 Most of the definitions are suppressed, but observe that the projections
978 and conditionals are defined as descriptions. Their properties are easily
979 proved using \tdx{select_equality}.
989 \it symbol & \it meta-type & \it priority & \it description \\
990 \cdx{0} & $nat$ & & zero \\
991 \cdx{Suc} & $nat \To nat$ & & successor function\\
992 \cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
994 \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
995 & & primitive recursor\\
996 \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
997 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
998 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
999 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
1000 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
1001 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1003 \subcaption{Constants and infixes}
1005 \begin{ttbox}\makeatother
1006 \tdx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
1007 (!x. n=Suc(x) --> z=f(x)))
1008 \tdx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
1009 \tdx{less_def} m<n == <m,n>:pred_nat^+
1010 \tdx{nat_rec_def} nat_rec(n,c,d) ==
1011 wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
1013 \tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
1014 \tdx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
1015 \tdx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
1016 \tdx{mod_def} m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
1017 \tdx{quo_def} m div n == wfrec(trancl(pred_nat),
1018 m, \%j f. if(j<n,0,Suc(f(j-n))))
1019 \subcaption{Definitions}
1021 \caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
1025 \begin{figure} \underscoreon
1027 \tdx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1029 \tdx{Suc_not_Zero} Suc(m) ~= 0
1030 \tdx{inj_Suc} inj(Suc)
1031 \tdx{n_not_Suc_n} n~=Suc(n)
1032 \subcaption{Basic properties}
1034 \tdx{pred_natI} <n, Suc(n)> : pred_nat
1036 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
1038 \tdx{nat_case_0} nat_case(0, a, f) = a
1039 \tdx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
1041 \tdx{wf_pred_nat} wf(pred_nat)
1042 \tdx{nat_rec_0} nat_rec(0,c,h) = c
1043 \tdx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1044 \subcaption{Case analysis and primitive recursion}
1046 \tdx{less_trans} [| i<j; j<k |] ==> i<k
1047 \tdx{lessI} n < Suc(n)
1048 \tdx{zero_less_Suc} 0 < Suc(n)
1050 \tdx{less_not_sym} n<m --> ~ m<n
1051 \tdx{less_not_refl} ~ n<n
1052 \tdx{not_less0} ~ n<0
1054 \tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1055 \tdx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1057 \tdx{less_linear} m<n | m=n | n<m
1058 \subcaption{The less-than relation}
1060 \caption{Derived rules for {\tt nat}} \label{hol-nat2}
1064 \subsection{The type of natural numbers, {\tt nat}}
1065 The theory \thydx{Nat} defines the natural numbers in a roundabout but
1066 traditional way. The axiom of infinity postulates an type~\tydx{ind} of
1067 individuals, which is non-empty and closed under an injective operation.
1068 The natural numbers are inductively generated by choosing an arbitrary
1069 individual for~0 and using the injective operation to take successors. As
1070 usual, the isomorphisms between~\tydx{nat} and its representation are made
1073 The definition makes use of a least fixed point operator \cdx{lfp},
1074 defined using the Knaster-Tarski theorem. This is used to define the
1075 operator \cdx{trancl}, for taking the transitive closure of a relation.
1076 Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
1077 along arbitrary well-founded relations. The corresponding theories are
1078 called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
1079 similar constructions in the context of set theory~\cite{paulson-set-II}.
1081 Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
1082 overloads $<$ and $\leq$ on the natural numbers. As of this writing,
1083 Isabelle provides no means of verifying that such overloading is sensible;
1084 there is no means of specifying the operators' properties and verifying
1085 that instances of the operators satisfy those properties. To be safe, the
1086 \HOL\ theory includes no polymorphic axioms asserting general properties of
1089 Theory \thydx{Arith} develops arithmetic on the natural numbers. It
1090 defines addition, multiplication, subtraction, division, and remainder.
1091 Many of their properties are proved: commutative, associative and
1092 distributive laws, identity and cancellation laws, etc. The most
1093 interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
1094 Division and remainder are defined by repeated subtraction, which requires
1095 well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
1098 The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1099 Recursion along this relation resembles primitive recursion, but is
1100 stronger because we are in higher-order logic; using primitive recursion to
1101 define a higher-order function, we can easily Ackermann's function, which
1102 is not primitive recursive \cite[page~104]{thompson91}.
1103 The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1104 natural numbers are most easily expressed using recursion along~$<$.
1106 The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
1107 variable~$n$ in subgoal~$i$.
1110 \index{#@{\tt\#} symbol}
1111 \index{"@@{\tt\at} symbol}
1113 \it symbol & \it meta-type & \it priority & \it description \\
1114 \cdx{Nil} & $\alpha list$ & & empty list\\
1115 \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
1117 \cdx{null} & $\alpha list \To bool$ & & emptiness test\\
1118 \cdx{hd} & $\alpha list \To \alpha$ & & head \\
1119 \cdx{tl} & $\alpha list \To \alpha list$ & & tail \\
1120 \cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\
1121 \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1122 \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
1123 \cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1124 & & mapping functional\\
1125 \cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1126 & & filter functional\\
1127 \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1128 & & forall functional\\
1129 \cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1130 \beta]\To\beta] \To \beta$
1133 \subcaption{Constants and infixes}
1135 \begin{center} \tt\frenchspacing
1136 \begin{tabular}{rrr}
1137 \it external & \it internal & \it description \\{}
1138 \sdx{[]} & Nil & \rm empty list \\{}
1139 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1140 \rm finite list \\{}
1141 [$x$:$l$. $P$] & filter($\lambda x{.}P$, $l$) &
1142 \rm list comprehension
1145 \subcaption{Translations}
1148 \tdx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1150 \tdx{Cons_not_Nil} (x # xs) ~= []
1151 \tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1152 \subcaption{Induction and freeness}
1154 \caption{The theory \thydx{List}} \label{hol-list}
1158 \begin{ttbox}\makeatother
1159 \tdx{list_rec_Nil} list_rec([],c,h) = c
1160 \tdx{list_rec_Cons} list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
1162 \tdx{list_case_Nil} list_case([],c,h) = c
1163 \tdx{list_case_Cons} list_case(x # xs, c, h) = h(x, xs)
1165 \tdx{map_Nil} map(f,[]) = []
1166 \tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs)
1168 \tdx{null_Nil} null([]) = True
1169 \tdx{null_Cons} null(x # xs) = False
1171 \tdx{hd_Cons} hd(x # xs) = x
1172 \tdx{tl_Cons} tl(x # xs) = xs
1174 \tdx{ttl_Nil} ttl([]) = []
1175 \tdx{ttl_Cons} ttl(x # xs) = xs
1177 \tdx{append_Nil} [] @ ys = ys
1178 \tdx{append_Cons} (x # xs) \at ys = x # xs \at ys
1180 \tdx{mem_Nil} x mem [] = False
1181 \tdx{mem_Cons} x mem y # ys = if(y = x, True, x mem ys)
1183 \tdx{filter_Nil} filter(P, []) = []
1184 \tdx{filter_Cons} filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
1186 \tdx{list_all_Nil} list_all(P,[]) = True
1187 \tdx{list_all_Cons} list_all(P, x # xs) = (P(x) & list_all(P, xs))
1189 \caption{Rewrite rules for lists} \label{hol-list-simps}
1193 \subsection{The type constructor for lists, {\tt list}}
1196 \HOL's definition of lists is an example of an experimental method for
1197 handling recursive data types. Figure~\ref{hol-list} presents the theory
1198 \thydx{List}: the basic list operations with their types and properties.
1200 The \sdx{case} construct is defined by the following translation:
1203 \begin{array}{r@{\;}l@{}l}
1204 "case " e " of" & "[]" & " => " a\\
1205 "|" & x"\#"xs & " => " b
1208 "list_case"(e, a, \lambda x\;xs.b)
1210 The theory includes \cdx{list_rec}, a primitive recursion operator
1211 for lists. It is derived from well-founded recursion, a general principle
1212 that can express arbitrary total recursive functions.
1214 The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
1215 the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
1217 The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
1218 variable~$xs$ in subgoal~$i$.
1221 \subsection{The type constructor for lazy lists, {\tt llist}}
1224 The definition of lazy lists demonstrates methods for handling infinite
1225 data structures and coinduction in higher-order logic. Theory
1226 \thydx{LList} defines an operator for corecursion on lazy lists, which is
1227 used to define a few simple functions such as map and append. Corecursion
1228 cannot easily define operations such as filter, which can compute
1229 indefinitely before yielding the next element (if any!) of the lazy list.
1230 A coinduction principle is defined for proving equations on lazy lists.
1232 I have written a paper discussing the treatment of lazy lists; it also
1233 covers finite lists~\cite{paulson-coind}.
1236 \section{The examples directories}
1237 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
1238 substitutions and unifiers. It is based on Paulson's previous
1239 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1242 Directory {\tt HOL/ex} contains other examples and experimental proofs in
1243 {\HOL}. Here is an overview of the more interesting files.
1244 \begin{ttdescription}
1245 \item[HOL/ex/cla.ML] demonstrates the classical reasoner on over sixty
1246 predicate calculus theorems, ranging from simple tautologies to
1247 moderately difficult problems involving equality and quantifiers.
1249 \item[HOL/ex/meson.ML] contains an experimental implementation of the {\sc
1250 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1251 much more powerful than Isabelle's classical reasoner. But it is less
1252 useful in practice because it works only for pure logic; it does not
1253 accept derived rules for the set theory primitives, for example.
1255 \item[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof
1256 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1258 \item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in
1259 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1261 \item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
1262 proofs about insertion sort and quick sort.
1264 \item[HOL/ex/PL.ML] proves the soundness and completeness of classical
1265 propositional logic, given a truth table semantics. The only connective
1266 is $\imp$. A Hilbert-style axiom system is specified, and its set of
1267 theorems defined inductively. A similar proof in \ZF{} is described
1268 elsewhere~\cite{paulson-set-II}.
1270 \item[HOL/ex/Term.ML]
1271 contains proofs about an experimental recursive type definition;
1272 the recursion goes through the type constructor~\tydx{list}.
1274 \item[HOL/ex/Simult.ML] defines primitives for solving mutually recursive
1275 equations over sets. It constructs sets of trees and forests as an
1276 example, including induction and recursion rules that handle the mutual
1279 \item[HOL/ex/MT.ML] contains Jacob Frost's formalization~\cite{frost93} of
1280 Milner and Tofte's coinduction example~\cite{milner-coind}. This
1281 substantial proof concerns the soundness of a type system for a simple
1282 functional language. The semantics of recursion is given by a cyclic
1283 environment, which makes a coinductive argument appropriate.
1288 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
1289 Cantor's Theorem states that every set has more subsets than it has
1290 elements. It has become a favourite example in higher-order logic since
1291 it is so easily expressed:
1292 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1293 \forall x::\alpha. f(x) \not= S
1296 Viewing types as sets, $\alpha\To bool$ represents the powerset
1297 of~$\alpha$. This version states that for every function from $\alpha$ to
1298 its powerset, some subset is outside its range.
1300 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1301 the operator \cdx{range}. The set~$S$ is given as an unknown instead of a
1302 quantified variable so that we may inspect the subset found by the proof.
1304 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1306 {\out ~ ?S : range(f)}
1307 {\out 1. ~ ?S : range(f)}
1309 The first two steps are routine. The rule \tdx{rangeE} replaces
1310 $\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
1312 by (resolve_tac [notI] 1);
1314 {\out ~ ?S : range(f)}
1315 {\out 1. ?S : range(f) ==> False}
1317 by (eresolve_tac [rangeE] 1);
1319 {\out ~ ?S : range(f)}
1320 {\out 1. !!x. ?S = f(x) ==> False}
1322 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1323 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1326 by (eresolve_tac [equalityCE] 1);
1328 {\out ~ ?S : range(f)}
1329 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1330 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1332 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
1333 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1334 $\Var{P}(\Var{c})$. Destruct-resolution using \tdx{CollectD}
1335 instantiates~$\Var{S}$ and creates the new assumption.
1337 by (dresolve_tac [CollectD] 1);
1339 {\out ~ \{x. ?P7(x)\} : range(f)}
1340 {\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
1341 {\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
1343 Forcing a contradiction between the two assumptions of subgoal~1 completes
1344 the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, which
1345 is the standard diagonal construction.
1349 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1350 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1352 The rest should be easy. To apply \tdx{CollectI} to the negated
1353 assumption, we employ \ttindex{swap_res_tac}:
1355 by (swap_res_tac [CollectI] 1);
1357 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1358 {\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
1362 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1365 How much creativity is required? As it happens, Isabelle can prove this
1366 theorem automatically. The classical set \ttindex{set_cs} contains rules
1367 for most of the constructs of \HOL's set theory. We must augment it with
1368 \tdx{equalityCE} to break up set equalities, and then apply best-first
1369 search. Depth-first search would diverge, but best-first search
1370 successfully navigates through the large search space.
1371 \index{search!best-first}
1375 {\out ~ ?S : range(f)}
1376 {\out 1. ~ ?S : range(f)}
1378 by (best_tac (set_cs addSEs [equalityCE]) 1);
1380 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1384 \index{higher-order logic|)}