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{Pow} & $\alpha\,set \To (\alpha\,set)set$
423 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
424 & range of a function \\[1ex]
425 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
426 & bounded quantifiers \\
427 \cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
429 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
430 & injective/surjective \\
431 \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
432 & injective over subset
435 \subcaption{Constants}
438 \begin{tabular}{llrrr}
439 \it symbol &\it name &\it meta-type & \it priority & \it description \\
440 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
441 intersection over a type\\
442 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
452 \begin{tabular}{rrrr}
453 \it symbol & \it meta-type & \it priority & \it description \\
454 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
456 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
457 & Left 70 & intersection ($\inter$) \\
458 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
459 & Left 65 & union ($\union$) \\
460 \tt: & $[\alpha ,\alpha\,set]\To bool$
461 & Left 50 & membership ($\in$) \\
462 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
463 & Left 50 & subset ($\subseteq$)
467 \caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}
472 \begin{center} \tt\frenchspacing
475 \it external & \it internal & \it description \\
476 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
477 \{$a@1$, $\ldots$\} & insert($a@1$, $\ldots$\{\}) & \rm finite set \\
478 \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
480 \sdx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
482 \sdx{UN}{\tt\ } $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
484 \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ &
485 Ball($A$,$\lambda x.P[x]$) &
486 \rm bounded $\forall$ \\
487 \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ &
488 Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$
491 \subcaption{Translations}
494 \[\begin{array}{rclcl}
495 term & = & \hbox{other terms\ldots} \\
497 & | & "\{ " term\; ("," term)^* " \}" \\
498 & | & "\{ " id " . " formula " \}" \\
499 & | & term " `` " term \\
500 & | & term " Int " term \\
501 & | & term " Un " term \\
502 & | & "INT~~" id ":" term " . " term \\
503 & | & "UN~~~" id ":" term " . " term \\
504 & | & "INT~~" id~id^* " . " term \\
505 & | & "UN~~~" id~id^* " . " term \\[2ex]
506 formula & = & \hbox{other formulae\ldots} \\
507 & | & term " : " term \\
508 & | & term " \ttilde: " term \\
509 & | & term " <= " term \\
510 & | & "!~" id ":" term " . " formula
511 & | & "ALL " id ":" term " . " formula \\
512 & | & "?~" id ":" term " . " formula
513 & | & "EX~~" id ":" term " . " formula
516 \subcaption{Full Grammar}
517 \caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
521 \section{A formulation of set theory}
522 Historically, higher-order logic gives a foundation for Russell and
523 Whitehead's theory of classes. Let us use modern terminology and call them
524 {\bf sets}, but note that these sets are distinct from those of {\ZF} set
525 theory, and behave more like {\ZF} classes.
528 Sets are given by predicates over some type~$\sigma$. Types serve to
529 define universes for sets, but type checking is still significant.
531 There is a universal set (for each type). Thus, sets have complements, and
532 may be defined by absolute comprehension.
534 Although sets may contain other sets as elements, the containing set must
535 have a more complex type.
537 Finite unions and intersections have the same behaviour in \HOL\ as they
538 do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
539 denoting the universal set for the given type.
542 \subsection{Syntax of set theory}\index{*set type}
543 \HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
544 essentially the same as $\alpha\To bool$. The new type is defined for
545 clarity and to avoid complications involving function types in unification.
546 Since Isabelle does not support type definitions (as mentioned in
547 \S\ref{HOL-types}), the isomorphisms between the two types are declared
548 explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
549 $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
552 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
553 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
554 constructs. Infix operators include union and intersection ($A\union B$
555 and $A\inter B$), the subset and membership relations, and the image
556 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
559 The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
560 obvious manner using~{\tt insert} and~$\{\}$:
562 \{a@1, \ldots, a@n\} & \equiv &
563 {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
566 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
567 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
568 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
569 x.P[x])$. It defines sets by absolute comprehension, which is impossible
570 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
572 The set theory defines two {\bf bounded quantifiers}:
574 \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
575 \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
577 The constants~\cdx{Ball} and~\cdx{Bex} are defined
578 accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
579 write\index{*"! symbol}\index{*"? symbol}
580 \index{*ALL symbol}\index{*EX symbol}
582 \hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's
583 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
584 for input. As with the primitive quantifiers, the {\ML} reference
585 \ttindex{HOL_quantifiers} specifies which notation to use for output.
587 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
588 $\bigcap@{x\in A}B[x]$, are written
589 \sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
590 \sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
592 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
593 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
594 \sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous
595 union and intersection operators when $A$ is the universal set.
597 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
598 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
602 \begin{figure} \underscoreon
604 \tdx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
605 \tdx{Collect_mem_eq} \{x.x:A\} = A
607 \tdx{empty_def} \{\} == \{x.False\}
608 \tdx{insert_def} insert(a,B) == \{x.x=a\} Un B
609 \tdx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
610 \tdx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
611 \tdx{subset_def} A <= B == ! x:A. x:B
612 \tdx{Un_def} A Un B == \{x.x:A | x:B\}
613 \tdx{Int_def} A Int B == \{x.x:A & x:B\}
614 \tdx{set_diff_def} A - B == \{x.x:A & x~:B\}
615 \tdx{Compl_def} Compl(A) == \{x. ~ x:A\}
616 \tdx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
617 \tdx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
618 \tdx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
619 \tdx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
620 \tdx{Inter_def} Inter(S) == (INT x:S. x)
621 \tdx{Union_def} Union(S) == (UN x:S. x)
622 \tdx{Pow_def} Pow(A) == \{B. B <= A\}
623 \tdx{image_def} f``A == \{y. ? x:A. y=f(x)\}
624 \tdx{range_def} range(f) == \{y. ? x. y=f(x)\}
625 \tdx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
626 \tdx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
627 \tdx{surj_def} surj(f) == ! y. ? x. y=f(x)
628 \tdx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
630 \caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
634 \begin{figure} \underscoreon
636 \tdx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
637 \tdx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
638 \tdx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
640 \tdx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
641 \tdx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
642 \tdx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
644 \tdx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
645 \tdx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
646 \tdx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
647 \subcaption{Comprehension and Bounded quantifiers}
649 \tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
650 \tdx{subsetD} [| A <= B; c:A |] ==> c:B
651 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
653 \tdx{subset_refl} A <= A
654 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
656 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B
657 \tdx{equalityD1} A = B ==> A<=B
658 \tdx{equalityD2} A = B ==> B<=A
659 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
661 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
662 [| ~ c:A; ~ c:B |] ==> P
664 \subcaption{The subset and equality relations}
666 \caption{Derived rules for set theory} \label{hol-set1}
670 \begin{figure} \underscoreon
672 \tdx{emptyE} a : \{\} ==> P
674 \tdx{insertI1} a : insert(a,B)
675 \tdx{insertI2} a : B ==> a : insert(b,B)
676 \tdx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
678 \tdx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
679 \tdx{ComplD} [| c : Compl(A) |] ==> ~ c:A
681 \tdx{UnI1} c:A ==> c : A Un B
682 \tdx{UnI2} c:B ==> c : A Un B
683 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
684 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
686 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B
687 \tdx{IntD1} c : A Int B ==> c:A
688 \tdx{IntD2} c : A Int B ==> c:B
689 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
691 \tdx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
692 \tdx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
694 \tdx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
695 \tdx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
696 \tdx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
698 \tdx{UnionI} [| X:C; A:X |] ==> A : Union(C)
699 \tdx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
701 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
702 \tdx{InterD} [| A : Inter(C); X:C |] ==> A:X
703 \tdx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
705 \tdx{PowI} A<=B ==> A: Pow(B)
706 \tdx{PowD} A: Pow(B) ==> A<=B
708 \caption{Further derived rules for set theory} \label{hol-set2}
712 \subsection{Axioms and rules of set theory}
713 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
714 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
715 that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms. Of
716 course, \hbox{\tt op :} also serves as the membership relation.
718 All the other axioms are definitions. They include the empty set, bounded
719 quantifiers, unions, intersections, complements and the subset relation.
720 They also include straightforward properties of functions: image~({\tt``}) and
721 {\tt range}, and predicates concerning monotonicity, injectiveness and
724 The predicate \cdx{inj_onto} is used for simulating type definitions.
725 The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
726 set~$A$, which specifies a subset of its domain type. In a type
727 definition, $f$ is the abstraction function and $A$ is the set of valid
728 representations; we should not expect $f$ to be injective outside of~$A$.
730 \begin{figure} \underscoreon
732 \tdx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
733 \tdx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
736 % [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
738 \tdx{imageI} [| x:A |] ==> f(x) : f``A
739 \tdx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
741 \tdx{rangeI} f(x) : range(f)
742 \tdx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
744 \tdx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
745 \tdx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
747 \tdx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
748 \tdx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
749 \tdx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
751 \tdx{inj_ontoI} (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
752 \tdx{inj_ontoD} [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
754 \tdx{inj_onto_inverseI}
755 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
756 \tdx{inj_onto_contraD}
757 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
759 \caption{Derived rules involving functions} \label{hol-fun}
763 \begin{figure} \underscoreon
765 \tdx{Union_upper} B:A ==> B <= Union(A)
766 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
768 \tdx{Inter_lower} B:A ==> Inter(A) <= B
769 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
771 \tdx{Un_upper1} A <= A Un B
772 \tdx{Un_upper2} B <= A Un B
773 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
775 \tdx{Int_lower1} A Int B <= A
776 \tdx{Int_lower2} A Int B <= B
777 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
779 \caption{Derived rules involving subsets} \label{hol-subset}
783 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
785 \tdx{Int_absorb} A Int A = A
786 \tdx{Int_commute} A Int B = B Int A
787 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
788 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
790 \tdx{Un_absorb} A Un A = A
791 \tdx{Un_commute} A Un B = B Un A
792 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
793 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
795 \tdx{Compl_disjoint} A Int Compl(A) = \{x.False\}
796 \tdx{Compl_partition} A Un Compl(A) = \{x.True\}
797 \tdx{double_complement} Compl(Compl(A)) = A
798 \tdx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
799 \tdx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
801 \tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
802 \tdx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
803 \tdx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
805 \tdx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
806 \tdx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
807 \tdx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
809 \caption{Set equalities} \label{hol-equalities}
813 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
814 obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
815 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
816 are designed for classical reasoning; the rules \tdx{subsetD},
817 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
818 strictly necessary but yield more natural proofs. Similarly,
819 \tdx{equalityCE} supports classical reasoning about extensionality,
820 after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for
821 proofs pertaining to set theory.
823 Figure~\ref{hol-fun} presents derived inference rules involving functions.
824 They also include rules for \cdx{Inv}, which is defined in theory~{\tt
825 HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
826 inverse of~$f$. They also include natural deduction rules for the image
827 and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
828 Reasoning about function composition (the operator~\sdx{o}) and the
829 predicate~\cdx{surj} is done simply by expanding the definitions. See
830 the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
832 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
833 Unions form least upper bounds; non-empty intersections form greatest lower
834 bounds. Reasoning directly about subsets often yields clearer proofs than
835 reasoning about the membership relation. See the file {\tt HOL/subset.ML}.
837 Figure~\ref{hol-equalities} presents many common set equalities. They
838 include commutative, associative and distributive laws involving unions,
839 intersections and complements. The proofs are mostly trivial, using the
840 classical reasoner; see file {\tt HOL/equalities.ML}.
845 \it symbol & \it meta-type & & \it description \\
846 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
847 & & ordered pairs $\langle a,b\rangle$ \\
848 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
849 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
850 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
851 & & generalized projection\\
853 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
854 & general sum of sets
856 \begin{ttbox}\makeatletter
857 \tdx{fst_def} fst(p) == @a. ? b. p = <a,b>
858 \tdx{snd_def} snd(p) == @b. ? a. p = <a,b>
859 \tdx{split_def} split(c,p) == c(fst(p),snd(p))
860 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
863 \tdx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
864 \tdx{fst_conv} fst(<a,b>) = a
865 \tdx{snd_conv} snd(<a,b>) = b
866 \tdx{split} split(c, <a,b>) = c(a,b)
868 \tdx{surjective_pairing} p = <fst(p),snd(p)>
870 \tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
872 \tdx{SigmaE} [| c: Sigma(A,B);
873 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
875 \caption{Type $\alpha\times\beta$}\label{hol-prod}
881 \it symbol & \it meta-type & & \it description \\
882 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
883 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
884 \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
887 \begin{ttbox}\makeatletter
888 \tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl(x) --> z=f(x)) &
889 (!y. p=Inr(y) --> z=g(y)))
891 \tdx{Inl_not_Inr} ~ Inl(a)=Inr(b)
893 \tdx{inj_Inl} inj(Inl)
894 \tdx{inj_Inr} inj(Inr)
896 \tdx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
898 \tdx{sum_case_Inl} sum_case(f, g, Inl(x)) = f(x)
899 \tdx{sum_case_Inr} sum_case(f, g, Inr(x)) = g(x)
901 \tdx{surjective_sum} sum_case(\%x::'a. f(Inl(x)), \%y::'b. f(Inr(y)), s) = f(s)
903 \caption{Type $\alpha+\beta$}\label{hol-sum}
907 \section{Generic packages and classical reasoning}
908 \HOL\ instantiates most of Isabelle's generic packages;
909 see {\tt HOL/ROOT.ML} for details.
912 Because it includes a general substitution rule, \HOL\ instantiates the
913 tactic {\tt hyp_subst_tac}, which substitutes for an equality
914 throughout a subgoal and its hypotheses.
916 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
917 simplification set for higher-order logic. Equality~($=$), which also
918 expresses logical equivalence, may be used for rewriting. See the file
919 {\tt HOL/simpdata.ML} for a complete listing of the simplification
922 It instantiates the classical reasoner, as described below.
924 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
925 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
926 rule; recall Fig.\ts\ref{hol-lemmas2} above.
928 The classical reasoner is set up as the structure
929 {\tt Classical}. This structure is open, so {\ML} identifiers such
930 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
931 \HOL\ defines the following classical rule sets:
937 \begin{ttdescription}
938 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
939 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
940 along with the rule~{\tt refl}.
942 \item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
943 {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
944 and~{\tt exI}, as well as rules for unique existence. Search using
945 this classical set is incomplete: quantified formulae are used at most
948 \item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
949 quantifiers, subsets, comprehensions, unions and intersections,
950 complements, finite sets, images and ranges.
953 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
954 {Chap.\ts\ref{chap:classical}}
955 for more discussion of classical proof methods.
959 The basic higher-order logic is augmented with a tremendous amount of
960 material, including support for recursive function and type definitions. A
961 detailed discussion appears elsewhere~\cite{paulson-coind}. The simpler
962 definitions are the same as those used the {\sc hol} system, but my
963 treatment of recursive types differs from Melham's~\cite{melham89}. The
964 present section describes product, sum, natural number and list types.
966 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
967 Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
968 the ordered pair syntax {\tt<$a$,$b$>}. Theory \thydx{Sum} defines the
969 sum type $\alpha+\beta$. These use fairly standard constructions; see
970 Figs.\ts\ref{hol-prod} and~\ref{hol-sum}. Because Isabelle does not
971 support abstract type definitions, the isomorphisms between these types and
972 their representations are made explicitly.
974 Most of the definitions are suppressed, but observe that the projections
975 and conditionals are defined as descriptions. Their properties are easily
976 proved using \tdx{select_equality}.
986 \it symbol & \it meta-type & \it priority & \it description \\
987 \cdx{0} & $nat$ & & zero \\
988 \cdx{Suc} & $nat \To nat$ & & successor function\\
989 \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$
991 \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
992 & & primitive recursor\\
993 \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
994 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
995 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
996 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
997 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
998 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1000 \subcaption{Constants and infixes}
1002 \begin{ttbox}\makeatother
1003 \tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 --> z=a) &
1004 (!x. n=Suc(x) --> z=f(x)))
1005 \tdx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
1006 \tdx{less_def} m<n == <m,n>:pred_nat^+
1007 \tdx{nat_rec_def} nat_rec(n,c,d) ==
1008 wfrec(pred_nat, n, nat_case(\%g.c, \%m g. d(m,g(m))))
1010 \tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
1011 \tdx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
1012 \tdx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
1013 \tdx{mod_def} m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
1014 \tdx{quo_def} m div n == wfrec(trancl(pred_nat),
1015 m, \%j f. if(j<n,0,Suc(f(j-n))))
1016 \subcaption{Definitions}
1018 \caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
1022 \begin{figure} \underscoreon
1024 \tdx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1026 \tdx{Suc_not_Zero} Suc(m) ~= 0
1027 \tdx{inj_Suc} inj(Suc)
1028 \tdx{n_not_Suc_n} n~=Suc(n)
1029 \subcaption{Basic properties}
1031 \tdx{pred_natI} <n, Suc(n)> : pred_nat
1033 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
1035 \tdx{nat_case_0} nat_case(a, f, 0) = a
1036 \tdx{nat_case_Suc} nat_case(a, f, Suc(k)) = f(k)
1038 \tdx{wf_pred_nat} wf(pred_nat)
1039 \tdx{nat_rec_0} nat_rec(0,c,h) = c
1040 \tdx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1041 \subcaption{Case analysis and primitive recursion}
1043 \tdx{less_trans} [| i<j; j<k |] ==> i<k
1044 \tdx{lessI} n < Suc(n)
1045 \tdx{zero_less_Suc} 0 < Suc(n)
1047 \tdx{less_not_sym} n<m --> ~ m<n
1048 \tdx{less_not_refl} ~ n<n
1049 \tdx{not_less0} ~ n<0
1051 \tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1052 \tdx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1054 \tdx{less_linear} m<n | m=n | n<m
1055 \subcaption{The less-than relation}
1057 \caption{Derived rules for {\tt nat}} \label{hol-nat2}
1061 \subsection{The type of natural numbers, {\tt nat}}
1062 The theory \thydx{Nat} defines the natural numbers in a roundabout but
1063 traditional way. The axiom of infinity postulates an type~\tydx{ind} of
1064 individuals, which is non-empty and closed under an injective operation.
1065 The natural numbers are inductively generated by choosing an arbitrary
1066 individual for~0 and using the injective operation to take successors. As
1067 usual, the isomorphisms between~\tydx{nat} and its representation are made
1070 The definition makes use of a least fixed point operator \cdx{lfp},
1071 defined using the Knaster-Tarski theorem. This is used to define the
1072 operator \cdx{trancl}, for taking the transitive closure of a relation.
1073 Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
1074 along arbitrary well-founded relations. The corresponding theories are
1075 called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
1076 similar constructions in the context of set theory~\cite{paulson-set-II}.
1078 Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
1079 overloads $<$ and $\leq$ on the natural numbers. As of this writing,
1080 Isabelle provides no means of verifying that such overloading is sensible;
1081 there is no means of specifying the operators' properties and verifying
1082 that instances of the operators satisfy those properties. To be safe, the
1083 \HOL\ theory includes no polymorphic axioms asserting general properties of
1086 Theory \thydx{Arith} develops arithmetic on the natural numbers. It
1087 defines addition, multiplication, subtraction, division, and remainder.
1088 Many of their properties are proved: commutative, associative and
1089 distributive laws, identity and cancellation laws, etc. The most
1090 interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
1091 Division and remainder are defined by repeated subtraction, which requires
1092 well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
1095 The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1096 Recursion along this relation resembles primitive recursion, but is
1097 stronger because we are in higher-order logic; using primitive recursion to
1098 define a higher-order function, we can easily Ackermann's function, which
1099 is not primitive recursive \cite[page~104]{thompson91}.
1100 The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1101 natural numbers are most easily expressed using recursion along~$<$.
1103 The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
1104 variable~$n$ in subgoal~$i$.
1107 \index{#@{\tt\#} symbol}
1108 \index{"@@{\tt\at} symbol}
1110 \it symbol & \it meta-type & \it priority & \it description \\
1111 \cdx{Nil} & $\alpha list$ & & empty list\\
1112 \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
1114 \cdx{null} & $\alpha list \To bool$ & & emptiness test\\
1115 \cdx{hd} & $\alpha list \To \alpha$ & & head \\
1116 \cdx{tl} & $\alpha list \To \alpha list$ & & tail \\
1117 \cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\
1118 \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1119 \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
1120 \cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1121 & & mapping functional\\
1122 \cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1123 & & filter functional\\
1124 \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1125 & & forall functional\\
1126 \cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1127 \beta]\To\beta] \To \beta$
1130 \subcaption{Constants and infixes}
1132 \begin{center} \tt\frenchspacing
1133 \begin{tabular}{rrr}
1134 \it external & \it internal & \it description \\{}
1135 \sdx{[]} & Nil & \rm empty list \\{}
1136 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1137 \rm finite list \\{}
1138 [$x$:$l$. $P$] & filter($\lambda x{.}P$, $l$) &
1139 \rm list comprehension
1142 \subcaption{Translations}
1145 \tdx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1147 \tdx{Cons_not_Nil} (x # xs) ~= []
1148 \tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1149 \subcaption{Induction and freeness}
1151 \caption{The theory \thydx{List}} \label{hol-list}
1155 \begin{ttbox}\makeatother
1156 \tdx{list_rec_Nil} list_rec([],c,h) = c
1157 \tdx{list_rec_Cons} list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))
1159 \tdx{list_case_Nil} list_case(c, h, []) = c
1160 \tdx{list_case_Cons} list_case(c, h, x#xs) = h(x, xs)
1162 \tdx{map_Nil} map(f,[]) = []
1163 \tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs)
1165 \tdx{null_Nil} null([]) = True
1166 \tdx{null_Cons} null(x#xs) = False
1168 \tdx{hd_Cons} hd(x#xs) = x
1169 \tdx{tl_Cons} tl(x#xs) = xs
1171 \tdx{ttl_Nil} ttl([]) = []
1172 \tdx{ttl_Cons} ttl(x#xs) = xs
1174 \tdx{append_Nil} [] @ ys = ys
1175 \tdx{append_Cons} (x#xs) \at ys = x # xs \at ys
1177 \tdx{mem_Nil} x mem [] = False
1178 \tdx{mem_Cons} x mem (y#ys) = if(y=x, True, x mem ys)
1180 \tdx{filter_Nil} filter(P, []) = []
1181 \tdx{filter_Cons} filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))
1183 \tdx{list_all_Nil} list_all(P,[]) = True
1184 \tdx{list_all_Cons} list_all(P, x#xs) = (P(x) & list_all(P, xs))
1186 \caption{Rewrite rules for lists} \label{hol-list-simps}
1190 \subsection{The type constructor for lists, {\tt list}}
1193 \HOL's definition of lists is an example of an experimental method for
1194 handling recursive data types. Figure~\ref{hol-list} presents the theory
1195 \thydx{List}: the basic list operations with their types and properties.
1197 The \sdx{case} construct is defined by the following translation:
1200 \begin{array}{r@{\;}l@{}l}
1201 "case " e " of" & "[]" & " => " a\\
1202 "|" & x"\#"xs & " => " b
1205 "list_case"(a, \lambda x\;xs.b, e)
1207 The theory includes \cdx{list_rec}, a primitive recursion operator
1208 for lists. It is derived from well-founded recursion, a general principle
1209 that can express arbitrary total recursive functions.
1211 The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
1212 the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
1214 The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
1215 variable~$xs$ in subgoal~$i$.
1218 \section{Datatype declarations}
1223 It is often necessary to extend a theory with \ML-like datatypes. This
1224 extension consists of the new type, declarations of its constructors and
1225 rules that describe the new type. The theory definition section {\tt
1226 datatype} represents a compact way of doing this.
1229 \subsection{Foundations}
1231 A datatype declaration has the following general structure:
1232 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
1233 C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
1234 C_m(\tau_{m1},\dots,\tau_{mk_m})
1236 where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
1237 $\tau_{ij}$ are one of the following:
1239 \item type variables $\alpha_1,\dots,\alpha_n$,
1240 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared
1241 type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq
1242 \{\alpha_1,\dots,\alpha_n\}$,
1243 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This
1244 makes it a recursive type. To ensure that the new type is not empty at
1245 least one constructor must consist of only non-recursive type
1248 If you would like one of the $\tau_{ij}$ to be a complex type expression
1249 $\tau$ you need to declare a new type synonym $syn = \tau$ first and use
1250 $syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the
1251 recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt
1252 datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[
1253 \mbox{\tt datatype}~ t ~=~ C(t~list). \]
1255 The constructors are automatically defined as functions of their respective
1257 \[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
1258 These functions have certain {\em freeness} properties:
1260 \item[\tt distinct] They are distinct:
1261 \[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad
1262 \mbox{for all}~ i \neq j.
1264 \item[\tt inject] They are injective:
1265 \[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) =
1266 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
1269 Because the number of inequalities is quadratic in the number of
1270 constructors, a different method is used if their number exceeds
1271 a certain value, currently 4. In that case every constructor is mapped to a
1275 \mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\
1277 \mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1
1280 and distinctness of constructors is expressed by:
1282 \mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.
1284 In addition a structural induction axiom {\tt induct} is provided:
1288 \Forall x_1\dots x_{k_1}.
1289 \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
1290 \Imp & P(C_1(x_1,\dots,x_{k_1})) \\
1292 \Forall x_1\dots x_{k_m}.
1293 \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
1294 \Imp & P(C_m(x_1,\dots,x_{k_m}))
1297 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}
1298 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for
1299 all arguments of the recursive type.
1301 The type also comes with an \ML-like \sdx{case}-construct:
1304 \mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
1306 \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
1309 In contrast to \ML, {\em all} constructors must be present, their order is
1310 fixed, and nested patterns are not supported.
1313 \subsection{Defining datatypes}
1315 A datatype is defined in a theory definition file using the keyword {\tt
1316 datatype}. The definition following {\tt datatype} must conform to the
1317 syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must
1318 obey the rules in the previous section. As a result the theory is extended
1319 with the new type, the constructors, and the theorems listed in the previous
1324 typedecl : typevarlist id '=' (cons + '|')
1326 cons : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
1328 typ : typevarlist id
1331 typevarlist : () | tid | '(' (tid + ',') ')'
1334 \caption{Syntax of datatype declarations}
1335 \label{datatype-grammar}
1338 Reading the theory file produces a structure which, in addition to the usual
1339 components, contains a structure named $t$ for each datatype $t$ defined in
1340 the file.\footnote{Otherwise multiple datatypes in the same theory file would
1341 lead to name clashes.} Each structure $t$ contains the following elements:
1343 val distinct : thm list
1344 val inject : thm list
1346 val cases : thm list
1347 val simps : thm list
1348 val induct_tac : string -> int -> tactic
1350 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
1351 above. For convenience {\tt distinct} contains inequalities in both
1354 If there are five or more constructors, the {\em t\_ord} scheme is used for
1355 {\tt distinct}. In this case the theory {\tt Arith} must be contained
1356 in the current theory, if necessary by including it explicitly.
1358 The reduction rules of the {\tt case}-construct are in {\tt cases}. All
1359 theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
1360 {\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em
1361 var i}\/}'' applies structural induction over variable {\em var} to
1365 \subsection{Examples}
1367 \subsubsection{The datatype $\alpha~list$}
1369 We want to define the type $\alpha~list$.\footnote{Of course there is a list
1370 type in HOL already. This is only an example.} To do this we have to build
1371 a new theory that contains the type definition. We start from {\tt HOL}.
1374 datatype 'a list = Nil | Cons ('a, 'a list)
1377 After loading the theory (\verb$use_thy "MyList"$), we can prove
1378 $Cons(x,xs)\neq xs$. First we build a suitable simpset for the simplifier:
1380 val mylist_ss = HOL_ss addsimps MyList.list.simps;
1381 goal MyList.thy "!x. Cons(x,xs) ~= xs";
1383 {\out ! x. Cons(x, xs) ~= xs}
1384 {\out 1. ! x. Cons(x, xs) ~= xs}
1386 This can be proved by the structural induction tactic:
1388 by (MyList.list.induct_tac "xs" 1);
1390 {\out ! x. Cons(x, xs) ~= xs}
1391 {\out 1. ! x. Cons(x, Nil) ~= Nil}
1393 {\out ! x. Cons(x, list) ~= list ==>}
1394 {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
1396 The first subgoal can be proved with the simplifier and the distinctness
1397 axioms which are part of \verb$mylist_ss$.
1399 by (simp_tac mylist_ss 1);
1401 {\out ! x. Cons(x, xs) ~= xs}
1403 {\out ! x. Cons(x, list) ~= list ==>}
1404 {\out ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
1406 Using the freeness axioms we can quickly prove the remaining goal.
1408 by (asm_simp_tac mylist_ss 1);
1410 {\out ! x. Cons(x, xs) ~= xs}
1413 Because both subgoals were proved by almost the same tactic we could have
1414 done that in one step using
1416 by (ALLGOALS (asm_simp_tac mylist_ss));
1420 \subsubsection{The datatype $\alpha~list$ with mixfix syntax}
1422 In this example we define the type $\alpha~list$ again but this time we want
1423 to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
1424 \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
1425 after the constructor declarations as follows:
1428 datatype 'a list = "[]" ("[]")
1429 | "#" ('a, 'a list) (infixr 70)
1432 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
1436 \subsubsection{A datatype for weekdays}
1438 This example shows a datatype that consists of more than four constructors:
1441 datatype days = Mo | Tu | We | Th | Fr | Sa | So
1444 Because there are more than four constructors, the theory must be based on
1445 {\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
1446 the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
1447 it can be proved by the simplifier if \verb$arith_ss$ is used:
1449 val days_ss = arith_ss addsimps Days.days.simps;
1451 goal Days.thy "Mo ~= Tu";
1452 by (simp_tac days_ss 1);
1454 Note that usually it is not necessary to derive these inequalities explicitly
1455 because the simplifier will dispose of them automatically.
1457 \subsection{Primitive recursive functions}
1458 \index{primitive recursion|(}
1461 Datatypes come with a uniform way of defining functions, {\bf primitive
1462 recursion}. Although it is possible to define primitive recursive functions
1463 by asserting their reduction rules as new axioms, e.g.\
1466 consts app :: "['a list,'a list] => 'a list"
1468 app_Nil "app([],ys) = ys"
1469 app_Cons "app(x#xs, ys) = x#app(xs,ys)"
1472 this carries with it the danger of accidentally asserting an inconsistency,
1473 as in \verb$app([],ys) = us$. Therefore primitive recursive functions on
1474 datatypes can be defined with a special syntax:
1477 consts app :: "['a list,'a list] => 'a list"
1478 primrec app MyList.list
1479 app_Nil "app([],ys) = ys"
1480 app_Cons "app(x#xs, ys) = x#app(xs,ys)"
1483 The system will now check that the two rules \verb$app_Nil$ and
1484 \verb$app_Cons$ do indeed form a primitive recursive definition, thus
1485 ensuring that consistency is maintained. For example
1487 primrec app MyList.list
1488 app_Nil "app([],ys) = us"
1492 Extra variables on rhs
1496 The general form of a primitive recursive definition is
1498 primrec {\it function} {\it type}
1499 {\it reduction rules}
1503 \item {\it function} is the name of the function, either as an {\it id} or a
1504 {\it string}. The function must already have been declared.
1505 \item {\it type} is the name of the datatype, either as an {\it id} or in the
1506 long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the
1507 datatype was declared in, and $t$ the name of the datatype. The long form
1508 is required if the {\tt datatype} and the {\tt primrec} sections are in
1510 \item {\it reduction rules} specify one or more named equations of the form
1511 {\it id\/}~{\it string}, where the identifier gives the name of the rule in
1512 the result structure, and {\it string} is a reduction rule of the form \[
1513 f(x_1,\dots,x_m,C(y_1,\dots,y_k),z_1,\dots,z_n) = r \] such that $C$ is a
1514 constructor of the datatype, $r$ contains only the free variables on the
1515 left-hand side, and all recursive calls in $r$ are of the form
1516 $f(\dots,y_i,\dots)$ for some $i$. There must be exactly one reduction
1517 rule for each constructor.
1519 A theory file may contain any number of {\tt primrec} sections which may be
1520 intermixed with other declarations.
1522 For the consistency-sensitive user it may be reassuring to know that {\tt
1523 primrec} does not assert the reduction rules as new axioms but derives them
1524 as theorems from an explicit definition of the recursive function in terms of
1525 a recursion operator on the datatype.
1527 The primitive recursive function can also use infix or mixfix syntax:
1530 consts "@" :: "['a list,'a list] => 'a list" (infixr 60)
1531 primrec "op @" MyList.list
1532 app_Nil "[] @ ys = ys"
1533 app_Cons "(x#xs) @ ys = x#(xs @ ys)"
1537 The reduction rules become part of the ML structure \verb$Append$ and can
1538 be used to prove theorems about the function:
1540 val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];
1542 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
1543 by (MyList.list.induct_tac "xs" 1);
1544 by (ALLGOALS(asm_simp_tac append_ss));
1547 %Note that underdefined primitive recursive functions are allowed:
1550 %consts tl :: "'a list => 'a list"
1551 %primrec tl MyList.list
1552 % tl_Cons "tl(x#xs) = xs"
1555 %Nevertheless {\tt tl} is total, although we do not know what the result of
1558 \index{primitive recursion|)}
1562 \section{Inductive and coinductive definitions}
1563 \index{*inductive|(}
1564 \index{*coinductive|(}
1566 An {\bf inductive definition} specifies the least set closed under given
1567 rules. For example, a structural operational semantics is an inductive
1568 definition of an evaluation relation. Dually, a {\bf coinductive
1569 definition} specifies the greatest set closed under given rules. An
1570 important example is using bisimulation relations to formalize equivalence
1571 of processes and infinite data structures.
1573 A theory file may contain any number of inductive and coinductive
1574 definitions. They may be intermixed with other declarations; in
1575 particular, the (co)inductive sets {\bf must} be declared separately as
1576 constants, and may have mixfix syntax or be subject to syntax translations.
1578 Each (co)inductive definition adds definitions to the theory and also
1579 proves some theorems. Each definition creates an ML structure, which is a
1580 substructure of the main theory structure.
1582 This package is derived from the ZF one, described in a
1583 separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
1584 longer version is distributed with Isabelle.} which you should refer to
1585 in case of difficulties. The package is simpler than ZF's, thanks to HOL's
1586 automatic type-checking. The type of the (co)inductive determines the
1587 domain of the fixedpoint definition, and the package does not use inference
1588 rules for type-checking.
1591 \subsection{The result structure}
1592 Many of the result structure's components have been discussed in the paper;
1593 others are self-explanatory.
1595 \item[\tt thy] is the new theory containing the recursive sets.
1597 \item[\tt defs] is the list of definitions of the recursive sets.
1599 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
1601 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
1602 the recursive sets, in the case of mutual recursion).
1604 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1605 the recursive sets. The rules are also available individually, using the
1606 names given them in the theory file.
1608 \item[\tt elim] is the elimination rule.
1610 \item[\tt mk\_cases] is a function to create simplified instances of {\tt
1611 elim}, using freeness reasoning on some underlying datatype.
1614 For an inductive definition, the result structure contains two induction rules,
1615 {\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
1616 contains the rule \verb|coinduct|.
1618 Figure~\ref{def-result-fig} summarizes the two result signatures,
1619 specifying the types of all these components.
1628 val intrs : thm list
1630 val mk_cases : thm list -> string -> thm
1631 {\it(Inductive definitions only)}
1633 val mutual_induct: thm
1634 {\it(Coinductive definitions only)}
1639 \caption{The result of a (co)inductive definition} \label{def-result-fig}
1642 \subsection{The syntax of a (co)inductive definition}
1643 An inductive definition has the form
1645 inductive {\it inductive sets}
1646 intrs {\it introduction rules}
1647 monos {\it monotonicity theorems}
1648 con_defs {\it constructor definitions}
1650 A coinductive definition is identical, except that it starts with the keyword
1653 The {\tt monos} and {\tt con\_defs} sections are optional. If present,
1654 each is specified as a string, which must be a valid ML expression of type
1655 {\tt thm list}. It is simply inserted into the {\tt .thy.ML} file; if it
1656 is ill-formed, it will trigger ML error messages. You can then inspect the
1657 file on your directory.
1660 \item The {\it inductive sets} are specified by one or more strings.
1662 \item The {\it introduction rules} specify one or more introduction rules in
1663 the form {\it ident\/}~{\it string}, where the identifier gives the name of
1664 the rule in the result structure.
1666 \item The {\it monotonicity theorems} are required for each operator
1667 applied to a recursive set in the introduction rules. There {\bf must}
1668 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
1669 premise $t\in M(R_i)$ in an introduction rule!
1671 \item The {\it constructor definitions} contain definitions of constants
1672 appearing in the introduction rules. In most cases it can be omitted.
1675 The package has a few notable restrictions:
1677 \item The theory must separately declare the recursive sets as
1680 \item The names of the recursive sets must be identifiers, not infix
1683 \item Side-conditions must not be conjunctions. However, an introduction rule
1684 may contain any number of side-conditions.
1686 \item Side-conditions of the form $x=t$, where the variable~$x$ does not
1687 occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
1691 \subsection{Example of an inductive definition}
1692 Two declarations, included in a theory file, define the finite powerset
1693 operator. First we declare the constant~{\tt Fin}. Then we declare it
1694 inductively, with two introduction rules:
1696 consts Fin :: "'a set => 'a set set"
1699 emptyI "{} : Fin(A)"
1700 insertI "[| a: A; b: Fin(A) |] ==> insert(a,b) : Fin(A)"
1702 The resulting theory structure contains a substructure, called~{\tt Fin}.
1703 It contains the {\tt Fin}$(A)$ introduction rules as the list {\tt Fin.intrs},
1704 and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
1705 rule is {\tt Fin.induct}.
1707 For another example, here is a theory file defining the accessible part of a
1708 relation. The main thing to note is the use of~{\tt Pow} in the sole
1709 introduction rule, and the corresponding mention of the rule
1710 \verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version
1711 of this example in more detail.
1714 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
1715 acc :: "('a * 'a)set => 'a set" (*Accessible part*)
1716 defs pred_def "pred(x,r) == {y. <y,x>:r}"
1719 pred "pred(a,r): Pow(acc(r)) ==> a: acc(r)"
1723 The HOL distribution contains many other inductive definitions, such as the
1724 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The
1725 theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
1727 \index{*coinductive|)} \index{*inductive|)} \underscoreoff
1730 \section{The examples directories}
1731 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
1732 substitutions and unifiers. It is based on Paulson's previous
1733 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1736 Directory {\tt HOL/IMP} contains a mechanised version of a semantic
1737 equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
1738 denotational and operational semantics of a simple while-language, then
1739 proves the two equivalent. It contains several datatype and inductive
1740 definitions, and demonstrates their use.
1742 Directory {\tt HOL/ex} contains other examples and experimental proofs in
1743 {\HOL}. Here is an overview of the more interesting files.
1745 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
1746 predicate calculus theorems, ranging from simple tautologies to
1747 moderately difficult problems involving equality and quantifiers.
1749 \item File {\tt meson.ML} contains an experimental implementation of the {\sc
1750 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1751 much more powerful than Isabelle's classical reasoner. But it is less
1752 useful in practice because it works only for pure logic; it does not
1753 accept derived rules for the set theory primitives, for example.
1755 \item File {\tt mesontest.ML} contains test data for the {\sc meson} proof
1756 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1758 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in
1759 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1761 \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
1762 insertion sort and quick sort.
1764 \item The definition of lazy lists demonstrates methods for handling
1765 infinite data structures and coinduction in higher-order
1766 logic~\cite{paulson-coind}. Theory \thydx{LList} defines an operator for
1767 corecursion on lazy lists, which is used to define a few simple functions
1768 such as map and append. Corecursion cannot easily define operations such
1769 as filter, which can compute indefinitely before yielding the next
1770 element (if any!) of the lazy list. A coinduction principle is defined
1771 for proving equations on lazy lists.
1773 \item Theory {\tt PropLog} proves the soundness and completeness of
1774 classical propositional logic, given a truth table semantics. The only
1775 connective is $\imp$. A Hilbert-style axiom system is specified, and its
1776 set of theorems defined inductively. A similar proof in \ZF{} is
1777 described elsewhere~\cite{paulson-set-II}.
1779 \item Theory {\tt Term} develops an experimental recursive type definition;
1780 the recursion goes through the type constructor~\tydx{list}.
1782 \item Theory {\tt Simult} constructs mutually recursive sets of trees and
1783 forests, including induction and recursion rules.
1785 \item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of
1786 Milner and Tofte's coinduction example~\cite{milner-coind}. This
1787 substantial proof concerns the soundness of a type system for a simple
1788 functional language. The semantics of recursion is given by a cyclic
1789 environment, which makes a coinductive argument appropriate.
1794 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
1795 Cantor's Theorem states that every set has more subsets than it has
1796 elements. It has become a favourite example in higher-order logic since
1797 it is so easily expressed:
1798 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1799 \forall x::\alpha. f(x) \not= S
1802 Viewing types as sets, $\alpha\To bool$ represents the powerset
1803 of~$\alpha$. This version states that for every function from $\alpha$ to
1804 its powerset, some subset is outside its range.
1806 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1807 the operator \cdx{range}. The set~$S$ is given as an unknown instead of a
1808 quantified variable so that we may inspect the subset found by the proof.
1810 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1812 {\out ~ ?S : range(f)}
1813 {\out 1. ~ ?S : range(f)}
1815 The first two steps are routine. The rule \tdx{rangeE} replaces
1816 $\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
1818 by (resolve_tac [notI] 1);
1820 {\out ~ ?S : range(f)}
1821 {\out 1. ?S : range(f) ==> False}
1823 by (eresolve_tac [rangeE] 1);
1825 {\out ~ ?S : range(f)}
1826 {\out 1. !!x. ?S = f(x) ==> False}
1828 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1829 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1832 by (eresolve_tac [equalityCE] 1);
1834 {\out ~ ?S : range(f)}
1835 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1836 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1838 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
1839 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1840 $\Var{P}(\Var{c})$. Destruct-resolution using \tdx{CollectD}
1841 instantiates~$\Var{S}$ and creates the new assumption.
1843 by (dresolve_tac [CollectD] 1);
1845 {\out ~ \{x. ?P7(x)\} : range(f)}
1846 {\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
1847 {\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
1849 Forcing a contradiction between the two assumptions of subgoal~1 completes
1850 the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, which
1851 is the standard diagonal construction.
1855 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1856 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1858 The rest should be easy. To apply \tdx{CollectI} to the negated
1859 assumption, we employ \ttindex{swap_res_tac}:
1861 by (swap_res_tac [CollectI] 1);
1863 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1864 {\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
1868 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1871 How much creativity is required? As it happens, Isabelle can prove this
1872 theorem automatically. The classical set \ttindex{set_cs} contains rules
1873 for most of the constructs of \HOL's set theory. We must augment it with
1874 \tdx{equalityCE} to break up set equalities, and then apply best-first
1875 search. Depth-first search would diverge, but best-first search
1876 successfully navigates through the large search space.
1877 \index{search!best-first}
1881 {\out ~ ?S : range(f)}
1882 {\out 1. ~ ?S : range(f)}
1884 by (best_tac (set_cs addSEs [equalityCE]) 1);
1886 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1890 \index{higher-order logic|)}