Documented usage of function types in datatype specifications.
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'\^etre\/}. 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 ($\neg$) \\
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 \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
63 Hilbert description ($\varepsilon$) \\
64 {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ &
65 universal quantifier ($\forall$) \\
66 {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
67 existential quantifier ($\exists$) \\
68 {\tt?!} or \texttt{EX!} & \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 & | & "\at~" id " . " formula \\
104 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
106 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
107 & | & "LEAST"~ id " . " formula \\[2ex]
108 formula & = & \hbox{expression of type~$bool$} \\
109 & | & term " = " term \\
110 & | & term " \ttilde= " term \\
111 & | & term " < " term \\
112 & | & term " <= " term \\
113 & | & "\ttilde\ " formula \\
114 & | & formula " \& " formula \\
115 & | & formula " | " formula \\
116 & | & formula " --> " formula \\
117 & | & "!~~~" id~id^* " . " formula
118 & | & "ALL~" id~id^* " . " formula \\
119 & | & "?~~~" id~id^* " . " formula
120 & | & "EX~~" id~id^* " . " formula \\
121 & | & "?!~~" id~id^* " . " formula
122 & | & "EX!~" id~id^* " . " formula
125 \caption{Full grammar for \HOL} \label{hol-grammar}
131 Figure~\ref{hol-constants} lists the constants (including infixes and
132 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
133 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
137 \HOL\ has no if-and-only-if connective; logical equivalence is expressed
138 using equality. But equality has a high priority, as befitting a
139 relation, while if-and-only-if typically has the lowest priority. Thus,
140 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
141 When using $=$ to mean logical equivalence, enclose both operands in
145 \subsection{Types and classes}
146 The universal type class of higher-order terms is called~\cldx{term}.
147 By default, explicit type variables have class \cldx{term}. In
148 particular the equality symbol and quantifiers are polymorphic over
151 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
152 formulae are terms. The built-in type~\tydx{fun}, which constructs
153 function types, is overloaded with arity {\tt(term,\thinspace
154 term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
155 term} if $\sigma$ and~$\tau$ do, allowing quantification over
158 \HOL\ offers various methods for introducing new types.
159 See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
161 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
162 signatures; the relations $<$ and $\leq$ are polymorphic over this
163 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
164 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
165 \cldx{order} of \cldx{ord} which axiomatizes partially ordered types
168 Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
169 \cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
170 symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In
171 particular, {\tt-} is instantiated for set difference and subtraction
174 If you state a goal containing overloaded functions, you may need to include
175 type constraints. Type inference may otherwise make the goal more
176 polymorphic than you intended, with confusing results. For example, the
177 variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type
178 $\alpha::\{ord,plus\}$, although you may have expected them to have some
179 numeric type, e.g. $nat$. Instead you should have stated the goal as
180 $(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have
184 If resolution fails for no obvious reason, try setting
185 \ttindex{show_types} to \texttt{true}, causing Isabelle to display
186 types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as
187 well, causing Isabelle to display type classes and sorts.
189 \index{unification!incompleteness of}
190 Where function types are involved, Isabelle's unification code does not
191 guarantee to find instantiations for type variables automatically. Be
192 prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
193 possibly instantiating type variables. Setting
194 \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
195 omitted search paths during unification.\index{tracing!of unification}
201 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
202 some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\
203 denote something, a description is always meaningful, but we do not
204 know its value unless $P$ defines it uniquely. We may write
205 descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
206 \hbox{\tt \at $x$.\ $P[x]$}.
208 Existential quantification is defined by
209 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
210 The unique existence quantifier, $\exists!x. P$, is defined in terms
211 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
212 quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates
213 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
214 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
216 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
217 Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
218 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
219 existential quantifier must be followed by a space; thus {\tt?x} is an
220 unknown, while \verb'? x. f x=y' is a quantification. Isabelle's usual
221 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
222 available. Both notations are accepted for input. The {\ML} reference
223 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
224 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
225 to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed.
227 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
228 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
229 to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
230 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
231 choice operator, so \texttt{Least} is always meaningful, but may yield
232 nothing useful in case there is not a unique least element satisfying
233 $P$.\footnote{Class $ord$ does not require much of its instances, so
234 $\le$ need not be a well-ordering, not even an order at all!}
236 \medskip All these binders have priority 10.
239 The low priority of binders means that they need to be enclosed in
240 parenthesis when they occur in the context of other operations. For example,
241 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
245 \subsection{The let and case constructions}
246 Local abbreviations can be introduced by a \texttt{let} construct whose
247 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
248 the constant~\cdx{Let}. It can be expanded by rewriting with its
249 definition, \tdx{Let_def}.
251 \HOL\ also defines the basic syntax
252 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
253 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
254 and \sdx{of} are reserved words. Initially, this is mere syntax and has no
255 logical meaning. By declaring translations, you can cause instances of the
256 \texttt{case} construct to denote applications of particular case operators.
257 This is what happens automatically for each \texttt{datatype} definition
258 (see~\S\ref{sec:HOL:datatype}).
261 Both \texttt{if} and \texttt{case} constructs have as low a priority as
262 quantifiers, which requires additional enclosing parentheses in the context
263 of most other operations. For example, instead of $f~x = {\tt if\dots
264 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
268 \section{Rules of inference}
271 \begin{ttbox}\makeatother
272 \tdx{refl} t = (t::'a)
273 \tdx{subst} [| s = t; P s |] ==> P (t::'a)
274 \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)
275 \tdx{impI} (P ==> Q) ==> P-->Q
276 \tdx{mp} [| P-->Q; P |] ==> Q
277 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
278 \tdx{selectI} P(x::'a) ==> P(@x. P x)
279 \tdx{True_or_False} (P=True) | (P=False)
281 \caption{The \texttt{HOL} rules} \label{hol-rules}
284 Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
285 with their~{\ML} names. Some of the rules deserve additional
287 \begin{ttdescription}
288 \item[\tdx{ext}] expresses extensionality of functions.
289 \item[\tdx{iff}] asserts that logically equivalent formulae are
291 \item[\tdx{selectI}] gives the defining property of the Hilbert
292 $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule
293 \tdx{select_equality} (see below) is often easier to use.
294 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
295 fact, the $\varepsilon$-operator already makes the logic classical, as
296 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
300 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
301 \begin{ttbox}\makeatother
302 \tdx{True_def} True == ((\%x::bool. x)=(\%x. x))
303 \tdx{All_def} All == (\%P. P = (\%x. True))
304 \tdx{Ex_def} Ex == (\%P. P(@x. P x))
305 \tdx{False_def} False == (!P. P)
306 \tdx{not_def} not == (\%P. P-->False)
307 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
308 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
309 \tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
311 \tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
312 \tdx{if_def} If P x y ==
313 (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
314 \tdx{Let_def} Let s f == f s
315 \tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
317 \caption{The \texttt{HOL} definitions} \label{hol-defs}
321 \HOL{} follows standard practice in higher-order logic: only a few
322 connectives are taken as primitive, with the remainder defined obscurely
323 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
324 corresponding definitions \cite[page~270]{mgordon-hol} using
325 object-equality~({\tt=}), which is possible because equality in
326 higher-order logic may equate formulae and even functions over formulae.
327 But theory~\HOL{}, like all other Isabelle theories, uses
328 meta-equality~({\tt==}) for definitions.
330 The definitions above should never be expanded and are shown for completeness
331 only. Instead users should reason in terms of the derived rules shown below
332 or, better still, using high-level tactics
333 (see~\S\ref{sec:HOL:generic-packages}).
336 Some of the rules mention type variables; for example, \texttt{refl}
337 mentions the type variable~{\tt'a}. This allows you to instantiate
338 type variables explicitly by calling \texttt{res_inst_tac}.
343 \tdx{sym} s=t ==> t=s
344 \tdx{trans} [| r=s; s=t |] ==> r=t
345 \tdx{ssubst} [| t=s; P s |] ==> P t
346 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
347 \tdx{arg_cong} x = y ==> f x = f y
348 \tdx{fun_cong} f = g ==> f x = g x
349 \tdx{cong} [| f = g; x = y |] ==> f x = g y
350 \tdx{not_sym} t ~= s ==> s ~= t
351 \subcaption{Equality}
354 \tdx{FalseE} False ==> P
356 \tdx{conjI} [| P; Q |] ==> P&Q
357 \tdx{conjunct1} [| P&Q |] ==> P
358 \tdx{conjunct2} [| P&Q |] ==> Q
359 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
361 \tdx{disjI1} P ==> P|Q
362 \tdx{disjI2} Q ==> P|Q
363 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
365 \tdx{notI} (P ==> False) ==> ~ P
366 \tdx{notE} [| ~ P; P |] ==> R
367 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
368 \subcaption{Propositional logic}
370 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
371 \tdx{iffD1} [| P=Q; P |] ==> Q
372 \tdx{iffD2} [| P=Q; Q |] ==> P
373 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
375 %\tdx{eqTrueI} P ==> P=True
376 %\tdx{eqTrueE} P=True ==> P
377 \subcaption{Logical equivalence}
380 \caption{Derived rules for \HOL} \label{hol-lemmas1}
385 \begin{ttbox}\makeatother
386 \tdx{allI} (!!x. P x) ==> !x. P x
387 \tdx{spec} !x. P x ==> P x
388 \tdx{allE} [| !x. P x; P x ==> R |] ==> R
389 \tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R
391 \tdx{exI} P x ==> ? x. P x
392 \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q
394 \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
395 \tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
398 \tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a
399 \subcaption{Quantifiers and descriptions}
401 \tdx{ccontr} (~P ==> False) ==> P
402 \tdx{classical} (~P ==> P) ==> P
403 \tdx{excluded_middle} ~P | P
405 \tdx{disjCI} (~Q ==> P) ==> P|Q
406 \tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x
407 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
408 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
409 \tdx{notnotD} ~~P ==> P
410 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
411 \subcaption{Classical logic}
413 %\tdx{if_True} (if True then x else y) = x
414 %\tdx{if_False} (if False then x else y) = y
415 \tdx{if_P} P ==> (if P then x else y) = x
416 \tdx{if_not_P} ~ P ==> (if P then x else y) = y
417 \tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
418 \subcaption{Conditionals}
420 \caption{More derived rules} \label{hol-lemmas2}
423 Some derived rules are shown in Figures~\ref{hol-lemmas1}
424 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
425 for the logical connectives, as well as sequent-style elimination rules for
426 conjunctions, implications, and universal quantifiers.
428 Note the equality rules: \tdx{ssubst} performs substitution in
429 backward proofs, while \tdx{box_equals} supports reasoning by
430 simplifying both sides of an equation.
432 The following simple tactics are occasionally useful:
433 \begin{ttdescription}
434 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
435 repeatedly to remove all outermost universal quantifiers and implications
437 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction
438 on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
439 with the added assumptions $P$ and $\neg P$, respectively.
446 \it name &\it meta-type & \it description \\
447 \index{{}@\verb'{}' symbol}
448 \verb|{}| & $\alpha\,set$ & the empty set \\
449 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
450 & insertion of element \\
451 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
453 \cdx{Compl} & $\alpha\,set\To\alpha\,set$
455 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
456 & intersection over a set\\
457 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
459 \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
460 &set of sets intersection \\
461 \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
462 &set of sets union \\
463 \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
465 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
466 & range of a function \\[1ex]
467 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
468 & bounded quantifiers
471 \subcaption{Constants}
474 \begin{tabular}{llrrr}
475 \it symbol &\it name &\it meta-type & \it priority & \it description \\
476 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
477 intersection over a type\\
478 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
488 \begin{tabular}{rrrr}
489 \it symbol & \it meta-type & \it priority & \it description \\
490 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$
492 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
493 & Left 70 & intersection ($\int$) \\
494 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
495 & Left 65 & union ($\un$) \\
496 \tt: & $[\alpha ,\alpha\,set]\To bool$
497 & Left 50 & membership ($\in$) \\
498 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
499 & Left 50 & subset ($\subseteq$)
503 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
508 \begin{center} \tt\frenchspacing
511 \it external & \it internal & \it description \\
512 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
513 {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
514 {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &
516 \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &
518 \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
520 \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ &
521 Ball $A$ $\lambda x. P[x]$ &
522 \rm bounded $\forall$ \\
523 \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ &
524 Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$
527 \subcaption{Translations}
530 \[\begin{array}{rclcl}
531 term & = & \hbox{other terms\ldots} \\
532 & | & "{\ttlbrace}{\ttrbrace}" \\
533 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
534 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
535 & | & term " `` " term \\
536 & | & term " Int " term \\
537 & | & term " Un " term \\
538 & | & "INT~~" id ":" term " . " term \\
539 & | & "UN~~~" id ":" term " . " term \\
540 & | & "INT~~" id~id^* " . " term \\
541 & | & "UN~~~" id~id^* " . " term \\[2ex]
542 formula & = & \hbox{other formulae\ldots} \\
543 & | & term " : " term \\
544 & | & term " \ttilde: " term \\
545 & | & term " <= " term \\
546 & | & "!~" id ":" term " . " formula
547 & | & "ALL " id ":" term " . " formula \\
548 & | & "?~" id ":" term " . " formula
549 & | & "EX~~" id ":" term " . " formula
552 \subcaption{Full Grammar}
553 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
557 \section{A formulation of set theory}
558 Historically, higher-order logic gives a foundation for Russell and
559 Whitehead's theory of classes. Let us use modern terminology and call them
560 {\bf sets}, but note that these sets are distinct from those of {\ZF} set
561 theory, and behave more like {\ZF} classes.
564 Sets are given by predicates over some type~$\sigma$. Types serve to
565 define universes for sets, but type-checking is still significant.
567 There is a universal set (for each type). Thus, sets have complements, and
568 may be defined by absolute comprehension.
570 Although sets may contain other sets as elements, the containing set must
571 have a more complex type.
573 Finite unions and intersections have the same behaviour in \HOL\ as they
574 do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
575 denoting the universal set for the given type.
577 \subsection{Syntax of set theory}\index{*set type}
578 \HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
579 essentially the same as $\alpha\To bool$. The new type is defined for
580 clarity and to avoid complications involving function types in unification.
581 The isomorphisms between the two types are declared explicitly. They are
582 very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
583 \hbox{\tt op :} maps in the other direction (ignoring argument order).
585 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
586 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
587 constructs. Infix operators include union and intersection ($A\un B$
588 and $A\int B$), the subset and membership relations, and the image
589 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
592 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
593 the obvious manner using~\texttt{insert} and~$\{\}$:
595 \{a, b, c\} & \equiv &
596 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
599 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
600 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
601 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
602 x. P[x])$. It defines sets by absolute comprehension, which is impossible
603 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
605 The set theory defines two {\bf bounded quantifiers}:
607 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
608 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
610 The constants~\cdx{Ball} and~\cdx{Bex} are defined
611 accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
612 write\index{*"! symbol}\index{*"? symbol}
613 \index{*ALL symbol}\index{*EX symbol}
615 \hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's
616 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
617 for input. As with the primitive quantifiers, the {\ML} reference
618 \ttindex{HOL_quantifiers} specifies which notation to use for output.
620 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
621 $\bigcap@{x\in A}B[x]$, are written
622 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
623 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.
625 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
626 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
627 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous
628 union and intersection operators when $A$ is the universal set.
630 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
631 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
636 \begin{figure} \underscoreon
638 \tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a
639 \tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A
641 \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}
642 \tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B
643 \tdx{Ball_def} Ball A P == ! x. x:A --> P x
644 \tdx{Bex_def} Bex A P == ? x. x:A & P x
645 \tdx{subset_def} A <= B == ! x:A. x:B
646 \tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}
647 \tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}
648 \tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}
649 \tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace}
650 \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
651 \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
652 \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B
653 \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B
654 \tdx{Inter_def} Inter S == (INT x:S. x)
655 \tdx{Union_def} Union S == (UN x:S. x)
656 \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
657 \tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
658 \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
660 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
664 \begin{figure} \underscoreon
666 \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}
667 \tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a
668 \tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W
670 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
671 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
672 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
674 \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
675 \tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x
676 \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
677 \subcaption{Comprehension and Bounded quantifiers}
679 \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B
680 \tdx{subsetD} [| A <= B; c:A |] ==> c:B
681 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
683 \tdx{subset_refl} A <= A
684 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
686 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B
687 \tdx{equalityD1} A = B ==> A<=B
688 \tdx{equalityD2} A = B ==> B<=A
689 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
691 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
692 [| ~ c:A; ~ c:B |] ==> P
694 \subcaption{The subset and equality relations}
696 \caption{Derived rules for set theory} \label{hol-set1}
700 \begin{figure} \underscoreon
702 \tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
704 \tdx{insertI1} a : insert a B
705 \tdx{insertI2} a : B ==> a : insert b B
706 \tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
708 \tdx{ComplI} [| c:A ==> False |] ==> c : Compl A
709 \tdx{ComplD} [| c : Compl A |] ==> ~ c:A
711 \tdx{UnI1} c:A ==> c : A Un B
712 \tdx{UnI2} c:B ==> c : A Un B
713 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
714 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
716 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B
717 \tdx{IntD1} c : A Int B ==> c:A
718 \tdx{IntD2} c : A Int B ==> c:B
719 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
721 \tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
722 \tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
724 \tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
725 \tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
726 \tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
728 \tdx{UnionI} [| X:C; A:X |] ==> A : Union C
729 \tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
731 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
732 \tdx{InterD} [| A : Inter C; X:C |] ==> A:X
733 \tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
735 \tdx{PowI} A<=B ==> A: Pow B
736 \tdx{PowD} A: Pow B ==> A<=B
738 \tdx{imageI} [| x:A |] ==> f x : f``A
739 \tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
741 \tdx{rangeI} f x : range f
742 \tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
744 \caption{Further derived rules for set theory} \label{hol-set2}
748 \subsection{Axioms and rules of set theory}
749 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
750 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
751 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of
752 course, \hbox{\tt op :} also serves as the membership relation.
754 All the other axioms are definitions. They include the empty set, bounded
755 quantifiers, unions, intersections, complements and the subset relation.
756 They also include straightforward constructions on functions: image~({\tt``})
759 %The predicate \cdx{inj_on} is used for simulating type definitions.
760 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
761 %set~$A$, which specifies a subset of its domain type. In a type
762 %definition, $f$ is the abstraction function and $A$ is the set of valid
763 %representations; we should not expect $f$ to be injective outside of~$A$.
765 %\begin{figure} \underscoreon
767 %\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
768 %\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
771 % [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
774 %\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
775 %\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
777 %\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
778 %\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
779 %\tdx{injD} [| inj f; f x = f y |] ==> x=y
781 %\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
782 %\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
784 %\tdx{inj_on_inverseI}
785 % (!!x. x:A ==> g(f x) = x) ==> inj_on f A
786 %\tdx{inj_on_contraD}
787 % [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
789 %\caption{Derived rules involving functions} \label{hol-fun}
793 \begin{figure} \underscoreon
795 \tdx{Union_upper} B:A ==> B <= Union A
796 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
798 \tdx{Inter_lower} B:A ==> Inter A <= B
799 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
801 \tdx{Un_upper1} A <= A Un B
802 \tdx{Un_upper2} B <= A Un B
803 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
805 \tdx{Int_lower1} A Int B <= A
806 \tdx{Int_lower2} A Int B <= B
807 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
809 \caption{Derived rules involving subsets} \label{hol-subset}
813 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
815 \tdx{Int_absorb} A Int A = A
816 \tdx{Int_commute} A Int B = B Int A
817 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
818 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
820 \tdx{Un_absorb} A Un A = A
821 \tdx{Un_commute} A Un B = B Un A
822 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
823 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
825 \tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace}
826 \tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x. True{\ttrbrace}
827 \tdx{double_complement} Compl(Compl A) = A
828 \tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B)
829 \tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B)
831 \tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
832 \tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
833 \tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
835 \tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
836 \tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
837 \tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
839 \caption{Set equalities} \label{hol-equalities}
843 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
844 obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
845 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
846 are designed for classical reasoning; the rules \tdx{subsetD},
847 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
848 strictly necessary but yield more natural proofs. Similarly,
849 \tdx{equalityCE} supports classical reasoning about extensionality,
850 after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for
851 proofs pertaining to set theory.
853 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
854 Unions form least upper bounds; non-empty intersections form greatest lower
855 bounds. Reasoning directly about subsets often yields clearer proofs than
856 reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.
858 Figure~\ref{hol-equalities} presents many common set equalities. They
859 include commutative, associative and distributive laws involving unions,
860 intersections and complements. For a complete listing see the file {\tt
864 \texttt{Blast_tac} proves many set-theoretic theorems automatically.
865 Hence you seldom need to refer to the theorems above.
871 \it name &\it meta-type & \it description \\
872 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
873 & injective/surjective \\
874 \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
875 & injective over subset\\
876 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
882 \tdx{inj_def} inj f == ! x y. f x=f y --> x=y
883 \tdx{surj_def} surj f == ! y. ? x. y=f x
884 \tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
885 \tdx{inv_def} inv f == (\%y. @x. f(x)=y)
887 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
890 \subsection{Properties of functions}\nopagebreak
891 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
892 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
893 of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
894 rules. Reasoning about function composition (the operator~\sdx{o}) and the
895 predicate~\cdx{surj} is done simply by expanding the definitions.
897 There is also a large collection of monotonicity theorems for constructions
898 on sets in the file \texttt{HOL/mono.ML}.
900 \section{Generic packages}
901 \label{sec:HOL:generic-packages}
903 \HOL\ instantiates most of Isabelle's generic packages, making available the
904 simplifier and the classical reasoner.
906 \subsection{Simplification and substitution}
908 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
909 (\texttt{simpset()}), which works for most purposes. A quite minimal
910 simplification set for higher-order logic is~\ttindexbold{HOL_ss};
911 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
912 also expresses logical equivalence, may be used for rewriting. See
913 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
914 simplification rules.
916 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
917 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
920 \begin{warn}\index{simplification!of conjunctions}%
921 Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
922 left part of a conjunction helps in simplifying the right part. This effect
923 is not available by default: it can be slow. It can be obtained by
924 including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
927 If the simplifier cannot use a certain rewrite rule --- either because
928 of nontermination or because its left-hand side is too flexible ---
929 then you might try \texttt{stac}:
930 \begin{ttdescription}
931 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
932 replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
933 $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking
934 may be necessary to select the desired ones.
936 If $thm$ is a conditional equality, the instantiated condition becomes an
937 additional (first) subgoal.
940 \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
941 for an equality throughout a subgoal and its hypotheses. This tactic uses
942 \HOL's general substitution rule.
944 \subsubsection{Case splitting}
945 \label{subsec:HOL:case:splitting}
947 \HOL{} also provides convenient means for case splitting during
948 rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
949 then\dots else\dots} often require a case distinction on $b$. This is
950 expressed by the theorem \tdx{split_if}:
952 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
953 ((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y})))
956 For example, a simple instance of $(*)$ is
958 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
959 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
961 Because $(*)$ is too general as a rewrite rule for the simplifier (the
962 left-hand side is not a higher-order pattern in the sense of
963 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
964 {Chap.\ts\ref{chap:simplification}}), there is a special infix function
965 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
966 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
969 by(simp_tac (simpset() addsplits [split_if]) 1);
971 The effect is that after each round of simplification, one occurrence of
972 \texttt{if} is split acording to \texttt{split_if}, until all occurences of
973 \texttt{if} have been eliminated.
975 It turns out that using \texttt{split_if} is almost always the right thing to
976 do. Hence \texttt{split_if} is already included in the default simpset. If
977 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
978 the inverse of \texttt{addsplits}:
980 by(simp_tac (simpset() delsplits [split_if]) 1);
983 In general, \texttt{addsplits} accepts rules of the form
985 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
987 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
988 right form because internally the left-hand side is
989 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
990 are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
991 and~\S\ref{subsec:datatype:basics}).
993 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
994 imperative versions of \texttt{addsplits} and \texttt{delsplits}
996 \ttindexbold{Addsplits}: thm list -> unit
997 \ttindexbold{Delsplits}: thm list -> unit
999 for adding splitting rules to, and deleting them from the current simpset.
1001 \subsection{Classical reasoning}
1003 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1004 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1005 rule; recall Fig.\ts\ref{hol-lemmas2} above.
1007 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
1008 Best_tac} refer to the default claset (\texttt{claset()}), which works for most
1009 purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
1010 propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
1011 rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules,
1012 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1013 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
1016 \section{Types}\label{sec:HOL:Types}
1017 This section describes \HOL's basic predefined types ($\alpha \times
1018 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
1019 introducing new types in general. The most important type
1020 construction, the \texttt{datatype}, is treated separately in
1021 \S\ref{sec:HOL:datatype}.
1024 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1025 \label{subsec:prod-sum}
1027 \begin{figure}[htbp]
1029 \it symbol & \it meta-type & & \it description \\
1030 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
1031 & & ordered pairs $(a,b)$ \\
1032 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
1033 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
1034 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
1035 & & generalized projection\\
1037 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
1038 & general sum of sets
1040 \begin{ttbox}\makeatletter
1041 %\tdx{fst_def} fst p == @a. ? b. p = (a,b)
1042 %\tdx{snd_def} snd p == @b. ? a. p = (a,b)
1043 %\tdx{split_def} split c p == c (fst p) (snd p)
1044 \tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
1046 \tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
1047 \tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
1048 \tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
1050 \tdx{fst_conv} fst (a,b) = a
1051 \tdx{snd_conv} snd (a,b) = b
1052 \tdx{surjective_pairing} p = (fst p,snd p)
1054 \tdx{split} split c (a,b) = c a b
1055 \tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
1057 \tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
1058 \tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
1060 \caption{Type $\alpha\times\beta$}\label{hol-prod}
1063 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
1064 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
1065 tuples are simulated by pairs nested to the right:
1067 \begin{tabular}{c|c}
1068 external & internal \\
1070 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
1072 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
1075 In addition, it is possible to use tuples
1076 as patterns in abstractions:
1078 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}
1080 Nested patterns are also supported. They are translated stepwise:
1081 {\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$
1082 {\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
1083 $z$.\ $t$))}. The reverse translation is performed upon printing.
1085 The translation between patterns and \texttt{split} is performed automatically
1086 by the parser and printer. Thus the internal and external form of a term
1087 may differ, which can affects proofs. For example the term {\tt
1088 (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
1089 default simpset) to rewrite to {\tt(b,a)}.
1091 In addition to explicit $\lambda$-abstractions, patterns can be used in any
1092 variable binding construct which is internally described by a
1093 $\lambda$-abstraction. Some important examples are
1095 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
1096 \item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
1097 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
1098 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
1099 \item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
1102 There is a simple tactic which supports reasoning about patterns:
1103 \begin{ttdescription}
1104 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
1105 {\tt!!}-quantified variables of product type by individual variables for
1106 each component. A simple example:
1108 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
1109 by(split_all_tac 1);
1110 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
1114 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
1115 which contains only a single element named {\tt()} with the property
1117 \tdx{unit_eq} u = ()
1121 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
1122 which associates to the right and has a lower priority than $*$: $\tau@1 +
1123 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
1125 The definition of products and sums in terms of existing types is not
1126 shown. The constructions are fairly standard and can be found in the
1127 respective theory files.
1131 \it symbol & \it meta-type & & \it description \\
1132 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
1133 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
1134 \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
1137 \begin{ttbox}\makeatletter
1138 %\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
1139 % (!y. p=Inr y --> z=g y))
1141 \tdx{Inl_not_Inr} Inl a ~= Inr b
1143 \tdx{inj_Inl} inj Inl
1144 \tdx{inj_Inr} inj Inr
1146 \tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
1148 \tdx{sum_case_Inl} sum_case f g (Inl x) = f x
1149 \tdx{sum_case_Inr} sum_case f g (Inr x) = g x
1151 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
1152 \tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
1153 (! y. s = Inr(y) --> R(g(y))))
1155 \caption{Type $\alpha+\beta$}\label{hol-sum}
1166 \it symbol & \it meta-type & \it priority & \it description \\
1167 \cdx{0} & $nat$ & & zero \\
1168 \cdx{Suc} & $nat \To nat$ & & successor function\\
1169 % \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\
1170 % \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
1171 % & & primitive recursor\\
1172 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
1173 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
1174 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
1175 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
1176 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1178 \subcaption{Constants and infixes}
1180 \begin{ttbox}\makeatother
1181 \tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n
1183 \tdx{Suc_not_Zero} Suc m ~= 0
1184 \tdx{inj_Suc} inj Suc
1185 \tdx{n_not_Suc_n} n~=Suc n
1186 \subcaption{Basic properties}
1188 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
1193 \begin{ttbox}\makeatother
1195 (Suc m)+n = Suc(m+n)
1204 \tdx{mod_less} m<n ==> m mod n = m
1205 \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
1207 \tdx{div_less} m<n ==> m div n = 0
1208 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
1210 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
1213 \subsection{The type of natural numbers, \textit{nat}}
1214 \index{nat@{\textit{nat}} type|(}
1216 The theory \thydx{NatDef} defines the natural numbers in a roundabout but
1217 traditional way. The axiom of infinity postulates a type~\tydx{ind} of
1218 individuals, which is non-empty and closed under an injective operation. The
1219 natural numbers are inductively generated by choosing an arbitrary individual
1220 for~0 and using the injective operation to take successors. This is a least
1221 fixedpoint construction. For details see the file \texttt{NatDef.thy}.
1223 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the
1224 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also
1225 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory
1226 \thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order,
1227 so \tydx{nat} is also an instance of class \cldx{order}.
1229 Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines
1230 addition, multiplication and subtraction. Theory \thydx{Divides} defines
1231 division, remainder and the ``divides'' relation. The numerous theorems
1232 proved include commutative, associative, distributive, identity and
1233 cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The
1234 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
1235 \texttt{nat} are part of the default simpset.
1237 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
1238 see \S\ref{sec:HOL:recursive}. A simple example is addition.
1239 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1240 the standard convention.
1244 "Suc m + n = Suc (m + n)"
1246 There is also a \sdx{case}-construct
1249 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
1251 Note that Isabelle insists on precisely this format; you may not even change
1252 the order of the two cases.
1253 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
1254 \cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.
1256 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1257 %Recursion along this relation resembles primitive recursion, but is
1258 %stronger because we are in higher-order logic; using primitive recursion to
1259 %define a higher-order function, we can easily Ackermann's function, which
1260 %is not primitive recursive \cite[page~104]{thompson91}.
1261 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1262 %natural numbers are most easily expressed using recursion along~$<$.
1264 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
1265 in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived
1266 theorem \tdx{less_induct}:
1268 [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
1272 Reasoning about arithmetic inequalities can be tedious. Fortunately HOL
1273 provides a decision procedure for quantifier-free linear arithmetic (i.e.\
1274 only addition and subtraction). The simplifier invokes a weak version of this
1275 decision procedure automatically. If this is not sufficent, you can invoke
1276 the full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary
1277 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
1278 min}, {\tt max} and numerical constants; other subterms are treated as
1279 atomic; subformulae not involving type $nat$ are ignored; quantified
1280 subformulae are ignored unless they are positive universal or negative
1281 existential. Note that the running time is exponential in the number of
1282 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
1283 distinctions. Note also that \texttt{arith_tac} is not complete: if
1284 divisibility plays a role, it may fail to prove a valid formula, for example
1285 $m+m \neq n+n+1$. Fortunately such examples are rare in practice.
1287 If \texttt{arith_tac} fails you, try to find relevant arithmetic results in
1288 the library. The theory \texttt{NatDef} contains theorems about {\tt<} and
1289 {\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
1290 \texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
1291 \texttt{div} and \texttt{mod}. Use the \texttt{find}-functions to locate them
1292 (see the {\em Reference Manual\/}).
1295 \index{#@{\tt[]} symbol}
1296 \index{#@{\tt\#} symbol}
1297 \index{"@@{\tt\at} symbol}
1300 \it symbol & \it meta-type & \it priority & \it description \\
1301 \tt[] & $\alpha\,list$ & & empty list\\
1302 \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
1304 \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
1305 \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
1306 \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
1307 \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
1308 \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
1309 \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
1310 \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
1312 \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
1313 & & filter functional\\
1314 \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
1315 \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
1316 \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
1318 \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
1319 \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
1320 \cdx{length} & $\alpha\,list \To nat$ & & length \\
1321 \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
1322 \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
1323 take or drop a prefix \\
1326 $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
1327 take or drop a prefix
1329 \subcaption{Constants and infixes}
1331 \begin{center} \tt\frenchspacing
1332 \begin{tabular}{rrr}
1333 \it external & \it internal & \it description \\{}
1334 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1335 \rm finite list \\{}
1336 [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
1337 \rm list comprehension
1340 \subcaption{Translations}
1341 \caption{The theory \thydx{List}} \label{hol-list}
1346 \begin{ttbox}\makeatother
1355 (x#xs) @ ys = x # xs @ ys
1358 map f (x#xs) = f x # map f xs
1361 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
1363 set [] = \ttlbrace\ttrbrace
1364 set (x#xs) = insert x (set xs)
1367 x mem (y#ys) = (if y=x then True else x mem ys)
1370 foldl f a (x#xs) = foldl f (f a x) xs
1373 concat(x#xs) = x @ concat(xs)
1376 rev(x#xs) = rev(xs) @ [x]
1379 length(x#xs) = Suc(length(xs))
1382 xs!(Suc n) = (tl xs)!n
1385 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
1388 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
1391 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
1394 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
1396 \caption{Recursions equations for list processing functions}
1397 \label{fig:HOL:list-simps}
1399 \index{nat@{\textit{nat}} type|)}
1402 \subsection{The type constructor for lists, \textit{list}}
1404 \index{list@{\textit{list}} type|(}
1406 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
1407 operations with their types and syntax. Type $\alpha \; list$ is
1408 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
1409 As a result the generic structural induction and case analysis tactics
1410 \texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for
1411 lists. A \sdx{case} construct of the form
1413 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
1415 is defined by translation. For details see~\S\ref{sec:HOL:datatype}. There
1416 is also a case splitting rule \tdx{split_list_case}
1419 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
1420 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
1421 ((e = \texttt{[]} \to P(a)) \land
1422 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
1425 which can be fed to \ttindex{addsplits} just like
1426 \texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}).
1428 \texttt{List} provides a basic library of list processing functions defined by
1429 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations
1430 are shown in Fig.\ts\ref{fig:HOL:list-simps}.
1432 \index{list@{\textit{list}} type|)}
1435 \subsection{Introducing new types} \label{sec:typedef}
1437 The \HOL-methodology dictates that all extensions to a theory should
1438 be \textbf{definitional}. The type definition mechanism that
1439 meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms},
1440 which are inherited from {\Pure} and described elsewhere, are just
1441 syntactic abbreviations that have no logical meaning.
1444 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1445 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
1447 A \bfindex{type definition} identifies the new type with a subset of
1448 an existing type. More precisely, the new type is defined by
1449 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
1450 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
1451 and the new type denotes this subset. New functions are defined that
1452 establish an isomorphism between the new type and the subset. If
1453 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
1454 then the type definition creates a type constructor
1455 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
1457 \begin{figure}[htbp]
1459 typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
1461 type : typevarlist name ( () | '(' infix ')' );
1463 witness : () | '(' id ')';
1465 \caption{Syntax of type definitions}
1466 \label{fig:HOL:typedef}
1469 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
1470 the definition of `typevarlist' and `infix' see
1471 \iflabelundefined{chap:classical}
1472 {the appendix of the {\em Reference Manual\/}}%
1473 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
1476 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
1477 optional infix annotation.
1478 \item[\it name:] an alphanumeric name $T$ for the type constructor
1479 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
1480 \item[\it set:] the representing subset $A$.
1481 \item[\it witness:] name of a theorem of the form $a:A$ proving
1482 non-emptiness. It can be omitted in case Isabelle manages to prove
1483 non-emptiness automatically.
1485 If all context conditions are met (no duplicate type variables in
1486 `typevarlist', no extra type variables in `set', and no free term variables
1487 in `set'), the following components are added to the theory:
1489 \item a type $ty :: (term,\dots,term)term$
1493 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
1494 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
1496 \item a definition and three axioms
1499 T{\tt_def} & T \equiv A \\
1500 {\tt Rep_}T & Rep_T\,x \in T \\
1501 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
1502 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y
1505 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
1506 and its inverse $Abs_T$.
1508 Below are two simple examples of \HOL\ type definitions. Non-emptiness
1509 is proved automatically here.
1511 typedef unit = "{\ttlbrace}True{\ttrbrace}"
1514 ('a, 'b) "*" (infixr 20)
1515 = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
1518 Type definitions permit the introduction of abstract data types in a safe
1519 way, namely by providing models based on already existing types. Given some
1520 abstract axiomatic description $P$ of a type, this involves two steps:
1522 \item Find an appropriate type $\tau$ and subset $A$ which has the desired
1523 properties $P$, and make a type definition based on this representation.
1524 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
1526 You can now forget about the representation and work solely in terms of the
1527 abstract properties $P$.
1530 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
1531 declaring the type and its operations and by stating the desired axioms, you
1532 should make sure the type has a non-empty model. You must also have a clause
1535 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
1537 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
1538 class of all \HOL\ types.
1544 At a first approximation, records are just a minor generalisation of tuples,
1545 where components may be addressed by labels instead of just position (think of
1546 {\ML}, for example). The version of records offered by Isabelle/HOL is
1547 slightly more advanced, though, supporting \emph{extensible record schemes}.
1548 This admits operations that are polymorphic with respect to record extension,
1549 yielding ``object-oriented'' effects like (single) inheritance. See also
1550 \cite{NaraschewskiW-TPHOLs98} for more details on object-oriented
1551 verification and record subtyping in HOL.
1556 Isabelle/HOL supports fixed and schematic records both at the level of terms
1557 and types. The concrete syntax is as follows:
1560 \begin{tabular}{l|l|l}
1561 & record terms & record types \\ \hline
1562 fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
1563 schematic & $\record{x = a\fs y = b\fs \more = m}$ &
1564 $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
1568 \noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
1570 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
1571 $y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$,
1572 assuming that $a \ty A$ and $b \ty B$.
1574 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
1575 $x$ and $y$ as before, but also possibly further fields as indicated by the
1576 ``$\more$'' notation (which is actually part of the syntax). The improper
1577 field ``$\more$'' of a record scheme is called the \emph{more part}.
1578 Logically it is just a free variable, which is occasionally referred to as
1579 \emph{row variable} in the literature. The more part of a record scheme may
1580 be instantiated by zero or more further components. For example, above scheme
1581 might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
1582 where $m'$ refers to a different more part. Fixed records are special
1583 instances of record schemes, where ``$\more$'' is properly terminated by the
1584 $() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an
1585 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
1589 There are two key features that make extensible records in a simply typed
1590 language like HOL feasible:
1592 \item the more part is internalised, as a free term or type variable,
1593 \item field names are externalised, they cannot be accessed within the logic
1594 as first-class values.
1599 In Isabelle/HOL record types have to be defined explicitly, fixing their field
1600 names and types, and their (optional) parent record (see
1601 \S\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
1602 syntax, while obeying the canonical order of fields as given by their
1603 declaration. The record package also provides several operations like
1604 selectors and updates (see \S\ref{sec:HOL:record-ops}), together with
1605 characteristic properties (see \S\ref{sec:HOL:record-thms}).
1607 There is an example theory demonstrating most basic aspects of extensible
1608 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
1611 \subsection{Defining records}\label{sec:HOL:record-def}
1613 The theory syntax for record type definitions is shown in
1614 Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see
1615 \iflabelundefined{chap:classical}
1616 {the appendix of the {\em Reference Manual\/}}%
1617 {Appendix~\ref{app:TheorySyntax}}.
1619 \begin{figure}[htbp]
1621 record : 'record' typevarlist name '=' parent (field +);
1623 parent : ( () | type '+');
1624 field : name '::' type;
1626 \caption{Syntax of record type definitions}
1627 \label{fig:HOL:record}
1630 A general \ttindex{record} specification is of the following form:
1632 \mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
1633 (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
1635 where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
1636 $\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
1637 Type constructor $t$ has to be new, while $s$ has to specify an existing
1638 record type. Furthermore, the $\vec c@l$ have to be distinct field names.
1639 There has to be at least one field.
1641 In principle, field names may never be shared with other records. This is no
1642 actual restriction in practice, since $\vec c@l$ are internally declared
1643 within a separate name space qualified by the name $t$ of the record.
1647 Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
1648 extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
1649 \vec\sigma@l$. The parent record specification is optional, by omitting it
1650 $t$ becomes a \emph{root record}. The hierarchy of all records declared
1651 within a theory forms a forest structure, i.e.\ a set of trees, where any of
1652 these is rooted by some root record.
1654 For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
1655 fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
1656 \zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
1657 \vec\sigma@l\fs \more \ty \zeta}$.
1661 The following simple example defines a root record type $point$ with fields $x
1662 \ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
1663 an additional $colour$ component.
1670 record cpoint = point +
1675 \subsection{Record operations}\label{sec:HOL:record-ops}
1677 Any record definition of the form presented above produces certain standard
1678 operations. Selectors and updates are provided for any field, including the
1679 improper one ``$more$''. There are also cumulative record constructor
1682 To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
1683 is a root record with fields $\vec c@l \ty \vec\sigma@l$.
1687 \textbf{Selectors} and \textbf{updates} are available for any field (including
1688 ``$more$'') as follows:
1689 \begin{matharray}{lll}
1690 c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
1691 c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
1692 \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1695 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
1696 term $x_update \, a \, r$. Repeated updates are also supported: $r \,
1697 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
1698 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of
1699 postfix notation the order of fields shown here is reverse than in the actual
1700 term. This might lead to confusion in conjunction with proof tools like
1703 Since repeated updates are just function applications, fields may be freely
1704 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
1705 is concerned. Thus commutativity of updates can be proven within the logic
1706 for any two fields, but not as a general theorem: fields are not first-class
1711 \textbf{Make} operations provide cumulative record constructor functions:
1712 \begin{matharray}{lll}
1713 make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
1714 make_scheme & \ty & \vec\sigma@l \To
1715 \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
1718 These functions are curried. The corresponding definitions in terms of actual
1719 record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$
1720 rewrites to $\record{x = a\fs y = b}$.
1724 Any of above selector, update and make operations are declared within a local
1725 name space prefixed by the name $t$ of the record. In case that different
1726 records share base names of fields, one has to qualify names explicitly (e.g.\
1727 $t\dtt c@i_update$). This is recommended especially for operations like
1728 $make$ or $update_more$ that always have the same base name. Just use $t\dtt
1729 make$ etc.\ to avoid confusion.
1733 We reconsider the case of non-root records, which are derived of some parent
1734 record. In general, the latter may depend on another parent as well,
1735 resulting in a list of \emph{ancestor records}. Appending the lists of fields
1736 of all ancestors results in a certain field prefix. The record package
1737 automatically takes care of this by lifting operations over this context of
1738 ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
1739 $\vec d@k \ty \vec\rho@k$, selectors will get the following types:
1740 \begin{matharray}{lll}
1741 c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1745 Update and make operations are analogous.
1748 \subsection{Proof tools}\label{sec:HOL:record-thms}
1750 The record package provides the following proof rules for any record type $t$.
1753 \item Standard conversions (selectors or updates applied to record constructor
1754 terms, make function definitions) are part of the standard simpset (via
1757 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
1758 \conj y=y'$ are made part of the standard simpset and claset (via
1761 \item A tactic for record field splitting (\ttindex{record_split_tac}) is made
1762 part of the standard claset (via \texttt{addSWrapper}). This tactic is
1763 based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a,
1767 The first two kinds of rules are stored within the theory as $t\dtt simps$ and
1768 $t\dtt iffs$, respectively. In some situations it might be appropriate to
1769 expand the definitions of updates: $t\dtt updates$. Following a new trend in
1770 Isabelle system architecture, these names are \emph{not} bound at the {\ML}
1775 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
1776 concerning records. The basic idea is to make \ttindex{record_split_tac}
1777 expand quantified record variables and then simplify by the conversion rules.
1778 By using a combination of the simplifier and classical prover together with
1779 the default simpset and claset, record problems should be solved with a single
1780 stroke of \texttt{Auto_tac} or \texttt{Force_tac}.
1783 \section{Datatype definitions}
1784 \label{sec:HOL:datatype}
1787 Inductive datatypes, similar to those of \ML, frequently appear in
1788 applications of Isabelle/HOL. In principle, such types could be defined by
1789 hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
1790 tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
1791 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an
1792 appropriate \texttt{typedef} based on a least fixed-point construction, and
1793 proves freeness theorems and induction rules, as well as theorems for
1794 recursion and case combinators. The user just has to give a simple
1795 specification of new inductive types using a notation similar to {\ML} or
1798 The current datatype package can handle both mutual and indirect recursion.
1799 It also offers to represent existing types as datatypes giving the advantage
1800 of a more uniform view on standard theories.
1804 \label{subsec:datatype:basics}
1806 A general \texttt{datatype} definition is of the following form:
1809 \mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = &
1810 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~
1811 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\
1813 \mathtt{and} & (\alpha@1,\ldots,\alpha@h)t@n & = &
1814 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~
1815 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}
1818 where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor
1819 names and $\tau^j@{i,i'}$ are {\em admissible} types containing at
1820 most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$
1821 occurring in a \texttt{datatype} definition is {\em admissible} iff
1823 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
1824 newly defined type constructors $t@1,\ldots,t@n$, or
1825 \item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or
1826 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
1827 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1828 are admissible types.
1829 \item $\tau = \sigma \rightarrow \tau'$, where $\tau'$ is an admissible
1830 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
1831 types are {\em strictly positive})
1833 If some $(\alpha@1,\ldots,\alpha@h)t@{j'}$ occurs in a type $\tau^j@{i,i'}$
1836 (\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t'
1838 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
1839 example of a datatype is the type \texttt{list}, which can be defined by
1841 datatype 'a list = Nil
1844 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
1845 by the mutually recursive datatype definition
1847 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
1848 | Sum ('a aexp) ('a aexp)
1849 | Diff ('a aexp) ('a aexp)
1852 and 'a bexp = Less ('a aexp) ('a aexp)
1853 | And ('a bexp) ('a bexp)
1854 | Or ('a bexp) ('a bexp)
1856 The datatype \texttt{term}, which is defined by
1858 datatype ('a, 'b) term = Var 'a
1859 | App 'b ((('a, 'b) term) list)
1861 is an example for a datatype with nested recursion. Using nested recursion
1862 involving function spaces, we may also define infinitely branching datatypes, e.g.
1864 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
1869 Types in HOL must be non-empty. Each of the new datatypes
1870 $(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a
1871 constructor $C^j@i$ with the following property: for all argument types
1872 $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
1873 $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
1875 If there are no nested occurrences of the newly defined datatypes, obviously
1876 at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$
1877 must have a constructor $C^j@i$ without recursive arguments, a \emph{base
1878 case}, to ensure that the new types are non-empty. If there are nested
1879 occurrences, a datatype can even be non-empty without having a base case
1880 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
1881 list)} is non-empty as well.
1884 \subsubsection{Freeness of the constructors}
1886 The datatype constructors are automatically defined as functions of their
1888 \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
1889 These functions have certain {\em freeness} properties. They construct
1892 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
1893 \mbox{for all}~ i \neq i'.
1895 The constructor functions are injective:
1897 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
1898 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
1900 Since the number of distinctness inequalities is quadratic in the number of
1901 constructors, the datatype package avoids proving them separately if there are
1902 too many constructors. Instead, specific inequalities are proved by a suitable
1903 simplification procedure on demand.\footnote{This procedure, which is already part
1904 of the default simpset, may be referred to by the ML identifier
1905 \texttt{DatatypePackage.distinct_simproc}.}
1907 \subsubsection{Structural induction}
1909 The datatype package also provides structural induction rules. For
1910 datatypes without nested recursion, this is of the following form:
1912 \infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
1914 \Forall x@1 \dots x@{m^1@1}.
1915 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
1916 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &
1917 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\
1919 \Forall x@1 \dots x@{m^1@{k@1}}.
1920 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;
1921 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &
1922 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\
1924 \Forall x@1 \dots x@{m^n@1}.
1925 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;
1926 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &
1927 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\
1929 \Forall x@1 \dots x@{m^n@{k@n}}.
1930 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots
1931 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &
1932 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)
1939 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
1940 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
1941 && \left\{(i',i'')~\left|~
1942 1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge
1943 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
1946 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
1948 For datatypes with nested recursion, such as the \texttt{term} example from
1949 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
1952 datatype ('a, 'b) term = Var 'a
1953 | App 'b ((('a, 'b) term) list)
1955 to an equivalent definition without nesting:
1957 datatype ('a, 'b) term = Var
1958 | App 'b (('a, 'b) term_list)
1959 and ('a, 'b) term_list = Nil'
1960 | Cons' (('a,'b) term) (('a,'b) term_list)
1962 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
1963 Nil'} and \texttt{Cons'} are not really introduced. One can directly work with
1964 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
1965 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
1966 \texttt{term} gets the form
1968 \infer{P@1~x@1 \wedge P@2~x@2}
1970 \Forall x.~P@1~(\mathtt{Var}~x) \\
1971 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
1973 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
1976 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
1977 and one for the type \texttt{(('a, 'b) term) list}.
1979 For a datatype with function types such as \texttt{'a tree}, the induction rule
1983 {\Forall a.~P~(\mathtt{Atom}~a) &
1984 \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}
1987 \medskip In principle, inductive types are already fully determined by
1988 freeness and structural induction. For convenience in applications,
1989 the following derived constructions are automatically provided for any
1992 \subsubsection{The \sdx{case} construct}
1994 The type comes with an \ML-like \texttt{case}-construct:
1997 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
1999 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}
2002 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
2003 \S\ref{subsec:prod-sum}.
2005 All constructors must be present, their order is fixed, and nested patterns
2006 are not supported (with the exception of tuples). Violating this
2007 restriction results in strange error messages.
2010 To perform case distinction on a goal containing a \texttt{case}-construct,
2011 the theorem $t@j.$\texttt{split} is provided:
2013 \begin{array}{@{}rcl@{}}
2014 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&
2015 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to
2016 P(f@1~x@1\dots x@{m^j@1})) \\
2017 &&\!\!\! ~\land~ \dots ~\land \\
2018 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to
2019 P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))
2022 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
2023 This theorem can be added to a simpset via \ttindex{addsplits}
2024 (see~\S\ref{subsec:HOL:case:splitting}).
2026 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
2028 Theory \texttt{Arith} declares a generic function \texttt{size} of type
2029 $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
2030 by overloading according to the following scheme:
2031 %%% FIXME: This formula is too big and is completely unreadable
2033 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
2036 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\
2037 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &
2038 \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
2039 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}
2043 where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
2044 size of a leaf is 0 and the size of a node is the sum of the sizes of its
2047 \subsection{Defining datatypes}
2049 The theory syntax for datatype definitions is shown in
2050 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
2051 definition has to obey the rules stated in the previous section. As a result
2052 the theory is extended with the new types, the constructors, and the theorems
2053 listed in the previous section.
2057 datatype : 'datatype' typedecls;
2059 typedecls: ( newtype '=' (cons + '|') ) + 'and'
2061 newtype : typevarlist id ( () | '(' infix ')' )
2063 cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
2065 argtype : id | tid | ('(' typevarlist id ')')
2068 \caption{Syntax of datatype declarations}
2069 \label{datatype-grammar}
2072 Most of the theorems about datatypes become part of the default simpset and
2073 you never need to see them again because the simplifier applies them
2074 automatically. Only induction or exhaustion are usually invoked by hand.
2075 \begin{ttdescription}
2076 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
2077 applies structural induction on variable $x$ to subgoal $i$, provided the
2078 type of $x$ is a datatype.
2079 \item[\ttindexbold{mutual_induct_tac}
2080 {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous
2081 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This
2082 is the canonical way to prove properties of mutually recursive datatypes
2083 such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as
2086 In some cases, induction is overkill and a case distinction over all
2087 constructors of the datatype suffices.
2088 \begin{ttdescription}
2089 \item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$]
2090 performs an exhaustive case analysis for the term $u$ whose type
2091 must be a datatype. If the datatype has $k@j$ constructors
2092 $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which
2093 contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for
2094 $i'=1$, $\dots$,~$k@j$.
2097 Note that induction is only allowed on free variables that should not occur
2098 among the premises of the subgoal. Exhaustion applies to arbitrary terms.
2103 For the technically minded, we exhibit some more details. Processing the
2104 theory file produces an \ML\ structure which, in addition to the usual
2105 components, contains a structure named $t$ for each datatype $t$ defined in
2106 the file. Each structure $t$ contains the following elements:
2108 val distinct : thm list
2109 val inject : thm list
2112 val cases : thm list
2117 val simps : thm list
2119 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}
2120 and \texttt{split} contain the theorems
2121 described above. For user convenience, \texttt{distinct} contains
2122 inequalities in both directions. The reduction rules of the {\tt
2123 case}-construct are in \texttt{cases}. All theorems from {\tt
2124 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
2125 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
2126 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
2129 \subsection{Representing existing types as datatypes}
2131 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
2132 +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
2133 but by more primitive means using \texttt{typedef}. To be able to use the
2134 tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by
2135 primitive recursion on these types, such types may be represented as actual
2136 datatypes. This is done by specifying an induction rule, as well as theorems
2137 stating the distinctness and injectivity of constructors in a {\tt
2138 rep_datatype} section. For type \texttt{nat} this works as follows:
2141 distinct Suc_not_Zero, Zero_not_Suc
2145 The datatype package automatically derives additional theorems for recursion
2146 and case combinators from these rules. Any of the basic HOL types mentioned
2147 above are represented as datatypes. Try an induction on \texttt{bool}
2151 \subsection{Examples}
2153 \subsubsection{The datatype $\alpha~mylist$}
2155 We want to define a type $\alpha~mylist$. To do this we have to build a new
2156 theory that contains the type definition. We start from the theory
2157 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
2158 \texttt{List} theory of Isabelle/HOL.
2161 datatype 'a mylist = Nil | Cons 'a ('a mylist)
2164 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To
2165 ease the induction applied below, we state the goal with $x$ quantified at the
2166 object-level. This will be stripped later using \ttindex{qed_spec_mp}.
2168 Goal "!x. Cons x xs ~= xs";
2170 {\out ! x. Cons x xs ~= xs}
2171 {\out 1. ! x. Cons x xs ~= xs}
2173 This can be proved by the structural induction tactic:
2175 by (induct_tac "xs" 1);
2177 {\out ! x. Cons x xs ~= xs}
2178 {\out 1. ! x. Cons x Nil ~= Nil}
2179 {\out 2. !!a mylist.}
2180 {\out ! x. Cons x mylist ~= mylist ==>}
2181 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
2183 The first subgoal can be proved using the simplifier. Isabelle/HOL has
2184 already added the freeness properties of lists to the default simplification
2189 {\out ! x. Cons x xs ~= xs}
2190 {\out 1. !!a mylist.}
2191 {\out ! x. Cons x mylist ~= mylist ==>}
2192 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
2194 Similarly, we prove the remaining goal.
2196 by (Asm_simp_tac 1);
2198 {\out ! x. Cons x xs ~= xs}
2201 qed_spec_mp "not_Cons_self";
2202 {\out val not_Cons_self = "Cons x xs ~= xs" : thm}
2204 Because both subgoals could have been proved by \texttt{Asm_simp_tac}
2205 we could have done that in one step:
2207 by (ALLGOALS Asm_simp_tac);
2211 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
2213 In this example we define the type $\alpha~mylist$ again but this time
2214 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix
2215 notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix
2216 annotations after the constructor declarations as follows:
2219 datatype 'a mylist =
2221 Cons 'a ('a mylist) (infixr "#" 70)
2224 Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
2227 \subsubsection{A datatype for weekdays}
2229 This example shows a datatype that consists of 7 constructors:
2232 datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
2235 Because there are more than 6 constructors, inequality is expressed via a function
2236 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
2237 contained among the distinctness theorems, but the simplifier can
2238 prove it thanks to rewrite rules inherited from theory \texttt{Arith}:
2243 You need not derive such inequalities explicitly: the simplifier will dispose
2244 of them automatically.
2248 \section{Recursive function definitions}\label{sec:HOL:recursive}
2249 \index{recursive functions|see{recursion}}
2251 Isabelle/HOL provides two main mechanisms of defining recursive functions.
2253 \item \textbf{Primitive recursion} is available only for datatypes, and it is
2254 somewhat restrictive. Recursive calls are only allowed on the argument's
2255 immediate constituents. On the other hand, it is the form of recursion most
2256 often wanted, and it is easy to use.
2258 \item \textbf{Well-founded recursion} requires that you supply a well-founded
2259 relation that governs the recursion. Recursive calls are only allowed if
2260 they make the argument decrease under the relation. Complicated recursion
2261 forms, such as nested recursion, can be dealt with. Termination can even be
2262 proved at a later time, though having unsolved termination conditions around
2263 can make work difficult.%
2264 \footnote{This facility is based on Konrad Slind's TFL
2265 package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
2266 and assisting with its installation.}
2269 Following good HOL tradition, these declarations do not assert arbitrary
2270 axioms. Instead, they define the function using a recursion operator. Both
2271 HOL and ZF derive the theory of well-founded recursion from first
2272 principles~\cite{paulson-set-II}. Primitive recursion over some datatype
2273 relies on the recursion operator provided by the datatype package. With
2274 either form of function definition, Isabelle proves the desired recursion
2275 equations as theorems.
2278 \subsection{Primitive recursive functions}
2279 \label{sec:HOL:primrec}
2280 \index{recursion!primitive|(}
2283 Datatypes come with a uniform way of defining functions, {\bf primitive
2284 recursion}. In principle, one could introduce primitive recursive functions
2285 by asserting their reduction rules as new axioms, but this is not recommended:
2286 \begin{ttbox}\slshape
2288 consts app :: ['a list, 'a list] => 'a list
2290 app_Nil "app [] ys = ys"
2291 app_Cons "app (x#xs) ys = x#app xs ys"
2294 Asserting axioms brings the danger of accidentally asserting nonsense, as
2295 in \verb$app [] ys = us$.
2297 The \ttindex{primrec} declaration is a safe means of defining primitive
2298 recursive functions on datatypes:
2301 consts app :: ['a list, 'a list] => 'a list
2304 "app (x#xs) ys = x#app xs ys"
2307 Isabelle will now check that the two rules do indeed form a primitive
2308 recursive definition. For example
2313 is rejected with an error message ``\texttt{Extra variables on rhs}''.
2317 The general form of a primitive recursive definition is
2320 {\it reduction rules}
2322 where \textit{reduction rules} specify one or more equations of the form
2323 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
2324 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
2325 contains only the free variables on the left-hand side, and all recursive
2326 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
2327 must be at most one reduction rule for each constructor. The order is
2328 immaterial. For missing constructors, the function is defined to return a
2331 If you would like to refer to some rule by name, then you must prefix
2332 the rule with an identifier. These identifiers, like those in the
2333 \texttt{rules} section of a theory, will be visible at the \ML\ level.
2335 The primitive recursive function can have infix or mixfix syntax:
2336 \begin{ttbox}\underscoreon
2337 consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
2340 "(x#xs) @ ys = x#(xs @ ys)"
2343 The reduction rules become part of the default simpset, which
2344 leads to short proof scripts:
2345 \begin{ttbox}\underscoreon
2346 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
2347 by (induct\_tac "xs" 1);
2348 by (ALLGOALS Asm\_simp\_tac);
2351 \subsubsection{Example: Evaluation of expressions}
2352 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
2353 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
2354 \S\ref{subsec:datatype:basics}:
2357 evala :: "['a => nat, 'a aexp] => nat"
2358 evalb :: "['a => nat, 'a bexp] => bool"
2361 "evala env (If_then_else b a1 a2) =
2362 (if evalb env b then evala env a1 else evala env a2)"
2363 "evala env (Sum a1 a2) = evala env a1 + evala env a2"
2364 "evala env (Diff a1 a2) = evala env a1 - evala env a2"
2365 "evala env (Var v) = env v"
2366 "evala env (Num n) = n"
2368 "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
2369 "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
2370 "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"
2372 Since the value of an expression depends on the value of its variables,
2373 the functions \texttt{evala} and \texttt{evalb} take an additional
2374 parameter, an {\em environment} of type \texttt{'a => nat}, which maps
2375 variables to their values.
2377 Similarly, we may define substitution functions \texttt{substa}
2378 and \texttt{substb} for expressions: The mapping \texttt{f} of type
2379 \texttt{'a => 'a aexp} given as a parameter is lifted canonically
2380 on the types \texttt{'a aexp} and \texttt{'a bexp}:
2383 substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"
2384 substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"
2387 "substa f (If_then_else b a1 a2) =
2388 If_then_else (substb f b) (substa f a1) (substa f a2)"
2389 "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
2390 "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
2391 "substa f (Var v) = f v"
2392 "substa f (Num n) = Num n"
2394 "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
2395 "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
2396 "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"
2398 In textbooks about semantics one often finds {\em substitution theorems},
2399 which express the relationship between substitution and evaluation. For
2400 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
2401 induction, followed by simplification:
2404 "evala env (substa (Var(v := a')) a) =
2405 evala (env(v := evala env a')) a &
2406 evalb env (substb (Var(v := a')) b) =
2407 evalb (env(v := evala env a')) b";
2408 by (mutual_induct_tac ["a","b"] 1);
2409 by (ALLGOALS Asm_full_simp_tac);
2412 \subsubsection{Example: A substitution function for terms}
2413 Functions on datatypes with nested recursion, such as the type
2414 \texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are
2415 also defined by mutual primitive recursion. A substitution
2416 function \texttt{subst_term} on type \texttt{term}, similar to the functions
2417 \texttt{substa} and \texttt{substb} described above, can
2418 be defined as follows:
2421 subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
2423 "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
2426 "subst_term f (Var a) = f a"
2427 "subst_term f (App b ts) = App b (subst_term_list f ts)"
2429 "subst_term_list f [] = []"
2430 "subst_term_list f (t # ts) =
2431 subst_term f t # subst_term_list f ts"
2433 The recursion scheme follows the structure of the unfolded definition of type
2434 \texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
2435 this substitution function, mutual induction is needed:
2438 "(subst_term ((subst_term f1) o f2) t) =
2439 (subst_term f1 (subst_term f2 t)) &
2440 (subst_term_list ((subst_term f1) o f2) ts) =
2441 (subst_term_list f1 (subst_term_list f2 ts))";
2442 by (mutual_induct_tac ["t", "ts"] 1);
2443 by (ALLGOALS Asm_full_simp_tac);
2446 \subsubsection{Example: A map function for infinitely branching trees}
2447 Defining functions on infinitely branching datatypes by primitive
2448 recursion is just as easy. For example, we can define a function
2449 \texttt{map_tree} on \texttt{'a tree} as follows:
2452 map_tree :: "('a => 'b) => 'a tree => 'b tree"
2455 "map_tree f (Atom a) = Atom (f a)"
2456 "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"
2458 Note that all occurrences of functions such as \texttt{ts} in the
2459 \texttt{primrec} clauses must be applied to an argument. In particular,
2460 \texttt{map_tree f o ts} is not allowed.
2462 \index{recursion!primitive|)}
2466 \subsection{General recursive functions}
2467 \label{sec:HOL:recdef}
2468 \index{recursion!general|(}
2471 Using \texttt{recdef}, you can declare functions involving nested recursion
2472 and pattern-matching. Recursion need not involve datatypes and there are few
2473 syntactic restrictions. Termination is proved by showing that each recursive
2474 call makes the argument smaller in a suitable sense, which you specify by
2475 supplying a well-founded relation.
2477 Here is a simple example, the Fibonacci function. The first line declares
2478 \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on
2479 the natural numbers). Pattern-matching is used here: \texttt{1} is a
2480 macro for \texttt{Suc~0}.
2482 consts fib :: "nat => nat"
2483 recdef fib "less_than"
2486 "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
2489 With \texttt{recdef}, function definitions may be incomplete, and patterns may
2490 overlap, as in functional programming. The \texttt{recdef} package
2491 disambiguates overlapping patterns by taking the order of rules into account.
2492 For missing patterns, the function is defined to return a default value.
2494 %For example, here is a declaration of the list function \cdx{hd}:
2496 %consts hd :: 'a list => 'a
2500 %Because this function is not recursive, we may supply the empty well-founded
2503 The well-founded relation defines a notion of ``smaller'' for the function's
2504 argument type. The relation $\prec$ is \textbf{well-founded} provided it
2505 admits no infinitely decreasing chains
2506 \[ \cdots\prec x@n\prec\cdots\prec x@1. \]
2507 If the function's argument has type~$\tau$, then $\prec$ has to be a relation
2508 over~$\tau$: it must have type $(\tau\times\tau)set$.
2510 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
2511 of operators for building well-founded relations. The package recognises
2512 these operators and automatically proves that the constructed relation is
2513 well-founded. Here are those operators, in order of importance:
2515 \item \texttt{less_than} is ``less than'' on the natural numbers.
2516 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.
2518 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
2519 relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$.
2520 Typically, $f$ takes the recursive function's arguments (as a tuple) and
2521 returns a result expressed in terms of the function \texttt{size}. It is
2522 called a \textbf{measure function}. Recall that \texttt{size} is overloaded
2523 and is defined on all datatypes (see \S\ref{sec:HOL:size}).
2525 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
2526 \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$
2527 is less than $f(y)$ according to~$R$, which must itself be a well-founded
2530 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It
2531 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$
2532 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$
2533 is less than $y@2$ according to~$R@2$.
2535 \item \texttt{finite_psubset} is the proper subset relation on finite sets.
2538 We can use \texttt{measure} to declare Euclid's algorithm for the greatest
2539 common divisor. The measure function, $\lambda(m,n). n$, specifies that the
2540 recursion terminates because argument~$n$ decreases.
2542 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
2543 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2546 The general form of a well-founded recursive definition is
2548 recdef {\it function} {\it rel}
2549 congs {\it congruence rules} {\bf(optional)}
2550 simpset {\it simplification set} {\bf(optional)}
2551 {\it reduction rules}
2555 \item \textit{function} is the name of the function, either as an \textit{id}
2556 or a \textit{string}.
2558 \item \textit{rel} is a {\HOL} expression for the well-founded termination
2561 \item \textit{congruence rules} are required only in highly exceptional
2564 \item The \textit{simplification set} is used to prove that the supplied
2565 relation is well-founded. It is also used to prove the \textbf{termination
2566 conditions}: assertions that arguments of recursive calls decrease under
2567 \textit{rel}. By default, simplification uses \texttt{simpset()}, which
2568 is sufficient to prove well-foundedness for the built-in relations listed
2571 \item \textit{reduction rules} specify one or more recursion equations. Each
2572 left-hand side must have the form $f\,t$, where $f$ is the function and $t$
2573 is a tuple of distinct variables. If more than one equation is present then
2574 $f$ is defined by pattern-matching on components of its argument whose type
2575 is a \texttt{datatype}.
2577 Unlike with \texttt{primrec}, the reduction rules are not added to the
2578 default simpset, and individual rules may not be labelled with identifiers.
2579 However, the identifier $f$\texttt{.rules} is visible at the \ML\ level
2580 as a list of theorems.
2583 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
2584 prove one termination condition. It remains as a precondition of the
2588 {\out ["! m n. n ~= 0 --> m mod n < n}
2589 {\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] }
2592 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
2593 conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard
2594 function \texttt{goalw}, which sets up a goal to prove, but its argument
2595 should be the identifier $f$\texttt{.rules} and its effect is to set up a
2596 proof of the termination conditions:
2598 Tfl.tgoalw thy [] gcd.rules;
2600 {\out ! m n. n ~= 0 --> m mod n < n}
2601 {\out 1. ! m n. n ~= 0 --> m mod n < n}
2603 This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem
2604 is proved, it can be used to eliminate the termination conditions from
2605 elements of \texttt{gcd.rules}. Theory \texttt{HOL/Subst/Unify} is a much
2606 more complicated example of this process, where the termination conditions can
2607 only be proved by complicated reasoning involving the recursive function
2610 Isabelle/HOL can prove the \texttt{gcd} function's termination condition
2611 automatically if supplied with the right simpset.
2613 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
2614 simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"
2615 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2618 A \texttt{recdef} definition also returns an induction rule specialised for
2619 the recursive function. For the \texttt{gcd} function above, the induction
2623 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}
2625 This rule should be used to reason inductively about the \texttt{gcd}
2626 function. It usually makes the induction hypothesis available at all
2627 recursive calls, leading to very direct proofs. If any termination conditions
2628 remain unproved, they will become additional premises of this rule.
2630 \index{recursion!general|)}
2634 \section{Inductive and coinductive definitions}
2635 \index{*inductive|(}
2636 \index{*coinductive|(}
2638 An {\bf inductive definition} specifies the least set~$R$ closed under given
2639 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
2640 example, a structural operational semantics is an inductive definition of an
2641 evaluation relation. Dually, a {\bf coinductive definition} specifies the
2642 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
2643 seen as arising by applying a rule to elements of~$R$.) An important example
2644 is using bisimulation relations to formalise equivalence of processes and
2645 infinite data structures.
2647 A theory file may contain any number of inductive and coinductive
2648 definitions. They may be intermixed with other declarations; in
2649 particular, the (co)inductive sets {\bf must} be declared separately as
2650 constants, and may have mixfix syntax or be subject to syntax translations.
2652 Each (co)inductive definition adds definitions to the theory and also
2653 proves some theorems. Each definition creates an \ML\ structure, which is a
2654 substructure of the main theory structure.
2656 This package is related to the \ZF\ one, described in a separate
2658 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
2659 distributed with Isabelle.} %
2660 which you should refer to in case of difficulties. The package is simpler
2661 than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types
2662 of the (co)inductive sets determine the domain of the fixedpoint definition,
2663 and the package does not have to use inference rules for type-checking.
2666 \subsection{The result structure}
2667 Many of the result structure's components have been discussed in the paper;
2668 others are self-explanatory.
2670 \item[\tt defs] is the list of definitions of the recursive sets.
2672 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
2674 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
2675 the recursive sets, in the case of mutual recursion).
2677 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
2678 the recursive sets. The rules are also available individually, using the
2679 names given them in the theory file.
2681 \item[\tt elims] is the list of elimination rule.
2683 \item[\tt elim] is the head of the list \texttt{elims}.
2685 \item[\tt mk_cases] is a function to create simplified instances of {\tt
2686 elim} using freeness reasoning on underlying datatypes.
2689 For an inductive definition, the result structure contains the
2690 rule \texttt{induct}. For a
2691 coinductive definition, it contains the rule \verb|coinduct|.
2693 Figure~\ref{def-result-fig} summarises the two result signatures,
2694 specifying the types of all these components.
2702 val intrs : thm list
2703 val elims : thm list
2705 val mk_cases : string -> thm
2706 {\it(Inductive definitions only)}
2708 {\it(coinductive definitions only)}
2713 \caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
2716 \subsection{The syntax of a (co)inductive definition}
2717 An inductive definition has the form
2719 inductive {\it inductive sets}
2720 intrs {\it introduction rules}
2721 monos {\it monotonicity theorems}
2722 con_defs {\it constructor definitions}
2724 A coinductive definition is identical, except that it starts with the keyword
2725 \texttt{coinductive}.
2727 The \texttt{monos} and \texttt{con_defs} sections are optional. If present,
2728 each is specified by a list of identifiers.
2731 \item The \textit{inductive sets} are specified by one or more strings.
2733 \item The \textit{introduction rules} specify one or more introduction rules in
2734 the form \textit{ident\/}~\textit{string}, where the identifier gives the name of
2735 the rule in the result structure.
2737 \item The \textit{monotonicity theorems} are required for each operator
2738 applied to a recursive set in the introduction rules. There {\bf must}
2739 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
2740 premise $t\in M(R@i)$ in an introduction rule!
2742 \item The \textit{constructor definitions} contain definitions of constants
2743 appearing in the introduction rules. In most cases it can be omitted.
2747 \subsection{Example of an inductive definition}
2748 Two declarations, included in a theory file, define the finite powerset
2749 operator. First we declare the constant~\texttt{Fin}. Then we declare it
2750 inductively, with two introduction rules:
2752 consts Fin :: 'a set => 'a set set
2755 emptyI "{\ttlbrace}{\ttrbrace} : Fin A"
2756 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
2758 The resulting theory structure contains a substructure, called~\texttt{Fin}.
2759 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
2760 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
2761 rule is \texttt{Fin.induct}.
2763 For another example, here is a theory file defining the accessible
2764 part of a relation. The main thing to note is the use of~\texttt{Pow} in
2765 the sole introduction rule, and the corresponding mention of the rule
2766 \verb|Pow_mono| in the \texttt{monos} list. The paper
2767 \cite{paulson-CADE} discusses a \ZF\ version of this example in more
2771 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
2772 acc :: "('a * 'a)set => 'a set" (*Accessible part*)
2773 defs pred_def "pred x r == {y. (y,x):r}"
2776 pred "pred a r: Pow(acc r) ==> a: acc r"
2780 The Isabelle distribution contains many other inductive definitions. Simple
2781 examples are collected on subdirectory \texttt{HOL/Induct}. The theory
2782 \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples
2783 may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},
2784 \texttt{Lambda} and \texttt{Auth}.
2786 \index{*coinductive|)} \index{*inductive|)}
2789 \section{The examples directories}
2791 Directory \texttt{HOL/Auth} contains theories for proving the correctness of
2792 cryptographic protocols~\cite{paulson-jcs}. The approach is based upon
2793 operational semantics rather than the more usual belief logics. On the same
2794 directory are proofs for some standard examples, such as the Needham-Schroeder
2795 public-key authentication protocol and the Otway-Rees
2798 Directory \texttt{HOL/IMP} contains a formalization of various denotational,
2799 operational and axiomatic semantics of a simple while-language, the necessary
2800 equivalence proofs, soundness and completeness of the Hoare rules with
2801 respect to the denotational semantics, and soundness and completeness of a
2802 verification condition generator. Much of development is taken from
2803 Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
2805 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
2806 logic, including a tactic for generating verification-conditions.
2808 Directory \texttt{HOL/MiniML} contains a formalization of the type system of
2809 the core functional language Mini-ML and a correctness proof for its type
2810 inference algorithm $\cal W$~\cite{milner78,nipkow-W}.
2812 Directory \texttt{HOL/Lambda} contains a formalization of untyped
2813 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
2814 and $\eta$ reduction~\cite{Nipkow-CR}.
2816 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of
2817 substitutions and unifiers. It is based on Paulson's previous
2818 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
2819 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef},
2820 with nested recursion.
2822 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive
2823 definitions and datatypes.
2825 \item Theory \texttt{PropLog} proves the soundness and completeness of
2826 classical propositional logic, given a truth table semantics. The only
2827 connective is $\imp$. A Hilbert-style axiom system is specified, and its
2828 set of theorems defined inductively. A similar proof in \ZF{} is
2829 described elsewhere~\cite{paulson-set-II}.
2831 \item Theory \texttt{Term} defines the datatype \texttt{term}.
2833 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions
2834 as mutually recursive datatypes.
2836 \item The definition of lazy lists demonstrates methods for handling
2837 infinite data structures and coinduction in higher-order
2838 logic~\cite{paulson-coind}.%
2839 \footnote{To be precise, these lists are \emph{potentially infinite} rather
2840 than lazy. Lazy implies a particular operational semantics.}
2841 Theory \thydx{LList} defines an operator for
2842 corecursion on lazy lists, which is used to define a few simple functions
2843 such as map and append. A coinduction principle is defined
2844 for proving equations on lazy lists.
2846 \item Theory \thydx{LFilter} defines the filter functional for lazy lists.
2847 This functional is notoriously difficult to define because finding the next
2848 element meeting the predicate requires possibly unlimited search. It is not
2849 computable, but can be expressed using a combination of induction and
2852 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions
2853 to express a programming language semantics that appears to require mutual
2854 induction. Iterated induction allows greater modularity.
2857 Directory \texttt{HOL/ex} contains other examples and experimental proofs in
2860 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
2861 to define recursive functions. Another example is \texttt{Fib}, which
2862 defines the Fibonacci function.
2864 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two
2865 natural numbers and proves a key lemma of the Fundamental Theorem of
2866 Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$
2869 \item Theory \texttt{Primrec} develops some computation theory. It
2870 inductively defines the set of primitive recursive functions and presents a
2871 proof that Ackermann's function is not primitive recursive.
2873 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty
2874 predicate calculus theorems, ranging from simple tautologies to
2875 moderately difficult problems involving equality and quantifiers.
2877 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc
2878 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
2879 much more powerful than Isabelle's classical reasoner. But it is less
2880 useful in practice because it works only for pure logic; it does not
2881 accept derived rules for the set theory primitives, for example.
2883 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof
2884 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
2886 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
2887 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
2889 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
2890 Milner and Tofte's coinduction example~\cite{milner-coind}. This
2891 substantial proof concerns the soundness of a type system for a simple
2892 functional language. The semantics of recursion is given by a cyclic
2893 environment, which makes a coinductive argument appropriate.
2898 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
2899 Cantor's Theorem states that every set has more subsets than it has
2900 elements. It has become a favourite example in higher-order logic since
2901 it is so easily expressed:
2902 \[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.
2903 \forall x::\alpha. f~x \not= S
2906 Viewing types as sets, $\alpha\To bool$ represents the powerset
2907 of~$\alpha$. This version states that for every function from $\alpha$ to
2908 its powerset, some subset is outside its range.
2910 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
2911 the operator \cdx{range}.
2915 The set~$S$ is given as an unknown instead of a
2916 quantified variable so that we may inspect the subset found by the proof.
2918 Goal "?S ~: range\thinspace(f :: 'a=>'a set)";
2920 {\out ?S ~: range f}
2921 {\out 1. ?S ~: range f}
2923 The first two steps are routine. The rule \tdx{rangeE} replaces
2924 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.
2926 by (resolve_tac [notI] 1);
2928 {\out ?S ~: range f}
2929 {\out 1. ?S : range f ==> False}
2931 by (eresolve_tac [rangeE] 1);
2933 {\out ?S ~: range f}
2934 {\out 1. !!x. ?S = f x ==> False}
2936 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,
2937 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for
2940 by (eresolve_tac [equalityCE] 1);
2942 {\out ?S ~: range f}
2943 {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}
2944 {\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}
2946 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
2947 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies
2948 $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD}
2949 instantiates~$\Var{S}$ and creates the new assumption.
2951 by (dresolve_tac [CollectD] 1);
2953 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}
2954 {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}
2955 {\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}
2957 Forcing a contradiction between the two assumptions of subgoal~1
2958 completes the instantiation of~$S$. It is now the set $\{x. x\not\in
2959 f~x\}$, which is the standard diagonal construction.
2963 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
2964 {\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}
2966 The rest should be easy. To apply \tdx{CollectI} to the negated
2967 assumption, we employ \ttindex{swap_res_tac}:
2969 by (swap_res_tac [CollectI] 1);
2971 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
2972 {\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}
2976 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
2979 How much creativity is required? As it happens, Isabelle can prove this
2980 theorem automatically. The default classical set \texttt{claset()} contains rules
2981 for most of the constructs of \HOL's set theory. We must augment it with
2982 \tdx{equalityCE} to break up set equalities, and then apply best-first
2983 search. Depth-first search would diverge, but best-first search
2984 successfully navigates through the large search space.
2985 \index{search!best-first}
2989 {\out ?S ~: range f}
2990 {\out 1. ?S ~: range f}
2992 by (best_tac (claset() addSEs [equalityCE]) 1);
2994 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
2997 If you run this example interactively, make sure your current theory contains
2998 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
2999 Otherwise the default claset may not contain the rules for set theory.
3000 \index{higher-order logic|)}
3002 %%% Local Variables:
3004 %%% TeX-master: "logics"