2 \chapter{Higher-order logic}
3 The directory~\ttindexbold{HOL} contains a theory for higher-order logic
4 based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is based on
5 Church~\cite{church40}. Andrews~\cite{andrews86} is a full description of
6 higher-order logic. Gordon's work has demonstrated that higher-order logic
7 is useful for hardware verification; beyond this, it is widely applicable
8 in many areas of mathematics. It is weaker than {\ZF} set theory but for
9 most applications this does not matter. If you prefer {\ML} to Lisp, you
10 will probably prefer {\HOL} to~{\ZF}.
12 Previous releases of Isabelle included a completely different version
13 of~{\HOL}, with explicit type inference rules~\cite{paulson-COLOG}. This
14 version no longer exists, but \ttindex{ZF} supports a similar style of
17 {\HOL} has a distinct feel, compared with {\ZF} and {\CTT}. It
18 identifies object-level types with meta-level types, taking advantage of
19 Isabelle's built-in type checker. It identifies object-level functions
20 with meta-level functions, so it uses Isabelle's operations for abstraction
21 and application. There is no ``apply'' operator: function applications are
22 written as simply~$f(a)$ rather than $f{\tt`}a$.
24 These identifications allow Isabelle to support {\HOL} particularly nicely,
25 but they also mean that {\HOL} requires more sophistication from the user
26 --- in particular, an understanding of Isabelle's type system. Beginners
27 should gain experience by working in first-order logic, before attempting
28 to use higher-order logic. This chapter assumes familiarity with~{\FOL{}}.
34 \it name &\it meta-type & \it description \\
35 \idx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
36 \idx{not} & $bool\To bool$ & negation ($\neg$) \\
37 \idx{True} & $bool$ & tautology ($\top$) \\
38 \idx{False} & $bool$ & absurdity ($\bot$) \\
39 \idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
40 \idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion
43 \subcaption{Constants}
47 \begin{tabular}{llrrr}
48 \it symbol &\it name &\it meta-type & \it prec & \it description \\
49 \tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 &
50 Hilbert description ($\epsilon$) \\
51 \idx{!} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
52 universal quantifier ($\forall$) \\
53 \idx{?} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
54 existential quantifier ($\exists$) \\
55 \idx{?!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
56 unique existence ($\exists!$)
62 \begin{tabular}{llrrr}
63 \it symbol &\it name &\it meta-type & \it prec & \it description \\
64 \idx{ALL} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
65 universal quantifier ($\forall$) \\
66 \idx{EX} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
67 existential quantifier ($\exists$) \\
68 \idx{EX!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
69 unique existence ($\exists!$)
72 \subcaption{Alternative quantifiers}
80 \it symbol & \it meta-type & \it precedence & \it description \\
81 \idx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
82 Right 50 & composition ($\circ$) \\
83 \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
84 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
85 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
86 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\
87 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
88 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
89 less than or equals ($\leq$)
93 \caption{Syntax of {\tt HOL}} \label{hol-constants}
100 term & = & \hbox{expression of class~$term$} \\
101 & | & "\at~~" id~id^* " . " formula \\[2ex]
102 formula & = & \hbox{expression of type~$bool$} \\
103 & | & term " = " term \\
104 & | & term " \ttilde= " term \\
105 & | & term " < " term \\
106 & | & term " <= " term \\
107 & | & "\ttilde\ " formula \\
108 & | & formula " \& " formula \\
109 & | & formula " | " formula \\
110 & | & formula " --> " formula \\
111 & | & "!~~~" id~id^* " . " formula \\
112 & | & "?~~~" id~id^* " . " formula \\
113 & | & "?!~~" id~id^* " . " formula \\
114 & | & "ALL~" id~id^* " . " formula \\
115 & | & "EX~~" id~id^* " . " formula \\
116 & | & "EX!~" id~id^* " . " formula
120 \caption{Full grammar for {\HOL}} \label{hol-grammar}
125 Type inference is automatic, exploiting Isabelle's type classes. The class
126 of higher-order terms is called {\it term\/}; type variables range over
127 this class by default. The equality symbol and quantifiers are polymorphic
128 over class {\it term}.
130 Class {\it ord\/} consists of all ordered types; the relations $<$ and
131 $\leq$ are polymorphic over this class, as are the functions
132 \ttindex{mono}, \ttindex{min} and \ttindex{max}. Three other
133 type classes --- {\it plus}, {\it minus\/} and {\it times} --- permit
134 overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
135 {\tt-} is overloaded for set difference and subtraction.
136 \index{*"+}\index{-@{\tt-}}\index{*@{\tt*}}
138 Figure~\ref{hol-constants} lists the constants (including infixes and
139 binders), while Figure~\ref{hol-grammar} presents the grammar. Note that
140 $a$\verb|~=|$b$ is translated to \verb|~(|$a$=$b$\verb|)|.
143 The type of formulae, {\it bool} belongs to class {\it term}; thus,
144 formulae are terms. The built-in type~$fun$, which constructs function
145 types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
146 $\sigma$ and~$\tau$ do; this allows quantification over functions. Types
147 in {\HOL} must be non-empty because of the form of quantifier
148 rules~\cite[\S7]{paulson-COLOG}.
150 Gordon's {\sc hol} system supports {\bf type definitions}. A type is
151 defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
152 bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$
153 specifies a non-empty subset of~$\sigma$, and the new type denotes this
154 subset. New function constants are generated to establish an isomorphism
155 between the new type and the subset. If type~$\sigma$ involves type
156 variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
157 a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
160 Isabelle does not support type definitions at present. Instead, they are
161 mimicked by explicit definitions of isomorphism functions. These should be
162 accompanied by theorems of the form $\exists x::\sigma.P(x)$, but this is
167 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
168 satisfying~$P[a]$, if such exists. Since all terms in {\HOL} denote
169 something, a description is always meaningful, but we do not know its value
170 unless $P[x]$ defines it uniquely. We may write descriptions as
171 \ttindexbold{Eps}($P$) or use the syntax
172 \hbox{\tt \at $x$.$P[x]$}. Existential quantification is defined
174 \[ \exists x.P(x) \equiv P(\epsilon x.P(x)) \]
175 The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
176 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
177 quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
178 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
179 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
181 \index{*"!}\index{*"?}
182 Quantifiers have two notations. As in Gordon's {\sc hol} system, {\HOL}
183 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
184 existential quantifier must be followed by a space; thus {\tt?x} is an
185 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
186 notation for quantifiers, \ttindex{ALL} and \ttindex{EX}, is also
187 available. Both notations are accepted for input. The {\ML} reference
188 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
189 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
190 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
193 Although the description operator does not usually allow iteration of the
194 form \hbox{\tt \at $x@1 \dots x@n$.$P[x@1,\dots,x@n]$}, there are cases where
195 this is legal. If \hbox{\tt \at $y$.$P[x,y]$} is of type~{\it bool},
196 then \hbox{\tt \at $x\,y$.$P[x,y]$} is legal. The pretty printer will
197 display \hbox{\tt \at $x$.\at $y$.$P[x,y]$} as
198 \hbox{\tt \at $x\,y$.$P[x,y]$}.
201 \begin{figure} \makeatother
204 \idx{subst} [| s=t; P(s) |] ==> P(t::'a)
205 \idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))
206 \idx{impI} (P ==> Q) ==> P-->Q
207 \idx{mp} [| P-->Q; P |] ==> Q
208 \idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
209 \idx{selectI} P(x::'a) ==> P(@x.P(x))
210 \idx{True_or_False} (P=True) | (P=False)
211 \subcaption{basic rules}
213 \idx{True_def} True = ((%x.x)=(%x.x))
214 \idx{All_def} All = (%P. P = (%x.True))
215 \idx{Ex_def} Ex = (%P. P(@x.P(x)))
216 \idx{False_def} False = (!P.P)
217 \idx{not_def} not = (%P. P-->False)
218 \idx{and_def} op & = (%P Q. !R. (P-->Q-->R) --> R)
219 \idx{or_def} op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)
220 \idx{Ex1_def} Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))
221 \subcaption{Definitions of the logical constants}
223 \idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y)
224 \idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x)))
225 \idx{if_def} if = (%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
226 \subcaption{Further definitions}
228 \caption{Rules of {\tt HOL}} \label{hol-rules}
232 \begin{figure} \makeatother
234 \idx{sym} s=t ==> t=s
235 \idx{trans} [| r=s; s=t |] ==> r=t
236 \idx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
237 \idx{box_equals} [| a=b; a=c; b=d |] ==> c=d
238 \idx{arg_cong} s=t ==> f(s)=f(t)
239 \idx{fun_cong} s::'a=>'b = t ==> s(x)=t(x)
240 \subcaption{Equality}
243 \idx{FalseE} False ==> P
245 \idx{conjI} [| P; Q |] ==> P&Q
246 \idx{conjunct1} [| P&Q |] ==> P
247 \idx{conjunct2} [| P&Q |] ==> Q
248 \idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
250 \idx{disjI1} P ==> P|Q
251 \idx{disjI2} Q ==> P|Q
252 \idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
254 \idx{notI} (P ==> False) ==> ~ P
255 \idx{notE} [| ~ P; P |] ==> R
256 \idx{impE} [| P-->Q; P; Q ==> R |] ==> R
257 \subcaption{Propositional logic}
259 \idx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
260 \idx{iffD1} [| P=Q; P |] ==> Q
261 \idx{iffD2} [| P=Q; Q |] ==> P
262 \idx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
264 \idx{eqTrueI} P ==> P=True
265 \idx{eqTrueE} P=True ==> P
266 \subcaption{Logical equivalence}
269 \caption{Derived rules for {\HOL}} \label{hol-lemmas1}
273 \begin{figure} \makeatother
275 \idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
276 \idx{spec} !x::'a.P(x) ==> P(x)
277 \idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
278 \idx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
280 \idx{exI} P(x) ==> ? x::'a.P(x)
281 \idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
283 \idx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
284 \idx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
287 \idx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
288 \subcaption{Quantifiers and descriptions}
290 \idx{ccontr} (~P ==> False) ==> P
291 \idx{classical} (~P ==> P) ==> P
292 \idx{excluded_middle} ~P | P
294 \idx{disjCI} (~Q ==> P) ==> P|Q
295 \idx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
296 \idx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
297 \idx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
298 \idx{notnotD} ~~P ==> P
299 \idx{swap} ~P ==> (~Q ==> P) ==> Q
300 \subcaption{Classical logic}
302 \idx{if_True} if(True,x,y) = x
303 \idx{if_False} if(False,x,y) = y
304 \idx{if_P} P ==> if(P,x,y) = x
305 \idx{if_not_P} ~ P ==> if(P,x,y) = y
306 \idx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
307 \subcaption{Conditionals}
309 \caption{More derived rules} \label{hol-lemmas2}
313 \section{Rules of inference}
314 The basic theory has the {\ML} identifier \ttindexbold{HOL.thy}. However,
315 many further theories are defined, introducing product and sum types, the
316 natural numbers, etc.
318 Figure~\ref{hol-rules} shows the inference rules with their~{\ML} names.
319 They follow standard practice in higher-order logic: only a few connectives
320 are taken as primitive, with the remainder defined obscurely.
322 Unusually, the definitions use object-equality~({\tt=}) rather than
323 meta-equality~({\tt==}). This is possible because equality in higher-order
324 logic may equate formulae and even functions over formulae. On the other
325 hand, meta-equality is Isabelle's usual symbol for making definitions.
326 Take care to note which form of equality is used before attempting a proof.
328 Some of the rules mention type variables; for example, {\tt refl} mentions
329 the type variable~{\tt'a}. This facilitates explicit instantiation of the
330 type variables. By default, such variables range over class {\it term}.
333 Where function types are involved, Isabelle's unification code does not
334 guarantee to find instantiations for type variables automatically. If
335 resolution fails for no obvious reason, try setting \ttindex{show_types} to
336 {\tt true}, causing Isabelle to display types of terms. (Possibly, set
337 \ttindex{show_sorts} to {\tt true} also, causing Isabelle to display sorts.)
338 Be prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}.
339 Setting \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to
340 report omitted search paths during unification.
343 Here are further comments on the rules:
345 \item[\ttindexbold{ext}]
346 expresses extensionality of functions.
347 \item[\ttindexbold{iff}]
348 asserts that logically equivalent formulae are equal.
349 \item[\ttindexbold{selectI}]
350 gives the defining property of the Hilbert $\epsilon$-operator. The
351 derived rule \ttindexbold{select_equality} (see below) is often easier to use.
352 \item[\ttindexbold{True_or_False}]
353 makes the logic classical.\footnote{In fact, the $\epsilon$-operator
354 already makes the logic classical, as shown by Diaconescu;
355 see Paulson~\cite{paulson-COLOG} for details.}
359 {\HOL} has no if-and-only-if connective; logical equivalence is expressed
360 using equality. But equality has a high precedence, as befitting a
361 relation, while if-and-only-if typically has the lowest precedence. Thus,
362 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. When
363 using $=$ to mean logical equivalence, enclose both operands in
367 Some derived rules are shown in Figures~\ref{hol-lemmas1}
368 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
369 for the logical connectives, as well as sequent-style elimination rules for
370 conjunctions, implications, and universal quantifiers.
372 Note the equality rules: \ttindexbold{ssubst} performs substitution in
373 backward proofs, while \ttindexbold{box_equals} supports reasoning by
374 simplifying both sides of an equation.
376 See the files \ttindexbold{HOL/hol.thy} and
377 \ttindexbold{HOL/hol.ML} for complete listings of the rules and
381 \section{Generic packages}
382 {\HOL} instantiates most of Isabelle's generic packages;
383 see \ttindexbold{HOL/ROOT.ML} for details.
386 Because it includes a general substitution rule, {\HOL} instantiates the
387 tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
388 throughout a subgoal and its hypotheses.
390 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
391 simplification set for higher-order logic. Equality~($=$), which also
392 expresses logical equivalence, may be used for rewriting. See the file
393 \ttindexbold{HOL/simpdata.ML} for a complete listing of the simplification
396 It instantiates the classical reasoning module. See~\S\ref{hol-cla-prover}
404 \it name &\it meta-type & \it description \\
405 \index{"{"}@{\tt\{\}}}
406 {\tt\{\}} & $\alpha\,set$ & the empty set \\
407 \idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
408 & insertion of element \\
409 \idx{Collect} & $(\alpha\To bool)\To\alpha\,set$
411 \idx{Compl} & $(\alpha\,set)\To\alpha\,set$
413 \idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
414 & intersection over a set\\
415 \idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
417 \idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
418 &set of sets intersection \\
419 \idx{Union} & $((\alpha\,set)set)\To\alpha\,set$
420 &set of sets union \\
421 \idx{range} & $(\alpha\To\beta )\To\beta\,set$
422 & range of a function \\[1ex]
423 \idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
424 & bounded quantifiers \\
425 \idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
427 \idx{inj}~~\idx{surj}& $(\alpha\To\beta )\To bool$
428 & injective/surjective \\
429 \idx{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 prec & \it description \\
438 \idx{INT} & \idx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
439 intersection over a type\\
440 \idx{UN} & \idx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
450 \begin{tabular}{rrrr}
451 \it symbol & \it meta-type & \it precedence & \it description \\
452 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
454 \idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
455 & Left 70 & intersection ($\inter$) \\
456 \idx{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 {\HOL}'s set theory} \label{hol-set-syntax}
470 \begin{center} \tt\frenchspacing
472 \it external & \it internal & \it description \\
473 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
474 \{$a@1$, $\ldots$, $a@n$\} & insert($a@1$,$\cdots$,insert($a@n$,0)) &
476 \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
478 \idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
479 \rm intersection over a set \\
480 \idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
481 \rm union over a set \\
482 \idx{!} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
483 \rm bounded $\forall$ \\
484 \idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
485 \rm bounded $\exists$ \\[1ex]
486 \idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
487 \rm bounded $\forall$ \\
488 \idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
489 \rm bounded $\exists$
492 \subcaption{Translations}
496 term & = & \hbox{other terms\ldots} \\
498 & | & "\{ " term\; ("," term)^* " \}" \\
499 & | & "\{ " id " . " formula " \}" \\
500 & | & term " `` " term \\
501 & | & term " Int " term \\
502 & | & term " Un " term \\
503 & | & "INT~~" id ":" term " . " term \\
504 & | & "UN~~~" id ":" term " . " term \\
505 & | & "INT~~" id~id^* " . " term \\
506 & | & "UN~~~" id~id^* " . " term \\[2ex]
507 formula & = & \hbox{other formulae\ldots} \\
508 & | & term " : " term \\
509 & | & term " \ttilde: " term \\
510 & | & term " <= " term \\
511 & | & "!~~~" id ":" term " . " formula \\
512 & | & "?~~~" id ":" term " . " formula \\
513 & | & "ALL " id ":" term " . " formula \\
514 & | & "EX~~" id ":" term " . " formula
517 \subcaption{Full Grammar}
518 \caption{Syntax of {\HOL}'s set theory (continued)} \label{hol-set-syntax2}
522 \begin{figure} \makeatother
524 \idx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
525 \idx{Collect_mem_eq} \{x.x:A\} = A
526 \subcaption{Isomorphisms between predicates and sets}
528 \idx{empty_def} \{\} == \{x.x= False\}
529 \idx{insert_def} insert(a,B) == \{x.x=a\} Un B
530 \idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
531 \idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
532 \idx{subset_def} A <= B == ! x:A. x:B
533 \idx{Un_def} A Un B == \{x.x:A | x:B\}
534 \idx{Int_def} A Int B == \{x.x:A & x:B\}
535 \idx{set_diff_def} A - B == \{x.x:A & x~:B\}
536 \idx{Compl_def} Compl(A) == \{x. ~ x:A\}
537 \idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
538 \idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
539 \idx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
540 \idx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
541 \idx{Inter_def} Inter(S) == (INT x:S. x)
542 \idx{Union_def} Union(S) == (UN x:S. x)
543 \idx{image_def} f``A == \{y. ? x:A. y=f(x)\}
544 \idx{range_def} range(f) == \{y. ? x. y=f(x)\}
545 \idx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
546 \idx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
547 \idx{surj_def} surj(f) == ! y. ? x. y=f(x)
548 \idx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
549 \subcaption{Definitions}
551 \caption{Rules of {\HOL}'s set theory} \label{hol-set-rules}
555 \begin{figure} \makeatother
557 \idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
558 \idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
559 \idx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
560 \idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
561 \subcaption{Comprehension}
563 \idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
564 \idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
565 \idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
566 \idx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
567 (! x:A. P(x)) = (! x:A'. P'(x))
569 \idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
570 \idx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
571 \idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
572 \subcaption{Bounded quantifiers}
574 \idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
575 \idx{subsetD} [| A <= B; c:A |] ==> c:B
576 \idx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
578 \idx{subset_refl} A <= A
579 \idx{subset_antisym} [| A <= B; B <= A |] ==> A = B
580 \idx{subset_trans} [| A<=B; B<=C |] ==> A<=C
582 \idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
583 \idx{equalityD1} A = B ==> A<=B
584 \idx{equalityD2} A = B ==> B<=A
585 \idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
587 \idx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
588 [| ~ c:A; ~ c:B |] ==> P
590 \subcaption{The subset and equality relations}
592 \caption{Derived rules for set theory} \label{hol-set1}
596 \begin{figure} \makeatother
598 \idx{emptyE} a : \{\} ==> P
600 \idx{insertI1} a : insert(a,B)
601 \idx{insertI2} a : B ==> a : insert(b,B)
602 \idx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==>
604 \idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
605 \idx{ComplD} [| c : Compl(A) |] ==> ~ c:A
607 \idx{UnI1} c:A ==> c : A Un B
608 \idx{UnI2} c:B ==> c : A Un B
609 \idx{UnCI} (~c:B ==> c:A) ==> c : A Un B
610 \idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
612 \idx{IntI} [| c:A; c:B |] ==> c : A Int B
613 \idx{IntD1} c : A Int B ==> c:A
614 \idx{IntD2} c : A Int B ==> c:B
615 \idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
617 \idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
618 \idx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
620 \idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
621 \idx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
622 \idx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
624 \idx{UnionI} [| X:C; A:X |] ==> A : Union(C)
625 \idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
627 \idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
628 \idx{InterD} [| A : Inter(C); X:C |] ==> A:X
629 \idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
631 \caption{Further derived rules for set theory} \label{hol-set2}
635 \section{A formulation of set theory}
636 Historically, higher-order logic gives a foundation for Russell and
637 Whitehead's theory of classes. Let us use modern terminology and call them
638 {\bf sets}, but note that these sets are distinct from those of {\ZF} set
639 theory, and behave more like {\ZF} classes.
642 Sets are given by predicates over some type~$\sigma$. Types serve to
643 define universes for sets, but type checking is still significant.
645 There is a universal set (for each type). Thus, sets have complements, and
646 may be defined by absolute comprehension.
648 Although sets may contain other sets as elements, the containing set must
649 have a more complex type.
651 Finite unions and intersections have the same behaviour in {\HOL} as they
652 do in~{\ZF}. In {\HOL} the intersection of the empty set is well-defined,
653 denoting the universal set for the given type.
655 \subsection{Syntax of set theory}
656 The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The new
657 type is defined for clarity and to avoid complications involving function
658 types in unification. Since Isabelle does not support type definitions (as
659 discussed above), the isomorphisms between the two types are declared
660 explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
661 $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
664 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
665 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
666 constructs. Infix operators include union and intersection ($A\union B$
667 and $A\inter B$), the subset and membership relations, and the image
668 operator~{\tt``}. Note that $a$\verb|~:|$b$ is translated to
669 \verb|~(|$a$:$b$\verb|)|. The {\tt\{\ldots\}} notation abbreviates finite
670 sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the
673 \{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\emptyset)))
676 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
677 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
678 occurrences of~$x$. This syntax expands to \ttindexbold{Collect}$(\lambda
681 The set theory defines two {\bf bounded quantifiers}:
683 \forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\
684 \exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]
686 The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined
687 accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
688 write\index{*"!}\index{*"?}\index{*ALL}\index{*EX}
689 \hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.
690 Isabelle's usual notation, \ttindex{ALL} and \ttindex{EX}, is also
692 ordinary quantifiers, the contents of \ttindexbold{HOL_quantifiers} specifies
693 which notation should be used for output.
695 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
696 $\bigcap@{x\in A}B[x]$, are written
697 \ttindexbold{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
698 \ttindexbold{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
699 Unions and intersections over types, namely $\bigcup@x B[x]$ and
700 $\bigcap@x B[x]$, are written
701 \ttindexbold{UN}~\hbox{\tt$x$.$B[x]$} and
702 \ttindexbold{INT}~\hbox{\tt$x$.$B[x]$}; they are equivalent to the previous
703 union/intersection operators when $A$ is the universal set.
704 The set of set union and intersection operators ($\bigcup A$ and $\bigcap
705 A$) are not binders, but equals $\bigcup@{x\in A}x$ and $\bigcap@{x\in
708 \subsection{Axioms and rules of set theory}
709 The axioms \ttindexbold{mem_Collect_eq} and
710 \ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and
711 \hbox{\tt op :} are isomorphisms.
712 All the other axioms are definitions; see Figure~\ref{hol-set-rules}.
713 These include straightforward properties of functions: image~({\tt``}) and
714 {\tt range}, and predicates concerning monotonicity, injectiveness, etc.
716 {\HOL}'s set theory has the {\ML} identifier \ttindexbold{Set.thy}.
718 \begin{figure} \makeatother
720 \idx{imageI} [| x:A |] ==> f(x) : f``A
721 \idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
723 \idx{rangeI} f(x) : range(f)
724 \idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
726 \idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
727 \idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
729 \idx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
730 \idx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
731 \idx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
733 \idx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
734 \idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
737 [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
740 (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
742 \idx{inj_onto_inverseI}
743 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
746 [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
748 \idx{inj_onto_contraD}
749 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
751 \caption{Derived rules involving functions} \label{hol-fun}
755 \begin{figure} \makeatother
757 \idx{Union_upper} B:A ==> B <= Union(A)
758 \idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
760 \idx{Inter_lower} B:A ==> Inter(A) <= B
761 \idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
763 \idx{Un_upper1} A <= A Un B
764 \idx{Un_upper2} B <= A Un B
765 \idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
767 \idx{Int_lower1} A Int B <= A
768 \idx{Int_lower2} A Int B <= B
769 \idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
771 \caption{Derived rules involving subsets} \label{hol-subset}
775 \begin{figure} \makeatother
777 \idx{Int_absorb} A Int A = A
778 \idx{Int_commute} A Int B = B Int A
779 \idx{Int_assoc} (A Int B) Int C = A Int (B Int C)
780 \idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
782 \idx{Un_absorb} A Un A = A
783 \idx{Un_commute} A Un B = B Un A
784 \idx{Un_assoc} (A Un B) Un C = A Un (B Un C)
785 \idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
787 \idx{Compl_disjoint} A Int Compl(A) = \{x.False\}
788 \idx{Compl_partition} A Un Compl(A) = \{x.True\}
789 \idx{double_complement} Compl(Compl(A)) = A
790 \idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
791 \idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
793 \idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
794 \idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C)
796 (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
798 \idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
799 \idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C)
800 \idx{Int_Inter_image}
801 (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
803 \caption{Set equalities} \label{hol-equalities}
807 \subsection{Derived rules for sets}
808 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most
809 are obvious and resemble rules of Isabelle's {\ZF} set theory. The
810 rules named $XXX${\tt_cong} break down equalities. Certain rules, such as
811 \ttindexbold{subsetCE}, \ttindexbold{bexCI} and \ttindexbold{UnCI}, are
812 designed for classical reasoning; the more natural rules \ttindexbold{subsetD},
813 \ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not
814 strictly necessary. Similarly, \ttindexbold{equalityCE} supports classical
815 reasoning about extensionality, after the fashion of \ttindex{iffCE}. See
816 the file \ttindexbold{HOL/set.ML} for proofs pertaining to set theory.
818 Figure~\ref{hol-fun} presents derived rules involving functions. See
819 the file \ttindexbold{HOL/fun.ML} for a complete listing.
821 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
822 See \ttindexbold{HOL/subset.ML}.
824 Figure~\ref{hol-equalities} presents set equalities. See
825 \ttindexbold{HOL/equalities.ML}.
828 \begin{figure} \makeatother
831 \it name &\it meta-type & \it description \\
832 \idx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
833 & ordered pairs $\langle a,b\rangle$ \\
834 \idx{fst} & $\alpha\times\beta \To \alpha$ & first projection\\
835 \idx{snd} & $\alpha\times\beta \To \beta$ & second projection\\
836 \idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
837 & generalized projection
840 \subcaption{Constants}
843 \idx{fst_def} fst(p) == @a. ? b. p = <a,b>
844 \idx{snd_def} snd(p) == @b. ? a. p = <a,b>
845 \idx{split_def} split(p,c) == c(fst(p),snd(p))
846 \subcaption{Definitions}
848 \idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
850 \idx{fst} fst(<a,b>) = a
851 \idx{snd} snd(<a,b>) = b
852 \idx{split} split(<a,b>, c) = c(a,b)
854 \idx{surjective_pairing} p = <fst(p),snd(p)>
855 \subcaption{Derived rules}
857 \caption{Type $\alpha\times\beta$}
862 \begin{figure} \makeatother
865 \it name &\it meta-type & \it description \\
866 \idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\
867 \idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\
868 \idx{case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
872 \subcaption{Constants}
875 \idx{case_def} case == (%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
876 (!y. p=Inr(y) --> z=g(y)))
877 \subcaption{Definition}
879 \idx{Inl_not_Inr} ~ Inl(a)=Inr(b)
881 \idx{inj_Inl} inj(Inl)
882 \idx{inj_Inr} inj(Inr)
884 \idx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
886 \idx{case_Inl} case(Inl(x), f, g) = f(x)
887 \idx{case_Inr} case(Inr(x), f, g) = g(x)
889 \idx{surjective_sum} case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
890 \subcaption{Derived rules}
892 \caption{Rules for type $\alpha+\beta$}
898 The basic higher-order logic is augmented with a tremendous amount of
899 material, including support for recursive function and type definitions.
900 Space does not permit a detailed discussion. The present section describes
901 product, sum, natural number and list types.
903 \subsection{Product and sum types}
904 {\HOL} defines the product type $\alpha\times\beta$ and the sum type
905 $\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
906 standard constructions (Figures~\ref{hol-prod} and~\ref{hol-sum}). Because
907 Isabelle does not support type definitions, the isomorphisms between these
908 types and their representations are made explicitly.
910 Most of the definitions are suppressed, but observe that the projections
911 and conditionals are defined as descriptions. Their properties are easily
912 proved using \ttindex{select_equality}. See \ttindexbold{HOL/prod.thy} and
913 \ttindexbold{HOL/sum.thy} for details.
915 \begin{figure} \makeatother
919 \it symbol & \it meta-type & \it description \\
920 \idx{0} & $nat$ & zero \\
921 \idx{Suc} & $nat \To nat$ & successor function\\
922 \idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
924 \idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
925 & primitive recursor\\
926 \idx{pred_nat} & $(nat\times nat) set$ & predecessor relation
932 \index{*@{\tt*}|bold}
933 \index{/@{\tt/}|bold}
934 \index{//@{\tt//}|bold}
935 \index{+@{\tt+}|bold}
936 \index{-@{\tt-}|bold}
937 \begin{tabular}{rrrr}
938 \it symbol & \it meta-type & \it precedence & \it description \\
939 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
940 \tt / & $[nat,nat]\To nat$ & Left 70 & division\\
941 \tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\
942 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
943 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
946 \subcaption{Constants and infixes}
949 \idx{nat_case_def} nat_case == (%n a f. @z. (n=0 --> z=a) &
950 (!x. n=Suc(x) --> z=f(x)))
951 \idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
952 \idx{less_def} m<n == <m,n>:pred_nat^+
953 \idx{nat_rec_def} nat_rec(n,c,d) ==
954 wfrec(pred_nat, n, %l g.nat_case(l, c, %m.d(m,g(m))))
956 \idx{add_def} m+n == nat_rec(m, n, %u v.Suc(v))
957 \idx{diff_def} m-n == nat_rec(n, m, %u v. nat_rec(v, 0, %x y.x))
958 \idx{mult_def} m*n == nat_rec(m, 0, %u v. n + v)
959 \idx{mod_def} m//n == wfrec(trancl(pred_nat), m, %j f. if(j<n,j,f(j-n)))
960 \idx{quo_def} m/n == wfrec(trancl(pred_nat),
961 m, %j f. if(j<n,0,Suc(f(j-n))))
962 \subcaption{Definitions}
964 \caption{Defining $nat$, the type of natural numbers} \label{hol-nat1}
968 \begin{figure} \makeatother
970 \idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
972 \idx{Suc_not_Zero} Suc(m) ~= 0
973 \idx{inj_Suc} inj(Suc)
974 \idx{n_not_Suc_n} n~=Suc(n)
975 \subcaption{Basic properties}
977 \idx{pred_natI} <n, Suc(n)> : pred_nat
979 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
981 \idx{nat_case_0} nat_case(0, a, f) = a
982 \idx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
984 \idx{wf_pred_nat} wf(pred_nat)
985 \idx{nat_rec_0} nat_rec(0,c,h) = c
986 \idx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
987 \subcaption{Case analysis and primitive recursion}
989 \idx{less_trans} [| i<j; j<k |] ==> i<k
990 \idx{lessI} n < Suc(n)
991 \idx{zero_less_Suc} 0 < Suc(n)
993 \idx{less_not_sym} n<m --> ~ m<n
994 \idx{less_not_refl} ~ n<n
995 \idx{not_less0} ~ n<0
997 \idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
998 \idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1000 \idx{less_linear} m<n | m=n | n<m
1001 \subcaption{The less-than relation}
1003 \caption{Derived rules for~$nat$} \label{hol-nat2}
1007 \subsection{The type of natural numbers, $nat$}
1008 {\HOL} defines the natural numbers in a roundabout but traditional way.
1009 The axiom of infinity postulates an type~$ind$ of individuals, which is
1010 non-empty and closed under an injective operation. The natural numbers are
1011 inductively generated by choosing an arbitrary individual for~0 and using
1012 the injective operation to take successors. As usual, the isomorphisms
1013 between~$nat$ and its representation are made explicitly.
1015 The definition makes use of a least fixed point operator \ttindex{lfp},
1016 defined using the Knaster-Tarski theorem. This in turn defines an operator
1017 \ttindex{trancl} for taking the transitive closure of a relation. See
1018 files \ttindexbold{HOL/lfp.thy} and \ttindexbold{HOL/trancl.thy} for
1019 details. The definition of~$nat$ resides on \ttindexbold{HOL/nat.thy}.
1021 Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
1022 $\leq$ on the natural numbers. As of this writing, Isabelle provides no
1023 means of verifying that such overloading is sensible. On the other hand,
1024 the {\HOL} theory includes no polymorphic axioms stating general properties
1027 File \ttindexbold{HOL/arith.ML} develops arithmetic on the natural numbers.
1028 It defines addition, multiplication, subtraction, division, and remainder,
1029 proving the theorem $a \bmod b + (a/b)\times b = a$. Division and
1030 remainder are defined by repeated subtraction, which requires well-founded
1031 rather than primitive recursion.
1033 Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion
1034 along arbitrary well-founded relations; see \ttindexbold{HOL/wf.ML} for the
1035 development. The predecessor relation, \ttindexbold{pred_nat}, is shown to
1036 be well-founded; recursion along this relation is primitive recursion,
1037 while its transitive closure is~$<$.
1040 \begin{figure} \makeatother
1042 \begin{tabular}{rrr}
1043 \it symbol & \it meta-type & \it description \\
1044 \idx{Nil} & $\alpha list$ & the empty list\\
1045 \idx{Cons} & $[\alpha, \alpha list] \To \alpha list$
1046 & list constructor\\
1047 \idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1048 \beta]\To\beta] \To \beta$
1050 \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1051 & mapping functional
1054 \subcaption{Constants}
1057 \idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r))
1058 \subcaption{Definition}
1061 [| P(Nil); !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l)
1063 \idx{Cons_not_Nil} ~ Cons(x,xs) = Nil
1064 \idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)
1066 \idx{list_rec_Nil} list_rec(Nil,c,h) = c
1067 \idx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))
1069 \idx{map_Nil} map(f,Nil) = Nil
1070 \idx{map_Cons} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))
1072 \caption{The type of lists and its operations} \label{hol-list}
1076 \subsection{The type constructor for lists, $\alpha\,list$}
1077 {\HOL}'s definition of lists is an example of an experimental method for
1078 handling recursive data types. The details need not concern us here; see
1079 the file \ttindexbold{HOL/list.ML}. Figure~\ref{hol-list} presents the
1080 basic list operations, with their types and properties. In particular,
1081 \ttindexbold{list_rec} is a primitive recursion operator for lists, in the
1082 style of Martin-L\"of type theory. It is derived from well-founded
1083 recursion, a general principle that can express arbitrary total recursive
1087 \subsection{The type constructor for lazy lists, $\alpha\,llist$}
1088 The definition of lazy lists demonstrates methods for handling infinite
1089 data structures and co-induction in higher-order logic. It defines an
1090 operator for co-recursion on lazy lists, which is used to define a few
1091 simple functions such as map and append. Co-recursion cannot easily define
1092 operations such as filter, which can compute indefinitely before yielding
1093 the next element (if any!) of the lazy list. A co-induction principle is
1094 defined for proving equations on lazy lists. See the files
1095 \ttindexbold{HOL/llist.thy} and \ttindexbold{HOL/llist.ML} for the formal
1096 derivations. I have written a report discussing the treatment of lazy
1097 lists, and finite lists also~\cite{paulson-coind}.
1100 \section{Classical proof procedures} \label{hol-cla-prover}
1101 {\HOL} derives classical introduction rules for $\disj$ and~$\exists$, as
1102 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1103 rule (Figure~\ref{hol-lemmas2}).
1105 The classical reasoning module is set up for \HOL, as the structure
1106 \ttindexbold{Classical}. This structure is open, so {\ML} identifiers such
1107 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
1109 {\HOL} defines the following classical rule sets:
1117 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
1118 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
1119 along with the rule~\ttindex{refl}.
1121 \item[\ttindexbold{HOL_cs}]
1122 extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
1123 and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for
1124 unique existence. Search using this is incomplete since quantified
1125 formulae are used at most once.
1127 \item[\ttindexbold{HOL_dup_cs}]
1128 extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
1129 and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as
1130 rules for unique existence. Search using this is complete --- quantified
1131 formulae may be duplicated --- but frequently fails to terminate. It is
1132 generally unsuitable for depth-first search.
1134 \item[\ttindexbold{set_cs}]
1135 extends {\tt HOL_cs} with rules for the bounded quantifiers, subsets,
1136 comprehensions, unions/intersections, complements, finite setes, images and
1140 See the {\em Reference Manual} for more discussion of classical proof
1144 \section{The examples directories}
1145 Directory {\tt Subst} contains Martin Coen's mechanization of a theory of
1146 substitutions and unifiers. It is based on Paulson's previous
1147 mechanization in {\LCF}~\cite{paulson85} of theory Manna and Waldinger's
1150 Directory {\tt ex} contains other examples and experimental proofs in
1151 {\HOL}. Here is an overview of the more interesting files.
1153 \item[\ttindexbold{HOL/ex/meson.ML}]
1154 contains an experimental implementation of the MESON proof procedure,
1155 inspired by Plaisted~\cite{plaisted90}. It is much more powerful than
1156 Isabelle's classical module.
1158 \item[\ttindexbold{HOL/ex/mesontest.ML}]
1159 contains test data for the MESON proof procedure.
1161 \item[\ttindexbold{HOL/ex/set.ML}]
1162 proves Cantor's Theorem (see below) and the Schr\"oder-Bernstein Theorem.
1164 \item[\ttindexbold{HOL/ex/pl.ML}]
1165 proves the soundness and completeness of classical propositional logic,
1166 given a truth table semantics. The only connective is $\imp$. A
1167 Hilbert-style axiom system is specified, and its set of theorems defined
1170 \item[\ttindexbold{HOL/ex/term.ML}]
1171 contains proofs about an experimental recursive type definition;
1172 the recursion goes through the type constructor~$list$.
1174 \item[\ttindexbold{HOL/ex/simult.ML}]
1175 defines primitives for solving mutually recursive equations over sets.
1176 It constructs sets of trees and forests as an example, including induction
1177 and recursion rules that handle the mutual recursion.
1179 \item[\ttindexbold{HOL/ex/mt.ML}]
1180 contains Jacob Frost's formalization~\cite{frost93} of a co-induction
1181 example by Milner and Tofte~\cite{milner-coind}.
1185 \section{Example: deriving the conjunction rules}
1186 {\HOL} comes with a body of derived rules, ranging from simple properties
1187 of the logical constants and set theory to well-founded recursion. Many of
1188 them are worth studying.
1190 Deriving natural deduction rules for the logical constants from their
1191 definitions is an archetypal example of higher-order reasoning. Let us
1192 verify two conjunction rules:
1193 \[ \infer[({\conj}I)]{P\conj Q}{P & Q} \qquad\qquad
1194 \infer[({\conj}E1)]{P}{P\conj Q}
1197 \subsection{The introduction rule}
1198 We begin by stating the rule as the goal. The list of premises $[P,Q]$ is
1199 bound to the {\ML} variable~{\tt prems}.
1201 val prems = goal HOL.thy "[| P; Q |] ==> P&Q";
1205 {\out val prems = ["P [P]", "Q [Q]"] : thm list}
1207 The next step is to unfold the definition of conjunction. But
1208 \ttindex{and_def} uses {\HOL}'s internal equality, so
1209 \ttindex{rewrite_goals_tac} is unsuitable.
1210 Instead, we perform substitution using the rule \ttindex{ssubst}:
1212 by (resolve_tac [and_def RS ssubst] 1);
1215 {\out 1. ! R. (P --> Q --> R) --> R}
1217 We now apply $(\forall I)$ and $({\imp}I)$:
1219 by (resolve_tac [allI] 1);
1222 {\out 1. !!R. (P --> Q --> R) --> R}
1223 by (resolve_tac [impI] 1);
1226 {\out 1. !!R. P --> Q --> R ==> R}
1228 The assumption is a nested implication, which may be eliminated
1229 using~\ttindex{mp} resolved with itself. Elim-resolution, here, performs
1230 backwards chaining. More straightforward would be to use~\ttindex{impE}
1234 by (eresolve_tac [mp RS mp] 1);
1240 These two subgoals are simply the premises:
1242 by (REPEAT (resolve_tac prems 1));
1249 \subsection{The elimination rule}
1250 Again, we bind the list of premises (in this case $[P\conj Q]$)
1253 val prems = goal HOL.thy "[| P & Q |] ==> P";
1257 {\out val prems = ["P & Q [P & Q]"] : thm list}
1259 Working with premises that involve defined constants can be tricky. We
1260 must expand the definition of conjunction in the meta-assumption $P\conj
1261 Q$. The rule \ttindex{subst} performs substitution in forward proofs.
1262 We get two resolvents, since the vacuous substitution is valid:
1264 prems RL [and_def RS subst];
1265 {\out val it = ["! R. (P --> Q --> R) --> R [P & Q]",}
1266 {\out "P & Q [P & Q]"] : thm list}
1268 By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of
1269 the vacuous one and put the other into a convenient form:\footnote
1270 {In higher-order logic, {\tt spec RS mp} fails because the resolution yields
1271 two results, namely $\List{\forall x.x; P}\Imp Q$ and $\List{\forall
1272 x.P(x)\imp Q(x); P(x)}\Imp Q(x)$. In first-order logic, the resolution
1273 yields only the latter result.}
1276 prems RL [and_def RS subst] RL [spec] RL [mp];
1277 {\out val it = ["P --> Q --> ?Q ==> ?Q [P & Q]"] : thm list}
1279 This is a list containing a single rule, which is directly applicable to
1282 by (resolve_tac it 1);
1285 {\out 1. P --> Q --> P}
1287 The subgoal is a trivial implication. Recall that \ttindex{ares_tac} is a
1288 combination of \ttindex{assume_tac} and \ttindex{resolve_tac}.
1290 by (REPEAT (ares_tac [impI] 1));
1297 \section{Example: Cantor's Theorem}
1298 Cantor's Theorem states that every set has more subsets than it has
1299 elements. It has become a favourite example in higher-order logic since
1300 it is so easily expressed:
1301 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1302 \forall x::\alpha. f(x) \not= S
1304 Viewing types as sets, $\alpha\To bool$ represents the powerset
1305 of~$\alpha$. This version states that for every function from $\alpha$ to
1306 its powerset, some subset is outside its range.
1308 The Isabelle proof uses {\HOL}'s set theory, with the type $\alpha\,set$ and
1309 the operator \ttindex{range}. Since it avoids quantification, we may
1310 inspect the subset found by the proof.
1312 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1314 {\out ~ ?S : range(f)}
1315 {\out 1. ~ ?S : range(f)}
1317 The first two steps are routine. The rule \ttindex{rangeE} reasons that,
1318 since $\Var{S}\in range(f)$, we have $\Var{S}=f(x)$ for some~$x$.
1320 by (resolve_tac [notI] 1);
1322 {\out ~ ?S : range(f)}
1323 {\out 1. ?S : range(f) ==> False}
1324 by (eresolve_tac [rangeE] 1);
1326 {\out ~ ?S : range(f)}
1327 {\out 1. !!x. ?S = f(x) ==> False}
1329 Next, we apply \ttindex{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1330 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1333 by (eresolve_tac [equalityCE] 1);
1335 {\out ~ ?S : range(f)}
1336 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1337 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1339 Now we use a bit of creativity. Suppose that $\Var{S}$ has the form of a
1340 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1341 $\Var{P}(\Var{c})\}$.\index{*CollectD}
1343 by (dresolve_tac [CollectD] 1);
1345 {\out ~ \{x. ?P7(x)\} : range(f)}
1346 {\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
1347 {\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
1349 Forcing a contradiction between the two assumptions of subgoal~1 completes
1350 the instantiation of~$S$. It is now $\{x. x\not\in f(x)\}$, the standard
1351 diagonal construction.
1355 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1356 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1358 The rest should be easy. To apply \ttindex{CollectI} to the negated
1359 assumption, we employ \ttindex{swap_res_tac}:
1361 by (swap_res_tac [CollectI] 1);
1363 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1364 {\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
1367 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1370 How much creativity is required? As it happens, Isabelle can prove this
1371 theorem automatically. The classical set \ttindex{set_cs} contains rules
1372 for most of the constructs of {\HOL}'s set theory. We augment it with
1373 \ttindex{equalityCE} --- set equalities are not broken up by default ---
1374 and apply best-first search. Depth-first search would diverge, but
1375 best-first search successfully navigates through the large search space.
1379 {\out ~ ?S : range(f)}
1380 {\out 1. ~ ?S : range(f)}
1381 by (best_tac (set_cs addSEs [equalityCE]) 1);
1383 {\out ~ \{x. ~ x : f(x)\} : range(f)}