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_trans} [| A<=B; B<=C |] ==> A<=C
653 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B
654 \tdx{equalityD1} A = B ==> A<=B
655 \tdx{equalityD2} A = B ==> B<=A
656 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
658 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
659 [| ~ c:A; ~ c:B |] ==> P
661 \subcaption{The subset and equality relations}
663 \caption{Derived rules for set theory} \label{hol-set1}
667 \begin{figure} \underscoreon
669 \tdx{emptyE} a : \{\} ==> P
671 \tdx{insertI1} a : insert(a,B)
672 \tdx{insertI2} a : B ==> a : insert(b,B)
673 \tdx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
675 \tdx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
676 \tdx{ComplD} [| c : Compl(A) |] ==> ~ c:A
678 \tdx{UnI1} c:A ==> c : A Un B
679 \tdx{UnI2} c:B ==> c : A Un B
680 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
681 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
683 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B
684 \tdx{IntD1} c : A Int B ==> c:A
685 \tdx{IntD2} c : A Int B ==> c:B
686 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
688 \tdx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
689 \tdx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
691 \tdx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
692 \tdx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
693 \tdx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
695 \tdx{UnionI} [| X:C; A:X |] ==> A : Union(C)
696 \tdx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
698 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
699 \tdx{InterD} [| A : Inter(C); X:C |] ==> A:X
700 \tdx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
702 \caption{Further derived rules for set theory} \label{hol-set2}
706 \subsection{Axioms and rules of set theory}
707 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
708 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
709 that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms. Of
710 course, \hbox{\tt op :} also serves as the membership relation.
712 All the other axioms are definitions. They include the empty set, bounded
713 quantifiers, unions, intersections, complements and the subset relation.
714 They also include straightforward properties of functions: image~({\tt``}) and
715 {\tt range}, and predicates concerning monotonicity, injectiveness and
718 The predicate \cdx{inj_onto} is used for simulating type definitions.
719 The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
720 set~$A$, which specifies a subset of its domain type. In a type
721 definition, $f$ is the abstraction function and $A$ is the set of valid
722 representations; we should not expect $f$ to be injective outside of~$A$.
724 \begin{figure} \underscoreon
726 \tdx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
727 \tdx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
730 % [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
732 \tdx{imageI} [| x:A |] ==> f(x) : f``A
733 \tdx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
735 \tdx{rangeI} f(x) : range(f)
736 \tdx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
738 \tdx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
739 \tdx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
741 \tdx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
742 \tdx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
743 \tdx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
745 \tdx{inj_ontoI} (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
746 \tdx{inj_ontoD} [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
748 \tdx{inj_onto_inverseI}
749 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
750 \tdx{inj_onto_contraD}
751 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
753 \caption{Derived rules involving functions} \label{hol-fun}
757 \begin{figure} \underscoreon
759 \tdx{Union_upper} B:A ==> B <= Union(A)
760 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
762 \tdx{Inter_lower} B:A ==> Inter(A) <= B
763 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
765 \tdx{Un_upper1} A <= A Un B
766 \tdx{Un_upper2} B <= A Un B
767 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
769 \tdx{Int_lower1} A Int B <= A
770 \tdx{Int_lower2} A Int B <= B
771 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
773 \caption{Derived rules involving subsets} \label{hol-subset}
777 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
779 \tdx{Int_absorb} A Int A = A
780 \tdx{Int_commute} A Int B = B Int A
781 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
782 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
784 \tdx{Un_absorb} A Un A = A
785 \tdx{Un_commute} A Un B = B Un A
786 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
787 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
789 \tdx{Compl_disjoint} A Int Compl(A) = \{x.False\}
790 \tdx{Compl_partition} A Un Compl(A) = \{x.True\}
791 \tdx{double_complement} Compl(Compl(A)) = A
792 \tdx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
793 \tdx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
795 \tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
796 \tdx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
797 \tdx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
799 \tdx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
800 \tdx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
801 \tdx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
803 \caption{Set equalities} \label{hol-equalities}
807 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
808 obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
809 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
810 are designed for classical reasoning; the rules \tdx{subsetD},
811 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
812 strictly necessary but yield more natural proofs. Similarly,
813 \tdx{equalityCE} supports classical reasoning about extensionality,
814 after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for
815 proofs pertaining to set theory.
817 Figure~\ref{hol-fun} presents derived inference rules involving functions.
818 They also include rules for \cdx{Inv}, which is defined in theory~{\tt
819 HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
820 inverse of~$f$. They also include natural deduction rules for the image
821 and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
822 Reasoning about function composition (the operator~\sdx{o}) and the
823 predicate~\cdx{surj} is done simply by expanding the definitions. See
824 the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
826 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
827 Unions form least upper bounds; non-empty intersections form greatest lower
828 bounds. Reasoning directly about subsets often yields clearer proofs than
829 reasoning about the membership relation. See the file {\tt HOL/subset.ML}.
831 Figure~\ref{hol-equalities} presents many common set equalities. They
832 include commutative, associative and distributive laws involving unions,
833 intersections and complements. The proofs are mostly trivial, using the
834 classical reasoner; see file {\tt HOL/equalities.ML}.
839 \it symbol & \it meta-type & & \it description \\
840 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
841 & & ordered pairs $\langle a,b\rangle$ \\
842 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
843 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
844 \cdx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
845 & & generalized projection\\
847 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
848 & general sum of sets
850 \begin{ttbox}\makeatletter
851 \tdx{fst_def} fst(p) == @a. ? b. p = <a,b>
852 \tdx{snd_def} snd(p) == @b. ? a. p = <a,b>
853 \tdx{split_def} split(p,c) == c(fst(p),snd(p))
854 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
857 \tdx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
858 \tdx{fst_conv} fst(<a,b>) = a
859 \tdx{snd_conv} snd(<a,b>) = b
860 \tdx{split} split(<a,b>, c) = c(a,b)
862 \tdx{surjective_pairing} p = <fst(p),snd(p)>
864 \tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
866 \tdx{SigmaE} [| c: Sigma(A,B);
867 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
869 \caption{Type $\alpha\times\beta$}\label{hol-prod}
875 \it symbol & \it meta-type & & \it description \\
876 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
877 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
878 \cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
881 \begin{ttbox}\makeatletter
882 \tdx{sum_case_def} sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
883 (!y. p=Inr(y) --> z=g(y)))
885 \tdx{Inl_not_Inr} ~ Inl(a)=Inr(b)
887 \tdx{inj_Inl} inj(Inl)
888 \tdx{inj_Inr} inj(Inr)
890 \tdx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
892 \tdx{sum_case_Inl} sum_case(Inl(x), f, g) = f(x)
893 \tdx{sum_case_Inr} sum_case(Inr(x), f, g) = g(x)
895 \tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)
897 \caption{Type $\alpha+\beta$}\label{hol-sum}
901 \section{Generic packages and classical reasoning}
902 \HOL\ instantiates most of Isabelle's generic packages;
903 see {\tt HOL/ROOT.ML} for details.
906 Because it includes a general substitution rule, \HOL\ instantiates the
907 tactic {\tt hyp_subst_tac}, which substitutes for an equality
908 throughout a subgoal and its hypotheses.
910 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
911 simplification set for higher-order logic. Equality~($=$), which also
912 expresses logical equivalence, may be used for rewriting. See the file
913 {\tt HOL/simpdata.ML} for a complete listing of the simplification
916 It instantiates the classical reasoner, as described below.
918 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
919 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
920 rule; recall Fig.\ts\ref{hol-lemmas2} above.
922 The classical reasoner is set up as the structure
923 {\tt Classical}. This structure is open, so {\ML} identifiers such
924 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
925 \HOL\ defines the following classical rule sets:
932 \begin{ttdescription}
933 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
934 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
935 along with the rule~{\tt refl}.
937 \item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
938 {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
939 and~{\tt exI}, as well as rules for unique existence. Search using
940 this classical set is incomplete: quantified formulae are used at most
943 \item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
944 {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
945 and~\tdx{exCI}, as well as rules for unique existence. Search using
946 this is complete --- quantified formulae may be duplicated --- but
947 frequently fails to terminate. It is generally unsuitable for
950 \item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
951 quantifiers, subsets, comprehensions, unions and intersections,
952 complements, finite sets, images and ranges.
955 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
956 {Chap.\ts\ref{chap:classical}}
957 for more discussion of classical proof methods.
961 The basic higher-order logic is augmented with a tremendous amount of
962 material, including support for recursive function and type definitions. A
963 detailed discussion appears elsewhere~\cite{paulson-coind}. The simpler
964 definitions are the same as those used the {\sc hol} system, but my
965 treatment of recursive types differs from Melham's~\cite{melham89}. The
966 present section describes product, sum, natural number and list types.
968 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
969 Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
970 the ordered pair syntax {\tt<$a$,$b$>}. Theory \thydx{Sum} defines the
971 sum type $\alpha+\beta$. These use fairly standard constructions; see
972 Figs.\ts\ref{hol-prod} and~\ref{hol-sum}. Because Isabelle does not
973 support abstract type definitions, the isomorphisms between these types and
974 their representations are made explicitly.
976 Most of the definitions are suppressed, but observe that the projections
977 and conditionals are defined as descriptions. Their properties are easily
978 proved using \tdx{select_equality}.
988 \it symbol & \it meta-type & \it priority & \it description \\
989 \cdx{0} & $nat$ & & zero \\
990 \cdx{Suc} & $nat \To nat$ & & successor function\\
991 \cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
993 \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
994 & & primitive recursor\\
995 \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
996 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
997 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
998 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
999 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
1000 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1002 \subcaption{Constants and infixes}
1004 \begin{ttbox}\makeatother
1005 \tdx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
1006 (!x. n=Suc(x) --> z=f(x)))
1007 \tdx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
1008 \tdx{less_def} m<n == <m,n>:pred_nat^+
1009 \tdx{nat_rec_def} nat_rec(n,c,d) ==
1010 wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
1012 \tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
1013 \tdx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
1014 \tdx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
1015 \tdx{mod_def} m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
1016 \tdx{quo_def} m div n == wfrec(trancl(pred_nat),
1017 m, \%j f. if(j<n,0,Suc(f(j-n))))
1018 \subcaption{Definitions}
1020 \caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
1024 \begin{figure} \underscoreon
1026 \tdx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1028 \tdx{Suc_not_Zero} Suc(m) ~= 0
1029 \tdx{inj_Suc} inj(Suc)
1030 \tdx{n_not_Suc_n} n~=Suc(n)
1031 \subcaption{Basic properties}
1033 \tdx{pred_natI} <n, Suc(n)> : pred_nat
1035 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
1037 \tdx{nat_case_0} nat_case(0, a, f) = a
1038 \tdx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
1040 \tdx{wf_pred_nat} wf(pred_nat)
1041 \tdx{nat_rec_0} nat_rec(0,c,h) = c
1042 \tdx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1043 \subcaption{Case analysis and primitive recursion}
1045 \tdx{less_trans} [| i<j; j<k |] ==> i<k
1046 \tdx{lessI} n < Suc(n)
1047 \tdx{zero_less_Suc} 0 < Suc(n)
1049 \tdx{less_not_sym} n<m --> ~ m<n
1050 \tdx{less_not_refl} ~ n<n
1051 \tdx{not_less0} ~ n<0
1053 \tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1054 \tdx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1056 \tdx{less_linear} m<n | m=n | n<m
1057 \subcaption{The less-than relation}
1059 \caption{Derived rules for {\tt nat}} \label{hol-nat2}
1063 \subsection{The type of natural numbers, {\tt nat}}
1064 The theory \thydx{Nat} defines the natural numbers in a roundabout but
1065 traditional way. The axiom of infinity postulates an type~\tydx{ind} of
1066 individuals, which is non-empty and closed under an injective operation.
1067 The natural numbers are inductively generated by choosing an arbitrary
1068 individual for~0 and using the injective operation to take successors. As
1069 usual, the isomorphisms between~\tydx{nat} and its representation are made
1072 The definition makes use of a least fixed point operator \cdx{lfp},
1073 defined using the Knaster-Tarski theorem. This is used to define the
1074 operator \cdx{trancl}, for taking the transitive closure of a relation.
1075 Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
1076 along arbitrary well-founded relations. The corresponding theories are
1077 called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
1078 similar constructions in the context of set theory~\cite{paulson-set-II}.
1080 Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
1081 overloads $<$ and $\leq$ on the natural numbers. As of this writing,
1082 Isabelle provides no means of verifying that such overloading is sensible;
1083 there is no means of specifying the operators' properties and verifying
1084 that instances of the operators satisfy those properties. To be safe, the
1085 \HOL\ theory includes no polymorphic axioms asserting general properties of
1088 Theory \thydx{Arith} develops arithmetic on the natural numbers. It
1089 defines addition, multiplication, subtraction, division, and remainder.
1090 Many of their properties are proved: commutative, associative and
1091 distributive laws, identity and cancellation laws, etc. The most
1092 interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
1093 Division and remainder are defined by repeated subtraction, which requires
1094 well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
1097 The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1098 Recursion along this relation resembles primitive recursion, but is
1099 stronger because we are in higher-order logic; using primitive recursion to
1100 define a higher-order function, we can easily Ackermann's function, which
1101 is not primitive recursive \cite[page~104]{thompson91}.
1102 The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1103 natural numbers are most easily expressed using recursion along~$<$.
1105 The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
1106 variable~$n$ in subgoal~$i$.
1109 \index{#@{\tt\#} symbol}
1110 \index{"@@{\tt\at} symbol}
1112 \it symbol & \it meta-type & \it priority & \it description \\
1113 \cdx{Nil} & $\alpha list$ & & empty list\\
1114 \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
1116 \cdx{null} & $\alpha list \To bool$ & & emptiness test\\
1117 \cdx{hd} & $\alpha list \To \alpha$ & & head \\
1118 \cdx{tl} & $\alpha list \To \alpha list$ & & tail \\
1119 \cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\
1120 \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1121 \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
1122 \cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1123 & & mapping functional\\
1124 \cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1125 & & filter functional\\
1126 \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1127 & & forall functional\\
1128 \cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1129 \beta]\To\beta] \To \beta$
1132 \subcaption{Constants and infixes}
1134 \begin{center} \tt\frenchspacing
1135 \begin{tabular}{rrr}
1136 \it external & \it internal & \it description \\{}
1137 \sdx{[]} & Nil & \rm empty list \\{}
1138 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1139 \rm finite list \\{}
1140 [$x$:$l$. $P$] & filter($\lambda x{.}P$, $l$) &
1141 \rm list comprehension
1144 \subcaption{Translations}
1147 \tdx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1149 \tdx{Cons_not_Nil} (x # xs) ~= []
1150 \tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1151 \subcaption{Induction and freeness}
1153 \caption{The theory \thydx{List}} \label{hol-list}
1157 \begin{ttbox}\makeatother
1158 \tdx{list_rec_Nil} list_rec([],c,h) = c
1159 \tdx{list_rec_Cons} list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))
1161 \tdx{list_case_Nil} list_case([],c,h) = c
1162 \tdx{list_case_Cons} list_case(x#xs, c, h) = h(x, xs)
1164 \tdx{map_Nil} map(f,[]) = []
1165 \tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs)
1167 \tdx{null_Nil} null([]) = True
1168 \tdx{null_Cons} null(x#xs) = False
1170 \tdx{hd_Cons} hd(x#xs) = x
1171 \tdx{tl_Cons} tl(x#xs) = xs
1173 \tdx{ttl_Nil} ttl([]) = []
1174 \tdx{ttl_Cons} ttl(x#xs) = xs
1176 \tdx{append_Nil} [] @ ys = ys
1177 \tdx{append_Cons} (x#xs) \at ys = x # xs \at ys
1179 \tdx{mem_Nil} x mem [] = False
1180 \tdx{mem_Cons} x mem (y#ys) = if(y=x, True, x mem ys)
1182 \tdx{filter_Nil} filter(P, []) = []
1183 \tdx{filter_Cons} filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))
1185 \tdx{list_all_Nil} list_all(P,[]) = True
1186 \tdx{list_all_Cons} list_all(P, x#xs) = (P(x) & list_all(P, xs))
1188 \caption{Rewrite rules for lists} \label{hol-list-simps}
1192 \subsection{The type constructor for lists, {\tt list}}
1195 \HOL's definition of lists is an example of an experimental method for
1196 handling recursive data types. Figure~\ref{hol-list} presents the theory
1197 \thydx{List}: the basic list operations with their types and properties.
1199 The \sdx{case} construct is defined by the following translation:
1202 \begin{array}{r@{\;}l@{}l}
1203 "case " e " of" & "[]" & " => " a\\
1204 "|" & x"\#"xs & " => " b
1207 "list_case"(e, a, \lambda x\;xs.b)
1209 The theory includes \cdx{list_rec}, a primitive recursion operator
1210 for lists. It is derived from well-founded recursion, a general principle
1211 that can express arbitrary total recursive functions.
1213 The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
1214 the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
1216 The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
1217 variable~$xs$ in subgoal~$i$.
1220 \subsection{The type constructor for lazy lists, {\tt llist}}
1223 The definition of lazy lists demonstrates methods for handling infinite
1224 data structures and coinduction in higher-order logic. Theory
1225 \thydx{LList} defines an operator for corecursion on lazy lists, which is
1226 used to define a few simple functions such as map and append. Corecursion
1227 cannot easily define operations such as filter, which can compute
1228 indefinitely before yielding the next element (if any!) of the lazy list.
1229 A coinduction principle is defined for proving equations on lazy lists.
1231 I have written a paper discussing the treatment of lazy lists; it also
1232 covers finite lists~\cite{paulson-coind}.
1235 \section{Datatype declarations}
1240 It is often necessary to extend a theory with \ML-like datatypes. This
1241 extension consists of the new type, declarations of its constructors and
1242 rules that describe the new type. The theory definition section {\tt
1243 datatype} represents a compact way of doing this.
1246 \subsection{Foundations}
1248 A datatype declaration has the following general structure:
1249 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
1250 C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
1251 C_m(\tau_{m1},\dots,\tau_{mk_m})
1253 where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
1254 $\tau_{ij}$ are one of the following:
1256 \item type variables $\alpha_1,\dots,\alpha_n$,
1257 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared
1258 type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq
1259 \{\alpha_1,\dots,\alpha_n\}$,
1260 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This
1261 makes it a recursive type. To ensure that the new type is not empty at
1262 least one constructor must consist of only non-recursive type
1265 If you would like one of the $\tau_{ij}$ to be a complex type expression
1266 $\tau$ you need to declare a new type synonym $syn = \tau$ first and use
1267 $syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the
1268 recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt
1269 datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[
1270 \mbox{\tt datatype}~ t ~=~ C(t~list). \]
1272 The constructors are automatically defined as functions of their respective
1274 \[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
1275 These functions have certain {\em freeness} properties:
1277 \item[\tt distinct] They are distinct:
1278 \[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad
1279 \mbox{for all}~ i \neq j.
1281 \item[\tt inject] They are injective:
1282 \[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) =
1283 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
1286 Because the number of inequalities is quadratic in the number of
1287 constructors, a different method is used if their number exceeds
1288 a certain value, currently 4. In that case every constructor is mapped to a
1292 \mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\
1294 \mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1
1297 and distinctness of constructors is expressed by:
1299 \mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.
1301 In addition a structural induction axiom {\tt induct} is provided:
1305 \Forall x_1\dots x_{k_1}.
1306 \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
1307 \Imp & P(C_1(x_1,\dots,x_{k_1})) \\
1309 \Forall x_1\dots x_{k_m}.
1310 \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
1311 \Imp & P(C_m(x_1,\dots,x_{k_m}))
1314 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}
1315 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for
1316 all arguments of the recursive type.
1318 The type also comes with an \ML-like \sdx{case}-construct:
1321 \mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
1323 \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
1326 In contrast to \ML, {\em all} constructors must be present, their order is
1327 fixed, and nested patterns are not supported.
1330 \subsection{Defining datatypes}
1332 A datatype is defined in a theory definition file using the keyword {\tt
1333 datatype}. The definition following {\tt datatype} must conform to the
1334 syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must
1335 obey the rules in the previous section. As a result the theory is extended
1336 with the new type, the constructors, and the theorems listed in the previous
1341 typedecl : typevarlist id '=' (cons + '|')
1343 cons : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
1345 typ : typevarlist id
1348 typevarlist : () | tid | '(' (tid + ',') ')'
1351 \caption{Syntax of datatype declarations}
1352 \label{datatype-grammar}
1355 Reading the theory file produces a structure which, in addition to the usual
1356 components, contains a structure named $t$ for each datatype $t$ defined in
1357 the file.\footnote{Otherwise multiple datatypes in the same theory file would
1358 lead to name clashes.} Each structure $t$ contains the following elements:
1360 val distinct : thm list
1361 val inject : thm list
1363 val cases : thm list
1364 val simps : thm list
1365 val induct_tac : string -> int -> tactic
1367 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
1368 above. For convenience {\tt distinct} contains inequalities in both
1371 If there are five or more constructors, the {\em t\_ord} scheme is used for
1372 {\tt distinct}. In this case the theory {\tt Arith} must be contained
1373 in the current theory, if necessary by including it explicitly.
1375 The reduction rules of the {\tt case}-construct are in {\tt cases}. All
1376 theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
1377 {\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em
1378 var i}\/}'' applies structural induction over variable {\em var} to
1382 \subsection{Examples}
1384 \subsubsection{The datatype $\alpha~list$}
1386 We want to define the type $\alpha~list$.\footnote{Of course there is a list
1387 type in HOL already. This is only an example.} To do this we have to build
1388 a new theory that contains the type definition. We start from {\tt HOL}.
1391 datatype 'a list = Nil | Cons ('a, 'a list)
1394 After loading the theory (\verb$use_thy "MyList"$), we can prove
1395 $Cons(x,xs)\neq xs$. First we build a suitable simpset for the simplifier:
1397 val mylist_ss = HOL_ss addsimps MyList.list.simps;
1398 goal MyList.thy "!x. Cons(x,xs) ~= xs";
1400 {\out ! x. Cons(x, xs) ~= xs}
1401 {\out 1. ! x. Cons(x, xs) ~= xs}
1403 This can be proved by the structural induction tactic:
1405 by (MyList.list.induct_tac "xs" 1);
1407 {\out ! x. Cons(x, xs) ~= xs}
1408 {\out 1. ! x. Cons(x, Nil) ~= Nil}
1410 {\out ! x. Cons(x, list) ~= list ==>}
1411 {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
1413 The first subgoal can be proved with the simplifier and the distinctness
1414 axioms which are part of \verb$mylist_ss$.
1416 by (simp_tac mylist_ss 1);
1418 {\out ! x. Cons(x, xs) ~= xs}
1420 {\out ! x. Cons(x, list) ~= list ==>}
1421 {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
1423 Using the freeness axioms we can quickly prove the remaining goal.
1425 by (asm_simp_tac mylist_ss 1);
1427 {\out ! x. Cons(x, xs) ~= xs}
1430 Because both subgoals were proved by almost the same tactic we could have
1431 done that in one step using
1433 by (ALLGOALS (asm_simp_tac mylist_ss));
1437 \subsubsection{The datatype $\alpha~list$ with mixfix syntax}
1439 In this example we define the type $\alpha~list$ again but this time we want
1440 to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
1441 \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
1442 after the constructor declarations as follows:
1445 datatype 'a list = "[]" ("[]")
1446 | "#" ('a, 'a list) (infixr 70)
1449 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
1452 \subsubsection{Defining functions on datatypes}
1454 Normally one wants to define functions dealing with a newly defined type and
1455 prove properties of these functions. As an example let us define \verb|@| for
1456 concatenation and {\tt ttl} for the (total) tail of a list, i.e.\ the list
1457 without its first element:
1460 consts ttl :: "'a list => 'a list"
1461 "@" :: "['a list,'a list] => 'a list" (infixr 60)
1463 ttl_def "ttl (l) == case l of [] => [] | y#ys => ys"
1465 app_Nil "[] @ ys = ys"
1466 app_Cons "(x#xs) @ ys = x#(xs @ ys)"
1469 Let us have a look at the use of {\tt case} in the definition of {\tt ttl}.
1470 The expression {\tt case e of [] => [] | y\#ys => ys} evaluates to {\tt []}
1471 if \verb|e=[]| and to {\tt ys} if \verb|e=y#ys|. These properties are
1472 trivial to derive by simplification:
1474 val mylist_ss = HOL_ss addsimps MyList.list.simps;
1476 goalw List_fun.thy [List_fun.ttl_def] "ttl([]) = []";
1477 by (simp_tac mylist_ss 1);
1478 val ttl_Nil = result();
1480 goalw List_fun.thy [List_fun.ttl_def] "ttl(y#ys) = ys";
1481 by (simp_tac mylist_ss 1);
1482 val ttl_Cons = result();
1484 val list_fun_ss = mylist_ss addsimps
1485 [ttl_Nil, ttl_Cons, List_fun.app_Nil, List_fun.app_Cons];
1487 Note that we include the derived properties in our simpset, not the original
1488 definition of {\tt ttl}. The former are better behaved because they only
1489 apply if the argument is already a constructor.
1491 One could have defined \verb$@$ with a single {\tt case}-construct
1493 app_def "x @ y == case x of [] => y | z#zs => z # (zs @ y)"
1495 and derived \verb$app_Nil$ and \verb$app_Cons$ from it. But \verb$app_def$ is
1496 not easy to work with: the left-hand side matches a subterm of the right-hand
1497 side, which causes the simplifier to loop.
1499 Here is a simple proof of the associativity of \verb$@$:
1501 goal List_fun.thy "(x @ y) @ z = x @ (y @ z)";
1502 by (MyList.list.induct_tac "x" 1);
1503 by (simp_tac list_fun_ss 1);
1504 by (asm_simp_tac list_fun_ss 1);
1506 The last two steps can again be combined using {\tt ALLGOALS}.
1509 \subsubsection{A datatype for weekdays}
1511 This example shows a datatype that consists of more than four constructors:
1514 datatype days = Mo | Tu | We | Th | Fr | Sa | So
1517 Because there are more than four constructors, the theory must be based on
1518 {\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
1519 the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
1520 it can be proved by the simplifier if \verb$arith_ss$ is used:
1522 val days_ss = arith_ss addsimps Days.days.simps;
1524 goal Days.thy "Mo ~= Tu";
1525 by (simp_tac days_ss 1);
1527 Note that usually it is not necessary to derive these inequalities explicitly
1528 because the simplifier will dispose of them automatically.
1535 \section{The examples directories}
1536 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
1537 substitutions and unifiers. It is based on Paulson's previous
1538 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1541 Directory {\tt HOL/ex} contains other examples and experimental proofs in
1542 {\HOL}. Here is an overview of the more interesting files.
1543 \begin{ttdescription}
1544 \item[HOL/ex/cla.ML] demonstrates the classical reasoner on over sixty
1545 predicate calculus theorems, ranging from simple tautologies to
1546 moderately difficult problems involving equality and quantifiers.
1548 \item[HOL/ex/meson.ML] contains an experimental implementation of the {\sc
1549 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1550 much more powerful than Isabelle's classical reasoner. But it is less
1551 useful in practice because it works only for pure logic; it does not
1552 accept derived rules for the set theory primitives, for example.
1554 \item[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof
1555 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1557 \item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in
1558 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1560 \item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
1561 proofs about insertion sort and quick sort.
1563 \item[HOL/ex/PropLog.ML] proves the soundness and completeness of classical
1564 propositional logic, given a truth table semantics. The only connective
1565 is $\imp$. A Hilbert-style axiom system is specified, and its set of
1566 theorems defined inductively. A similar proof in \ZF{} is described
1567 elsewhere~\cite{paulson-set-II}.
1569 \item[HOL/ex/Term.ML]
1570 contains proofs about an experimental recursive type definition;
1571 the recursion goes through the type constructor~\tydx{list}.
1573 \item[HOL/ex/Simult.ML] defines primitives for solving mutually recursive
1574 equations over sets. It constructs sets of trees and forests as an
1575 example, including induction and recursion rules that handle the mutual
1578 \item[HOL/ex/MT.ML] contains Jacob Frost's formalization~\cite{frost93} of
1579 Milner and Tofte's coinduction example~\cite{milner-coind}. This
1580 substantial proof concerns the soundness of a type system for a simple
1581 functional language. The semantics of recursion is given by a cyclic
1582 environment, which makes a coinductive argument appropriate.
1587 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
1588 Cantor's Theorem states that every set has more subsets than it has
1589 elements. It has become a favourite example in higher-order logic since
1590 it is so easily expressed:
1591 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1592 \forall x::\alpha. f(x) \not= S
1595 Viewing types as sets, $\alpha\To bool$ represents the powerset
1596 of~$\alpha$. This version states that for every function from $\alpha$ to
1597 its powerset, some subset is outside its range.
1599 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1600 the operator \cdx{range}. The set~$S$ is given as an unknown instead of a
1601 quantified variable so that we may inspect the subset found by the proof.
1603 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1605 {\out ~ ?S : range(f)}
1606 {\out 1. ~ ?S : range(f)}
1608 The first two steps are routine. The rule \tdx{rangeE} replaces
1609 $\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
1611 by (resolve_tac [notI] 1);
1613 {\out ~ ?S : range(f)}
1614 {\out 1. ?S : range(f) ==> False}
1616 by (eresolve_tac [rangeE] 1);
1618 {\out ~ ?S : range(f)}
1619 {\out 1. !!x. ?S = f(x) ==> False}
1621 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1622 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1625 by (eresolve_tac [equalityCE] 1);
1627 {\out ~ ?S : range(f)}
1628 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1629 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1631 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
1632 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1633 $\Var{P}(\Var{c})$. Destruct-resolution using \tdx{CollectD}
1634 instantiates~$\Var{S}$ and creates the new assumption.
1636 by (dresolve_tac [CollectD] 1);
1638 {\out ~ \{x. ?P7(x)\} : range(f)}
1639 {\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
1640 {\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
1642 Forcing a contradiction between the two assumptions of subgoal~1 completes
1643 the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, which
1644 is the standard diagonal construction.
1648 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1649 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1651 The rest should be easy. To apply \tdx{CollectI} to the negated
1652 assumption, we employ \ttindex{swap_res_tac}:
1654 by (swap_res_tac [CollectI] 1);
1656 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1657 {\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
1661 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1664 How much creativity is required? As it happens, Isabelle can prove this
1665 theorem automatically. The classical set \ttindex{set_cs} contains rules
1666 for most of the constructs of \HOL's set theory. We must augment it with
1667 \tdx{equalityCE} to break up set equalities, and then apply best-first
1668 search. Depth-first search would diverge, but best-first search
1669 successfully navigates through the large search space.
1670 \index{search!best-first}
1674 {\out ~ ?S : range(f)}
1675 {\out 1. ~ ?S : range(f)}
1677 by (best_tac (set_cs addSEs [equalityCE]) 1);
1679 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1683 \index{higher-order logic|)}