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. It is based on
7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
8 Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a
9 full description of higher-order logic. Experience with the {\sc hol} system
10 has demonstrated that higher-order logic is useful for hardware verification;
11 beyond this, it is widely applicable in many areas of mathematics. It is
12 weaker than ZF set theory but for most applications this does not matter. If
13 you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
15 Previous releases of Isabelle included a different version of~HOL, with
16 explicit type inference rules~\cite{paulson-COLOG}. This version no longer
17 exists, but \thydx{ZF} supports a similar style of reasoning.
19 HOL has a distinct feel, compared with ZF and CTT. It identifies object-level
20 types with meta-level types, taking advantage of Isabelle's built-in type
21 checker. It identifies object-level functions with meta-level functions, so
22 it uses Isabelle's operations for abstraction and application. There is no
23 `apply' operator: function applications are written as simply~$f(a)$ rather
26 These identifications allow Isabelle to support HOL particularly nicely, but
27 they also mean that HOL requires more sophistication from the user --- in
28 particular, an understanding of Isabelle's type system. Beginners should work
29 with {\tt show_types} set to {\tt true}. Gain experience by working in
30 first-order logic before attempting to use higher-order logic. This chapter
31 assumes familiarity with~FOL.
37 \it name &\it meta-type & \it description \\
38 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
39 \cdx{not} & $bool\To bool$ & negation ($\neg$) \\
40 \cdx{True} & $bool$ & tautology ($\top$) \\
41 \cdx{False} & $bool$ & absurdity ($\bot$) \\
42 \cdx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
43 \cdx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
44 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
47 \subcaption{Constants}
50 \index{"@@{\tt\at} symbol}
51 \index{*"! symbol}\index{*"? symbol}
52 \index{*"?"! symbol}\index{*"E"X"! symbol}
53 \begin{tabular}{llrrr}
54 \it symbol &\it name &\it meta-type & \it description \\
55 \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ &
56 Hilbert description ($\epsilon$) \\
57 {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ &
58 universal quantifier ($\forall$) \\
59 {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ &
60 existential quantifier ($\exists$) \\
61 {\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ &
62 unique existence ($\exists!$)
69 \index{&@{\tt\&} symbol}
71 \index{*"-"-"> symbol}
73 \it symbol & \it meta-type & \it priority & \it description \\
74 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
75 Right 50 & composition ($\circ$) \\
76 \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
77 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
78 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
79 less than or equals ($\leq$)\\
80 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
81 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
82 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
86 \caption{Syntax of {\tt HOL}} \label{hol-constants}
94 \[\begin{array}{rclcl}
95 term & = & \hbox{expression of class~$term$} \\
96 & | & "\at~" id~id^* " . " formula \\
98 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term}
100 formula & = & \hbox{expression of type~$bool$} \\
101 & | & term " = " term \\
102 & | & term " \ttilde= " term \\
103 & | & term " < " term \\
104 & | & term " <= " term \\
105 & | & "\ttilde\ " formula \\
106 & | & formula " \& " formula \\
107 & | & formula " | " formula \\
108 & | & formula " --> " formula \\
109 & | & "!~~~" id~id^* " . " formula
110 & | & "ALL~" id~id^* " . " formula \\
111 & | & "?~~~" id~id^* " . " formula
112 & | & "EX~~" id~id^* " . " formula \\
113 & | & "?!~~" id~id^* " . " formula
114 & | & "EX!~" id~id^* " . " formula
117 \caption{Full grammar for HOL} \label{hol-grammar}
122 The type class of higher-order terms is called~\cldx{term}. Type variables
123 range over this class by default. The equality symbol and quantifiers are
124 polymorphic over class {\tt term}.
126 Class \cldx{ord} consists of all ordered types; the relations $<$ and
127 $\leq$ are polymorphic over this class, as are the functions
128 \cdx{mono}, \cdx{min} and \cdx{max}. Three other
129 type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
130 overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
131 {\tt-} is overloaded for set difference and subtraction.
136 Figure~\ref{hol-constants} lists the constants (including infixes and
137 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
138 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
142 HOL has no if-and-only-if connective; logical equivalence is expressed
143 using equality. But equality has a high priority, as befitting a
144 relation, while if-and-only-if typically has the lowest priority. Thus,
145 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
146 When using $=$ to mean logical equivalence, enclose both operands in
150 \subsection{Types}\label{HOL-types}
151 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
152 formulae are terms. The built-in type~\tydx{fun}, which constructs function
153 types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$
154 belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
157 Types in HOL must be non-empty; otherwise the quantifier rules would be
158 unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
160 \index{type definitions}
161 Gordon's {\sc hol} system supports {\bf type definitions}. A type is
162 defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
163 bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$
164 specifies a non-empty subset of~$\sigma$, and the new type denotes this
165 subset. New function constants are generated to establish an isomorphism
166 between the new type and the subset. If type~$\sigma$ involves type
167 variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
168 a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
169 type. Melham~\cite{melham89} discusses type definitions at length, with
172 Isabelle does not support type definitions at present. Instead, they are
173 mimicked by explicit definitions of isomorphism functions. The definitions
174 should be supported by theorems of the form $\exists x::\sigma.P(x)$, but
175 Isabelle cannot enforce this.
179 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
180 satisfying~$P[a]$, if such exists. Since all terms in HOL denote something, a
181 description is always meaningful, but we do not know its value unless $P[x]$
182 defines it uniquely. We may write descriptions as \cdx{Eps}($P$) or use the
183 syntax \hbox{\tt \at $x$.$P[x]$}.
185 Existential quantification is defined by
186 \[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
187 The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
188 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
189 quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
190 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
191 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
193 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
194 Quantifiers have two notations. As in Gordon's {\sc hol} system, HOL
195 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
196 existential quantifier must be followed by a space; thus {\tt?x} is an
197 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
198 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available. Both
199 notations are accepted for input. The {\ML} reference
200 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
201 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
202 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
204 All these binders have priority 10.
207 \subsection{The \sdx{let} and \sdx{case} constructions}
208 Local abbreviations can be introduced by a {\tt let} construct whose
209 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
210 the constant~\cdx{Let}. It can be expanded by rewriting with its
211 definition, \tdx{Let_def}.
213 HOL also defines the basic syntax
214 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
215 as a uniform means of expressing {\tt case} constructs. Therefore {\tt
216 case} and \sdx{of} are reserved words. However, so far this is mere
217 syntax and has no logical meaning. By declaring translations, you can
218 cause instances of the {\tt case} construct to denote applications of
219 particular case operators. The patterns supplied for $c@1$,~\ldots,~$c@n$
220 distinguish among the different case operators. For an example, see the
221 case construct for lists on page~\pageref{hol-list} below.
225 \begin{ttbox}\makeatother
226 \tdx{refl} t = (t::'a)
227 \tdx{subst} [| s=t; P(s) |] ==> P(t::'a)
228 \tdx{ext} (!!x::'a. (f(x)::'b) = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
229 \tdx{impI} (P ==> Q) ==> P-->Q
230 \tdx{mp} [| P-->Q; P |] ==> Q
231 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
232 \tdx{selectI} P(x::'a) ==> P(@x.P(x))
233 \tdx{True_or_False} (P=True) | (P=False)
235 \caption{The {\tt HOL} rules} \label{hol-rules}
239 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
240 \begin{ttbox}\makeatother
241 \tdx{True_def} True == ((\%x::bool.x)=(\%x.x))
242 \tdx{All_def} All == (\%P. P = (\%x.True))
243 \tdx{Ex_def} Ex == (\%P. P(@x.P(x)))
244 \tdx{False_def} False == (!P.P)
245 \tdx{not_def} not == (\%P. P-->False)
246 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
247 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
248 \tdx{Ex1_def} Ex1 == (\%P. ? x. P(x) & (! y. P(y) --> y=x))
250 \tdx{Inv_def} Inv == (\%(f::'a=>'b) y. @x. f(x)=y)
251 \tdx{o_def} op o == (\%(f::'b=>'c) g (x::'a). f(g(x)))
252 \tdx{if_def} if == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
253 \tdx{Let_def} Let(s,f) == f(s)
255 \caption{The {\tt HOL} definitions} \label{hol-defs}
259 \section{Rules of inference}
260 Figure~\ref{hol-rules} shows the inference rules of~HOL, with their~{\ML}
261 names. Some of the rules deserve additional comments:
262 \begin{ttdescription}
263 \item[\tdx{ext}] expresses extensionality of functions.
264 \item[\tdx{iff}] asserts that logically equivalent formulae are
266 \item[\tdx{selectI}] gives the defining property of the Hilbert
267 $\epsilon$-operator. It is a form of the Axiom of Choice. The derived rule
268 \tdx{select_equality} (see below) is often easier to use.
269 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
270 fact, the $\epsilon$-operator already makes the logic classical, as
271 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
274 HOL follows standard practice in higher-order logic: only a few connectives
275 are taken as primitive, with the remainder defined obscurely
276 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
277 corresponding definitions \cite[page~270]{mgordon-hol} using
278 object-equality~({\tt=}), which is possible because equality in higher-order
279 logic may equate formulae and even functions over formulae. But theory~HOL,
280 like all other Isabelle theories, uses meta-equality~({\tt==}) for
283 Some of the rules mention type variables; for
284 example, {\tt refl} mentions the type variable~{\tt'a}. This allows you to
285 instantiate type variables explicitly by calling {\tt res_inst_tac}. By
286 default, explicit type variables have class \cldx{term}.
288 Include type constraints whenever you state a polymorphic goal. Type
289 inference may otherwise make the goal more polymorphic than you intended,
290 with confusing results.
293 If resolution fails for no obvious reason, try setting
294 \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
295 terms. Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
296 Isabelle to display sorts.
298 \index{unification!incompleteness of}
299 Where function types are involved, Isabelle's unification code does not
300 guarantee to find instantiations for type variables automatically. Be
301 prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
302 possibly instantiating type variables. Setting
303 \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
304 omitted search paths during unification.\index{tracing!of unification}
310 \tdx{sym} s=t ==> t=s
311 \tdx{trans} [| r=s; s=t |] ==> r=t
312 \tdx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
313 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
314 \tdx{arg_cong} x=y ==> f(x)=f(y)
315 \tdx{fun_cong} f=g ==> f(x)=g(x)
316 \subcaption{Equality}
319 \tdx{FalseE} False ==> P
321 \tdx{conjI} [| P; Q |] ==> P&Q
322 \tdx{conjunct1} [| P&Q |] ==> P
323 \tdx{conjunct2} [| P&Q |] ==> Q
324 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
326 \tdx{disjI1} P ==> P|Q
327 \tdx{disjI2} Q ==> P|Q
328 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
330 \tdx{notI} (P ==> False) ==> ~ P
331 \tdx{notE} [| ~ P; P |] ==> R
332 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
333 \subcaption{Propositional logic}
335 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
336 \tdx{iffD1} [| P=Q; P |] ==> Q
337 \tdx{iffD2} [| P=Q; Q |] ==> P
338 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
340 \tdx{eqTrueI} P ==> P=True
341 \tdx{eqTrueE} P=True ==> P
342 \subcaption{Logical equivalence}
345 \caption{Derived rules for HOL} \label{hol-lemmas1}
350 \begin{ttbox}\makeatother
351 \tdx{allI} (!!x::'a. P(x)) ==> !x. P(x)
352 \tdx{spec} !x::'a.P(x) ==> P(x)
353 \tdx{allE} [| !x.P(x); P(x) ==> R |] ==> R
354 \tdx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
356 \tdx{exI} P(x) ==> ? x::'a.P(x)
357 \tdx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
359 \tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
360 \tdx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
363 \tdx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
364 \subcaption{Quantifiers and descriptions}
366 \tdx{ccontr} (~P ==> False) ==> P
367 \tdx{classical} (~P ==> P) ==> P
368 \tdx{excluded_middle} ~P | P
370 \tdx{disjCI} (~Q ==> P) ==> P|Q
371 \tdx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
372 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
373 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
374 \tdx{notnotD} ~~P ==> P
375 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
376 \subcaption{Classical logic}
378 \tdx{if_True} if(True,x,y) = x
379 \tdx{if_False} if(False,x,y) = y
380 \tdx{if_P} P ==> if(P,x,y) = x
381 \tdx{if_not_P} ~ P ==> if(P,x,y) = y
382 \tdx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
383 \subcaption{Conditionals}
385 \caption{More derived rules} \label{hol-lemmas2}
389 Some derived rules are shown in Figures~\ref{hol-lemmas1}
390 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
391 for the logical connectives, as well as sequent-style elimination rules for
392 conjunctions, implications, and universal quantifiers.
394 Note the equality rules: \tdx{ssubst} performs substitution in
395 backward proofs, while \tdx{box_equals} supports reasoning by
396 simplifying both sides of an equation.
402 \it name &\it meta-type & \it description \\
403 \index{{}@\verb'{}' symbol}
404 \verb|{}| & $\alpha\,set$ & the empty set \\
405 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
406 & insertion of element \\
407 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
409 \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$
411 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
412 & intersection over a set\\
413 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
415 \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
416 &set of sets intersection \\
417 \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
418 &set of sets union \\
419 \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
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 theory,
523 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 do
536 in~ZF. In HOL the intersection of the empty set is well-defined, denoting the
537 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 essentially
542 the same as $\alpha\To bool$. The new type is defined for clarity and to
543 avoid complications involving function types in unification. Since Isabelle
544 does not support type definitions (as mentioned in \S\ref{HOL-types}), the
545 isomorphisms between the two types are declared explicitly. Here they are
546 natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt
547 op :} maps in the other direction (ignoring argument order).
549 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
550 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
551 constructs. Infix operators include union and intersection ($A\union B$
552 and $A\inter B$), the subset and membership relations, and the image
553 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
556 The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
557 obvious manner using~{\tt insert} and~$\{\}$:
559 \{a@1, \ldots, a@n\} & \equiv &
560 {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
563 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) that
564 satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences
565 of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.P[x])$. It defines
566 sets by absolute comprehension, which is impossible in~ZF; the type of~$x$
567 implicitly restricts the comprehension.
569 The set theory defines two {\bf bounded quantifiers}:
571 \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
572 \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
574 The constants~\cdx{Ball} and~\cdx{Bex} are defined
575 accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
576 write\index{*"! symbol}\index{*"? symbol}
577 \index{*ALL symbol}\index{*EX symbol}
579 \hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's
580 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
581 for input. As with the primitive quantifiers, the {\ML} reference
582 \ttindex{HOL_quantifiers} specifies which notation to use for output.
584 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
585 $\bigcap@{x\in A}B[x]$, are written
586 \sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
587 \sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
589 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
590 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
591 \sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous
592 union and intersection operators when $A$ is the universal set.
594 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
595 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
599 \begin{figure} \underscoreon
601 \tdx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
602 \tdx{Collect_mem_eq} \{x.x:A\} = A
604 \tdx{empty_def} \{\} == \{x.False\}
605 \tdx{insert_def} insert(a,B) == \{x.x=a\} Un B
606 \tdx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
607 \tdx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
608 \tdx{subset_def} A <= B == ! x:A. x:B
609 \tdx{Un_def} A Un B == \{x.x:A | x:B\}
610 \tdx{Int_def} A Int B == \{x.x:A & x:B\}
611 \tdx{set_diff_def} A - B == \{x.x:A & x~:B\}
612 \tdx{Compl_def} Compl(A) == \{x. ~ x:A\}
613 \tdx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
614 \tdx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
615 \tdx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
616 \tdx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
617 \tdx{Inter_def} Inter(S) == (INT x:S. x)
618 \tdx{Union_def} Union(S) == (UN x:S. x)
619 \tdx{Pow_def} Pow(A) == \{B. B <= A\}
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 \tdx{PowI} A<=B ==> A: Pow(B)
703 \tdx{PowD} A: Pow(B) ==> A<=B
705 \caption{Further derived rules for set theory} \label{hol-set2}
709 \subsection{Axioms and rules of set theory}
710 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
711 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
712 that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms. Of
713 course, \hbox{\tt op :} also serves as the membership relation.
715 All the other axioms are definitions. They include the empty set, bounded
716 quantifiers, unions, intersections, complements and the subset relation.
717 They also include straightforward properties of functions: image~({\tt``}) and
718 {\tt range}, and predicates concerning monotonicity, injectiveness and
721 The predicate \cdx{inj_onto} is used for simulating type definitions.
722 The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
723 set~$A$, which specifies a subset of its domain type. In a type
724 definition, $f$ is the abstraction function and $A$ is the set of valid
725 representations; we should not expect $f$ to be injective outside of~$A$.
727 \begin{figure} \underscoreon
729 \tdx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
730 \tdx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
733 % [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
735 \tdx{imageI} [| x:A |] ==> f(x) : f``A
736 \tdx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
738 \tdx{rangeI} f(x) : range(f)
739 \tdx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
741 \tdx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
742 \tdx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
744 \tdx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
745 \tdx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
746 \tdx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
748 \tdx{inj_ontoI} (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
749 \tdx{inj_ontoD} [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
751 \tdx{inj_onto_inverseI}
752 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
753 \tdx{inj_onto_contraD}
754 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
756 \caption{Derived rules involving functions} \label{hol-fun}
760 \begin{figure} \underscoreon
762 \tdx{Union_upper} B:A ==> B <= Union(A)
763 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
765 \tdx{Inter_lower} B:A ==> Inter(A) <= B
766 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
768 \tdx{Un_upper1} A <= A Un B
769 \tdx{Un_upper2} B <= A Un B
770 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
772 \tdx{Int_lower1} A Int B <= A
773 \tdx{Int_lower2} A Int B <= B
774 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
776 \caption{Derived rules involving subsets} \label{hol-subset}
780 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
782 \tdx{Int_absorb} A Int A = A
783 \tdx{Int_commute} A Int B = B Int A
784 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
785 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
787 \tdx{Un_absorb} A Un A = A
788 \tdx{Un_commute} A Un B = B Un A
789 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
790 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
792 \tdx{Compl_disjoint} A Int Compl(A) = \{x.False\}
793 \tdx{Compl_partition} A Un Compl(A) = \{x.True\}
794 \tdx{double_complement} Compl(Compl(A)) = A
795 \tdx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
796 \tdx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
798 \tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
799 \tdx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
800 \tdx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
802 \tdx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
803 \tdx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
804 \tdx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
806 \caption{Set equalities} \label{hol-equalities}
810 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
811 obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such
812 as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
813 reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
814 not strictly necessary but yield more natural proofs. Similarly,
815 \tdx{equalityCE} supports classical reasoning about extensionality, after the
816 fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for proofs pertaining
819 Figure~\ref{hol-fun} presents derived inference rules involving functions.
820 They also include rules for \cdx{Inv}, which is defined in theory~{\tt
821 HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
822 inverse of~$f$. They also include natural deduction rules for the image
823 and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
824 Reasoning about function composition (the operator~\sdx{o}) and the
825 predicate~\cdx{surj} is done simply by expanding the definitions. See
826 the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
828 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
829 Unions form least upper bounds; non-empty intersections form greatest lower
830 bounds. Reasoning directly about subsets often yields clearer proofs than
831 reasoning about the membership relation. See the file {\tt HOL/subset.ML}.
833 Figure~\ref{hol-equalities} presents many common set equalities. They
834 include commutative, associative and distributive laws involving unions,
835 intersections and complements. The proofs are mostly trivial, using the
836 classical reasoner; see file {\tt HOL/equalities.ML}.
841 \it symbol & \it meta-type & & \it description \\
842 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
843 & & ordered pairs $\langle a,b\rangle$ \\
844 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
845 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
846 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
847 & & generalized projection\\
849 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
850 & general sum of sets
852 \begin{ttbox}\makeatletter
853 \tdx{fst_def} fst(p) == @a. ? b. p = <a,b>
854 \tdx{snd_def} snd(p) == @b. ? a. p = <a,b>
855 \tdx{split_def} split(c,p) == c(fst(p),snd(p))
856 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
859 \tdx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
860 \tdx{fst_conv} fst(<a,b>) = a
861 \tdx{snd_conv} snd(<a,b>) = b
862 \tdx{split} split(c, <a,b>) = c(a,b)
864 \tdx{surjective_pairing} p = <fst(p),snd(p)>
866 \tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
868 \tdx{SigmaE} [| c: Sigma(A,B);
869 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
871 \caption{Type $\alpha\times\beta$}\label{hol-prod}
877 \it symbol & \it meta-type & & \it description \\
878 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
879 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
880 \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
883 \begin{ttbox}\makeatletter
884 \tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl(x) --> z=f(x)) &
885 (!y. p=Inr(y) --> z=g(y)))
887 \tdx{Inl_not_Inr} ~ Inl(a)=Inr(b)
889 \tdx{inj_Inl} inj(Inl)
890 \tdx{inj_Inr} inj(Inr)
892 \tdx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
894 \tdx{sum_case_Inl} sum_case(f, g, Inl(x)) = f(x)
895 \tdx{sum_case_Inr} sum_case(f, g, Inr(x)) = g(x)
897 \tdx{surjective_sum} sum_case(\%x::'a. f(Inl(x)), \%y::'b. f(Inr(y)), s) = f(s)
899 \caption{Type $\alpha+\beta$}\label{hol-sum}
903 \section{Generic packages and classical reasoning}
904 HOL instantiates most of Isabelle's generic packages; see {\tt HOL/ROOT.ML}
907 \item Because it includes a general substitution rule, HOL instantiates the
908 tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
909 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 well as
920 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
921 Fig.\ts\ref{hol-lemmas2} above.
923 The classical reasoner is set up as the structure {\tt Classical}. This
924 structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt
925 fast_tac}, {\tt best_tac}, etc., refer to it. HOL defines the following
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{set_cs}] extends {\tt HOL_cs} with rules for the bounded
944 quantifiers, subsets, comprehensions, unions and intersections,
945 complements, finite sets, images and ranges.
948 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
949 {Chap.\ts\ref{chap:classical}}
950 for more discussion of classical proof methods.
954 The basic higher-order logic is augmented with a tremendous amount of
955 material, including support for recursive function and type definitions. A
956 detailed discussion appears elsewhere~\cite{paulson-coind}. The simpler
957 definitions are the same as those used the {\sc hol} system, but my
958 treatment of recursive types differs from Melham's~\cite{melham89}. The
959 present section describes product, sum, natural number and list types.
961 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
962 Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
963 the ordered pair syntax {\tt<$a$,$b$>}. Theory \thydx{Sum} defines the
964 sum type $\alpha+\beta$. These use fairly standard constructions; see
965 Figs.\ts\ref{hol-prod} and~\ref{hol-sum}. Because Isabelle does not
966 support abstract type definitions, the isomorphisms between these types and
967 their representations are made explicitly.
969 Most of the definitions are suppressed, but observe that the projections
970 and conditionals are defined as descriptions. Their properties are easily
971 proved using \tdx{select_equality}.
981 \it symbol & \it meta-type & \it priority & \it description \\
982 \cdx{0} & $nat$ & & zero \\
983 \cdx{Suc} & $nat \To nat$ & & successor function\\
984 \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$
986 \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
987 & & primitive recursor\\
988 \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
989 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
990 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
991 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
992 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
993 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
995 \subcaption{Constants and infixes}
997 \begin{ttbox}\makeatother
998 \tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 --> z=a) &
999 (!x. n=Suc(x) --> z=f(x)))
1000 \tdx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
1001 \tdx{less_def} m<n == <m,n>:pred_nat^+
1002 \tdx{nat_rec_def} nat_rec(n,c,d) ==
1003 wfrec(pred_nat, n, nat_case(\%g.c, \%m g. d(m,g(m))))
1005 \tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
1006 \tdx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
1007 \tdx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
1008 \tdx{mod_def} m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
1009 \tdx{quo_def} m div n == wfrec(trancl(pred_nat),
1010 m, \%j f. if(j<n,0,Suc(f(j-n))))
1011 \subcaption{Definitions}
1013 \caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
1017 \begin{figure} \underscoreon
1019 \tdx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1021 \tdx{Suc_not_Zero} Suc(m) ~= 0
1022 \tdx{inj_Suc} inj(Suc)
1023 \tdx{n_not_Suc_n} n~=Suc(n)
1024 \subcaption{Basic properties}
1026 \tdx{pred_natI} <n, Suc(n)> : pred_nat
1028 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
1030 \tdx{nat_case_0} nat_case(a, f, 0) = a
1031 \tdx{nat_case_Suc} nat_case(a, f, Suc(k)) = f(k)
1033 \tdx{wf_pred_nat} wf(pred_nat)
1034 \tdx{nat_rec_0} nat_rec(0,c,h) = c
1035 \tdx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1036 \subcaption{Case analysis and primitive recursion}
1038 \tdx{less_trans} [| i<j; j<k |] ==> i<k
1039 \tdx{lessI} n < Suc(n)
1040 \tdx{zero_less_Suc} 0 < Suc(n)
1042 \tdx{less_not_sym} n<m --> ~ m<n
1043 \tdx{less_not_refl} ~ n<n
1044 \tdx{not_less0} ~ n<0
1046 \tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1047 \tdx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1049 \tdx{less_linear} m<n | m=n | n<m
1050 \subcaption{The less-than relation}
1052 \caption{Derived rules for {\tt nat}} \label{hol-nat2}
1056 \subsection{The type of natural numbers, {\tt nat}}
1057 The theory \thydx{Nat} defines the natural numbers in a roundabout but
1058 traditional way. The axiom of infinity postulates an type~\tydx{ind} of
1059 individuals, which is non-empty and closed under an injective operation.
1060 The natural numbers are inductively generated by choosing an arbitrary
1061 individual for~0 and using the injective operation to take successors. As
1062 usual, the isomorphisms between~\tydx{nat} and its representation are made
1065 The definition makes use of a least fixed point operator \cdx{lfp},
1066 defined using the Knaster-Tarski theorem. This is used to define the
1067 operator \cdx{trancl}, for taking the transitive closure of a relation.
1068 Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
1069 along arbitrary well-founded relations. The corresponding theories are
1070 called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
1071 similar constructions in the context of set theory~\cite{paulson-set-II}.
1073 Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which overloads
1074 $<$ and $\leq$ on the natural numbers. As of this writing, Isabelle provides
1075 no means of verifying that such overloading is sensible; there is no means of
1076 specifying the operators' properties and verifying that instances of the
1077 operators satisfy those properties. To be safe, the HOL theory includes no
1078 polymorphic axioms asserting general properties of $<$ and~$\leq$.
1080 Theory \thydx{Arith} develops arithmetic on the natural numbers. It
1081 defines addition, multiplication, subtraction, division, and remainder.
1082 Many of their properties are proved: commutative, associative and
1083 distributive laws, identity and cancellation laws, etc. The most
1084 interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
1085 Division and remainder are defined by repeated subtraction, which requires
1086 well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
1089 The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1090 Recursion along this relation resembles primitive recursion, but is
1091 stronger because we are in higher-order logic; using primitive recursion to
1092 define a higher-order function, we can easily Ackermann's function, which
1093 is not primitive recursive \cite[page~104]{thompson91}.
1094 The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1095 natural numbers are most easily expressed using recursion along~$<$.
1097 The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
1098 variable~$n$ in subgoal~$i$.
1101 \index{#@{\tt\#} symbol}
1102 \index{"@@{\tt\at} symbol}
1104 \it symbol & \it meta-type & \it priority & \it description \\
1105 \cdx{Nil} & $\alpha list$ & & empty list\\
1106 \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
1108 \cdx{null} & $\alpha list \To bool$ & & emptiness test\\
1109 \cdx{hd} & $\alpha list \To \alpha$ & & head \\
1110 \cdx{tl} & $\alpha list \To \alpha list$ & & tail \\
1111 \cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\
1112 \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1113 \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
1114 \cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1115 & & mapping functional\\
1116 \cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1117 & & filter functional\\
1118 \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1119 & & forall functional\\
1120 \cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1121 \beta]\To\beta] \To \beta$
1124 \subcaption{Constants and infixes}
1126 \begin{center} \tt\frenchspacing
1127 \begin{tabular}{rrr}
1128 \it external & \it internal & \it description \\{}
1129 \sdx{[]} & Nil & \rm empty list \\{}
1130 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1131 \rm finite list \\{}
1132 [$x$:$l$. $P$] & filter($\lambda x{.}P$, $l$) &
1133 \rm list comprehension
1136 \subcaption{Translations}
1139 \tdx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1141 \tdx{Cons_not_Nil} (x # xs) ~= []
1142 \tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1143 \subcaption{Induction and freeness}
1145 \caption{The theory \thydx{List}} \label{hol-list}
1149 \begin{ttbox}\makeatother
1150 \tdx{list_rec_Nil} list_rec([],c,h) = c
1151 \tdx{list_rec_Cons} list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))
1153 \tdx{list_case_Nil} list_case(c, h, []) = c
1154 \tdx{list_case_Cons} list_case(c, h, x#xs) = h(x, xs)
1156 \tdx{map_Nil} map(f,[]) = []
1157 \tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs)
1159 \tdx{null_Nil} null([]) = True
1160 \tdx{null_Cons} null(x#xs) = False
1162 \tdx{hd_Cons} hd(x#xs) = x
1163 \tdx{tl_Cons} tl(x#xs) = xs
1165 \tdx{ttl_Nil} ttl([]) = []
1166 \tdx{ttl_Cons} ttl(x#xs) = xs
1168 \tdx{append_Nil} [] @ ys = ys
1169 \tdx{append_Cons} (x#xs) \at ys = x # xs \at ys
1171 \tdx{mem_Nil} x mem [] = False
1172 \tdx{mem_Cons} x mem (y#ys) = if(y=x, True, x mem ys)
1174 \tdx{filter_Nil} filter(P, []) = []
1175 \tdx{filter_Cons} filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))
1177 \tdx{list_all_Nil} list_all(P,[]) = True
1178 \tdx{list_all_Cons} list_all(P, x#xs) = (P(x) & list_all(P, xs))
1180 \caption{Rewrite rules for lists} \label{hol-list-simps}
1184 \subsection{The type constructor for lists, {\tt list}}
1187 HOL's definition of lists is an example of an experimental method for handling
1188 recursive data types. Figure~\ref{hol-list} presents the theory \thydx{List}:
1189 the basic list operations with their types and properties.
1191 The \sdx{case} construct is defined by the following translation:
1194 \begin{array}{r@{\;}l@{}l}
1195 "case " e " of" & "[]" & " => " a\\
1196 "|" & x"\#"xs & " => " b
1199 "list_case"(a, \lambda x\;xs.b, e)
1201 The theory includes \cdx{list_rec}, a primitive recursion operator
1202 for lists. It is derived from well-founded recursion, a general principle
1203 that can express arbitrary total recursive functions.
1205 The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
1206 the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
1208 The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
1209 variable~$xs$ in subgoal~$i$.
1212 \section{Datatype declarations}
1217 It is often necessary to extend a theory with \ML-like datatypes. This
1218 extension consists of the new type, declarations of its constructors and
1219 rules that describe the new type. The theory definition section {\tt
1220 datatype} represents a compact way of doing this.
1223 \subsection{Foundations}
1225 A datatype declaration has the following general structure:
1226 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
1227 C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
1228 C_m(\tau_{m1},\dots,\tau_{mk_m})
1230 where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
1231 $\tau_{ij}$ are one of the following:
1233 \item type variables $\alpha_1,\dots,\alpha_n$,
1234 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared
1235 type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq
1236 \{\alpha_1,\dots,\alpha_n\}$,
1237 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This
1238 makes it a recursive type. To ensure that the new type is not empty at
1239 least one constructor must consist of only non-recursive type
1242 If you would like one of the $\tau_{ij}$ to be a complex type expression
1243 $\tau$ you need to declare a new type synonym $syn = \tau$ first and use
1244 $syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the
1245 recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt
1246 datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[
1247 \mbox{\tt datatype}~ t ~=~ C(t~list). \]
1249 The constructors are automatically defined as functions of their respective
1251 \[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
1252 These functions have certain {\em freeness} properties:
1254 \item[\tt distinct] They are distinct:
1255 \[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad
1256 \mbox{for all}~ i \neq j.
1258 \item[\tt inject] They are injective:
1259 \[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) =
1260 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
1263 Because the number of inequalities is quadratic in the number of
1264 constructors, a different method is used if their number exceeds
1265 a certain value, currently 4. In that case every constructor is mapped to a
1269 \mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\
1271 \mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1
1274 and distinctness of constructors is expressed by:
1276 \mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.
1278 In addition a structural induction axiom {\tt induct} is provided:
1282 \Forall x_1\dots x_{k_1}.
1283 \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
1284 \Imp & P(C_1(x_1,\dots,x_{k_1})) \\
1286 \Forall x_1\dots x_{k_m}.
1287 \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
1288 \Imp & P(C_m(x_1,\dots,x_{k_m}))
1291 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}
1292 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for
1293 all arguments of the recursive type.
1295 The type also comes with an \ML-like \sdx{case}-construct:
1298 \mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
1300 \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
1303 In contrast to \ML, {\em all} constructors must be present, their order is
1304 fixed, and nested patterns are not supported.
1307 \subsection{Defining datatypes}
1309 A datatype is defined in a theory definition file using the keyword {\tt
1310 datatype}. The definition following {\tt datatype} must conform to the
1311 syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must
1312 obey the rules in the previous section. As a result the theory is extended
1313 with the new type, the constructors, and the theorems listed in the previous
1318 typedecl : typevarlist id '=' (cons + '|')
1320 cons : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
1322 typ : typevarlist id
1325 typevarlist : () | tid | '(' (tid + ',') ')'
1328 \caption{Syntax of datatype declarations}
1329 \label{datatype-grammar}
1332 Reading the theory file produces a structure which, in addition to the usual
1333 components, contains a structure named $t$ for each datatype $t$ defined in
1334 the file.\footnote{Otherwise multiple datatypes in the same theory file would
1335 lead to name clashes.} Each structure $t$ contains the following elements:
1337 val distinct : thm list
1338 val inject : thm list
1340 val cases : thm list
1341 val simps : thm list
1342 val induct_tac : string -> int -> tactic
1344 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
1345 above. For convenience {\tt distinct} contains inequalities in both
1348 If there are five or more constructors, the {\em t\_ord} scheme is used for
1349 {\tt distinct}. In this case the theory {\tt Arith} must be contained
1350 in the current theory, if necessary by including it explicitly.
1352 The reduction rules of the {\tt case}-construct are in {\tt cases}. All
1353 theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
1354 {\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em
1355 var i}\/} applies structural induction over variable {\em var} to
1359 \subsection{Examples}
1361 \subsubsection{The datatype $\alpha~list$}
1363 We want to define the type $\alpha~list$.\footnote{Of course there is a list
1364 type in HOL already. This is only an example.} To do this we have to build
1365 a new theory that contains the type definition. We start from {\tt HOL}.
1368 datatype 'a list = Nil | Cons ('a, 'a list)
1371 After loading the theory (\verb$use_thy "MyList"$), we can prove
1372 $Cons(x,xs)\neq xs$. First we build a suitable simpset for the simplifier:
1374 val mylist_ss = HOL_ss addsimps MyList.list.simps;
1375 goal MyList.thy "!x. Cons(x,xs) ~= xs";
1377 {\out ! x. Cons(x, xs) ~= xs}
1378 {\out 1. ! x. Cons(x, xs) ~= xs}
1380 This can be proved by the structural induction tactic:
1382 by (MyList.list.induct_tac "xs" 1);
1384 {\out ! x. Cons(x, xs) ~= xs}
1385 {\out 1. ! x. Cons(x, Nil) ~= Nil}
1387 {\out ! x. Cons(x, list) ~= list ==>}
1388 {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
1390 The first subgoal can be proved with the simplifier and the distinctness
1391 axioms which are part of \verb$mylist_ss$.
1393 by (simp_tac mylist_ss 1);
1395 {\out ! x. Cons(x, xs) ~= xs}
1397 {\out ! x. Cons(x, list) ~= list ==>}
1398 {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
1400 Using the freeness axioms we can quickly prove the remaining goal.
1402 by (asm_simp_tac mylist_ss 1);
1404 {\out ! x. Cons(x, xs) ~= xs}
1407 Because both subgoals were proved by almost the same tactic we could have
1408 done that in one step using
1410 by (ALLGOALS (asm_simp_tac mylist_ss));
1414 \subsubsection{The datatype $\alpha~list$ with mixfix syntax}
1416 In this example we define the type $\alpha~list$ again but this time we want
1417 to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
1418 \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
1419 after the constructor declarations as follows:
1422 datatype 'a list = "[]" ("[]")
1423 | "#" ('a, 'a list) (infixr 70)
1426 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
1430 \subsubsection{A datatype for weekdays}
1432 This example shows a datatype that consists of more than four constructors:
1435 datatype days = Mo | Tu | We | Th | Fr | Sa | So
1438 Because there are more than four constructors, the theory must be based on
1439 {\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
1440 the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
1441 it can be proved by the simplifier if \verb$arith_ss$ is used:
1443 val days_ss = arith_ss addsimps Days.days.simps;
1445 goal Days.thy "Mo ~= Tu";
1446 by (simp_tac days_ss 1);
1448 Note that usually it is not necessary to derive these inequalities explicitly
1449 because the simplifier will dispose of them automatically.
1451 \subsection{Primitive recursive functions}
1452 \index{primitive recursion|(}
1455 Datatypes come with a uniform way of defining functions, {\bf primitive
1456 recursion}. Although it is possible to define primitive recursive functions
1457 by asserting their reduction rules as new axioms, e.g.\
1460 consts app :: "['a list,'a list] => 'a list"
1462 app_Nil "app([],ys) = ys"
1463 app_Cons "app(x#xs, ys) = x#app(xs,ys)"
1466 this carries with it the danger of accidentally asserting an inconsistency,
1467 as in \verb$app([],ys) = us$. Therefore primitive recursive functions on
1468 datatypes can be defined with a special syntax:
1471 consts app :: "['a list,'a list] => 'a list"
1472 primrec app MyList.list
1473 app_Nil "app([],ys) = ys"
1474 app_Cons "app(x#xs, ys) = x#app(xs,ys)"
1477 The system will now check that the two rules \verb$app_Nil$ and
1478 \verb$app_Cons$ do indeed form a primitive recursive definition, thus
1479 ensuring that consistency is maintained. For example
1481 primrec app MyList.list
1482 app_Nil "app([],ys) = us"
1486 Extra variables on rhs
1490 The general form of a primitive recursive definition is
1492 primrec {\it function} {\it type}
1493 {\it reduction rules}
1497 \item {\it function} is the name of the function, either as an {\it id} or a
1498 {\it string}. The function must already have been declared.
1499 \item {\it type} is the name of the datatype, either as an {\it id} or in the
1500 long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the
1501 datatype was declared in, and $t$ the name of the datatype. The long form
1502 is required if the {\tt datatype} and the {\tt primrec} sections are in
1504 \item {\it reduction rules} specify one or more named equations of the form
1505 {\it id\/}~{\it string}, where the identifier gives the name of the rule in
1506 the result structure, and {\it string} is a reduction rule of the form \[
1507 f(x_1,\dots,x_m,C(y_1,\dots,y_k),z_1,\dots,z_n) = r \] such that $C$ is a
1508 constructor of the datatype, $r$ contains only the free variables on the
1509 left-hand side, and all recursive calls in $r$ are of the form
1510 $f(\dots,y_i,\dots)$ for some $i$. There must be exactly one reduction
1511 rule for each constructor.
1513 A theory file may contain any number of {\tt primrec} sections which may be
1514 intermixed with other declarations.
1516 For the consistency-sensitive user it may be reassuring to know that {\tt
1517 primrec} does not assert the reduction rules as new axioms but derives them
1518 as theorems from an explicit definition of the recursive function in terms of
1519 a recursion operator on the datatype.
1521 The primitive recursive function can also use infix or mixfix syntax:
1524 consts "@" :: "['a list,'a list] => 'a list" (infixr 60)
1525 primrec "op @" MyList.list
1526 app_Nil "[] @ ys = ys"
1527 app_Cons "(x#xs) @ ys = x#(xs @ ys)"
1531 The reduction rules become part of the ML structure \verb$Append$ and can
1532 be used to prove theorems about the function:
1534 val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];
1536 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
1537 by (MyList.list.induct_tac "xs" 1);
1538 by (ALLGOALS(asm_simp_tac append_ss));
1541 %Note that underdefined primitive recursive functions are allowed:
1544 %consts tl :: "'a list => 'a list"
1545 %primrec tl MyList.list
1546 % tl_Cons "tl(x#xs) = xs"
1549 %Nevertheless {\tt tl} is total, although we do not know what the result of
1552 \index{primitive recursion|)}
1557 \section{Inductive and coinductive definitions}
1558 \index{*inductive|(}
1559 \index{*coinductive|(}
1561 An {\bf inductive definition} specifies the least set closed under given
1562 rules. For example, a structural operational semantics is an inductive
1563 definition of an evaluation relation. Dually, a {\bf coinductive
1564 definition} specifies the greatest set consistent with given rules. An
1565 important example is using bisimulation relations to formalize equivalence
1566 of processes and infinite data structures.
1568 A theory file may contain any number of inductive and coinductive
1569 definitions. They may be intermixed with other declarations; in
1570 particular, the (co)inductive sets {\bf must} be declared separately as
1571 constants, and may have mixfix syntax or be subject to syntax translations.
1573 Each (co)inductive definition adds definitions to the theory and also
1574 proves some theorems. Each definition creates an ML structure, which is a
1575 substructure of the main theory structure.
1577 This package is derived from the ZF one, described in a
1578 separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
1579 longer version is distributed with Isabelle.} which you should refer to
1580 in case of difficulties. The package is simpler than ZF's, thanks to HOL's
1581 automatic type-checking. The type of the (co)inductive determines the
1582 domain of the fixedpoint definition, and the package does not use inference
1583 rules for type-checking.
1586 \subsection{The result structure}
1587 Many of the result structure's components have been discussed in the paper;
1588 others are self-explanatory.
1590 \item[\tt thy] is the new theory containing the recursive sets.
1592 \item[\tt defs] is the list of definitions of the recursive sets.
1594 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
1596 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
1597 the recursive sets, in the case of mutual recursion).
1599 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1600 the recursive sets. The rules are also available individually, using the
1601 names given them in the theory file.
1603 \item[\tt elim] is the elimination rule.
1605 \item[\tt mk\_cases] is a function to create simplified instances of {\tt
1606 elim}, using freeness reasoning on some underlying datatype.
1609 For an inductive definition, the result structure contains two induction rules,
1610 {\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
1611 contains the rule \verb|coinduct|.
1613 Figure~\ref{def-result-fig} summarizes the two result signatures,
1614 specifying the types of all these components.
1623 val intrs : thm list
1625 val mk_cases : thm list -> string -> thm
1626 {\it(Inductive definitions only)}
1628 val mutual_induct: thm
1629 {\it(Coinductive definitions only)}
1634 \caption{The result of a (co)inductive definition} \label{def-result-fig}
1637 \subsection{The syntax of a (co)inductive definition}
1638 An inductive definition has the form
1640 inductive {\it inductive sets}
1641 intrs {\it introduction rules}
1642 monos {\it monotonicity theorems}
1643 con_defs {\it constructor definitions}
1645 A coinductive definition is identical, except that it starts with the keyword
1648 The {\tt monos} and {\tt con\_defs} sections are optional. If present,
1649 each is specified as a string, which must be a valid ML expression of type
1650 {\tt thm list}. It is simply inserted into the {\tt .thy.ML} file; if it
1651 is ill-formed, it will trigger ML error messages. You can then inspect the
1652 file on your directory.
1655 \item The {\it inductive sets} are specified by one or more strings.
1657 \item The {\it introduction rules} specify one or more introduction rules in
1658 the form {\it ident\/}~{\it string}, where the identifier gives the name of
1659 the rule in the result structure.
1661 \item The {\it monotonicity theorems} are required for each operator
1662 applied to a recursive set in the introduction rules. There {\bf must}
1663 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
1664 premise $t\in M(R_i)$ in an introduction rule!
1666 \item The {\it constructor definitions} contain definitions of constants
1667 appearing in the introduction rules. In most cases it can be omitted.
1670 The package has a few notable restrictions:
1672 \item The theory must separately declare the recursive sets as
1675 \item The names of the recursive sets must be identifiers, not infix
1678 \item Side-conditions must not be conjunctions. However, an introduction rule
1679 may contain any number of side-conditions.
1681 \item Side-conditions of the form $x=t$, where the variable~$x$ does not
1682 occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
1686 \subsection{Example of an inductive definition}
1687 Two declarations, included in a theory file, define the finite powerset
1688 operator. First we declare the constant~{\tt Fin}. Then we declare it
1689 inductively, with two introduction rules:
1691 consts Fin :: "'a set => 'a set set"
1694 emptyI "{} : Fin(A)"
1695 insertI "[| a: A; b: Fin(A) |] ==> insert(a,b) : Fin(A)"
1697 The resulting theory structure contains a substructure, called~{\tt Fin}.
1698 It contains the {\tt Fin}$(A)$ introduction rules as the list {\tt Fin.intrs},
1699 and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
1700 rule is {\tt Fin.induct}.
1702 For another example, here is a theory file defining the accessible part of a
1703 relation. The main thing to note is the use of~{\tt Pow} in the sole
1704 introduction rule, and the corresponding mention of the rule
1705 \verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version
1706 of this example in more detail.
1709 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
1710 acc :: "('a * 'a)set => 'a set" (*Accessible part*)
1711 defs pred_def "pred(x,r) == {y. <y,x>:r}"
1714 pred "pred(a,r): Pow(acc(r)) ==> a: acc(r)"
1718 The HOL distribution contains many other inductive definitions, such as the
1719 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The
1720 theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
1722 \index{*coinductive|)} \index{*inductive|)} \underscoreoff
1725 \section{The examples directories}
1726 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
1727 substitutions and unifiers. It is based on Paulson's previous
1728 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1731 Directory {\tt HOL/IMP} contains a mechanised version of a semantic
1732 equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
1733 denotational and operational semantics of a simple while-language, then
1734 proves the two equivalent. It contains several datatype and inductive
1735 definitions, and demonstrates their use.
1737 Directory {\tt HOL/ex} contains other examples and experimental proofs in HOL.
1738 Here is an overview of the more interesting files.
1740 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
1741 predicate calculus theorems, ranging from simple tautologies to
1742 moderately difficult problems involving equality and quantifiers.
1744 \item File {\tt meson.ML} contains an experimental implementation of the {\sc
1745 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1746 much more powerful than Isabelle's classical reasoner. But it is less
1747 useful in practice because it works only for pure logic; it does not
1748 accept derived rules for the set theory primitives, for example.
1750 \item File {\tt mesontest.ML} contains test data for the {\sc meson} proof
1751 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1753 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in
1754 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1756 \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
1757 insertion sort and quick sort.
1759 \item The definition of lazy lists demonstrates methods for handling
1760 infinite data structures and coinduction in higher-order
1761 logic~\cite{paulson-coind}. Theory \thydx{LList} defines an operator for
1762 corecursion on lazy lists, which is used to define a few simple functions
1763 such as map and append. Corecursion cannot easily define operations such
1764 as filter, which can compute indefinitely before yielding the next
1765 element (if any!) of the lazy list. A coinduction principle is defined
1766 for proving equations on lazy lists.
1768 \item Theory {\tt PropLog} proves the soundness and completeness of classical
1769 propositional logic, given a truth table semantics. The only connective is
1770 $\imp$. A Hilbert-style axiom system is specified, and its set of theorems
1771 defined inductively. A similar proof in ZF is described
1772 elsewhere~\cite{paulson-set-II}.
1774 \item Theory {\tt Term} develops an experimental recursive type definition;
1775 the recursion goes through the type constructor~\tydx{list}.
1777 \item Theory {\tt Simult} constructs mutually recursive sets of trees and
1778 forests, including induction and recursion rules.
1780 \item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of
1781 Milner and Tofte's coinduction example~\cite{milner-coind}. This
1782 substantial proof concerns the soundness of a type system for a simple
1783 functional language. The semantics of recursion is given by a cyclic
1784 environment, which makes a coinductive argument appropriate.
1789 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
1790 Cantor's Theorem states that every set has more subsets than it has
1791 elements. It has become a favourite example in higher-order logic since
1792 it is so easily expressed:
1793 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1794 \forall x::\alpha. f(x) \not= S
1797 Viewing types as sets, $\alpha\To bool$ represents the powerset
1798 of~$\alpha$. This version states that for every function from $\alpha$ to
1799 its powerset, some subset is outside its range.
1801 The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and the
1802 operator \cdx{range}. The set~$S$ is given as an unknown instead of a
1803 quantified variable so that we may inspect the subset found by the proof.
1805 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1807 {\out ~ ?S : range(f)}
1808 {\out 1. ~ ?S : range(f)}
1810 The first two steps are routine. The rule \tdx{rangeE} replaces
1811 $\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
1813 by (resolve_tac [notI] 1);
1815 {\out ~ ?S : range(f)}
1816 {\out 1. ?S : range(f) ==> False}
1818 by (eresolve_tac [rangeE] 1);
1820 {\out ~ ?S : range(f)}
1821 {\out 1. !!x. ?S = f(x) ==> False}
1823 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1824 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1827 by (eresolve_tac [equalityCE] 1);
1829 {\out ~ ?S : range(f)}
1830 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1831 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1833 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
1834 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1835 $\Var{P}(\Var{c})$. Destruct-resolution using \tdx{CollectD}
1836 instantiates~$\Var{S}$ and creates the new assumption.
1838 by (dresolve_tac [CollectD] 1);
1840 {\out ~ \{x. ?P7(x)\} : range(f)}
1841 {\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
1842 {\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
1844 Forcing a contradiction between the two assumptions of subgoal~1 completes
1845 the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, which
1846 is the standard diagonal construction.
1850 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1851 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1853 The rest should be easy. To apply \tdx{CollectI} to the negated
1854 assumption, we employ \ttindex{swap_res_tac}:
1856 by (swap_res_tac [CollectI] 1);
1858 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1859 {\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
1863 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1866 How much creativity is required? As it happens, Isabelle can prove this
1867 theorem automatically. The classical set \ttindex{set_cs} contains rules for
1868 most of the constructs of HOL's set theory. We must augment it with
1869 \tdx{equalityCE} to break up set equalities, and then apply best-first search.
1870 Depth-first search would diverge, but best-first search successfully navigates
1871 through the large search space. \index{search!best-first}
1875 {\out ~ ?S : range(f)}
1876 {\out 1. ~ ?S : range(f)}
1878 by (best_tac (set_cs addSEs [equalityCE]) 1);
1880 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1884 \index{higher-order logic|)}