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 book~\cite{andrews86} is a
9 full description of the original Church-style higher-order logic. Experience
10 with the {\sc hol} system has demonstrated that higher-order logic is widely
11 applicable in many areas of mathematics and computer science, not just
12 hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It
13 is weaker than ZF set theory but for most applications this does not matter.
14 If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
16 The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different
17 syntax. Ancient releases of Isabelle included still another version of~HOL,
18 with explicit type inference rules~\cite{paulson-COLOG}. This version no
19 longer exists, but \thydx{ZF} supports a similar style of reasoning.}
20 follows $\lambda$-calculus and functional programming. Function application
21 is curried. To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to
22 the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$. There is no
23 `apply' operator as in \thydx{ZF}. Note that $f(a,b)$ means ``$f$ applied to
24 the pair $(a,b)$'' in HOL. We write ordered pairs as $(a,b)$, not $\langle
27 HOL has a distinct feel, compared with ZF and CTT. It identifies object-level
28 types with meta-level types, taking advantage of Isabelle's built-in
29 type-checker. It identifies object-level functions with meta-level functions,
30 so it uses Isabelle's operations for abstraction and application.
32 These identifications allow Isabelle to support HOL particularly nicely, but
33 they also mean that HOL requires more sophistication from the user --- in
34 particular, an understanding of Isabelle's type system. Beginners should work
35 with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.
40 \it name &\it meta-type & \it description \\
41 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
42 \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\
43 \cdx{True} & $bool$ & tautology ($\top$) \\
44 \cdx{False} & $bool$ & absurdity ($\bot$) \\
45 \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
46 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
48 \subcaption{Constants}
51 \index{"@@{\tt\at} symbol}
52 \index{*"! symbol}\index{*"? symbol}
53 \index{*"?"! symbol}\index{*"E"X"! symbol}
54 \it symbol &\it name &\it meta-type & \it description \\
55 \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
56 Hilbert description ($\varepsilon$) \\
57 \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ &
58 universal quantifier ($\forall$) \\
59 \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
60 existential quantifier ($\exists$) \\
61 \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
62 unique existence ($\exists!$)\\
63 \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
70 \index{&@{\tt\&} symbol}
72 \index{*"-"-"> symbol}
73 \it symbol & \it meta-type & \it priority & \it description \\
74 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
75 Left 55 & composition ($\circ$) \\
76 \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
77 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
78 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
79 less than or equals ($\leq$)\\
80 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
81 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
82 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
85 \caption{Syntax of \texttt{HOL}} \label{hol-constants}
93 \[\begin{array}{rclcl}
94 term & = & \hbox{expression of class~$term$} \\
95 & | & "SOME~" id " . " formula
96 & | & "\at~" id " . " formula \\
98 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
100 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
101 & | & "LEAST"~ id " . " formula \\[2ex]
102 formula & = & \hbox{expression of type~$bool$} \\
103 & | & term " = " term \\
104 & | & term " \ttilde= " term \\
105 & | & term " < " term \\
106 & | & term " <= " term \\
107 & | & "\ttilde\ " formula \\
108 & | & formula " \& " formula \\
109 & | & formula " | " formula \\
110 & | & formula " --> " formula \\
111 & | & "ALL~" id~id^* " . " formula
112 & | & "!~~~" id~id^* " . " formula \\
113 & | & "EX~~" id~id^* " . " formula
114 & | & "?~~~" id~id^* " . " formula \\
115 & | & "EX!~" id~id^* " . " formula
116 & | & "?!~~" id~id^* " . " formula \\
119 \caption{Full grammar for HOL} \label{hol-grammar}
125 Figure~\ref{hol-constants} lists the constants (including infixes and
126 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
127 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
131 HOL has no if-and-only-if connective; logical equivalence is expressed using
132 equality. But equality has a high priority, as befitting a relation, while
133 if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$
134 abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$
135 to mean logical equivalence, enclose both operands in parentheses.
138 \subsection{Types and overloading}
139 The universal type class of higher-order terms is called~\cldx{term}.
140 By default, explicit type variables have class \cldx{term}. In
141 particular the equality symbol and quantifiers are polymorphic over
144 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
145 formulae are terms. The built-in type~\tydx{fun}, which constructs
146 function types, is overloaded with arity {\tt(term,\thinspace
147 term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
148 term} if $\sigma$ and~$\tau$ do, allowing quantification over
151 HOL allows new types to be declared as subsets of existing types;
152 see~{\S}\ref{sec:HOL:Types}. ML-like datatypes can also be declared; see
153 ~{\S}\ref{sec:HOL:datatype}.
155 Several syntactic type classes --- \cldx{plus}, \cldx{minus},
157 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+
158 symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol}
159 and \verb|^|.\index{^@\verb.^. symbol}
161 They are overloaded to denote the obvious arithmetic operations on types
162 \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the
163 exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also
164 done: the operator {\tt-} can denote set difference, while \verb|^| can
165 denote exponentiation of relations (iterated composition). Unary minus is
166 also written as~{\tt-} and is overloaded like its 2-place counterpart; it even
167 can stand for set complement.
169 The constant \cdx{0} is also overloaded. It serves as the zero element of
170 several types, of which the most important is \tdx{nat} (the natural
171 numbers). The type class \cldx{plus_ac0} comprises all types for which 0
172 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These
173 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also
174 multisets. The summation operator \cdx{setsum} is available for all types in
177 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
178 signatures. The relations $<$ and $\leq$ are polymorphic over this
179 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
180 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
181 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially
182 ordered with respect to~$\leq$. A further subclass \cldx{linorder} of
183 \cldx{order} axiomatizes linear orderings.
184 For details, see the file \texttt{Ord.thy}.
186 If you state a goal containing overloaded functions, you may need to include
187 type constraints. Type inference may otherwise make the goal more
188 polymorphic than you intended, with confusing results. For example, the
189 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type
190 $\alpha::\{ord,plus\}$, although you may have expected them to have some
191 numeric type, e.g. $nat$. Instead you should have stated the goal as
192 $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have
196 If resolution fails for no obvious reason, try setting
197 \ttindex{show_types} to \texttt{true}, causing Isabelle to display
198 types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as
199 well, causing Isabelle to display type classes and sorts.
201 \index{unification!incompleteness of}
202 Where function types are involved, Isabelle's unification code does not
203 guarantee to find instantiations for type variables automatically. Be
204 prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
205 possibly instantiating type variables. Setting
206 \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
207 omitted search paths during unification.\index{tracing!of unification}
213 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$
214 satisfying~$P$, if such exists. Since all terms in HOL denote something, a
215 description is always meaningful, but we do not know its value unless $P$
216 defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x.
217 P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.
219 Existential quantification is defined by
220 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
221 The unique existence quantifier, $\exists!x. P$, is defined in terms
222 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
223 quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates
224 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
225 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
229 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The
230 basic Isabelle/HOL binders have two notations. Apart from the usual
231 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also
232 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\
233 and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be
234 followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a
235 quantification. Both notations are accepted for input. The print mode
236 ``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by
237 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),
238 then~{\tt!}\ and~{\tt?}\ are displayed.
242 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
243 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
244 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see
245 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
246 choice operator, so \texttt{Least} is always meaningful, but may yield
247 nothing useful in case there is not a unique least element satisfying
248 $P$.\footnote{Class $ord$ does not require much of its instances, so
249 $\leq$ need not be a well-ordering, not even an order at all!}
251 \medskip All these binders have priority 10.
254 The low priority of binders means that they need to be enclosed in
255 parenthesis when they occur in the context of other operations. For example,
256 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
260 \subsection{The let and case constructions}
261 Local abbreviations can be introduced by a \texttt{let} construct whose
262 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
263 the constant~\cdx{Let}. It can be expanded by rewriting with its
264 definition, \tdx{Let_def}.
266 HOL also defines the basic syntax
267 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
268 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
269 and \sdx{of} are reserved words. Initially, this is mere syntax and has no
270 logical meaning. By declaring translations, you can cause instances of the
271 \texttt{case} construct to denote applications of particular case operators.
272 This is what happens automatically for each \texttt{datatype} definition
273 (see~{\S}\ref{sec:HOL:datatype}).
276 Both \texttt{if} and \texttt{case} constructs have as low a priority as
277 quantifiers, which requires additional enclosing parentheses in the context
278 of most other operations. For example, instead of $f~x = {\tt if\dots
279 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
283 \section{Rules of inference}
286 \begin{ttbox}\makeatother
287 \tdx{refl} t = (t::'a)
288 \tdx{subst} [| s = t; P s |] ==> P (t::'a)
289 \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)
290 \tdx{impI} (P ==> Q) ==> P-->Q
291 \tdx{mp} [| P-->Q; P |] ==> Q
292 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
293 \tdx{someI} P(x::'a) ==> P(@x. P x)
294 \tdx{True_or_False} (P=True) | (P=False)
296 \caption{The \texttt{HOL} rules} \label{hol-rules}
299 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
300 their~{\ML} names. Some of the rules deserve additional comments:
301 \begin{ttdescription}
302 \item[\tdx{ext}] expresses extensionality of functions.
303 \item[\tdx{iff}] asserts that logically equivalent formulae are
305 \item[\tdx{someI}] gives the defining property of the Hilbert
306 $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule
307 \tdx{some_equality} (see below) is often easier to use.
308 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
309 fact, the $\varepsilon$-operator already makes the logic classical, as
310 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
314 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
315 \begin{ttbox}\makeatother
316 \tdx{True_def} True == ((\%x::bool. x)=(\%x. x))
317 \tdx{All_def} All == (\%P. P = (\%x. True))
318 \tdx{Ex_def} Ex == (\%P. P(@x. P x))
319 \tdx{False_def} False == (!P. P)
320 \tdx{not_def} not == (\%P. P-->False)
321 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
322 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
323 \tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
325 \tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
326 \tdx{if_def} If P x y ==
327 (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
328 \tdx{Let_def} Let s f == f s
329 \tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
331 \caption{The \texttt{HOL} definitions} \label{hol-defs}
335 HOL follows standard practice in higher-order logic: only a few connectives
336 are taken as primitive, with the remainder defined obscurely
337 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
338 corresponding definitions \cite[page~270]{mgordon-hol} using
339 object-equality~({\tt=}), which is possible because equality in higher-order
340 logic may equate formulae and even functions over formulae. But theory~HOL,
341 like all other Isabelle theories, uses meta-equality~({\tt==}) for
344 The definitions above should never be expanded and are shown for completeness
345 only. Instead users should reason in terms of the derived rules shown below
346 or, better still, using high-level tactics
347 (see~{\S}\ref{sec:HOL:generic-packages}).
350 Some of the rules mention type variables; for example, \texttt{refl}
351 mentions the type variable~{\tt'a}. This allows you to instantiate
352 type variables explicitly by calling \texttt{res_inst_tac}.
357 \tdx{sym} s=t ==> t=s
358 \tdx{trans} [| r=s; s=t |] ==> r=t
359 \tdx{ssubst} [| t=s; P s |] ==> P t
360 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
361 \tdx{arg_cong} x = y ==> f x = f y
362 \tdx{fun_cong} f = g ==> f x = g x
363 \tdx{cong} [| f = g; x = y |] ==> f x = g y
364 \tdx{not_sym} t ~= s ==> s ~= t
365 \subcaption{Equality}
368 \tdx{FalseE} False ==> P
370 \tdx{conjI} [| P; Q |] ==> P&Q
371 \tdx{conjunct1} [| P&Q |] ==> P
372 \tdx{conjunct2} [| P&Q |] ==> Q
373 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
375 \tdx{disjI1} P ==> P|Q
376 \tdx{disjI2} Q ==> P|Q
377 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
379 \tdx{notI} (P ==> False) ==> ~ P
380 \tdx{notE} [| ~ P; P |] ==> R
381 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
382 \subcaption{Propositional logic}
384 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
385 \tdx{iffD1} [| P=Q; P |] ==> Q
386 \tdx{iffD2} [| P=Q; Q |] ==> P
387 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
389 %\tdx{eqTrueI} P ==> P=True
390 %\tdx{eqTrueE} P=True ==> P
391 \subcaption{Logical equivalence}
394 \caption{Derived rules for HOL} \label{hol-lemmas1}
399 \begin{ttbox}\makeatother
400 \tdx{allI} (!!x. P x) ==> !x. P x
401 \tdx{spec} !x. P x ==> P x
402 \tdx{allE} [| !x. P x; P x ==> R |] ==> R
403 \tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R
405 \tdx{exI} P x ==> ? x. P x
406 \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q
408 \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
409 \tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
412 \tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a
413 \subcaption{Quantifiers and descriptions}
415 \tdx{ccontr} (~P ==> False) ==> P
416 \tdx{classical} (~P ==> P) ==> P
417 \tdx{excluded_middle} ~P | P
419 \tdx{disjCI} (~Q ==> P) ==> P|Q
420 \tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x
421 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
422 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
423 \tdx{notnotD} ~~P ==> P
424 \tdx{swap} ~P ==> (~Q ==> P) ==> Q
425 \subcaption{Classical logic}
427 \tdx{if_P} P ==> (if P then x else y) = x
428 \tdx{if_not_P} ~ P ==> (if P then x else y) = y
429 \tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
430 \subcaption{Conditionals}
432 \caption{More derived rules} \label{hol-lemmas2}
435 Some derived rules are shown in Figures~\ref{hol-lemmas1}
436 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
437 for the logical connectives, as well as sequent-style elimination rules for
438 conjunctions, implications, and universal quantifiers.
440 Note the equality rules: \tdx{ssubst} performs substitution in
441 backward proofs, while \tdx{box_equals} supports reasoning by
442 simplifying both sides of an equation.
444 The following simple tactics are occasionally useful:
445 \begin{ttdescription}
446 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
447 repeatedly to remove all outermost universal quantifiers and implications
449 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on
450 $P$ for subgoal $i$: the latter is replaced by two identical subgoals with
451 the added assumptions $P$ and $\lnot P$, respectively.
452 \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then
453 \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining
454 from an induction hypothesis. As a generalization of \texttt{mp_tac},
455 if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and
456 $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)
457 then it replaces the universally quantified implication by $Q \vec{a}$.
458 It may instantiate unknowns. It fails if it can do nothing.
465 \it name &\it meta-type & \it description \\
466 \index{{}@\verb'{}' symbol}
467 \verb|{}| & $\alpha\,set$ & the empty set \\
468 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
469 & insertion of element \\
470 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
472 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
473 & intersection over a set\\
474 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
476 \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
477 &set of sets intersection \\
478 \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
479 &set of sets union \\
480 \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
482 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
483 & range of a function \\[1ex]
484 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
485 & bounded quantifiers
488 \subcaption{Constants}
491 \begin{tabular}{llrrr}
492 \it symbol &\it name &\it meta-type & \it priority & \it description \\
493 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
495 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
505 \begin{tabular}{rrrr}
506 \it symbol & \it meta-type & \it priority & \it description \\
507 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$
509 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
510 & Left 70 & intersection ($\int$) \\
511 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
512 & Left 65 & union ($\un$) \\
513 \tt: & $[\alpha ,\alpha\,set]\To bool$
514 & Left 50 & membership ($\in$) \\
515 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
516 & Left 50 & subset ($\subseteq$)
520 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
525 \begin{center} \tt\frenchspacing
528 \it external & \it internal & \it description \\
529 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\
530 {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
531 {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &
533 \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &
535 \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
537 \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ &
538 Ball $A$ $\lambda x.\ P[x]$ &
539 \rm bounded $\forall$ \\
540 \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ &
541 Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$
544 \subcaption{Translations}
547 \[\begin{array}{rclcl}
548 term & = & \hbox{other terms\ldots} \\
549 & | & "{\ttlbrace}{\ttrbrace}" \\
550 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
551 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
552 & | & term " `` " term \\
553 & | & term " Int " term \\
554 & | & term " Un " term \\
555 & | & "INT~~" id ":" term " . " term \\
556 & | & "UN~~~" id ":" term " . " term \\
557 & | & "INT~~" id~id^* " . " term \\
558 & | & "UN~~~" id~id^* " . " term \\[2ex]
559 formula & = & \hbox{other formulae\ldots} \\
560 & | & term " : " term \\
561 & | & term " \ttilde: " term \\
562 & | & term " <= " term \\
563 & | & "ALL " id ":" term " . " formula
564 & | & "!~" id ":" term " . " formula \\
565 & | & "EX~~" id ":" term " . " formula
566 & | & "?~" id ":" term " . " formula \\
569 \subcaption{Full Grammar}
570 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
574 \section{A formulation of set theory}
575 Historically, higher-order logic gives a foundation for Russell and
576 Whitehead's theory of classes. Let us use modern terminology and call them
577 {\bf sets}, but note that these sets are distinct from those of ZF set theory,
578 and behave more like ZF classes.
581 Sets are given by predicates over some type~$\sigma$. Types serve to
582 define universes for sets, but type-checking is still significant.
584 There is a universal set (for each type). Thus, sets have complements, and
585 may be defined by absolute comprehension.
587 Although sets may contain other sets as elements, the containing set must
588 have a more complex type.
590 Finite unions and intersections have the same behaviour in HOL as they do
591 in~ZF. In HOL the intersection of the empty set is well-defined, denoting the
592 universal set for the given type.
594 \subsection{Syntax of set theory}\index{*set type}
595 HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially
596 the same as $\alpha\To bool$. The new type is defined for clarity and to
597 avoid complications involving function types in unification. The isomorphisms
598 between the two types are declared explicitly. They are very natural:
599 \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
600 maps in the other direction (ignoring argument order).
602 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
603 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
604 constructs. Infix operators include union and intersection ($A\un B$
605 and $A\int B$), the subset and membership relations, and the image
606 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
609 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
610 the obvious manner using~\texttt{insert} and~$\{\}$:
612 \{a, b, c\} & \equiv &
613 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
616 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of
617 suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain
618 free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.
619 P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF;
620 the type of~$x$ implicitly restricts the comprehension.
622 The set theory defines two {\bf bounded quantifiers}:
624 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
625 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
627 The constants~\cdx{Ball} and~\cdx{Bex} are defined
628 accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
629 write\index{*"! symbol}\index{*"? symbol}
630 \index{*ALL symbol}\index{*EX symbol}
632 \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The
633 original notation of Gordon's {\sc hol} system is supported as well:
634 \texttt{!}\ and \texttt{?}.
636 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
637 $\bigcap@{x\in A}B[x]$, are written
638 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
639 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.
641 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
642 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
643 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous
644 union and intersection operators when $A$ is the universal set.
646 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
647 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
652 \begin{figure} \underscoreon
654 \tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a
655 \tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A
657 \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}
658 \tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B
659 \tdx{Ball_def} Ball A P == ! x. x:A --> P x
660 \tdx{Bex_def} Bex A P == ? x. x:A & P x
661 \tdx{subset_def} A <= B == ! x:A. x:B
662 \tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}
663 \tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}
664 \tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}
665 \tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace}
666 \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
667 \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
668 \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B
669 \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B
670 \tdx{Inter_def} Inter S == (INT x:S. x)
671 \tdx{Union_def} Union S == (UN x:S. x)
672 \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
673 \tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
674 \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
676 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
680 \begin{figure} \underscoreon
682 \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}
683 \tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a
684 \tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W
686 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
687 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
688 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
690 \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
691 \tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x
692 \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
693 \subcaption{Comprehension and Bounded quantifiers}
695 \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B
696 \tdx{subsetD} [| A <= B; c:A |] ==> c:B
697 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
699 \tdx{subset_refl} A <= A
700 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
702 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B
703 \tdx{equalityD1} A = B ==> A<=B
704 \tdx{equalityD2} A = B ==> B<=A
705 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
707 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
708 [| ~ c:A; ~ c:B |] ==> P
710 \subcaption{The subset and equality relations}
712 \caption{Derived rules for set theory} \label{hol-set1}
716 \begin{figure} \underscoreon
718 \tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
720 \tdx{insertI1} a : insert a B
721 \tdx{insertI2} a : B ==> a : insert b B
722 \tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
724 \tdx{ComplI} [| c:A ==> False |] ==> c : -A
725 \tdx{ComplD} [| c : -A |] ==> ~ c:A
727 \tdx{UnI1} c:A ==> c : A Un B
728 \tdx{UnI2} c:B ==> c : A Un B
729 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
730 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
732 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B
733 \tdx{IntD1} c : A Int B ==> c:A
734 \tdx{IntD2} c : A Int B ==> c:B
735 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
737 \tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
738 \tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
740 \tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
741 \tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
742 \tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
744 \tdx{UnionI} [| X:C; A:X |] ==> A : Union C
745 \tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
747 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
748 \tdx{InterD} [| A : Inter C; X:C |] ==> A:X
749 \tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
751 \tdx{PowI} A<=B ==> A: Pow B
752 \tdx{PowD} A: Pow B ==> A<=B
754 \tdx{imageI} [| x:A |] ==> f x : f``A
755 \tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
757 \tdx{rangeI} f x : range f
758 \tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
760 \caption{Further derived rules for set theory} \label{hol-set2}
764 \subsection{Axioms and rules of set theory}
765 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
766 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
767 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of
768 course, \hbox{\tt op :} also serves as the membership relation.
770 All the other axioms are definitions. They include the empty set, bounded
771 quantifiers, unions, intersections, complements and the subset relation.
772 They also include straightforward constructions on functions: image~({\tt``})
775 %The predicate \cdx{inj_on} is used for simulating type definitions.
776 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
777 %set~$A$, which specifies a subset of its domain type. In a type
778 %definition, $f$ is the abstraction function and $A$ is the set of valid
779 %representations; we should not expect $f$ to be injective outside of~$A$.
781 %\begin{figure} \underscoreon
783 %\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
784 %\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
787 % [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
790 %\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
791 %\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
793 %\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
794 %\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
795 %\tdx{injD} [| inj f; f x = f y |] ==> x=y
797 %\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
798 %\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
800 %\tdx{inj_on_inverseI}
801 % (!!x. x:A ==> g(f x) = x) ==> inj_on f A
802 %\tdx{inj_on_contraD}
803 % [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
805 %\caption{Derived rules involving functions} \label{hol-fun}
809 \begin{figure} \underscoreon
811 \tdx{Union_upper} B:A ==> B <= Union A
812 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
814 \tdx{Inter_lower} B:A ==> Inter A <= B
815 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
817 \tdx{Un_upper1} A <= A Un B
818 \tdx{Un_upper2} B <= A Un B
819 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
821 \tdx{Int_lower1} A Int B <= A
822 \tdx{Int_lower2} A Int B <= B
823 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
825 \caption{Derived rules involving subsets} \label{hol-subset}
829 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
831 \tdx{Int_absorb} A Int A = A
832 \tdx{Int_commute} A Int B = B Int A
833 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
834 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
836 \tdx{Un_absorb} A Un A = A
837 \tdx{Un_commute} A Un B = B Un A
838 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
839 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
841 \tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace}
842 \tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace}
843 \tdx{double_complement} -(-A) = A
844 \tdx{Compl_Un} -(A Un B) = (-A) Int (-B)
845 \tdx{Compl_Int} -(A Int B) = (-A) Un (-B)
847 \tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
848 \tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
849 %\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
851 \tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
852 \tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
853 %\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
855 \caption{Set equalities} \label{hol-equalities}
859 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
860 obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such
861 as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
862 reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
863 not strictly necessary but yield more natural proofs. Similarly,
864 \tdx{equalityCE} supports classical reasoning about extensionality, after the
865 fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs
866 pertaining to set theory.
868 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
869 Unions form least upper bounds; non-empty intersections form greatest lower
870 bounds. Reasoning directly about subsets often yields clearer proofs than
871 reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.
873 Figure~\ref{hol-equalities} presents many common set equalities. They
874 include commutative, associative and distributive laws involving unions,
875 intersections and complements. For a complete listing see the file {\tt
879 \texttt{Blast_tac} proves many set-theoretic theorems automatically.
880 Hence you seldom need to refer to the theorems above.
886 \it name &\it meta-type & \it description \\
887 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
888 & injective/surjective \\
889 \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
890 & injective over subset\\
891 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
897 \tdx{inj_def} inj f == ! x y. f x=f y --> x=y
898 \tdx{surj_def} surj f == ! y. ? x. y=f x
899 \tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
900 \tdx{inv_def} inv f == (\%y. @x. f(x)=y)
902 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
905 \subsection{Properties of functions}\nopagebreak
906 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
907 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
908 of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
909 rules. Reasoning about function composition (the operator~\sdx{o}) and the
910 predicate~\cdx{surj} is done simply by expanding the definitions.
912 There is also a large collection of monotonicity theorems for constructions
913 on sets in the file \texttt{HOL/mono.ML}.
916 \section{Generic packages}
917 \label{sec:HOL:generic-packages}
919 HOL instantiates most of Isabelle's generic packages, making available the
920 simplifier and the classical reasoner.
922 \subsection{Simplification and substitution}
924 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
925 (\texttt{simpset()}), which works for most purposes. A quite minimal
926 simplification set for higher-order logic is~\ttindexbold{HOL_ss};
927 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
928 also expresses logical equivalence, may be used for rewriting. See
929 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
930 simplification rules.
932 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
933 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
936 \begin{warn}\index{simplification!of conjunctions}%
937 Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
938 left part of a conjunction helps in simplifying the right part. This effect
939 is not available by default: it can be slow. It can be obtained by
940 including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
943 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%
944 By default only the condition of an \ttindex{if} is simplified but not the
945 \texttt{then} and \texttt{else} parts. Of course the latter are simplified
946 once the condition simplifies to \texttt{True} or \texttt{False}. To ensure
947 full simplification of all parts of a conditional you must remove
948 \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.
951 If the simplifier cannot use a certain rewrite rule --- either because
952 of nontermination or because its left-hand side is too flexible ---
953 then you might try \texttt{stac}:
954 \begin{ttdescription}
955 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
956 replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
957 $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking
958 may be necessary to select the desired ones.
960 If $thm$ is a conditional equality, the instantiated condition becomes an
961 additional (first) subgoal.
964 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
965 equality throughout a subgoal and its hypotheses. This tactic uses HOL's
966 general substitution rule.
968 \subsubsection{Case splitting}
969 \label{subsec:HOL:case:splitting}
971 HOL also provides convenient means for case splitting during rewriting. Goals
972 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
973 often require a case distinction on $b$. This is expressed by the theorem
976 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
977 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
980 For example, a simple instance of $(*)$ is
982 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
983 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
985 Because $(*)$ is too general as a rewrite rule for the simplifier (the
986 left-hand side is not a higher-order pattern in the sense of
987 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
988 {Chap.\ts\ref{chap:simplification}}), there is a special infix function
989 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
990 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
993 by(simp_tac (simpset() addsplits [split_if]) 1);
995 The effect is that after each round of simplification, one occurrence of
996 \texttt{if} is split acording to \texttt{split_if}, until all occurences of
997 \texttt{if} have been eliminated.
999 It turns out that using \texttt{split_if} is almost always the right thing to
1000 do. Hence \texttt{split_if} is already included in the default simpset. If
1001 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
1002 the inverse of \texttt{addsplits}:
1004 by(simp_tac (simpset() delsplits [split_if]) 1);
1007 In general, \texttt{addsplits} accepts rules of the form
1009 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
1011 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
1012 right form because internally the left-hand side is
1013 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
1014 are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}
1015 and~{\S}\ref{subsec:datatype:basics}).
1017 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
1018 imperative versions of \texttt{addsplits} and \texttt{delsplits}
1020 \ttindexbold{Addsplits}: thm list -> unit
1021 \ttindexbold{Delsplits}: thm list -> unit
1023 for adding splitting rules to, and deleting them from the current simpset.
1025 \subsection{Classical reasoning}
1027 HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
1028 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
1029 Fig.\ts\ref{hol-lemmas2} above.
1031 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and
1032 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
1033 for most purposes. Named clasets include \ttindexbold{prop_cs}, which
1034 includes the propositional rules, and \ttindexbold{HOL_cs}, which also
1035 includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of
1036 the classical rules,
1037 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1038 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
1041 \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
1043 \index{SVC decision procedure|(}
1045 The Stanford Validity Checker (SVC) is a tool that can check the validity of
1046 certain types of formulae. If it is installed on your machine, then
1047 Isabelle/HOL can be configured to call it through the tactic
1048 \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in
1049 linear arithmetic. Subexpressions that SVC cannot handle are automatically
1050 replaced by variables, so you can call the tactic on any subgoal. See the
1051 file \texttt{HOL/ex/svc_test.ML} for examples.
1053 svc_tac : int -> tactic
1054 Svc.trace : bool ref \hfill{\bf initially false}
1057 \begin{ttdescription}
1058 \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
1059 it into a formula recognized by~SVC\@. If it succeeds then the subgoal is
1060 removed. It fails if SVC is unable to prove the subgoal. It crashes with
1061 an error message if SVC appears not to be installed. Numeric variables may
1062 have types \texttt{nat}, \texttt{int} or \texttt{real}.
1064 \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
1065 to trace its operations: abstraction of the subgoal, translation to SVC
1066 syntax, SVC's response.
1069 Here is an example, with tracing turned on:
1072 {\out val it : bool = true}
1073 Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback
1074 \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c";
1077 {\out Subgoal abstracted to}
1078 {\out #3 * a <= #2 + #4 * b + #6 * c &}
1079 {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
1080 {\out #2 + #3 * b <= #2 * a + #6 * c}
1082 {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )}
1083 {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } }
1084 {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }}
1085 {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 }
1086 {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ }
1087 {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) }
1091 {\out #3 * a <= #2 + #4 * b + #6 * c &}
1092 {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
1093 {\out #2 + #3 * b <= #2 * a + #6 * c}
1099 Calling \ttindex{svc_tac} entails an above-average risk of
1100 unsoundness. Isabelle does not check SVC's result independently. Moreover,
1101 the tactic translates the submitted formula using code that lies outside
1102 Isabelle's inference core. Theorems that depend upon results proved using SVC
1103 (and other oracles) are displayed with the annotation \texttt{[!]} attached.
1104 You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
1105 theorem~$th$, as described in the \emph{Reference Manual}.
1108 To start, first download SVC from the Internet at URL
1110 http://agamemnon.stanford.edu/~levitt/vc/index.html
1112 and install it using the instructions supplied. SVC requires two environment
1114 \begin{ttdescription}
1115 \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
1116 distribution directory.
1118 \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
1121 You can set these environment variables either using the Unix shell or through
1122 an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if
1123 \texttt{SVC_HOME} is defined.
1125 \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren
1129 \index{SVC decision procedure|)}
1134 \section{Types}\label{sec:HOL:Types}
1135 This section describes HOL's basic predefined types ($\alpha \times \beta$,
1136 $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new
1137 types in general. The most important type construction, the
1138 \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.
1141 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1142 \label{subsec:prod-sum}
1144 \begin{figure}[htbp]
1146 \it symbol & \it meta-type & & \it description \\
1147 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
1148 & & ordered pairs $(a,b)$ \\
1149 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
1150 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
1151 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
1152 & & generalized projection\\
1154 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
1155 & general sum of sets
1157 \begin{ttbox}\makeatletter
1158 %\tdx{fst_def} fst p == @a. ? b. p = (a,b)
1159 %\tdx{snd_def} snd p == @b. ? a. p = (a,b)
1160 %\tdx{split_def} split c p == c (fst p) (snd p)
1161 \tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
1163 \tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
1164 \tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
1165 \tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
1167 \tdx{fst_conv} fst (a,b) = a
1168 \tdx{snd_conv} snd (a,b) = b
1169 \tdx{surjective_pairing} p = (fst p,snd p)
1171 \tdx{split} split c (a,b) = c a b
1172 \tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
1174 \tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
1176 \tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P
1179 \caption{Type $\alpha\times\beta$}\label{hol-prod}
1182 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
1183 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
1184 tuples are simulated by pairs nested to the right:
1186 \begin{tabular}{c|c}
1187 external & internal \\
1189 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
1191 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
1194 In addition, it is possible to use tuples
1195 as patterns in abstractions:
1197 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}
1199 Nested patterns are also supported. They are translated stepwise:
1201 \hbox{\tt\%($x$,$y$,$z$).\ $t$}
1202 & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\
1203 & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\
1204 & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}
1206 The reverse translation is performed upon printing.
1208 The translation between patterns and \texttt{split} is performed automatically
1209 by the parser and printer. Thus the internal and external form of a term
1210 may differ, which can affects proofs. For example the term {\tt
1211 (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
1212 default simpset) to rewrite to {\tt(b,a)}.
1214 In addition to explicit $\lambda$-abstractions, patterns can be used in any
1215 variable binding construct which is internally described by a
1216 $\lambda$-abstraction. Some important examples are
1218 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
1219 \item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
1220 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
1221 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
1222 \item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
1225 There is a simple tactic which supports reasoning about patterns:
1226 \begin{ttdescription}
1227 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
1228 {\tt!!}-quantified variables of product type by individual variables for
1229 each component. A simple example:
1231 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
1232 by(split_all_tac 1);
1233 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
1237 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
1238 which contains only a single element named {\tt()} with the property
1240 \tdx{unit_eq} u = ()
1244 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
1245 which associates to the right and has a lower priority than $*$: $\tau@1 +
1246 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
1248 The definition of products and sums in terms of existing types is not
1249 shown. The constructions are fairly standard and can be found in the
1250 respective theory files. Although the sum and product types are
1251 constructed manually for foundational reasons, they are represented as
1252 actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).
1253 Therefore, the theory \texttt{Datatype} should be used instead of
1254 \texttt{Sum} or \texttt{Prod}.
1258 \it symbol & \it meta-type & & \it description \\
1259 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
1260 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
1261 \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
1264 \begin{ttbox}\makeatletter
1265 \tdx{Inl_not_Inr} Inl a ~= Inr b
1267 \tdx{inj_Inl} inj Inl
1268 \tdx{inj_Inr} inj Inr
1270 \tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
1272 \tdx{sum_case_Inl} sum_case f g (Inl x) = f x
1273 \tdx{sum_case_Inr} sum_case f g (Inr x) = g x
1275 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
1276 \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
1277 (! y. s = Inr(y) --> R(g(y))))
1279 \caption{Type $\alpha+\beta$}\label{hol-sum}
1291 \it symbol & \it meta-type & \it priority & \it description \\
1292 \cdx{0} & $\alpha$ & & zero \\
1293 \cdx{Suc} & $nat \To nat$ & & successor function\\
1294 \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\
1295 \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\
1296 \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\
1297 \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\
1298 \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\
1299 \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction
1301 \subcaption{Constants and infixes}
1303 \begin{ttbox}\makeatother
1304 \tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n
1306 \tdx{Suc_not_Zero} Suc m ~= 0
1307 \tdx{inj_Suc} inj Suc
1308 \tdx{n_not_Suc_n} n~=Suc n
1309 \subcaption{Basic properties}
1311 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
1316 \begin{ttbox}\makeatother
1318 (Suc m)+n = Suc(m+n)
1327 \tdx{mod_less} m<n ==> m mod n = m
1328 \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
1330 \tdx{div_less} m<n ==> m div n = 0
1331 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
1333 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
1336 \subsection{The type of natural numbers, \textit{nat}}
1337 \index{nat@{\textit{nat}} type|(}
1339 The theory \thydx{NatDef} defines the natural numbers in a roundabout but
1340 traditional way. The axiom of infinity postulates a type~\tydx{ind} of
1341 individuals, which is non-empty and closed under an injective operation. The
1342 natural numbers are inductively generated by choosing an arbitrary individual
1343 for~0 and using the injective operation to take successors. This is a least
1344 fixedpoint construction. For details see the file \texttt{NatDef.thy}.
1346 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded
1347 functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},
1348 \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} builds
1349 on \texttt{NatDef} and shows that {\tt<=} is a linear order, so \tydx{nat} is
1350 also an instance of class \cldx{linorder}.
1352 Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines
1353 addition, multiplication and subtraction. Theory \thydx{Divides} defines
1354 division, remainder and the ``divides'' relation. The numerous theorems
1355 proved include commutative, associative, distributive, identity and
1356 cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The
1357 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
1358 \texttt{nat} are part of the default simpset.
1360 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
1361 see {\S}\ref{sec:HOL:recursive}. A simple example is addition.
1362 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1363 the standard convention.
1367 "Suc m + n = Suc (m + n)"
1369 There is also a \sdx{case}-construct
1372 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
1374 Note that Isabelle insists on precisely this format; you may not even change
1375 the order of the two cases.
1376 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
1377 \cdx{nat_rec}, which is available because \textit{nat} is represented as
1378 a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).
1380 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1381 %Recursion along this relation resembles primitive recursion, but is
1382 %stronger because we are in higher-order logic; using primitive recursion to
1383 %define a higher-order function, we can easily Ackermann's function, which
1384 %is not primitive recursive \cite[page~104]{thompson91}.
1385 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1386 %natural numbers are most easily expressed using recursion along~$<$.
1388 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
1389 in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived
1390 theorem \tdx{less_induct}:
1392 [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
1396 \subsection{Numerical types and numerical reasoning}
1398 The integers (type \tdx{int}) are also available in HOL, and the reals (type
1399 \tdx{real}) are available in the logic image \texttt{HOL-Real}. They support
1400 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
1401 multiplication (\texttt{*}), and much else. Type \tdx{int} provides the
1402 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real
1403 division and other operations. Both types belong to class \cldx{linorder}, so
1404 they inherit the relational operators and all the usual properties of linear
1405 orderings. For full details, please survey the theories in subdirectories
1406 \texttt{Integ} and \texttt{Real}.
1408 All three numeric types admit numerals of the form \texttt{\#$sd\ldots d$},
1409 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.
1410 Numerals are represented internally by a datatype for binary notation, which
1411 allows numerical calculations to be performed by rewriting. For example, the
1412 integer division of \texttt{\#54342339} by \texttt{\#3452} takes about five
1413 seconds. By default, the simplifier cancels like terms on the opposite sites
1414 of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for
1415 instance. The simplifier also collects like terms, replacing
1416 \texttt{x+y+x*\#3} by \texttt{\#4*x+y}.
1418 Sometimes numerals are not wanted, because for example \texttt{n+\#3} does not
1419 match a pattern of the form \texttt{Suc $k$}. You can re-arrange the form of
1420 an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such
1421 as \texttt{n+\#3 = Suc (Suc (Suc n))}. As an alternative, you can disable the
1422 fancier simplifications by using a basic simpset such as \texttt{HOL_ss}
1423 rather than the default one, \texttt{simpset()}.
1425 Reasoning about arithmetic inequalities can be tedious. Fortunately HOL
1426 provides a decision procedure for quantifier-free linear arithmetic (that is,
1427 addition and subtraction). The simplifier invokes a weak version of this
1428 decision procedure automatically. If this is not sufficent, you can invoke the
1429 full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary
1430 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
1431 min}, {\tt max} and numerical constants; other subterms are treated as
1432 atomic; subformulae not involving numerical types are ignored; quantified
1433 subformulae are ignored unless they are positive universal or negative
1434 existential. Note that the running time is exponential in the number of
1435 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
1436 distinctions. Note also that \texttt{arith_tac} is not complete: if
1437 divisibility plays a role, it may fail to prove a valid formula, for example
1438 $m+m \neq n+n+1$. Fortunately such examples are rare in practice.
1440 If \texttt{arith_tac} fails you, try to find relevant arithmetic results in
1441 the library. The theory \texttt{NatDef} contains theorems about {\tt<} and
1442 {\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
1443 \texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
1444 \texttt{div} and \texttt{mod}. Use \texttt{thms_containing} or the
1445 \texttt{find}-functions to locate them (see the {\em Reference Manual\/}).
1447 \index{nat@{\textit{nat}} type|)}
1451 \index{#@{\tt[]} symbol}
1452 \index{#@{\tt\#} symbol}
1453 \index{"@@{\tt\at} symbol}
1456 \it symbol & \it meta-type & \it priority & \it description \\
1457 \tt[] & $\alpha\,list$ & & empty list\\
1458 \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
1460 \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
1461 \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
1462 \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
1463 \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
1464 \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
1465 \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
1466 \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
1468 \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
1469 & & filter functional\\
1470 \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
1471 \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
1472 \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
1474 \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
1475 \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
1476 \cdx{length} & $\alpha\,list \To nat$ & & length \\
1477 \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
1478 \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
1479 take/drop a prefix \\
1482 $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
1485 \subcaption{Constants and infixes}
1487 \begin{center} \tt\frenchspacing
1488 \begin{tabular}{rrr}
1489 \it external & \it internal & \it description \\{}
1490 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1491 \rm finite list \\{}
1492 [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
1493 \rm list comprehension
1496 \subcaption{Translations}
1497 \caption{The theory \thydx{List}} \label{hol-list}
1502 \begin{ttbox}\makeatother
1512 (x#xs) @ ys = x # xs @ ys
1514 set [] = \ttlbrace\ttrbrace
1515 set (x#xs) = insert x (set xs)
1518 x mem (y#ys) = (if y=x then True else x mem ys)
1521 concat(x#xs) = x @ concat(xs)
1524 rev(x#xs) = rev(xs) @ [x]
1527 length(x#xs) = Suc(length(xs))
1530 xs!(Suc n) = (tl xs)!n
1532 \caption{Simple list processing functions}
1533 \label{fig:HOL:list-simps}
1537 \begin{ttbox}\makeatother
1539 map f (x#xs) = f x # map f xs
1542 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
1545 foldl f a (x#xs) = foldl f (f a x) xs
1548 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
1551 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
1554 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
1557 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
1559 \caption{Further list processing functions}
1560 \label{fig:HOL:list-simps2}
1564 \subsection{The type constructor for lists, \textit{list}}
1566 \index{list@{\textit{list}} type|(}
1568 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
1569 operations with their types and syntax. Type $\alpha \; list$ is
1570 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
1571 As a result the generic structural induction and case analysis tactics
1572 \texttt{induct\_tac} and \texttt{cases\_tac} also become available for
1573 lists. A \sdx{case} construct of the form
1575 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
1577 is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There
1578 is also a case splitting rule \tdx{split_list_case}
1581 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
1582 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
1583 ((e = \texttt{[]} \to P(a)) \land
1584 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
1587 which can be fed to \ttindex{addsplits} just like
1588 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
1590 \texttt{List} provides a basic library of list processing functions defined by
1591 primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations
1592 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.
1594 \index{list@{\textit{list}} type|)}
1597 \subsection{Introducing new types} \label{sec:typedef}
1599 The HOL-methodology dictates that all extensions to a theory should be
1600 \textbf{definitional}. The type definition mechanism that meets this
1601 criterion is \ttindex{typedef}. Note that \emph{type synonyms}, which are
1602 inherited from Pure and described elsewhere, are just syntactic abbreviations
1603 that have no logical meaning.
1606 Types in HOL must be non-empty; otherwise the quantifier rules would be
1607 unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
1609 A \bfindex{type definition} identifies the new type with a subset of
1610 an existing type. More precisely, the new type is defined by
1611 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
1612 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
1613 and the new type denotes this subset. New functions are defined that
1614 establish an isomorphism between the new type and the subset. If
1615 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
1616 then the type definition creates a type constructor
1617 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
1619 \begin{figure}[htbp]
1621 typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
1623 type : typevarlist name ( () | '(' infix ')' );
1625 witness : () | '(' id ')';
1627 \caption{Syntax of type definitions}
1628 \label{fig:HOL:typedef}
1631 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
1632 the definition of `typevarlist' and `infix' see
1633 \iflabelundefined{chap:classical}
1634 {the appendix of the {\em Reference Manual\/}}%
1635 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
1638 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
1639 optional infix annotation.
1640 \item[\it name:] an alphanumeric name $T$ for the type constructor
1641 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
1642 \item[\it set:] the representing subset $A$.
1643 \item[\it witness:] name of a theorem of the form $a:A$ proving
1644 non-emptiness. It can be omitted in case Isabelle manages to prove
1645 non-emptiness automatically.
1647 If all context conditions are met (no duplicate type variables in
1648 `typevarlist', no extra type variables in `set', and no free term variables
1649 in `set'), the following components are added to the theory:
1651 \item a type $ty :: (term,\dots,term)term$
1655 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
1656 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
1658 \item a definition and three axioms
1661 T{\tt_def} & T \equiv A \\
1662 {\tt Rep_}T & Rep_T\,x \in T \\
1663 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
1664 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y
1667 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
1668 and its inverse $Abs_T$.
1670 Below are two simple examples of HOL type definitions. Non-emptiness is
1671 proved automatically here.
1673 typedef unit = "{\ttlbrace}True{\ttrbrace}"
1676 ('a, 'b) "*" (infixr 20)
1677 = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
1680 Type definitions permit the introduction of abstract data types in a safe
1681 way, namely by providing models based on already existing types. Given some
1682 abstract axiomatic description $P$ of a type, this involves two steps:
1684 \item Find an appropriate type $\tau$ and subset $A$ which has the desired
1685 properties $P$, and make a type definition based on this representation.
1686 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
1688 You can now forget about the representation and work solely in terms of the
1689 abstract properties $P$.
1692 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
1693 declaring the type and its operations and by stating the desired axioms, you
1694 should make sure the type has a non-empty model. You must also have a clause
1697 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
1699 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
1700 class of all HOL types.
1706 At a first approximation, records are just a minor generalisation of tuples,
1707 where components may be addressed by labels instead of just position (think of
1708 {\ML}, for example). The version of records offered by Isabelle/HOL is
1709 slightly more advanced, though, supporting \emph{extensible record schemes}.
1710 This admits operations that are polymorphic with respect to record extension,
1711 yielding ``object-oriented'' effects like (single) inheritance. See also
1712 \cite{NaraschewskiW-TPHOLs98} for more details on object-oriented
1713 verification and record subtyping in HOL.
1718 Isabelle/HOL supports fixed and schematic records both at the level of terms
1719 and types. The concrete syntax is as follows:
1722 \begin{tabular}{l|l|l}
1723 & record terms & record types \\ \hline
1724 fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
1725 schematic & $\record{x = a\fs y = b\fs \more = m}$ &
1726 $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
1730 \noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
1732 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
1733 $y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$,
1734 assuming that $a \ty A$ and $b \ty B$.
1736 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
1737 $x$ and $y$ as before, but also possibly further fields as indicated by the
1738 ``$\more$'' notation (which is actually part of the syntax). The improper
1739 field ``$\more$'' of a record scheme is called the \emph{more part}.
1740 Logically it is just a free variable, which is occasionally referred to as
1741 \emph{row variable} in the literature. The more part of a record scheme may
1742 be instantiated by zero or more further components. For example, above scheme
1743 might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
1744 where $m'$ refers to a different more part. Fixed records are special
1745 instances of record schemes, where ``$\more$'' is properly terminated by the
1746 $() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an
1747 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
1751 There are two key features that make extensible records in a simply typed
1752 language like HOL feasible:
1754 \item the more part is internalised, as a free term or type variable,
1755 \item field names are externalised, they cannot be accessed within the logic
1756 as first-class values.
1761 In Isabelle/HOL record types have to be defined explicitly, fixing their field
1762 names and types, and their (optional) parent record (see
1763 {\S}\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
1764 syntax, while obeying the canonical order of fields as given by their
1765 declaration. The record package also provides several operations like
1766 selectors and updates (see {\S}\ref{sec:HOL:record-ops}), together with
1767 characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
1769 There is an example theory demonstrating most basic aspects of extensible
1770 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
1773 \subsection{Defining records}\label{sec:HOL:record-def}
1775 The theory syntax for record type definitions is shown in
1776 Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see
1777 \iflabelundefined{chap:classical}
1778 {the appendix of the {\em Reference Manual\/}}%
1779 {Appendix~\ref{app:TheorySyntax}}.
1781 \begin{figure}[htbp]
1783 record : 'record' typevarlist name '=' parent (field +);
1785 parent : ( () | type '+');
1786 field : name '::' type;
1788 \caption{Syntax of record type definitions}
1789 \label{fig:HOL:record}
1792 A general \ttindex{record} specification is of the following form:
1794 \mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
1795 (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
1797 where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
1798 $\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
1799 Type constructor $t$ has to be new, while $s$ has to specify an existing
1800 record type. Furthermore, the $\vec c@l$ have to be distinct field names.
1801 There has to be at least one field.
1803 In principle, field names may never be shared with other records. This is no
1804 actual restriction in practice, since $\vec c@l$ are internally declared
1805 within a separate name space qualified by the name $t$ of the record.
1809 Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
1810 extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
1811 \vec\sigma@l$. The parent record specification is optional, by omitting it
1812 $t$ becomes a \emph{root record}. The hierarchy of all records declared
1813 within a theory forms a forest structure, i.e.\ a set of trees, where any of
1814 these is rooted by some root record.
1816 For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
1817 fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
1818 \zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
1819 \vec\sigma@l\fs \more \ty \zeta}$.
1823 The following simple example defines a root record type $point$ with fields $x
1824 \ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
1825 an additional $colour$ component.
1832 record cpoint = point +
1837 \subsection{Record operations}\label{sec:HOL:record-ops}
1839 Any record definition of the form presented above produces certain standard
1840 operations. Selectors and updates are provided for any field, including the
1841 improper one ``$more$''. There are also cumulative record constructor
1844 To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
1845 is a root record with fields $\vec c@l \ty \vec\sigma@l$.
1849 \textbf{Selectors} and \textbf{updates} are available for any field (including
1850 ``$more$'') as follows:
1851 \begin{matharray}{lll}
1852 c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
1853 c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
1854 \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1857 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
1858 term $x_update \, a \, r$. Repeated updates are also supported: $r \,
1859 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
1860 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of
1861 postfix notation the order of fields shown here is reverse than in the actual
1862 term. This might lead to confusion in conjunction with proof tools like
1865 Since repeated updates are just function applications, fields may be freely
1866 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
1867 is concerned. Thus commutativity of updates can be proven within the logic
1868 for any two fields, but not as a general theorem: fields are not first-class
1873 \textbf{Make} operations provide cumulative record constructor functions:
1874 \begin{matharray}{lll}
1875 make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
1876 make_scheme & \ty & \vec\sigma@l \To
1877 \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
1880 These functions are curried. The corresponding definitions in terms of actual
1881 record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$
1882 rewrites to $\record{x = a\fs y = b}$.
1886 Any of above selector, update and make operations are declared within a local
1887 name space prefixed by the name $t$ of the record. In case that different
1888 records share base names of fields, one has to qualify names explicitly (e.g.\
1889 $t\dtt c@i_update$). This is recommended especially for operations like
1890 $make$ or $update_more$ that always have the same base name. Just use $t\dtt
1891 make$ etc.\ to avoid confusion.
1895 We reconsider the case of non-root records, which are derived of some parent
1896 record. In general, the latter may depend on another parent as well,
1897 resulting in a list of \emph{ancestor records}. Appending the lists of fields
1898 of all ancestors results in a certain field prefix. The record package
1899 automatically takes care of this by lifting operations over this context of
1900 ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
1901 $\vec d@k \ty \vec\rho@k$, selectors will get the following types:
1902 \begin{matharray}{lll}
1903 c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1907 Update and make operations are analogous.
1910 \subsection{Proof tools}\label{sec:HOL:record-thms}
1912 The record package provides the following proof rules for any record type $t$.
1915 \item Standard conversions (selectors or updates applied to record constructor
1916 terms, make function definitions) are part of the standard simpset (via
1919 \item Selectors applied to updated records are automatically reduced by
1920 simplification procedure \ttindex{record_simproc}, which is part of the
1923 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
1924 \conj y=y'$ are made part of the standard simpset and claset (via
1927 \item A tactic for record field splitting (\ttindex{record_split_tac}) may be
1928 made part of the claset (via \texttt{addSWrapper}). This tactic is based on
1929 rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for
1933 The first two kinds of rules are stored within the theory as $t\dtt simps$ and
1934 $t\dtt iffs$, respectively. In some situations it might be appropriate to
1935 expand the definitions of updates: $t\dtt update_defs$. Note that these names
1936 are \emph{not} bound at the {\ML} level.
1940 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
1941 concerning records. The basic idea is to make \ttindex{record_split_tac}
1942 expand quantified record variables and then simplify by the conversion rules.
1943 By using a combination of the simplifier and classical prover together with
1944 the default simpset and claset, record problems should be solved with a single
1945 stroke of \texttt{Auto_tac} or \texttt{Force_tac}. Most of the time, plain
1946 \texttt{Simp_tac} should be sufficient, though.
1949 \section{Datatype definitions}
1950 \label{sec:HOL:datatype}
1953 Inductive datatypes, similar to those of \ML, frequently appear in
1954 applications of Isabelle/HOL. In principle, such types could be defined by
1955 hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too
1956 tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
1957 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an
1958 appropriate \texttt{typedef} based on a least fixed-point construction, and
1959 proves freeness theorems and induction rules, as well as theorems for
1960 recursion and case combinators. The user just has to give a simple
1961 specification of new inductive types using a notation similar to {\ML} or
1964 The current datatype package can handle both mutual and indirect recursion.
1965 It also offers to represent existing types as datatypes giving the advantage
1966 of a more uniform view on standard theories.
1970 \label{subsec:datatype:basics}
1972 A general \texttt{datatype} definition is of the following form:
1975 \mathtt{datatype} & (\vec{\alpha})t@1 & = &
1976 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~
1977 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\
1979 \mathtt{and} & (\vec{\alpha})t@n & = &
1980 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~
1981 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}
1984 where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,
1985 $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em
1986 admissible} types containing at most the type variables $\alpha@1, \ldots,
1987 \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em
1988 admissible} if and only if
1990 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
1991 newly defined type constructors $t@1,\ldots,t@n$, or
1992 \item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or
1993 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
1994 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1995 are admissible types.
1996 \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible
1997 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
1998 types are {\em strictly positive})
2000 If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$
2003 (\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t'
2005 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
2006 example of a datatype is the type \texttt{list}, which can be defined by
2008 datatype 'a list = Nil
2011 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
2012 by the mutually recursive datatype definition
2014 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
2015 | Sum ('a aexp) ('a aexp)
2016 | Diff ('a aexp) ('a aexp)
2019 and 'a bexp = Less ('a aexp) ('a aexp)
2020 | And ('a bexp) ('a bexp)
2021 | Or ('a bexp) ('a bexp)
2023 The datatype \texttt{term}, which is defined by
2025 datatype ('a, 'b) term = Var 'a
2026 | App 'b ((('a, 'b) term) list)
2028 is an example for a datatype with nested recursion. Using nested recursion
2029 involving function spaces, we may also define infinitely branching datatypes, e.g.
2031 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
2036 Types in HOL must be non-empty. Each of the new datatypes
2037 $(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a
2038 constructor $C^j@i$ with the following property: for all argument types
2039 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype
2040 $(\vec{\alpha})t@{j'}$ is non-empty.
2042 If there are no nested occurrences of the newly defined datatypes, obviously
2043 at least one of the newly defined datatypes $(\vec{\alpha})t@j$
2044 must have a constructor $C^j@i$ without recursive arguments, a \emph{base
2045 case}, to ensure that the new types are non-empty. If there are nested
2046 occurrences, a datatype can even be non-empty without having a base case
2047 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
2048 list)} is non-empty as well.
2051 \subsubsection{Freeness of the constructors}
2053 The datatype constructors are automatically defined as functions of their
2055 \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
2056 These functions have certain {\em freeness} properties. They construct
2059 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
2060 \mbox{for all}~ i \neq i'.
2062 The constructor functions are injective:
2064 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
2065 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
2067 Since the number of distinctness inequalities is quadratic in the number of
2068 constructors, the datatype package avoids proving them separately if there are
2069 too many constructors. Instead, specific inequalities are proved by a suitable
2070 simplification procedure on demand.\footnote{This procedure, which is already part
2071 of the default simpset, may be referred to by the ML identifier
2072 \texttt{DatatypePackage.distinct_simproc}.}
2074 \subsubsection{Structural induction}
2076 The datatype package also provides structural induction rules. For
2077 datatypes without nested recursion, this is of the following form:
2079 \infer{P@1~x@1 \land \dots \land P@n~x@n}
2081 \Forall x@1 \dots x@{m^1@1}.
2082 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
2083 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &
2084 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\
2086 \Forall x@1 \dots x@{m^1@{k@1}}.
2087 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;
2088 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &
2089 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\
2091 \Forall x@1 \dots x@{m^n@1}.
2092 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;
2093 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &
2094 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\
2096 \Forall x@1 \dots x@{m^n@{k@n}}.
2097 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots
2098 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &
2099 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)
2106 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
2107 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
2108 && \left\{(i',i'')~\left|~
2109 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land
2110 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
2113 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
2115 For datatypes with nested recursion, such as the \texttt{term} example from
2116 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
2119 datatype ('a,'b) term = Var 'a
2120 | App 'b ((('a, 'b) term) list)
2122 to an equivalent definition without nesting:
2124 datatype ('a,'b) term = Var
2125 | App 'b (('a, 'b) term_list)
2126 and ('a,'b) term_list = Nil'
2127 | Cons' (('a,'b) term) (('a,'b) term_list)
2129 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
2130 Nil'} and \texttt{Cons'} are not really introduced. One can directly work with
2131 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
2132 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
2133 \texttt{term} gets the form
2135 \infer{P@1~x@1 \land P@2~x@2}
2137 \Forall x.~P@1~(\mathtt{Var}~x) \\
2138 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
2140 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
2143 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
2144 and one for the type \texttt{(('a, 'b) term) list}.
2146 For a datatype with function types such as \texttt{'a tree}, the induction rule
2150 {\Forall a.~P~(\mathtt{Atom}~a) &
2151 \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}
2154 \medskip In principle, inductive types are already fully determined by
2155 freeness and structural induction. For convenience in applications,
2156 the following derived constructions are automatically provided for any
2159 \subsubsection{The \sdx{case} construct}
2161 The type comes with an \ML-like \texttt{case}-construct:
2164 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
2166 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}
2169 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
2170 {\S}\ref{subsec:prod-sum}.
2172 All constructors must be present, their order is fixed, and nested patterns
2173 are not supported (with the exception of tuples). Violating this
2174 restriction results in strange error messages.
2177 To perform case distinction on a goal containing a \texttt{case}-construct,
2178 the theorem $t@j.$\texttt{split} is provided:
2180 \begin{array}{@{}rcl@{}}
2181 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&
2182 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to
2183 P(f@1~x@1\dots x@{m^j@1})) \\
2184 &&\!\!\! ~\land~ \dots ~\land \\
2185 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to
2186 P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))
2189 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
2190 This theorem can be added to a simpset via \ttindex{addsplits}
2191 (see~{\S}\ref{subsec:HOL:case:splitting}).
2193 \begin{warn}\index{simplification!of \texttt{case}}%
2194 By default only the selector expression ($e$ above) in a
2195 \texttt{case}-construct is simplified, in analogy with \texttt{if} (see
2196 page~\pageref{if-simp}). Only if that reduces to a constructor is one of
2197 the arms of the \texttt{case}-construct exposed and simplified. To ensure
2198 full simplification of all parts of a \texttt{case}-construct for datatype
2199 $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
2200 example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
2203 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
2205 Theory \texttt{Arith} declares a generic function \texttt{size} of type
2206 $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
2207 by overloading according to the following scheme:
2208 %%% FIXME: This formula is too big and is completely unreadable
2210 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
2213 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\
2214 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &
2215 \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
2216 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}
2220 where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
2221 size of a leaf is 0 and the size of a node is the sum of the sizes of its
2224 \subsection{Defining datatypes}
2226 The theory syntax for datatype definitions is shown in
2227 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
2228 definition has to obey the rules stated in the previous section. As a result
2229 the theory is extended with the new types, the constructors, and the theorems
2230 listed in the previous section.
2234 datatype : 'datatype' typedecls;
2236 typedecls: ( newtype '=' (cons + '|') ) + 'and'
2238 newtype : typevarlist id ( () | '(' infix ')' )
2240 cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
2242 argtype : id | tid | ('(' typevarlist id ')')
2245 \caption{Syntax of datatype declarations}
2246 \label{datatype-grammar}
2249 Most of the theorems about datatypes become part of the default simpset and
2250 you never need to see them again because the simplifier applies them
2251 automatically. Only induction or case distinction are usually invoked by hand.
2252 \begin{ttdescription}
2253 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
2254 applies structural induction on variable $x$ to subgoal $i$, provided the
2255 type of $x$ is a datatype.
2256 \item[\texttt{induct_tac}
2257 {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous
2258 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This
2259 is the canonical way to prove properties of mutually recursive datatypes
2260 such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as
2263 In some cases, induction is overkill and a case distinction over all
2264 constructors of the datatype suffices.
2265 \begin{ttdescription}
2266 \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]
2267 performs a case analysis for the term $u$ whose type must be a datatype.
2268 If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal
2269 $i$ is replaced by $k@j$ new subgoals which contain the additional
2270 assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$.
2273 Note that induction is only allowed on free variables that should not occur
2274 among the premises of the subgoal. Case distinction applies to arbitrary terms.
2279 For the technically minded, we exhibit some more details. Processing the
2280 theory file produces an \ML\ structure which, in addition to the usual
2281 components, contains a structure named $t$ for each datatype $t$ defined in
2282 the file. Each structure $t$ contains the following elements:
2284 val distinct : thm list
2285 val inject : thm list
2288 val cases : thm list
2293 val simps : thm list
2295 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}
2296 and \texttt{split} contain the theorems
2297 described above. For user convenience, \texttt{distinct} contains
2298 inequalities in both directions. The reduction rules of the {\tt
2299 case}-construct are in \texttt{cases}. All theorems from {\tt
2300 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
2301 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
2302 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
2305 \subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}
2307 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
2308 +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
2309 but by more primitive means using \texttt{typedef}. To be able to use the
2310 tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by
2311 primitive recursion on these types, such types may be represented as actual
2312 datatypes. This is done by specifying an induction rule, as well as theorems
2313 stating the distinctness and injectivity of constructors in a {\tt
2314 rep_datatype} section. For type \texttt{nat} this works as follows:
2317 distinct Suc_not_Zero, Zero_not_Suc
2321 The datatype package automatically derives additional theorems for recursion
2322 and case combinators from these rules. Any of the basic HOL types mentioned
2323 above are represented as datatypes. Try an induction on \texttt{bool}
2327 \subsection{Examples}
2329 \subsubsection{The datatype $\alpha~mylist$}
2331 We want to define a type $\alpha~mylist$. To do this we have to build a new
2332 theory that contains the type definition. We start from the theory
2333 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
2334 \texttt{List} theory of Isabelle/HOL.
2337 datatype 'a mylist = Nil | Cons 'a ('a mylist)
2340 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To
2341 ease the induction applied below, we state the goal with $x$ quantified at the
2342 object-level. This will be stripped later using \ttindex{qed_spec_mp}.
2344 Goal "!x. Cons x xs ~= xs";
2346 {\out ! x. Cons x xs ~= xs}
2347 {\out 1. ! x. Cons x xs ~= xs}
2349 This can be proved by the structural induction tactic:
2351 by (induct_tac "xs" 1);
2353 {\out ! x. Cons x xs ~= xs}
2354 {\out 1. ! x. Cons x Nil ~= Nil}
2355 {\out 2. !!a mylist.}
2356 {\out ! x. Cons x mylist ~= mylist ==>}
2357 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
2359 The first subgoal can be proved using the simplifier. Isabelle/HOL has
2360 already added the freeness properties of lists to the default simplification
2365 {\out ! x. Cons x xs ~= xs}
2366 {\out 1. !!a mylist.}
2367 {\out ! x. Cons x mylist ~= mylist ==>}
2368 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
2370 Similarly, we prove the remaining goal.
2372 by (Asm_simp_tac 1);
2374 {\out ! x. Cons x xs ~= xs}
2377 qed_spec_mp "not_Cons_self";
2378 {\out val not_Cons_self = "Cons x xs ~= xs" : thm}
2380 Because both subgoals could have been proved by \texttt{Asm_simp_tac}
2381 we could have done that in one step:
2383 by (ALLGOALS Asm_simp_tac);
2387 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
2389 In this example we define the type $\alpha~mylist$ again but this time
2390 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix
2391 notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix
2392 annotations after the constructor declarations as follows:
2395 datatype 'a mylist =
2397 Cons 'a ('a mylist) (infixr "#" 70)
2400 Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
2403 \subsubsection{A datatype for weekdays}
2405 This example shows a datatype that consists of 7 constructors:
2408 datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
2411 Because there are more than 6 constructors, inequality is expressed via a function
2412 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
2413 contained among the distinctness theorems, but the simplifier can
2414 prove it thanks to rewrite rules inherited from theory \texttt{Arith}:
2419 You need not derive such inequalities explicitly: the simplifier will dispose
2420 of them automatically.
2424 \section{Recursive function definitions}\label{sec:HOL:recursive}
2425 \index{recursive functions|see{recursion}}
2427 Isabelle/HOL provides two main mechanisms of defining recursive functions.
2429 \item \textbf{Primitive recursion} is available only for datatypes, and it is
2430 somewhat restrictive. Recursive calls are only allowed on the argument's
2431 immediate constituents. On the other hand, it is the form of recursion most
2432 often wanted, and it is easy to use.
2434 \item \textbf{Well-founded recursion} requires that you supply a well-founded
2435 relation that governs the recursion. Recursive calls are only allowed if
2436 they make the argument decrease under the relation. Complicated recursion
2437 forms, such as nested recursion, can be dealt with. Termination can even be
2438 proved at a later time, though having unsolved termination conditions around
2439 can make work difficult.%
2440 \footnote{This facility is based on Konrad Slind's TFL
2441 package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
2442 and assisting with its installation.}
2445 Following good HOL tradition, these declarations do not assert arbitrary
2446 axioms. Instead, they define the function using a recursion operator. Both
2447 HOL and ZF derive the theory of well-founded recursion from first
2448 principles~\cite{paulson-set-II}. Primitive recursion over some datatype
2449 relies on the recursion operator provided by the datatype package. With
2450 either form of function definition, Isabelle proves the desired recursion
2451 equations as theorems.
2454 \subsection{Primitive recursive functions}
2455 \label{sec:HOL:primrec}
2456 \index{recursion!primitive|(}
2459 Datatypes come with a uniform way of defining functions, {\bf primitive
2460 recursion}. In principle, one could introduce primitive recursive functions
2461 by asserting their reduction rules as new axioms, but this is not recommended:
2462 \begin{ttbox}\slshape
2464 consts app :: ['a list, 'a list] => 'a list
2466 app_Nil "app [] ys = ys"
2467 app_Cons "app (x#xs) ys = x#app xs ys"
2470 Asserting axioms brings the danger of accidentally asserting nonsense, as
2471 in \verb$app [] ys = us$.
2473 The \ttindex{primrec} declaration is a safe means of defining primitive
2474 recursive functions on datatypes:
2477 consts app :: ['a list, 'a list] => 'a list
2480 "app (x#xs) ys = x#app xs ys"
2483 Isabelle will now check that the two rules do indeed form a primitive
2484 recursive definition. For example
2489 is rejected with an error message ``\texttt{Extra variables on rhs}''.
2493 The general form of a primitive recursive definition is
2496 {\it reduction rules}
2498 where \textit{reduction rules} specify one or more equations of the form
2499 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
2500 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
2501 contains only the free variables on the left-hand side, and all recursive
2502 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
2503 must be at most one reduction rule for each constructor. The order is
2504 immaterial. For missing constructors, the function is defined to return a
2507 If you would like to refer to some rule by name, then you must prefix
2508 the rule with an identifier. These identifiers, like those in the
2509 \texttt{rules} section of a theory, will be visible at the \ML\ level.
2511 The primitive recursive function can have infix or mixfix syntax:
2512 \begin{ttbox}\underscoreon
2513 consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
2516 "(x#xs) @ ys = x#(xs @ ys)"
2519 The reduction rules become part of the default simpset, which
2520 leads to short proof scripts:
2521 \begin{ttbox}\underscoreon
2522 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
2523 by (induct\_tac "xs" 1);
2524 by (ALLGOALS Asm\_simp\_tac);
2527 \subsubsection{Example: Evaluation of expressions}
2528 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
2529 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
2530 {\S}\ref{subsec:datatype:basics}:
2533 evala :: "['a => nat, 'a aexp] => nat"
2534 evalb :: "['a => nat, 'a bexp] => bool"
2537 "evala env (If_then_else b a1 a2) =
2538 (if evalb env b then evala env a1 else evala env a2)"
2539 "evala env (Sum a1 a2) = evala env a1 + evala env a2"
2540 "evala env (Diff a1 a2) = evala env a1 - evala env a2"
2541 "evala env (Var v) = env v"
2542 "evala env (Num n) = n"
2544 "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
2545 "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
2546 "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"
2548 Since the value of an expression depends on the value of its variables,
2549 the functions \texttt{evala} and \texttt{evalb} take an additional
2550 parameter, an {\em environment} of type \texttt{'a => nat}, which maps
2551 variables to their values.
2553 Similarly, we may define substitution functions \texttt{substa}
2554 and \texttt{substb} for expressions: The mapping \texttt{f} of type
2555 \texttt{'a => 'a aexp} given as a parameter is lifted canonically
2556 on the types \texttt{'a aexp} and \texttt{'a bexp}:
2559 substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"
2560 substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"
2563 "substa f (If_then_else b a1 a2) =
2564 If_then_else (substb f b) (substa f a1) (substa f a2)"
2565 "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
2566 "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
2567 "substa f (Var v) = f v"
2568 "substa f (Num n) = Num n"
2570 "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
2571 "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
2572 "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"
2574 In textbooks about semantics one often finds {\em substitution theorems},
2575 which express the relationship between substitution and evaluation. For
2576 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
2577 induction, followed by simplification:
2580 "evala env (substa (Var(v := a')) a) =
2581 evala (env(v := evala env a')) a &
2582 evalb env (substb (Var(v := a')) b) =
2583 evalb (env(v := evala env a')) b";
2584 by (induct_tac "a b" 1);
2585 by (ALLGOALS Asm_full_simp_tac);
2588 \subsubsection{Example: A substitution function for terms}
2589 Functions on datatypes with nested recursion, such as the type
2590 \texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
2591 also defined by mutual primitive recursion. A substitution
2592 function \texttt{subst_term} on type \texttt{term}, similar to the functions
2593 \texttt{substa} and \texttt{substb} described above, can
2594 be defined as follows:
2597 subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"
2599 "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"
2602 "subst_term f (Var a) = f a"
2603 "subst_term f (App b ts) = App b (subst_term_list f ts)"
2605 "subst_term_list f [] = []"
2606 "subst_term_list f (t # ts) =
2607 subst_term f t # subst_term_list f ts"
2609 The recursion scheme follows the structure of the unfolded definition of type
2610 \texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
2611 this substitution function, mutual induction is needed:
2614 "(subst_term ((subst_term f1) o f2) t) =
2615 (subst_term f1 (subst_term f2 t)) &
2616 (subst_term_list ((subst_term f1) o f2) ts) =
2617 (subst_term_list f1 (subst_term_list f2 ts))";
2618 by (induct_tac "t ts" 1);
2619 by (ALLGOALS Asm_full_simp_tac);
2622 \subsubsection{Example: A map function for infinitely branching trees}
2623 Defining functions on infinitely branching datatypes by primitive
2624 recursion is just as easy. For example, we can define a function
2625 \texttt{map_tree} on \texttt{'a tree} as follows:
2628 map_tree :: "('a => 'b) => 'a tree => 'b tree"
2631 "map_tree f (Atom a) = Atom (f a)"
2632 "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"
2634 Note that all occurrences of functions such as \texttt{ts} in the
2635 \texttt{primrec} clauses must be applied to an argument. In particular,
2636 \texttt{map_tree f o ts} is not allowed.
2638 \index{recursion!primitive|)}
2642 \subsection{General recursive functions}
2643 \label{sec:HOL:recdef}
2644 \index{recursion!general|(}
2647 Using \texttt{recdef}, you can declare functions involving nested recursion
2648 and pattern-matching. Recursion need not involve datatypes and there are few
2649 syntactic restrictions. Termination is proved by showing that each recursive
2650 call makes the argument smaller in a suitable sense, which you specify by
2651 supplying a well-founded relation.
2653 Here is a simple example, the Fibonacci function. The first line declares
2654 \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on
2655 the natural numbers). Pattern-matching is used here: \texttt{1} is a
2656 macro for \texttt{Suc~0}.
2658 consts fib :: "nat => nat"
2659 recdef fib "less_than"
2662 "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
2665 With \texttt{recdef}, function definitions may be incomplete, and patterns may
2666 overlap, as in functional programming. The \texttt{recdef} package
2667 disambiguates overlapping patterns by taking the order of rules into account.
2668 For missing patterns, the function is defined to return a default value.
2670 %For example, here is a declaration of the list function \cdx{hd}:
2672 %consts hd :: 'a list => 'a
2676 %Because this function is not recursive, we may supply the empty well-founded
2679 The well-founded relation defines a notion of ``smaller'' for the function's
2680 argument type. The relation $\prec$ is \textbf{well-founded} provided it
2681 admits no infinitely decreasing chains
2682 \[ \cdots\prec x@n\prec\cdots\prec x@1. \]
2683 If the function's argument has type~$\tau$, then $\prec$ has to be a relation
2684 over~$\tau$: it must have type $(\tau\times\tau)set$.
2686 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
2687 of operators for building well-founded relations. The package recognises
2688 these operators and automatically proves that the constructed relation is
2689 well-founded. Here are those operators, in order of importance:
2691 \item \texttt{less_than} is ``less than'' on the natural numbers.
2692 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.
2694 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
2695 relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if
2697 Typically, $f$ takes the recursive function's arguments (as a tuple) and
2698 returns a result expressed in terms of the function \texttt{size}. It is
2699 called a \textbf{measure function}. Recall that \texttt{size} is overloaded
2700 and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
2702 \item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of
2703 \texttt{measure}. It specifies a relation such that $x\prec y$ if and only
2705 is less than $f(y)$ according to~$R$, which must itself be a well-founded
2708 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It
2709 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only
2711 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$
2712 is less than $y@2$ according to~$R@2$.
2714 \item \texttt{finite_psubset} is the proper subset relation on finite sets.
2717 We can use \texttt{measure} to declare Euclid's algorithm for the greatest
2718 common divisor. The measure function, $\lambda(m,n). n$, specifies that the
2719 recursion terminates because argument~$n$ decreases.
2721 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
2722 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2725 The general form of a well-founded recursive definition is
2727 recdef {\it function} {\it rel}
2728 congs {\it congruence rules} {\bf(optional)}
2729 simpset {\it simplification set} {\bf(optional)}
2730 {\it reduction rules}
2734 \item \textit{function} is the name of the function, either as an \textit{id}
2735 or a \textit{string}.
2737 \item \textit{rel} is a HOL expression for the well-founded termination
2740 \item \textit{congruence rules} are required only in highly exceptional
2743 \item The \textit{simplification set} is used to prove that the supplied
2744 relation is well-founded. It is also used to prove the \textbf{termination
2745 conditions}: assertions that arguments of recursive calls decrease under
2746 \textit{rel}. By default, simplification uses \texttt{simpset()}, which
2747 is sufficient to prove well-foundedness for the built-in relations listed
2750 \item \textit{reduction rules} specify one or more recursion equations. Each
2751 left-hand side must have the form $f\,t$, where $f$ is the function and $t$
2752 is a tuple of distinct variables. If more than one equation is present then
2753 $f$ is defined by pattern-matching on components of its argument whose type
2754 is a \texttt{datatype}.
2756 The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as
2760 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
2761 prove one termination condition. It remains as a precondition of the
2765 {\out ["! m n. n ~= 0 --> m mod n < n}
2766 {\out ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] }
2769 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
2770 conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard
2771 function \texttt{goalw}, which sets up a goal to prove, but its argument
2772 should be the identifier $f$\texttt{.simps} and its effect is to set up a
2773 proof of the termination conditions:
2775 Tfl.tgoalw thy [] gcd.simps;
2777 {\out ! m n. n ~= 0 --> m mod n < n}
2778 {\out 1. ! m n. n ~= 0 --> m mod n < n}
2780 This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem
2781 is proved, it can be used to eliminate the termination conditions from
2782 elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much
2783 more complicated example of this process, where the termination conditions can
2784 only be proved by complicated reasoning involving the recursive function
2787 Isabelle/HOL can prove the \texttt{gcd} function's termination condition
2788 automatically if supplied with the right simpset.
2790 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
2791 simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"
2792 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2795 If all termination conditions were proved automatically, $f$\texttt{.simps}
2796 is added to the simpset automatically, just as in \texttt{primrec}.
2797 The simplification rules corresponding to clause $i$ (where counting starts
2798 at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms
2800 which returns a list of theorems. Thus you can, for example, remove specific
2801 clauses from the simpset. Note that a single clause may give rise to a set of
2802 simplification rules in order to capture the fact that if clauses overlap,
2803 their order disambiguates them.
2805 A \texttt{recdef} definition also returns an induction rule specialised for
2806 the recursive function. For the \texttt{gcd} function above, the induction
2810 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}
2812 This rule should be used to reason inductively about the \texttt{gcd}
2813 function. It usually makes the induction hypothesis available at all
2814 recursive calls, leading to very direct proofs. If any termination conditions
2815 remain unproved, they will become additional premises of this rule.
2817 \index{recursion!general|)}
2821 \section{Inductive and coinductive definitions}
2822 \index{*inductive|(}
2823 \index{*coinductive|(}
2825 An {\bf inductive definition} specifies the least set~$R$ closed under given
2826 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
2827 example, a structural operational semantics is an inductive definition of an
2828 evaluation relation. Dually, a {\bf coinductive definition} specifies the
2829 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
2830 seen as arising by applying a rule to elements of~$R$.) An important example
2831 is using bisimulation relations to formalise equivalence of processes and
2832 infinite data structures.
2834 A theory file may contain any number of inductive and coinductive
2835 definitions. They may be intermixed with other declarations; in
2836 particular, the (co)inductive sets {\bf must} be declared separately as
2837 constants, and may have mixfix syntax or be subject to syntax translations.
2839 Each (co)inductive definition adds definitions to the theory and also
2840 proves some theorems. Each definition creates an \ML\ structure, which is a
2841 substructure of the main theory structure.
2843 This package is related to the ZF one, described in a separate
2845 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
2846 distributed with Isabelle.} %
2847 which you should refer to in case of difficulties. The package is simpler
2848 than ZF's thanks to HOL's extra-logical automatic type-checking. The types of
2849 the (co)inductive sets determine the domain of the fixedpoint definition, and
2850 the package does not have to use inference rules for type-checking.
2853 \subsection{The result structure}
2854 Many of the result structure's components have been discussed in the paper;
2855 others are self-explanatory.
2857 \item[\tt defs] is the list of definitions of the recursive sets.
2859 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
2861 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
2862 the recursive sets, in the case of mutual recursion).
2864 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
2865 the recursive sets. The rules are also available individually, using the
2866 names given them in the theory file.
2868 \item[\tt elims] is the list of elimination rule.
2870 \item[\tt elim] is the head of the list \texttt{elims}.
2872 \item[\tt mk_cases] is a function to create simplified instances of {\tt
2873 elim} using freeness reasoning on underlying datatypes.
2876 For an inductive definition, the result structure contains the
2877 rule \texttt{induct}. For a
2878 coinductive definition, it contains the rule \verb|coinduct|.
2880 Figure~\ref{def-result-fig} summarises the two result signatures,
2881 specifying the types of all these components.
2889 val intrs : thm list
2890 val elims : thm list
2892 val mk_cases : string -> thm
2893 {\it(Inductive definitions only)}
2895 {\it(coinductive definitions only)}
2900 \caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
2903 \subsection{The syntax of a (co)inductive definition}
2904 An inductive definition has the form
2906 inductive {\it inductive sets}
2907 intrs {\it introduction rules}
2908 monos {\it monotonicity theorems}
2909 con_defs {\it constructor definitions}
2911 A coinductive definition is identical, except that it starts with the keyword
2912 \texttt{coinductive}.
2914 The \texttt{monos} and \texttt{con_defs} sections are optional. If present,
2915 each is specified by a list of identifiers.
2918 \item The \textit{inductive sets} are specified by one or more strings.
2920 \item The \textit{introduction rules} specify one or more introduction rules in
2921 the form \textit{ident\/}~\textit{string}, where the identifier gives the name of
2922 the rule in the result structure.
2924 \item The \textit{monotonicity theorems} are required for each operator
2925 applied to a recursive set in the introduction rules. There {\bf must}
2926 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
2927 premise $t\in M(R@i)$ in an introduction rule!
2929 \item The \textit{constructor definitions} contain definitions of constants
2930 appearing in the introduction rules. In most cases it can be omitted.
2934 \subsection{*Monotonicity theorems}
2936 Each theory contains a default set of theorems that are used in monotonicity
2937 proofs. New rules can be added to this set via the \texttt{mono} attribute.
2938 Theory \texttt{Inductive} shows how this is done. In general, the following
2939 monotonicity theorems may be added:
2941 \item Theorems of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for proving
2942 monotonicity of inductive definitions whose introduction rules have premises
2943 involving terms such as $t\in M(R@i)$.
2944 \item Monotonicity theorems for logical operators, which are of the general form
2945 $\List{\cdots \rightarrow \cdots;~\ldots;~\cdots \rightarrow \cdots} \Imp
2946 \cdots \rightarrow \cdots$.
2947 For example, in the case of the operator $\vee$, the corresponding theorem is
2949 \infer{P@1 \vee P@2 \rightarrow Q@1 \vee Q@2}
2950 {P@1 \rightarrow Q@1 & P@2 \rightarrow Q@2}
2952 \item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g.
2954 (\neg \neg P) ~=~ P \qquad\qquad
2955 (\neg (P \wedge Q)) ~=~ (\neg P \vee \neg Q)
2957 \item Equations for reducing complex operators to more primitive ones whose
2958 monotonicity can easily be proved, e.g.
2960 (P \rightarrow Q) ~=~ (\neg P \vee Q) \qquad\qquad
2961 \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \rightarrow P~x
2965 \subsection{Example of an inductive definition}
2966 Two declarations, included in a theory file, define the finite powerset
2967 operator. First we declare the constant~\texttt{Fin}. Then we declare it
2968 inductively, with two introduction rules:
2970 consts Fin :: 'a set => 'a set set
2973 emptyI "{\ttlbrace}{\ttrbrace} : Fin A"
2974 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
2976 The resulting theory structure contains a substructure, called~\texttt{Fin}.
2977 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
2978 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
2979 rule is \texttt{Fin.induct}.
2981 For another example, here is a theory file defining the accessible part of a
2982 relation. The paper \cite{paulson-CADE} discusses a ZF version of this
2983 example in more detail.
2985 Acc = WF + Inductive +
2987 consts acc :: "('a * 'a)set => 'a set" (* accessible part *)
2991 accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
2995 The Isabelle distribution contains many other inductive definitions. Simple
2996 examples are collected on subdirectory \texttt{HOL/Induct}. The theory
2997 \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples
2998 may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},
2999 \texttt{Lambda} and \texttt{Auth}.
3001 \index{*coinductive|)} \index{*inductive|)}
3004 \section{The examples directories}
3006 Directory \texttt{HOL/Auth} contains theories for proving the correctness of
3007 cryptographic protocols~\cite{paulson-jcs}. The approach is based upon
3008 operational semantics rather than the more usual belief logics. On the same
3009 directory are proofs for some standard examples, such as the Needham-Schroeder
3010 public-key authentication protocol and the Otway-Rees
3013 Directory \texttt{HOL/IMP} contains a formalization of various denotational,
3014 operational and axiomatic semantics of a simple while-language, the necessary
3015 equivalence proofs, soundness and completeness of the Hoare rules with
3016 respect to the denotational semantics, and soundness and completeness of a
3017 verification condition generator. Much of development is taken from
3018 Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
3020 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
3021 logic, including a tactic for generating verification-conditions.
3023 Directory \texttt{HOL/MiniML} contains a formalization of the type system of
3024 the core functional language Mini-ML and a correctness proof for its type
3025 inference algorithm $\cal W$~\cite{milner78,nipkow-W}.
3027 Directory \texttt{HOL/Lambda} contains a formalization of untyped
3028 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
3029 and $\eta$ reduction~\cite{Nipkow-CR}.
3031 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory
3032 of substitutions and unifiers. It is based on Paulson's previous
3033 mechanisation in LCF~\cite{paulson85} of Manna and Waldinger's
3034 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef},
3035 with nested recursion.
3037 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive
3038 definitions and datatypes.
3040 \item Theory \texttt{PropLog} proves the soundness and completeness of
3041 classical propositional logic, given a truth table semantics. The only
3042 connective is $\imp$. A Hilbert-style axiom system is specified, and its
3043 set of theorems defined inductively. A similar proof in ZF is described
3044 elsewhere~\cite{paulson-set-II}.
3046 \item Theory \texttt{Term} defines the datatype \texttt{term}.
3048 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions
3049 as mutually recursive datatypes.
3051 \item The definition of lazy lists demonstrates methods for handling
3052 infinite data structures and coinduction in higher-order
3053 logic~\cite{paulson-coind}.%
3054 \footnote{To be precise, these lists are \emph{potentially infinite} rather
3055 than lazy. Lazy implies a particular operational semantics.}
3056 Theory \thydx{LList} defines an operator for
3057 corecursion on lazy lists, which is used to define a few simple functions
3058 such as map and append. A coinduction principle is defined
3059 for proving equations on lazy lists.
3061 \item Theory \thydx{LFilter} defines the filter functional for lazy lists.
3062 This functional is notoriously difficult to define because finding the next
3063 element meeting the predicate requires possibly unlimited search. It is not
3064 computable, but can be expressed using a combination of induction and
3067 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions
3068 to express a programming language semantics that appears to require mutual
3069 induction. Iterated induction allows greater modularity.
3072 Directory \texttt{HOL/ex} contains other examples and experimental proofs in
3075 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
3076 to define recursive functions. Another example is \texttt{Fib}, which
3077 defines the Fibonacci function.
3079 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two
3080 natural numbers and proves a key lemma of the Fundamental Theorem of
3081 Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$
3084 \item Theory \texttt{Primrec} develops some computation theory. It
3085 inductively defines the set of primitive recursive functions and presents a
3086 proof that Ackermann's function is not primitive recursive.
3088 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty
3089 predicate calculus theorems, ranging from simple tautologies to
3090 moderately difficult problems involving equality and quantifiers.
3092 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc
3093 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
3094 much more powerful than Isabelle's classical reasoner. But it is less
3095 useful in practice because it works only for pure logic; it does not
3096 accept derived rules for the set theory primitives, for example.
3098 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof
3099 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
3101 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
3102 {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem.
3104 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
3105 Milner and Tofte's coinduction example~\cite{milner-coind}. This
3106 substantial proof concerns the soundness of a type system for a simple
3107 functional language. The semantics of recursion is given by a cyclic
3108 environment, which makes a coinductive argument appropriate.
3113 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}
3114 Cantor's Theorem states that every set has more subsets than it has
3115 elements. It has become a favourite example in higher-order logic since
3116 it is so easily expressed:
3117 \[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.
3118 \forall x::\alpha. f~x \not= S
3121 Viewing types as sets, $\alpha\To bool$ represents the powerset
3122 of~$\alpha$. This version states that for every function from $\alpha$ to
3123 its powerset, some subset is outside its range.
3125 The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and
3126 the operator \cdx{range}.
3130 The set~$S$ is given as an unknown instead of a
3131 quantified variable so that we may inspect the subset found by the proof.
3133 Goal "?S ~: range\thinspace(f :: 'a=>'a set)";
3135 {\out ?S ~: range f}
3136 {\out 1. ?S ~: range f}
3138 The first two steps are routine. The rule \tdx{rangeE} replaces
3139 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.
3141 by (resolve_tac [notI] 1);
3143 {\out ?S ~: range f}
3144 {\out 1. ?S : range f ==> False}
3146 by (eresolve_tac [rangeE] 1);
3148 {\out ?S ~: range f}
3149 {\out 1. !!x. ?S = f x ==> False}
3151 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,
3152 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for
3155 by (eresolve_tac [equalityCE] 1);
3157 {\out ?S ~: range f}
3158 {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}
3159 {\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}
3161 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
3162 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies
3163 $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD}
3164 instantiates~$\Var{S}$ and creates the new assumption.
3166 by (dresolve_tac [CollectD] 1);
3168 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}
3169 {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}
3170 {\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}
3172 Forcing a contradiction between the two assumptions of subgoal~1
3173 completes the instantiation of~$S$. It is now the set $\{x. x\not\in
3174 f~x\}$, which is the standard diagonal construction.
3178 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3179 {\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}
3181 The rest should be easy. To apply \tdx{CollectI} to the negated
3182 assumption, we employ \ttindex{swap_res_tac}:
3184 by (swap_res_tac [CollectI] 1);
3186 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3187 {\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}
3191 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3194 How much creativity is required? As it happens, Isabelle can prove this
3195 theorem automatically. The default classical set \texttt{claset()} contains
3196 rules for most of the constructs of HOL's set theory. We must augment it with
3197 \tdx{equalityCE} to break up set equalities, and then apply best-first search.
3198 Depth-first search would diverge, but best-first search successfully navigates
3199 through the large search space. \index{search!best-first}
3203 {\out ?S ~: range f}
3204 {\out 1. ?S ~: range f}
3206 by (best_tac (claset() addSEs [equalityCE]) 1);
3208 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3211 If you run this example interactively, make sure your current theory contains
3212 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
3213 Otherwise the default claset may not contain the rules for set theory.
3214 \index{higher-order logic|)}
3216 %%% Local Variables:
3218 %%% TeX-master: "logics"