2 \chapter{Higher-Order logic}
3 The directory~\ttindexbold{HOL} contains a theory for higher-order logic.
4 It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is
5 based on Church~\cite{church40}. Andrews~\cite{andrews86} is a full
6 description of higher-order logic. Gordon's work has demonstrated that
7 higher-order logic is useful for hardware verification; beyond this, it is
8 widely applicable in many areas of mathematics. It is weaker than {\ZF}
9 set theory but for most applications this does not matter. If you prefer
10 {\ML} to Lisp, you 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 Fig.\ts \ref{hol-grammar} presents the grammar of
140 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
141 \verb|~(|$a$=$b$\verb|)|.
143 \subsection{Types}\label{HOL-types}
144 The type of formulae, {\it bool} belongs to class {\it term}; thus,
145 formulae are terms. The built-in type~$fun$, which constructs function
146 types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
147 $\sigma$ and~$\tau$ do; this allows quantification over functions. Types
148 in {\HOL} must be non-empty; otherwise the quantifier rules would be
149 unsound~\cite[\S7]{paulson-COLOG}.
151 Gordon's {\sc hol} system supports {\bf type definitions}. A type is
152 defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
153 bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$
154 specifies a non-empty subset of~$\sigma$, and the new type denotes this
155 subset. New function constants are generated to establish an isomorphism
156 between the new type and the subset. If type~$\sigma$ involves type
157 variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
158 a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
161 Isabelle does not support type definitions at present. Instead, they are
162 mimicked by explicit definitions of isomorphism functions. These should be
163 accompanied by theorems of the form $\exists x::\sigma.P(x)$, but this is
168 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
169 satisfying~$P[a]$, if such exists. Since all terms in {\HOL} denote
170 something, a description is always meaningful, but we do not know its value
171 unless $P[x]$ defines it uniquely. We may write descriptions as
172 \ttindexbold{Eps}($P$) or use the syntax
173 \hbox{\tt \at $x$.$P[x]$}. Existential quantification is defined
175 \[ \exists x.P(x) \equiv P(\epsilon x.P(x)) \]
176 The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
177 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
178 quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
179 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
180 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
182 \index{*"!}\index{*"?}
183 Quantifiers have two notations. As in Gordon's {\sc hol} system, {\HOL}
184 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
185 existential quantifier must be followed by a space; thus {\tt?x} is an
186 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
187 notation for quantifiers, \ttindex{ALL} and \ttindex{EX}, is also
188 available. Both notations are accepted for input. The {\ML} reference
189 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
190 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
191 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
194 Although the description operator does not usually allow iteration of the
195 form \hbox{\tt \at $x@1 \dots x@n$.$P[x@1,\dots,x@n]$}, there are cases where
196 this is legal. If \hbox{\tt \at $y$.$P[x,y]$} is of type~{\it bool},
197 then \hbox{\tt \at $x\,y$.$P[x,y]$} is legal. The pretty printer will
198 display \hbox{\tt \at $x$.\at $y$.$P[x,y]$} as
199 \hbox{\tt \at $x\,y$.$P[x,y]$}.
203 \begin{ttbox}\makeatother
205 \idx{subst} [| s=t; P(s) |] ==> P(t::'a)
206 \idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
207 \idx{impI} (P ==> Q) ==> P-->Q
208 \idx{mp} [| P-->Q; P |] ==> Q
209 \idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
210 \idx{selectI} P(x::'a) ==> P(@x.P(x))
211 \idx{True_or_False} (P=True) | (P=False)
212 \subcaption{basic rules}
214 \idx{True_def} True = ((\%x.x)=(\%x.x))
215 \idx{All_def} All = (\%P. P = (\%x.True))
216 \idx{Ex_def} Ex = (\%P. P(@x.P(x)))
217 \idx{False_def} False = (!P.P)
218 \idx{not_def} not = (\%P. P-->False)
219 \idx{and_def} op & = (\%P Q. !R. (P-->Q-->R) --> R)
220 \idx{or_def} op | = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
221 \idx{Ex1_def} Ex1 = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
222 \subcaption{Definitions of the logical constants}
224 \idx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y)
225 \idx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
226 \idx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
227 \subcaption{Further definitions}
229 \caption{Rules of {\tt HOL}} \label{hol-rules}
235 \idx{sym} s=t ==> t=s
236 \idx{trans} [| r=s; s=t |] ==> r=t
237 \idx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
238 \idx{box_equals} [| a=b; a=c; b=d |] ==> c=d
239 \idx{arg_cong} s=t ==> f(s)=f(t)
240 \idx{fun_cong} s::'a=>'b = t ==> s(x)=t(x)
241 \subcaption{Equality}
244 \idx{FalseE} False ==> P
246 \idx{conjI} [| P; Q |] ==> P&Q
247 \idx{conjunct1} [| P&Q |] ==> P
248 \idx{conjunct2} [| P&Q |] ==> Q
249 \idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
251 \idx{disjI1} P ==> P|Q
252 \idx{disjI2} Q ==> P|Q
253 \idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
255 \idx{notI} (P ==> False) ==> ~ P
256 \idx{notE} [| ~ P; P |] ==> R
257 \idx{impE} [| P-->Q; P; Q ==> R |] ==> R
258 \subcaption{Propositional logic}
260 \idx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
261 \idx{iffD1} [| P=Q; P |] ==> Q
262 \idx{iffD2} [| P=Q; Q |] ==> P
263 \idx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
265 \idx{eqTrueI} P ==> P=True
266 \idx{eqTrueE} P=True ==> P
267 \subcaption{Logical equivalence}
270 \caption{Derived rules for {\HOL}} \label{hol-lemmas1}
275 \begin{ttbox}\makeatother
276 \idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
277 \idx{spec} !x::'a.P(x) ==> P(x)
278 \idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
279 \idx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
281 \idx{exI} P(x) ==> ? x::'a.P(x)
282 \idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
284 \idx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
285 \idx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
288 \idx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
289 \subcaption{Quantifiers and descriptions}
291 \idx{ccontr} (~P ==> False) ==> P
292 \idx{classical} (~P ==> P) ==> P
293 \idx{excluded_middle} ~P | P
295 \idx{disjCI} (~Q ==> P) ==> P|Q
296 \idx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
297 \idx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
298 \idx{iffCE} [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
299 \idx{notnotD} ~~P ==> P
300 \idx{swap} ~P ==> (~Q ==> P) ==> Q
301 \subcaption{Classical logic}
303 \idx{if_True} if(True,x,y) = x
304 \idx{if_False} if(False,x,y) = y
305 \idx{if_P} P ==> if(P,x,y) = x
306 \idx{if_not_P} ~ P ==> if(P,x,y) = y
307 \idx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
308 \subcaption{Conditionals}
310 \caption{More derived rules} \label{hol-lemmas2}
314 \section{Rules of inference}
315 The basic theory has the {\ML} identifier \ttindexbold{HOL.thy}. However,
316 many further theories are defined, introducing product and sum types, the
317 natural numbers, etc.
319 Figure~\ref{hol-rules} shows the inference rules with their~{\ML} names.
320 They follow standard practice in higher-order logic: only a few connectives
321 are taken as primitive, with the remainder defined obscurely.
323 Unusually, the definitions are expressed using object-equality~({\tt=})
324 rather than meta-equality~({\tt==}). This is possible because equality in
325 higher-order logic may equate formulae and even functions over formulae.
326 On the other hand, meta-equality is Isabelle's usual symbol for making
327 definitions. Take care to note which form of equality is used before
330 Some of the rules mention type variables; for example, {\tt refl} mentions
331 the type variable~{\tt'a}. This facilitates explicit instantiation of the
332 type variables. By default, such variables range over class {\it term}.
335 Where function types are involved, Isabelle's unification code does not
336 guarantee to find instantiations for type variables automatically. If
337 resolution fails for no obvious reason, try setting \ttindex{show_types} to
338 {\tt true}, causing Isabelle to display types of terms. (Possibly, set
339 \ttindex{show_sorts} to {\tt true} also, causing Isabelle to display sorts.)
340 Be prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}.
341 Setting \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to
342 report omitted search paths during unification.
345 Here are further comments on the rules:
347 \item[\ttindexbold{ext}]
348 expresses extensionality of functions.
349 \item[\ttindexbold{iff}]
350 asserts that logically equivalent formulae are equal.
351 \item[\ttindexbold{selectI}]
352 gives the defining property of the Hilbert $\epsilon$-operator. The
353 derived rule \ttindexbold{select_equality} (see below) is often easier to use.
354 \item[\ttindexbold{True_or_False}]
355 makes the logic classical.\footnote{In fact, the $\epsilon$-operator
356 already makes the logic classical, as shown by Diaconescu;
357 see Paulson~\cite{paulson-COLOG} for details.}
361 {\HOL} has no if-and-only-if connective; logical equivalence is expressed
362 using equality. But equality has a high precedence, as befitting a
363 relation, while if-and-only-if typically has the lowest precedence. Thus,
364 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. When
365 using $=$ to mean logical equivalence, enclose both operands in
369 Some derived rules are shown in Figures~\ref{hol-lemmas1}
370 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
371 for the logical connectives, as well as sequent-style elimination rules for
372 conjunctions, implications, and universal quantifiers.
374 Note the equality rules: \ttindexbold{ssubst} performs substitution in
375 backward proofs, while \ttindexbold{box_equals} supports reasoning by
376 simplifying both sides of an equation.
378 See the files {\tt HOL/hol.thy} and
379 {\tt HOL/hol.ML} for complete listings of the rules and
383 \section{Generic packages}
384 {\HOL} instantiates most of Isabelle's generic packages;
385 see {\tt HOL/ROOT.ML} for details.
388 Because it includes a general substitution rule, {\HOL} instantiates the
389 tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
390 throughout a subgoal and its hypotheses.
392 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
393 simplification set for higher-order logic. Equality~($=$), which also
394 expresses logical equivalence, may be used for rewriting. See the file
395 {\tt HOL/simpdata.ML} for a complete listing of the simplification
398 It instantiates the classical reasoning module. See~\S\ref{hol-cla-prover}
406 \it name &\it meta-type & \it description \\
407 \index{"{"}@{\tt\{\}}}
408 {\tt\{\}} & $\alpha\,set$ & the empty set \\
409 \idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
410 & insertion of element \\
411 \idx{Collect} & $(\alpha\To bool)\To\alpha\,set$
413 \idx{Compl} & $(\alpha\,set)\To\alpha\,set$
415 \idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
416 & intersection over a set\\
417 \idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
419 \idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
420 &set of sets intersection \\
421 \idx{Union} & $((\alpha\,set)set)\To\alpha\,set$
422 &set of sets union \\
423 \idx{range} & $(\alpha\To\beta )\To\beta\,set$
424 & range of a function \\[1ex]
425 \idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
426 & bounded quantifiers \\
427 \idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
429 \idx{inj}~~\idx{surj}& $(\alpha\To\beta )\To bool$
430 & injective/surjective \\
431 \idx{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 prec & \it description \\
440 \idx{INT} & \idx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
441 intersection over a type\\
442 \idx{UN} & \idx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
452 \begin{tabular}{rrrr}
453 \it symbol & \it meta-type & \it precedence & \it description \\
454 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
456 \idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
457 & Left 70 & intersection ($\inter$) \\
458 \idx{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 {\HOL}'s set theory} \label{hol-set-syntax}
472 \begin{center} \tt\frenchspacing
474 \it external & \it internal & \it description \\
475 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
476 \{$a@1$, $\ldots$, $a@n$\} & insert($a@1$,$\cdots$,insert($a@n$,\{\})) &
478 \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
480 \idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
481 \rm intersection over a set \\
482 \idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
483 \rm union over a set \\
484 \idx{!} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
485 \rm bounded $\forall$ \\
486 \idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
487 \rm bounded $\exists$ \\[1ex]
488 \idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
489 \rm bounded $\forall$ \\
490 \idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
491 \rm bounded $\exists$
494 \subcaption{Translations}
498 term & = & \hbox{other terms\ldots} \\
500 & | & "\{ " term\; ("," term)^* " \}" \\
501 & | & "\{ " id " . " formula " \}" \\
502 & | & term " `` " term \\
503 & | & term " Int " term \\
504 & | & term " Un " term \\
505 & | & "INT~~" id ":" term " . " term \\
506 & | & "UN~~~" id ":" term " . " term \\
507 & | & "INT~~" id~id^* " . " term \\
508 & | & "UN~~~" id~id^* " . " term \\[2ex]
509 formula & = & \hbox{other formulae\ldots} \\
510 & | & term " : " term \\
511 & | & term " \ttilde: " term \\
512 & | & term " <= " term \\
513 & | & "!~~~" id ":" term " . " formula \\
514 & | & "?~~~" id ":" term " . " formula \\
515 & | & "ALL " id ":" term " . " formula \\
516 & | & "EX~~" id ":" term " . " formula
519 \subcaption{Full Grammar}
520 \caption{Syntax of {\HOL}'s set theory (continued)} \label{hol-set-syntax2}
524 \begin{figure} \underscoreon
526 \idx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
527 \idx{Collect_mem_eq} \{x.x:A\} = A
528 \subcaption{Isomorphisms between predicates and sets}
530 \idx{empty_def} \{\} == \{x.x=False\}
531 \idx{insert_def} insert(a,B) == \{x.x=a\} Un B
532 \idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
533 \idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
534 \idx{subset_def} A <= B == ! x:A. x:B
535 \idx{Un_def} A Un B == \{x.x:A | x:B\}
536 \idx{Int_def} A Int B == \{x.x:A & x:B\}
537 \idx{set_diff_def} A - B == \{x.x:A & x~:B\}
538 \idx{Compl_def} Compl(A) == \{x. ~ x:A\}
539 \idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
540 \idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
541 \idx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
542 \idx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
543 \idx{Inter_def} Inter(S) == (INT x:S. x)
544 \idx{Union_def} Union(S) == (UN x:S. x)
545 \idx{image_def} f``A == \{y. ? x:A. y=f(x)\}
546 \idx{range_def} range(f) == \{y. ? x. y=f(x)\}
547 \idx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
548 \idx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
549 \idx{surj_def} surj(f) == ! y. ? x. y=f(x)
550 \idx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
551 \subcaption{Definitions}
553 \caption{Rules of {\HOL}'s set theory} \label{hol-set-rules}
557 \begin{figure} \underscoreon
559 \idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
560 \idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
561 \idx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
562 \idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
563 \subcaption{Comprehension}
565 \idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
566 \idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
567 \idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
568 \idx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
569 (! x:A. P(x)) = (! x:A'. P'(x))
571 \idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
572 \idx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
573 \idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
574 \subcaption{Bounded quantifiers}
576 \idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
577 \idx{subsetD} [| A <= B; c:A |] ==> c:B
578 \idx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
580 \idx{subset_refl} A <= A
581 \idx{subset_antisym} [| A <= B; B <= A |] ==> A = B
582 \idx{subset_trans} [| A<=B; B<=C |] ==> A<=C
584 \idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
585 \idx{equalityD1} A = B ==> A<=B
586 \idx{equalityD2} A = B ==> B<=A
587 \idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
589 \idx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
590 [| ~ c:A; ~ c:B |] ==> P
592 \subcaption{The subset and equality relations}
594 \caption{Derived rules for set theory} \label{hol-set1}
598 \begin{figure} \underscoreon
600 \idx{emptyE} a : \{\} ==> P
602 \idx{insertI1} a : insert(a,B)
603 \idx{insertI2} a : B ==> a : insert(b,B)
604 \idx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
606 \idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
607 \idx{ComplD} [| c : Compl(A) |] ==> ~ c:A
609 \idx{UnI1} c:A ==> c : A Un B
610 \idx{UnI2} c:B ==> c : A Un B
611 \idx{UnCI} (~c:B ==> c:A) ==> c : A Un B
612 \idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
614 \idx{IntI} [| c:A; c:B |] ==> c : A Int B
615 \idx{IntD1} c : A Int B ==> c:A
616 \idx{IntD2} c : A Int B ==> c:B
617 \idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
619 \idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
620 \idx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
622 \idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
623 \idx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
624 \idx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
626 \idx{UnionI} [| X:C; A:X |] ==> A : Union(C)
627 \idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
629 \idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
630 \idx{InterD} [| A : Inter(C); X:C |] ==> A:X
631 \idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
633 \caption{Further derived rules for set theory} \label{hol-set2}
637 \section{A formulation of set theory}
638 Historically, higher-order logic gives a foundation for Russell and
639 Whitehead's theory of classes. Let us use modern terminology and call them
640 {\bf sets}, but note that these sets are distinct from those of {\ZF} set
641 theory, and behave more like {\ZF} classes.
644 Sets are given by predicates over some type~$\sigma$. Types serve to
645 define universes for sets, but type checking is still significant.
647 There is a universal set (for each type). Thus, sets have complements, and
648 may be defined by absolute comprehension.
650 Although sets may contain other sets as elements, the containing set must
651 have a more complex type.
653 Finite unions and intersections have the same behaviour in {\HOL} as they
654 do in~{\ZF}. In {\HOL} the intersection of the empty set is well-defined,
655 denoting the universal set for the given type.
657 \subsection{Syntax of set theory}
658 The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The
659 new type is defined for clarity and to avoid complications involving
660 function types in unification. Since Isabelle does not support type
661 definitions (as mentioned in \S\ref{HOL-types}), the isomorphisms between
662 the two types are declared explicitly. Here they are natural: {\tt
663 Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
664 maps in the other direction (ignoring argument order).
666 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
667 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
668 constructs. Infix operators include union and intersection ($A\union B$
669 and $A\inter B$), the subset and membership relations, and the image
670 operator~{\tt``}. Note that $a$\verb|~:|$b$ is translated to
671 \verb|~(|$a$:$b$\verb|)|. The {\tt\{\ldots\}} notation abbreviates finite
672 sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the
675 \{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\{\})))
678 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
679 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
680 occurrences of~$x$. This syntax expands to \ttindexbold{Collect}$(\lambda
683 The set theory defines two {\bf bounded quantifiers}:
685 \forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\
686 \exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]
688 The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined
689 accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
690 write\index{*"!}\index{*"?}\index{*ALL}\index{*EX}
691 \hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.
692 Isabelle's usual notation, \ttindex{ALL} and \ttindex{EX}, is also
694 ordinary quantifiers, the contents of \ttindexbold{HOL_quantifiers} specifies
695 which notation should be used for output.
697 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
698 $\bigcap@{x\in A}B[x]$, are written
699 \ttindexbold{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
700 \ttindexbold{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
701 Unions and intersections over types, namely $\bigcup@x B[x]$ and
702 $\bigcap@x B[x]$, are written
703 \ttindexbold{UN}~\hbox{\tt$x$.$B[x]$} and
704 \ttindexbold{INT}~\hbox{\tt$x$.$B[x]$}; they are equivalent to the previous
705 union/intersection operators when $A$ is the universal set.
706 The set of set union and intersection operators ($\bigcup A$ and $\bigcap
707 A$) are not binders, but equals $\bigcup@{x\in A}x$ and $\bigcap@{x\in
710 \subsection{Axioms and rules of set theory}
711 The axioms \ttindexbold{mem_Collect_eq} and
712 \ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and
713 \hbox{\tt op :} are isomorphisms.
714 All the other axioms are definitions; see Fig.\ts \ref{hol-set-rules}.
715 These include straightforward properties of functions: image~({\tt``}) and
716 {\tt range}, and predicates concerning monotonicity, injectiveness, etc.
718 {\HOL}'s set theory has the {\ML} identifier \ttindexbold{Set.thy}.
720 \begin{figure} \underscoreon
722 \idx{imageI} [| x:A |] ==> f(x) : f``A
723 \idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
725 \idx{rangeI} f(x) : range(f)
726 \idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
728 \idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
729 \idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
731 \idx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
732 \idx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
733 \idx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
735 \idx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
736 \idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
739 [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
742 (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
744 \idx{inj_onto_inverseI}
745 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
748 [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
750 \idx{inj_onto_contraD}
751 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
753 \caption{Derived rules involving functions} \label{hol-fun}
757 \begin{figure} \underscoreon
759 \idx{Union_upper} B:A ==> B <= Union(A)
760 \idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
762 \idx{Inter_lower} B:A ==> Inter(A) <= B
763 \idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
765 \idx{Un_upper1} A <= A Un B
766 \idx{Un_upper2} B <= A Un B
767 \idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
769 \idx{Int_lower1} A Int B <= A
770 \idx{Int_lower2} A Int B <= B
771 \idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
773 \caption{Derived rules involving subsets} \label{hol-subset}
777 \begin{figure} \underscoreon
779 \idx{Int_absorb} A Int A = A
780 \idx{Int_commute} A Int B = B Int A
781 \idx{Int_assoc} (A Int B) Int C = A Int (B Int C)
782 \idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
784 \idx{Un_absorb} A Un A = A
785 \idx{Un_commute} A Un B = B Un A
786 \idx{Un_assoc} (A Un B) Un C = A Un (B Un C)
787 \idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
789 \idx{Compl_disjoint} A Int Compl(A) = \{x.False\}
790 \idx{Compl_partition} A Un Compl(A) = \{x.True\}
791 \idx{double_complement} Compl(Compl(A)) = A
792 \idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
793 \idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
795 \idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
796 \idx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
798 (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
800 \idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
801 \idx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
802 \idx{Int_Inter_image}
803 (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
805 \caption{Set equalities} \label{hol-equalities}
809 \subsection{Derived rules for sets}
810 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most
811 are obvious and resemble rules of Isabelle's {\ZF} set theory. The
812 rules named $XXX${\tt_cong} break down equalities. Certain rules, such as
813 \ttindexbold{subsetCE}, \ttindexbold{bexCI} and \ttindexbold{UnCI}, are
814 designed for classical reasoning; the more natural rules \ttindexbold{subsetD},
815 \ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not
816 strictly necessary. Similarly, \ttindexbold{equalityCE} supports classical
817 reasoning about extensionality, after the fashion of \ttindex{iffCE}. See
818 the file {\tt HOL/set.ML} for proofs pertaining to set theory.
820 Figure~\ref{hol-fun} presents derived inference rules involving functions. See
821 the file {\tt HOL/fun.ML} for a complete listing.
823 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
824 See the file {\tt HOL/subset.ML}.
826 Figure~\ref{hol-equalities} presents set equalities. See
827 {\tt HOL/equalities.ML}.
833 \it name &\it meta-type & \it description \\
834 \idx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
835 & ordered pairs $\langle a,b\rangle$ \\
836 \idx{fst} & $\alpha\times\beta \To \alpha$ & first projection\\
837 \idx{snd} & $\alpha\times\beta \To \beta$ & second projection\\
838 \idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
839 & generalized projection\\
841 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
845 \subcaption{Constants}
847 \begin{ttbox}\makeatletter
848 \idx{fst_def} fst(p) == @a. ? b. p = <a,b>
849 \idx{snd_def} snd(p) == @b. ? a. p = <a,b>
850 \idx{split_def} split(p,c) == c(fst(p),snd(p))
851 \idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
852 \subcaption{Definitions}
854 \idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
856 \idx{fst} fst(<a,b>) = a
857 \idx{snd} snd(<a,b>) = b
858 \idx{split} split(<a,b>, c) = c(a,b)
860 \idx{surjective_pairing} p = <fst(p),snd(p)>
862 \idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
864 \idx{SigmaE} [| c: Sigma(A,B);
865 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
866 \subcaption{Derived rules}
868 \caption{Type $\alpha\times\beta$}
876 \it name &\it meta-type & \it description \\
877 \idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\
878 \idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\
879 \idx{case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
883 \subcaption{Constants}
885 \begin{ttbox}\makeatletter
886 \idx{case_def} case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
887 (!y. p=Inr(y) --> z=g(y)))
888 \subcaption{Definition}
890 \idx{Inl_not_Inr} ~ Inl(a)=Inr(b)
892 \idx{inj_Inl} inj(Inl)
893 \idx{inj_Inr} inj(Inr)
895 \idx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
897 \idx{case_Inl} case(Inl(x), f, g) = f(x)
898 \idx{case_Inr} case(Inr(x), f, g) = g(x)
900 \idx{surjective_sum} case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
901 \subcaption{Derived rules}
903 \caption{Rules for type $\alpha+\beta$}
909 The basic higher-order logic is augmented with a tremendous amount of
910 material, including support for recursive function and type definitions.
911 Space does not permit a detailed discussion. The present section describes
912 product, sum, natural number and list types.
914 \subsection{Product and sum types}
915 {\HOL} defines the product type $\alpha\times\beta$ and the sum type
916 $\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
917 standard constructions (Figs.~\ref{hol-prod} and~\ref{hol-sum}). Because
918 Isabelle does not support abstract type definitions, the isomorphisms
919 between these types and their representations are made explicitly.
921 Most of the definitions are suppressed, but observe that the projections
922 and conditionals are defined as descriptions. Their properties are easily
923 proved using \ttindex{select_equality}. See {\tt HOL/prod.thy} and
924 {\tt HOL/sum.thy} for details.
930 \it symbol & \it meta-type & \it description \\
931 \idx{0} & $nat$ & zero \\
932 \idx{Suc} & $nat \To nat$ & successor function\\
933 \idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
935 \idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
936 & primitive recursor\\
937 \idx{pred_nat} & $(nat\times nat) set$ & predecessor relation
943 \index{*@{\tt*}|bold}
944 \index{/@{\tt/}|bold}
945 \index{//@{\tt//}|bold}
946 \index{+@{\tt+}|bold}
947 \index{-@{\tt-}|bold}
948 \begin{tabular}{rrrr}
949 \it symbol & \it meta-type & \it precedence & \it description \\
950 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
951 \tt / & $[nat,nat]\To nat$ & Left 70 & division\\
952 \tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\
953 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
954 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
957 \subcaption{Constants and infixes}
959 \begin{ttbox}\makeatother
960 \idx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
961 (!x. n=Suc(x) --> z=f(x)))
962 \idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
963 \idx{less_def} m<n == <m,n>:pred_nat^+
964 \idx{nat_rec_def} nat_rec(n,c,d) ==
965 wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
967 \idx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
968 \idx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
969 \idx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
970 \idx{mod_def} m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
971 \idx{quo_def} m/n == wfrec(trancl(pred_nat),
972 m, \%j f. if(j<n,0,Suc(f(j-n))))
973 \subcaption{Definitions}
975 \caption{Defining $nat$, the type of natural numbers} \label{hol-nat1}
979 \begin{figure} \underscoreon
981 \idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
983 \idx{Suc_not_Zero} Suc(m) ~= 0
984 \idx{inj_Suc} inj(Suc)
985 \idx{n_not_Suc_n} n~=Suc(n)
986 \subcaption{Basic properties}
988 \idx{pred_natI} <n, Suc(n)> : pred_nat
990 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
992 \idx{nat_case_0} nat_case(0, a, f) = a
993 \idx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
995 \idx{wf_pred_nat} wf(pred_nat)
996 \idx{nat_rec_0} nat_rec(0,c,h) = c
997 \idx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
998 \subcaption{Case analysis and primitive recursion}
1000 \idx{less_trans} [| i<j; j<k |] ==> i<k
1001 \idx{lessI} n < Suc(n)
1002 \idx{zero_less_Suc} 0 < Suc(n)
1004 \idx{less_not_sym} n<m --> ~ m<n
1005 \idx{less_not_refl} ~ n<n
1006 \idx{not_less0} ~ n<0
1008 \idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1009 \idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1011 \idx{less_linear} m<n | m=n | n<m
1012 \subcaption{The less-than relation}
1014 \caption{Derived rules for~$nat$} \label{hol-nat2}
1018 \subsection{The type of natural numbers, $nat$}
1019 {\HOL} defines the natural numbers in a roundabout but traditional way.
1020 The axiom of infinity postulates an type~$ind$ of individuals, which is
1021 non-empty and closed under an injective operation. The natural numbers are
1022 inductively generated by choosing an arbitrary individual for~0 and using
1023 the injective operation to take successors. As usual, the isomorphisms
1024 between~$nat$ and its representation are made explicitly.
1026 The definition makes use of a least fixed point operator \ttindex{lfp},
1027 defined using the Knaster-Tarski theorem. This in turn defines an operator
1028 \ttindex{trancl} for taking the transitive closure of a relation. See
1029 files {\tt HOL/lfp.thy} and {\tt HOL/trancl.thy} for
1030 details. The definition of~$nat$ resides on {\tt HOL/nat.thy}.
1032 Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
1033 $\leq$ on the natural numbers. As of this writing, Isabelle provides no
1034 means of verifying that such overloading is sensible. On the other hand,
1035 the {\HOL} theory includes no polymorphic axioms stating general properties
1038 File {\tt HOL/arith.ML} develops arithmetic on the natural numbers.
1039 It defines addition, multiplication, subtraction, division, and remainder,
1040 proving the theorem $a \bmod b + (a/b)\times b = a$. Division and
1041 remainder are defined by repeated subtraction, which requires well-founded
1042 rather than primitive recursion.
1044 Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion
1045 along arbitrary well-founded relations; see {\tt HOL/wf.ML} for the
1046 development. The predecessor relation, \ttindexbold{pred_nat}, is shown to
1047 be well-founded; recursion along this relation is primitive recursion,
1048 while its transitive closure is~$<$.
1053 \begin{tabular}{rrr}
1054 \it symbol & \it meta-type & \it description \\
1055 \idx{Nil} & $\alpha list$ & the empty list\\
1056 \idx{Cons} & $[\alpha, \alpha list] \To \alpha list$
1057 & list constructor\\
1058 \idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1059 \beta]\To\beta] \To \beta$
1061 \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1062 & mapping functional
1065 \subcaption{Constants}
1068 \idx{map_def} map(f,xs) == list_rec(xs, Nil, \%x l r. Cons(f(x), r))
1069 \subcaption{Definition}
1072 [| P(Nil); !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l)
1074 \idx{Cons_not_Nil} ~ Cons(x,xs) = Nil
1075 \idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)
1077 \idx{list_rec_Nil} list_rec(Nil,c,h) = c
1078 \idx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))
1080 \idx{map_Nil} map(f,Nil) = Nil
1081 \idx{map_Cons} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))
1083 \caption{The type of lists and its operations} \label{hol-list}
1087 \subsection{The type constructor for lists, $\alpha\,list$}
1088 {\HOL}'s definition of lists is an example of an experimental method for
1089 handling recursive data types. The details need not concern us here; see
1090 the file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the
1091 basic list operations, with their types and properties. In particular,
1092 \ttindexbold{list_rec} is a primitive recursion operator for lists, in the
1093 style of Martin-L\"of type theory. It is derived from well-founded
1094 recursion, a general principle that can express arbitrary total recursive
1098 \subsection{The type constructor for lazy lists, $\alpha\,llist$}
1099 The definition of lazy lists demonstrates methods for handling infinite
1100 data structures and co-induction in higher-order logic. It defines an
1101 operator for co-recursion on lazy lists, which is used to define a few
1102 simple functions such as map and append. Co-recursion cannot easily define
1103 operations such as filter, which can compute indefinitely before yielding
1104 the next element (if any!) of the lazy list. A co-induction principle is
1105 defined for proving equations on lazy lists. See the files
1106 {\tt HOL/llist.thy} and {\tt HOL/llist.ML} for the formal
1107 derivations. I have written a report discussing the treatment of lazy
1108 lists, and finite lists also~\cite{paulson-coind}.
1111 \section{Classical proof procedures} \label{hol-cla-prover}
1112 {\HOL} derives classical introduction rules for $\disj$ and~$\exists$, as
1113 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1114 rule (Fig.~\ref{hol-lemmas2}).
1116 The classical reasoning module is set up for \HOL, as the structure
1117 \ttindexbold{Classical}. This structure is open, so {\ML} identifiers such
1118 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
1120 {\HOL} defines the following classical rule sets:
1128 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
1129 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
1130 along with the rule~\ttindex{refl}.
1132 \item[\ttindexbold{HOL_cs}]
1133 extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
1134 and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for
1135 unique existence. Search using this is incomplete since quantified
1136 formulae are used at most once.
1138 \item[\ttindexbold{HOL_dup_cs}]
1139 extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
1140 and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as
1141 rules for unique existence. Search using this is complete --- quantified
1142 formulae may be duplicated --- but frequently fails to terminate. It is
1143 generally unsuitable for depth-first search.
1145 \item[\ttindexbold{set_cs}]
1146 extends {\tt HOL_cs} with rules for the bounded quantifiers, subsets,
1147 comprehensions, unions/intersections, complements, finite setes, images and
1151 See the {\em Reference Manual} for more discussion of classical proof
1155 \section{The examples directories}
1156 Directory {\tt Subst} contains Martin Coen's mechanization of a theory of
1157 substitutions and unifiers. It is based on Paulson's previous
1158 mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1161 Directory {\tt ex} contains other examples and experimental proofs in
1162 {\HOL}. Here is an overview of the more interesting files.
1164 \item[{\tt HOL/ex/meson.ML}]
1165 contains an experimental implementation of the MESON proof procedure,
1166 inspired by Plaisted~\cite{plaisted90}. It is much more powerful than
1167 Isabelle's classical module.
1169 \item[{\tt HOL/ex/mesontest.ML}]
1170 contains test data for the MESON proof procedure.
1172 \item[{\tt HOL/ex/set.ML}]
1173 proves Cantor's Theorem, which is presented below, and the
1174 Schr\"oder-Bernstein Theorem.
1176 \item[{\tt HOL/ex/pl.ML}]
1177 proves the soundness and completeness of classical propositional logic,
1178 given a truth table semantics. The only connective is $\imp$. A
1179 Hilbert-style axiom system is specified, and its set of theorems defined
1182 \item[{\tt HOL/ex/term.ML}]
1183 contains proofs about an experimental recursive type definition;
1184 the recursion goes through the type constructor~$list$.
1186 \item[{\tt HOL/ex/simult.ML}]
1187 defines primitives for solving mutually recursive equations over sets.
1188 It constructs sets of trees and forests as an example, including induction
1189 and recursion rules that handle the mutual recursion.
1191 \item[{\tt HOL/ex/mt.ML}]
1192 contains Jacob Frost's formalization~\cite{frost93} of a co-induction
1193 example by Milner and Tofte~\cite{milner-coind}.
1197 \section{Example: deriving the conjunction rules}
1198 {\HOL} comes with a body of derived rules, ranging from simple properties
1199 of the logical constants and set theory to well-founded recursion. Many of
1200 them are worth studying.
1202 Deriving natural deduction rules for the logical constants from their
1203 definitions is an archetypal example of higher-order reasoning. Let us
1204 verify two conjunction rules:
1205 \[ \infer[({\conj}I)]{P\conj Q}{P & Q} \qquad\qquad
1206 \infer[({\conj}E1)]{P}{P\conj Q}
1209 \subsection{The introduction rule}
1210 We begin by stating the rule as the goal. The list of premises $[P,Q]$ is
1211 bound to the {\ML} variable~{\tt prems}.
1213 val prems = goal HOL.thy "[| P; Q |] ==> P&Q";
1217 {\out val prems = ["P [P]", "Q [Q]"] : thm list}
1219 The next step is to unfold the definition of conjunction. But
1220 \ttindex{and_def} uses {\HOL}'s internal equality, so
1221 \ttindex{rewrite_goals_tac} is unsuitable.
1222 Instead, we perform substitution using the rule \ttindex{ssubst}:
1224 by (resolve_tac [and_def RS ssubst] 1);
1227 {\out 1. ! R. (P --> Q --> R) --> R}
1229 We now apply $(\forall I)$ and $({\imp}I)$:
1231 by (resolve_tac [allI] 1);
1234 {\out 1. !!R. (P --> Q --> R) --> R}
1236 by (resolve_tac [impI] 1);
1239 {\out 1. !!R. P --> Q --> R ==> R}
1241 The assumption is a nested implication, which may be eliminated
1242 using~\ttindex{mp} resolved with itself. Elim-resolution, here, performs
1243 backwards chaining. More straightforward would be to use~\ttindex{impE}
1247 by (eresolve_tac [mp RS mp] 1);
1253 These two subgoals are simply the premises:
1255 by (REPEAT (resolve_tac prems 1));
1262 \subsection{The elimination rule}
1263 Again, we bind the list of premises (in this case $[P\conj Q]$)
1266 val prems = goal HOL.thy "[| P & Q |] ==> P";
1270 {\out val prems = ["P & Q [P & Q]"] : thm list}
1272 Working with premises that involve defined constants can be tricky. We
1273 must expand the definition of conjunction in the meta-assumption $P\conj
1274 Q$. The rule \ttindex{subst} performs substitution in forward proofs.
1275 We get {\it two\/} resolvents since the vacuous substitution is valid:
1277 prems RL [and_def RS subst];
1278 {\out val it = ["! R. (P --> Q --> R) --> R [P & Q]",}
1279 {\out "P & Q [P & Q]"] : thm list}
1281 By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of
1282 the vacuous one and put the other into a convenient form:\footnote {Why use
1283 {\tt [spec] RL [mp]} instead of {\tt [spec RS mp]} to join the rules? In
1284 higher-order logic, {\tt spec RS mp} fails because the resolution yields
1285 two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall
1286 x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$. In first-order logic, the
1287 resolution yields only the latter result because $\forall x.x$ is not a
1288 first-order formula; in fact, it is equivalent to falsity.} \index{*RL}
1290 prems RL [and_def RS subst] RL [spec] RL [mp];
1291 {\out val it = ["P --> Q --> ?Q ==> ?Q [P & Q]"] : thm list}
1293 This is a list containing a single rule, which is directly applicable to
1296 by (resolve_tac it 1);
1299 {\out 1. P --> Q --> P}
1301 The subgoal is a trivial implication. Recall that \ttindex{ares_tac} is a
1302 combination of \ttindex{assume_tac} and \ttindex{resolve_tac}.
1304 by (REPEAT (ares_tac [impI] 1));
1311 \section{Example: Cantor's Theorem}
1312 Cantor's Theorem states that every set has more subsets than it has
1313 elements. It has become a favourite example in higher-order logic since
1314 it is so easily expressed:
1315 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1316 \forall x::\alpha. f(x) \not= S
1318 Viewing types as sets, $\alpha\To bool$ represents the powerset
1319 of~$\alpha$. This version states that for every function from $\alpha$ to
1320 its powerset, some subset is outside its range.
1321 The Isabelle proof uses {\HOL}'s set theory, with the type $\alpha\,set$ and
1322 the operator \ttindex{range}. Since it avoids quantification, we may
1323 inspect the subset found by the proof.
1325 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1327 {\out ~ ?S : range(f)}
1328 {\out 1. ~ ?S : range(f)}
1330 The first two steps are routine. The rule \ttindex{rangeE} reasons that,
1331 since $\Var{S}\in range(f)$, we have $\Var{S}=f(x)$ for some~$x$.
1333 by (resolve_tac [notI] 1);
1335 {\out ~ ?S : range(f)}
1336 {\out 1. ?S : range(f) ==> False}
1338 by (eresolve_tac [rangeE] 1);
1340 {\out ~ ?S : range(f)}
1341 {\out 1. !!x. ?S = f(x) ==> False}
1343 Next, we apply \ttindex{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1344 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1347 by (eresolve_tac [equalityCE] 1);
1349 {\out ~ ?S : range(f)}
1350 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1351 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1353 Now we use a bit of creativity. Suppose that $\Var{S}$ has the form of a
1354 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1355 $\Var{P}(\Var{c})\}$.\index{*CollectD}
1357 by (dresolve_tac [CollectD] 1);
1359 {\out ~ \{x. ?P7(x)\} : range(f)}
1360 {\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
1361 {\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
1363 Forcing a contradiction between the two assumptions of subgoal~1 completes
1364 the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, the
1365 standard diagonal construction.
1369 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1370 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1372 The rest should be easy. To apply \ttindex{CollectI} to the negated
1373 assumption, we employ \ttindex{swap_res_tac}:
1375 by (swap_res_tac [CollectI] 1);
1377 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1378 {\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
1382 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1385 How much creativity is required? As it happens, Isabelle can prove this
1386 theorem automatically. The classical set \ttindex{set_cs} contains rules
1387 for most of the constructs of {\HOL}'s set theory. We augment it with
1388 \ttindex{equalityCE} --- set equalities are not broken up by default ---
1389 and apply best-first search. Depth-first search would diverge, but
1390 best-first search successfully navigates through the large search space.
1394 {\out ~ ?S : range(f)}
1395 {\out 1. ~ ?S : range(f)}
1397 by (best_tac (set_cs addSEs [equalityCE]) 1);
1399 {\out ~ \{x. ~ x : f(x)\} : range(f)}