2 \chapter{Higher-Order Logic}
3 \index{higher-order logic|(}
4 \index{HOL system@{\sc hol} system}
6 The theory~\thydx{HOL} implements higher-order logic. It is based on
7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
8 Church's original paper~\cite{church40}. Andrews's
9 book~\cite{andrews86} is a full description of the original
10 Church-style higher-order logic. Experience with the {\sc hol} system
11 has demonstrated that higher-order logic is widely applicable in many
12 areas of mathematics and computer science, not just hardware
13 verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It is
14 weaker than {\ZF} set theory but for most applications this does not
15 matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\
18 The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
19 different syntax. Ancient releases of Isabelle included still another version
20 of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
21 version no longer exists, but \thydx{ZF} supports a similar style of
22 reasoning.} follows $\lambda$-calculus and functional programming. Function
23 application is curried. To apply the function~$f$ of type
24 $\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
25 write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that
26 $f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered
27 pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
29 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
30 identifies object-level types with meta-level types, taking advantage of
31 Isabelle's built-in type-checker. It identifies object-level functions
32 with meta-level functions, so it uses Isabelle's operations for abstraction
35 These identifications allow Isabelle to support \HOL\ particularly
36 nicely, but they also mean that \HOL\ requires more sophistication
37 from the user --- in particular, an understanding of Isabelle's type
38 system. Beginners should work with \texttt{show_types} (or even
39 \texttt{show_sorts}) set to \texttt{true}.
41 %working in first-order logic before attempting to use higher-order logic.
42 %This chapter assumes familiarity with~{\FOL{}}.
47 \it name &\it meta-type & \it description \\
48 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
49 \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\
50 \cdx{True} & $bool$ & tautology ($\top$) \\
51 \cdx{False} & $bool$ & absurdity ($\bot$) \\
52 \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
53 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
55 \subcaption{Constants}
58 \index{"@@{\tt\at} symbol}
59 \index{*"! symbol}\index{*"? symbol}
60 \index{*"?"! symbol}\index{*"E"X"! symbol}
61 \it symbol &\it name &\it meta-type & \it description \\
62 \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
63 Hilbert description ($\varepsilon$) \\
64 \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ &
65 universal quantifier ($\forall$) \\
66 \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
67 existential quantifier ($\exists$) \\
68 \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
69 unique existence ($\exists!$)\\
70 \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
77 \index{&@{\tt\&} symbol}
79 \index{*"-"-"> symbol}
80 \it symbol & \it meta-type & \it priority & \it description \\
81 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
82 Left 55 & composition ($\circ$) \\
83 \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
84 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
85 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
86 less than or equals ($\leq$)\\
87 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
88 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
89 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
92 \caption{Syntax of \texttt{HOL}} \label{hol-constants}
100 \[\begin{array}{rclcl}
101 term & = & \hbox{expression of class~$term$} \\
102 & | & "SOME~" id " . " formula
103 & | & "\at~" id " . " formula \\
105 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
107 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
108 & | & "LEAST"~ id " . " formula \\[2ex]
109 formula & = & \hbox{expression of type~$bool$} \\
110 & | & term " = " term \\
111 & | & term " \ttilde= " term \\
112 & | & term " < " term \\
113 & | & term " <= " term \\
114 & | & "\ttilde\ " formula \\
115 & | & formula " \& " formula \\
116 & | & formula " | " formula \\
117 & | & formula " --> " formula \\
118 & | & "ALL~" id~id^* " . " formula
119 & | & "!~~~" id~id^* " . " formula \\
120 & | & "EX~~" id~id^* " . " formula
121 & | & "?~~~" id~id^* " . " formula \\
122 & | & "EX!~" id~id^* " . " formula
123 & | & "?!~~" id~id^* " . " formula \\
126 \caption{Full grammar for \HOL} \label{hol-grammar}
132 Figure~\ref{hol-constants} lists the constants (including infixes and
133 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
134 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
138 \HOL\ has no if-and-only-if connective; logical equivalence is expressed
139 using equality. But equality has a high priority, as befitting a
140 relation, while if-and-only-if typically has the lowest priority. Thus,
141 $\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.
142 When using $=$ to mean logical equivalence, enclose both operands in
146 \subsection{Types and classes}
147 The universal type class of higher-order terms is called~\cldx{term}.
148 By default, explicit type variables have class \cldx{term}. In
149 particular the equality symbol and quantifiers are polymorphic over
152 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
153 formulae are terms. The built-in type~\tydx{fun}, which constructs
154 function types, is overloaded with arity {\tt(term,\thinspace
155 term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
156 term} if $\sigma$ and~$\tau$ do, allowing quantification over
159 \HOL\ offers various methods for introducing new types.
160 See~{\S}\ref{sec:HOL:Types} and~{\S}\ref{sec:HOL:datatype}.
162 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
163 signatures; the relations $<$ and $\leq$ are polymorphic over this
164 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
165 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
166 \cldx{order} of \cldx{ord} which axiomatizes partially ordered types
169 Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
170 \cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
171 symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In
172 particular, {\tt-} is instantiated for set difference and subtraction
175 If you state a goal containing overloaded functions, you may need to include
176 type constraints. Type inference may otherwise make the goal more
177 polymorphic than you intended, with confusing results. For example, the
178 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type
179 $\alpha::\{ord,plus\}$, although you may have expected them to have some
180 numeric type, e.g. $nat$. Instead you should have stated the goal as
181 $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have
185 If resolution fails for no obvious reason, try setting
186 \ttindex{show_types} to \texttt{true}, causing Isabelle to display
187 types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as
188 well, causing Isabelle to display type classes and sorts.
190 \index{unification!incompleteness of}
191 Where function types are involved, Isabelle's unification code does not
192 guarantee to find instantiations for type variables automatically. Be
193 prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
194 possibly instantiating type variables. Setting
195 \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
196 omitted search paths during unification.\index{tracing!of unification}
202 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
203 some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\
204 denote something, a description is always meaningful, but we do not
205 know its value unless $P$ defines it uniquely. We may write
206 descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
207 \hbox{\tt SOME~$x$.~$P[x]$}.
209 Existential quantification is defined by
210 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
211 The unique existence quantifier, $\exists!x. P$, is defined in terms
212 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
213 quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates
214 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
215 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
219 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The
220 basic Isabelle/HOL binders have two notations. Apart from the usual
221 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also
222 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\
223 and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be
224 followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a
225 quantification. Both notations are accepted for input. The print mode
226 ``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by
227 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),
228 then~{\tt!}\ and~{\tt?}\ are displayed.
232 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
233 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
234 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see
235 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
236 choice operator, so \texttt{Least} is always meaningful, but may yield
237 nothing useful in case there is not a unique least element satisfying
238 $P$.\footnote{Class $ord$ does not require much of its instances, so
239 $\leq$ need not be a well-ordering, not even an order at all!}
241 \medskip All these binders have priority 10.
244 The low priority of binders means that they need to be enclosed in
245 parenthesis when they occur in the context of other operations. For example,
246 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
250 \subsection{The let and case constructions}
251 Local abbreviations can be introduced by a \texttt{let} construct whose
252 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
253 the constant~\cdx{Let}. It can be expanded by rewriting with its
254 definition, \tdx{Let_def}.
256 \HOL\ also defines the basic syntax
257 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
258 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
259 and \sdx{of} are reserved words. Initially, this is mere syntax and has no
260 logical meaning. By declaring translations, you can cause instances of the
261 \texttt{case} construct to denote applications of particular case operators.
262 This is what happens automatically for each \texttt{datatype} definition
263 (see~{\S}\ref{sec:HOL:datatype}).
266 Both \texttt{if} and \texttt{case} constructs have as low a priority as
267 quantifiers, which requires additional enclosing parentheses in the context
268 of most other operations. For example, instead of $f~x = {\tt if\dots
269 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
273 \section{Rules of inference}
276 \begin{ttbox}\makeatother
277 \tdx{refl} t = (t::'a)
278 \tdx{subst} [| s = t; P s |] ==> P (t::'a)
279 \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)
280 \tdx{impI} (P ==> Q) ==> P-->Q
281 \tdx{mp} [| P-->Q; P |] ==> Q
282 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
283 \tdx{selectI} P(x::'a) ==> P(@x. P x)
284 \tdx{True_or_False} (P=True) | (P=False)
286 \caption{The \texttt{HOL} rules} \label{hol-rules}
289 Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
290 with their~{\ML} names. Some of the rules deserve additional
292 \begin{ttdescription}
293 \item[\tdx{ext}] expresses extensionality of functions.
294 \item[\tdx{iff}] asserts that logically equivalent formulae are
296 \item[\tdx{selectI}] gives the defining property of the Hilbert
297 $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule
298 \tdx{select_equality} (see below) is often easier to use.
299 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
300 fact, the $\varepsilon$-operator already makes the logic classical, as
301 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
305 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
306 \begin{ttbox}\makeatother
307 \tdx{True_def} True == ((\%x::bool. x)=(\%x. x))
308 \tdx{All_def} All == (\%P. P = (\%x. True))
309 \tdx{Ex_def} Ex == (\%P. P(@x. P x))
310 \tdx{False_def} False == (!P. P)
311 \tdx{not_def} not == (\%P. P-->False)
312 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
313 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
314 \tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
316 \tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
317 \tdx{if_def} If P x y ==
318 (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
319 \tdx{Let_def} Let s f == f s
320 \tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
322 \caption{The \texttt{HOL} definitions} \label{hol-defs}
326 \HOL{} follows standard practice in higher-order logic: only a few
327 connectives are taken as primitive, with the remainder defined obscurely
328 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
329 corresponding definitions \cite[page~270]{mgordon-hol} using
330 object-equality~({\tt=}), which is possible because equality in
331 higher-order logic may equate formulae and even functions over formulae.
332 But theory~\HOL{}, like all other Isabelle theories, uses
333 meta-equality~({\tt==}) for definitions.
335 The definitions above should never be expanded and are shown for completeness
336 only. Instead users should reason in terms of the derived rules shown below
337 or, better still, using high-level tactics
338 (see~{\S}\ref{sec:HOL:generic-packages}).
341 Some of the rules mention type variables; for example, \texttt{refl}
342 mentions the type variable~{\tt'a}. This allows you to instantiate
343 type variables explicitly by calling \texttt{res_inst_tac}.
348 \tdx{sym} s=t ==> t=s
349 \tdx{trans} [| r=s; s=t |] ==> r=t
350 \tdx{ssubst} [| t=s; P s |] ==> P t
351 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
352 \tdx{arg_cong} x = y ==> f x = f y
353 \tdx{fun_cong} f = g ==> f x = g x
354 \tdx{cong} [| f = g; x = y |] ==> f x = g y
355 \tdx{not_sym} t ~= s ==> s ~= t
356 \subcaption{Equality}
359 \tdx{FalseE} False ==> P
361 \tdx{conjI} [| P; Q |] ==> P&Q
362 \tdx{conjunct1} [| P&Q |] ==> P
363 \tdx{conjunct2} [| P&Q |] ==> Q
364 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
366 \tdx{disjI1} P ==> P|Q
367 \tdx{disjI2} Q ==> P|Q
368 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
370 \tdx{notI} (P ==> False) ==> ~ P
371 \tdx{notE} [| ~ P; P |] ==> R
372 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
373 \subcaption{Propositional logic}
375 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
376 \tdx{iffD1} [| P=Q; P |] ==> Q
377 \tdx{iffD2} [| P=Q; Q |] ==> P
378 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
380 %\tdx{eqTrueI} P ==> P=True
381 %\tdx{eqTrueE} P=True ==> P
382 \subcaption{Logical equivalence}
385 \caption{Derived rules for \HOL} \label{hol-lemmas1}
390 \begin{ttbox}\makeatother
391 \tdx{allI} (!!x. P x) ==> !x. P x
392 \tdx{spec} !x. P x ==> P x
393 \tdx{allE} [| !x. P x; P x ==> R |] ==> R
394 \tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R
396 \tdx{exI} P x ==> ? x. P x
397 \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q
399 \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
400 \tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
403 \tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a
404 \subcaption{Quantifiers and descriptions}
406 \tdx{ccontr} (~P ==> False) ==> P
407 \tdx{classical} (~P ==> P) ==> P
408 \tdx{excluded_middle} ~P | P
410 \tdx{disjCI} (~Q ==> P) ==> P|Q
411 \tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x
412 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
413 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
414 \tdx{notnotD} ~~P ==> P
415 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
416 \subcaption{Classical logic}
418 %\tdx{if_True} (if True then x else y) = x
419 %\tdx{if_False} (if False then x else y) = y
420 \tdx{if_P} P ==> (if P then x else y) = x
421 \tdx{if_not_P} ~ P ==> (if P then x else y) = y
422 \tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
423 \subcaption{Conditionals}
425 \caption{More derived rules} \label{hol-lemmas2}
428 Some derived rules are shown in Figures~\ref{hol-lemmas1}
429 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
430 for the logical connectives, as well as sequent-style elimination rules for
431 conjunctions, implications, and universal quantifiers.
433 Note the equality rules: \tdx{ssubst} performs substitution in
434 backward proofs, while \tdx{box_equals} supports reasoning by
435 simplifying both sides of an equation.
437 The following simple tactics are occasionally useful:
438 \begin{ttdescription}
439 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
440 repeatedly to remove all outermost universal quantifiers and implications
442 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on
443 $P$ for subgoal $i$: the latter is replaced by two identical subgoals with
444 the added assumptions $P$ and $\lnot P$, respectively.
445 \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then
446 \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining
447 from an induction hypothesis. As a generalization of \texttt{mp_tac},
448 if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and
449 $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)
450 then it replaces the universally quantified implication by $Q \vec{a}$.
451 It may instantiate unknowns. It fails if it can do nothing.
458 \it name &\it meta-type & \it description \\
459 \index{{}@\verb'{}' symbol}
460 \verb|{}| & $\alpha\,set$ & the empty set \\
461 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
462 & insertion of element \\
463 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
465 \cdx{Compl} & $\alpha\,set\To\alpha\,set$
467 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
468 & intersection over a set\\
469 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
471 \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
472 &set of sets intersection \\
473 \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
474 &set of sets union \\
475 \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
477 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
478 & range of a function \\[1ex]
479 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
480 & bounded quantifiers
483 \subcaption{Constants}
486 \begin{tabular}{llrrr}
487 \it symbol &\it name &\it meta-type & \it priority & \it description \\
488 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
489 intersection over a type\\
490 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
500 \begin{tabular}{rrrr}
501 \it symbol & \it meta-type & \it priority & \it description \\
502 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$
504 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
505 & Left 70 & intersection ($\int$) \\
506 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
507 & Left 65 & union ($\un$) \\
508 \tt: & $[\alpha ,\alpha\,set]\To bool$
509 & Left 50 & membership ($\in$) \\
510 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
511 & Left 50 & subset ($\subseteq$)
515 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
520 \begin{center} \tt\frenchspacing
523 \it external & \it internal & \it description \\
524 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
525 {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
526 {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &
528 \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &
530 \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
532 \sdx{ALL} $x$:$A$. $P[x]$ or \sdx{!} $x$:$A$. $P[x]$ &
533 Ball $A$ $\lambda x. P[x]$ &
534 \rm bounded $\forall$ \\
535 \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ or \sdx{?} $x$:$A$. $P[x]$ &
536 Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$
539 \subcaption{Translations}
542 \[\begin{array}{rclcl}
543 term & = & \hbox{other terms\ldots} \\
544 & | & "{\ttlbrace}{\ttrbrace}" \\
545 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
546 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
547 & | & term " `` " term \\
548 & | & term " Int " term \\
549 & | & term " Un " term \\
550 & | & "INT~~" id ":" term " . " term \\
551 & | & "UN~~~" id ":" term " . " term \\
552 & | & "INT~~" id~id^* " . " term \\
553 & | & "UN~~~" id~id^* " . " term \\[2ex]
554 formula & = & \hbox{other formulae\ldots} \\
555 & | & term " : " term \\
556 & | & term " \ttilde: " term \\
557 & | & term " <= " term \\
558 & | & "ALL " id ":" term " . " formula
559 & | & "!~" id ":" term " . " formula \\
560 & | & "EX~~" id ":" term " . " formula
561 & | & "?~" id ":" term " . " formula \\
564 \subcaption{Full Grammar}
565 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
569 \section{A formulation of set theory}
570 Historically, higher-order logic gives a foundation for Russell and
571 Whitehead's theory of classes. Let us use modern terminology and call them
572 {\bf sets}, but note that these sets are distinct from those of {\ZF} set
573 theory, and behave more like {\ZF} classes.
576 Sets are given by predicates over some type~$\sigma$. Types serve to
577 define universes for sets, but type-checking is still significant.
579 There is a universal set (for each type). Thus, sets have complements, and
580 may be defined by absolute comprehension.
582 Although sets may contain other sets as elements, the containing set must
583 have a more complex type.
585 Finite unions and intersections have the same behaviour in \HOL\ as they
586 do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
587 denoting the universal set for the given type.
589 \subsection{Syntax of set theory}\index{*set type}
590 \HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
591 essentially the same as $\alpha\To bool$. The new type is defined for
592 clarity and to avoid complications involving function types in unification.
593 The isomorphisms between the two types are declared explicitly. They are
594 very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
595 \hbox{\tt op :} maps in the other direction (ignoring argument order).
597 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
598 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
599 constructs. Infix operators include union and intersection ($A\un B$
600 and $A\int B$), the subset and membership relations, and the image
601 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
604 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
605 the obvious manner using~\texttt{insert} and~$\{\}$:
607 \{a, b, c\} & \equiv &
608 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
611 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
612 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
613 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
614 x. P[x])$. It defines sets by absolute comprehension, which is impossible
615 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
617 The set theory defines two {\bf bounded quantifiers}:
619 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
620 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
622 The constants~\cdx{Ball} and~\cdx{Bex} are defined
623 accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
624 write\index{*"! symbol}\index{*"? symbol}
625 \index{*ALL symbol}\index{*EX symbol}
627 \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The
628 original notation of Gordon's {\sc hol} system is supported as well: \sdx{!}\
631 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
632 $\bigcap@{x\in A}B[x]$, are written
633 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
634 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.
636 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
637 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
638 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous
639 union and intersection operators when $A$ is the universal set.
641 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
642 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
647 \begin{figure} \underscoreon
649 \tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a
650 \tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A
652 \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}
653 \tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B
654 \tdx{Ball_def} Ball A P == ! x. x:A --> P x
655 \tdx{Bex_def} Bex A P == ? x. x:A & P x
656 \tdx{subset_def} A <= B == ! x:A. x:B
657 \tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}
658 \tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}
659 \tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}
660 \tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace}
661 \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
662 \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
663 \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B
664 \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B
665 \tdx{Inter_def} Inter S == (INT x:S. x)
666 \tdx{Union_def} Union S == (UN x:S. x)
667 \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
668 \tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
669 \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
671 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
675 \begin{figure} \underscoreon
677 \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}
678 \tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a
679 \tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W
681 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
682 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
683 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
685 \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
686 \tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x
687 \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
688 \subcaption{Comprehension and Bounded quantifiers}
690 \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B
691 \tdx{subsetD} [| A <= B; c:A |] ==> c:B
692 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
694 \tdx{subset_refl} A <= A
695 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
697 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B
698 \tdx{equalityD1} A = B ==> A<=B
699 \tdx{equalityD2} A = B ==> B<=A
700 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
702 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
703 [| ~ c:A; ~ c:B |] ==> P
705 \subcaption{The subset and equality relations}
707 \caption{Derived rules for set theory} \label{hol-set1}
711 \begin{figure} \underscoreon
713 \tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
715 \tdx{insertI1} a : insert a B
716 \tdx{insertI2} a : B ==> a : insert b B
717 \tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
719 \tdx{ComplI} [| c:A ==> False |] ==> c : Compl A
720 \tdx{ComplD} [| c : Compl A |] ==> ~ c:A
722 \tdx{UnI1} c:A ==> c : A Un B
723 \tdx{UnI2} c:B ==> c : A Un B
724 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
725 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
727 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B
728 \tdx{IntD1} c : A Int B ==> c:A
729 \tdx{IntD2} c : A Int B ==> c:B
730 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
732 \tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
733 \tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
735 \tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
736 \tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
737 \tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
739 \tdx{UnionI} [| X:C; A:X |] ==> A : Union C
740 \tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
742 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
743 \tdx{InterD} [| A : Inter C; X:C |] ==> A:X
744 \tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
746 \tdx{PowI} A<=B ==> A: Pow B
747 \tdx{PowD} A: Pow B ==> A<=B
749 \tdx{imageI} [| x:A |] ==> f x : f``A
750 \tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
752 \tdx{rangeI} f x : range f
753 \tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
755 \caption{Further derived rules for set theory} \label{hol-set2}
759 \subsection{Axioms and rules of set theory}
760 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
761 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
762 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of
763 course, \hbox{\tt op :} also serves as the membership relation.
765 All the other axioms are definitions. They include the empty set, bounded
766 quantifiers, unions, intersections, complements and the subset relation.
767 They also include straightforward constructions on functions: image~({\tt``})
770 %The predicate \cdx{inj_on} is used for simulating type definitions.
771 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
772 %set~$A$, which specifies a subset of its domain type. In a type
773 %definition, $f$ is the abstraction function and $A$ is the set of valid
774 %representations; we should not expect $f$ to be injective outside of~$A$.
776 %\begin{figure} \underscoreon
778 %\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
779 %\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
782 % [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
785 %\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
786 %\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
788 %\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
789 %\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
790 %\tdx{injD} [| inj f; f x = f y |] ==> x=y
792 %\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
793 %\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
795 %\tdx{inj_on_inverseI}
796 % (!!x. x:A ==> g(f x) = x) ==> inj_on f A
797 %\tdx{inj_on_contraD}
798 % [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
800 %\caption{Derived rules involving functions} \label{hol-fun}
804 \begin{figure} \underscoreon
806 \tdx{Union_upper} B:A ==> B <= Union A
807 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
809 \tdx{Inter_lower} B:A ==> Inter A <= B
810 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
812 \tdx{Un_upper1} A <= A Un B
813 \tdx{Un_upper2} B <= A Un B
814 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
816 \tdx{Int_lower1} A Int B <= A
817 \tdx{Int_lower2} A Int B <= B
818 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
820 \caption{Derived rules involving subsets} \label{hol-subset}
824 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
826 \tdx{Int_absorb} A Int A = A
827 \tdx{Int_commute} A Int B = B Int A
828 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
829 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
831 \tdx{Un_absorb} A Un A = A
832 \tdx{Un_commute} A Un B = B Un A
833 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
834 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
836 \tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace}
837 \tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x. True{\ttrbrace}
838 \tdx{double_complement} Compl(Compl A) = A
839 \tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B)
840 \tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B)
842 \tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
843 \tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
844 \tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
846 \tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
847 \tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
848 \tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
850 \caption{Set equalities} \label{hol-equalities}
854 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
855 obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
856 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
857 are designed for classical reasoning; the rules \tdx{subsetD},
858 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
859 strictly necessary but yield more natural proofs. Similarly,
860 \tdx{equalityCE} supports classical reasoning about extensionality,
861 after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for
862 proofs pertaining to set theory.
864 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
865 Unions form least upper bounds; non-empty intersections form greatest lower
866 bounds. Reasoning directly about subsets often yields clearer proofs than
867 reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.
869 Figure~\ref{hol-equalities} presents many common set equalities. They
870 include commutative, associative and distributive laws involving unions,
871 intersections and complements. For a complete listing see the file {\tt
875 \texttt{Blast_tac} proves many set-theoretic theorems automatically.
876 Hence you seldom need to refer to the theorems above.
882 \it name &\it meta-type & \it description \\
883 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
884 & injective/surjective \\
885 \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
886 & injective over subset\\
887 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
893 \tdx{inj_def} inj f == ! x y. f x=f y --> x=y
894 \tdx{surj_def} surj f == ! y. ? x. y=f x
895 \tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
896 \tdx{inv_def} inv f == (\%y. @x. f(x)=y)
898 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
901 \subsection{Properties of functions}\nopagebreak
902 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
903 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
904 of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
905 rules. Reasoning about function composition (the operator~\sdx{o}) and the
906 predicate~\cdx{surj} is done simply by expanding the definitions.
908 There is also a large collection of monotonicity theorems for constructions
909 on sets in the file \texttt{HOL/mono.ML}.
912 \section{Generic packages}
913 \label{sec:HOL:generic-packages}
915 \HOL\ instantiates most of Isabelle's generic packages, making available the
916 simplifier and the classical reasoner.
918 \subsection{Simplification and substitution}
920 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
921 (\texttt{simpset()}), which works for most purposes. A quite minimal
922 simplification set for higher-order logic is~\ttindexbold{HOL_ss};
923 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
924 also expresses logical equivalence, may be used for rewriting. See
925 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
926 simplification rules.
928 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
929 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
932 \begin{warn}\index{simplification!of conjunctions}%
933 Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
934 left part of a conjunction helps in simplifying the right part. This effect
935 is not available by default: it can be slow. It can be obtained by
936 including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
939 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%
940 By default only the condition of an \ttindex{if} is simplified but not the
941 \texttt{then} and \texttt{else} parts. Of course the latter are simplified
942 once the condition simplifies to \texttt{True} or \texttt{False}. To ensure
943 full simplification of all parts of a conditional you must remove
944 \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.
947 If the simplifier cannot use a certain rewrite rule --- either because
948 of nontermination or because its left-hand side is too flexible ---
949 then you might try \texttt{stac}:
950 \begin{ttdescription}
951 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
952 replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
953 $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking
954 may be necessary to select the desired ones.
956 If $thm$ is a conditional equality, the instantiated condition becomes an
957 additional (first) subgoal.
960 \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
961 for an equality throughout a subgoal and its hypotheses. This tactic uses
962 \HOL's general substitution rule.
964 \subsubsection{Case splitting}
965 \label{subsec:HOL:case:splitting}
967 \HOL{} also provides convenient means for case splitting during
968 rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
969 then\dots else\dots} often require a case distinction on $b$. This is
970 expressed by the theorem \tdx{split_if}:
972 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
973 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
976 For example, a simple instance of $(*)$ is
978 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
979 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
981 Because $(*)$ is too general as a rewrite rule for the simplifier (the
982 left-hand side is not a higher-order pattern in the sense of
983 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
984 {Chap.\ts\ref{chap:simplification}}), there is a special infix function
985 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
986 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
989 by(simp_tac (simpset() addsplits [split_if]) 1);
991 The effect is that after each round of simplification, one occurrence of
992 \texttt{if} is split acording to \texttt{split_if}, until all occurences of
993 \texttt{if} have been eliminated.
995 It turns out that using \texttt{split_if} is almost always the right thing to
996 do. Hence \texttt{split_if} is already included in the default simpset. If
997 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
998 the inverse of \texttt{addsplits}:
1000 by(simp_tac (simpset() delsplits [split_if]) 1);
1003 In general, \texttt{addsplits} accepts rules of the form
1005 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
1007 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
1008 right form because internally the left-hand side is
1009 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
1010 are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}
1011 and~{\S}\ref{subsec:datatype:basics}).
1013 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
1014 imperative versions of \texttt{addsplits} and \texttt{delsplits}
1016 \ttindexbold{Addsplits}: thm list -> unit
1017 \ttindexbold{Delsplits}: thm list -> unit
1019 for adding splitting rules to, and deleting them from the current simpset.
1021 \subsection{Classical reasoning}
1023 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1024 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1025 rule; recall Fig.\ts\ref{hol-lemmas2} above.
1027 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and
1028 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
1029 for most purposes. Named clasets include \ttindexbold{prop_cs}, which
1030 includes the propositional rules, and \ttindexbold{HOL_cs}, which also
1031 includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of
1032 the classical rules,
1033 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1034 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
1037 \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
1039 \index{SVC decision procedure|(}
1041 The Stanford Validity Checker (SVC) is a tool that can check the validity of
1042 certain types of formulae. If it is installed on your machine, then
1043 Isabelle/HOL can be configured to call it through the tactic
1044 \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in
1045 linear arithmetic. Subexpressions that SVC cannot handle are automatically
1046 replaced by variables, so you can call the tactic on any subgoal. See the
1047 file \texttt{HOL/ex/svc_test.ML} for examples.
1049 svc_tac : int -> tactic
1050 Svc.trace : bool ref \hfill{\bf initially false}
1053 \begin{ttdescription}
1054 \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
1055 it into a formula recognized by~SVC\@. If it succeeds then the subgoal is
1056 removed. It fails if SVC is unable to prove the subgoal. It crashes with
1057 an error message if SVC appears not to be installed. Numeric variables may
1058 have types \texttt{nat}, \texttt{int} or \texttt{real}.
1060 \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
1061 to trace its operations: abstraction of the subgoal, translation to SVC
1062 syntax, SVC's response.
1065 Here is an example, with tracing turned on:
1068 {\out val it : bool = true}
1069 Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback
1070 \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c";
1073 {\out Subgoal abstracted to}
1074 {\out #3 * a <= #2 + #4 * b + #6 * c &}
1075 {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
1076 {\out #2 + #3 * b <= #2 * a + #6 * c}
1078 {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )}
1079 {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } }
1080 {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }}
1081 {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 }
1082 {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ }
1083 {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) }
1087 {\out #3 * a <= #2 + #4 * b + #6 * c &}
1088 {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
1089 {\out #2 + #3 * b <= #2 * a + #6 * c}
1095 Calling \ttindex{svc_tac} entails an above-average risk of
1096 unsoundness. Isabelle does not check SVC's result independently. Moreover,
1097 the tactic translates the submitted formula using code that lies outside
1098 Isabelle's inference core. Theorems that depend upon results proved using SVC
1099 (and other oracles) are displayed with the annotation \texttt{[!]} attached.
1100 You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
1101 theorem~$th$, as described in the \emph{Reference Manual}.
1104 To start, first download SVC from the Internet at URL
1106 http://agamemnon.stanford.edu/~levitt/vc/index.html
1108 and install it using the instructions supplied. SVC requires two environment
1110 \begin{ttdescription}
1111 \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
1112 distribution directory.
1114 \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
1117 You can set these environment variables either using the Unix shell or through
1118 an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if
1119 \texttt{SVC_HOME} is defined.
1121 \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren
1125 \index{SVC decision procedure|)}
1130 \section{Types}\label{sec:HOL:Types}
1131 This section describes \HOL's basic predefined types ($\alpha \times
1132 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
1133 introducing new types in general. The most important type
1134 construction, the \texttt{datatype}, is treated separately in
1135 {\S}\ref{sec:HOL:datatype}.
1138 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1139 \label{subsec:prod-sum}
1141 \begin{figure}[htbp]
1143 \it symbol & \it meta-type & & \it description \\
1144 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
1145 & & ordered pairs $(a,b)$ \\
1146 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
1147 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
1148 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
1149 & & generalized projection\\
1151 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
1152 & general sum of sets
1154 \begin{ttbox}\makeatletter
1155 %\tdx{fst_def} fst p == @a. ? b. p = (a,b)
1156 %\tdx{snd_def} snd p == @b. ? a. p = (a,b)
1157 %\tdx{split_def} split c p == c (fst p) (snd p)
1158 \tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
1160 \tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
1161 \tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
1162 \tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
1164 \tdx{fst_conv} fst (a,b) = a
1165 \tdx{snd_conv} snd (a,b) = b
1166 \tdx{surjective_pairing} p = (fst p,snd p)
1168 \tdx{split} split c (a,b) = c a b
1169 \tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
1171 \tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
1172 \tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
1174 \caption{Type $\alpha\times\beta$}\label{hol-prod}
1177 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
1178 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
1179 tuples are simulated by pairs nested to the right:
1181 \begin{tabular}{c|c}
1182 external & internal \\
1184 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
1186 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
1189 In addition, it is possible to use tuples
1190 as patterns in abstractions:
1192 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}
1194 Nested patterns are also supported. They are translated stepwise:
1195 {\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$
1196 {\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
1197 $z$.\ $t$))}. The reverse translation is performed upon printing.
1199 The translation between patterns and \texttt{split} is performed automatically
1200 by the parser and printer. Thus the internal and external form of a term
1201 may differ, which can affects proofs. For example the term {\tt
1202 (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
1203 default simpset) to rewrite to {\tt(b,a)}.
1205 In addition to explicit $\lambda$-abstractions, patterns can be used in any
1206 variable binding construct which is internally described by a
1207 $\lambda$-abstraction. Some important examples are
1209 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
1210 \item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
1211 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
1212 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
1213 \item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
1216 There is a simple tactic which supports reasoning about patterns:
1217 \begin{ttdescription}
1218 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
1219 {\tt!!}-quantified variables of product type by individual variables for
1220 each component. A simple example:
1222 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
1223 by(split_all_tac 1);
1224 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
1228 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
1229 which contains only a single element named {\tt()} with the property
1231 \tdx{unit_eq} u = ()
1235 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
1236 which associates to the right and has a lower priority than $*$: $\tau@1 +
1237 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
1239 The definition of products and sums in terms of existing types is not
1240 shown. The constructions are fairly standard and can be found in the
1241 respective theory files. Although the sum and product types are
1242 constructed manually for foundational reasons, they are represented as
1243 actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).
1244 Therefore, the theory \texttt{Datatype} should be used instead of
1245 \texttt{Sum} or \texttt{Prod}.
1249 \it symbol & \it meta-type & & \it description \\
1250 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
1251 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
1252 \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
1255 \begin{ttbox}\makeatletter
1256 \tdx{Inl_not_Inr} Inl a ~= Inr b
1258 \tdx{inj_Inl} inj Inl
1259 \tdx{inj_Inr} inj Inr
1261 \tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
1263 \tdx{sum_case_Inl} sum_case f g (Inl x) = f x
1264 \tdx{sum_case_Inr} sum_case f g (Inr x) = g x
1266 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
1267 \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
1268 (! y. s = Inr(y) --> R(g(y))))
1270 \caption{Type $\alpha+\beta$}\label{hol-sum}
1281 \it symbol & \it meta-type & \it priority & \it description \\
1282 \cdx{0} & $nat$ & & zero \\
1283 \cdx{Suc} & $nat \To nat$ & & successor function\\
1284 % \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\
1285 % \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
1286 % & & primitive recursor\\
1287 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
1288 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
1289 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
1290 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
1291 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1293 \subcaption{Constants and infixes}
1295 \begin{ttbox}\makeatother
1296 \tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n
1298 \tdx{Suc_not_Zero} Suc m ~= 0
1299 \tdx{inj_Suc} inj Suc
1300 \tdx{n_not_Suc_n} n~=Suc n
1301 \subcaption{Basic properties}
1303 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
1308 \begin{ttbox}\makeatother
1310 (Suc m)+n = Suc(m+n)
1319 \tdx{mod_less} m<n ==> m mod n = m
1320 \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
1322 \tdx{div_less} m<n ==> m div n = 0
1323 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
1325 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
1328 \subsection{The type of natural numbers, \textit{nat}}
1329 \index{nat@{\textit{nat}} type|(}
1331 The theory \thydx{NatDef} defines the natural numbers in a roundabout but
1332 traditional way. The axiom of infinity postulates a type~\tydx{ind} of
1333 individuals, which is non-empty and closed under an injective operation. The
1334 natural numbers are inductively generated by choosing an arbitrary individual
1335 for~0 and using the injective operation to take successors. This is a least
1336 fixedpoint construction. For details see the file \texttt{NatDef.thy}.
1338 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the
1339 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also
1340 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory
1341 \thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order,
1342 so \tydx{nat} is also an instance of class \cldx{order}.
1344 Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines
1345 addition, multiplication and subtraction. Theory \thydx{Divides} defines
1346 division, remainder and the ``divides'' relation. The numerous theorems
1347 proved include commutative, associative, distributive, identity and
1348 cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The
1349 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
1350 \texttt{nat} are part of the default simpset.
1352 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
1353 see {\S}\ref{sec:HOL:recursive}. A simple example is addition.
1354 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1355 the standard convention.
1359 "Suc m + n = Suc (m + n)"
1361 There is also a \sdx{case}-construct
1364 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
1366 Note that Isabelle insists on precisely this format; you may not even change
1367 the order of the two cases.
1368 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
1369 \cdx{nat_rec}, which is available because \textit{nat} is represented as
1370 a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).
1372 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1373 %Recursion along this relation resembles primitive recursion, but is
1374 %stronger because we are in higher-order logic; using primitive recursion to
1375 %define a higher-order function, we can easily Ackermann's function, which
1376 %is not primitive recursive \cite[page~104]{thompson91}.
1377 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1378 %natural numbers are most easily expressed using recursion along~$<$.
1380 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
1381 in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived
1382 theorem \tdx{less_induct}:
1384 [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
1388 Reasoning about arithmetic inequalities can be tedious. Fortunately HOL
1389 provides a decision procedure for quantifier-free linear arithmetic (i.e.\
1390 only addition and subtraction). The simplifier invokes a weak version of this
1391 decision procedure automatically. If this is not sufficent, you can invoke
1392 the full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary
1393 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
1394 min}, {\tt max} and numerical constants; other subterms are treated as
1395 atomic; subformulae not involving type $nat$ are ignored; quantified
1396 subformulae are ignored unless they are positive universal or negative
1397 existential. Note that the running time is exponential in the number of
1398 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
1399 distinctions. Note also that \texttt{arith_tac} is not complete: if
1400 divisibility plays a role, it may fail to prove a valid formula, for example
1401 $m+m \neq n+n+1$. Fortunately such examples are rare in practice.
1403 If \texttt{arith_tac} fails you, try to find relevant arithmetic results in
1404 the library. The theory \texttt{NatDef} contains theorems about {\tt<} and
1405 {\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
1406 \texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
1407 \texttt{div} and \texttt{mod}. Use the \texttt{find}-functions to locate them
1408 (see the {\em Reference Manual\/}).
1411 \index{#@{\tt[]} symbol}
1412 \index{#@{\tt\#} symbol}
1413 \index{"@@{\tt\at} symbol}
1416 \it symbol & \it meta-type & \it priority & \it description \\
1417 \tt[] & $\alpha\,list$ & & empty list\\
1418 \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
1420 \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
1421 \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
1422 \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
1423 \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
1424 \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
1425 \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
1426 \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
1428 \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
1429 & & filter functional\\
1430 \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
1431 \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
1432 \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
1434 \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
1435 \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
1436 \cdx{length} & $\alpha\,list \To nat$ & & length \\
1437 \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
1438 \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
1439 take or drop a prefix \\
1442 $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
1443 take or drop a prefix
1445 \subcaption{Constants and infixes}
1447 \begin{center} \tt\frenchspacing
1448 \begin{tabular}{rrr}
1449 \it external & \it internal & \it description \\{}
1450 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1451 \rm finite list \\{}
1452 [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
1453 \rm list comprehension
1456 \subcaption{Translations}
1457 \caption{The theory \thydx{List}} \label{hol-list}
1462 \begin{ttbox}\makeatother
1471 (x#xs) @ ys = x # xs @ ys
1474 map f (x#xs) = f x # map f xs
1477 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
1479 set [] = \ttlbrace\ttrbrace
1480 set (x#xs) = insert x (set xs)
1483 x mem (y#ys) = (if y=x then True else x mem ys)
1486 foldl f a (x#xs) = foldl f (f a x) xs
1489 concat(x#xs) = x @ concat(xs)
1492 rev(x#xs) = rev(xs) @ [x]
1495 length(x#xs) = Suc(length(xs))
1498 xs!(Suc n) = (tl xs)!n
1501 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
1504 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
1507 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
1510 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
1512 \caption{Recursions equations for list processing functions}
1513 \label{fig:HOL:list-simps}
1515 \index{nat@{\textit{nat}} type|)}
1518 \subsection{The type constructor for lists, \textit{list}}
1520 \index{list@{\textit{list}} type|(}
1522 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
1523 operations with their types and syntax. Type $\alpha \; list$ is
1524 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
1525 As a result the generic structural induction and case analysis tactics
1526 \texttt{induct\_tac} and \texttt{cases\_tac} also become available for
1527 lists. A \sdx{case} construct of the form
1529 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
1531 is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There
1532 is also a case splitting rule \tdx{split_list_case}
1535 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
1536 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
1537 ((e = \texttt{[]} \to P(a)) \land
1538 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
1541 which can be fed to \ttindex{addsplits} just like
1542 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
1544 \texttt{List} provides a basic library of list processing functions defined by
1545 primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations
1546 are shown in Fig.\ts\ref{fig:HOL:list-simps}.
1548 \index{list@{\textit{list}} type|)}
1551 \subsection{Introducing new types} \label{sec:typedef}
1553 The \HOL-methodology dictates that all extensions to a theory should
1554 be \textbf{definitional}. The type definition mechanism that
1555 meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms},
1556 which are inherited from {\Pure} and described elsewhere, are just
1557 syntactic abbreviations that have no logical meaning.
1560 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1561 unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
1563 A \bfindex{type definition} identifies the new type with a subset of
1564 an existing type. More precisely, the new type is defined by
1565 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
1566 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
1567 and the new type denotes this subset. New functions are defined that
1568 establish an isomorphism between the new type and the subset. If
1569 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
1570 then the type definition creates a type constructor
1571 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
1573 \begin{figure}[htbp]
1575 typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
1577 type : typevarlist name ( () | '(' infix ')' );
1579 witness : () | '(' id ')';
1581 \caption{Syntax of type definitions}
1582 \label{fig:HOL:typedef}
1585 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
1586 the definition of `typevarlist' and `infix' see
1587 \iflabelundefined{chap:classical}
1588 {the appendix of the {\em Reference Manual\/}}%
1589 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
1592 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
1593 optional infix annotation.
1594 \item[\it name:] an alphanumeric name $T$ for the type constructor
1595 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
1596 \item[\it set:] the representing subset $A$.
1597 \item[\it witness:] name of a theorem of the form $a:A$ proving
1598 non-emptiness. It can be omitted in case Isabelle manages to prove
1599 non-emptiness automatically.
1601 If all context conditions are met (no duplicate type variables in
1602 `typevarlist', no extra type variables in `set', and no free term variables
1603 in `set'), the following components are added to the theory:
1605 \item a type $ty :: (term,\dots,term)term$
1609 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
1610 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
1612 \item a definition and three axioms
1615 T{\tt_def} & T \equiv A \\
1616 {\tt Rep_}T & Rep_T\,x \in T \\
1617 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
1618 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y
1621 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
1622 and its inverse $Abs_T$.
1624 Below are two simple examples of \HOL\ type definitions. Non-emptiness
1625 is proved automatically here.
1627 typedef unit = "{\ttlbrace}True{\ttrbrace}"
1630 ('a, 'b) "*" (infixr 20)
1631 = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
1634 Type definitions permit the introduction of abstract data types in a safe
1635 way, namely by providing models based on already existing types. Given some
1636 abstract axiomatic description $P$ of a type, this involves two steps:
1638 \item Find an appropriate type $\tau$ and subset $A$ which has the desired
1639 properties $P$, and make a type definition based on this representation.
1640 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
1642 You can now forget about the representation and work solely in terms of the
1643 abstract properties $P$.
1646 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
1647 declaring the type and its operations and by stating the desired axioms, you
1648 should make sure the type has a non-empty model. You must also have a clause
1651 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
1653 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
1654 class of all \HOL\ types.
1660 At a first approximation, records are just a minor generalisation of tuples,
1661 where components may be addressed by labels instead of just position (think of
1662 {\ML}, for example). The version of records offered by Isabelle/HOL is
1663 slightly more advanced, though, supporting \emph{extensible record schemes}.
1664 This admits operations that are polymorphic with respect to record extension,
1665 yielding ``object-oriented'' effects like (single) inheritance. See also
1666 \cite{NaraschewskiW-TPHOLs98} for more details on object-oriented
1667 verification and record subtyping in HOL.
1672 Isabelle/HOL supports fixed and schematic records both at the level of terms
1673 and types. The concrete syntax is as follows:
1676 \begin{tabular}{l|l|l}
1677 & record terms & record types \\ \hline
1678 fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
1679 schematic & $\record{x = a\fs y = b\fs \more = m}$ &
1680 $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
1684 \noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
1686 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
1687 $y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$,
1688 assuming that $a \ty A$ and $b \ty B$.
1690 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
1691 $x$ and $y$ as before, but also possibly further fields as indicated by the
1692 ``$\more$'' notation (which is actually part of the syntax). The improper
1693 field ``$\more$'' of a record scheme is called the \emph{more part}.
1694 Logically it is just a free variable, which is occasionally referred to as
1695 \emph{row variable} in the literature. The more part of a record scheme may
1696 be instantiated by zero or more further components. For example, above scheme
1697 might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
1698 where $m'$ refers to a different more part. Fixed records are special
1699 instances of record schemes, where ``$\more$'' is properly terminated by the
1700 $() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an
1701 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
1705 There are two key features that make extensible records in a simply typed
1706 language like HOL feasible:
1708 \item the more part is internalised, as a free term or type variable,
1709 \item field names are externalised, they cannot be accessed within the logic
1710 as first-class values.
1715 In Isabelle/HOL record types have to be defined explicitly, fixing their field
1716 names and types, and their (optional) parent record (see
1717 {\S}\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
1718 syntax, while obeying the canonical order of fields as given by their
1719 declaration. The record package also provides several operations like
1720 selectors and updates (see {\S}\ref{sec:HOL:record-ops}), together with
1721 characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
1723 There is an example theory demonstrating most basic aspects of extensible
1724 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
1727 \subsection{Defining records}\label{sec:HOL:record-def}
1729 The theory syntax for record type definitions is shown in
1730 Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see
1731 \iflabelundefined{chap:classical}
1732 {the appendix of the {\em Reference Manual\/}}%
1733 {Appendix~\ref{app:TheorySyntax}}.
1735 \begin{figure}[htbp]
1737 record : 'record' typevarlist name '=' parent (field +);
1739 parent : ( () | type '+');
1740 field : name '::' type;
1742 \caption{Syntax of record type definitions}
1743 \label{fig:HOL:record}
1746 A general \ttindex{record} specification is of the following form:
1748 \mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
1749 (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
1751 where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
1752 $\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
1753 Type constructor $t$ has to be new, while $s$ has to specify an existing
1754 record type. Furthermore, the $\vec c@l$ have to be distinct field names.
1755 There has to be at least one field.
1757 In principle, field names may never be shared with other records. This is no
1758 actual restriction in practice, since $\vec c@l$ are internally declared
1759 within a separate name space qualified by the name $t$ of the record.
1763 Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
1764 extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
1765 \vec\sigma@l$. The parent record specification is optional, by omitting it
1766 $t$ becomes a \emph{root record}. The hierarchy of all records declared
1767 within a theory forms a forest structure, i.e.\ a set of trees, where any of
1768 these is rooted by some root record.
1770 For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
1771 fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
1772 \zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
1773 \vec\sigma@l\fs \more \ty \zeta}$.
1777 The following simple example defines a root record type $point$ with fields $x
1778 \ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
1779 an additional $colour$ component.
1786 record cpoint = point +
1791 \subsection{Record operations}\label{sec:HOL:record-ops}
1793 Any record definition of the form presented above produces certain standard
1794 operations. Selectors and updates are provided for any field, including the
1795 improper one ``$more$''. There are also cumulative record constructor
1798 To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
1799 is a root record with fields $\vec c@l \ty \vec\sigma@l$.
1803 \textbf{Selectors} and \textbf{updates} are available for any field (including
1804 ``$more$'') as follows:
1805 \begin{matharray}{lll}
1806 c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
1807 c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
1808 \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1811 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
1812 term $x_update \, a \, r$. Repeated updates are also supported: $r \,
1813 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
1814 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of
1815 postfix notation the order of fields shown here is reverse than in the actual
1816 term. This might lead to confusion in conjunction with proof tools like
1819 Since repeated updates are just function applications, fields may be freely
1820 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
1821 is concerned. Thus commutativity of updates can be proven within the logic
1822 for any two fields, but not as a general theorem: fields are not first-class
1827 \textbf{Make} operations provide cumulative record constructor functions:
1828 \begin{matharray}{lll}
1829 make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
1830 make_scheme & \ty & \vec\sigma@l \To
1831 \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
1834 These functions are curried. The corresponding definitions in terms of actual
1835 record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$
1836 rewrites to $\record{x = a\fs y = b}$.
1840 Any of above selector, update and make operations are declared within a local
1841 name space prefixed by the name $t$ of the record. In case that different
1842 records share base names of fields, one has to qualify names explicitly (e.g.\
1843 $t\dtt c@i_update$). This is recommended especially for operations like
1844 $make$ or $update_more$ that always have the same base name. Just use $t\dtt
1845 make$ etc.\ to avoid confusion.
1849 We reconsider the case of non-root records, which are derived of some parent
1850 record. In general, the latter may depend on another parent as well,
1851 resulting in a list of \emph{ancestor records}. Appending the lists of fields
1852 of all ancestors results in a certain field prefix. The record package
1853 automatically takes care of this by lifting operations over this context of
1854 ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
1855 $\vec d@k \ty \vec\rho@k$, selectors will get the following types:
1856 \begin{matharray}{lll}
1857 c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1861 Update and make operations are analogous.
1864 \subsection{Proof tools}\label{sec:HOL:record-thms}
1866 The record package provides the following proof rules for any record type $t$.
1869 \item Standard conversions (selectors or updates applied to record constructor
1870 terms, make function definitions) are part of the standard simpset (via
1873 \item Selectors applied to updated records are automatically reduced by
1874 simplification procedure \ttindex{record_simproc}, which is part of the
1877 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
1878 \conj y=y'$ are made part of the standard simpset and claset (via
1881 \item A tactic for record field splitting (\ttindex{record_split_tac}) may be
1882 made part of the claset (via \texttt{addSWrapper}). This tactic is based on
1883 rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for
1887 The first two kinds of rules are stored within the theory as $t\dtt simps$ and
1888 $t\dtt iffs$, respectively. In some situations it might be appropriate to
1889 expand the definitions of updates: $t\dtt update_defs$. Note that these names
1890 are \emph{not} bound at the {\ML} level.
1894 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
1895 concerning records. The basic idea is to make \ttindex{record_split_tac}
1896 expand quantified record variables and then simplify by the conversion rules.
1897 By using a combination of the simplifier and classical prover together with
1898 the default simpset and claset, record problems should be solved with a single
1899 stroke of \texttt{Auto_tac} or \texttt{Force_tac}. Most of the time, plain
1900 \texttt{Simp_tac} should be sufficient, though.
1903 \section{Datatype definitions}
1904 \label{sec:HOL:datatype}
1907 Inductive datatypes, similar to those of \ML, frequently appear in
1908 applications of Isabelle/HOL. In principle, such types could be defined by
1909 hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too
1910 tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
1911 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an
1912 appropriate \texttt{typedef} based on a least fixed-point construction, and
1913 proves freeness theorems and induction rules, as well as theorems for
1914 recursion and case combinators. The user just has to give a simple
1915 specification of new inductive types using a notation similar to {\ML} or
1918 The current datatype package can handle both mutual and indirect recursion.
1919 It also offers to represent existing types as datatypes giving the advantage
1920 of a more uniform view on standard theories.
1924 \label{subsec:datatype:basics}
1926 A general \texttt{datatype} definition is of the following form:
1929 \mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = &
1930 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~
1931 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\
1933 \mathtt{and} & (\alpha@1,\ldots,\alpha@h)t@n & = &
1934 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~
1935 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}
1938 where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor
1939 names and $\tau^j@{i,i'}$ are {\em admissible} types containing at
1940 most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$
1941 occurring in a \texttt{datatype} definition is {\em admissible} iff
1943 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
1944 newly defined type constructors $t@1,\ldots,t@n$, or
1945 \item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or
1946 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
1947 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1948 are admissible types.
1949 \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible
1950 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
1951 types are {\em strictly positive})
1953 If some $(\alpha@1,\ldots,\alpha@h)t@{j'}$ occurs in a type $\tau^j@{i,i'}$
1956 (\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t'
1958 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
1959 example of a datatype is the type \texttt{list}, which can be defined by
1961 datatype 'a list = Nil
1964 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
1965 by the mutually recursive datatype definition
1967 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
1968 | Sum ('a aexp) ('a aexp)
1969 | Diff ('a aexp) ('a aexp)
1972 and 'a bexp = Less ('a aexp) ('a aexp)
1973 | And ('a bexp) ('a bexp)
1974 | Or ('a bexp) ('a bexp)
1976 The datatype \texttt{term}, which is defined by
1978 datatype ('a, 'b) term = Var 'a
1979 | App 'b ((('a, 'b) term) list)
1981 is an example for a datatype with nested recursion. Using nested recursion
1982 involving function spaces, we may also define infinitely branching datatypes, e.g.
1984 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
1989 Types in HOL must be non-empty. Each of the new datatypes
1990 $(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \leq j \leq n$ is non-empty iff it has a
1991 constructor $C^j@i$ with the following property: for all argument types
1992 $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
1993 $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
1995 If there are no nested occurrences of the newly defined datatypes, obviously
1996 at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$
1997 must have a constructor $C^j@i$ without recursive arguments, a \emph{base
1998 case}, to ensure that the new types are non-empty. If there are nested
1999 occurrences, a datatype can even be non-empty without having a base case
2000 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
2001 list)} is non-empty as well.
2004 \subsubsection{Freeness of the constructors}
2006 The datatype constructors are automatically defined as functions of their
2008 \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
2009 These functions have certain {\em freeness} properties. They construct
2012 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
2013 \mbox{for all}~ i \neq i'.
2015 The constructor functions are injective:
2017 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
2018 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
2020 Since the number of distinctness inequalities is quadratic in the number of
2021 constructors, the datatype package avoids proving them separately if there are
2022 too many constructors. Instead, specific inequalities are proved by a suitable
2023 simplification procedure on demand.\footnote{This procedure, which is already part
2024 of the default simpset, may be referred to by the ML identifier
2025 \texttt{DatatypePackage.distinct_simproc}.}
2027 \subsubsection{Structural induction}
2029 The datatype package also provides structural induction rules. For
2030 datatypes without nested recursion, this is of the following form:
2032 \infer{P@1~x@1 \land \dots \land P@n~x@n}
2034 \Forall x@1 \dots x@{m^1@1}.
2035 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
2036 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &
2037 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\
2039 \Forall x@1 \dots x@{m^1@{k@1}}.
2040 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;
2041 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &
2042 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\
2044 \Forall x@1 \dots x@{m^n@1}.
2045 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;
2046 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &
2047 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\
2049 \Forall x@1 \dots x@{m^n@{k@n}}.
2050 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots
2051 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &
2052 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)
2059 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
2060 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
2061 && \left\{(i',i'')~\left|~
2062 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land
2063 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
2066 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
2068 For datatypes with nested recursion, such as the \texttt{term} example from
2069 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
2072 datatype ('a, 'b) term = Var 'a
2073 | App 'b ((('a, 'b) term) list)
2075 to an equivalent definition without nesting:
2077 datatype ('a, 'b) term = Var
2078 | App 'b (('a, 'b) term_list)
2079 and ('a, 'b) term_list = Nil'
2080 | Cons' (('a,'b) term) (('a,'b) term_list)
2082 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
2083 Nil'} and \texttt{Cons'} are not really introduced. One can directly work with
2084 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
2085 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
2086 \texttt{term} gets the form
2088 \infer{P@1~x@1 \land P@2~x@2}
2090 \Forall x.~P@1~(\mathtt{Var}~x) \\
2091 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
2093 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
2096 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
2097 and one for the type \texttt{(('a, 'b) term) list}.
2099 For a datatype with function types such as \texttt{'a tree}, the induction rule
2103 {\Forall a.~P~(\mathtt{Atom}~a) &
2104 \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}
2107 \medskip In principle, inductive types are already fully determined by
2108 freeness and structural induction. For convenience in applications,
2109 the following derived constructions are automatically provided for any
2112 \subsubsection{The \sdx{case} construct}
2114 The type comes with an \ML-like \texttt{case}-construct:
2117 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
2119 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}
2122 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
2123 {\S}\ref{subsec:prod-sum}.
2125 All constructors must be present, their order is fixed, and nested patterns
2126 are not supported (with the exception of tuples). Violating this
2127 restriction results in strange error messages.
2130 To perform case distinction on a goal containing a \texttt{case}-construct,
2131 the theorem $t@j.$\texttt{split} is provided:
2133 \begin{array}{@{}rcl@{}}
2134 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&
2135 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to
2136 P(f@1~x@1\dots x@{m^j@1})) \\
2137 &&\!\!\! ~\land~ \dots ~\land \\
2138 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to
2139 P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))
2142 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
2143 This theorem can be added to a simpset via \ttindex{addsplits}
2144 (see~{\S}\ref{subsec:HOL:case:splitting}).
2146 \begin{warn}\index{simplification!of \texttt{case}}%
2147 By default only the selector expression ($e$ above) in a
2148 \texttt{case}-construct is simplified, in analogy with \texttt{if} (see
2149 page~\pageref{if-simp}). Only if that reduces to a constructor is one of
2150 the arms of the \texttt{case}-construct exposed and simplified. To ensure
2151 full simplification of all parts of a \texttt{case}-construct for datatype
2152 $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
2153 example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
2156 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
2158 Theory \texttt{Arith} declares a generic function \texttt{size} of type
2159 $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
2160 by overloading according to the following scheme:
2161 %%% FIXME: This formula is too big and is completely unreadable
2163 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
2166 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\
2167 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &
2168 \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
2169 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}
2173 where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
2174 size of a leaf is 0 and the size of a node is the sum of the sizes of its
2177 \subsection{Defining datatypes}
2179 The theory syntax for datatype definitions is shown in
2180 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
2181 definition has to obey the rules stated in the previous section. As a result
2182 the theory is extended with the new types, the constructors, and the theorems
2183 listed in the previous section.
2187 datatype : 'datatype' typedecls;
2189 typedecls: ( newtype '=' (cons + '|') ) + 'and'
2191 newtype : typevarlist id ( () | '(' infix ')' )
2193 cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
2195 argtype : id | tid | ('(' typevarlist id ')')
2198 \caption{Syntax of datatype declarations}
2199 \label{datatype-grammar}
2202 Most of the theorems about datatypes become part of the default simpset and
2203 you never need to see them again because the simplifier applies them
2204 automatically. Only induction or case distinction are usually invoked by hand.
2205 \begin{ttdescription}
2206 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
2207 applies structural induction on variable $x$ to subgoal $i$, provided the
2208 type of $x$ is a datatype.
2209 \item[\texttt{induct_tac}
2210 {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous
2211 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This
2212 is the canonical way to prove properties of mutually recursive datatypes
2213 such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as
2216 In some cases, induction is overkill and a case distinction over all
2217 constructors of the datatype suffices.
2218 \begin{ttdescription}
2219 \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]
2220 performs a case analysis for the term $u$ whose type must be a datatype.
2221 If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal
2222 $i$ is replaced by $k@j$ new subgoals which contain the additional
2223 assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$.
2226 Note that induction is only allowed on free variables that should not occur
2227 among the premises of the subgoal. Case distinction applies to arbitrary terms.
2232 For the technically minded, we exhibit some more details. Processing the
2233 theory file produces an \ML\ structure which, in addition to the usual
2234 components, contains a structure named $t$ for each datatype $t$ defined in
2235 the file. Each structure $t$ contains the following elements:
2237 val distinct : thm list
2238 val inject : thm list
2241 val cases : thm list
2246 val simps : thm list
2248 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}
2249 and \texttt{split} contain the theorems
2250 described above. For user convenience, \texttt{distinct} contains
2251 inequalities in both directions. The reduction rules of the {\tt
2252 case}-construct are in \texttt{cases}. All theorems from {\tt
2253 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
2254 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
2255 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
2258 \subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}
2260 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
2261 +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
2262 but by more primitive means using \texttt{typedef}. To be able to use the
2263 tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by
2264 primitive recursion on these types, such types may be represented as actual
2265 datatypes. This is done by specifying an induction rule, as well as theorems
2266 stating the distinctness and injectivity of constructors in a {\tt
2267 rep_datatype} section. For type \texttt{nat} this works as follows:
2270 distinct Suc_not_Zero, Zero_not_Suc
2274 The datatype package automatically derives additional theorems for recursion
2275 and case combinators from these rules. Any of the basic HOL types mentioned
2276 above are represented as datatypes. Try an induction on \texttt{bool}
2280 \subsection{Examples}
2282 \subsubsection{The datatype $\alpha~mylist$}
2284 We want to define a type $\alpha~mylist$. To do this we have to build a new
2285 theory that contains the type definition. We start from the theory
2286 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
2287 \texttt{List} theory of Isabelle/HOL.
2290 datatype 'a mylist = Nil | Cons 'a ('a mylist)
2293 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To
2294 ease the induction applied below, we state the goal with $x$ quantified at the
2295 object-level. This will be stripped later using \ttindex{qed_spec_mp}.
2297 Goal "!x. Cons x xs ~= xs";
2299 {\out ! x. Cons x xs ~= xs}
2300 {\out 1. ! x. Cons x xs ~= xs}
2302 This can be proved by the structural induction tactic:
2304 by (induct_tac "xs" 1);
2306 {\out ! x. Cons x xs ~= xs}
2307 {\out 1. ! x. Cons x Nil ~= Nil}
2308 {\out 2. !!a mylist.}
2309 {\out ! x. Cons x mylist ~= mylist ==>}
2310 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
2312 The first subgoal can be proved using the simplifier. Isabelle/HOL has
2313 already added the freeness properties of lists to the default simplification
2318 {\out ! x. Cons x xs ~= xs}
2319 {\out 1. !!a mylist.}
2320 {\out ! x. Cons x mylist ~= mylist ==>}
2321 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
2323 Similarly, we prove the remaining goal.
2325 by (Asm_simp_tac 1);
2327 {\out ! x. Cons x xs ~= xs}
2330 qed_spec_mp "not_Cons_self";
2331 {\out val not_Cons_self = "Cons x xs ~= xs" : thm}
2333 Because both subgoals could have been proved by \texttt{Asm_simp_tac}
2334 we could have done that in one step:
2336 by (ALLGOALS Asm_simp_tac);
2340 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
2342 In this example we define the type $\alpha~mylist$ again but this time
2343 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix
2344 notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix
2345 annotations after the constructor declarations as follows:
2348 datatype 'a mylist =
2350 Cons 'a ('a mylist) (infixr "#" 70)
2353 Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
2356 \subsubsection{A datatype for weekdays}
2358 This example shows a datatype that consists of 7 constructors:
2361 datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
2364 Because there are more than 6 constructors, inequality is expressed via a function
2365 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
2366 contained among the distinctness theorems, but the simplifier can
2367 prove it thanks to rewrite rules inherited from theory \texttt{Arith}:
2372 You need not derive such inequalities explicitly: the simplifier will dispose
2373 of them automatically.
2377 \section{Recursive function definitions}\label{sec:HOL:recursive}
2378 \index{recursive functions|see{recursion}}
2380 Isabelle/HOL provides two main mechanisms of defining recursive functions.
2382 \item \textbf{Primitive recursion} is available only for datatypes, and it is
2383 somewhat restrictive. Recursive calls are only allowed on the argument's
2384 immediate constituents. On the other hand, it is the form of recursion most
2385 often wanted, and it is easy to use.
2387 \item \textbf{Well-founded recursion} requires that you supply a well-founded
2388 relation that governs the recursion. Recursive calls are only allowed if
2389 they make the argument decrease under the relation. Complicated recursion
2390 forms, such as nested recursion, can be dealt with. Termination can even be
2391 proved at a later time, though having unsolved termination conditions around
2392 can make work difficult.%
2393 \footnote{This facility is based on Konrad Slind's TFL
2394 package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
2395 and assisting with its installation.}
2398 Following good HOL tradition, these declarations do not assert arbitrary
2399 axioms. Instead, they define the function using a recursion operator. Both
2400 HOL and ZF derive the theory of well-founded recursion from first
2401 principles~\cite{paulson-set-II}. Primitive recursion over some datatype
2402 relies on the recursion operator provided by the datatype package. With
2403 either form of function definition, Isabelle proves the desired recursion
2404 equations as theorems.
2407 \subsection{Primitive recursive functions}
2408 \label{sec:HOL:primrec}
2409 \index{recursion!primitive|(}
2412 Datatypes come with a uniform way of defining functions, {\bf primitive
2413 recursion}. In principle, one could introduce primitive recursive functions
2414 by asserting their reduction rules as new axioms, but this is not recommended:
2415 \begin{ttbox}\slshape
2417 consts app :: ['a list, 'a list] => 'a list
2419 app_Nil "app [] ys = ys"
2420 app_Cons "app (x#xs) ys = x#app xs ys"
2423 Asserting axioms brings the danger of accidentally asserting nonsense, as
2424 in \verb$app [] ys = us$.
2426 The \ttindex{primrec} declaration is a safe means of defining primitive
2427 recursive functions on datatypes:
2430 consts app :: ['a list, 'a list] => 'a list
2433 "app (x#xs) ys = x#app xs ys"
2436 Isabelle will now check that the two rules do indeed form a primitive
2437 recursive definition. For example
2442 is rejected with an error message ``\texttt{Extra variables on rhs}''.
2446 The general form of a primitive recursive definition is
2449 {\it reduction rules}
2451 where \textit{reduction rules} specify one or more equations of the form
2452 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
2453 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
2454 contains only the free variables on the left-hand side, and all recursive
2455 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
2456 must be at most one reduction rule for each constructor. The order is
2457 immaterial. For missing constructors, the function is defined to return a
2460 If you would like to refer to some rule by name, then you must prefix
2461 the rule with an identifier. These identifiers, like those in the
2462 \texttt{rules} section of a theory, will be visible at the \ML\ level.
2464 The primitive recursive function can have infix or mixfix syntax:
2465 \begin{ttbox}\underscoreon
2466 consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
2469 "(x#xs) @ ys = x#(xs @ ys)"
2472 The reduction rules become part of the default simpset, which
2473 leads to short proof scripts:
2474 \begin{ttbox}\underscoreon
2475 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
2476 by (induct\_tac "xs" 1);
2477 by (ALLGOALS Asm\_simp\_tac);
2480 \subsubsection{Example: Evaluation of expressions}
2481 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
2482 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
2483 {\S}\ref{subsec:datatype:basics}:
2486 evala :: "['a => nat, 'a aexp] => nat"
2487 evalb :: "['a => nat, 'a bexp] => bool"
2490 "evala env (If_then_else b a1 a2) =
2491 (if evalb env b then evala env a1 else evala env a2)"
2492 "evala env (Sum a1 a2) = evala env a1 + evala env a2"
2493 "evala env (Diff a1 a2) = evala env a1 - evala env a2"
2494 "evala env (Var v) = env v"
2495 "evala env (Num n) = n"
2497 "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
2498 "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
2499 "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"
2501 Since the value of an expression depends on the value of its variables,
2502 the functions \texttt{evala} and \texttt{evalb} take an additional
2503 parameter, an {\em environment} of type \texttt{'a => nat}, which maps
2504 variables to their values.
2506 Similarly, we may define substitution functions \texttt{substa}
2507 and \texttt{substb} for expressions: The mapping \texttt{f} of type
2508 \texttt{'a => 'a aexp} given as a parameter is lifted canonically
2509 on the types \texttt{'a aexp} and \texttt{'a bexp}:
2512 substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"
2513 substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"
2516 "substa f (If_then_else b a1 a2) =
2517 If_then_else (substb f b) (substa f a1) (substa f a2)"
2518 "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
2519 "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
2520 "substa f (Var v) = f v"
2521 "substa f (Num n) = Num n"
2523 "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
2524 "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
2525 "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"
2527 In textbooks about semantics one often finds {\em substitution theorems},
2528 which express the relationship between substitution and evaluation. For
2529 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
2530 induction, followed by simplification:
2533 "evala env (substa (Var(v := a')) a) =
2534 evala (env(v := evala env a')) a &
2535 evalb env (substb (Var(v := a')) b) =
2536 evalb (env(v := evala env a')) b";
2537 by (induct_tac "a b" 1);
2538 by (ALLGOALS Asm_full_simp_tac);
2541 \subsubsection{Example: A substitution function for terms}
2542 Functions on datatypes with nested recursion, such as the type
2543 \texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
2544 also defined by mutual primitive recursion. A substitution
2545 function \texttt{subst_term} on type \texttt{term}, similar to the functions
2546 \texttt{substa} and \texttt{substb} described above, can
2547 be defined as follows:
2550 subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
2552 "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
2555 "subst_term f (Var a) = f a"
2556 "subst_term f (App b ts) = App b (subst_term_list f ts)"
2558 "subst_term_list f [] = []"
2559 "subst_term_list f (t # ts) =
2560 subst_term f t # subst_term_list f ts"
2562 The recursion scheme follows the structure of the unfolded definition of type
2563 \texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
2564 this substitution function, mutual induction is needed:
2567 "(subst_term ((subst_term f1) o f2) t) =
2568 (subst_term f1 (subst_term f2 t)) &
2569 (subst_term_list ((subst_term f1) o f2) ts) =
2570 (subst_term_list f1 (subst_term_list f2 ts))";
2571 by (induct_tac "t ts" 1);
2572 by (ALLGOALS Asm_full_simp_tac);
2575 \subsubsection{Example: A map function for infinitely branching trees}
2576 Defining functions on infinitely branching datatypes by primitive
2577 recursion is just as easy. For example, we can define a function
2578 \texttt{map_tree} on \texttt{'a tree} as follows:
2581 map_tree :: "('a => 'b) => 'a tree => 'b tree"
2584 "map_tree f (Atom a) = Atom (f a)"
2585 "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"
2587 Note that all occurrences of functions such as \texttt{ts} in the
2588 \texttt{primrec} clauses must be applied to an argument. In particular,
2589 \texttt{map_tree f o ts} is not allowed.
2591 \index{recursion!primitive|)}
2595 \subsection{General recursive functions}
2596 \label{sec:HOL:recdef}
2597 \index{recursion!general|(}
2600 Using \texttt{recdef}, you can declare functions involving nested recursion
2601 and pattern-matching. Recursion need not involve datatypes and there are few
2602 syntactic restrictions. Termination is proved by showing that each recursive
2603 call makes the argument smaller in a suitable sense, which you specify by
2604 supplying a well-founded relation.
2606 Here is a simple example, the Fibonacci function. The first line declares
2607 \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on
2608 the natural numbers). Pattern-matching is used here: \texttt{1} is a
2609 macro for \texttt{Suc~0}.
2611 consts fib :: "nat => nat"
2612 recdef fib "less_than"
2615 "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
2618 With \texttt{recdef}, function definitions may be incomplete, and patterns may
2619 overlap, as in functional programming. The \texttt{recdef} package
2620 disambiguates overlapping patterns by taking the order of rules into account.
2621 For missing patterns, the function is defined to return a default value.
2623 %For example, here is a declaration of the list function \cdx{hd}:
2625 %consts hd :: 'a list => 'a
2629 %Because this function is not recursive, we may supply the empty well-founded
2632 The well-founded relation defines a notion of ``smaller'' for the function's
2633 argument type. The relation $\prec$ is \textbf{well-founded} provided it
2634 admits no infinitely decreasing chains
2635 \[ \cdots\prec x@n\prec\cdots\prec x@1. \]
2636 If the function's argument has type~$\tau$, then $\prec$ has to be a relation
2637 over~$\tau$: it must have type $(\tau\times\tau)set$.
2639 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
2640 of operators for building well-founded relations. The package recognises
2641 these operators and automatically proves that the constructed relation is
2642 well-founded. Here are those operators, in order of importance:
2644 \item \texttt{less_than} is ``less than'' on the natural numbers.
2645 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.
2647 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
2648 relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$.
2649 Typically, $f$ takes the recursive function's arguments (as a tuple) and
2650 returns a result expressed in terms of the function \texttt{size}. It is
2651 called a \textbf{measure function}. Recall that \texttt{size} is overloaded
2652 and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
2654 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
2655 \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$
2656 is less than $f(y)$ according to~$R$, which must itself be a well-founded
2659 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It
2660 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$
2661 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$
2662 is less than $y@2$ according to~$R@2$.
2664 \item \texttt{finite_psubset} is the proper subset relation on finite sets.
2667 We can use \texttt{measure} to declare Euclid's algorithm for the greatest
2668 common divisor. The measure function, $\lambda(m,n). n$, specifies that the
2669 recursion terminates because argument~$n$ decreases.
2671 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
2672 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2675 The general form of a well-founded recursive definition is
2677 recdef {\it function} {\it rel}
2678 congs {\it congruence rules} {\bf(optional)}
2679 simpset {\it simplification set} {\bf(optional)}
2680 {\it reduction rules}
2684 \item \textit{function} is the name of the function, either as an \textit{id}
2685 or a \textit{string}.
2687 \item \textit{rel} is a {\HOL} expression for the well-founded termination
2690 \item \textit{congruence rules} are required only in highly exceptional
2693 \item The \textit{simplification set} is used to prove that the supplied
2694 relation is well-founded. It is also used to prove the \textbf{termination
2695 conditions}: assertions that arguments of recursive calls decrease under
2696 \textit{rel}. By default, simplification uses \texttt{simpset()}, which
2697 is sufficient to prove well-foundedness for the built-in relations listed
2700 \item \textit{reduction rules} specify one or more recursion equations. Each
2701 left-hand side must have the form $f\,t$, where $f$ is the function and $t$
2702 is a tuple of distinct variables. If more than one equation is present then
2703 $f$ is defined by pattern-matching on components of its argument whose type
2704 is a \texttt{datatype}.
2706 The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as
2710 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
2711 prove one termination condition. It remains as a precondition of the
2715 {\out ["! m n. n ~= 0 --> m mod n < n}
2716 {\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] }
2719 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
2720 conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard
2721 function \texttt{goalw}, which sets up a goal to prove, but its argument
2722 should be the identifier $f$\texttt{.simps} and its effect is to set up a
2723 proof of the termination conditions:
2725 Tfl.tgoalw thy [] gcd.simps;
2727 {\out ! m n. n ~= 0 --> m mod n < n}
2728 {\out 1. ! m n. n ~= 0 --> m mod n < n}
2730 This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem
2731 is proved, it can be used to eliminate the termination conditions from
2732 elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much
2733 more complicated example of this process, where the termination conditions can
2734 only be proved by complicated reasoning involving the recursive function
2737 Isabelle/HOL can prove the \texttt{gcd} function's termination condition
2738 automatically if supplied with the right simpset.
2740 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
2741 simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"
2742 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2745 If all termination conditions were proved automatically, $f$\texttt{.simps}
2746 is added to the simpset automatically, just as in \texttt{primrec}.
2747 The simplification rules corresponding to clause $i$ (where counting starts
2748 at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms
2750 which returns a list of theorems. Thus you can, for example, remove specific
2751 clauses from the simpset. Note that a single clause may give rise to a set of
2752 simplification rules in order to capture the fact that if clauses overlap,
2753 their order disambiguates them.
2755 A \texttt{recdef} definition also returns an induction rule specialised for
2756 the recursive function. For the \texttt{gcd} function above, the induction
2760 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}
2762 This rule should be used to reason inductively about the \texttt{gcd}
2763 function. It usually makes the induction hypothesis available at all
2764 recursive calls, leading to very direct proofs. If any termination conditions
2765 remain unproved, they will become additional premises of this rule.
2767 \index{recursion!general|)}
2771 \section{Inductive and coinductive definitions}
2772 \index{*inductive|(}
2773 \index{*coinductive|(}
2775 An {\bf inductive definition} specifies the least set~$R$ closed under given
2776 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
2777 example, a structural operational semantics is an inductive definition of an
2778 evaluation relation. Dually, a {\bf coinductive definition} specifies the
2779 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
2780 seen as arising by applying a rule to elements of~$R$.) An important example
2781 is using bisimulation relations to formalise equivalence of processes and
2782 infinite data structures.
2784 A theory file may contain any number of inductive and coinductive
2785 definitions. They may be intermixed with other declarations; in
2786 particular, the (co)inductive sets {\bf must} be declared separately as
2787 constants, and may have mixfix syntax or be subject to syntax translations.
2789 Each (co)inductive definition adds definitions to the theory and also
2790 proves some theorems. Each definition creates an \ML\ structure, which is a
2791 substructure of the main theory structure.
2793 This package is related to the \ZF\ one, described in a separate
2795 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
2796 distributed with Isabelle.} %
2797 which you should refer to in case of difficulties. The package is simpler
2798 than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types
2799 of the (co)inductive sets determine the domain of the fixedpoint definition,
2800 and the package does not have to use inference rules for type-checking.
2803 \subsection{The result structure}
2804 Many of the result structure's components have been discussed in the paper;
2805 others are self-explanatory.
2807 \item[\tt defs] is the list of definitions of the recursive sets.
2809 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
2811 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
2812 the recursive sets, in the case of mutual recursion).
2814 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
2815 the recursive sets. The rules are also available individually, using the
2816 names given them in the theory file.
2818 \item[\tt elims] is the list of elimination rule.
2820 \item[\tt elim] is the head of the list \texttt{elims}.
2822 \item[\tt mk_cases] is a function to create simplified instances of {\tt
2823 elim} using freeness reasoning on underlying datatypes.
2826 For an inductive definition, the result structure contains the
2827 rule \texttt{induct}. For a
2828 coinductive definition, it contains the rule \verb|coinduct|.
2830 Figure~\ref{def-result-fig} summarises the two result signatures,
2831 specifying the types of all these components.
2839 val intrs : thm list
2840 val elims : thm list
2842 val mk_cases : string -> thm
2843 {\it(Inductive definitions only)}
2845 {\it(coinductive definitions only)}
2850 \caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
2853 \subsection{The syntax of a (co)inductive definition}
2854 An inductive definition has the form
2856 inductive {\it inductive sets}
2857 intrs {\it introduction rules}
2858 monos {\it monotonicity theorems}
2859 con_defs {\it constructor definitions}
2861 A coinductive definition is identical, except that it starts with the keyword
2862 \texttt{coinductive}.
2864 The \texttt{monos} and \texttt{con_defs} sections are optional. If present,
2865 each is specified by a list of identifiers.
2868 \item The \textit{inductive sets} are specified by one or more strings.
2870 \item The \textit{introduction rules} specify one or more introduction rules in
2871 the form \textit{ident\/}~\textit{string}, where the identifier gives the name of
2872 the rule in the result structure.
2874 \item The \textit{monotonicity theorems} are required for each operator
2875 applied to a recursive set in the introduction rules. There {\bf must}
2876 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
2877 premise $t\in M(R@i)$ in an introduction rule!
2879 \item The \textit{constructor definitions} contain definitions of constants
2880 appearing in the introduction rules. In most cases it can be omitted.
2884 \subsection{*Monotonicity theorems}
2886 Each theory contains a default set of theorems that are used in monotonicity
2887 proofs. New rules can be added to this set via the \texttt{mono} attribute.
2888 Theory \texttt{Inductive} shows how this is done. In general, the following
2889 monotonicity theorems may be added:
2891 \item Theorems of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for proving
2892 monotonicity of inductive definitions whose introduction rules have premises
2893 involving terms such as $t\in M(R@i)$.
2894 \item Monotonicity theorems for logical operators, which are of the general form
2895 $\List{\cdots \rightarrow \cdots;~\ldots;~\cdots \rightarrow \cdots} \Imp
2896 \cdots \rightarrow \cdots$.
2897 For example, in the case of the operator $\vee$, the corresponding theorem is
2899 \infer{P@1 \vee P@2 \rightarrow Q@1 \vee Q@2}
2900 {P@1 \rightarrow Q@1 & P@2 \rightarrow Q@2}
2902 \item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g.
2904 (\neg \neg P) ~=~ P \qquad\qquad
2905 (\neg (P \wedge Q)) ~=~ (\neg P \vee \neg Q)
2907 \item Equations for reducing complex operators to more primitive ones whose
2908 monotonicity can easily be proved, e.g.
2910 (P \rightarrow Q) ~=~ (\neg P \vee Q) \qquad\qquad
2911 \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \rightarrow P~x
2915 \subsection{Example of an inductive definition}
2916 Two declarations, included in a theory file, define the finite powerset
2917 operator. First we declare the constant~\texttt{Fin}. Then we declare it
2918 inductively, with two introduction rules:
2920 consts Fin :: 'a set => 'a set set
2923 emptyI "{\ttlbrace}{\ttrbrace} : Fin A"
2924 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
2926 The resulting theory structure contains a substructure, called~\texttt{Fin}.
2927 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
2928 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
2929 rule is \texttt{Fin.induct}.
2931 For another example, here is a theory file defining the accessible
2932 part of a relation. The paper
2933 \cite{paulson-CADE} discusses a \ZF\ version of this example in more
2936 Acc = WF + Inductive +
2938 consts acc :: "('a * 'a)set => 'a set" (* accessible part *)
2942 accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
2946 The Isabelle distribution contains many other inductive definitions. Simple
2947 examples are collected on subdirectory \texttt{HOL/Induct}. The theory
2948 \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples
2949 may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},
2950 \texttt{Lambda} and \texttt{Auth}.
2952 \index{*coinductive|)} \index{*inductive|)}
2955 \section{The examples directories}
2957 Directory \texttt{HOL/Auth} contains theories for proving the correctness of
2958 cryptographic protocols~\cite{paulson-jcs}. The approach is based upon
2959 operational semantics rather than the more usual belief logics. On the same
2960 directory are proofs for some standard examples, such as the Needham-Schroeder
2961 public-key authentication protocol and the Otway-Rees
2964 Directory \texttt{HOL/IMP} contains a formalization of various denotational,
2965 operational and axiomatic semantics of a simple while-language, the necessary
2966 equivalence proofs, soundness and completeness of the Hoare rules with
2967 respect to the denotational semantics, and soundness and completeness of a
2968 verification condition generator. Much of development is taken from
2969 Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
2971 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
2972 logic, including a tactic for generating verification-conditions.
2974 Directory \texttt{HOL/MiniML} contains a formalization of the type system of
2975 the core functional language Mini-ML and a correctness proof for its type
2976 inference algorithm $\cal W$~\cite{milner78,nipkow-W}.
2978 Directory \texttt{HOL/Lambda} contains a formalization of untyped
2979 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
2980 and $\eta$ reduction~\cite{Nipkow-CR}.
2982 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of
2983 substitutions and unifiers. It is based on Paulson's previous
2984 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
2985 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef},
2986 with nested recursion.
2988 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive
2989 definitions and datatypes.
2991 \item Theory \texttt{PropLog} proves the soundness and completeness of
2992 classical propositional logic, given a truth table semantics. The only
2993 connective is $\imp$. A Hilbert-style axiom system is specified, and its
2994 set of theorems defined inductively. A similar proof in \ZF{} is
2995 described elsewhere~\cite{paulson-set-II}.
2997 \item Theory \texttt{Term} defines the datatype \texttt{term}.
2999 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions
3000 as mutually recursive datatypes.
3002 \item The definition of lazy lists demonstrates methods for handling
3003 infinite data structures and coinduction in higher-order
3004 logic~\cite{paulson-coind}.%
3005 \footnote{To be precise, these lists are \emph{potentially infinite} rather
3006 than lazy. Lazy implies a particular operational semantics.}
3007 Theory \thydx{LList} defines an operator for
3008 corecursion on lazy lists, which is used to define a few simple functions
3009 such as map and append. A coinduction principle is defined
3010 for proving equations on lazy lists.
3012 \item Theory \thydx{LFilter} defines the filter functional for lazy lists.
3013 This functional is notoriously difficult to define because finding the next
3014 element meeting the predicate requires possibly unlimited search. It is not
3015 computable, but can be expressed using a combination of induction and
3018 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions
3019 to express a programming language semantics that appears to require mutual
3020 induction. Iterated induction allows greater modularity.
3023 Directory \texttt{HOL/ex} contains other examples and experimental proofs in
3026 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
3027 to define recursive functions. Another example is \texttt{Fib}, which
3028 defines the Fibonacci function.
3030 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two
3031 natural numbers and proves a key lemma of the Fundamental Theorem of
3032 Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$
3035 \item Theory \texttt{Primrec} develops some computation theory. It
3036 inductively defines the set of primitive recursive functions and presents a
3037 proof that Ackermann's function is not primitive recursive.
3039 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty
3040 predicate calculus theorems, ranging from simple tautologies to
3041 moderately difficult problems involving equality and quantifiers.
3043 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc
3044 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
3045 much more powerful than Isabelle's classical reasoner. But it is less
3046 useful in practice because it works only for pure logic; it does not
3047 accept derived rules for the set theory primitives, for example.
3049 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof
3050 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
3052 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
3053 {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem.
3055 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
3056 Milner and Tofte's coinduction example~\cite{milner-coind}. This
3057 substantial proof concerns the soundness of a type system for a simple
3058 functional language. The semantics of recursion is given by a cyclic
3059 environment, which makes a coinductive argument appropriate.
3064 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
3065 Cantor's Theorem states that every set has more subsets than it has
3066 elements. It has become a favourite example in higher-order logic since
3067 it is so easily expressed:
3068 \[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.
3069 \forall x::\alpha. f~x \not= S
3072 Viewing types as sets, $\alpha\To bool$ represents the powerset
3073 of~$\alpha$. This version states that for every function from $\alpha$ to
3074 its powerset, some subset is outside its range.
3076 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
3077 the operator \cdx{range}.
3081 The set~$S$ is given as an unknown instead of a
3082 quantified variable so that we may inspect the subset found by the proof.
3084 Goal "?S ~: range\thinspace(f :: 'a=>'a set)";
3086 {\out ?S ~: range f}
3087 {\out 1. ?S ~: range f}
3089 The first two steps are routine. The rule \tdx{rangeE} replaces
3090 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.
3092 by (resolve_tac [notI] 1);
3094 {\out ?S ~: range f}
3095 {\out 1. ?S : range f ==> False}
3097 by (eresolve_tac [rangeE] 1);
3099 {\out ?S ~: range f}
3100 {\out 1. !!x. ?S = f x ==> False}
3102 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,
3103 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for
3106 by (eresolve_tac [equalityCE] 1);
3108 {\out ?S ~: range f}
3109 {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}
3110 {\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}
3112 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
3113 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies
3114 $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD}
3115 instantiates~$\Var{S}$ and creates the new assumption.
3117 by (dresolve_tac [CollectD] 1);
3119 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}
3120 {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}
3121 {\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}
3123 Forcing a contradiction between the two assumptions of subgoal~1
3124 completes the instantiation of~$S$. It is now the set $\{x. x\not\in
3125 f~x\}$, which is the standard diagonal construction.
3129 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3130 {\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}
3132 The rest should be easy. To apply \tdx{CollectI} to the negated
3133 assumption, we employ \ttindex{swap_res_tac}:
3135 by (swap_res_tac [CollectI] 1);
3137 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3138 {\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}
3142 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3145 How much creativity is required? As it happens, Isabelle can prove this
3146 theorem automatically. The default classical set \texttt{claset()} contains rules
3147 for most of the constructs of \HOL's set theory. We must augment it with
3148 \tdx{equalityCE} to break up set equalities, and then apply best-first
3149 search. Depth-first search would diverge, but best-first search
3150 successfully navigates through the large search space.
3151 \index{search!best-first}
3155 {\out ?S ~: range f}
3156 {\out 1. ?S ~: range f}
3158 by (best_tac (claset() addSEs [equalityCE]) 1);
3160 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3163 If you run this example interactively, make sure your current theory contains
3164 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
3165 Otherwise the default claset may not contain the rules for set theory.
3166 \index{higher-order logic|)}
3168 %%% Local Variables:
3170 %%% TeX-master: "logics"