|
1 %% $Id$ |
|
2 \chapter{Higher-Order Logic} |
|
3 \index{higher-order logic|(} |
|
4 \index{HOL system@{\sc hol} system} |
|
5 |
|
6 The theory~\thydx{HOL} implements higher-order logic. It is based on |
|
7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on |
|
8 Church's original paper~\cite{church40}. Andrews's |
|
9 book~\cite{andrews86} is a full description of the original |
|
10 Church-style higher-order logic. Experience with the {\sc hol} system |
|
11 has demonstrated that higher-order logic is widely applicable in many |
|
12 areas of mathematics and computer science, not just hardware |
|
13 verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is |
|
14 weaker than {\ZF} set theory but for most applications this does not |
|
15 matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\ |
|
16 to~{\ZF}. |
|
17 |
|
18 The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a |
|
19 different syntax. Ancient releases of Isabelle included still another version |
|
20 of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This |
|
21 version no longer exists, but \thydx{ZF} supports a similar style of |
|
22 reasoning.} follows $\lambda$-calculus and functional programming. Function |
|
23 application is curried. To apply the function~$f$ of type |
|
24 $\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply |
|
25 write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that |
|
26 $f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered |
|
27 pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}. |
|
28 |
|
29 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It |
|
30 identifies object-level types with meta-level types, taking advantage of |
|
31 Isabelle's built-in type-checker. It identifies object-level functions |
|
32 with meta-level functions, so it uses Isabelle's operations for abstraction |
|
33 and application. |
|
34 |
|
35 These identifications allow Isabelle to support \HOL\ particularly |
|
36 nicely, but they also mean that \HOL\ requires more sophistication |
|
37 from the user --- in particular, an understanding of Isabelle's type |
|
38 system. Beginners should work with \texttt{show_types} (or even |
|
39 \texttt{show_sorts}) set to \texttt{true}. |
|
40 % Gain experience by |
|
41 %working in first-order logic before attempting to use higher-order logic. |
|
42 %This chapter assumes familiarity with~{\FOL{}}. |
|
43 |
|
44 |
|
45 \begin{figure} |
|
46 \begin{constants} |
|
47 \it name &\it meta-type & \it description \\ |
|
48 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ |
|
49 \cdx{Not} & $bool\To bool$ & negation ($\neg$) \\ |
|
50 \cdx{True} & $bool$ & tautology ($\top$) \\ |
|
51 \cdx{False} & $bool$ & absurdity ($\bot$) \\ |
|
52 \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\ |
|
53 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder |
|
54 \end{constants} |
|
55 \subcaption{Constants} |
|
56 |
|
57 \begin{constants} |
|
58 \index{"@@{\tt\at} symbol} |
|
59 \index{*"! symbol}\index{*"? symbol} |
|
60 \index{*"?"! symbol}\index{*"E"X"! symbol} |
|
61 \it symbol &\it name &\it meta-type & \it description \\ |
|
62 \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & |
|
63 Hilbert description ($\varepsilon$) \\ |
|
64 {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ & |
|
65 universal quantifier ($\forall$) \\ |
|
66 {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & |
|
67 existential quantifier ($\exists$) \\ |
|
68 {\tt?!} or \texttt{EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & |
|
69 unique existence ($\exists!$)\\ |
|
70 \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & |
|
71 least element |
|
72 \end{constants} |
|
73 \subcaption{Binders} |
|
74 |
|
75 \begin{constants} |
|
76 \index{*"= symbol} |
|
77 \index{&@{\tt\&} symbol} |
|
78 \index{*"| symbol} |
|
79 \index{*"-"-"> symbol} |
|
80 \it symbol & \it meta-type & \it priority & \it description \\ |
|
81 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & |
|
82 Left 55 & composition ($\circ$) \\ |
|
83 \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\ |
|
84 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ |
|
85 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & |
|
86 less than or equals ($\leq$)\\ |
|
87 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ |
|
88 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ |
|
89 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) |
|
90 \end{constants} |
|
91 \subcaption{Infixes} |
|
92 \caption{Syntax of \texttt{HOL}} \label{hol-constants} |
|
93 \end{figure} |
|
94 |
|
95 |
|
96 \begin{figure} |
|
97 \index{*let symbol} |
|
98 \index{*in symbol} |
|
99 \dquotes |
|
100 \[\begin{array}{rclcl} |
|
101 term & = & \hbox{expression of class~$term$} \\ |
|
102 & | & "\at~" id " . " formula \\ |
|
103 & | & |
|
104 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ |
|
105 & | & |
|
106 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\ |
|
107 & | & "LEAST"~ id " . " formula \\[2ex] |
|
108 formula & = & \hbox{expression of type~$bool$} \\ |
|
109 & | & term " = " term \\ |
|
110 & | & term " \ttilde= " term \\ |
|
111 & | & term " < " term \\ |
|
112 & | & term " <= " term \\ |
|
113 & | & "\ttilde\ " formula \\ |
|
114 & | & formula " \& " formula \\ |
|
115 & | & formula " | " formula \\ |
|
116 & | & formula " --> " formula \\ |
|
117 & | & "!~~~" id~id^* " . " formula |
|
118 & | & "ALL~" id~id^* " . " formula \\ |
|
119 & | & "?~~~" id~id^* " . " formula |
|
120 & | & "EX~~" id~id^* " . " formula \\ |
|
121 & | & "?!~~" id~id^* " . " formula |
|
122 & | & "EX!~" id~id^* " . " formula |
|
123 \end{array} |
|
124 \] |
|
125 \caption{Full grammar for \HOL} \label{hol-grammar} |
|
126 \end{figure} |
|
127 |
|
128 |
|
129 \section{Syntax} |
|
130 |
|
131 Figure~\ref{hol-constants} lists the constants (including infixes and |
|
132 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of |
|
133 higher-order logic. Note that $a$\verb|~=|$b$ is translated to |
|
134 $\neg(a=b)$. |
|
135 |
|
136 \begin{warn} |
|
137 \HOL\ has no if-and-only-if connective; logical equivalence is expressed |
|
138 using equality. But equality has a high priority, as befitting a |
|
139 relation, while if-and-only-if typically has the lowest priority. Thus, |
|
140 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. |
|
141 When using $=$ to mean logical equivalence, enclose both operands in |
|
142 parentheses. |
|
143 \end{warn} |
|
144 |
|
145 \subsection{Types and classes} |
|
146 The universal type class of higher-order terms is called~\cldx{term}. |
|
147 By default, explicit type variables have class \cldx{term}. In |
|
148 particular the equality symbol and quantifiers are polymorphic over |
|
149 class \texttt{term}. |
|
150 |
|
151 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, |
|
152 formulae are terms. The built-in type~\tydx{fun}, which constructs |
|
153 function types, is overloaded with arity {\tt(term,\thinspace |
|
154 term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt |
|
155 term} if $\sigma$ and~$\tau$ do, allowing quantification over |
|
156 functions. |
|
157 |
|
158 \HOL\ offers various methods for introducing new types. |
|
159 See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}. |
|
160 |
|
161 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order |
|
162 signatures; the relations $<$ and $\leq$ are polymorphic over this |
|
163 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and |
|
164 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass |
|
165 \cldx{order} of \cldx{ord} which axiomatizes partially ordered types |
|
166 (w.r.t.\ $\le$). |
|
167 |
|
168 Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and |
|
169 \cldx{times} --- permit overloading of the operators {\tt+},\index{*"+ |
|
170 symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In |
|
171 particular, {\tt-} is instantiated for set difference and subtraction |
|
172 on natural numbers. |
|
173 |
|
174 If you state a goal containing overloaded functions, you may need to include |
|
175 type constraints. Type inference may otherwise make the goal more |
|
176 polymorphic than you intended, with confusing results. For example, the |
|
177 variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type |
|
178 $\alpha::\{ord,plus\}$, although you may have expected them to have some |
|
179 numeric type, e.g. $nat$. Instead you should have stated the goal as |
|
180 $(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have |
|
181 type $nat$. |
|
182 |
|
183 \begin{warn} |
|
184 If resolution fails for no obvious reason, try setting |
|
185 \ttindex{show_types} to \texttt{true}, causing Isabelle to display |
|
186 types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as |
|
187 well, causing Isabelle to display type classes and sorts. |
|
188 |
|
189 \index{unification!incompleteness of} |
|
190 Where function types are involved, Isabelle's unification code does not |
|
191 guarantee to find instantiations for type variables automatically. Be |
|
192 prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, |
|
193 possibly instantiating type variables. Setting |
|
194 \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report |
|
195 omitted search paths during unification.\index{tracing!of unification} |
|
196 \end{warn} |
|
197 |
|
198 |
|
199 \subsection{Binders} |
|
200 |
|
201 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for |
|
202 some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\ |
|
203 denote something, a description is always meaningful, but we do not |
|
204 know its value unless $P$ defines it uniquely. We may write |
|
205 descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax |
|
206 \hbox{\tt \at $x$.\ $P[x]$}. |
|
207 |
|
208 Existential quantification is defined by |
|
209 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] |
|
210 The unique existence quantifier, $\exists!x. P$, is defined in terms |
|
211 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested |
|
212 quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates |
|
213 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there |
|
214 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. |
|
215 |
|
216 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} |
|
217 Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\ |
|
218 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The |
|
219 existential quantifier must be followed by a space; thus {\tt?x} is an |
|
220 unknown, while \verb'? x. f x=y' is a quantification. Isabelle's usual |
|
221 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also |
|
222 available. Both notations are accepted for input. The {\ML} reference |
|
223 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt |
|
224 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set |
|
225 to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed. |
|
226 |
|
227 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a |
|
228 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined |
|
229 to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see |
|
230 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ |
|
231 choice operator, so \texttt{Least} is always meaningful, but may yield |
|
232 nothing useful in case there is not a unique least element satisfying |
|
233 $P$.\footnote{Class $ord$ does not require much of its instances, so |
|
234 $\le$ need not be a well-ordering, not even an order at all!} |
|
235 |
|
236 \medskip All these binders have priority 10. |
|
237 |
|
238 \begin{warn} |
|
239 The low priority of binders means that they need to be enclosed in |
|
240 parenthesis when they occur in the context of other operations. For example, |
|
241 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$. |
|
242 \end{warn} |
|
243 |
|
244 |
|
245 \subsection{The \sdx{let} and \sdx{case} constructions} |
|
246 Local abbreviations can be introduced by a \texttt{let} construct whose |
|
247 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into |
|
248 the constant~\cdx{Let}. It can be expanded by rewriting with its |
|
249 definition, \tdx{Let_def}. |
|
250 |
|
251 \HOL\ also defines the basic syntax |
|
252 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] |
|
253 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} |
|
254 and \sdx{of} are reserved words. Initially, this is mere syntax and has no |
|
255 logical meaning. By declaring translations, you can cause instances of the |
|
256 \texttt{case} construct to denote applications of particular case operators. |
|
257 This is what happens automatically for each \texttt{datatype} definition |
|
258 (see~\S\ref{sec:HOL:datatype}). |
|
259 |
|
260 \begin{warn} |
|
261 Both \texttt{if} and \texttt{case} constructs have as low a priority as |
|
262 quantifiers, which requires additional enclosing parentheses in the context |
|
263 of most other operations. For example, instead of $f~x = {\tt if\dots |
|
264 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots |
|
265 else\dots})$. |
|
266 \end{warn} |
|
267 |
|
268 \section{Rules of inference} |
|
269 |
|
270 \begin{figure} |
|
271 \begin{ttbox}\makeatother |
|
272 \tdx{refl} t = (t::'a) |
|
273 \tdx{subst} [| s = t; P s |] ==> P (t::'a) |
|
274 \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) |
|
275 \tdx{impI} (P ==> Q) ==> P-->Q |
|
276 \tdx{mp} [| P-->Q; P |] ==> Q |
|
277 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) |
|
278 \tdx{selectI} P(x::'a) ==> P(@x. P x) |
|
279 \tdx{True_or_False} (P=True) | (P=False) |
|
280 \end{ttbox} |
|
281 \caption{The \texttt{HOL} rules} \label{hol-rules} |
|
282 \end{figure} |
|
283 |
|
284 Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{}, |
|
285 with their~{\ML} names. Some of the rules deserve additional |
|
286 comments: |
|
287 \begin{ttdescription} |
|
288 \item[\tdx{ext}] expresses extensionality of functions. |
|
289 \item[\tdx{iff}] asserts that logically equivalent formulae are |
|
290 equal. |
|
291 \item[\tdx{selectI}] gives the defining property of the Hilbert |
|
292 $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule |
|
293 \tdx{select_equality} (see below) is often easier to use. |
|
294 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In |
|
295 fact, the $\varepsilon$-operator already makes the logic classical, as |
|
296 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} |
|
297 \end{ttdescription} |
|
298 |
|
299 |
|
300 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message |
|
301 \begin{ttbox}\makeatother |
|
302 \tdx{True_def} True == ((\%x::bool. x)=(\%x. x)) |
|
303 \tdx{All_def} All == (\%P. P = (\%x. True)) |
|
304 \tdx{Ex_def} Ex == (\%P. P(@x. P x)) |
|
305 \tdx{False_def} False == (!P. P) |
|
306 \tdx{not_def} not == (\%P. P-->False) |
|
307 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) |
|
308 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) |
|
309 \tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x)) |
|
310 |
|
311 \tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x)) |
|
312 \tdx{if_def} If P x y == |
|
313 (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y)) |
|
314 \tdx{Let_def} Let s f == f s |
|
315 \tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" |
|
316 \end{ttbox} |
|
317 \caption{The \texttt{HOL} definitions} \label{hol-defs} |
|
318 \end{figure} |
|
319 |
|
320 |
|
321 \HOL{} follows standard practice in higher-order logic: only a few |
|
322 connectives are taken as primitive, with the remainder defined obscurely |
|
323 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the |
|
324 corresponding definitions \cite[page~270]{mgordon-hol} using |
|
325 object-equality~({\tt=}), which is possible because equality in |
|
326 higher-order logic may equate formulae and even functions over formulae. |
|
327 But theory~\HOL{}, like all other Isabelle theories, uses |
|
328 meta-equality~({\tt==}) for definitions. |
|
329 \begin{warn} |
|
330 The definitions above should never be expanded and are shown for completeness |
|
331 only. Instead users should reason in terms of the derived rules shown below |
|
332 or, better still, using high-level tactics |
|
333 (see~\S\ref{sec:HOL:generic-packages}). |
|
334 \end{warn} |
|
335 |
|
336 Some of the rules mention type variables; for example, \texttt{refl} |
|
337 mentions the type variable~{\tt'a}. This allows you to instantiate |
|
338 type variables explicitly by calling \texttt{res_inst_tac}. |
|
339 |
|
340 |
|
341 \begin{figure} |
|
342 \begin{ttbox} |
|
343 \tdx{sym} s=t ==> t=s |
|
344 \tdx{trans} [| r=s; s=t |] ==> r=t |
|
345 \tdx{ssubst} [| t=s; P s |] ==> P t |
|
346 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d |
|
347 \tdx{arg_cong} x = y ==> f x = f y |
|
348 \tdx{fun_cong} f = g ==> f x = g x |
|
349 \tdx{cong} [| f = g; x = y |] ==> f x = g y |
|
350 \tdx{not_sym} t ~= s ==> s ~= t |
|
351 \subcaption{Equality} |
|
352 |
|
353 \tdx{TrueI} True |
|
354 \tdx{FalseE} False ==> P |
|
355 |
|
356 \tdx{conjI} [| P; Q |] ==> P&Q |
|
357 \tdx{conjunct1} [| P&Q |] ==> P |
|
358 \tdx{conjunct2} [| P&Q |] ==> Q |
|
359 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R |
|
360 |
|
361 \tdx{disjI1} P ==> P|Q |
|
362 \tdx{disjI2} Q ==> P|Q |
|
363 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R |
|
364 |
|
365 \tdx{notI} (P ==> False) ==> ~ P |
|
366 \tdx{notE} [| ~ P; P |] ==> R |
|
367 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R |
|
368 \subcaption{Propositional logic} |
|
369 |
|
370 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q |
|
371 \tdx{iffD1} [| P=Q; P |] ==> Q |
|
372 \tdx{iffD2} [| P=Q; Q |] ==> P |
|
373 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R |
|
374 % |
|
375 %\tdx{eqTrueI} P ==> P=True |
|
376 %\tdx{eqTrueE} P=True ==> P |
|
377 \subcaption{Logical equivalence} |
|
378 |
|
379 \end{ttbox} |
|
380 \caption{Derived rules for \HOL} \label{hol-lemmas1} |
|
381 \end{figure} |
|
382 |
|
383 |
|
384 \begin{figure} |
|
385 \begin{ttbox}\makeatother |
|
386 \tdx{allI} (!!x. P x) ==> !x. P x |
|
387 \tdx{spec} !x. P x ==> P x |
|
388 \tdx{allE} [| !x. P x; P x ==> R |] ==> R |
|
389 \tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R |
|
390 |
|
391 \tdx{exI} P x ==> ? x. P x |
|
392 \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q |
|
393 |
|
394 \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x |
|
395 \tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R |
|
396 |] ==> R |
|
397 |
|
398 \tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a |
|
399 \subcaption{Quantifiers and descriptions} |
|
400 |
|
401 \tdx{ccontr} (~P ==> False) ==> P |
|
402 \tdx{classical} (~P ==> P) ==> P |
|
403 \tdx{excluded_middle} ~P | P |
|
404 |
|
405 \tdx{disjCI} (~Q ==> P) ==> P|Q |
|
406 \tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x |
|
407 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R |
|
408 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R |
|
409 \tdx{notnotD} ~~P ==> P |
|
410 \tdx{swap} ~P ==> (~Q ==> P) ==> Q |
|
411 \subcaption{Classical logic} |
|
412 |
|
413 %\tdx{if_True} (if True then x else y) = x |
|
414 %\tdx{if_False} (if False then x else y) = y |
|
415 \tdx{if_P} P ==> (if P then x else y) = x |
|
416 \tdx{if_not_P} ~ P ==> (if P then x else y) = y |
|
417 \tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) |
|
418 \subcaption{Conditionals} |
|
419 \end{ttbox} |
|
420 \caption{More derived rules} \label{hol-lemmas2} |
|
421 \end{figure} |
|
422 |
|
423 Some derived rules are shown in Figures~\ref{hol-lemmas1} |
|
424 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules |
|
425 for the logical connectives, as well as sequent-style elimination rules for |
|
426 conjunctions, implications, and universal quantifiers. |
|
427 |
|
428 Note the equality rules: \tdx{ssubst} performs substitution in |
|
429 backward proofs, while \tdx{box_equals} supports reasoning by |
|
430 simplifying both sides of an equation. |
|
431 |
|
432 The following simple tactics are occasionally useful: |
|
433 \begin{ttdescription} |
|
434 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} |
|
435 repeatedly to remove all outermost universal quantifiers and implications |
|
436 from subgoal $i$. |
|
437 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction |
|
438 on $P$ for subgoal $i$: the latter is replaced by two identical subgoals |
|
439 with the added assumptions $P$ and $\neg P$, respectively. |
|
440 \end{ttdescription} |
|
441 |
|
442 |
|
443 \begin{figure} |
|
444 \begin{center} |
|
445 \begin{tabular}{rrr} |
|
446 \it name &\it meta-type & \it description \\ |
|
447 \index{{}@\verb'{}' symbol} |
|
448 \verb|{}| & $\alpha\,set$ & the empty set \\ |
|
449 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ |
|
450 & insertion of element \\ |
|
451 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ |
|
452 & comprehension \\ |
|
453 \cdx{Compl} & $\alpha\,set\To\alpha\,set$ |
|
454 & complement \\ |
|
455 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ |
|
456 & intersection over a set\\ |
|
457 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ |
|
458 & union over a set\\ |
|
459 \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ |
|
460 &set of sets intersection \\ |
|
461 \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ |
|
462 &set of sets union \\ |
|
463 \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ |
|
464 & powerset \\[1ex] |
|
465 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ |
|
466 & range of a function \\[1ex] |
|
467 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ |
|
468 & bounded quantifiers |
|
469 \end{tabular} |
|
470 \end{center} |
|
471 \subcaption{Constants} |
|
472 |
|
473 \begin{center} |
|
474 \begin{tabular}{llrrr} |
|
475 \it symbol &\it name &\it meta-type & \it priority & \it description \\ |
|
476 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & |
|
477 intersection over a type\\ |
|
478 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & |
|
479 union over a type |
|
480 \end{tabular} |
|
481 \end{center} |
|
482 \subcaption{Binders} |
|
483 |
|
484 \begin{center} |
|
485 \index{*"`"` symbol} |
|
486 \index{*": symbol} |
|
487 \index{*"<"= symbol} |
|
488 \begin{tabular}{rrrr} |
|
489 \it symbol & \it meta-type & \it priority & \it description \\ |
|
490 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$ |
|
491 & Left 90 & image \\ |
|
492 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ |
|
493 & Left 70 & intersection ($\int$) \\ |
|
494 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ |
|
495 & Left 65 & union ($\un$) \\ |
|
496 \tt: & $[\alpha ,\alpha\,set]\To bool$ |
|
497 & Left 50 & membership ($\in$) \\ |
|
498 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ |
|
499 & Left 50 & subset ($\subseteq$) |
|
500 \end{tabular} |
|
501 \end{center} |
|
502 \subcaption{Infixes} |
|
503 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax} |
|
504 \end{figure} |
|
505 |
|
506 |
|
507 \begin{figure} |
|
508 \begin{center} \tt\frenchspacing |
|
509 \index{*"! symbol} |
|
510 \begin{tabular}{rrr} |
|
511 \it external & \it internal & \it description \\ |
|
512 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\ |
|
513 {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ |
|
514 {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & |
|
515 \rm comprehension \\ |
|
516 \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ & |
|
517 \rm intersection \\ |
|
518 \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & |
|
519 \rm union \\ |
|
520 \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ & |
|
521 Ball $A$ $\lambda x. P[x]$ & |
|
522 \rm bounded $\forall$ \\ |
|
523 \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ & |
|
524 Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$ |
|
525 \end{tabular} |
|
526 \end{center} |
|
527 \subcaption{Translations} |
|
528 |
|
529 \dquotes |
|
530 \[\begin{array}{rclcl} |
|
531 term & = & \hbox{other terms\ldots} \\ |
|
532 & | & "{\ttlbrace}{\ttrbrace}" \\ |
|
533 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ |
|
534 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\ |
|
535 & | & term " `` " term \\ |
|
536 & | & term " Int " term \\ |
|
537 & | & term " Un " term \\ |
|
538 & | & "INT~~" id ":" term " . " term \\ |
|
539 & | & "UN~~~" id ":" term " . " term \\ |
|
540 & | & "INT~~" id~id^* " . " term \\ |
|
541 & | & "UN~~~" id~id^* " . " term \\[2ex] |
|
542 formula & = & \hbox{other formulae\ldots} \\ |
|
543 & | & term " : " term \\ |
|
544 & | & term " \ttilde: " term \\ |
|
545 & | & term " <= " term \\ |
|
546 & | & "!~" id ":" term " . " formula |
|
547 & | & "ALL " id ":" term " . " formula \\ |
|
548 & | & "?~" id ":" term " . " formula |
|
549 & | & "EX~~" id ":" term " . " formula |
|
550 \end{array} |
|
551 \] |
|
552 \subcaption{Full Grammar} |
|
553 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2} |
|
554 \end{figure} |
|
555 |
|
556 |
|
557 \section{A formulation of set theory} |
|
558 Historically, higher-order logic gives a foundation for Russell and |
|
559 Whitehead's theory of classes. Let us use modern terminology and call them |
|
560 {\bf sets}, but note that these sets are distinct from those of {\ZF} set |
|
561 theory, and behave more like {\ZF} classes. |
|
562 \begin{itemize} |
|
563 \item |
|
564 Sets are given by predicates over some type~$\sigma$. Types serve to |
|
565 define universes for sets, but type-checking is still significant. |
|
566 \item |
|
567 There is a universal set (for each type). Thus, sets have complements, and |
|
568 may be defined by absolute comprehension. |
|
569 \item |
|
570 Although sets may contain other sets as elements, the containing set must |
|
571 have a more complex type. |
|
572 \end{itemize} |
|
573 Finite unions and intersections have the same behaviour in \HOL\ as they |
|
574 do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined, |
|
575 denoting the universal set for the given type. |
|
576 |
|
577 \subsection{Syntax of set theory}\index{*set type} |
|
578 \HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is |
|
579 essentially the same as $\alpha\To bool$. The new type is defined for |
|
580 clarity and to avoid complications involving function types in unification. |
|
581 The isomorphisms between the two types are declared explicitly. They are |
|
582 very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while |
|
583 \hbox{\tt op :} maps in the other direction (ignoring argument order). |
|
584 |
|
585 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax |
|
586 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new |
|
587 constructs. Infix operators include union and intersection ($A\un B$ |
|
588 and $A\int B$), the subset and membership relations, and the image |
|
589 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to |
|
590 $\neg(a\in b)$. |
|
591 |
|
592 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in |
|
593 the obvious manner using~\texttt{insert} and~$\{\}$: |
|
594 \begin{eqnarray*} |
|
595 \{a, b, c\} & \equiv & |
|
596 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) |
|
597 \end{eqnarray*} |
|
598 |
|
599 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type) |
|
600 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free |
|
601 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda |
|
602 x. P[x])$. It defines sets by absolute comprehension, which is impossible |
|
603 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension. |
|
604 |
|
605 The set theory defines two {\bf bounded quantifiers}: |
|
606 \begin{eqnarray*} |
|
607 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ |
|
608 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] |
|
609 \end{eqnarray*} |
|
610 The constants~\cdx{Ball} and~\cdx{Bex} are defined |
|
611 accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may |
|
612 write\index{*"! symbol}\index{*"? symbol} |
|
613 \index{*ALL symbol}\index{*EX symbol} |
|
614 % |
|
615 \hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's |
|
616 usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted |
|
617 for input. As with the primitive quantifiers, the {\ML} reference |
|
618 \ttindex{HOL_quantifiers} specifies which notation to use for output. |
|
619 |
|
620 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and |
|
621 $\bigcap@{x\in A}B[x]$, are written |
|
622 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and |
|
623 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}. |
|
624 |
|
625 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x |
|
626 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and |
|
627 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous |
|
628 union and intersection operators when $A$ is the universal set. |
|
629 |
|
630 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are |
|
631 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$, |
|
632 respectively. |
|
633 |
|
634 |
|
635 |
|
636 \begin{figure} \underscoreon |
|
637 \begin{ttbox} |
|
638 \tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a |
|
639 \tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A |
|
640 |
|
641 \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace} |
|
642 \tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B |
|
643 \tdx{Ball_def} Ball A P == ! x. x:A --> P x |
|
644 \tdx{Bex_def} Bex A P == ? x. x:A & P x |
|
645 \tdx{subset_def} A <= B == ! x:A. x:B |
|
646 \tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace} |
|
647 \tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace} |
|
648 \tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace} |
|
649 \tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace} |
|
650 \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} |
|
651 \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} |
|
652 \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B |
|
653 \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B |
|
654 \tdx{Inter_def} Inter S == (INT x:S. x) |
|
655 \tdx{Union_def} Union S == (UN x:S. x) |
|
656 \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} |
|
657 \tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} |
|
658 \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} |
|
659 \end{ttbox} |
|
660 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules} |
|
661 \end{figure} |
|
662 |
|
663 |
|
664 \begin{figure} \underscoreon |
|
665 \begin{ttbox} |
|
666 \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace} |
|
667 \tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a |
|
668 \tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W |
|
669 |
|
670 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x |
|
671 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x |
|
672 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q |
|
673 |
|
674 \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x |
|
675 \tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x |
|
676 \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q |
|
677 \subcaption{Comprehension and Bounded quantifiers} |
|
678 |
|
679 \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B |
|
680 \tdx{subsetD} [| A <= B; c:A |] ==> c:B |
|
681 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P |
|
682 |
|
683 \tdx{subset_refl} A <= A |
|
684 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C |
|
685 |
|
686 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B |
|
687 \tdx{equalityD1} A = B ==> A<=B |
|
688 \tdx{equalityD2} A = B ==> B<=A |
|
689 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P |
|
690 |
|
691 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P; |
|
692 [| ~ c:A; ~ c:B |] ==> P |
|
693 |] ==> P |
|
694 \subcaption{The subset and equality relations} |
|
695 \end{ttbox} |
|
696 \caption{Derived rules for set theory} \label{hol-set1} |
|
697 \end{figure} |
|
698 |
|
699 |
|
700 \begin{figure} \underscoreon |
|
701 \begin{ttbox} |
|
702 \tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P |
|
703 |
|
704 \tdx{insertI1} a : insert a B |
|
705 \tdx{insertI2} a : B ==> a : insert b B |
|
706 \tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P |
|
707 |
|
708 \tdx{ComplI} [| c:A ==> False |] ==> c : Compl A |
|
709 \tdx{ComplD} [| c : Compl A |] ==> ~ c:A |
|
710 |
|
711 \tdx{UnI1} c:A ==> c : A Un B |
|
712 \tdx{UnI2} c:B ==> c : A Un B |
|
713 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B |
|
714 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P |
|
715 |
|
716 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B |
|
717 \tdx{IntD1} c : A Int B ==> c:A |
|
718 \tdx{IntD2} c : A Int B ==> c:B |
|
719 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P |
|
720 |
|
721 \tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x) |
|
722 \tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R |
|
723 |
|
724 \tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x) |
|
725 \tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a |
|
726 \tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R |
|
727 |
|
728 \tdx{UnionI} [| X:C; A:X |] ==> A : Union C |
|
729 \tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R |
|
730 |
|
731 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C |
|
732 \tdx{InterD} [| A : Inter C; X:C |] ==> A:X |
|
733 \tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R |
|
734 |
|
735 \tdx{PowI} A<=B ==> A: Pow B |
|
736 \tdx{PowD} A: Pow B ==> A<=B |
|
737 |
|
738 \tdx{imageI} [| x:A |] ==> f x : f``A |
|
739 \tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P |
|
740 |
|
741 \tdx{rangeI} f x : range f |
|
742 \tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P |
|
743 \end{ttbox} |
|
744 \caption{Further derived rules for set theory} \label{hol-set2} |
|
745 \end{figure} |
|
746 |
|
747 |
|
748 \subsection{Axioms and rules of set theory} |
|
749 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The |
|
750 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert |
|
751 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of |
|
752 course, \hbox{\tt op :} also serves as the membership relation. |
|
753 |
|
754 All the other axioms are definitions. They include the empty set, bounded |
|
755 quantifiers, unions, intersections, complements and the subset relation. |
|
756 They also include straightforward constructions on functions: image~({\tt``}) |
|
757 and \texttt{range}. |
|
758 |
|
759 %The predicate \cdx{inj_on} is used for simulating type definitions. |
|
760 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the |
|
761 %set~$A$, which specifies a subset of its domain type. In a type |
|
762 %definition, $f$ is the abstraction function and $A$ is the set of valid |
|
763 %representations; we should not expect $f$ to be injective outside of~$A$. |
|
764 |
|
765 %\begin{figure} \underscoreon |
|
766 %\begin{ttbox} |
|
767 %\tdx{Inv_f_f} inj f ==> Inv f (f x) = x |
|
768 %\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y |
|
769 % |
|
770 %\tdx{Inv_injective} |
|
771 % [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y |
|
772 % |
|
773 % |
|
774 %\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f |
|
775 %\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B |
|
776 % |
|
777 %\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f |
|
778 %\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f |
|
779 %\tdx{injD} [| inj f; f x = f y |] ==> x=y |
|
780 % |
|
781 %\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A |
|
782 %\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y |
|
783 % |
|
784 %\tdx{inj_on_inverseI} |
|
785 % (!!x. x:A ==> g(f x) = x) ==> inj_on f A |
|
786 %\tdx{inj_on_contraD} |
|
787 % [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y |
|
788 %\end{ttbox} |
|
789 %\caption{Derived rules involving functions} \label{hol-fun} |
|
790 %\end{figure} |
|
791 |
|
792 |
|
793 \begin{figure} \underscoreon |
|
794 \begin{ttbox} |
|
795 \tdx{Union_upper} B:A ==> B <= Union A |
|
796 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C |
|
797 |
|
798 \tdx{Inter_lower} B:A ==> Inter A <= B |
|
799 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A |
|
800 |
|
801 \tdx{Un_upper1} A <= A Un B |
|
802 \tdx{Un_upper2} B <= A Un B |
|
803 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C |
|
804 |
|
805 \tdx{Int_lower1} A Int B <= A |
|
806 \tdx{Int_lower2} A Int B <= B |
|
807 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B |
|
808 \end{ttbox} |
|
809 \caption{Derived rules involving subsets} \label{hol-subset} |
|
810 \end{figure} |
|
811 |
|
812 |
|
813 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message |
|
814 \begin{ttbox} |
|
815 \tdx{Int_absorb} A Int A = A |
|
816 \tdx{Int_commute} A Int B = B Int A |
|
817 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) |
|
818 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) |
|
819 |
|
820 \tdx{Un_absorb} A Un A = A |
|
821 \tdx{Un_commute} A Un B = B Un A |
|
822 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) |
|
823 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) |
|
824 |
|
825 \tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace} |
|
826 \tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x. True{\ttrbrace} |
|
827 \tdx{double_complement} Compl(Compl A) = A |
|
828 \tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B) |
|
829 \tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B) |
|
830 |
|
831 \tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B) |
|
832 \tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C) |
|
833 \tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) |
|
834 |
|
835 \tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B) |
|
836 \tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C) |
|
837 \tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) |
|
838 \end{ttbox} |
|
839 \caption{Set equalities} \label{hol-equalities} |
|
840 \end{figure} |
|
841 |
|
842 |
|
843 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are |
|
844 obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules, |
|
845 such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, |
|
846 are designed for classical reasoning; the rules \tdx{subsetD}, |
|
847 \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not |
|
848 strictly necessary but yield more natural proofs. Similarly, |
|
849 \tdx{equalityCE} supports classical reasoning about extensionality, |
|
850 after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for |
|
851 proofs pertaining to set theory. |
|
852 |
|
853 Figure~\ref{hol-subset} presents lattice properties of the subset relation. |
|
854 Unions form least upper bounds; non-empty intersections form greatest lower |
|
855 bounds. Reasoning directly about subsets often yields clearer proofs than |
|
856 reasoning about the membership relation. See the file \texttt{HOL/subset.ML}. |
|
857 |
|
858 Figure~\ref{hol-equalities} presents many common set equalities. They |
|
859 include commutative, associative and distributive laws involving unions, |
|
860 intersections and complements. For a complete listing see the file {\tt |
|
861 HOL/equalities.ML}. |
|
862 |
|
863 \begin{warn} |
|
864 \texttt{Blast_tac} proves many set-theoretic theorems automatically. |
|
865 Hence you seldom need to refer to the theorems above. |
|
866 \end{warn} |
|
867 |
|
868 \begin{figure} |
|
869 \begin{center} |
|
870 \begin{tabular}{rrr} |
|
871 \it name &\it meta-type & \it description \\ |
|
872 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ |
|
873 & injective/surjective \\ |
|
874 \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$ |
|
875 & injective over subset\\ |
|
876 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function |
|
877 \end{tabular} |
|
878 \end{center} |
|
879 |
|
880 \underscoreon |
|
881 \begin{ttbox} |
|
882 \tdx{inj_def} inj f == ! x y. f x=f y --> x=y |
|
883 \tdx{surj_def} surj f == ! y. ? x. y=f x |
|
884 \tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y |
|
885 \tdx{inv_def} inv f == (\%y. @x. f(x)=y) |
|
886 \end{ttbox} |
|
887 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun} |
|
888 \end{figure} |
|
889 |
|
890 \subsection{Properties of functions}\nopagebreak |
|
891 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. |
|
892 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse |
|
893 of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived |
|
894 rules. Reasoning about function composition (the operator~\sdx{o}) and the |
|
895 predicate~\cdx{surj} is done simply by expanding the definitions. |
|
896 |
|
897 There is also a large collection of monotonicity theorems for constructions |
|
898 on sets in the file \texttt{HOL/mono.ML}. |
|
899 |
|
900 \section{Generic packages} |
|
901 \label{sec:HOL:generic-packages} |
|
902 |
|
903 \HOL\ instantiates most of Isabelle's generic packages, making available the |
|
904 simplifier and the classical reasoner. |
|
905 |
|
906 \subsection{Simplification and substitution} |
|
907 |
|
908 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset |
|
909 (\texttt{simpset()}), which works for most purposes. A quite minimal |
|
910 simplification set for higher-order logic is~\ttindexbold{HOL_ss}; |
|
911 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which |
|
912 also expresses logical equivalence, may be used for rewriting. See |
|
913 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic |
|
914 simplification rules. |
|
915 |
|
916 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
|
917 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution |
|
918 and simplification. |
|
919 |
|
920 \begin{warn}\index{simplification!of conjunctions}% |
|
921 Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The |
|
922 left part of a conjunction helps in simplifying the right part. This effect |
|
923 is not available by default: it can be slow. It can be obtained by |
|
924 including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. |
|
925 \end{warn} |
|
926 |
|
927 If the simplifier cannot use a certain rewrite rule --- either because |
|
928 of nontermination or because its left-hand side is too flexible --- |
|
929 then you might try \texttt{stac}: |
|
930 \begin{ttdescription} |
|
931 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$, |
|
932 replaces in subgoal $i$ instances of $lhs$ by corresponding instances of |
|
933 $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking |
|
934 may be necessary to select the desired ones. |
|
935 |
|
936 If $thm$ is a conditional equality, the instantiated condition becomes an |
|
937 additional (first) subgoal. |
|
938 \end{ttdescription} |
|
939 |
|
940 \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes |
|
941 for an equality throughout a subgoal and its hypotheses. This tactic uses |
|
942 \HOL's general substitution rule. |
|
943 |
|
944 \subsubsection{Case splitting} |
|
945 \label{subsec:HOL:case:splitting} |
|
946 |
|
947 \HOL{} also provides convenient means for case splitting during |
|
948 rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt |
|
949 then\dots else\dots} often require a case distinction on $b$. This is |
|
950 expressed by the theorem \tdx{split_if}: |
|
951 $$ |
|
952 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~ |
|
953 ((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y}))) |
|
954 \eqno{(*)} |
|
955 $$ |
|
956 For example, a simple instance of $(*)$ is |
|
957 \[ |
|
958 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~ |
|
959 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\})) |
|
960 \] |
|
961 Because $(*)$ is too general as a rewrite rule for the simplifier (the |
|
962 left-hand side is not a higher-order pattern in the sense of |
|
963 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}% |
|
964 {Chap.\ts\ref{chap:simplification}}), there is a special infix function |
|
965 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset} |
|
966 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a |
|
967 simpset, as in |
|
968 \begin{ttbox} |
|
969 by(simp_tac (simpset() addsplits [split_if]) 1); |
|
970 \end{ttbox} |
|
971 The effect is that after each round of simplification, one occurrence of |
|
972 \texttt{if} is split acording to \texttt{split_if}, until all occurences of |
|
973 \texttt{if} have been eliminated. |
|
974 |
|
975 It turns out that using \texttt{split_if} is almost always the right thing to |
|
976 do. Hence \texttt{split_if} is already included in the default simpset. If |
|
977 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is |
|
978 the inverse of \texttt{addsplits}: |
|
979 \begin{ttbox} |
|
980 by(simp_tac (simpset() delsplits [split_if]) 1); |
|
981 \end{ttbox} |
|
982 |
|
983 In general, \texttt{addsplits} accepts rules of the form |
|
984 \[ |
|
985 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs |
|
986 \] |
|
987 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the |
|
988 right form because internally the left-hand side is |
|
989 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples |
|
990 are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list} |
|
991 and~\S\ref{subsec:datatype:basics}). |
|
992 |
|
993 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also |
|
994 imperative versions of \texttt{addsplits} and \texttt{delsplits} |
|
995 \begin{ttbox} |
|
996 \ttindexbold{Addsplits}: thm list -> unit |
|
997 \ttindexbold{Delsplits}: thm list -> unit |
|
998 \end{ttbox} |
|
999 for adding splitting rules to, and deleting them from the current simpset. |
|
1000 |
|
1001 \subsection{Classical reasoning} |
|
1002 |
|
1003 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as |
|
1004 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap |
|
1005 rule; recall Fig.\ts\ref{hol-lemmas2} above. |
|
1006 |
|
1007 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt |
|
1008 Best_tac} refer to the default claset (\texttt{claset()}), which works for most |
|
1009 purposes. Named clasets include \ttindexbold{prop_cs}, which includes the |
|
1010 propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier |
|
1011 rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules, |
|
1012 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
|
1013 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. |
|
1014 |
|
1015 |
|
1016 \section{Types}\label{sec:HOL:Types} |
|
1017 This section describes \HOL's basic predefined types ($\alpha \times |
|
1018 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for |
|
1019 introducing new types in general. The most important type |
|
1020 construction, the \texttt{datatype}, is treated separately in |
|
1021 \S\ref{sec:HOL:datatype}. |
|
1022 |
|
1023 |
|
1024 \subsection{Product and sum types}\index{*"* type}\index{*"+ type} |
|
1025 \label{subsec:prod-sum} |
|
1026 |
|
1027 \begin{figure}[htbp] |
|
1028 \begin{constants} |
|
1029 \it symbol & \it meta-type & & \it description \\ |
|
1030 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ |
|
1031 & & ordered pairs $(a,b)$ \\ |
|
1032 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ |
|
1033 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ |
|
1034 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ |
|
1035 & & generalized projection\\ |
|
1036 \cdx{Sigma} & |
|
1037 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & |
|
1038 & general sum of sets |
|
1039 \end{constants} |
|
1040 \begin{ttbox}\makeatletter |
|
1041 %\tdx{fst_def} fst p == @a. ? b. p = (a,b) |
|
1042 %\tdx{snd_def} snd p == @b. ? a. p = (a,b) |
|
1043 %\tdx{split_def} split c p == c (fst p) (snd p) |
|
1044 \tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} |
|
1045 |
|
1046 \tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b') |
|
1047 \tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R |
|
1048 \tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q |
|
1049 |
|
1050 \tdx{fst_conv} fst (a,b) = a |
|
1051 \tdx{snd_conv} snd (a,b) = b |
|
1052 \tdx{surjective_pairing} p = (fst p,snd p) |
|
1053 |
|
1054 \tdx{split} split c (a,b) = c a b |
|
1055 \tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y)) |
|
1056 |
|
1057 \tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B |
|
1058 \tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P |
|
1059 \end{ttbox} |
|
1060 \caption{Type $\alpha\times\beta$}\label{hol-prod} |
|
1061 \end{figure} |
|
1062 |
|
1063 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type |
|
1064 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General |
|
1065 tuples are simulated by pairs nested to the right: |
|
1066 \begin{center} |
|
1067 \begin{tabular}{c|c} |
|
1068 external & internal \\ |
|
1069 \hline |
|
1070 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\ |
|
1071 \hline |
|
1072 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ |
|
1073 \end{tabular} |
|
1074 \end{center} |
|
1075 In addition, it is possible to use tuples |
|
1076 as patterns in abstractions: |
|
1077 \begin{center} |
|
1078 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} |
|
1079 \end{center} |
|
1080 Nested patterns are also supported. They are translated stepwise: |
|
1081 {\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$ |
|
1082 {\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$ |
|
1083 $z$.\ $t$))}. The reverse translation is performed upon printing. |
|
1084 \begin{warn} |
|
1085 The translation between patterns and \texttt{split} is performed automatically |
|
1086 by the parser and printer. Thus the internal and external form of a term |
|
1087 may differ, which can affects proofs. For example the term {\tt |
|
1088 (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the |
|
1089 default simpset) to rewrite to {\tt(b,a)}. |
|
1090 \end{warn} |
|
1091 In addition to explicit $\lambda$-abstractions, patterns can be used in any |
|
1092 variable binding construct which is internally described by a |
|
1093 $\lambda$-abstraction. Some important examples are |
|
1094 \begin{description} |
|
1095 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$} |
|
1096 \item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$} |
|
1097 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$} |
|
1098 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} |
|
1099 \item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}} |
|
1100 \end{description} |
|
1101 |
|
1102 There is a simple tactic which supports reasoning about patterns: |
|
1103 \begin{ttdescription} |
|
1104 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all |
|
1105 {\tt!!}-quantified variables of product type by individual variables for |
|
1106 each component. A simple example: |
|
1107 \begin{ttbox} |
|
1108 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} |
|
1109 by(split_all_tac 1); |
|
1110 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} |
|
1111 \end{ttbox} |
|
1112 \end{ttdescription} |
|
1113 |
|
1114 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} |
|
1115 which contains only a single element named {\tt()} with the property |
|
1116 \begin{ttbox} |
|
1117 \tdx{unit_eq} u = () |
|
1118 \end{ttbox} |
|
1119 \bigskip |
|
1120 |
|
1121 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$ |
|
1122 which associates to the right and has a lower priority than $*$: $\tau@1 + |
|
1123 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$. |
|
1124 |
|
1125 The definition of products and sums in terms of existing types is not |
|
1126 shown. The constructions are fairly standard and can be found in the |
|
1127 respective theory files. |
|
1128 |
|
1129 \begin{figure} |
|
1130 \begin{constants} |
|
1131 \it symbol & \it meta-type & & \it description \\ |
|
1132 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ |
|
1133 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ |
|
1134 \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ |
|
1135 & & conditional |
|
1136 \end{constants} |
|
1137 \begin{ttbox}\makeatletter |
|
1138 %\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) & |
|
1139 % (!y. p=Inr y --> z=g y)) |
|
1140 % |
|
1141 \tdx{Inl_not_Inr} Inl a ~= Inr b |
|
1142 |
|
1143 \tdx{inj_Inl} inj Inl |
|
1144 \tdx{inj_Inr} inj Inr |
|
1145 |
|
1146 \tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s |
|
1147 |
|
1148 \tdx{sum_case_Inl} sum_case f g (Inl x) = f x |
|
1149 \tdx{sum_case_Inr} sum_case f g (Inr x) = g x |
|
1150 |
|
1151 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s |
|
1152 \tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) & |
|
1153 (! y. s = Inr(y) --> R(g(y)))) |
|
1154 \end{ttbox} |
|
1155 \caption{Type $\alpha+\beta$}\label{hol-sum} |
|
1156 \end{figure} |
|
1157 |
|
1158 \begin{figure} |
|
1159 \index{*"< symbol} |
|
1160 \index{*"* symbol} |
|
1161 \index{*div symbol} |
|
1162 \index{*mod symbol} |
|
1163 \index{*"+ symbol} |
|
1164 \index{*"- symbol} |
|
1165 \begin{constants} |
|
1166 \it symbol & \it meta-type & \it priority & \it description \\ |
|
1167 \cdx{0} & $nat$ & & zero \\ |
|
1168 \cdx{Suc} & $nat \To nat$ & & successor function\\ |
|
1169 % \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\ |
|
1170 % \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$ |
|
1171 % & & primitive recursor\\ |
|
1172 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ |
|
1173 \tt div & $[nat,nat]\To nat$ & Left 70 & division\\ |
|
1174 \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\ |
|
1175 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ |
|
1176 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction |
|
1177 \end{constants} |
|
1178 \subcaption{Constants and infixes} |
|
1179 |
|
1180 \begin{ttbox}\makeatother |
|
1181 \tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n |
|
1182 |
|
1183 \tdx{Suc_not_Zero} Suc m ~= 0 |
|
1184 \tdx{inj_Suc} inj Suc |
|
1185 \tdx{n_not_Suc_n} n~=Suc n |
|
1186 \subcaption{Basic properties} |
|
1187 \end{ttbox} |
|
1188 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1} |
|
1189 \end{figure} |
|
1190 |
|
1191 |
|
1192 \begin{figure} |
|
1193 \begin{ttbox}\makeatother |
|
1194 0+n = n |
|
1195 (Suc m)+n = Suc(m+n) |
|
1196 |
|
1197 m-0 = m |
|
1198 0-n = n |
|
1199 Suc(m)-Suc(n) = m-n |
|
1200 |
|
1201 0*n = 0 |
|
1202 Suc(m)*n = n + m*n |
|
1203 |
|
1204 \tdx{mod_less} m<n ==> m mod n = m |
|
1205 \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n |
|
1206 |
|
1207 \tdx{div_less} m<n ==> m div n = 0 |
|
1208 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n) |
|
1209 \end{ttbox} |
|
1210 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2} |
|
1211 \end{figure} |
|
1212 |
|
1213 \subsection{The type of natural numbers, \textit{nat}} |
|
1214 \index{nat@{\textit{nat}} type|(} |
|
1215 |
|
1216 The theory \thydx{NatDef} defines the natural numbers in a roundabout but |
|
1217 traditional way. The axiom of infinity postulates a type~\tydx{ind} of |
|
1218 individuals, which is non-empty and closed under an injective operation. The |
|
1219 natural numbers are inductively generated by choosing an arbitrary individual |
|
1220 for~0 and using the injective operation to take successors. This is a least |
|
1221 fixedpoint construction. For details see the file \texttt{NatDef.thy}. |
|
1222 |
|
1223 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the |
|
1224 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also |
|
1225 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory |
|
1226 \thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order, |
|
1227 so \tydx{nat} is also an instance of class \cldx{order}. |
|
1228 |
|
1229 Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines |
|
1230 addition, multiplication and subtraction. Theory \thydx{Divides} defines |
|
1231 division, remainder and the ``divides'' relation. The numerous theorems |
|
1232 proved include commutative, associative, distributive, identity and |
|
1233 cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The |
|
1234 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on |
|
1235 \texttt{nat} are part of the default simpset. |
|
1236 |
|
1237 Functions on \tydx{nat} can be defined by primitive or well-founded recursion; |
|
1238 see \S\ref{sec:HOL:recursive}. A simple example is addition. |
|
1239 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following |
|
1240 the standard convention. |
|
1241 \begin{ttbox} |
|
1242 \sdx{primrec} |
|
1243 "0 + n = n" |
|
1244 "Suc m + n = Suc (m + n)" |
|
1245 \end{ttbox} |
|
1246 There is also a \sdx{case}-construct |
|
1247 of the form |
|
1248 \begin{ttbox} |
|
1249 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) |
|
1250 \end{ttbox} |
|
1251 Note that Isabelle insists on precisely this format; you may not even change |
|
1252 the order of the two cases. |
|
1253 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator |
|
1254 \cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}. |
|
1255 |
|
1256 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. |
|
1257 %Recursion along this relation resembles primitive recursion, but is |
|
1258 %stronger because we are in higher-order logic; using primitive recursion to |
|
1259 %define a higher-order function, we can easily Ackermann's function, which |
|
1260 %is not primitive recursive \cite[page~104]{thompson91}. |
|
1261 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the |
|
1262 %natural numbers are most easily expressed using recursion along~$<$. |
|
1263 |
|
1264 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ |
|
1265 in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived |
|
1266 theorem \tdx{less_induct}: |
|
1267 \begin{ttbox} |
|
1268 [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n |
|
1269 \end{ttbox} |
|
1270 |
|
1271 |
|
1272 Reasoning about arithmetic inequalities can be tedious. Fortunately HOL |
|
1273 provides a decision procedure for quantifier-free linear arithmetic (i.e.\ |
|
1274 only addition and subtraction). The simplifier invokes a weak version of this |
|
1275 decision procedure automatically. If this is not sufficent, you can invoke |
|
1276 the full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary |
|
1277 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt |
|
1278 min}, {\tt max} and numerical constants; other subterms are treated as |
|
1279 atomic; subformulae not involving type $nat$ are ignored; quantified |
|
1280 subformulae are ignored unless they are positive universal or negative |
|
1281 existential. Note that the running time is exponential in the number of |
|
1282 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case |
|
1283 distinctions. Note also that \texttt{arith_tac} is not complete: if |
|
1284 divisibility plays a role, it may fail to prove a valid formula, for example |
|
1285 $m+m \neq n+n+1$. Fortunately such examples are rare in practice. |
|
1286 |
|
1287 If \texttt{arith_tac} fails you, try to find relevant arithmetic results in |
|
1288 the library. The theory \texttt{NatDef} contains theorems about {\tt<} and |
|
1289 {\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+}, |
|
1290 \texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about |
|
1291 \texttt{div} and \texttt{mod}. Use the \texttt{find}-functions to locate them |
|
1292 (see the {\em Reference Manual\/}). |
|
1293 |
|
1294 \begin{figure} |
|
1295 \index{#@{\tt[]} symbol} |
|
1296 \index{#@{\tt\#} symbol} |
|
1297 \index{"@@{\tt\at} symbol} |
|
1298 \index{*"! symbol} |
|
1299 \begin{constants} |
|
1300 \it symbol & \it meta-type & \it priority & \it description \\ |
|
1301 \tt[] & $\alpha\,list$ & & empty list\\ |
|
1302 \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & |
|
1303 list constructor \\ |
|
1304 \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\ |
|
1305 \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\ |
|
1306 \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\ |
|
1307 \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\ |
|
1308 \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\ |
|
1309 \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\ |
|
1310 \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$ |
|
1311 & & apply to all\\ |
|
1312 \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$ |
|
1313 & & filter functional\\ |
|
1314 \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\ |
|
1315 \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\ |
|
1316 \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ & |
|
1317 & iteration \\ |
|
1318 \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\ |
|
1319 \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\ |
|
1320 \cdx{length} & $\alpha\,list \To nat$ & & length \\ |
|
1321 \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\ |
|
1322 \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ && |
|
1323 take or drop a prefix \\ |
|
1324 \cdx{takeWhile},\\ |
|
1325 \cdx{dropWhile} & |
|
1326 $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ && |
|
1327 take or drop a prefix |
|
1328 \end{constants} |
|
1329 \subcaption{Constants and infixes} |
|
1330 |
|
1331 \begin{center} \tt\frenchspacing |
|
1332 \begin{tabular}{rrr} |
|
1333 \it external & \it internal & \it description \\{} |
|
1334 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] & |
|
1335 \rm finite list \\{} |
|
1336 [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ & |
|
1337 \rm list comprehension |
|
1338 \end{tabular} |
|
1339 \end{center} |
|
1340 \subcaption{Translations} |
|
1341 \caption{The theory \thydx{List}} \label{hol-list} |
|
1342 \end{figure} |
|
1343 |
|
1344 |
|
1345 \begin{figure} |
|
1346 \begin{ttbox}\makeatother |
|
1347 null [] = True |
|
1348 null (x#xs) = False |
|
1349 |
|
1350 hd (x#xs) = x |
|
1351 tl (x#xs) = xs |
|
1352 tl [] = [] |
|
1353 |
|
1354 [] @ ys = ys |
|
1355 (x#xs) @ ys = x # xs @ ys |
|
1356 |
|
1357 map f [] = [] |
|
1358 map f (x#xs) = f x # map f xs |
|
1359 |
|
1360 filter P [] = [] |
|
1361 filter P (x#xs) = (if P x then x#filter P xs else filter P xs) |
|
1362 |
|
1363 set [] = \ttlbrace\ttrbrace |
|
1364 set (x#xs) = insert x (set xs) |
|
1365 |
|
1366 x mem [] = False |
|
1367 x mem (y#ys) = (if y=x then True else x mem ys) |
|
1368 |
|
1369 foldl f a [] = a |
|
1370 foldl f a (x#xs) = foldl f (f a x) xs |
|
1371 |
|
1372 concat([]) = [] |
|
1373 concat(x#xs) = x @ concat(xs) |
|
1374 |
|
1375 rev([]) = [] |
|
1376 rev(x#xs) = rev(xs) @ [x] |
|
1377 |
|
1378 length([]) = 0 |
|
1379 length(x#xs) = Suc(length(xs)) |
|
1380 |
|
1381 xs!0 = hd xs |
|
1382 xs!(Suc n) = (tl xs)!n |
|
1383 |
|
1384 take n [] = [] |
|
1385 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs) |
|
1386 |
|
1387 drop n [] = [] |
|
1388 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs) |
|
1389 |
|
1390 takeWhile P [] = [] |
|
1391 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else []) |
|
1392 |
|
1393 dropWhile P [] = [] |
|
1394 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) |
|
1395 \end{ttbox} |
|
1396 \caption{Recursions equations for list processing functions} |
|
1397 \label{fig:HOL:list-simps} |
|
1398 \end{figure} |
|
1399 \index{nat@{\textit{nat}} type|)} |
|
1400 |
|
1401 |
|
1402 \subsection{The type constructor for lists, \textit{list}} |
|
1403 \label{subsec:list} |
|
1404 \index{list@{\textit{list}} type|(} |
|
1405 |
|
1406 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list |
|
1407 operations with their types and syntax. Type $\alpha \; list$ is |
|
1408 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}. |
|
1409 As a result the generic structural induction and case analysis tactics |
|
1410 \texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for |
|
1411 lists. A \sdx{case} construct of the form |
|
1412 \begin{center}\tt |
|
1413 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b |
|
1414 \end{center} |
|
1415 is defined by translation. For details see~\S\ref{sec:HOL:datatype}. There |
|
1416 is also a case splitting rule \tdx{split_list_case} |
|
1417 \[ |
|
1418 \begin{array}{l} |
|
1419 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~ |
|
1420 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\ |
|
1421 ((e = \texttt{[]} \to P(a)) \land |
|
1422 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs))) |
|
1423 \end{array} |
|
1424 \] |
|
1425 which can be fed to \ttindex{addsplits} just like |
|
1426 \texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}). |
|
1427 |
|
1428 \texttt{List} provides a basic library of list processing functions defined by |
|
1429 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations |
|
1430 are shown in Fig.\ts\ref{fig:HOL:list-simps}. |
|
1431 |
|
1432 \index{list@{\textit{list}} type|)} |
|
1433 |
|
1434 |
|
1435 \subsection{Introducing new types} \label{sec:typedef} |
|
1436 |
|
1437 The \HOL-methodology dictates that all extensions to a theory should |
|
1438 be \textbf{definitional}. The type definition mechanism that |
|
1439 meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms}, |
|
1440 which are inherited from {\Pure} and described elsewhere, are just |
|
1441 syntactic abbreviations that have no logical meaning. |
|
1442 |
|
1443 \begin{warn} |
|
1444 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be |
|
1445 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}. |
|
1446 \end{warn} |
|
1447 A \bfindex{type definition} identifies the new type with a subset of |
|
1448 an existing type. More precisely, the new type is defined by |
|
1449 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a |
|
1450 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$, |
|
1451 and the new type denotes this subset. New functions are defined that |
|
1452 establish an isomorphism between the new type and the subset. If |
|
1453 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$, |
|
1454 then the type definition creates a type constructor |
|
1455 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type. |
|
1456 |
|
1457 \begin{figure}[htbp] |
|
1458 \begin{rail} |
|
1459 typedef : 'typedef' ( () | '(' name ')') type '=' set witness; |
|
1460 |
|
1461 type : typevarlist name ( () | '(' infix ')' ); |
|
1462 set : string; |
|
1463 witness : () | '(' id ')'; |
|
1464 \end{rail} |
|
1465 \caption{Syntax of type definitions} |
|
1466 \label{fig:HOL:typedef} |
|
1467 \end{figure} |
|
1468 |
|
1469 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For |
|
1470 the definition of `typevarlist' and `infix' see |
|
1471 \iflabelundefined{chap:classical} |
|
1472 {the appendix of the {\em Reference Manual\/}}% |
|
1473 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the |
|
1474 following meaning: |
|
1475 \begin{description} |
|
1476 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with |
|
1477 optional infix annotation. |
|
1478 \item[\it name:] an alphanumeric name $T$ for the type constructor |
|
1479 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$. |
|
1480 \item[\it set:] the representing subset $A$. |
|
1481 \item[\it witness:] name of a theorem of the form $a:A$ proving |
|
1482 non-emptiness. It can be omitted in case Isabelle manages to prove |
|
1483 non-emptiness automatically. |
|
1484 \end{description} |
|
1485 If all context conditions are met (no duplicate type variables in |
|
1486 `typevarlist', no extra type variables in `set', and no free term variables |
|
1487 in `set'), the following components are added to the theory: |
|
1488 \begin{itemize} |
|
1489 \item a type $ty :: (term,\dots,term)term$ |
|
1490 \item constants |
|
1491 \begin{eqnarray*} |
|
1492 T &::& \tau\;set \\ |
|
1493 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\ |
|
1494 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty |
|
1495 \end{eqnarray*} |
|
1496 \item a definition and three axioms |
|
1497 \[ |
|
1498 \begin{array}{ll} |
|
1499 T{\tt_def} & T \equiv A \\ |
|
1500 {\tt Rep_}T & Rep_T\,x \in T \\ |
|
1501 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\ |
|
1502 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y |
|
1503 \end{array} |
|
1504 \] |
|
1505 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$ |
|
1506 and its inverse $Abs_T$. |
|
1507 \end{itemize} |
|
1508 Below are two simple examples of \HOL\ type definitions. Non-emptiness |
|
1509 is proved automatically here. |
|
1510 \begin{ttbox} |
|
1511 typedef unit = "{\ttlbrace}True{\ttrbrace}" |
|
1512 |
|
1513 typedef (prod) |
|
1514 ('a, 'b) "*" (infixr 20) |
|
1515 = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}" |
|
1516 \end{ttbox} |
|
1517 |
|
1518 Type definitions permit the introduction of abstract data types in a safe |
|
1519 way, namely by providing models based on already existing types. Given some |
|
1520 abstract axiomatic description $P$ of a type, this involves two steps: |
|
1521 \begin{enumerate} |
|
1522 \item Find an appropriate type $\tau$ and subset $A$ which has the desired |
|
1523 properties $P$, and make a type definition based on this representation. |
|
1524 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation. |
|
1525 \end{enumerate} |
|
1526 You can now forget about the representation and work solely in terms of the |
|
1527 abstract properties $P$. |
|
1528 |
|
1529 \begin{warn} |
|
1530 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by |
|
1531 declaring the type and its operations and by stating the desired axioms, you |
|
1532 should make sure the type has a non-empty model. You must also have a clause |
|
1533 \par |
|
1534 \begin{ttbox} |
|
1535 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term |
|
1536 \end{ttbox} |
|
1537 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the |
|
1538 class of all \HOL\ types. |
|
1539 \end{warn} |
|
1540 |
|
1541 |
|
1542 \section{Records} |
|
1543 |
|
1544 At a first approximation, records are just a minor generalisation of tuples, |
|
1545 where components may be addressed by labels instead of just position (think of |
|
1546 {\ML}, for example). The version of records offered by Isabelle/HOL is |
|
1547 slightly more advanced, though, supporting \emph{extensible record schemes}. |
|
1548 This admits operations that are polymorphic with respect to record extension, |
|
1549 yielding ``object-oriented'' effects like (single) inheritance. See also |
|
1550 \cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented |
|
1551 verification and record subtyping in HOL. |
|
1552 |
|
1553 |
|
1554 \subsection{Basics} |
|
1555 |
|
1556 Isabelle/HOL supports fixed and schematic records both at the level of terms |
|
1557 and types. The concrete syntax is as follows: |
|
1558 |
|
1559 \begin{center} |
|
1560 \begin{tabular}{l|l|l} |
|
1561 & record terms & record types \\ \hline |
|
1562 fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\ |
|
1563 schematic & $\record{x = a\fs y = b\fs \more = m}$ & |
|
1564 $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\ |
|
1565 \end{tabular} |
|
1566 \end{center} |
|
1567 |
|
1568 \noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}. |
|
1569 |
|
1570 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field |
|
1571 $y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$, |
|
1572 assuming that $a \ty A$ and $b \ty B$. |
|
1573 |
|
1574 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields |
|
1575 $x$ and $y$ as before, but also possibly further fields as indicated by the |
|
1576 ``$\more$'' notation (which is actually part of the syntax). The improper |
|
1577 field ``$\more$'' of a record scheme is called the \emph{more part}. |
|
1578 Logically it is just a free variable, which is occasionally referred to as |
|
1579 \emph{row variable} in the literature. The more part of a record scheme may |
|
1580 be instantiated by zero or more further components. For example, above scheme |
|
1581 might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$, |
|
1582 where $m'$ refers to a different more part. Fixed records are special |
|
1583 instances of record schemes, where ``$\more$'' is properly terminated by the |
|
1584 $() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an |
|
1585 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$. |
|
1586 |
|
1587 \medskip |
|
1588 |
|
1589 There are two key features that make extensible records in a simply typed |
|
1590 language like HOL feasible: |
|
1591 \begin{enumerate} |
|
1592 \item the more part is internalised, as a free term or type variable, |
|
1593 \item field names are externalised, they cannot be accessed within the logic |
|
1594 as first-class values. |
|
1595 \end{enumerate} |
|
1596 |
|
1597 \medskip |
|
1598 |
|
1599 In Isabelle/HOL record types have to be defined explicitly, fixing their field |
|
1600 names and types, and their (optional) parent record (see |
|
1601 \S\ref{sec:HOL:record-def}). Afterwards, records may be formed using above |
|
1602 syntax, while obeying the canonical order of fields as given by their |
|
1603 declaration. The record package also provides several operations like |
|
1604 selectors and updates (see \S\ref{sec:HOL:record-ops}), together with |
|
1605 characteristic properties (see \S\ref{sec:HOL:record-thms}). |
|
1606 |
|
1607 There is an example theory demonstrating most basic aspects of extensible |
|
1608 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources). |
|
1609 |
|
1610 |
|
1611 \subsection{Defining records}\label{sec:HOL:record-def} |
|
1612 |
|
1613 The theory syntax for record type definitions is shown in |
|
1614 Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see |
|
1615 \iflabelundefined{chap:classical} |
|
1616 {the appendix of the {\em Reference Manual\/}}% |
|
1617 {Appendix~\ref{app:TheorySyntax}}. |
|
1618 |
|
1619 \begin{figure}[htbp] |
|
1620 \begin{rail} |
|
1621 record : 'record' typevarlist name '=' parent (field +); |
|
1622 |
|
1623 parent : ( () | type '+'); |
|
1624 field : name '::' type; |
|
1625 \end{rail} |
|
1626 \caption{Syntax of record type definitions} |
|
1627 \label{fig:HOL:record} |
|
1628 \end{figure} |
|
1629 |
|
1630 A general \ttindex{record} specification is of the following form: |
|
1631 \[ |
|
1632 \mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~ |
|
1633 (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l |
|
1634 \] |
|
1635 where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$, |
|
1636 $\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$. |
|
1637 Type constructor $t$ has to be new, while $s$ has to specify an existing |
|
1638 record type. Furthermore, the $\vec c@l$ have to be distinct field names. |
|
1639 There has to be at least one field. |
|
1640 |
|
1641 In principle, field names may never be shared with other records. This is no |
|
1642 actual restriction in practice, since $\vec c@l$ are internally declared |
|
1643 within a separate name space qualified by the name $t$ of the record. |
|
1644 |
|
1645 \medskip |
|
1646 |
|
1647 Above definition introduces a new record type $(\vec\alpha@n) \, t$ by |
|
1648 extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty |
|
1649 \vec\sigma@l$. The parent record specification is optional, by omitting it |
|
1650 $t$ becomes a \emph{root record}. The hierarchy of all records declared |
|
1651 within a theory forms a forest structure, i.e.\ a set of trees, where any of |
|
1652 these is rooted by some root record. |
|
1653 |
|
1654 For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the |
|
1655 fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n, |
|
1656 \zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty |
|
1657 \vec\sigma@l\fs \more \ty \zeta}$. |
|
1658 |
|
1659 \medskip |
|
1660 |
|
1661 The following simple example defines a root record type $point$ with fields $x |
|
1662 \ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with |
|
1663 an additional $colour$ component. |
|
1664 |
|
1665 \begin{ttbox} |
|
1666 record point = |
|
1667 x :: nat |
|
1668 y :: nat |
|
1669 |
|
1670 record cpoint = point + |
|
1671 colour :: string |
|
1672 \end{ttbox} |
|
1673 |
|
1674 |
|
1675 \subsection{Record operations}\label{sec:HOL:record-ops} |
|
1676 |
|
1677 Any record definition of the form presented above produces certain standard |
|
1678 operations. Selectors and updates are provided for any field, including the |
|
1679 improper one ``$more$''. There are also cumulative record constructor |
|
1680 functions. |
|
1681 |
|
1682 To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$ |
|
1683 is a root record with fields $\vec c@l \ty \vec\sigma@l$. |
|
1684 |
|
1685 \medskip |
|
1686 |
|
1687 \textbf{Selectors} and \textbf{updates} are available for any field (including |
|
1688 ``$more$'') as follows: |
|
1689 \begin{matharray}{lll} |
|
1690 c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\ |
|
1691 c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To |
|
1692 \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} |
|
1693 \end{matharray} |
|
1694 |
|
1695 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates |
|
1696 term $x_update \, a \, r$. Repeated updates are also supported: $r \, |
|
1697 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as |
|
1698 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of |
|
1699 postfix notation the order of fields shown here is reverse than in the actual |
|
1700 term. This might lead to confusion in conjunction with proof tools like |
|
1701 ordered rewriting. |
|
1702 |
|
1703 Since repeated updates are just function applications, fields may be freely |
|
1704 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic |
|
1705 is concerned. Thus commutativity of updates can be proven within the logic |
|
1706 for any two fields, but not as a general theorem: fields are not first-class |
|
1707 values. |
|
1708 |
|
1709 \medskip |
|
1710 |
|
1711 \textbf{Make} operations provide cumulative record constructor functions: |
|
1712 \begin{matharray}{lll} |
|
1713 make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\ |
|
1714 make_scheme & \ty & \vec\sigma@l \To |
|
1715 \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\ |
|
1716 \end{matharray} |
|
1717 \noindent |
|
1718 These functions are curried. The corresponding definitions in terms of actual |
|
1719 record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$ |
|
1720 rewrites to $\record{x = a\fs y = b}$. |
|
1721 |
|
1722 \medskip |
|
1723 |
|
1724 Any of above selector, update and make operations are declared within a local |
|
1725 name space prefixed by the name $t$ of the record. In case that different |
|
1726 records share base names of fields, one has to qualify names explicitly (e.g.\ |
|
1727 $t\dtt c@i_update$). This is recommended especially for operations like |
|
1728 $make$ or $update_more$ that always have the same base name. Just use $t\dtt |
|
1729 make$ etc.\ to avoid confusion. |
|
1730 |
|
1731 \bigskip |
|
1732 |
|
1733 We reconsider the case of non-root records, which are derived of some parent |
|
1734 record. In general, the latter may depend on another parent as well, |
|
1735 resulting in a list of \emph{ancestor records}. Appending the lists of fields |
|
1736 of all ancestors results in a certain field prefix. The record package |
|
1737 automatically takes care of this by lifting operations over this context of |
|
1738 ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields |
|
1739 $\vec d@k \ty \vec\rho@k$, selectors will get the following types: |
|
1740 \begin{matharray}{lll} |
|
1741 c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta} |
|
1742 \To \sigma@i |
|
1743 \end{matharray} |
|
1744 \noindent |
|
1745 Update and make operations are analogous. |
|
1746 |
|
1747 |
|
1748 \subsection{Proof tools}\label{sec:HOL:record-thms} |
|
1749 |
|
1750 The record package provides the following proof rules for any record type $t$. |
|
1751 \begin{enumerate} |
|
1752 |
|
1753 \item Standard conversions (selectors or updates applied to record constructor |
|
1754 terms, make function definitions) are part of the standard simpset (via |
|
1755 \texttt{addsimps}). |
|
1756 |
|
1757 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' |
|
1758 \conj y=y'$ are made part of the standard simpset and claset (via |
|
1759 \texttt{addIffs}). |
|
1760 |
|
1761 \item A tactic for record field splitting (\ttindex{record_split_tac}) is made |
|
1762 part of the standard claset (via \texttt{addSWrapper}). This tactic is |
|
1763 based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, |
|
1764 b))$ for any field. |
|
1765 \end{enumerate} |
|
1766 |
|
1767 The first two kinds of rules are stored within the theory as $t\dtt simps$ and |
|
1768 $t\dtt iffs$, respectively. In some situations it might be appropriate to |
|
1769 expand the definitions of updates: $t\dtt updates$. Following a new trend in |
|
1770 Isabelle system architecture, these names are \emph{not} bound at the {\ML} |
|
1771 level, though. |
|
1772 |
|
1773 \medskip |
|
1774 |
|
1775 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs |
|
1776 concerning records. The basic idea is to make \ttindex{record_split_tac} |
|
1777 expand quantified record variables and then simplify by the conversion rules. |
|
1778 By using a combination of the simplifier and classical prover together with |
|
1779 the default simpset and claset, record problems should be solved with a single |
|
1780 stroke of \texttt{Auto_tac} or \texttt{Force_tac}. |
|
1781 |
|
1782 |
|
1783 \section{Datatype definitions} |
|
1784 \label{sec:HOL:datatype} |
|
1785 \index{*datatype|(} |
|
1786 |
|
1787 Inductive datatypes, similar to those of \ML, frequently appear in |
|
1788 applications of Isabelle/HOL. In principle, such types could be defined by |
|
1789 hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too |
|
1790 tedious. The \ttindex{datatype} definition package of \HOL\ automates such |
|
1791 chores. It generates an appropriate \texttt{typedef} based on a least |
|
1792 fixed-point construction, and proves freeness theorems and induction rules, as |
|
1793 well as theorems for recursion and case combinators. The user just has to |
|
1794 give a simple specification of new inductive types using a notation similar to |
|
1795 {\ML} or Haskell. |
|
1796 |
|
1797 The current datatype package can handle both mutual and indirect recursion. |
|
1798 It also offers to represent existing types as datatypes giving the advantage |
|
1799 of a more uniform view on standard theories. |
|
1800 |
|
1801 |
|
1802 \subsection{Basics} |
|
1803 \label{subsec:datatype:basics} |
|
1804 |
|
1805 A general \texttt{datatype} definition is of the following form: |
|
1806 \[ |
|
1807 \begin{array}{llcl} |
|
1808 \mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = & |
|
1809 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~ |
|
1810 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\ |
|
1811 & & \vdots \\ |
|
1812 \mathtt{and} & (\alpha@1,\ldots,\alpha@h)t@n & = & |
|
1813 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~ |
|
1814 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}} |
|
1815 \end{array} |
|
1816 \] |
|
1817 where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor |
|
1818 names and $\tau^j@{i,i'}$ are {\em admissible} types containing at |
|
1819 most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$ |
|
1820 occurring in a \texttt{datatype} definition is {\em admissible} iff |
|
1821 \begin{itemize} |
|
1822 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the |
|
1823 newly defined type constructors $t@1,\ldots,t@n$, or |
|
1824 \item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or |
|
1825 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is |
|
1826 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$ |
|
1827 are admissible types. |
|
1828 \end{itemize} |
|
1829 If some $(\alpha@1,\ldots,\alpha@h)t@{j'}$ occurs in a type $\tau^j@{i,i'}$ |
|
1830 of the form |
|
1831 \[ |
|
1832 (\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t' |
|
1833 \] |
|
1834 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple |
|
1835 example of a datatype is the type \texttt{list}, which can be defined by |
|
1836 \begin{ttbox} |
|
1837 datatype 'a list = Nil |
|
1838 | Cons 'a ('a list) |
|
1839 \end{ttbox} |
|
1840 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled |
|
1841 by the mutually recursive datatype definition |
|
1842 \begin{ttbox} |
|
1843 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) |
|
1844 | Sum ('a aexp) ('a aexp) |
|
1845 | Diff ('a aexp) ('a aexp) |
|
1846 | Var 'a |
|
1847 | Num nat |
|
1848 and 'a bexp = Less ('a aexp) ('a aexp) |
|
1849 | And ('a bexp) ('a bexp) |
|
1850 | Or ('a bexp) ('a bexp) |
|
1851 \end{ttbox} |
|
1852 The datatype \texttt{term}, which is defined by |
|
1853 \begin{ttbox} |
|
1854 datatype ('a, 'b) term = Var 'a |
|
1855 | App 'b ((('a, 'b) term) list) |
|
1856 \end{ttbox} |
|
1857 is an example for a datatype with nested recursion. |
|
1858 |
|
1859 \medskip |
|
1860 |
|
1861 Types in HOL must be non-empty. Each of the new datatypes |
|
1862 $(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a |
|
1863 constructor $C^j@i$ with the following property: for all argument types |
|
1864 $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype |
|
1865 $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty. |
|
1866 |
|
1867 If there are no nested occurrences of the newly defined datatypes, obviously |
|
1868 at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$ |
|
1869 must have a constructor $C^j@i$ without recursive arguments, a \emph{base |
|
1870 case}, to ensure that the new types are non-empty. If there are nested |
|
1871 occurrences, a datatype can even be non-empty without having a base case |
|
1872 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t |
|
1873 list)} is non-empty as well. |
|
1874 |
|
1875 |
|
1876 \subsubsection{Freeness of the constructors} |
|
1877 |
|
1878 The datatype constructors are automatically defined as functions of their |
|
1879 respective type: |
|
1880 \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \] |
|
1881 These functions have certain {\em freeness} properties. They construct |
|
1882 distinct values: |
|
1883 \[ |
|
1884 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad |
|
1885 \mbox{for all}~ i \neq i'. |
|
1886 \] |
|
1887 The constructor functions are injective: |
|
1888 \[ |
|
1889 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) = |
|
1890 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i}) |
|
1891 \] |
|
1892 Because the number of distinctness inequalities is quadratic in the number of |
|
1893 constructors, a different representation is used if there are $7$ or more of |
|
1894 them. In that case every constructor term is mapped to a natural number: |
|
1895 \[ |
|
1896 t@j_ord \, (C^j@i \, x@1 \, \dots \, x@{m^j@i}) = i - 1 |
|
1897 \] |
|
1898 Then distinctness of constructor terms is expressed by: |
|
1899 \[ |
|
1900 t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y. |
|
1901 \] |
|
1902 |
|
1903 \subsubsection{Structural induction} |
|
1904 |
|
1905 The datatype package also provides structural induction rules. For |
|
1906 datatypes without nested recursion, this is of the following form: |
|
1907 \[ |
|
1908 \infer{P@1~x@1 \wedge \dots \wedge P@n~x@n} |
|
1909 {\begin{array}{lcl} |
|
1910 \Forall x@1 \dots x@{m^1@1}. |
|
1911 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots; |
|
1912 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp & |
|
1913 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\ |
|
1914 & \vdots \\ |
|
1915 \Forall x@1 \dots x@{m^1@{k@1}}. |
|
1916 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots; |
|
1917 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp & |
|
1918 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\ |
|
1919 & \vdots \\ |
|
1920 \Forall x@1 \dots x@{m^n@1}. |
|
1921 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots; |
|
1922 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp & |
|
1923 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\ |
|
1924 & \vdots \\ |
|
1925 \Forall x@1 \dots x@{m^n@{k@n}}. |
|
1926 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots |
|
1927 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp & |
|
1928 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right) |
|
1929 \end{array}} |
|
1930 \] |
|
1931 where |
|
1932 \[ |
|
1933 \begin{array}{rcl} |
|
1934 Rec^j@i & := & |
|
1935 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, |
|
1936 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex] |
|
1937 && \left\{(i',i'')~\left|~ |
|
1938 1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge |
|
1939 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\} |
|
1940 \end{array} |
|
1941 \] |
|
1942 i.e.\ the properties $P@j$ can be assumed for all recursive arguments. |
|
1943 |
|
1944 For datatypes with nested recursion, such as the \texttt{term} example from |
|
1945 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds |
|
1946 a definition like |
|
1947 \begin{ttbox} |
|
1948 datatype ('a, 'b) term = Var 'a |
|
1949 | App 'b ((('a, 'b) term) list) |
|
1950 \end{ttbox} |
|
1951 to an equivalent definition without nesting: |
|
1952 \begin{ttbox} |
|
1953 datatype ('a, 'b) term = Var |
|
1954 | App 'b (('a, 'b) term_list) |
|
1955 and ('a, 'b) term_list = Nil' |
|
1956 | Cons' (('a,'b) term) (('a,'b) term_list) |
|
1957 \end{ttbox} |
|
1958 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt |
|
1959 Nil'} and \texttt{Cons'} are not really introduced. One can directly work with |
|
1960 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing |
|
1961 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for |
|
1962 \texttt{term} gets the form |
|
1963 \[ |
|
1964 \infer{P@1~x@1 \wedge P@2~x@2} |
|
1965 {\begin{array}{l} |
|
1966 \Forall x.~P@1~(\mathtt{Var}~x) \\ |
|
1967 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\ |
|
1968 P@2~\mathtt{Nil} \\ |
|
1969 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) |
|
1970 \end{array}} |
|
1971 \] |
|
1972 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} |
|
1973 and one for the type \texttt{(('a, 'b) term) list}. |
|
1974 |
|
1975 \medskip In principle, inductive types are already fully determined by |
|
1976 freeness and structural induction. For convenience in applications, |
|
1977 the following derived constructions are automatically provided for any |
|
1978 datatype. |
|
1979 |
|
1980 \subsubsection{The \sdx{case} construct} |
|
1981 |
|
1982 The type comes with an \ML-like \texttt{case}-construct: |
|
1983 \[ |
|
1984 \begin{array}{rrcl} |
|
1985 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\ |
|
1986 \vdots \\ |
|
1987 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j} |
|
1988 \end{array} |
|
1989 \] |
|
1990 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in |
|
1991 \S\ref{subsec:prod-sum}. |
|
1992 \begin{warn} |
|
1993 All constructors must be present, their order is fixed, and nested patterns |
|
1994 are not supported (with the exception of tuples). Violating this |
|
1995 restriction results in strange error messages. |
|
1996 \end{warn} |
|
1997 |
|
1998 To perform case distinction on a goal containing a \texttt{case}-construct, |
|
1999 the theorem $t@j.$\texttt{split} is provided: |
|
2000 \[ |
|
2001 \begin{array}{@{}rcl@{}} |
|
2002 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=& |
|
2003 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to |
|
2004 P(f@1~x@1\dots x@{m^j@1})) \\ |
|
2005 &&\!\!\! ~\land~ \dots ~\land \\ |
|
2006 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to |
|
2007 P(f@{k@j}~x@1\dots x@{m^j@{k@j}}))) |
|
2008 \end{array} |
|
2009 \] |
|
2010 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct. |
|
2011 This theorem can be added to a simpset via \ttindex{addsplits} |
|
2012 (see~\S\ref{subsec:HOL:case:splitting}). |
|
2013 |
|
2014 \subsubsection{The function \cdx{size}}\label{sec:HOL:size} |
|
2015 |
|
2016 Theory \texttt{Arith} declares a generic function \texttt{size} of type |
|
2017 $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} |
|
2018 by overloading according to the following scheme: |
|
2019 %%% FIXME: This formula is too big and is completely unreadable |
|
2020 \[ |
|
2021 size(C^j@i~x@1~\dots~x@{m^j@i}) = \! |
|
2022 \left\{ |
|
2023 \begin{array}{ll} |
|
2024 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\ |
|
2025 \!\!\begin{array}{l} |
|
2026 size~x@{r^j@{i,1}} + \cdots \\ |
|
2027 \cdots + size~x@{r^j@{i,l^j@i}} + 1 |
|
2028 \end{array} & |
|
2029 \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, |
|
2030 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$} |
|
2031 \end{array} |
|
2032 \right. |
|
2033 \] |
|
2034 where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the |
|
2035 size of a leaf is 0 and the size of a node is the sum of the sizes of its |
|
2036 subtrees ${}+1$. |
|
2037 |
|
2038 \subsection{Defining datatypes} |
|
2039 |
|
2040 The theory syntax for datatype definitions is shown in |
|
2041 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype |
|
2042 definition has to obey the rules stated in the previous section. As a result |
|
2043 the theory is extended with the new types, the constructors, and the theorems |
|
2044 listed in the previous section. |
|
2045 |
|
2046 \begin{figure} |
|
2047 \begin{rail} |
|
2048 datatype : 'datatype' typedecls; |
|
2049 |
|
2050 typedecls: ( newtype '=' (cons + '|') ) + 'and' |
|
2051 ; |
|
2052 newtype : typevarlist id ( () | '(' infix ')' ) |
|
2053 ; |
|
2054 cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) |
|
2055 ; |
|
2056 argtype : id | tid | ('(' typevarlist id ')') |
|
2057 ; |
|
2058 \end{rail} |
|
2059 \caption{Syntax of datatype declarations} |
|
2060 \label{datatype-grammar} |
|
2061 \end{figure} |
|
2062 |
|
2063 Most of the theorems about datatypes become part of the default simpset and |
|
2064 you never need to see them again because the simplifier applies them |
|
2065 automatically. Only induction or exhaustion are usually invoked by hand. |
|
2066 \begin{ttdescription} |
|
2067 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] |
|
2068 applies structural induction on variable $x$ to subgoal $i$, provided the |
|
2069 type of $x$ is a datatype. |
|
2070 \item[\ttindexbold{mutual_induct_tac} |
|
2071 {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous |
|
2072 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This |
|
2073 is the canonical way to prove properties of mutually recursive datatypes |
|
2074 such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as |
|
2075 \texttt{term}. |
|
2076 \end{ttdescription} |
|
2077 In some cases, induction is overkill and a case distinction over all |
|
2078 constructors of the datatype suffices. |
|
2079 \begin{ttdescription} |
|
2080 \item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$] |
|
2081 performs an exhaustive case analysis for the term $u$ whose type |
|
2082 must be a datatype. If the datatype has $k@j$ constructors |
|
2083 $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which |
|
2084 contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for |
|
2085 $i'=1$, $\dots$,~$k@j$. |
|
2086 \end{ttdescription} |
|
2087 |
|
2088 Note that induction is only allowed on free variables that should not occur |
|
2089 among the premises of the subgoal. Exhaustion applies to arbitrary terms. |
|
2090 |
|
2091 \bigskip |
|
2092 |
|
2093 |
|
2094 For the technically minded, we exhibit some more details. Processing the |
|
2095 theory file produces an \ML\ structure which, in addition to the usual |
|
2096 components, contains a structure named $t$ for each datatype $t$ defined in |
|
2097 the file. Each structure $t$ contains the following elements: |
|
2098 \begin{ttbox} |
|
2099 val distinct : thm list |
|
2100 val inject : thm list |
|
2101 val induct : thm |
|
2102 val exhaust : thm |
|
2103 val cases : thm list |
|
2104 val split : thm |
|
2105 val split_asm : thm |
|
2106 val recs : thm list |
|
2107 val size : thm list |
|
2108 val simps : thm list |
|
2109 \end{ttbox} |
|
2110 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} |
|
2111 and \texttt{split} contain the theorems |
|
2112 described above. For user convenience, \texttt{distinct} contains |
|
2113 inequalities in both directions. The reduction rules of the {\tt |
|
2114 case}-construct are in \texttt{cases}. All theorems from {\tt |
|
2115 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. |
|
2116 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} |
|
2117 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. |
|
2118 |
|
2119 |
|
2120 \subsection{Representing existing types as datatypes} |
|
2121 |
|
2122 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt |
|
2123 +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section, |
|
2124 but by more primitive means using \texttt{typedef}. To be able to use the |
|
2125 tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by |
|
2126 primitive recursion on these types, such types may be represented as actual |
|
2127 datatypes. This is done by specifying an induction rule, as well as theorems |
|
2128 stating the distinctness and injectivity of constructors in a {\tt |
|
2129 rep_datatype} section. For type \texttt{nat} this works as follows: |
|
2130 \begin{ttbox} |
|
2131 rep_datatype nat |
|
2132 distinct Suc_not_Zero, Zero_not_Suc |
|
2133 inject Suc_Suc_eq |
|
2134 induct nat_induct |
|
2135 \end{ttbox} |
|
2136 The datatype package automatically derives additional theorems for recursion |
|
2137 and case combinators from these rules. Any of the basic HOL types mentioned |
|
2138 above are represented as datatypes. Try an induction on \texttt{bool} |
|
2139 today. |
|
2140 |
|
2141 |
|
2142 \subsection{Examples} |
|
2143 |
|
2144 \subsubsection{The datatype $\alpha~mylist$} |
|
2145 |
|
2146 We want to define a type $\alpha~mylist$. To do this we have to build a new |
|
2147 theory that contains the type definition. We start from the theory |
|
2148 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the |
|
2149 \texttt{List} theory of Isabelle/HOL. |
|
2150 \begin{ttbox} |
|
2151 MyList = Datatype + |
|
2152 datatype 'a mylist = Nil | Cons 'a ('a mylist) |
|
2153 end |
|
2154 \end{ttbox} |
|
2155 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To |
|
2156 ease the induction applied below, we state the goal with $x$ quantified at the |
|
2157 object-level. This will be stripped later using \ttindex{qed_spec_mp}. |
|
2158 \begin{ttbox} |
|
2159 Goal "!x. Cons x xs ~= xs"; |
|
2160 {\out Level 0} |
|
2161 {\out ! x. Cons x xs ~= xs} |
|
2162 {\out 1. ! x. Cons x xs ~= xs} |
|
2163 \end{ttbox} |
|
2164 This can be proved by the structural induction tactic: |
|
2165 \begin{ttbox} |
|
2166 by (induct_tac "xs" 1); |
|
2167 {\out Level 1} |
|
2168 {\out ! x. Cons x xs ~= xs} |
|
2169 {\out 1. ! x. Cons x Nil ~= Nil} |
|
2170 {\out 2. !!a mylist.} |
|
2171 {\out ! x. Cons x mylist ~= mylist ==>} |
|
2172 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist} |
|
2173 \end{ttbox} |
|
2174 The first subgoal can be proved using the simplifier. Isabelle/HOL has |
|
2175 already added the freeness properties of lists to the default simplification |
|
2176 set. |
|
2177 \begin{ttbox} |
|
2178 by (Simp_tac 1); |
|
2179 {\out Level 2} |
|
2180 {\out ! x. Cons x xs ~= xs} |
|
2181 {\out 1. !!a mylist.} |
|
2182 {\out ! x. Cons x mylist ~= mylist ==>} |
|
2183 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist} |
|
2184 \end{ttbox} |
|
2185 Similarly, we prove the remaining goal. |
|
2186 \begin{ttbox} |
|
2187 by (Asm_simp_tac 1); |
|
2188 {\out Level 3} |
|
2189 {\out ! x. Cons x xs ~= xs} |
|
2190 {\out No subgoals!} |
|
2191 \ttbreak |
|
2192 qed_spec_mp "not_Cons_self"; |
|
2193 {\out val not_Cons_self = "Cons x xs ~= xs" : thm} |
|
2194 \end{ttbox} |
|
2195 Because both subgoals could have been proved by \texttt{Asm_simp_tac} |
|
2196 we could have done that in one step: |
|
2197 \begin{ttbox} |
|
2198 by (ALLGOALS Asm_simp_tac); |
|
2199 \end{ttbox} |
|
2200 |
|
2201 |
|
2202 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax} |
|
2203 |
|
2204 In this example we define the type $\alpha~mylist$ again but this time |
|
2205 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix |
|
2206 notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix |
|
2207 annotations after the constructor declarations as follows: |
|
2208 \begin{ttbox} |
|
2209 MyList = Datatype + |
|
2210 datatype 'a mylist = |
|
2211 Nil ("[]") | |
|
2212 Cons 'a ('a mylist) (infixr "#" 70) |
|
2213 end |
|
2214 \end{ttbox} |
|
2215 Now the theorem in the previous example can be written \verb|x#xs ~= xs|. |
|
2216 |
|
2217 |
|
2218 \subsubsection{A datatype for weekdays} |
|
2219 |
|
2220 This example shows a datatype that consists of 7 constructors: |
|
2221 \begin{ttbox} |
|
2222 Days = Main + |
|
2223 datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun |
|
2224 end |
|
2225 \end{ttbox} |
|
2226 Because there are more than 6 constructors, inequality is expressed via a function |
|
2227 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly |
|
2228 contained among the distinctness theorems, but the simplifier can |
|
2229 prove it thanks to rewrite rules inherited from theory \texttt{Arith}: |
|
2230 \begin{ttbox} |
|
2231 Goal "Mon ~= Tue"; |
|
2232 by (Simp_tac 1); |
|
2233 \end{ttbox} |
|
2234 You need not derive such inequalities explicitly: the simplifier will dispose |
|
2235 of them automatically. |
|
2236 \index{*datatype|)} |
|
2237 |
|
2238 |
|
2239 \section{Recursive function definitions}\label{sec:HOL:recursive} |
|
2240 \index{recursive functions|see{recursion}} |
|
2241 |
|
2242 Isabelle/HOL provides two main mechanisms of defining recursive functions. |
|
2243 \begin{enumerate} |
|
2244 \item \textbf{Primitive recursion} is available only for datatypes, and it is |
|
2245 somewhat restrictive. Recursive calls are only allowed on the argument's |
|
2246 immediate constituents. On the other hand, it is the form of recursion most |
|
2247 often wanted, and it is easy to use. |
|
2248 |
|
2249 \item \textbf{Well-founded recursion} requires that you supply a well-founded |
|
2250 relation that governs the recursion. Recursive calls are only allowed if |
|
2251 they make the argument decrease under the relation. Complicated recursion |
|
2252 forms, such as nested recursion, can be dealt with. Termination can even be |
|
2253 proved at a later time, though having unsolved termination conditions around |
|
2254 can make work difficult.% |
|
2255 \footnote{This facility is based on Konrad Slind's TFL |
|
2256 package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL |
|
2257 and assisting with its installation.} |
|
2258 \end{enumerate} |
|
2259 |
|
2260 Following good HOL tradition, these declarations do not assert arbitrary |
|
2261 axioms. Instead, they define the function using a recursion operator. Both |
|
2262 HOL and ZF derive the theory of well-founded recursion from first |
|
2263 principles~\cite{paulson-set-II}. Primitive recursion over some datatype |
|
2264 relies on the recursion operator provided by the datatype package. With |
|
2265 either form of function definition, Isabelle proves the desired recursion |
|
2266 equations as theorems. |
|
2267 |
|
2268 |
|
2269 \subsection{Primitive recursive functions} |
|
2270 \label{sec:HOL:primrec} |
|
2271 \index{recursion!primitive|(} |
|
2272 \index{*primrec|(} |
|
2273 |
|
2274 Datatypes come with a uniform way of defining functions, {\bf primitive |
|
2275 recursion}. In principle, one could introduce primitive recursive functions |
|
2276 by asserting their reduction rules as new axioms, but this is not recommended: |
|
2277 \begin{ttbox}\slshape |
|
2278 Append = Main + |
|
2279 consts app :: ['a list, 'a list] => 'a list |
|
2280 rules |
|
2281 app_Nil "app [] ys = ys" |
|
2282 app_Cons "app (x#xs) ys = x#app xs ys" |
|
2283 end |
|
2284 \end{ttbox} |
|
2285 Asserting axioms brings the danger of accidentally asserting nonsense, as |
|
2286 in \verb$app [] ys = us$. |
|
2287 |
|
2288 The \ttindex{primrec} declaration is a safe means of defining primitive |
|
2289 recursive functions on datatypes: |
|
2290 \begin{ttbox} |
|
2291 Append = Main + |
|
2292 consts app :: ['a list, 'a list] => 'a list |
|
2293 primrec |
|
2294 "app [] ys = ys" |
|
2295 "app (x#xs) ys = x#app xs ys" |
|
2296 end |
|
2297 \end{ttbox} |
|
2298 Isabelle will now check that the two rules do indeed form a primitive |
|
2299 recursive definition. For example |
|
2300 \begin{ttbox} |
|
2301 primrec |
|
2302 "app [] ys = us" |
|
2303 \end{ttbox} |
|
2304 is rejected with an error message ``\texttt{Extra variables on rhs}''. |
|
2305 |
|
2306 \bigskip |
|
2307 |
|
2308 The general form of a primitive recursive definition is |
|
2309 \begin{ttbox} |
|
2310 primrec |
|
2311 {\it reduction rules} |
|
2312 \end{ttbox} |
|
2313 where \textit{reduction rules} specify one or more equations of the form |
|
2314 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, |
|
2315 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$ |
|
2316 contains only the free variables on the left-hand side, and all recursive |
|
2317 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There |
|
2318 must be at most one reduction rule for each constructor. The order is |
|
2319 immaterial. For missing constructors, the function is defined to return a |
|
2320 default value. |
|
2321 |
|
2322 If you would like to refer to some rule by name, then you must prefix |
|
2323 the rule with an identifier. These identifiers, like those in the |
|
2324 \texttt{rules} section of a theory, will be visible at the \ML\ level. |
|
2325 |
|
2326 The primitive recursive function can have infix or mixfix syntax: |
|
2327 \begin{ttbox}\underscoreon |
|
2328 consts "@" :: ['a list, 'a list] => 'a list (infixr 60) |
|
2329 primrec |
|
2330 "[] @ ys = ys" |
|
2331 "(x#xs) @ ys = x#(xs @ ys)" |
|
2332 \end{ttbox} |
|
2333 |
|
2334 The reduction rules become part of the default simpset, which |
|
2335 leads to short proof scripts: |
|
2336 \begin{ttbox}\underscoreon |
|
2337 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
|
2338 by (induct\_tac "xs" 1); |
|
2339 by (ALLGOALS Asm\_simp\_tac); |
|
2340 \end{ttbox} |
|
2341 |
|
2342 \subsubsection{Example: Evaluation of expressions} |
|
2343 Using mutual primitive recursion, we can define evaluation functions \texttt{eval_aexp} |
|
2344 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in |
|
2345 \S\ref{subsec:datatype:basics}: |
|
2346 \begin{ttbox} |
|
2347 consts |
|
2348 eval_aexp :: "['a => nat, 'a aexp] => nat" |
|
2349 eval_bexp :: "['a => nat, 'a bexp] => bool" |
|
2350 |
|
2351 primrec |
|
2352 "eval_aexp env (If_then_else b a1 a2) = |
|
2353 (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)" |
|
2354 "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2" |
|
2355 "eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2" |
|
2356 "eval_aexp env (Var v) = env v" |
|
2357 "eval_aexp env (Num n) = n" |
|
2358 |
|
2359 "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)" |
|
2360 "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)" |
|
2361 "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)" |
|
2362 \end{ttbox} |
|
2363 Since the value of an expression depends on the value of its variables, |
|
2364 the functions \texttt{eval_aexp} and \texttt{eval_bexp} take an additional |
|
2365 parameter, an {\em environment} of type \texttt{'a => nat}, which maps |
|
2366 variables to their values. |
|
2367 |
|
2368 Similarly, we may define substitution functions \texttt{subst_aexp} |
|
2369 and \texttt{subst_bexp} for expressions: The mapping \texttt{f} of type |
|
2370 \texttt{'a => 'a aexp} given as a parameter is lifted canonically |
|
2371 on the types {'a aexp} and {'a bexp}: |
|
2372 \begin{ttbox} |
|
2373 consts |
|
2374 subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp" |
|
2375 subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp" |
|
2376 |
|
2377 primrec |
|
2378 "subst_aexp f (If_then_else b a1 a2) = |
|
2379 If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)" |
|
2380 "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)" |
|
2381 "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)" |
|
2382 "subst_aexp f (Var v) = f v" |
|
2383 "subst_aexp f (Num n) = Num n" |
|
2384 |
|
2385 "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)" |
|
2386 "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)" |
|
2387 "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)" |
|
2388 \end{ttbox} |
|
2389 In textbooks about semantics one often finds {\em substitution theorems}, |
|
2390 which express the relationship between substitution and evaluation. For |
|
2391 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual |
|
2392 induction, followed by simplification: |
|
2393 \begin{ttbox} |
|
2394 Goal |
|
2395 "eval_aexp env (subst_aexp (Var(v := a')) a) = |
|
2396 eval_aexp (env(v := eval_aexp env a')) a & |
|
2397 eval_bexp env (subst_bexp (Var(v := a')) b) = |
|
2398 eval_bexp (env(v := eval_aexp env a')) b"; |
|
2399 by (mutual_induct_tac ["a","b"] 1); |
|
2400 by (ALLGOALS Asm_full_simp_tac); |
|
2401 \end{ttbox} |
|
2402 |
|
2403 \subsubsection{Example: A substitution function for terms} |
|
2404 Functions on datatypes with nested recursion, such as the type |
|
2405 \texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are |
|
2406 also defined by mutual primitive recursion. A substitution |
|
2407 function \texttt{subst_term} on type \texttt{term}, similar to the functions |
|
2408 \texttt{subst_aexp} and \texttt{subst_bexp} described above, can |
|
2409 be defined as follows: |
|
2410 \begin{ttbox} |
|
2411 consts |
|
2412 subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term" |
|
2413 subst_term_list :: |
|
2414 "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list" |
|
2415 |
|
2416 primrec |
|
2417 "subst_term f (Var a) = f a" |
|
2418 "subst_term f (App b ts) = App b (subst_term_list f ts)" |
|
2419 |
|
2420 "subst_term_list f [] = []" |
|
2421 "subst_term_list f (t # ts) = |
|
2422 subst_term f t # subst_term_list f ts" |
|
2423 \end{ttbox} |
|
2424 The recursion scheme follows the structure of the unfolded definition of type |
|
2425 \texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of |
|
2426 this substitution function, mutual induction is needed: |
|
2427 \begin{ttbox} |
|
2428 Goal |
|
2429 "(subst_term ((subst_term f1) o f2) t) = |
|
2430 (subst_term f1 (subst_term f2 t)) & |
|
2431 (subst_term_list ((subst_term f1) o f2) ts) = |
|
2432 (subst_term_list f1 (subst_term_list f2 ts))"; |
|
2433 by (mutual_induct_tac ["t", "ts"] 1); |
|
2434 by (ALLGOALS Asm_full_simp_tac); |
|
2435 \end{ttbox} |
|
2436 |
|
2437 \index{recursion!primitive|)} |
|
2438 \index{*primrec|)} |
|
2439 |
|
2440 |
|
2441 \subsection{General recursive functions} |
|
2442 \label{sec:HOL:recdef} |
|
2443 \index{recursion!general|(} |
|
2444 \index{*recdef|(} |
|
2445 |
|
2446 Using \texttt{recdef}, you can declare functions involving nested recursion |
|
2447 and pattern-matching. Recursion need not involve datatypes and there are few |
|
2448 syntactic restrictions. Termination is proved by showing that each recursive |
|
2449 call makes the argument smaller in a suitable sense, which you specify by |
|
2450 supplying a well-founded relation. |
|
2451 |
|
2452 Here is a simple example, the Fibonacci function. The first line declares |
|
2453 \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on |
|
2454 the natural numbers). Pattern-matching is used here: \texttt{1} is a |
|
2455 macro for \texttt{Suc~0}. |
|
2456 \begin{ttbox} |
|
2457 consts fib :: "nat => nat" |
|
2458 recdef fib "less_than" |
|
2459 "fib 0 = 0" |
|
2460 "fib 1 = 1" |
|
2461 "fib (Suc(Suc x)) = (fib x + fib (Suc x))" |
|
2462 \end{ttbox} |
|
2463 |
|
2464 With \texttt{recdef}, function definitions may be incomplete, and patterns may |
|
2465 overlap, as in functional programming. The \texttt{recdef} package |
|
2466 disambiguates overlapping patterns by taking the order of rules into account. |
|
2467 For missing patterns, the function is defined to return a default value. |
|
2468 |
|
2469 %For example, here is a declaration of the list function \cdx{hd}: |
|
2470 %\begin{ttbox} |
|
2471 %consts hd :: 'a list => 'a |
|
2472 %recdef hd "\{\}" |
|
2473 % "hd (x#l) = x" |
|
2474 %\end{ttbox} |
|
2475 %Because this function is not recursive, we may supply the empty well-founded |
|
2476 %relation, $\{\}$. |
|
2477 |
|
2478 The well-founded relation defines a notion of ``smaller'' for the function's |
|
2479 argument type. The relation $\prec$ is \textbf{well-founded} provided it |
|
2480 admits no infinitely decreasing chains |
|
2481 \[ \cdots\prec x@n\prec\cdots\prec x@1. \] |
|
2482 If the function's argument has type~$\tau$, then $\prec$ has to be a relation |
|
2483 over~$\tau$: it must have type $(\tau\times\tau)set$. |
|
2484 |
|
2485 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection |
|
2486 of operators for building well-founded relations. The package recognises |
|
2487 these operators and automatically proves that the constructed relation is |
|
2488 well-founded. Here are those operators, in order of importance: |
|
2489 \begin{itemize} |
|
2490 \item \texttt{less_than} is ``less than'' on the natural numbers. |
|
2491 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. |
|
2492 |
|
2493 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the |
|
2494 relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$. |
|
2495 Typically, $f$ takes the recursive function's arguments (as a tuple) and |
|
2496 returns a result expressed in terms of the function \texttt{size}. It is |
|
2497 called a \textbf{measure function}. Recall that \texttt{size} is overloaded |
|
2498 and is defined on all datatypes (see \S\ref{sec:HOL:size}). |
|
2499 |
|
2500 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of |
|
2501 \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$ |
|
2502 is less than $f(y)$ according to~$R$, which must itself be a well-founded |
|
2503 relation. |
|
2504 |
|
2505 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It |
|
2506 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$ |
|
2507 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ |
|
2508 is less than $y@2$ according to~$R@2$. |
|
2509 |
|
2510 \item \texttt{finite_psubset} is the proper subset relation on finite sets. |
|
2511 \end{itemize} |
|
2512 |
|
2513 We can use \texttt{measure} to declare Euclid's algorithm for the greatest |
|
2514 common divisor. The measure function, $\lambda(m,n). n$, specifies that the |
|
2515 recursion terminates because argument~$n$ decreases. |
|
2516 \begin{ttbox} |
|
2517 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" |
|
2518 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
|
2519 \end{ttbox} |
|
2520 |
|
2521 The general form of a well-founded recursive definition is |
|
2522 \begin{ttbox} |
|
2523 recdef {\it function} {\it rel} |
|
2524 congs {\it congruence rules} {\bf(optional)} |
|
2525 simpset {\it simplification set} {\bf(optional)} |
|
2526 {\it reduction rules} |
|
2527 \end{ttbox} |
|
2528 where |
|
2529 \begin{itemize} |
|
2530 \item \textit{function} is the name of the function, either as an \textit{id} |
|
2531 or a \textit{string}. |
|
2532 |
|
2533 \item \textit{rel} is a {\HOL} expression for the well-founded termination |
|
2534 relation. |
|
2535 |
|
2536 \item \textit{congruence rules} are required only in highly exceptional |
|
2537 circumstances. |
|
2538 |
|
2539 \item The \textit{simplification set} is used to prove that the supplied |
|
2540 relation is well-founded. It is also used to prove the \textbf{termination |
|
2541 conditions}: assertions that arguments of recursive calls decrease under |
|
2542 \textit{rel}. By default, simplification uses \texttt{simpset()}, which |
|
2543 is sufficient to prove well-foundedness for the built-in relations listed |
|
2544 above. |
|
2545 |
|
2546 \item \textit{reduction rules} specify one or more recursion equations. Each |
|
2547 left-hand side must have the form $f\,t$, where $f$ is the function and $t$ |
|
2548 is a tuple of distinct variables. If more than one equation is present then |
|
2549 $f$ is defined by pattern-matching on components of its argument whose type |
|
2550 is a \texttt{datatype}. |
|
2551 |
|
2552 Unlike with \texttt{primrec}, the reduction rules are not added to the |
|
2553 default simpset, and individual rules may not be labelled with identifiers. |
|
2554 However, the identifier $f$\texttt{.rules} is visible at the \ML\ level |
|
2555 as a list of theorems. |
|
2556 \end{itemize} |
|
2557 |
|
2558 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to |
|
2559 prove one termination condition. It remains as a precondition of the |
|
2560 recursion theorems. |
|
2561 \begin{ttbox} |
|
2562 gcd.rules; |
|
2563 {\out ["! m n. n ~= 0 --> m mod n < n} |
|
2564 {\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] } |
|
2565 {\out : thm list} |
|
2566 \end{ttbox} |
|
2567 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination |
|
2568 conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard |
|
2569 function \texttt{goalw}, which sets up a goal to prove, but its argument |
|
2570 should be the identifier $f$\texttt{.rules} and its effect is to set up a |
|
2571 proof of the termination conditions: |
|
2572 \begin{ttbox} |
|
2573 Tfl.tgoalw thy [] gcd.rules; |
|
2574 {\out Level 0} |
|
2575 {\out ! m n. n ~= 0 --> m mod n < n} |
|
2576 {\out 1. ! m n. n ~= 0 --> m mod n < n} |
|
2577 \end{ttbox} |
|
2578 This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem |
|
2579 is proved, it can be used to eliminate the termination conditions from |
|
2580 elements of \texttt{gcd.rules}. Theory \texttt{HOL/Subst/Unify} is a much |
|
2581 more complicated example of this process, where the termination conditions can |
|
2582 only be proved by complicated reasoning involving the recursive function |
|
2583 itself. |
|
2584 |
|
2585 Isabelle/HOL can prove the \texttt{gcd} function's termination condition |
|
2586 automatically if supplied with the right simpset. |
|
2587 \begin{ttbox} |
|
2588 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" |
|
2589 simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" |
|
2590 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
|
2591 \end{ttbox} |
|
2592 |
|
2593 A \texttt{recdef} definition also returns an induction rule specialised for |
|
2594 the recursive function. For the \texttt{gcd} function above, the induction |
|
2595 rule is |
|
2596 \begin{ttbox} |
|
2597 gcd.induct; |
|
2598 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} |
|
2599 \end{ttbox} |
|
2600 This rule should be used to reason inductively about the \texttt{gcd} |
|
2601 function. It usually makes the induction hypothesis available at all |
|
2602 recursive calls, leading to very direct proofs. If any termination conditions |
|
2603 remain unproved, they will become additional premises of this rule. |
|
2604 |
|
2605 \index{recursion!general|)} |
|
2606 \index{*recdef|)} |
|
2607 |
|
2608 |
|
2609 \section{Inductive and coinductive definitions} |
|
2610 \index{*inductive|(} |
|
2611 \index{*coinductive|(} |
|
2612 |
|
2613 An {\bf inductive definition} specifies the least set~$R$ closed under given |
|
2614 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For |
|
2615 example, a structural operational semantics is an inductive definition of an |
|
2616 evaluation relation. Dually, a {\bf coinductive definition} specifies the |
|
2617 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be |
|
2618 seen as arising by applying a rule to elements of~$R$.) An important example |
|
2619 is using bisimulation relations to formalise equivalence of processes and |
|
2620 infinite data structures. |
|
2621 |
|
2622 A theory file may contain any number of inductive and coinductive |
|
2623 definitions. They may be intermixed with other declarations; in |
|
2624 particular, the (co)inductive sets {\bf must} be declared separately as |
|
2625 constants, and may have mixfix syntax or be subject to syntax translations. |
|
2626 |
|
2627 Each (co)inductive definition adds definitions to the theory and also |
|
2628 proves some theorems. Each definition creates an \ML\ structure, which is a |
|
2629 substructure of the main theory structure. |
|
2630 |
|
2631 This package is related to the \ZF\ one, described in a separate |
|
2632 paper,% |
|
2633 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is |
|
2634 distributed with Isabelle.} % |
|
2635 which you should refer to in case of difficulties. The package is simpler |
|
2636 than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types |
|
2637 of the (co)inductive sets determine the domain of the fixedpoint definition, |
|
2638 and the package does not have to use inference rules for type-checking. |
|
2639 |
|
2640 |
|
2641 \subsection{The result structure} |
|
2642 Many of the result structure's components have been discussed in the paper; |
|
2643 others are self-explanatory. |
|
2644 \begin{description} |
|
2645 \item[\tt defs] is the list of definitions of the recursive sets. |
|
2646 |
|
2647 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator. |
|
2648 |
|
2649 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of |
|
2650 the recursive sets, in the case of mutual recursion). |
|
2651 |
|
2652 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for |
|
2653 the recursive sets. The rules are also available individually, using the |
|
2654 names given them in the theory file. |
|
2655 |
|
2656 \item[\tt elims] is the list of elimination rule. |
|
2657 |
|
2658 \item[\tt elim] is the head of the list \texttt{elims}. |
|
2659 |
|
2660 \item[\tt mk_cases] is a function to create simplified instances of {\tt |
|
2661 elim} using freeness reasoning on underlying datatypes. |
|
2662 \end{description} |
|
2663 |
|
2664 For an inductive definition, the result structure contains the |
|
2665 rule \texttt{induct}. For a |
|
2666 coinductive definition, it contains the rule \verb|coinduct|. |
|
2667 |
|
2668 Figure~\ref{def-result-fig} summarises the two result signatures, |
|
2669 specifying the types of all these components. |
|
2670 |
|
2671 \begin{figure} |
|
2672 \begin{ttbox} |
|
2673 sig |
|
2674 val defs : thm list |
|
2675 val mono : thm |
|
2676 val unfold : thm |
|
2677 val intrs : thm list |
|
2678 val elims : thm list |
|
2679 val elim : thm |
|
2680 val mk_cases : string -> thm |
|
2681 {\it(Inductive definitions only)} |
|
2682 val induct : thm |
|
2683 {\it(coinductive definitions only)} |
|
2684 val coinduct : thm |
|
2685 end |
|
2686 \end{ttbox} |
|
2687 \hrule |
|
2688 \caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig} |
|
2689 \end{figure} |
|
2690 |
|
2691 \subsection{The syntax of a (co)inductive definition} |
|
2692 An inductive definition has the form |
|
2693 \begin{ttbox} |
|
2694 inductive {\it inductive sets} |
|
2695 intrs {\it introduction rules} |
|
2696 monos {\it monotonicity theorems} |
|
2697 con_defs {\it constructor definitions} |
|
2698 \end{ttbox} |
|
2699 A coinductive definition is identical, except that it starts with the keyword |
|
2700 \texttt{coinductive}. |
|
2701 |
|
2702 The \texttt{monos} and \texttt{con_defs} sections are optional. If present, |
|
2703 each is specified by a list of identifiers. |
|
2704 |
|
2705 \begin{itemize} |
|
2706 \item The \textit{inductive sets} are specified by one or more strings. |
|
2707 |
|
2708 \item The \textit{introduction rules} specify one or more introduction rules in |
|
2709 the form \textit{ident\/}~\textit{string}, where the identifier gives the name of |
|
2710 the rule in the result structure. |
|
2711 |
|
2712 \item The \textit{monotonicity theorems} are required for each operator |
|
2713 applied to a recursive set in the introduction rules. There {\bf must} |
|
2714 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each |
|
2715 premise $t\in M(R@i)$ in an introduction rule! |
|
2716 |
|
2717 \item The \textit{constructor definitions} contain definitions of constants |
|
2718 appearing in the introduction rules. In most cases it can be omitted. |
|
2719 \end{itemize} |
|
2720 |
|
2721 |
|
2722 \subsection{Example of an inductive definition} |
|
2723 Two declarations, included in a theory file, define the finite powerset |
|
2724 operator. First we declare the constant~\texttt{Fin}. Then we declare it |
|
2725 inductively, with two introduction rules: |
|
2726 \begin{ttbox} |
|
2727 consts Fin :: 'a set => 'a set set |
|
2728 inductive "Fin A" |
|
2729 intrs |
|
2730 emptyI "{\ttlbrace}{\ttrbrace} : Fin A" |
|
2731 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" |
|
2732 \end{ttbox} |
|
2733 The resulting theory structure contains a substructure, called~\texttt{Fin}. |
|
2734 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs}, |
|
2735 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction |
|
2736 rule is \texttt{Fin.induct}. |
|
2737 |
|
2738 For another example, here is a theory file defining the accessible |
|
2739 part of a relation. The main thing to note is the use of~\texttt{Pow} in |
|
2740 the sole introduction rule, and the corresponding mention of the rule |
|
2741 \verb|Pow_mono| in the \texttt{monos} list. The paper |
|
2742 \cite{paulson-CADE} discusses a \ZF\ version of this example in more |
|
2743 detail. |
|
2744 \begin{ttbox} |
|
2745 Acc = WF + |
|
2746 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
|
2747 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
|
2748 defs pred_def "pred x r == {y. (y,x):r}" |
|
2749 inductive "acc r" |
|
2750 intrs |
|
2751 pred "pred a r: Pow(acc r) ==> a: acc r" |
|
2752 monos Pow_mono |
|
2753 end |
|
2754 \end{ttbox} |
|
2755 The Isabelle distribution contains many other inductive definitions. Simple |
|
2756 examples are collected on subdirectory \texttt{HOL/Induct}. The theory |
|
2757 \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples |
|
2758 may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP}, |
|
2759 \texttt{Lambda} and \texttt{Auth}. |
|
2760 |
|
2761 \index{*coinductive|)} \index{*inductive|)} |
|
2762 |
|
2763 |
|
2764 \section{The examples directories} |
|
2765 |
|
2766 Directory \texttt{HOL/Auth} contains theories for proving the correctness of |
|
2767 cryptographic protocols. The approach is based upon operational |
|
2768 semantics~\cite{paulson-security} rather than the more usual belief logics. |
|
2769 On the same directory are proofs for some standard examples, such as the |
|
2770 Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} |
|
2771 and the Otway-Rees protocol. |
|
2772 |
|
2773 Directory \texttt{HOL/IMP} contains a formalization of various denotational, |
|
2774 operational and axiomatic semantics of a simple while-language, the necessary |
|
2775 equivalence proofs, soundness and completeness of the Hoare rules with respect |
|
2776 to the |
|
2777 denotational semantics, and soundness and completeness of a verification |
|
2778 condition generator. Much of development is taken from |
|
2779 Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}. |
|
2780 |
|
2781 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare |
|
2782 logic, including a tactic for generating verification-conditions. |
|
2783 |
|
2784 Directory \texttt{HOL/MiniML} contains a formalization of the type system of the |
|
2785 core functional language Mini-ML and a correctness proof for its type |
|
2786 inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}. |
|
2787 |
|
2788 Directory \texttt{HOL/Lambda} contains a formalization of untyped |
|
2789 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$ |
|
2790 and $\eta$ reduction~\cite{Nipkow-CR}. |
|
2791 |
|
2792 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of |
|
2793 substitutions and unifiers. It is based on Paulson's previous |
|
2794 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's |
|
2795 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef}, |
|
2796 with nested recursion. |
|
2797 |
|
2798 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive |
|
2799 definitions and datatypes. |
|
2800 \begin{itemize} |
|
2801 \item Theory \texttt{PropLog} proves the soundness and completeness of |
|
2802 classical propositional logic, given a truth table semantics. The only |
|
2803 connective is $\imp$. A Hilbert-style axiom system is specified, and its |
|
2804 set of theorems defined inductively. A similar proof in \ZF{} is |
|
2805 described elsewhere~\cite{paulson-set-II}. |
|
2806 |
|
2807 \item Theory \texttt{Term} defines the datatype \texttt{term}. |
|
2808 |
|
2809 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions |
|
2810 as mutually recursive datatypes. |
|
2811 |
|
2812 \item The definition of lazy lists demonstrates methods for handling |
|
2813 infinite data structures and coinduction in higher-order |
|
2814 logic~\cite{paulson-coind}.% |
|
2815 \footnote{To be precise, these lists are \emph{potentially infinite} rather |
|
2816 than lazy. Lazy implies a particular operational semantics.} |
|
2817 Theory \thydx{LList} defines an operator for |
|
2818 corecursion on lazy lists, which is used to define a few simple functions |
|
2819 such as map and append. A coinduction principle is defined |
|
2820 for proving equations on lazy lists. |
|
2821 |
|
2822 \item Theory \thydx{LFilter} defines the filter functional for lazy lists. |
|
2823 This functional is notoriously difficult to define because finding the next |
|
2824 element meeting the predicate requires possibly unlimited search. It is not |
|
2825 computable, but can be expressed using a combination of induction and |
|
2826 corecursion. |
|
2827 |
|
2828 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions |
|
2829 to express a programming language semantics that appears to require mutual |
|
2830 induction. Iterated induction allows greater modularity. |
|
2831 \end{itemize} |
|
2832 |
|
2833 Directory \texttt{HOL/ex} contains other examples and experimental proofs in |
|
2834 {\HOL}. |
|
2835 \begin{itemize} |
|
2836 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef} |
|
2837 to define recursive functions. Another example is \texttt{Fib}, which |
|
2838 defines the Fibonacci function. |
|
2839 |
|
2840 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two |
|
2841 natural numbers and proves a key lemma of the Fundamental Theorem of |
|
2842 Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$ |
|
2843 or $p$ divides~$n$. |
|
2844 |
|
2845 \item Theory \texttt{Primrec} develops some computation theory. It |
|
2846 inductively defines the set of primitive recursive functions and presents a |
|
2847 proof that Ackermann's function is not primitive recursive. |
|
2848 |
|
2849 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty |
|
2850 predicate calculus theorems, ranging from simple tautologies to |
|
2851 moderately difficult problems involving equality and quantifiers. |
|
2852 |
|
2853 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc |
|
2854 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is |
|
2855 much more powerful than Isabelle's classical reasoner. But it is less |
|
2856 useful in practice because it works only for pure logic; it does not |
|
2857 accept derived rules for the set theory primitives, for example. |
|
2858 |
|
2859 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof |
|
2860 procedure. These are mostly taken from Pelletier \cite{pelletier86}. |
|
2861 |
|
2862 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in |
|
2863 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. |
|
2864 |
|
2865 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of |
|
2866 Milner and Tofte's coinduction example~\cite{milner-coind}. This |
|
2867 substantial proof concerns the soundness of a type system for a simple |
|
2868 functional language. The semantics of recursion is given by a cyclic |
|
2869 environment, which makes a coinductive argument appropriate. |
|
2870 \end{itemize} |
|
2871 |
|
2872 |
|
2873 \goodbreak |
|
2874 \section{Example: Cantor's Theorem}\label{sec:hol-cantor} |
|
2875 Cantor's Theorem states that every set has more subsets than it has |
|
2876 elements. It has become a favourite example in higher-order logic since |
|
2877 it is so easily expressed: |
|
2878 \[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool. |
|
2879 \forall x::\alpha. f~x \not= S |
|
2880 \] |
|
2881 % |
|
2882 Viewing types as sets, $\alpha\To bool$ represents the powerset |
|
2883 of~$\alpha$. This version states that for every function from $\alpha$ to |
|
2884 its powerset, some subset is outside its range. |
|
2885 |
|
2886 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and |
|
2887 the operator \cdx{range}. |
|
2888 \begin{ttbox} |
|
2889 context Set.thy; |
|
2890 \end{ttbox} |
|
2891 The set~$S$ is given as an unknown instead of a |
|
2892 quantified variable so that we may inspect the subset found by the proof. |
|
2893 \begin{ttbox} |
|
2894 Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; |
|
2895 {\out Level 0} |
|
2896 {\out ?S ~: range f} |
|
2897 {\out 1. ?S ~: range f} |
|
2898 \end{ttbox} |
|
2899 The first two steps are routine. The rule \tdx{rangeE} replaces |
|
2900 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$. |
|
2901 \begin{ttbox} |
|
2902 by (resolve_tac [notI] 1); |
|
2903 {\out Level 1} |
|
2904 {\out ?S ~: range f} |
|
2905 {\out 1. ?S : range f ==> False} |
|
2906 \ttbreak |
|
2907 by (eresolve_tac [rangeE] 1); |
|
2908 {\out Level 2} |
|
2909 {\out ?S ~: range f} |
|
2910 {\out 1. !!x. ?S = f x ==> False} |
|
2911 \end{ttbox} |
|
2912 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, |
|
2913 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for |
|
2914 any~$\Var{c}$. |
|
2915 \begin{ttbox} |
|
2916 by (eresolve_tac [equalityCE] 1); |
|
2917 {\out Level 3} |
|
2918 {\out ?S ~: range f} |
|
2919 {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} |
|
2920 {\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False} |
|
2921 \end{ttbox} |
|
2922 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a |
|
2923 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies |
|
2924 $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} |
|
2925 instantiates~$\Var{S}$ and creates the new assumption. |
|
2926 \begin{ttbox} |
|
2927 by (dresolve_tac [CollectD] 1); |
|
2928 {\out Level 4} |
|
2929 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} |
|
2930 {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} |
|
2931 {\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False} |
|
2932 \end{ttbox} |
|
2933 Forcing a contradiction between the two assumptions of subgoal~1 |
|
2934 completes the instantiation of~$S$. It is now the set $\{x. x\not\in |
|
2935 f~x\}$, which is the standard diagonal construction. |
|
2936 \begin{ttbox} |
|
2937 by (contr_tac 1); |
|
2938 {\out Level 5} |
|
2939 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
|
2940 {\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False} |
|
2941 \end{ttbox} |
|
2942 The rest should be easy. To apply \tdx{CollectI} to the negated |
|
2943 assumption, we employ \ttindex{swap_res_tac}: |
|
2944 \begin{ttbox} |
|
2945 by (swap_res_tac [CollectI] 1); |
|
2946 {\out Level 6} |
|
2947 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
|
2948 {\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x} |
|
2949 \ttbreak |
|
2950 by (assume_tac 1); |
|
2951 {\out Level 7} |
|
2952 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
|
2953 {\out No subgoals!} |
|
2954 \end{ttbox} |
|
2955 How much creativity is required? As it happens, Isabelle can prove this |
|
2956 theorem automatically. The default classical set \texttt{claset()} contains rules |
|
2957 for most of the constructs of \HOL's set theory. We must augment it with |
|
2958 \tdx{equalityCE} to break up set equalities, and then apply best-first |
|
2959 search. Depth-first search would diverge, but best-first search |
|
2960 successfully navigates through the large search space. |
|
2961 \index{search!best-first} |
|
2962 \begin{ttbox} |
|
2963 choplev 0; |
|
2964 {\out Level 0} |
|
2965 {\out ?S ~: range f} |
|
2966 {\out 1. ?S ~: range f} |
|
2967 \ttbreak |
|
2968 by (best_tac (claset() addSEs [equalityCE]) 1); |
|
2969 {\out Level 1} |
|
2970 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
|
2971 {\out No subgoals!} |
|
2972 \end{ttbox} |
|
2973 If you run this example interactively, make sure your current theory contains |
|
2974 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. |
|
2975 Otherwise the default claset may not contain the rules for set theory. |
|
2976 \index{higher-order logic|)} |
|
2977 |
|
2978 %%% Local Variables: |
|
2979 %%% mode: latex |
|
2980 %%% TeX-master: "logics" |
|
2981 %%% End: |