|
1 %% $Id$ |
|
2 \chapter{Zermelo-Fraenkel Set Theory} |
|
3 \index{set theory|(} |
|
4 |
|
5 The theory~\thydx{ZF} implements Zermelo-Fraenkel set |
|
6 theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical |
|
7 first-order logic. The theory includes a collection of derived natural |
|
8 deduction rules, for use with Isabelle's classical reasoner. Much |
|
9 of it is based on the work of No\"el~\cite{noel}. |
|
10 |
|
11 A tremendous amount of set theory has been formally developed, including the |
|
12 basic properties of relations, functions, ordinals and cardinals. Significant |
|
13 results have been proved, such as the Schr\"oder-Bernstein Theorem, the |
|
14 Wellordering Theorem and a version of Ramsey's Theorem. \texttt{ZF} provides |
|
15 both the integers and the natural numbers. General methods have been |
|
16 developed for solving recursion equations over monotonic functors; these have |
|
17 been applied to yield constructions of lists, trees, infinite lists, etc. |
|
18 |
|
19 \texttt{ZF} has a flexible package for handling inductive definitions, |
|
20 such as inference systems, and datatype definitions, such as lists and |
|
21 trees. Moreover it handles coinductive definitions, such as |
|
22 bisimulation relations, and codatatype definitions, such as streams. It |
|
23 provides a streamlined syntax for defining primitive recursive functions over |
|
24 datatypes. |
|
25 |
|
26 Because {\ZF} is an extension of {\FOL}, it provides the same |
|
27 packages, namely \texttt{hyp_subst_tac}, the simplifier, and the |
|
28 classical reasoner. The default simpset and claset are usually |
|
29 satisfactory. |
|
30 |
|
31 Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF} |
|
32 less formally than this chapter. Isabelle employs a novel treatment of |
|
33 non-well-founded data structures within the standard {\sc zf} axioms including |
|
34 the Axiom of Foundation~\cite{paulson-final}. |
|
35 |
|
36 |
|
37 \section{Which version of axiomatic set theory?} |
|
38 The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg}) |
|
39 and Zermelo-Fraenkel~({\sc zf}). Resolution theorem provers can use {\sc |
|
40 bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not |
|
41 have a finite axiom system because of its Axiom Scheme of Replacement. |
|
42 This makes it awkward to use with many theorem provers, since instances |
|
43 of the axiom scheme have to be invoked explicitly. Since Isabelle has no |
|
44 difficulty with axiom schemes, we may adopt either axiom system. |
|
45 |
|
46 These two theories differ in their treatment of {\bf classes}, which are |
|
47 collections that are `too big' to be sets. The class of all sets,~$V$, |
|
48 cannot be a set without admitting Russell's Paradox. In {\sc bg}, both |
|
49 classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In |
|
50 {\sc zf}, all variables denote sets; classes are identified with unary |
|
51 predicates. The two systems define essentially the same sets and classes, |
|
52 with similar properties. In particular, a class cannot belong to another |
|
53 class (let alone a set). |
|
54 |
|
55 Modern set theorists tend to prefer {\sc zf} because they are mainly concerned |
|
56 with sets, rather than classes. {\sc bg} requires tiresome proofs that various |
|
57 collections are sets; for instance, showing $x\in\{x\}$ requires showing that |
|
58 $x$ is a set. |
|
59 |
|
60 |
|
61 \begin{figure} \small |
|
62 \begin{center} |
|
63 \begin{tabular}{rrr} |
|
64 \it name &\it meta-type & \it description \\ |
|
65 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\ |
|
66 \cdx{0} & $i$ & empty set\\ |
|
67 \cdx{cons} & $[i,i]\To i$ & finite set constructor\\ |
|
68 \cdx{Upair} & $[i,i]\To i$ & unordered pairing\\ |
|
69 \cdx{Pair} & $[i,i]\To i$ & ordered pairing\\ |
|
70 \cdx{Inf} & $i$ & infinite set\\ |
|
71 \cdx{Pow} & $i\To i$ & powerset\\ |
|
72 \cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\ |
|
73 \cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ |
|
74 \cdx{fst} \cdx{snd} & $i\To i$ & projections\\ |
|
75 \cdx{converse}& $i\To i$ & converse of a relation\\ |
|
76 \cdx{succ} & $i\To i$ & successor\\ |
|
77 \cdx{Collect} & $[i,i\To o]\To i$ & separation\\ |
|
78 \cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ |
|
79 \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ |
|
80 \cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ |
|
81 \cdx{Pi} \cdx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ |
|
82 \cdx{domain} & $i\To i$ & domain of a relation\\ |
|
83 \cdx{range} & $i\To i$ & range of a relation\\ |
|
84 \cdx{field} & $i\To i$ & field of a relation\\ |
|
85 \cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\ |
|
86 \cdx{restrict}& $[i, i] \To i$ & restriction of a function\\ |
|
87 \cdx{The} & $[i\To o]\To i$ & definite description\\ |
|
88 \cdx{if} & $[o,i,i]\To i$ & conditional\\ |
|
89 \cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers |
|
90 \end{tabular} |
|
91 \end{center} |
|
92 \subcaption{Constants} |
|
93 |
|
94 \begin{center} |
|
95 \index{*"`"` symbol} |
|
96 \index{*"-"`"` symbol} |
|
97 \index{*"` symbol}\index{function applications!in \ZF} |
|
98 \index{*"- symbol} |
|
99 \index{*": symbol} |
|
100 \index{*"<"= symbol} |
|
101 \begin{tabular}{rrrr} |
|
102 \it symbol & \it meta-type & \it priority & \it description \\ |
|
103 \tt `` & $[i,i]\To i$ & Left 90 & image \\ |
|
104 \tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\ |
|
105 \tt ` & $[i,i]\To i$ & Left 90 & application \\ |
|
106 \sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\int$) \\ |
|
107 \sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\un$) \\ |
|
108 \tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex] |
|
109 \tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ |
|
110 \tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) |
|
111 \end{tabular} |
|
112 \end{center} |
|
113 \subcaption{Infixes} |
|
114 \caption{Constants of {\ZF}} \label{zf-constants} |
|
115 \end{figure} |
|
116 |
|
117 |
|
118 \section{The syntax of set theory} |
|
119 The language of set theory, as studied by logicians, has no constants. The |
|
120 traditional axioms merely assert the existence of empty sets, unions, |
|
121 powersets, etc.; this would be intolerable for practical reasoning. The |
|
122 Isabelle theory declares constants for primitive sets. It also extends |
|
123 \texttt{FOL} with additional syntax for finite sets, ordered pairs, |
|
124 comprehension, general union/intersection, general sums/products, and |
|
125 bounded quantifiers. In most other respects, Isabelle implements precisely |
|
126 Zermelo-Fraenkel set theory. |
|
127 |
|
128 Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while |
|
129 Figure~\ref{zf-trans} presents the syntax translations. Finally, |
|
130 Figure~\ref{zf-syntax} presents the full grammar for set theory, including |
|
131 the constructs of \FOL. |
|
132 |
|
133 Local abbreviations can be introduced by a \texttt{let} construct whose |
|
134 syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into |
|
135 the constant~\cdx{Let}. It can be expanded by rewriting with its |
|
136 definition, \tdx{Let_def}. |
|
137 |
|
138 Apart from \texttt{let}, set theory does not use polymorphism. All terms in |
|
139 {\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt |
|
140 term}. The type of first-order formulae, remember, is~\textit{o}. |
|
141 |
|
142 Infix operators include binary union and intersection ($A\un B$ and |
|
143 $A\int B$), set difference ($A-B$), and the subset and membership |
|
144 relations. Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$. The |
|
145 union and intersection operators ($\bigcup A$ and $\bigcap A$) form the |
|
146 union or intersection of a set of sets; $\bigcup A$ means the same as |
|
147 $\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive. |
|
148 |
|
149 The constant \cdx{Upair} constructs unordered pairs; thus {\tt |
|
150 Upair($A$,$B$)} denotes the set~$\{A,B\}$ and \texttt{Upair($A$,$A$)} |
|
151 denotes the singleton~$\{A\}$. General union is used to define binary |
|
152 union. The Isabelle version goes on to define the constant |
|
153 \cdx{cons}: |
|
154 \begin{eqnarray*} |
|
155 A\cup B & \equiv & \bigcup(\texttt{Upair}(A,B)) \\ |
|
156 \texttt{cons}(a,B) & \equiv & \texttt{Upair}(a,a) \un B |
|
157 \end{eqnarray*} |
|
158 The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the |
|
159 obvious manner using~\texttt{cons} and~$\emptyset$ (the empty set): |
|
160 \begin{eqnarray*} |
|
161 \{a,b,c\} & \equiv & \texttt{cons}(a,\texttt{cons}(b,\texttt{cons}(c,\emptyset))) |
|
162 \end{eqnarray*} |
|
163 |
|
164 The constant \cdx{Pair} constructs ordered pairs, as in {\tt |
|
165 Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets, |
|
166 as {\tt<$a$,$b$>}. The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>} |
|
167 abbreviates the nest of pairs\par\nobreak |
|
168 \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}} |
|
169 |
|
170 In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an |
|
171 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not |
|
172 say $i\To i$. The infix operator~{\tt`} denotes the application of a |
|
173 function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The |
|
174 syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$. |
|
175 |
|
176 |
|
177 \begin{figure} |
|
178 \index{lambda abs@$\lambda$-abstractions!in \ZF} |
|
179 \index{*"-"> symbol} |
|
180 \index{*"* symbol} |
|
181 \begin{center} \footnotesize\tt\frenchspacing |
|
182 \begin{tabular}{rrr} |
|
183 \it external & \it internal & \it description \\ |
|
184 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ |
|
185 \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace & cons($a@1$,$\ldots$,cons($a@n$,0)) & |
|
186 \rm finite set \\ |
|
187 <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & |
|
188 Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & |
|
189 \rm ordered $n$-tuple \\ |
|
190 \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x. P[x]$) & |
|
191 \rm separation \\ |
|
192 \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y. Q[x,y]$) & |
|
193 \rm replacement \\ |
|
194 \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x. b[x]$) & |
|
195 \rm functional replacement \\ |
|
196 \sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) & |
|
197 \rm general intersection \\ |
|
198 \sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) & |
|
199 \rm general union \\ |
|
200 \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x. B[x]$) & |
|
201 \rm general product \\ |
|
202 \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x. B[x]$) & |
|
203 \rm general sum \\ |
|
204 $A$ -> $B$ & Pi($A$,$\lambda x. B$) & |
|
205 \rm function space \\ |
|
206 $A$ * $B$ & Sigma($A$,$\lambda x. B$) & |
|
207 \rm binary product \\ |
|
208 \sdx{THE} $x . P[x]$ & The($\lambda x. P[x]$) & |
|
209 \rm definite description \\ |
|
210 \sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x. b[x]$) & |
|
211 \rm $\lambda$-abstraction\\[1ex] |
|
212 \sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x. P[x]$) & |
|
213 \rm bounded $\forall$ \\ |
|
214 \sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x. P[x]$) & |
|
215 \rm bounded $\exists$ |
|
216 \end{tabular} |
|
217 \end{center} |
|
218 \caption{Translations for {\ZF}} \label{zf-trans} |
|
219 \end{figure} |
|
220 |
|
221 |
|
222 \begin{figure} |
|
223 \index{*let symbol} |
|
224 \index{*in symbol} |
|
225 \dquotes |
|
226 \[\begin{array}{rcl} |
|
227 term & = & \hbox{expression of type~$i$} \\ |
|
228 & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ |
|
229 & | & "if"~term~"then"~term~"else"~term \\ |
|
230 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ |
|
231 & | & "< " term\; ("," term)^* " >" \\ |
|
232 & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\ |
|
233 & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\ |
|
234 & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\ |
|
235 & | & term " `` " term \\ |
|
236 & | & term " -`` " term \\ |
|
237 & | & term " ` " term \\ |
|
238 & | & term " * " term \\ |
|
239 & | & term " Int " term \\ |
|
240 & | & term " Un " term \\ |
|
241 & | & term " - " term \\ |
|
242 & | & term " -> " term \\ |
|
243 & | & "THE~~" id " . " formula\\ |
|
244 & | & "lam~~" id ":" term " . " term \\ |
|
245 & | & "INT~~" id ":" term " . " term \\ |
|
246 & | & "UN~~~" id ":" term " . " term \\ |
|
247 & | & "PROD~" id ":" term " . " term \\ |
|
248 & | & "SUM~~" id ":" term " . " term \\[2ex] |
|
249 formula & = & \hbox{expression of type~$o$} \\ |
|
250 & | & term " : " term \\ |
|
251 & | & term " \ttilde: " term \\ |
|
252 & | & term " <= " term \\ |
|
253 & | & term " = " term \\ |
|
254 & | & term " \ttilde= " term \\ |
|
255 & | & "\ttilde\ " formula \\ |
|
256 & | & formula " \& " formula \\ |
|
257 & | & formula " | " formula \\ |
|
258 & | & formula " --> " formula \\ |
|
259 & | & formula " <-> " formula \\ |
|
260 & | & "ALL " id ":" term " . " formula \\ |
|
261 & | & "EX~~" id ":" term " . " formula \\ |
|
262 & | & "ALL~" id~id^* " . " formula \\ |
|
263 & | & "EX~~" id~id^* " . " formula \\ |
|
264 & | & "EX!~" id~id^* " . " formula |
|
265 \end{array} |
|
266 \] |
|
267 \caption{Full grammar for {\ZF}} \label{zf-syntax} |
|
268 \end{figure} |
|
269 |
|
270 |
|
271 \section{Binding operators} |
|
272 The constant \cdx{Collect} constructs sets by the principle of {\bf |
|
273 separation}. The syntax for separation is |
|
274 \hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula |
|
275 that may contain free occurrences of~$x$. It abbreviates the set {\tt |
|
276 Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that |
|
277 satisfy~$P[x]$. Note that \texttt{Collect} is an unfortunate choice of |
|
278 name: some set theories adopt a set-formation principle, related to |
|
279 replacement, called collection. |
|
280 |
|
281 The constant \cdx{Replace} constructs sets by the principle of {\bf |
|
282 replacement}. The syntax |
|
283 \hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt |
|
284 Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such |
|
285 that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom |
|
286 has the condition that $Q$ must be single-valued over~$A$: for |
|
287 all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A |
|
288 single-valued binary predicate is also called a {\bf class function}. |
|
289 |
|
290 The constant \cdx{RepFun} expresses a special case of replacement, |
|
291 where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially |
|
292 single-valued, since it is just the graph of the meta-level |
|
293 function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$ |
|
294 for~$x\in A$. This is analogous to the \ML{} functional \texttt{map}, |
|
295 since it applies a function to every element of a set. The syntax is |
|
296 \hbox{\tt\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to {\tt |
|
297 RepFun($A$,$\lambda x. b[x]$)}. |
|
298 |
|
299 \index{*INT symbol}\index{*UN symbol} |
|
300 General unions and intersections of indexed |
|
301 families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, |
|
302 are written \hbox{\tt UN $x$:$A$.\ $B[x]$} and \hbox{\tt INT $x$:$A$.\ $B[x]$}. |
|
303 Their meaning is expressed using \texttt{RepFun} as |
|
304 \[ |
|
305 \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad |
|
306 \bigcap(\{B[x]. x\in A\}). |
|
307 \] |
|
308 General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be |
|
309 constructed in set theory, where $B[x]$ is a family of sets over~$A$. They |
|
310 have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set. |
|
311 This is similar to the situation in Constructive Type Theory (set theory |
|
312 has `dependent sets') and calls for similar syntactic conventions. The |
|
313 constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and |
|
314 products. Instead of \texttt{Sigma($A$,$B$)} and \texttt{Pi($A$,$B$)} we may |
|
315 write |
|
316 \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt PROD $x$:$A$.\ $B[x]$}. |
|
317 \index{*SUM symbol}\index{*PROD symbol}% |
|
318 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate |
|
319 general sums and products over a constant family.\footnote{Unlike normal |
|
320 infix operators, {\tt*} and {\tt->} merely define abbreviations; there are |
|
321 no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these |
|
322 abbreviations in parsing and uses them whenever possible for printing. |
|
323 |
|
324 \index{*THE symbol} |
|
325 As mentioned above, whenever the axioms assert the existence and uniqueness |
|
326 of a set, Isabelle's set theory declares a constant for that set. These |
|
327 constants can express the {\bf definite description} operator~$\iota |
|
328 x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists. |
|
329 Since all terms in {\ZF} denote something, a description is always |
|
330 meaningful, but we do not know its value unless $P[x]$ defines it uniquely. |
|
331 Using the constant~\cdx{The}, we may write descriptions as {\tt |
|
332 The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}. |
|
333 |
|
334 \index{*lam symbol} |
|
335 Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$ |
|
336 stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for |
|
337 this to be a set, the function's domain~$A$ must be given. Using the |
|
338 constant~\cdx{Lambda}, we may express function sets as {\tt |
|
339 Lambda($A$,$\lambda x. b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.\ $b[x]$}. |
|
340 |
|
341 Isabelle's set theory defines two {\bf bounded quantifiers}: |
|
342 \begin{eqnarray*} |
|
343 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ |
|
344 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] |
|
345 \end{eqnarray*} |
|
346 The constants~\cdx{Ball} and~\cdx{Bex} are defined |
|
347 accordingly. Instead of \texttt{Ball($A$,$P$)} and \texttt{Bex($A$,$P$)} we may |
|
348 write |
|
349 \hbox{\tt ALL $x$:$A$.\ $P[x]$} and \hbox{\tt EX $x$:$A$.\ $P[x]$}. |
|
350 |
|
351 |
|
352 %%%% ZF.thy |
|
353 |
|
354 \begin{figure} |
|
355 \begin{ttbox} |
|
356 \tdx{Let_def} Let(s, f) == f(s) |
|
357 |
|
358 \tdx{Ball_def} Ball(A,P) == ALL x. x:A --> P(x) |
|
359 \tdx{Bex_def} Bex(A,P) == EX x. x:A & P(x) |
|
360 |
|
361 \tdx{subset_def} A <= B == ALL x:A. x:B |
|
362 \tdx{extension} A = B <-> A <= B & B <= A |
|
363 |
|
364 \tdx{Union_iff} A : Union(C) <-> (EX B:C. A:B) |
|
365 \tdx{Pow_iff} A : Pow(B) <-> A <= B |
|
366 \tdx{foundation} A=0 | (EX x:A. ALL y:x. ~ y:A) |
|
367 |
|
368 \tdx{replacement} (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> |
|
369 b : PrimReplace(A,P) <-> (EX x:A. P(x,b)) |
|
370 \subcaption{The Zermelo-Fraenkel Axioms} |
|
371 |
|
372 \tdx{Replace_def} Replace(A,P) == |
|
373 PrimReplace(A, \%x y. (EX!z. P(x,z)) & P(x,y)) |
|
374 \tdx{RepFun_def} RepFun(A,f) == {\ttlbrace}y . x:A, y=f(x)\ttrbrace |
|
375 \tdx{the_def} The(P) == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace}) |
|
376 \tdx{if_def} if(P,a,b) == THE z. P & z=a | ~P & z=b |
|
377 \tdx{Collect_def} Collect(A,P) == {\ttlbrace}y . x:A, x=y & P(x){\ttrbrace} |
|
378 \tdx{Upair_def} Upair(a,b) == |
|
379 {\ttlbrace}y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b){\ttrbrace} |
|
380 \subcaption{Consequences of replacement} |
|
381 |
|
382 \tdx{Inter_def} Inter(A) == {\ttlbrace}x:Union(A) . ALL y:A. x:y{\ttrbrace} |
|
383 \tdx{Un_def} A Un B == Union(Upair(A,B)) |
|
384 \tdx{Int_def} A Int B == Inter(Upair(A,B)) |
|
385 \tdx{Diff_def} A - B == {\ttlbrace}x:A . x~:B{\ttrbrace} |
|
386 \subcaption{Union, intersection, difference} |
|
387 \end{ttbox} |
|
388 \caption{Rules and axioms of {\ZF}} \label{zf-rules} |
|
389 \end{figure} |
|
390 |
|
391 |
|
392 \begin{figure} |
|
393 \begin{ttbox} |
|
394 \tdx{cons_def} cons(a,A) == Upair(a,a) Un A |
|
395 \tdx{succ_def} succ(i) == cons(i,i) |
|
396 \tdx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) |
|
397 \subcaption{Finite and infinite sets} |
|
398 |
|
399 \tdx{Pair_def} <a,b> == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace} |
|
400 \tdx{split_def} split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b) |
|
401 \tdx{fst_def} fst(A) == split(\%x y. x, p) |
|
402 \tdx{snd_def} snd(A) == split(\%x y. y, p) |
|
403 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x,y>{\ttrbrace} |
|
404 \subcaption{Ordered pairs and Cartesian products} |
|
405 |
|
406 \tdx{converse_def} converse(r) == {\ttlbrace}z. w:r, EX x y. w=<x,y> & z=<y,x>{\ttrbrace} |
|
407 \tdx{domain_def} domain(r) == {\ttlbrace}x. w:r, EX y. w=<x,y>{\ttrbrace} |
|
408 \tdx{range_def} range(r) == domain(converse(r)) |
|
409 \tdx{field_def} field(r) == domain(r) Un range(r) |
|
410 \tdx{image_def} r `` A == {\ttlbrace}y : range(r) . EX x:A. <x,y> : r{\ttrbrace} |
|
411 \tdx{vimage_def} r -`` A == converse(r)``A |
|
412 \subcaption{Operations on relations} |
|
413 |
|
414 \tdx{lam_def} Lambda(A,b) == {\ttlbrace}<x,b(x)> . x:A{\ttrbrace} |
|
415 \tdx{apply_def} f`a == THE y. <a,y> : f |
|
416 \tdx{Pi_def} Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f{\ttrbrace} |
|
417 \tdx{restrict_def} restrict(f,A) == lam x:A. f`x |
|
418 \subcaption{Functions and general product} |
|
419 \end{ttbox} |
|
420 \caption{Further definitions of {\ZF}} \label{zf-defs} |
|
421 \end{figure} |
|
422 |
|
423 |
|
424 |
|
425 \section{The Zermelo-Fraenkel axioms} |
|
426 The axioms appear in Fig.\ts \ref{zf-rules}. They resemble those |
|
427 presented by Suppes~\cite{suppes72}. Most of the theory consists of |
|
428 definitions. In particular, bounded quantifiers and the subset relation |
|
429 appear in other axioms. Object-level quantifiers and implications have |
|
430 been replaced by meta-level ones wherever possible, to simplify use of the |
|
431 axioms. See the file \texttt{ZF/ZF.thy} for details. |
|
432 |
|
433 The traditional replacement axiom asserts |
|
434 \[ y \in \texttt{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \] |
|
435 subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$. |
|
436 The Isabelle theory defines \cdx{Replace} to apply |
|
437 \cdx{PrimReplace} to the single-valued part of~$P$, namely |
|
438 \[ (\exists!z. P(x,z)) \conj P(x,y). \] |
|
439 Thus $y\in \texttt{Replace}(A,P)$ if and only if there is some~$x$ such that |
|
440 $P(x,-)$ holds uniquely for~$y$. Because the equivalence is unconditional, |
|
441 \texttt{Replace} is much easier to use than \texttt{PrimReplace}; it defines the |
|
442 same set, if $P(x,y)$ is single-valued. The nice syntax for replacement |
|
443 expands to \texttt{Replace}. |
|
444 |
|
445 Other consequences of replacement include functional replacement |
|
446 (\cdx{RepFun}) and definite descriptions (\cdx{The}). |
|
447 Axioms for separation (\cdx{Collect}) and unordered pairs |
|
448 (\cdx{Upair}) are traditionally assumed, but they actually follow |
|
449 from replacement~\cite[pages 237--8]{suppes72}. |
|
450 |
|
451 The definitions of general intersection, etc., are straightforward. Note |
|
452 the definition of \texttt{cons}, which underlies the finite set notation. |
|
453 The axiom of infinity gives us a set that contains~0 and is closed under |
|
454 successor (\cdx{succ}). Although this set is not uniquely defined, |
|
455 the theory names it (\cdx{Inf}) in order to simplify the |
|
456 construction of the natural numbers. |
|
457 |
|
458 Further definitions appear in Fig.\ts\ref{zf-defs}. Ordered pairs are |
|
459 defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall |
|
460 that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two |
|
461 sets. It is defined to be the union of all singleton sets |
|
462 $\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of |
|
463 general union. |
|
464 |
|
465 The projections \cdx{fst} and~\cdx{snd} are defined in terms of the |
|
466 generalized projection \cdx{split}. The latter has been borrowed from |
|
467 Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst} |
|
468 and~\cdx{snd}. |
|
469 |
|
470 Operations on relations include converse, domain, range, and image. The |
|
471 set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets. |
|
472 Note the simple definitions of $\lambda$-abstraction (using |
|
473 \cdx{RepFun}) and application (using a definite description). The |
|
474 function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only |
|
475 over the domain~$A$. |
|
476 |
|
477 |
|
478 %%%% zf.ML |
|
479 |
|
480 \begin{figure} |
|
481 \begin{ttbox} |
|
482 \tdx{ballI} [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x) |
|
483 \tdx{bspec} [| ALL x:A. P(x); x: A |] ==> P(x) |
|
484 \tdx{ballE} [| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q |
|
485 |
|
486 \tdx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
487 (ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) |
|
488 |
|
489 \tdx{bexI} [| P(x); x: A |] ==> EX x:A. P(x) |
|
490 \tdx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x) |
|
491 \tdx{bexE} [| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q |
|
492 |
|
493 \tdx{bex_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
494 (EX x:A. P(x)) <-> (EX x:A'. P'(x)) |
|
495 \subcaption{Bounded quantifiers} |
|
496 |
|
497 \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B |
|
498 \tdx{subsetD} [| A <= B; c:A |] ==> c:B |
|
499 \tdx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P |
|
500 \tdx{subset_refl} A <= A |
|
501 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C |
|
502 |
|
503 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B |
|
504 \tdx{equalityD1} A = B ==> A<=B |
|
505 \tdx{equalityD2} A = B ==> B<=A |
|
506 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P |
|
507 \subcaption{Subsets and extensionality} |
|
508 |
|
509 \tdx{emptyE} a:0 ==> P |
|
510 \tdx{empty_subsetI} 0 <= A |
|
511 \tdx{equals0I} [| !!y. y:A ==> False |] ==> A=0 |
|
512 \tdx{equals0D} [| A=0; a:A |] ==> P |
|
513 |
|
514 \tdx{PowI} A <= B ==> A : Pow(B) |
|
515 \tdx{PowD} A : Pow(B) ==> A<=B |
|
516 \subcaption{The empty set; power sets} |
|
517 \end{ttbox} |
|
518 \caption{Basic derived rules for {\ZF}} \label{zf-lemmas1} |
|
519 \end{figure} |
|
520 |
|
521 |
|
522 \section{From basic lemmas to function spaces} |
|
523 Faced with so many definitions, it is essential to prove lemmas. Even |
|
524 trivial theorems like $A \int B = B \int A$ would be difficult to |
|
525 prove from the definitions alone. Isabelle's set theory derives many |
|
526 rules using a natural deduction style. Ideally, a natural deduction |
|
527 rule should introduce or eliminate just one operator, but this is not |
|
528 always practical. For most operators, we may forget its definition |
|
529 and use its derived rules instead. |
|
530 |
|
531 \subsection{Fundamental lemmas} |
|
532 Figure~\ref{zf-lemmas1} presents the derived rules for the most basic |
|
533 operators. The rules for the bounded quantifiers resemble those for the |
|
534 ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption |
|
535 in the style of Isabelle's classical reasoner. The \rmindex{congruence |
|
536 rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's |
|
537 simplifier, but have few other uses. Congruence rules must be specially |
|
538 derived for all binding operators, and henceforth will not be shown. |
|
539 |
|
540 Figure~\ref{zf-lemmas1} also shows rules for the subset and equality |
|
541 relations (proof by extensionality), and rules about the empty set and the |
|
542 power set operator. |
|
543 |
|
544 Figure~\ref{zf-lemmas2} presents rules for replacement and separation. |
|
545 The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than |
|
546 comparable rules for \texttt{PrimReplace} would be. The principle of |
|
547 separation is proved explicitly, although most proofs should use the |
|
548 natural deduction rules for \texttt{Collect}. The elimination rule |
|
549 \tdx{CollectE} is equivalent to the two destruction rules |
|
550 \tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to |
|
551 particular circumstances. Although too many rules can be confusing, there |
|
552 is no reason to aim for a minimal set of rules. See the file |
|
553 \texttt{ZF/ZF.ML} for a complete listing. |
|
554 |
|
555 Figure~\ref{zf-lemmas3} presents rules for general union and intersection. |
|
556 The empty intersection should be undefined. We cannot have |
|
557 $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All |
|
558 expressions denote something in {\ZF} set theory; the definition of |
|
559 intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is |
|
560 arbitrary. The rule \tdx{InterI} must have a premise to exclude |
|
561 the empty intersection. Some of the laws governing intersections require |
|
562 similar premises. |
|
563 |
|
564 |
|
565 %the [p] gives better page breaking for the book |
|
566 \begin{figure}[p] |
|
567 \begin{ttbox} |
|
568 \tdx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> |
|
569 b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace} |
|
570 |
|
571 \tdx{ReplaceE} [| b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace}; |
|
572 !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R |
|
573 |] ==> R |
|
574 |
|
575 \tdx{RepFunI} [| a : A |] ==> f(a) : {\ttlbrace}f(x). x:A{\ttrbrace} |
|
576 \tdx{RepFunE} [| b : {\ttlbrace}f(x). x:A{\ttrbrace}; |
|
577 !!x.[| x:A; b=f(x) |] ==> P |] ==> P |
|
578 |
|
579 \tdx{separation} a : {\ttlbrace}x:A. P(x){\ttrbrace} <-> a:A & P(a) |
|
580 \tdx{CollectI} [| a:A; P(a) |] ==> a : {\ttlbrace}x:A. P(x){\ttrbrace} |
|
581 \tdx{CollectE} [| a : {\ttlbrace}x:A. P(x){\ttrbrace}; [| a:A; P(a) |] ==> R |] ==> R |
|
582 \tdx{CollectD1} a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> a:A |
|
583 \tdx{CollectD2} a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> P(a) |
|
584 \end{ttbox} |
|
585 \caption{Replacement and separation} \label{zf-lemmas2} |
|
586 \end{figure} |
|
587 |
|
588 |
|
589 \begin{figure} |
|
590 \begin{ttbox} |
|
591 \tdx{UnionI} [| B: C; A: B |] ==> A: Union(C) |
|
592 \tdx{UnionE} [| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R |
|
593 |
|
594 \tdx{InterI} [| !!x. x: C ==> A: x; c:C |] ==> A : Inter(C) |
|
595 \tdx{InterD} [| A : Inter(C); B : C |] ==> A : B |
|
596 \tdx{InterE} [| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R |
|
597 |
|
598 \tdx{UN_I} [| a: A; b: B(a) |] ==> b: (UN x:A. B(x)) |
|
599 \tdx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |
|
600 |] ==> R |
|
601 |
|
602 \tdx{INT_I} [| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x)) |
|
603 \tdx{INT_E} [| b : (INT x:A. B(x)); a: A |] ==> b : B(a) |
|
604 \end{ttbox} |
|
605 \caption{General union and intersection} \label{zf-lemmas3} |
|
606 \end{figure} |
|
607 |
|
608 |
|
609 %%% upair.ML |
|
610 |
|
611 \begin{figure} |
|
612 \begin{ttbox} |
|
613 \tdx{pairing} a:Upair(b,c) <-> (a=b | a=c) |
|
614 \tdx{UpairI1} a : Upair(a,b) |
|
615 \tdx{UpairI2} b : Upair(a,b) |
|
616 \tdx{UpairE} [| a : Upair(b,c); a = b ==> P; a = c ==> P |] ==> P |
|
617 \end{ttbox} |
|
618 \caption{Unordered pairs} \label{zf-upair1} |
|
619 \end{figure} |
|
620 |
|
621 |
|
622 \begin{figure} |
|
623 \begin{ttbox} |
|
624 \tdx{UnI1} c : A ==> c : A Un B |
|
625 \tdx{UnI2} c : B ==> c : A Un B |
|
626 \tdx{UnCI} (~c : B ==> c : A) ==> c : A Un B |
|
627 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P |
|
628 |
|
629 \tdx{IntI} [| c : A; c : B |] ==> c : A Int B |
|
630 \tdx{IntD1} c : A Int B ==> c : A |
|
631 \tdx{IntD2} c : A Int B ==> c : B |
|
632 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P |
|
633 |
|
634 \tdx{DiffI} [| c : A; ~ c : B |] ==> c : A - B |
|
635 \tdx{DiffD1} c : A - B ==> c : A |
|
636 \tdx{DiffD2} c : A - B ==> c ~: B |
|
637 \tdx{DiffE} [| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P |
|
638 \end{ttbox} |
|
639 \caption{Union, intersection, difference} \label{zf-Un} |
|
640 \end{figure} |
|
641 |
|
642 |
|
643 \begin{figure} |
|
644 \begin{ttbox} |
|
645 \tdx{consI1} a : cons(a,B) |
|
646 \tdx{consI2} a : B ==> a : cons(b,B) |
|
647 \tdx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B) |
|
648 \tdx{consE} [| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P |
|
649 |
|
650 \tdx{singletonI} a : {\ttlbrace}a{\ttrbrace} |
|
651 \tdx{singletonE} [| a : {\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P |
|
652 \end{ttbox} |
|
653 \caption{Finite and singleton sets} \label{zf-upair2} |
|
654 \end{figure} |
|
655 |
|
656 |
|
657 \begin{figure} |
|
658 \begin{ttbox} |
|
659 \tdx{succI1} i : succ(i) |
|
660 \tdx{succI2} i : j ==> i : succ(j) |
|
661 \tdx{succCI} (~ i:j ==> i=j) ==> i: succ(j) |
|
662 \tdx{succE} [| i : succ(j); i=j ==> P; i:j ==> P |] ==> P |
|
663 \tdx{succ_neq_0} [| succ(n)=0 |] ==> P |
|
664 \tdx{succ_inject} succ(m) = succ(n) ==> m=n |
|
665 \end{ttbox} |
|
666 \caption{The successor function} \label{zf-succ} |
|
667 \end{figure} |
|
668 |
|
669 |
|
670 \begin{figure} |
|
671 \begin{ttbox} |
|
672 \tdx{the_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a |
|
673 \tdx{theI} EX! x. P(x) ==> P(THE x. P(x)) |
|
674 |
|
675 \tdx{if_P} P ==> (if P then a else b) = a |
|
676 \tdx{if_not_P} ~P ==> (if P then a else b) = b |
|
677 |
|
678 \tdx{mem_asym} [| a:b; b:a |] ==> P |
|
679 \tdx{mem_irrefl} a:a ==> P |
|
680 \end{ttbox} |
|
681 \caption{Descriptions; non-circularity} \label{zf-the} |
|
682 \end{figure} |
|
683 |
|
684 |
|
685 \subsection{Unordered pairs and finite sets} |
|
686 Figure~\ref{zf-upair1} presents the principle of unordered pairing, along |
|
687 with its derived rules. Binary union and intersection are defined in terms |
|
688 of ordered pairs (Fig.\ts\ref{zf-Un}). Set difference is also included. The |
|
689 rule \tdx{UnCI} is useful for classical reasoning about unions, |
|
690 like \texttt{disjCI}\@; it supersedes \tdx{UnI1} and |
|
691 \tdx{UnI2}, but these rules are often easier to work with. For |
|
692 intersection and difference we have both elimination and destruction rules. |
|
693 Again, there is no reason to provide a minimal rule set. |
|
694 |
|
695 Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules |
|
696 for~\texttt{cons}, the finite set constructor, and rules for singleton |
|
697 sets. Figure~\ref{zf-succ} presents derived rules for the successor |
|
698 function, which is defined in terms of~\texttt{cons}. The proof that {\tt |
|
699 succ} is injective appears to require the Axiom of Foundation. |
|
700 |
|
701 Definite descriptions (\sdx{THE}) are defined in terms of the singleton |
|
702 set~$\{0\}$, but their derived rules fortunately hide this |
|
703 (Fig.\ts\ref{zf-the}). The rule~\tdx{theI} is difficult to apply |
|
704 because of the two occurrences of~$\Var{P}$. However, |
|
705 \tdx{the_equality} does not have this problem and the files contain |
|
706 many examples of its use. |
|
707 |
|
708 Finally, the impossibility of having both $a\in b$ and $b\in a$ |
|
709 (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to |
|
710 the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence. |
|
711 |
|
712 See the file \texttt{ZF/upair.ML} for full proofs of the rules discussed in |
|
713 this section. |
|
714 |
|
715 |
|
716 %%% subset.ML |
|
717 |
|
718 \begin{figure} |
|
719 \begin{ttbox} |
|
720 \tdx{Union_upper} B:A ==> B <= Union(A) |
|
721 \tdx{Union_least} [| !!x. x:A ==> x<=C |] ==> Union(A) <= C |
|
722 |
|
723 \tdx{Inter_lower} B:A ==> Inter(A) <= B |
|
724 \tdx{Inter_greatest} [| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A) |
|
725 |
|
726 \tdx{Un_upper1} A <= A Un B |
|
727 \tdx{Un_upper2} B <= A Un B |
|
728 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C |
|
729 |
|
730 \tdx{Int_lower1} A Int B <= A |
|
731 \tdx{Int_lower2} A Int B <= B |
|
732 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B |
|
733 |
|
734 \tdx{Diff_subset} A-B <= A |
|
735 \tdx{Diff_contains} [| C<=A; C Int B = 0 |] ==> C <= A-B |
|
736 |
|
737 \tdx{Collect_subset} Collect(A,P) <= A |
|
738 \end{ttbox} |
|
739 \caption{Subset and lattice properties} \label{zf-subset} |
|
740 \end{figure} |
|
741 |
|
742 |
|
743 \subsection{Subset and lattice properties} |
|
744 The subset relation is a complete lattice. Unions form least upper bounds; |
|
745 non-empty intersections form greatest lower bounds. Figure~\ref{zf-subset} |
|
746 shows the corresponding rules. A few other laws involving subsets are |
|
747 included. Proofs are in the file \texttt{ZF/subset.ML}. |
|
748 |
|
749 Reasoning directly about subsets often yields clearer proofs than |
|
750 reasoning about the membership relation. Section~\ref{sec:ZF-pow-example} |
|
751 below presents an example of this, proving the equation ${{\tt Pow}(A)\cap |
|
752 {\tt Pow}(B)}= {\tt Pow}(A\cap B)$. |
|
753 |
|
754 %%% pair.ML |
|
755 |
|
756 \begin{figure} |
|
757 \begin{ttbox} |
|
758 \tdx{Pair_inject1} <a,b> = <c,d> ==> a=c |
|
759 \tdx{Pair_inject2} <a,b> = <c,d> ==> b=d |
|
760 \tdx{Pair_inject} [| <a,b> = <c,d>; [| a=c; b=d |] ==> P |] ==> P |
|
761 \tdx{Pair_neq_0} <a,b>=0 ==> P |
|
762 |
|
763 \tdx{fst_conv} fst(<a,b>) = a |
|
764 \tdx{snd_conv} snd(<a,b>) = b |
|
765 \tdx{split} split(\%x y. c(x,y), <a,b>) = c(a,b) |
|
766 |
|
767 \tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B) |
|
768 |
|
769 \tdx{SigmaE} [| c: Sigma(A,B); |
|
770 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P |
|
771 |
|
772 \tdx{SigmaE2} [| <a,b> : Sigma(A,B); |
|
773 [| a:A; b:B(a) |] ==> P |] ==> P |
|
774 \end{ttbox} |
|
775 \caption{Ordered pairs; projections; general sums} \label{zf-pair} |
|
776 \end{figure} |
|
777 |
|
778 |
|
779 \subsection{Ordered pairs} \label{sec:pairs} |
|
780 |
|
781 Figure~\ref{zf-pair} presents the rules governing ordered pairs, |
|
782 projections and general sums. File \texttt{ZF/pair.ML} contains the |
|
783 full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered |
|
784 pair. This property is expressed as two destruction rules, |
|
785 \tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently |
|
786 as the elimination rule \tdx{Pair_inject}. |
|
787 |
|
788 The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This |
|
789 is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other |
|
790 encodings of ordered pairs. The non-standard ordered pairs mentioned below |
|
791 satisfy $\pair{\emptyset;\emptyset}=\emptyset$. |
|
792 |
|
793 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} |
|
794 assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form |
|
795 $\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \tdx{SigmaE2} |
|
796 merely states that $\pair{a,b}\in \texttt{Sigma}(A,B)$ implies $a\in A$ and |
|
797 $b\in B(a)$. |
|
798 |
|
799 In addition, it is possible to use tuples as patterns in abstractions: |
|
800 \begin{center} |
|
801 {\tt\%<$x$,$y$>. $t$} \quad stands for\quad \texttt{split(\%$x$ $y$.\ $t$)} |
|
802 \end{center} |
|
803 Nested patterns are translated recursively: |
|
804 {\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$ |
|
805 \texttt{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$ |
|
806 $z$.\ $t$))}. The reverse translation is performed upon printing. |
|
807 \begin{warn} |
|
808 The translation between patterns and \texttt{split} is performed automatically |
|
809 by the parser and printer. Thus the internal and external form of a term |
|
810 may differ, which affects proofs. For example the term {\tt |
|
811 (\%<x,y>.<y,x>)<a,b>} requires the theorem \texttt{split} to rewrite to |
|
812 {\tt<b,a>}. |
|
813 \end{warn} |
|
814 In addition to explicit $\lambda$-abstractions, patterns can be used in any |
|
815 variable binding construct which is internally described by a |
|
816 $\lambda$-abstraction. Here are some important examples: |
|
817 \begin{description} |
|
818 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$} |
|
819 \item[Choice:] \texttt{THE~{\it pattern}~.~$P$} |
|
820 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} |
|
821 \item[Comprehension:] \texttt{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}} |
|
822 \end{description} |
|
823 |
|
824 |
|
825 %%% domrange.ML |
|
826 |
|
827 \begin{figure} |
|
828 \begin{ttbox} |
|
829 \tdx{domainI} <a,b>: r ==> a : domain(r) |
|
830 \tdx{domainE} [| a : domain(r); !!y. <a,y>: r ==> P |] ==> P |
|
831 \tdx{domain_subset} domain(Sigma(A,B)) <= A |
|
832 |
|
833 \tdx{rangeI} <a,b>: r ==> b : range(r) |
|
834 \tdx{rangeE} [| b : range(r); !!x. <x,b>: r ==> P |] ==> P |
|
835 \tdx{range_subset} range(A*B) <= B |
|
836 |
|
837 \tdx{fieldI1} <a,b>: r ==> a : field(r) |
|
838 \tdx{fieldI2} <a,b>: r ==> b : field(r) |
|
839 \tdx{fieldCI} (~ <c,a>:r ==> <a,b>: r) ==> a : field(r) |
|
840 |
|
841 \tdx{fieldE} [| a : field(r); |
|
842 !!x. <a,x>: r ==> P; |
|
843 !!x. <x,a>: r ==> P |
|
844 |] ==> P |
|
845 |
|
846 \tdx{field_subset} field(A*A) <= A |
|
847 \end{ttbox} |
|
848 \caption{Domain, range and field of a relation} \label{zf-domrange} |
|
849 \end{figure} |
|
850 |
|
851 \begin{figure} |
|
852 \begin{ttbox} |
|
853 \tdx{imageI} [| <a,b>: r; a:A |] ==> b : r``A |
|
854 \tdx{imageE} [| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P |
|
855 |
|
856 \tdx{vimageI} [| <a,b>: r; b:B |] ==> a : r-``B |
|
857 \tdx{vimageE} [| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P |
|
858 \end{ttbox} |
|
859 \caption{Image and inverse image} \label{zf-domrange2} |
|
860 \end{figure} |
|
861 |
|
862 |
|
863 \subsection{Relations} |
|
864 Figure~\ref{zf-domrange} presents rules involving relations, which are sets |
|
865 of ordered pairs. The converse of a relation~$r$ is the set of all pairs |
|
866 $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then |
|
867 {\cdx{converse}$(r)$} is its inverse. The rules for the domain |
|
868 operation, namely \tdx{domainI} and~\tdx{domainE}, assert that |
|
869 \cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains |
|
870 some pair of the form~$\pair{x,y}$. The range operation is similar, and |
|
871 the field of a relation is merely the union of its domain and range. |
|
872 |
|
873 Figure~\ref{zf-domrange2} presents rules for images and inverse images. |
|
874 Note that these operations are generalisations of range and domain, |
|
875 respectively. See the file \texttt{ZF/domrange.ML} for derivations of the |
|
876 rules. |
|
877 |
|
878 |
|
879 %%% func.ML |
|
880 |
|
881 \begin{figure} |
|
882 \begin{ttbox} |
|
883 \tdx{fun_is_rel} f: Pi(A,B) ==> f <= Sigma(A,B) |
|
884 |
|
885 \tdx{apply_equality} [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b |
|
886 \tdx{apply_equality2} [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c |
|
887 |
|
888 \tdx{apply_type} [| f: Pi(A,B); a:A |] ==> f`a : B(a) |
|
889 \tdx{apply_Pair} [| f: Pi(A,B); a:A |] ==> <a,f`a>: f |
|
890 \tdx{apply_iff} f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b |
|
891 |
|
892 \tdx{fun_extension} [| f : Pi(A,B); g: Pi(A,D); |
|
893 !!x. x:A ==> f`x = g`x |] ==> f=g |
|
894 |
|
895 \tdx{domain_type} [| <a,b> : f; f: Pi(A,B) |] ==> a : A |
|
896 \tdx{range_type} [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a) |
|
897 |
|
898 \tdx{Pi_type} [| f: A->C; !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B) |
|
899 \tdx{domain_of_fun} f: Pi(A,B) ==> domain(f)=A |
|
900 \tdx{range_of_fun} f: Pi(A,B) ==> f: A->range(f) |
|
901 |
|
902 \tdx{restrict} a : A ==> restrict(f,A) ` a = f`a |
|
903 \tdx{restrict_type} [| !!x. x:A ==> f`x: B(x) |] ==> |
|
904 restrict(f,A) : Pi(A,B) |
|
905 \end{ttbox} |
|
906 \caption{Functions} \label{zf-func1} |
|
907 \end{figure} |
|
908 |
|
909 |
|
910 \begin{figure} |
|
911 \begin{ttbox} |
|
912 \tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x)) |
|
913 \tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P |
|
914 |] ==> P |
|
915 |
|
916 \tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B) |
|
917 |
|
918 \tdx{beta} a : A ==> (lam x:A. b(x)) ` a = b(a) |
|
919 \tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f |
|
920 \end{ttbox} |
|
921 \caption{$\lambda$-abstraction} \label{zf-lam} |
|
922 \end{figure} |
|
923 |
|
924 |
|
925 \begin{figure} |
|
926 \begin{ttbox} |
|
927 \tdx{fun_empty} 0: 0->0 |
|
928 \tdx{fun_single} {\ttlbrace}<a,b>{\ttrbrace} : {\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace} |
|
929 |
|
930 \tdx{fun_disjoint_Un} [| f: A->B; g: C->D; A Int C = 0 |] ==> |
|
931 (f Un g) : (A Un C) -> (B Un D) |
|
932 |
|
933 \tdx{fun_disjoint_apply1} [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> |
|
934 (f Un g)`a = f`a |
|
935 |
|
936 \tdx{fun_disjoint_apply2} [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> |
|
937 (f Un g)`c = g`c |
|
938 \end{ttbox} |
|
939 \caption{Constructing functions from smaller sets} \label{zf-func2} |
|
940 \end{figure} |
|
941 |
|
942 |
|
943 \subsection{Functions} |
|
944 Functions, represented by graphs, are notoriously difficult to reason |
|
945 about. The file \texttt{ZF/func.ML} derives many rules, which overlap more |
|
946 than they ought. This section presents the more important rules. |
|
947 |
|
948 Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$, |
|
949 the generalized function space. For example, if $f$ is a function and |
|
950 $\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}). Two functions |
|
951 are equal provided they have equal domains and deliver equals results |
|
952 (\tdx{fun_extension}). |
|
953 |
|
954 By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be |
|
955 refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable |
|
956 family of sets $\{B(x)\}@{x\in A}$. Conversely, by \tdx{range_of_fun}, |
|
957 any dependent typing can be flattened to yield a function type of the form |
|
958 $A\to C$; here, $C={\tt range}(f)$. |
|
959 |
|
960 Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE} |
|
961 describe the graph of the generated function, while \tdx{beta} and |
|
962 \tdx{eta} are the standard conversions. We essentially have a |
|
963 dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}). |
|
964 |
|
965 Figure~\ref{zf-func2} presents some rules that can be used to construct |
|
966 functions explicitly. We start with functions consisting of at most one |
|
967 pair, and may form the union of two functions provided their domains are |
|
968 disjoint. |
|
969 |
|
970 |
|
971 \begin{figure} |
|
972 \begin{ttbox} |
|
973 \tdx{Int_absorb} A Int A = A |
|
974 \tdx{Int_commute} A Int B = B Int A |
|
975 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) |
|
976 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) |
|
977 |
|
978 \tdx{Un_absorb} A Un A = A |
|
979 \tdx{Un_commute} A Un B = B Un A |
|
980 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) |
|
981 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) |
|
982 |
|
983 \tdx{Diff_cancel} A-A = 0 |
|
984 \tdx{Diff_disjoint} A Int (B-A) = 0 |
|
985 \tdx{Diff_partition} A<=B ==> A Un (B-A) = B |
|
986 \tdx{double_complement} [| A<=B; B<= C |] ==> (B - (C-A)) = A |
|
987 \tdx{Diff_Un} A - (B Un C) = (A-B) Int (A-C) |
|
988 \tdx{Diff_Int} A - (B Int C) = (A-B) Un (A-C) |
|
989 |
|
990 \tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) |
|
991 \tdx{Inter_Un_distrib} [| a:A; b:B |] ==> |
|
992 Inter(A Un B) = Inter(A) Int Inter(B) |
|
993 |
|
994 \tdx{Int_Union_RepFun} A Int Union(B) = (UN C:B. A Int C) |
|
995 |
|
996 \tdx{Un_Inter_RepFun} b:B ==> |
|
997 A Un Inter(B) = (INT C:B. A Un C) |
|
998 |
|
999 \tdx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) = |
|
1000 (SUM x:A. C(x)) Un (SUM x:B. C(x)) |
|
1001 |
|
1002 \tdx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) = |
|
1003 (SUM x:C. A(x)) Un (SUM x:C. B(x)) |
|
1004 |
|
1005 \tdx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) = |
|
1006 (SUM x:A. C(x)) Int (SUM x:B. C(x)) |
|
1007 |
|
1008 \tdx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) = |
|
1009 (SUM x:C. A(x)) Int (SUM x:C. B(x)) |
|
1010 \end{ttbox} |
|
1011 \caption{Equalities} \label{zf-equalities} |
|
1012 \end{figure} |
|
1013 |
|
1014 |
|
1015 \begin{figure} |
|
1016 %\begin{constants} |
|
1017 % \cdx{1} & $i$ & & $\{\emptyset\}$ \\ |
|
1018 % \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ |
|
1019 % \cdx{cond} & $[i,i,i]\To i$ & & conditional for \texttt{bool} \\ |
|
1020 % \cdx{not} & $i\To i$ & & negation for \texttt{bool} \\ |
|
1021 % \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for \texttt{bool} \\ |
|
1022 % \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for \texttt{bool} \\ |
|
1023 % \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusive-or for \texttt{bool} |
|
1024 %\end{constants} |
|
1025 % |
|
1026 \begin{ttbox} |
|
1027 \tdx{bool_def} bool == {\ttlbrace}0,1{\ttrbrace} |
|
1028 \tdx{cond_def} cond(b,c,d) == if b=1 then c else d |
|
1029 \tdx{not_def} not(b) == cond(b,0,1) |
|
1030 \tdx{and_def} a and b == cond(a,b,0) |
|
1031 \tdx{or_def} a or b == cond(a,1,b) |
|
1032 \tdx{xor_def} a xor b == cond(a,not(b),b) |
|
1033 |
|
1034 \tdx{bool_1I} 1 : bool |
|
1035 \tdx{bool_0I} 0 : bool |
|
1036 \tdx{boolE} [| c: bool; c=1 ==> P; c=0 ==> P |] ==> P |
|
1037 \tdx{cond_1} cond(1,c,d) = c |
|
1038 \tdx{cond_0} cond(0,c,d) = d |
|
1039 \end{ttbox} |
|
1040 \caption{The booleans} \label{zf-bool} |
|
1041 \end{figure} |
|
1042 |
|
1043 |
|
1044 \section{Further developments} |
|
1045 The next group of developments is complex and extensive, and only |
|
1046 highlights can be covered here. It involves many theories and ML files of |
|
1047 proofs. |
|
1048 |
|
1049 Figure~\ref{zf-equalities} presents commutative, associative, distributive, |
|
1050 and idempotency laws of union and intersection, along with other equations. |
|
1051 See file \texttt{ZF/equalities.ML}. |
|
1052 |
|
1053 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual |
|
1054 operators including a conditional (Fig.\ts\ref{zf-bool}). Although {\ZF} is a |
|
1055 first-order theory, you can obtain the effect of higher-order logic using |
|
1056 \texttt{bool}-valued functions, for example. The constant~\texttt{1} is |
|
1057 translated to \texttt{succ(0)}. |
|
1058 |
|
1059 \begin{figure} |
|
1060 \index{*"+ symbol} |
|
1061 \begin{constants} |
|
1062 \it symbol & \it meta-type & \it priority & \it description \\ |
|
1063 \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ |
|
1064 \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ |
|
1065 \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ |
|
1066 \end{constants} |
|
1067 \begin{ttbox} |
|
1068 \tdx{sum_def} A+B == {\ttlbrace}0{\ttrbrace}*A Un {\ttlbrace}1{\ttrbrace}*B |
|
1069 \tdx{Inl_def} Inl(a) == <0,a> |
|
1070 \tdx{Inr_def} Inr(b) == <1,b> |
|
1071 \tdx{case_def} case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) |
|
1072 |
|
1073 \tdx{sum_InlI} a : A ==> Inl(a) : A+B |
|
1074 \tdx{sum_InrI} b : B ==> Inr(b) : A+B |
|
1075 |
|
1076 \tdx{Inl_inject} Inl(a)=Inl(b) ==> a=b |
|
1077 \tdx{Inr_inject} Inr(a)=Inr(b) ==> a=b |
|
1078 \tdx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P |
|
1079 |
|
1080 \tdx{sumE2} u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y)) |
|
1081 |
|
1082 \tdx{case_Inl} case(c,d,Inl(a)) = c(a) |
|
1083 \tdx{case_Inr} case(c,d,Inr(b)) = d(b) |
|
1084 \end{ttbox} |
|
1085 \caption{Disjoint unions} \label{zf-sum} |
|
1086 \end{figure} |
|
1087 |
|
1088 |
|
1089 Theory \thydx{Sum} defines the disjoint union of two sets, with |
|
1090 injections and a case analysis operator (Fig.\ts\ref{zf-sum}). Disjoint |
|
1091 unions play a role in datatype definitions, particularly when there is |
|
1092 mutual recursion~\cite{paulson-set-II}. |
|
1093 |
|
1094 \begin{figure} |
|
1095 \begin{ttbox} |
|
1096 \tdx{QPair_def} <a;b> == a+b |
|
1097 \tdx{qsplit_def} qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b) |
|
1098 \tdx{qfsplit_def} qfsplit(R,z) == EX x y. z=<x;y> & R(x,y) |
|
1099 \tdx{qconverse_def} qconverse(r) == {\ttlbrace}z. w:r, EX x y. w=<x;y> & z=<y;x>{\ttrbrace} |
|
1100 \tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x;y>{\ttrbrace} |
|
1101 |
|
1102 \tdx{qsum_def} A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) Un ({\ttlbrace}1{\ttrbrace} <*> B) |
|
1103 \tdx{QInl_def} QInl(a) == <0;a> |
|
1104 \tdx{QInr_def} QInr(b) == <1;b> |
|
1105 \tdx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) |
|
1106 \end{ttbox} |
|
1107 \caption{Non-standard pairs, products and sums} \label{zf-qpair} |
|
1108 \end{figure} |
|
1109 |
|
1110 Theory \thydx{QPair} defines a notion of ordered pair that admits |
|
1111 non-well-founded tupling (Fig.\ts\ref{zf-qpair}). Such pairs are written |
|
1112 {\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the |
|
1113 converse operator \cdx{qconverse}, and the summation operator |
|
1114 \cdx{QSigma}. These are completely analogous to the corresponding |
|
1115 versions for standard ordered pairs. The theory goes on to define a |
|
1116 non-standard notion of disjoint sum using non-standard pairs. All of these |
|
1117 concepts satisfy the same properties as their standard counterparts; in |
|
1118 addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive |
|
1119 definitions, for example of infinite lists~\cite{paulson-final}. |
|
1120 |
|
1121 \begin{figure} |
|
1122 \begin{ttbox} |
|
1123 \tdx{bnd_mono_def} bnd_mono(D,h) == |
|
1124 h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X)) |
|
1125 |
|
1126 \tdx{lfp_def} lfp(D,h) == Inter({\ttlbrace}X: Pow(D). h(X) <= X{\ttrbrace}) |
|
1127 \tdx{gfp_def} gfp(D,h) == Union({\ttlbrace}X: Pow(D). X <= h(X){\ttrbrace}) |
|
1128 |
|
1129 |
|
1130 \tdx{lfp_lowerbound} [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A |
|
1131 |
|
1132 \tdx{lfp_subset} lfp(D,h) <= D |
|
1133 |
|
1134 \tdx{lfp_greatest} [| bnd_mono(D,h); |
|
1135 !!X. [| h(X) <= X; X<=D |] ==> A<=X |
|
1136 |] ==> A <= lfp(D,h) |
|
1137 |
|
1138 \tdx{lfp_Tarski} bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) |
|
1139 |
|
1140 \tdx{induct} [| a : lfp(D,h); bnd_mono(D,h); |
|
1141 !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |
|
1142 |] ==> P(a) |
|
1143 |
|
1144 \tdx{lfp_mono} [| bnd_mono(D,h); bnd_mono(E,i); |
|
1145 !!X. X<=D ==> h(X) <= i(X) |
|
1146 |] ==> lfp(D,h) <= lfp(E,i) |
|
1147 |
|
1148 \tdx{gfp_upperbound} [| A <= h(A); A<=D |] ==> A <= gfp(D,h) |
|
1149 |
|
1150 \tdx{gfp_subset} gfp(D,h) <= D |
|
1151 |
|
1152 \tdx{gfp_least} [| bnd_mono(D,h); |
|
1153 !!X. [| X <= h(X); X<=D |] ==> X<=A |
|
1154 |] ==> gfp(D,h) <= A |
|
1155 |
|
1156 \tdx{gfp_Tarski} bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) |
|
1157 |
|
1158 \tdx{coinduct} [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |
|
1159 |] ==> a : gfp(D,h) |
|
1160 |
|
1161 \tdx{gfp_mono} [| bnd_mono(D,h); D <= E; |
|
1162 !!X. X<=D ==> h(X) <= i(X) |
|
1163 |] ==> gfp(D,h) <= gfp(E,i) |
|
1164 \end{ttbox} |
|
1165 \caption{Least and greatest fixedpoints} \label{zf-fixedpt} |
|
1166 \end{figure} |
|
1167 |
|
1168 The Knaster-Tarski Theorem states that every monotone function over a |
|
1169 complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the |
|
1170 Theorem only for a particular lattice, namely the lattice of subsets of a |
|
1171 set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest |
|
1172 fixedpoint operators with corresponding induction and coinduction rules. |
|
1173 These are essential to many definitions that follow, including the natural |
|
1174 numbers and the transitive closure operator. The (co)inductive definition |
|
1175 package also uses the fixedpoint operators~\cite{paulson-CADE}. See |
|
1176 Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski |
|
1177 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle |
|
1178 proofs. |
|
1179 |
|
1180 Monotonicity properties are proved for most of the set-forming operations: |
|
1181 union, intersection, Cartesian product, image, domain, range, etc. These |
|
1182 are useful for applying the Knaster-Tarski Fixedpoint Theorem. The proofs |
|
1183 themselves are trivial applications of Isabelle's classical reasoner. See |
|
1184 file \texttt{ZF/mono.ML}. |
|
1185 |
|
1186 |
|
1187 \begin{figure} |
|
1188 \begin{constants} |
|
1189 \it symbol & \it meta-type & \it priority & \it description \\ |
|
1190 \sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ |
|
1191 \cdx{id} & $i\To i$ & & identity function \\ |
|
1192 \cdx{inj} & $[i,i]\To i$ & & injective function space\\ |
|
1193 \cdx{surj} & $[i,i]\To i$ & & surjective function space\\ |
|
1194 \cdx{bij} & $[i,i]\To i$ & & bijective function space |
|
1195 \end{constants} |
|
1196 |
|
1197 \begin{ttbox} |
|
1198 \tdx{comp_def} r O s == {\ttlbrace}xz : domain(s)*range(r) . |
|
1199 EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r{\ttrbrace} |
|
1200 \tdx{id_def} id(A) == (lam x:A. x) |
|
1201 \tdx{inj_def} inj(A,B) == {\ttlbrace} f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x {\ttrbrace} |
|
1202 \tdx{surj_def} surj(A,B) == {\ttlbrace} f: A->B . ALL y:B. EX x:A. f`x=y {\ttrbrace} |
|
1203 \tdx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B) |
|
1204 |
|
1205 |
|
1206 \tdx{left_inverse} [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a |
|
1207 \tdx{right_inverse} [| f: inj(A,B); b: range(f) |] ==> |
|
1208 f`(converse(f)`b) = b |
|
1209 |
|
1210 \tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A) |
|
1211 \tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A) |
|
1212 |
|
1213 \tdx{comp_type} [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C |
|
1214 \tdx{comp_assoc} (r O s) O t = r O (s O t) |
|
1215 |
|
1216 \tdx{left_comp_id} r<=A*B ==> id(B) O r = r |
|
1217 \tdx{right_comp_id} r<=A*B ==> r O id(A) = r |
|
1218 |
|
1219 \tdx{comp_func} [| g:A->B; f:B->C |] ==> (f O g):A->C |
|
1220 \tdx{comp_func_apply} [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a) |
|
1221 |
|
1222 \tdx{comp_inj} [| g:inj(A,B); f:inj(B,C) |] ==> (f O g):inj(A,C) |
|
1223 \tdx{comp_surj} [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C) |
|
1224 \tdx{comp_bij} [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C) |
|
1225 |
|
1226 \tdx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A) |
|
1227 \tdx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B) |
|
1228 |
|
1229 \tdx{bij_disjoint_Un} |
|
1230 [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> |
|
1231 (f Un g) : bij(A Un C, B Un D) |
|
1232 |
|
1233 \tdx{restrict_bij} [| f:inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C) |
|
1234 \end{ttbox} |
|
1235 \caption{Permutations} \label{zf-perm} |
|
1236 \end{figure} |
|
1237 |
|
1238 The theory \thydx{Perm} is concerned with permutations (bijections) and |
|
1239 related concepts. These include composition of relations, the identity |
|
1240 relation, and three specialized function spaces: injective, surjective and |
|
1241 bijective. Figure~\ref{zf-perm} displays many of their properties that |
|
1242 have been proved. These results are fundamental to a treatment of |
|
1243 equipollence and cardinality. |
|
1244 |
|
1245 \begin{figure}\small |
|
1246 \index{#*@{\tt\#*} symbol} |
|
1247 \index{*div symbol} |
|
1248 \index{*mod symbol} |
|
1249 \index{#+@{\tt\#+} symbol} |
|
1250 \index{#-@{\tt\#-} symbol} |
|
1251 \begin{constants} |
|
1252 \it symbol & \it meta-type & \it priority & \it description \\ |
|
1253 \cdx{nat} & $i$ & & set of natural numbers \\ |
|
1254 \cdx{nat_case}& $[i,i\To i,i]\To i$ & & conditional for $nat$\\ |
|
1255 \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ |
|
1256 \tt div & $[i,i]\To i$ & Left 70 & division\\ |
|
1257 \tt mod & $[i,i]\To i$ & Left 70 & modulus\\ |
|
1258 \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ |
|
1259 \tt \#- & $[i,i]\To i$ & Left 65 & subtraction |
|
1260 \end{constants} |
|
1261 |
|
1262 \begin{ttbox} |
|
1263 \tdx{nat_def} nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace} |
|
1264 |
|
1265 \tdx{mod_def} m mod n == transrec(m, \%j f. if j:n then j else f`(j#-n)) |
|
1266 \tdx{div_def} m div n == transrec(m, \%j f. if j:n then 0 else succ(f`(j#-n))) |
|
1267 |
|
1268 \tdx{nat_case_def} nat_case(a,b,k) == |
|
1269 THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x)) |
|
1270 |
|
1271 \tdx{nat_0I} 0 : nat |
|
1272 \tdx{nat_succI} n : nat ==> succ(n) : nat |
|
1273 |
|
1274 \tdx{nat_induct} |
|
1275 [| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |
|
1276 |] ==> P(n) |
|
1277 |
|
1278 \tdx{nat_case_0} nat_case(a,b,0) = a |
|
1279 \tdx{nat_case_succ} nat_case(a,b,succ(m)) = b(m) |
|
1280 |
|
1281 \tdx{add_0} 0 #+ n = n |
|
1282 \tdx{add_succ} succ(m) #+ n = succ(m #+ n) |
|
1283 |
|
1284 \tdx{mult_type} [| m:nat; n:nat |] ==> m #* n : nat |
|
1285 \tdx{mult_0} 0 #* n = 0 |
|
1286 \tdx{mult_succ} succ(m) #* n = n #+ (m #* n) |
|
1287 \tdx{mult_commute} [| m:nat; n:nat |] ==> m #* n = n #* m |
|
1288 \tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k) |
|
1289 \tdx{mult_assoc} |
|
1290 [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k) |
|
1291 \tdx{mod_quo_equality} |
|
1292 [| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m |
|
1293 \end{ttbox} |
|
1294 \caption{The natural numbers} \label{zf-nat} |
|
1295 \end{figure} |
|
1296 |
|
1297 Theory \thydx{Nat} defines the natural numbers and mathematical |
|
1298 induction, along with a case analysis operator. The set of natural |
|
1299 numbers, here called \texttt{nat}, is known in set theory as the ordinal~$\omega$. |
|
1300 |
|
1301 Theory \thydx{Arith} develops arithmetic on the natural numbers |
|
1302 (Fig.\ts\ref{zf-nat}). Addition, multiplication and subtraction are defined |
|
1303 by primitive recursion. Division and remainder are defined by repeated |
|
1304 subtraction, which requires well-founded recursion; the termination argument |
|
1305 relies on the divisor's being non-zero. Many properties are proved: |
|
1306 commutative, associative and distributive laws, identity and cancellation |
|
1307 laws, etc. The most interesting result is perhaps the theorem $a \bmod b + |
|
1308 (a/b)\times b = a$. |
|
1309 |
|
1310 Theory \thydx{Univ} defines a `universe' $\texttt{univ}(A)$, which is used by |
|
1311 the datatype package. This set contains $A$ and the |
|
1312 natural numbers. Vitally, it is closed under finite products: ${\tt |
|
1313 univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$. This theory also |
|
1314 defines the cumulative hierarchy of axiomatic set theory, which |
|
1315 traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The |
|
1316 `universe' is a simple generalization of~$V@\omega$. |
|
1317 |
|
1318 Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, which is used by |
|
1319 the datatype package to construct codatatypes such as streams. It is |
|
1320 analogous to ${\tt univ}(A)$ (and is defined in terms of it) but is closed |
|
1321 under the non-standard product and sum. |
|
1322 |
|
1323 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator; |
|
1324 ${\tt Fin}(A)$ is the set of all finite sets over~$A$. The theory employs |
|
1325 Isabelle's inductive definition package, which proves various rules |
|
1326 automatically. The induction rule shown is stronger than the one proved by |
|
1327 the package. The theory also defines the set of all finite functions |
|
1328 between two given sets. |
|
1329 |
|
1330 \begin{figure} |
|
1331 \begin{ttbox} |
|
1332 \tdx{Fin.emptyI} 0 : Fin(A) |
|
1333 \tdx{Fin.consI} [| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A) |
|
1334 |
|
1335 \tdx{Fin_induct} |
|
1336 [| b: Fin(A); |
|
1337 P(0); |
|
1338 !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) |
|
1339 |] ==> P(b) |
|
1340 |
|
1341 \tdx{Fin_mono} A<=B ==> Fin(A) <= Fin(B) |
|
1342 \tdx{Fin_UnI} [| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A) |
|
1343 \tdx{Fin_UnionI} C : Fin(Fin(A)) ==> Union(C) : Fin(A) |
|
1344 \tdx{Fin_subset} [| c<=b; b: Fin(A) |] ==> c: Fin(A) |
|
1345 \end{ttbox} |
|
1346 \caption{The finite set operator} \label{zf-fin} |
|
1347 \end{figure} |
|
1348 |
|
1349 \begin{figure} |
|
1350 \begin{constants} |
|
1351 \it symbol & \it meta-type & \it priority & \it description \\ |
|
1352 \cdx{list} & $i\To i$ && lists over some set\\ |
|
1353 \cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\ |
|
1354 \cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\ |
|
1355 \cdx{length} & $i\To i$ & & length of a list\\ |
|
1356 \cdx{rev} & $i\To i$ & & reverse of a list\\ |
|
1357 \tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ |
|
1358 \cdx{flat} & $i\To i$ & & append of list of lists |
|
1359 \end{constants} |
|
1360 |
|
1361 \underscoreon %%because @ is used here |
|
1362 \begin{ttbox} |
|
1363 \tdx{NilI} Nil : list(A) |
|
1364 \tdx{ConsI} [| a: A; l: list(A) |] ==> Cons(a,l) : list(A) |
|
1365 |
|
1366 \tdx{List.induct} |
|
1367 [| l: list(A); |
|
1368 P(Nil); |
|
1369 !!x y. [| x: A; y: list(A); P(y) |] ==> P(Cons(x,y)) |
|
1370 |] ==> P(l) |
|
1371 |
|
1372 \tdx{Cons_iff} Cons(a,l)=Cons(a',l') <-> a=a' & l=l' |
|
1373 \tdx{Nil_Cons_iff} ~ Nil=Cons(a,l) |
|
1374 |
|
1375 \tdx{list_mono} A<=B ==> list(A) <= list(B) |
|
1376 |
|
1377 \tdx{map_ident} l: list(A) ==> map(\%u. u, l) = l |
|
1378 \tdx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l) |
|
1379 \tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys) |
|
1380 \tdx{map_type} |
|
1381 [| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B) |
|
1382 \tdx{map_flat} |
|
1383 ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) |
|
1384 \end{ttbox} |
|
1385 \caption{Lists} \label{zf-list} |
|
1386 \end{figure} |
|
1387 |
|
1388 |
|
1389 Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$. The |
|
1390 definition employs Isabelle's datatype package, which defines the introduction |
|
1391 and induction rules automatically, as well as the constructors, case operator |
|
1392 (\verb|list_case|) and recursion operator. The theory then defines the usual |
|
1393 list functions by primitive recursion. See theory \texttt{List}. |
|
1394 |
|
1395 |
|
1396 \section{Simplification and classical reasoning} |
|
1397 |
|
1398 {\ZF} inherits simplification from {\FOL} but adopts it for set theory. The |
|
1399 extraction of rewrite rules takes the {\ZF} primitives into account. It can |
|
1400 strip bounded universal quantifiers from a formula; for example, ${\forall |
|
1401 x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp |
|
1402 f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in |
|
1403 A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in A-B$. |
|
1404 |
|
1405 Simplification tactics tactics such as \texttt{Asm_simp_tac} and |
|
1406 \texttt{Full_simp_tac} use the default simpset (\texttt{simpset()}), which |
|
1407 works for most purposes. A small simplification set for set theory is |
|
1408 called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal |
|
1409 starting point. \texttt{ZF_ss} contains congruence rules for all the binding |
|
1410 operators of {\ZF}\@. It contains all the conversion rules, such as |
|
1411 \texttt{fst} and \texttt{snd}, as well as the rewrites shown in |
|
1412 Fig.\ts\ref{zf-simpdata}. See the file \texttt{ZF/simpdata.ML} for a fuller |
|
1413 list. |
|
1414 |
|
1415 As for the classical reasoner, tactics such as \texttt{Blast_tac} and {\tt |
|
1416 Best_tac} refer to the default claset (\texttt{claset()}). This works for |
|
1417 most purposes. Named clasets include \ttindexbold{ZF_cs} (basic set theory) |
|
1418 and \ttindexbold{le_cs} (useful for reasoning about the relations $<$ and |
|
1419 $\le$). You can use \ttindex{FOL_cs} as a minimal basis for building your own |
|
1420 clasets. See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
|
1421 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. |
|
1422 |
|
1423 |
|
1424 \begin{figure} |
|
1425 \begin{eqnarray*} |
|
1426 a\in \emptyset & \bimp & \bot\\ |
|
1427 a \in A \un B & \bimp & a\in A \disj a\in B\\ |
|
1428 a \in A \int B & \bimp & a\in A \conj a\in B\\ |
|
1429 a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\ |
|
1430 \pair{a,b}\in {\tt Sigma}(A,B) |
|
1431 & \bimp & a\in A \conj b\in B(a)\\ |
|
1432 a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\ |
|
1433 (\forall x \in \emptyset. P(x)) & \bimp & \top\\ |
|
1434 (\forall x \in A. \top) & \bimp & \top |
|
1435 \end{eqnarray*} |
|
1436 \caption{Some rewrite rules for set theory} \label{zf-simpdata} |
|
1437 \end{figure} |
|
1438 |
|
1439 |
|
1440 \section{Datatype definitions} |
|
1441 \label{sec:ZF:datatype} |
|
1442 \index{*datatype|(} |
|
1443 |
|
1444 The \ttindex{datatype} definition package of \ZF\ constructs inductive |
|
1445 datatypes similar to those of \ML. It can also construct coinductive |
|
1446 datatypes (codatatypes), which are non-well-founded structures such as |
|
1447 streams. It defines the set using a fixed-point construction and proves |
|
1448 induction rules, as well as theorems for recursion and case combinators. It |
|
1449 supplies mechanisms for reasoning about freeness. The datatype package can |
|
1450 handle both mutual and indirect recursion. |
|
1451 |
|
1452 |
|
1453 \subsection{Basics} |
|
1454 \label{subsec:datatype:basics} |
|
1455 |
|
1456 A \texttt{datatype} definition has the following form: |
|
1457 \[ |
|
1458 \begin{array}{llcl} |
|
1459 \mathtt{datatype} & t@1(A@1,\ldots,A@h) & = & |
|
1460 constructor^1@1 ~\mid~ \ldots ~\mid~ constructor^1@{k@1} \\ |
|
1461 & & \vdots \\ |
|
1462 \mathtt{and} & t@n(A@1,\ldots,A@h) & = & |
|
1463 constructor^n@1~ ~\mid~ \ldots ~\mid~ constructor^n@{k@n} |
|
1464 \end{array} |
|
1465 \] |
|
1466 Here $t@1$, \ldots,~$t@n$ are identifiers and $A@1$, \ldots,~$A@h$ are |
|
1467 variables: the datatype's parameters. Each constructor specification has the |
|
1468 form \dquotesoff |
|
1469 \[ C \hbox{\tt~( } \hbox{\tt"} x@1 \hbox{\tt:} T@1 \hbox{\tt"},\; |
|
1470 \ldots,\; |
|
1471 \hbox{\tt"} x@m \hbox{\tt:} T@m \hbox{\tt"} |
|
1472 \hbox{\tt~)} |
|
1473 \] |
|
1474 Here $C$ is the constructor name, and variables $x@1$, \ldots,~$x@m$ are the |
|
1475 constructor arguments, belonging to the sets $T@1$, \ldots, $T@m$, |
|
1476 respectively. Typically each $T@j$ is either a constant set, a datatype |
|
1477 parameter (one of $A@1$, \ldots, $A@h$) or a recursive occurrence of one of |
|
1478 the datatypes, say $t@i(A@1,\ldots,A@h)$. More complex possibilities exist, |
|
1479 but they are much harder to realize. Often, additional information must be |
|
1480 supplied in the form of theorems. |
|
1481 |
|
1482 A datatype can occur recursively as the argument of some function~$F$. This |
|
1483 is called a {\em nested} (or \emph{indirect}) occurrence. It is only allowed |
|
1484 if the datatype package is given a theorem asserting that $F$ is monotonic. |
|
1485 If the datatype has indirect occurrences, then Isabelle/ZF does not support |
|
1486 recursive function definitions. |
|
1487 |
|
1488 A simple example of a datatype is \texttt{list}, which is built-in, and is |
|
1489 defined by |
|
1490 \begin{ttbox} |
|
1491 consts list :: i=>i |
|
1492 datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)") |
|
1493 \end{ttbox} |
|
1494 Note that the datatype operator must be declared as a constant first. |
|
1495 However, the package declares the constructors. Here, \texttt{Nil} gets type |
|
1496 $i$ and \texttt{Cons} gets type $[i,i]\To i$. |
|
1497 |
|
1498 Trees and forests can be modelled by the mutually recursive datatype |
|
1499 definition |
|
1500 \begin{ttbox} |
|
1501 consts tree, forest, tree_forest :: i=>i |
|
1502 datatype "tree(A)" = Tcons ("a: A", "f: forest(A)") |
|
1503 and "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") |
|
1504 \end{ttbox} |
|
1505 Here $\texttt{tree}(A)$ is the set of trees over $A$, $\texttt{forest}(A)$ is |
|
1506 the set of forests over $A$, and $\texttt{tree_forest}(A)$ is the union of |
|
1507 the previous two sets. All three operators must be declared first. |
|
1508 |
|
1509 The datatype \texttt{term}, which is defined by |
|
1510 \begin{ttbox} |
|
1511 consts term :: i=>i |
|
1512 datatype "term(A)" = Apply ("a: A", "l: list(term(A))") |
|
1513 monos "[list_mono]" |
|
1514 \end{ttbox} |
|
1515 is an example of nested recursion. (The theorem \texttt{list_mono} is proved |
|
1516 in file \texttt{List.ML}, and the \texttt{term} example is devaloped in theory |
|
1517 \thydx{ex/Term}.) |
|
1518 |
|
1519 \subsubsection{Freeness of the constructors} |
|
1520 |
|
1521 Constructors satisfy {\em freeness} properties. Constructions are distinct, |
|
1522 for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for |
|
1523 example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$. |
|
1524 Because the number of freeness is quadratic in the number of constructors, the |
|
1525 datatype package does not prove them, but instead provides several means of |
|
1526 proving them dynamically. For the \texttt{list} datatype, freeness reasoning |
|
1527 can be done in two ways: by simplifying with the theorems |
|
1528 \texttt{list.free_iffs} or by invoking the classical reasoner with |
|
1529 \texttt{list.free_SEs} as safe elimination rules. Occasionally this exposes |
|
1530 the underlying representation of some constructor, which can be rectified |
|
1531 using the command \hbox{\tt fold_tac list.con_defs}. |
|
1532 |
|
1533 \subsubsection{Structural induction} |
|
1534 |
|
1535 The datatype package also provides structural induction rules. For datatypes |
|
1536 without mutual or nested recursion, the rule has the form exemplified by |
|
1537 \texttt{list.induct} in Fig.\ts\ref{zf-list}. For mutually recursive |
|
1538 datatypes, the induction rule is supplied in two forms. Consider datatype |
|
1539 \texttt{TF}. The rule \texttt{tree_forest.induct} performs induction over a |
|
1540 single predicate~\texttt{P}, which is presumed to be defined for both trees |
|
1541 and forests: |
|
1542 \begin{ttbox} |
|
1543 [| x : tree_forest(A); |
|
1544 !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); P(Fnil); |
|
1545 !!f t. [| t : tree(A); P(t); f : forest(A); P(f) |] |
|
1546 ==> P(Fcons(t, f)) |
|
1547 |] ==> P(x) |
|
1548 \end{ttbox} |
|
1549 The rule \texttt{tree_forest.mutual_induct} performs induction over two |
|
1550 distinct predicates, \texttt{P_tree} and \texttt{P_forest}. |
|
1551 \begin{ttbox} |
|
1552 [| !!a f. |
|
1553 [| a : A; f : forest(A); P_forest(f) |] ==> P_tree(Tcons(a, f)); |
|
1554 P_forest(Fnil); |
|
1555 !!f t. [| t : tree(A); P_tree(t); f : forest(A); P_forest(f) |] |
|
1556 ==> P_forest(Fcons(t, f)) |
|
1557 |] ==> (ALL za. za : tree(A) --> P_tree(za)) & |
|
1558 (ALL za. za : forest(A) --> P_forest(za)) |
|
1559 \end{ttbox} |
|
1560 |
|
1561 For datatypes with nested recursion, such as the \texttt{term} example from |
|
1562 above, things are a bit more complicated. The rule \texttt{term.induct} |
|
1563 refers to the monotonic operator, \texttt{list}: |
|
1564 \begin{ttbox} |
|
1565 [| x : term(A); |
|
1566 !!a l. [| a : A; l : list(Collect(term(A), P)) |] ==> P(Apply(a, l)) |
|
1567 |] ==> P(x) |
|
1568 \end{ttbox} |
|
1569 The file \texttt{ex/Term.ML} derives two higher-level induction rules, one of |
|
1570 which is particularly useful for proving equations: |
|
1571 \begin{ttbox} |
|
1572 [| t : term(A); |
|
1573 !!x zs. [| x : A; zs : list(term(A)); map(f, zs) = map(g, zs) |] |
|
1574 ==> f(Apply(x, zs)) = g(Apply(x, zs)) |
|
1575 |] ==> f(t) = g(t) |
|
1576 \end{ttbox} |
|
1577 How this can be generalized to other nested datatypes is a matter for future |
|
1578 research. |
|
1579 |
|
1580 |
|
1581 \subsubsection{The \texttt{case} operator} |
|
1582 |
|
1583 The package defines an operator for performing case analysis over the |
|
1584 datatype. For \texttt{list}, it is called \texttt{list_case} and satisfies |
|
1585 the equations |
|
1586 \begin{ttbox} |
|
1587 list_case(f_Nil, f_Cons, []) = f_Nil |
|
1588 list_case(f_Nil, f_Cons, Cons(a, l)) = f_Cons(a, l) |
|
1589 \end{ttbox} |
|
1590 Here \texttt{f_Nil} is the value to return if the argument is \texttt{Nil} and |
|
1591 \texttt{f_Cons} is a function that computes the value to return if the |
|
1592 argument has the form $\texttt{Cons}(a,l)$. The function can be expressed as |
|
1593 an abstraction, over patterns if desired (\S\ref{sec:pairs}). |
|
1594 |
|
1595 For mutually recursive datatypes, there is a single \texttt{case} operator. |
|
1596 In the tree/forest example, the constant \texttt{tree_forest_case} handles all |
|
1597 of the constructors of the two datatypes. |
|
1598 |
|
1599 |
|
1600 |
|
1601 |
|
1602 \subsection{Defining datatypes} |
|
1603 |
|
1604 The theory syntax for datatype definitions is shown in |
|
1605 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype |
|
1606 definition has to obey the rules stated in the previous section. As a result |
|
1607 the theory is extended with the new types, the constructors, and the theorems |
|
1608 listed in the previous section. The quotation marks are necessary because |
|
1609 they enclose general Isabelle formul\ae. |
|
1610 |
|
1611 \begin{figure} |
|
1612 \begin{rail} |
|
1613 datatype : ( 'datatype' | 'codatatype' ) datadecls; |
|
1614 |
|
1615 datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' |
|
1616 ; |
|
1617 constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) |
|
1618 ; |
|
1619 consargs : '(' ('"' var ':' term '"' + ',') ')' |
|
1620 ; |
|
1621 \end{rail} |
|
1622 \caption{Syntax of datatype declarations} |
|
1623 \label{datatype-grammar} |
|
1624 \end{figure} |
|
1625 |
|
1626 Codatatypes are declared like datatypes and are identical to them in every |
|
1627 respect except that they have a coinduction rule instead of an induction rule. |
|
1628 Note that while an induction rule has the effect of limiting the values |
|
1629 contained in the set, a coinduction rule gives a way of constructing new |
|
1630 values of the set. |
|
1631 |
|
1632 Most of the theorems about datatypes become part of the default simpset. You |
|
1633 never need to see them again because the simplifier applies them |
|
1634 automatically. Add freeness properties (\texttt{free_iffs}) to the simpset |
|
1635 when you want them. Induction or exhaustion are usually invoked by hand, |
|
1636 usually via these special-purpose tactics: |
|
1637 \begin{ttdescription} |
|
1638 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural |
|
1639 induction on variable $x$ to subgoal $i$, provided the type of $x$ is a |
|
1640 datatype. The induction variable should not occur among other assumptions |
|
1641 of the subgoal. |
|
1642 \end{ttdescription} |
|
1643 In some cases, induction is overkill and a case distinction over all |
|
1644 constructors of the datatype suffices. |
|
1645 \begin{ttdescription} |
|
1646 \item[\ttindexbold{exhaust_tac} {\tt"}$x${\tt"} $i$] |
|
1647 performs an exhaustive case analysis for the variable~$x$. |
|
1648 \end{ttdescription} |
|
1649 |
|
1650 Both tactics can only be applied to a variable, whose typing must be given in |
|
1651 some assumption, for example the assumption \texttt{x:\ list(A)}. The tactics |
|
1652 also work for the natural numbers (\texttt{nat}) and disjoint sums, although |
|
1653 these sets were not defined using the datatype package. (Disjoint sums are |
|
1654 not recursive, so only \texttt{exhaust_tac} is available.) |
|
1655 |
|
1656 \bigskip |
|
1657 Here are some more details for the technically minded. Processing the |
|
1658 theory file produces an \ML\ structure which, in addition to the usual |
|
1659 components, contains a structure named $t$ for each datatype $t$ defined in |
|
1660 the file. Each structure $t$ contains the following elements: |
|
1661 \begin{ttbox} |
|
1662 val intrs : thm list \textrm{the introduction rules} |
|
1663 val elim : thm \textrm{the elimination (case analysis) rule} |
|
1664 val induct : thm \textrm{the standard induction rule} |
|
1665 val mutual_induct : thm \textrm{the mutual induction rule, or \texttt{True}} |
|
1666 val case_eqns : thm list \textrm{equations for the case operator} |
|
1667 val recursor_eqns : thm list \textrm{equations for the recursor} |
|
1668 val con_defs : thm list \textrm{definitions of the case operator and constructors} |
|
1669 val free_iffs : thm list \textrm{logical equivalences for proving freeness} |
|
1670 val free_SEs : thm list \textrm{elimination rules for proving freeness} |
|
1671 val mk_free : string -> thm \textrm{A function for proving freeness theorems} |
|
1672 val mk_cases : thm list -> string -> thm \textrm{case analysis, see below} |
|
1673 val defs : thm list \textrm{definitions of operators} |
|
1674 val bnd_mono : thm list \textrm{monotonicity property} |
|
1675 val dom_subset : thm list \textrm{inclusion in `bounding set'} |
|
1676 \end{ttbox} |
|
1677 Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for |
|
1678 example, the \texttt{list} datatype's introduction rules are bound to the |
|
1679 identifiers \texttt{Nil_I} and \texttt{Cons_I}. |
|
1680 |
|
1681 For a codatatype, the component \texttt{coinduct} is the coinduction rule, |
|
1682 replacing the \texttt{induct} component. |
|
1683 |
|
1684 See the theories \texttt{ex/Ntree} and \texttt{ex/Brouwer} for examples of |
|
1685 infinitely branching datatypes. See theory \texttt{ex/LList} for an example |
|
1686 of a codatatype. Some of these theories illustrate the use of additional, |
|
1687 undocumented features of the datatype package. Datatype definitions are |
|
1688 reduced to inductive definitions, and the advanced features should be |
|
1689 understood in that light. |
|
1690 |
|
1691 |
|
1692 \subsection{Examples} |
|
1693 |
|
1694 \subsubsection{The datatype of binary trees} |
|
1695 |
|
1696 Let us define the set $\texttt{bt}(A)$ of binary trees over~$A$. The theory |
|
1697 must contain these lines: |
|
1698 \begin{ttbox} |
|
1699 consts bt :: i=>i |
|
1700 datatype "bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)") |
|
1701 \end{ttbox} |
|
1702 After loading the theory, we can prove, for example, that no tree equals its |
|
1703 left branch. To ease the induction, we state the goal using quantifiers. |
|
1704 \begin{ttbox} |
|
1705 Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l"; |
|
1706 {\out Level 0} |
|
1707 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} |
|
1708 {\out 1. l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} |
|
1709 \end{ttbox} |
|
1710 This can be proved by the structural induction tactic: |
|
1711 \begin{ttbox} |
|
1712 by (induct_tac "l" 1); |
|
1713 {\out Level 1} |
|
1714 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} |
|
1715 {\out 1. ALL x r. Br(x, Lf, r) ~= Lf} |
|
1716 {\out 2. !!a t1 t2.} |
|
1717 {\out [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);} |
|
1718 {\out ALL x r. Br(x, t2, r) ~= t2 |]} |
|
1719 {\out ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)} |
|
1720 \end{ttbox} |
|
1721 Both subgoals are proved using the simplifier. Tactic |
|
1722 \texttt{asm_full_simp_tac} is used, rewriting the assumptions. |
|
1723 This is because simplification using the freeness properties can unfold the |
|
1724 definition of constructor~\texttt{Br}, so we arrange that all occurrences are |
|
1725 unfolded. |
|
1726 \begin{ttbox} |
|
1727 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs))); |
|
1728 {\out Level 2} |
|
1729 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} |
|
1730 {\out No subgoals!} |
|
1731 \end{ttbox} |
|
1732 To remove the quantifiers from the induction formula, we save the theorem using |
|
1733 \ttindex{qed_spec_mp}. |
|
1734 \begin{ttbox} |
|
1735 qed_spec_mp "Br_neq_left"; |
|
1736 {\out val Br_neq_left = "?l : bt(?A) ==> Br(?x, ?l, ?r) ~= ?l" : thm} |
|
1737 \end{ttbox} |
|
1738 |
|
1739 When there are only a few constructors, we might prefer to prove the freenness |
|
1740 theorems for each constructor. This is trivial, using the function given us |
|
1741 for that purpose: |
|
1742 \begin{ttbox} |
|
1743 val Br_iff = bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'"; |
|
1744 {\out val Br_iff =} |
|
1745 {\out "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->} |
|
1746 {\out ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm} |
|
1747 \end{ttbox} |
|
1748 |
|
1749 The purpose of \ttindex{mk_cases} is to generate simplified instances of the |
|
1750 elimination (case analysis) rule. Its theorem list argument is a list of |
|
1751 constructor definitions, which it uses for freeness reasoning. For example, |
|
1752 this instance of the elimination rule propagates type-checking information |
|
1753 from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$: |
|
1754 \begin{ttbox} |
|
1755 val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)"; |
|
1756 {\out val BrE =} |
|
1757 {\out "[| Br(?a, ?l, ?r) : bt(?A);} |
|
1758 {\out [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm} |
|
1759 \end{ttbox} |
|
1760 |
|
1761 |
|
1762 \subsubsection{Mixfix syntax in datatypes} |
|
1763 |
|
1764 Mixfix syntax is sometimes convenient. The theory \texttt{ex/PropLog} makes a |
|
1765 deep embedding of propositional logic: |
|
1766 \begin{ttbox} |
|
1767 consts prop :: i |
|
1768 datatype "prop" = Fls |
|
1769 | Var ("n: nat") ("#_" [100] 100) |
|
1770 | "=>" ("p: prop", "q: prop") (infixr 90) |
|
1771 \end{ttbox} |
|
1772 The second constructor has a special $\#n$ syntax, while the third constructor |
|
1773 is an infixed arrow. |
|
1774 |
|
1775 |
|
1776 \subsubsection{A giant enumeration type} |
|
1777 |
|
1778 This example shows a datatype that consists of 60 constructors: |
|
1779 \begin{ttbox} |
|
1780 consts enum :: i |
|
1781 datatype |
|
1782 "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09 |
|
1783 | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19 |
|
1784 | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29 |
|
1785 | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39 |
|
1786 | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49 |
|
1787 | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59 |
|
1788 end |
|
1789 \end{ttbox} |
|
1790 The datatype package scales well. Even though all properties are proved |
|
1791 rather than assumed, full processing of this definition takes under 15 seconds |
|
1792 (on a 300 MHz Pentium). The constructors have a balanced representation, |
|
1793 essentially binary notation, so freeness properties can be proved fast. |
|
1794 \begin{ttbox} |
|
1795 Goal "C00 ~= C01"; |
|
1796 by (simp_tac (simpset() addsimps enum.free_iffs) 1); |
|
1797 \end{ttbox} |
|
1798 You need not derive such inequalities explicitly. The simplifier will dispose |
|
1799 of them automatically, given the theorem list \texttt{free_iffs}. |
|
1800 |
|
1801 \index{*datatype|)} |
|
1802 |
|
1803 |
|
1804 \subsection{Recursive function definitions}\label{sec:ZF:recursive} |
|
1805 \index{recursive functions|see{recursion}} |
|
1806 \index{*primrec|(} |
|
1807 |
|
1808 Datatypes come with a uniform way of defining functions, {\bf primitive |
|
1809 recursion}. Such definitions rely on the recursion operator defined by the |
|
1810 datatype package. Isabelle proves the desired recursion equations as |
|
1811 theorems. |
|
1812 |
|
1813 In principle, one could introduce primitive recursive functions by asserting |
|
1814 their reduction rules as new axioms. Here is a dangerous way of defining the |
|
1815 append function for lists: |
|
1816 \begin{ttbox}\slshape |
|
1817 consts "\at" :: [i,i]=>i (infixr 60) |
|
1818 rules |
|
1819 app_Nil "[] \at ys = ys" |
|
1820 app_Cons "(Cons(a,l)) \at ys = Cons(a, l \at ys)" |
|
1821 \end{ttbox} |
|
1822 Asserting axioms brings the danger of accidentally asserting nonsense. It |
|
1823 should be avoided at all costs! |
|
1824 |
|
1825 The \ttindex{primrec} declaration is a safe means of defining primitive |
|
1826 recursive functions on datatypes: |
|
1827 \begin{ttbox} |
|
1828 consts "\at" :: [i,i]=>i (infixr 60) |
|
1829 primrec |
|
1830 "[] \at ys = ys" |
|
1831 "(Cons(a,l)) \at ys = Cons(a, l \at ys)" |
|
1832 \end{ttbox} |
|
1833 Isabelle will now check that the two rules do indeed form a primitive |
|
1834 recursive definition. For example, the declaration |
|
1835 \begin{ttbox} |
|
1836 primrec |
|
1837 "[] \at ys = us" |
|
1838 \end{ttbox} |
|
1839 is rejected with an error message ``\texttt{Extra variables on rhs}''. |
|
1840 |
|
1841 |
|
1842 \subsubsection{Syntax of recursive definitions} |
|
1843 |
|
1844 The general form of a primitive recursive definition is |
|
1845 \begin{ttbox} |
|
1846 primrec |
|
1847 {\it reduction rules} |
|
1848 \end{ttbox} |
|
1849 where \textit{reduction rules} specify one or more equations of the form |
|
1850 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, |
|
1851 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$ |
|
1852 contains only the free variables on the left-hand side, and all recursive |
|
1853 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. |
|
1854 There must be at most one reduction rule for each constructor. The order is |
|
1855 immaterial. For missing constructors, the function is defined to return zero. |
|
1856 |
|
1857 All reduction rules are added to the default simpset. |
|
1858 If you would like to refer to some rule by name, then you must prefix |
|
1859 the rule with an identifier. These identifiers, like those in the |
|
1860 \texttt{rules} section of a theory, will be visible at the \ML\ level. |
|
1861 |
|
1862 The reduction rules for {\tt\at} become part of the default simpset, which |
|
1863 leads to short proof scripts: |
|
1864 \begin{ttbox}\underscoreon |
|
1865 Goal "xs: list(A) ==> (xs @ ys) @ zs = xs @ (ys @ zs)"; |
|
1866 by (induct\_tac "xs" 1); |
|
1867 by (ALLGOALS Asm\_simp\_tac); |
|
1868 \end{ttbox} |
|
1869 |
|
1870 You can even use the \texttt{primrec} form with non-recursive datatypes and |
|
1871 with codatatypes. Recursion is not allowed, but it provides a convenient |
|
1872 syntax for defining functions by cases. |
|
1873 |
|
1874 |
|
1875 \subsubsection{Example: varying arguments} |
|
1876 |
|
1877 All arguments, other than the recursive one, must be the same in each equation |
|
1878 and in each recursive call. To get around this restriction, use explict |
|
1879 $\lambda$-abstraction and function application. Here is an example, drawn |
|
1880 from the theory \texttt{Resid/Substitution}. The type of redexes is declared |
|
1881 as follows: |
|
1882 \begin{ttbox} |
|
1883 consts redexes :: i |
|
1884 datatype |
|
1885 "redexes" = Var ("n: nat") |
|
1886 | Fun ("t: redexes") |
|
1887 | App ("b:bool" ,"f:redexes" , "a:redexes") |
|
1888 \end{ttbox} |
|
1889 |
|
1890 The function \texttt{lift} takes a second argument, $k$, which varies in |
|
1891 recursive calls. |
|
1892 \begin{ttbox} |
|
1893 primrec |
|
1894 "lift(Var(i)) = (lam k:nat. if i<k then Var(i) else Var(succ(i)))" |
|
1895 "lift(Fun(t)) = (lam k:nat. Fun(lift(t) ` succ(k)))" |
|
1896 "lift(App(b,f,a)) = (lam k:nat. App(b, lift(f)`k, lift(a)`k))" |
|
1897 \end{ttbox} |
|
1898 Now \texttt{lift(r)`k} satisfies the required recursion equations. |
|
1899 |
|
1900 \index{recursion!primitive|)} |
|
1901 \index{*primrec|)} |
|
1902 |
|
1903 |
|
1904 \section{Inductive and coinductive definitions} |
|
1905 \index{*inductive|(} |
|
1906 \index{*coinductive|(} |
|
1907 |
|
1908 An {\bf inductive definition} specifies the least set~$R$ closed under given |
|
1909 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For |
|
1910 example, a structural operational semantics is an inductive definition of an |
|
1911 evaluation relation. Dually, a {\bf coinductive definition} specifies the |
|
1912 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be |
|
1913 seen as arising by applying a rule to elements of~$R$.) An important example |
|
1914 is using bisimulation relations to formalise equivalence of processes and |
|
1915 infinite data structures. |
|
1916 |
|
1917 A theory file may contain any number of inductive and coinductive |
|
1918 definitions. They may be intermixed with other declarations; in |
|
1919 particular, the (co)inductive sets {\bf must} be declared separately as |
|
1920 constants, and may have mixfix syntax or be subject to syntax translations. |
|
1921 |
|
1922 Each (co)inductive definition adds definitions to the theory and also |
|
1923 proves some theorems. Each definition creates an \ML\ structure, which is a |
|
1924 substructure of the main theory structure. |
|
1925 This package is described in detail in a separate paper,% |
|
1926 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is |
|
1927 distributed with Isabelle as \emph{A Fixedpoint Approach to |
|
1928 (Co)Inductive and (Co)Datatype Definitions}.} % |
|
1929 which you might refer to for background information. |
|
1930 |
|
1931 |
|
1932 \subsection{The syntax of a (co)inductive definition} |
|
1933 An inductive definition has the form |
|
1934 \begin{ttbox} |
|
1935 inductive |
|
1936 domains {\it domain declarations} |
|
1937 intrs {\it introduction rules} |
|
1938 monos {\it monotonicity theorems} |
|
1939 con_defs {\it constructor definitions} |
|
1940 type_intrs {\it introduction rules for type-checking} |
|
1941 type_elims {\it elimination rules for type-checking} |
|
1942 \end{ttbox} |
|
1943 A coinductive definition is identical, but starts with the keyword |
|
1944 {\tt coinductive}. |
|
1945 |
|
1946 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims} |
|
1947 sections are optional. If present, each is specified either as a list of |
|
1948 identifiers or as a string. If the latter, then the string must be a valid |
|
1949 \textsc{ml} expression of type {\tt thm list}. The string is simply inserted |
|
1950 into the {\tt _thy.ML} file; if it is ill-formed, it will trigger \textsc{ml} |
|
1951 error messages. You can then inspect the file on the temporary directory. |
|
1952 |
|
1953 \begin{description} |
|
1954 \item[\it domain declarations] consist of one or more items of the form |
|
1955 {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with |
|
1956 its domain. (The domain is some existing set that is large enough to |
|
1957 hold the new set being defined.) |
|
1958 |
|
1959 \item[\it introduction rules] specify one or more introduction rules in |
|
1960 the form {\it ident\/}~{\it string}, where the identifier gives the name of |
|
1961 the rule in the result structure. |
|
1962 |
|
1963 \item[\it monotonicity theorems] are required for each operator applied to |
|
1964 a recursive set in the introduction rules. There \textbf{must} be a theorem |
|
1965 of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each premise $t\in M(R_i)$ |
|
1966 in an introduction rule! |
|
1967 |
|
1968 \item[\it constructor definitions] contain definitions of constants |
|
1969 appearing in the introduction rules. The (co)datatype package supplies |
|
1970 the constructors' definitions here. Most (co)inductive definitions omit |
|
1971 this section; one exception is the primitive recursive functions example; |
|
1972 see theory \texttt{ex/Primrec}. |
|
1973 |
|
1974 \item[\it type\_intrs] consists of introduction rules for type-checking the |
|
1975 definition: for demonstrating that the new set is included in its domain. |
|
1976 (The proof uses depth-first search.) |
|
1977 |
|
1978 \item[\it type\_elims] consists of elimination rules for type-checking the |
|
1979 definition. They are presumed to be safe and are applied as often as |
|
1980 possible prior to the {\tt type\_intrs} search. |
|
1981 \end{description} |
|
1982 |
|
1983 The package has a few restrictions: |
|
1984 \begin{itemize} |
|
1985 \item The theory must separately declare the recursive sets as |
|
1986 constants. |
|
1987 |
|
1988 \item The names of the recursive sets must be identifiers, not infix |
|
1989 operators. |
|
1990 |
|
1991 \item Side-conditions must not be conjunctions. However, an introduction rule |
|
1992 may contain any number of side-conditions. |
|
1993 |
|
1994 \item Side-conditions of the form $x=t$, where the variable~$x$ does not |
|
1995 occur in~$t$, will be substituted through the rule \verb|mutual_induct|. |
|
1996 \end{itemize} |
|
1997 |
|
1998 |
|
1999 \subsection{Example of an inductive definition} |
|
2000 |
|
2001 Two declarations, included in a theory file, define the finite powerset |
|
2002 operator. First we declare the constant~\texttt{Fin}. Then we declare it |
|
2003 inductively, with two introduction rules: |
|
2004 \begin{ttbox} |
|
2005 consts Fin :: i=>i |
|
2006 |
|
2007 inductive |
|
2008 domains "Fin(A)" <= "Pow(A)" |
|
2009 intrs |
|
2010 emptyI "0 : Fin(A)" |
|
2011 consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" |
|
2012 type_intrs empty_subsetI, cons_subsetI, PowI |
|
2013 type_elims "[make_elim PowD]" |
|
2014 \end{ttbox} |
|
2015 The resulting theory structure contains a substructure, called~\texttt{Fin}. |
|
2016 It contains the \texttt{Fin}$~A$ introduction rules as the list |
|
2017 \texttt{Fin.intrs}, and also individually as \texttt{Fin.emptyI} and |
|
2018 \texttt{Fin.consI}. The induction rule is \texttt{Fin.induct}. |
|
2019 |
|
2020 The chief problem with making (co)inductive definitions involves type-checking |
|
2021 the rules. Sometimes, additional theorems need to be supplied under |
|
2022 \texttt{type_intrs} or \texttt{type_elims}. If the package fails when trying |
|
2023 to prove your introduction rules, then set the flag \ttindexbold{trace_induct} |
|
2024 to \texttt{true} and try again. (See the manual \emph{A Fixedpoint Approach |
|
2025 \ldots} for more discussion of type-checking.) |
|
2026 |
|
2027 In the example above, $\texttt{Pow}(A)$ is given as the domain of |
|
2028 $\texttt{Fin}(A)$, for obviously every finite subset of~$A$ is a subset |
|
2029 of~$A$. However, the inductive definition package can only prove that given a |
|
2030 few hints. |
|
2031 Here is the output that results (with the flag set) when the |
|
2032 \texttt{type_intrs} and \texttt{type_elims} are omitted from the inductive |
|
2033 definition above: |
|
2034 \begin{ttbox} |
|
2035 Inductive definition Finite.Fin |
|
2036 Fin(A) == |
|
2037 lfp(Pow(A), |
|
2038 \%X. {z: Pow(A) . z = 0 | (EX a b. z = cons(a, b) & a : A & b : X)}) |
|
2039 Proving monotonicity... |
|
2040 \ttbreak |
|
2041 Proving the introduction rules... |
|
2042 The typechecking subgoal: |
|
2043 0 : Fin(A) |
|
2044 1. 0 : Pow(A) |
|
2045 \ttbreak |
|
2046 The subgoal after monos, type_elims: |
|
2047 0 : Fin(A) |
|
2048 1. 0 : Pow(A) |
|
2049 *** prove_goal: tactic failed |
|
2050 \end{ttbox} |
|
2051 We see the need to supply theorems to let the package prove |
|
2052 $\emptyset\in\texttt{Pow}(A)$. Restoring the \texttt{type_intrs} but not the |
|
2053 \texttt{type_elims}, we again get an error message: |
|
2054 \begin{ttbox} |
|
2055 The typechecking subgoal: |
|
2056 0 : Fin(A) |
|
2057 1. 0 : Pow(A) |
|
2058 \ttbreak |
|
2059 The subgoal after monos, type_elims: |
|
2060 0 : Fin(A) |
|
2061 1. 0 : Pow(A) |
|
2062 \ttbreak |
|
2063 The typechecking subgoal: |
|
2064 cons(a, b) : Fin(A) |
|
2065 1. [| a : A; b : Fin(A) |] ==> cons(a, b) : Pow(A) |
|
2066 \ttbreak |
|
2067 The subgoal after monos, type_elims: |
|
2068 cons(a, b) : Fin(A) |
|
2069 1. [| a : A; b : Pow(A) |] ==> cons(a, b) : Pow(A) |
|
2070 *** prove_goal: tactic failed |
|
2071 \end{ttbox} |
|
2072 The first rule has been type-checked, but the second one has failed. The |
|
2073 simplest solution to such problems is to prove the failed subgoal separately |
|
2074 and to supply it under \texttt{type_intrs}. The solution actually used is |
|
2075 to supply, under \texttt{type_elims}, a rule that changes |
|
2076 $b\in\texttt{Pow}(A)$ to $b\subseteq A$; together with \texttt{cons_subsetI} |
|
2077 and \texttt{PowI}, it is enough to complete the type-checking. |
|
2078 |
|
2079 |
|
2080 |
|
2081 \subsection{Further examples} |
|
2082 |
|
2083 An inductive definition may involve arbitrary monotonic operators. Here is a |
|
2084 standard example: the accessible part of a relation. Note the use |
|
2085 of~\texttt{Pow} in the introduction rule and the corresponding mention of the |
|
2086 rule \verb|Pow_mono| in the \texttt{monos} list. If the desired rule has a |
|
2087 universally quantified premise, usually the effect can be obtained using |
|
2088 \texttt{Pow}. |
|
2089 \begin{ttbox} |
|
2090 consts acc :: i=>i |
|
2091 inductive |
|
2092 domains "acc(r)" <= "field(r)" |
|
2093 intrs |
|
2094 vimage "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)" |
|
2095 monos Pow_mono |
|
2096 \end{ttbox} |
|
2097 |
|
2098 Finally, here is a coinductive definition. It captures (as a bisimulation) |
|
2099 the notion of equality on lazy lists, which are first defined as a codatatype: |
|
2100 \begin{ttbox} |
|
2101 consts llist :: i=>i |
|
2102 codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)") |
|
2103 \ttbreak |
|
2104 |
|
2105 consts lleq :: i=>i |
|
2106 coinductive |
|
2107 domains "lleq(A)" <= "llist(A) * llist(A)" |
|
2108 intrs |
|
2109 LNil "<LNil, LNil> : lleq(A)" |
|
2110 LCons "[| a:A; <l,l'>: lleq(A) |] |
|
2111 ==> <LCons(a,l), LCons(a,l')>: lleq(A)" |
|
2112 type_intrs "llist.intrs" |
|
2113 \end{ttbox} |
|
2114 This use of \texttt{type_intrs} is typical: the relation concerns the |
|
2115 codatatype \texttt{llist}, so naturally the introduction rules for that |
|
2116 codatatype will be required for type-checking the rules. |
|
2117 |
|
2118 The Isabelle distribution contains many other inductive definitions. Simple |
|
2119 examples are collected on subdirectory \texttt{ZF/ex}. The directory |
|
2120 \texttt{Coind} and the theory \texttt{ZF/ex/LList} contain coinductive |
|
2121 definitions. Larger examples may be found on other subdirectories of |
|
2122 \texttt{ZF}, such as \texttt{IMP}, and \texttt{Resid}. |
|
2123 |
|
2124 |
|
2125 \subsection{The result structure} |
|
2126 |
|
2127 Each (co)inductive set defined in a theory file generates an \ML\ substructure |
|
2128 having the same name. The the substructure contains the following elements: |
|
2129 |
|
2130 \begin{ttbox} |
|
2131 val intrs : thm list \textrm{the introduction rules} |
|
2132 val elim : thm \textrm{the elimination (case analysis) rule} |
|
2133 val mk_cases : thm list -> string -> thm \textrm{case analysis, see below} |
|
2134 val induct : thm \textrm{the standard induction rule} |
|
2135 val mutual_induct : thm \textrm{the mutual induction rule, or \texttt{True}} |
|
2136 val defs : thm list \textrm{definitions of operators} |
|
2137 val bnd_mono : thm list \textrm{monotonicity property} |
|
2138 val dom_subset : thm list \textrm{inclusion in `bounding set'} |
|
2139 \end{ttbox} |
|
2140 Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for |
|
2141 example, the \texttt{list} datatype's introduction rules are bound to the |
|
2142 identifiers \texttt{Nil_I} and \texttt{Cons_I}. |
|
2143 |
|
2144 For a codatatype, the component \texttt{coinduct} is the coinduction rule, |
|
2145 replacing the \texttt{induct} component. |
|
2146 |
|
2147 Recall that \ttindex{mk_cases} generates simplified instances of the |
|
2148 elimination (case analysis) rule. It is as useful for inductive definitions |
|
2149 as it is for datatypes. There are many examples in the theory |
|
2150 \texttt{ex/Comb}, which is discussed at length |
|
2151 elsewhere~\cite{paulson-generic}. The theory first defines the datatype |
|
2152 \texttt{comb} of combinators: |
|
2153 \begin{ttbox} |
|
2154 consts comb :: i |
|
2155 datatype "comb" = K |
|
2156 | S |
|
2157 | "#" ("p: comb", "q: comb") (infixl 90) |
|
2158 \end{ttbox} |
|
2159 The theory goes on to define contraction and parallel contraction |
|
2160 inductively. Then the file \texttt{ex/Comb.ML} defines special cases of |
|
2161 contraction using \texttt{mk_cases}: |
|
2162 \begin{ttbox} |
|
2163 val K_contractE = contract.mk_cases comb.con_defs "K -1-> r"; |
|
2164 {\out val K_contractE = "K -1-> ?r ==> ?Q" : thm} |
|
2165 \end{ttbox} |
|
2166 We can read this as saying that the combinator \texttt{K} cannot reduce to |
|
2167 anything. Similar elimination rules for \texttt{S} and application are also |
|
2168 generated and are supplied to the classical reasoner. Note that |
|
2169 \texttt{comb.con_defs} is given to \texttt{mk_cases} to allow freeness |
|
2170 reasoning on datatype \texttt{comb}. |
|
2171 |
|
2172 \index{*coinductive|)} \index{*inductive|)} |
|
2173 |
|
2174 |
|
2175 |
|
2176 |
|
2177 \section{The outer reaches of set theory} |
|
2178 |
|
2179 The constructions of the natural numbers and lists use a suite of |
|
2180 operators for handling recursive function definitions. I have described |
|
2181 the developments in detail elsewhere~\cite{paulson-set-II}. Here is a brief |
|
2182 summary: |
|
2183 \begin{itemize} |
|
2184 \item Theory \texttt{Trancl} defines the transitive closure of a relation |
|
2185 (as a least fixedpoint). |
|
2186 |
|
2187 \item Theory \texttt{WF} proves the Well-Founded Recursion Theorem, using an |
|
2188 elegant approach of Tobias Nipkow. This theorem permits general |
|
2189 recursive definitions within set theory. |
|
2190 |
|
2191 \item Theory \texttt{Ord} defines the notions of transitive set and ordinal |
|
2192 number. It derives transfinite induction. A key definition is {\bf |
|
2193 less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and |
|
2194 $i\in j$. As a special case, it includes less than on the natural |
|
2195 numbers. |
|
2196 |
|
2197 \item Theory \texttt{Epsilon} derives $\varepsilon$-induction and |
|
2198 $\varepsilon$-recursion, which are generalisations of transfinite |
|
2199 induction and recursion. It also defines \cdx{rank}$(x)$, which |
|
2200 is the least ordinal $\alpha$ such that $x$ is constructed at |
|
2201 stage $\alpha$ of the cumulative hierarchy (thus $x\in |
|
2202 V@{\alpha+1}$). |
|
2203 \end{itemize} |
|
2204 |
|
2205 Other important theories lead to a theory of cardinal numbers. They have |
|
2206 not yet been written up anywhere. Here is a summary: |
|
2207 \begin{itemize} |
|
2208 \item Theory \texttt{Rel} defines the basic properties of relations, such as |
|
2209 (ir)reflexivity, (a)symmetry, and transitivity. |
|
2210 |
|
2211 \item Theory \texttt{EquivClass} develops a theory of equivalence |
|
2212 classes, not using the Axiom of Choice. |
|
2213 |
|
2214 \item Theory \texttt{Order} defines partial orderings, total orderings and |
|
2215 wellorderings. |
|
2216 |
|
2217 \item Theory \texttt{OrderArith} defines orderings on sum and product sets. |
|
2218 These can be used to define ordinal arithmetic and have applications to |
|
2219 cardinal arithmetic. |
|
2220 |
|
2221 \item Theory \texttt{OrderType} defines order types. Every wellordering is |
|
2222 equivalent to a unique ordinal, which is its order type. |
|
2223 |
|
2224 \item Theory \texttt{Cardinal} defines equipollence and cardinal numbers. |
|
2225 |
|
2226 \item Theory \texttt{CardinalArith} defines cardinal addition and |
|
2227 multiplication, and proves their elementary laws. It proves that there |
|
2228 is no greatest cardinal. It also proves a deep result, namely |
|
2229 $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see |
|
2230 Kunen~\cite[page 29]{kunen80}. None of these results assume the Axiom of |
|
2231 Choice, which complicates their proofs considerably. |
|
2232 \end{itemize} |
|
2233 |
|
2234 The following developments involve the Axiom of Choice (AC): |
|
2235 \begin{itemize} |
|
2236 \item Theory \texttt{AC} asserts the Axiom of Choice and proves some simple |
|
2237 equivalent forms. |
|
2238 |
|
2239 \item Theory \texttt{Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma |
|
2240 and the Wellordering Theorem, following Abrial and |
|
2241 Laffitte~\cite{abrial93}. |
|
2242 |
|
2243 \item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about |
|
2244 the cardinals. It also proves a theorem needed to justify |
|
2245 infinitely branching datatype declarations: if $\kappa$ is an infinite |
|
2246 cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then |
|
2247 $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$. |
|
2248 |
|
2249 \item Theory \texttt{InfDatatype} proves theorems to justify infinitely |
|
2250 branching datatypes. Arbitrary index sets are allowed, provided their |
|
2251 cardinalities have an upper bound. The theory also justifies some |
|
2252 unusual cases of finite branching, involving the finite powerset operator |
|
2253 and the finite function space operator. |
|
2254 \end{itemize} |
|
2255 |
|
2256 |
|
2257 |
|
2258 \section{The examples directories} |
|
2259 Directory \texttt{HOL/IMP} contains a mechanised version of a semantic |
|
2260 equivalence proof taken from Winskel~\cite{winskel93}. It formalises the |
|
2261 denotational and operational semantics of a simple while-language, then |
|
2262 proves the two equivalent. It contains several datatype and inductive |
|
2263 definitions, and demonstrates their use. |
|
2264 |
|
2265 The directory \texttt{ZF/ex} contains further developments in {\ZF} set |
|
2266 theory. Here is an overview; see the files themselves for more details. I |
|
2267 describe much of this material in other |
|
2268 publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. |
|
2269 \begin{itemize} |
|
2270 \item File \texttt{misc.ML} contains miscellaneous examples such as |
|
2271 Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition |
|
2272 of homomorphisms' challenge~\cite{boyer86}. |
|
2273 |
|
2274 \item Theory \texttt{Ramsey} proves the finite exponent 2 version of |
|
2275 Ramsey's Theorem, following Basin and Kaufmann's |
|
2276 presentation~\cite{basin91}. |
|
2277 |
|
2278 \item Theory \texttt{Integ} develops a theory of the integers as |
|
2279 equivalence classes of pairs of natural numbers. |
|
2280 |
|
2281 \item Theory \texttt{Primrec} develops some computation theory. It |
|
2282 inductively defines the set of primitive recursive functions and presents a |
|
2283 proof that Ackermann's function is not primitive recursive. |
|
2284 |
|
2285 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two |
|
2286 natural numbers and and the ``divides'' relation. |
|
2287 |
|
2288 \item Theory \texttt{Bin} defines a datatype for two's complement binary |
|
2289 integers, then proves rewrite rules to perform binary arithmetic. For |
|
2290 instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds. |
|
2291 |
|
2292 \item Theory \texttt{BT} defines the recursive data structure ${\tt |
|
2293 bt}(A)$, labelled binary trees. |
|
2294 |
|
2295 \item Theory \texttt{Term} defines a recursive data structure for terms |
|
2296 and term lists. These are simply finite branching trees. |
|
2297 |
|
2298 \item Theory \texttt{TF} defines primitives for solving mutually |
|
2299 recursive equations over sets. It constructs sets of trees and forests |
|
2300 as an example, including induction and recursion rules that handle the |
|
2301 mutual recursion. |
|
2302 |
|
2303 \item Theory \texttt{Prop} proves soundness and completeness of |
|
2304 propositional logic~\cite{paulson-set-II}. This illustrates datatype |
|
2305 definitions, inductive definitions, structural induction and rule |
|
2306 induction. |
|
2307 |
|
2308 \item Theory \texttt{ListN} inductively defines the lists of $n$ |
|
2309 elements~\cite{paulin92}. |
|
2310 |
|
2311 \item Theory \texttt{Acc} inductively defines the accessible part of a |
|
2312 relation~\cite{paulin92}. |
|
2313 |
|
2314 \item Theory \texttt{Comb} defines the datatype of combinators and |
|
2315 inductively defines contraction and parallel contraction. It goes on to |
|
2316 prove the Church-Rosser Theorem. This case study follows Camilleri and |
|
2317 Melham~\cite{camilleri92}. |
|
2318 |
|
2319 \item Theory \texttt{LList} defines lazy lists and a coinduction |
|
2320 principle for proving equations between them. |
|
2321 \end{itemize} |
|
2322 |
|
2323 |
|
2324 \section{A proof about powersets}\label{sec:ZF-pow-example} |
|
2325 To demonstrate high-level reasoning about subsets, let us prove the |
|
2326 equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$. Compared |
|
2327 with first-order logic, set theory involves a maze of rules, and theorems |
|
2328 have many different proofs. Attempting other proofs of the theorem might |
|
2329 be instructive. This proof exploits the lattice properties of |
|
2330 intersection. It also uses the monotonicity of the powerset operation, |
|
2331 from \texttt{ZF/mono.ML}: |
|
2332 \begin{ttbox} |
|
2333 \tdx{Pow_mono} A<=B ==> Pow(A) <= Pow(B) |
|
2334 \end{ttbox} |
|
2335 We enter the goal and make the first step, which breaks the equation into |
|
2336 two inclusions by extensionality:\index{*equalityI theorem} |
|
2337 \begin{ttbox} |
|
2338 Goal "Pow(A Int B) = Pow(A) Int Pow(B)"; |
|
2339 {\out Level 0} |
|
2340 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2341 {\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2342 \ttbreak |
|
2343 by (resolve_tac [equalityI] 1); |
|
2344 {\out Level 1} |
|
2345 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2346 {\out 1. Pow(A Int B) <= Pow(A) Int Pow(B)} |
|
2347 {\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
2348 \end{ttbox} |
|
2349 Both inclusions could be tackled straightforwardly using \texttt{subsetI}. |
|
2350 A shorter proof results from noting that intersection forms the greatest |
|
2351 lower bound:\index{*Int_greatest theorem} |
|
2352 \begin{ttbox} |
|
2353 by (resolve_tac [Int_greatest] 1); |
|
2354 {\out Level 2} |
|
2355 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2356 {\out 1. Pow(A Int B) <= Pow(A)} |
|
2357 {\out 2. Pow(A Int B) <= Pow(B)} |
|
2358 {\out 3. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
2359 \end{ttbox} |
|
2360 Subgoal~1 follows by applying the monotonicity of \texttt{Pow} to $A\int |
|
2361 B\subseteq A$; subgoal~2 follows similarly: |
|
2362 \index{*Int_lower1 theorem}\index{*Int_lower2 theorem} |
|
2363 \begin{ttbox} |
|
2364 by (resolve_tac [Int_lower1 RS Pow_mono] 1); |
|
2365 {\out Level 3} |
|
2366 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2367 {\out 1. Pow(A Int B) <= Pow(B)} |
|
2368 {\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
2369 \ttbreak |
|
2370 by (resolve_tac [Int_lower2 RS Pow_mono] 1); |
|
2371 {\out Level 4} |
|
2372 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2373 {\out 1. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
2374 \end{ttbox} |
|
2375 We are left with the opposite inclusion, which we tackle in the |
|
2376 straightforward way:\index{*subsetI theorem} |
|
2377 \begin{ttbox} |
|
2378 by (resolve_tac [subsetI] 1); |
|
2379 {\out Level 5} |
|
2380 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2381 {\out 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)} |
|
2382 \end{ttbox} |
|
2383 The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt |
|
2384 Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two |
|
2385 subgoals. The rule \tdx{IntE} treats the intersection like a conjunction |
|
2386 instead of unfolding its definition. |
|
2387 \begin{ttbox} |
|
2388 by (eresolve_tac [IntE] 1); |
|
2389 {\out Level 6} |
|
2390 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2391 {\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)} |
|
2392 \end{ttbox} |
|
2393 The next step replaces the \texttt{Pow} by the subset |
|
2394 relation~($\subseteq$).\index{*PowI theorem} |
|
2395 \begin{ttbox} |
|
2396 by (resolve_tac [PowI] 1); |
|
2397 {\out Level 7} |
|
2398 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2399 {\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B} |
|
2400 \end{ttbox} |
|
2401 We perform the same replacement in the assumptions. This is a good |
|
2402 demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem} |
|
2403 \begin{ttbox} |
|
2404 by (REPEAT (dresolve_tac [PowD] 1)); |
|
2405 {\out Level 8} |
|
2406 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2407 {\out 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B} |
|
2408 \end{ttbox} |
|
2409 The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but |
|
2410 $A\int B$ is the greatest lower bound:\index{*Int_greatest theorem} |
|
2411 \begin{ttbox} |
|
2412 by (resolve_tac [Int_greatest] 1); |
|
2413 {\out Level 9} |
|
2414 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2415 {\out 1. !!x. [| x <= A; x <= B |] ==> x <= A} |
|
2416 {\out 2. !!x. [| x <= A; x <= B |] ==> x <= B} |
|
2417 \end{ttbox} |
|
2418 To conclude the proof, we clear up the trivial subgoals: |
|
2419 \begin{ttbox} |
|
2420 by (REPEAT (assume_tac 1)); |
|
2421 {\out Level 10} |
|
2422 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2423 {\out No subgoals!} |
|
2424 \end{ttbox} |
|
2425 \medskip |
|
2426 We could have performed this proof in one step by applying |
|
2427 \ttindex{Blast_tac}. Let us |
|
2428 go back to the start: |
|
2429 \begin{ttbox} |
|
2430 choplev 0; |
|
2431 {\out Level 0} |
|
2432 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2433 {\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2434 by (Blast_tac 1); |
|
2435 {\out Depth = 0} |
|
2436 {\out Depth = 1} |
|
2437 {\out Depth = 2} |
|
2438 {\out Depth = 3} |
|
2439 {\out Level 1} |
|
2440 {\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
2441 {\out No subgoals!} |
|
2442 \end{ttbox} |
|
2443 Past researchers regarded this as a difficult proof, as indeed it is if all |
|
2444 the symbols are replaced by their definitions. |
|
2445 \goodbreak |
|
2446 |
|
2447 \section{Monotonicity of the union operator} |
|
2448 For another example, we prove that general union is monotonic: |
|
2449 ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we |
|
2450 tackle the inclusion using \tdx{subsetI}: |
|
2451 \begin{ttbox} |
|
2452 Goal "C<=D ==> Union(C) <= Union(D)"; |
|
2453 {\out Level 0} |
|
2454 {\out C <= D ==> Union(C) <= Union(D)} |
|
2455 {\out 1. C <= D ==> Union(C) <= Union(D)} |
|
2456 \ttbreak |
|
2457 by (resolve_tac [subsetI] 1); |
|
2458 {\out Level 1} |
|
2459 {\out C <= D ==> Union(C) <= Union(D)} |
|
2460 {\out 1. !!x. [| C <= D; x : Union(C) |] ==> x : Union(D)} |
|
2461 \end{ttbox} |
|
2462 Big union is like an existential quantifier --- the occurrence in the |
|
2463 assumptions must be eliminated early, since it creates parameters. |
|
2464 \index{*UnionE theorem} |
|
2465 \begin{ttbox} |
|
2466 by (eresolve_tac [UnionE] 1); |
|
2467 {\out Level 2} |
|
2468 {\out C <= D ==> Union(C) <= Union(D)} |
|
2469 {\out 1. !!x B. [| C <= D; x : B; B : C |] ==> x : Union(D)} |
|
2470 \end{ttbox} |
|
2471 Now we may apply \tdx{UnionI}, which creates an unknown involving the |
|
2472 parameters. To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs |
|
2473 to some element, say~$\Var{B2}(x,B)$, of~$D$. |
|
2474 \begin{ttbox} |
|
2475 by (resolve_tac [UnionI] 1); |
|
2476 {\out Level 3} |
|
2477 {\out C <= D ==> Union(C) <= Union(D)} |
|
2478 {\out 1. !!x B. [| C <= D; x : B; B : C |] ==> ?B2(x,B) : D} |
|
2479 {\out 2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)} |
|
2480 \end{ttbox} |
|
2481 Combining \tdx{subsetD} with the assumption $C\subseteq D$ yields |
|
2482 $\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1. Note that |
|
2483 \texttt{eresolve_tac} has removed that assumption. |
|
2484 \begin{ttbox} |
|
2485 by (eresolve_tac [subsetD] 1); |
|
2486 {\out Level 4} |
|
2487 {\out C <= D ==> Union(C) <= Union(D)} |
|
2488 {\out 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C} |
|
2489 {\out 2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)} |
|
2490 \end{ttbox} |
|
2491 The rest is routine. Observe how~$\Var{B2}(x,B)$ is instantiated. |
|
2492 \begin{ttbox} |
|
2493 by (assume_tac 1); |
|
2494 {\out Level 5} |
|
2495 {\out C <= D ==> Union(C) <= Union(D)} |
|
2496 {\out 1. !!x B. [| C <= D; x : B; B : C |] ==> x : B} |
|
2497 by (assume_tac 1); |
|
2498 {\out Level 6} |
|
2499 {\out C <= D ==> Union(C) <= Union(D)} |
|
2500 {\out No subgoals!} |
|
2501 \end{ttbox} |
|
2502 Again, \ttindex{Blast_tac} can prove the theorem in one step. |
|
2503 \begin{ttbox} |
|
2504 by (Blast_tac 1); |
|
2505 {\out Depth = 0} |
|
2506 {\out Depth = 1} |
|
2507 {\out Depth = 2} |
|
2508 {\out Level 1} |
|
2509 {\out C <= D ==> Union(C) <= Union(D)} |
|
2510 {\out No subgoals!} |
|
2511 \end{ttbox} |
|
2512 |
|
2513 The file \texttt{ZF/equalities.ML} has many similar proofs. Reasoning about |
|
2514 general intersection can be difficult because of its anomalous behaviour on |
|
2515 the empty set. However, \ttindex{Blast_tac} copes well with these. Here is |
|
2516 a typical example, borrowed from Devlin~\cite[page 12]{devlin79}: |
|
2517 \begin{ttbox} |
|
2518 a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C. A(x)) Int (INT x:C. B(x)) |
|
2519 \end{ttbox} |
|
2520 In traditional notation this is |
|
2521 \[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) = |
|
2522 \Bigl(\inter@{x\in C} A(x)\Bigr) \int |
|
2523 \Bigl(\inter@{x\in C} B(x)\Bigr) \] |
|
2524 |
|
2525 \section{Low-level reasoning about functions} |
|
2526 The derived rules \texttt{lamI}, \texttt{lamE}, \texttt{lam_type}, \texttt{beta} |
|
2527 and \texttt{eta} support reasoning about functions in a |
|
2528 $\lambda$-calculus style. This is generally easier than regarding |
|
2529 functions as sets of ordered pairs. But sometimes we must look at the |
|
2530 underlying representation, as in the following proof |
|
2531 of~\tdx{fun_disjoint_apply1}. This states that if $f$ and~$g$ are |
|
2532 functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then |
|
2533 $(f\un g)`a = f`a$: |
|
2534 \begin{ttbox} |
|
2535 Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback |
|
2536 \ttback (f Un g)`a = f`a"; |
|
2537 {\out Level 0} |
|
2538 {\out [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]} |
|
2539 {\out ==> (f Un g) ` a = f ` a} |
|
2540 {\out 1. [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]} |
|
2541 {\out ==> (f Un g) ` a = f ` a} |
|
2542 \end{ttbox} |
|
2543 Using \tdx{apply_equality}, we reduce the equality to reasoning about |
|
2544 ordered pairs. The second subgoal is to verify that $f\un g$ is a function. |
|
2545 To save space, the assumptions will be abbreviated below. |
|
2546 \begin{ttbox} |
|
2547 by (resolve_tac [apply_equality] 1); |
|
2548 {\out Level 1} |
|
2549 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2550 {\out 1. [| \ldots |] ==> <a,f ` a> : f Un g} |
|
2551 {\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} |
|
2552 \end{ttbox} |
|
2553 We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we |
|
2554 choose~$f$: |
|
2555 \begin{ttbox} |
|
2556 by (resolve_tac [UnI1] 1); |
|
2557 {\out Level 2} |
|
2558 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2559 {\out 1. [| \ldots |] ==> <a,f ` a> : f} |
|
2560 {\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} |
|
2561 \end{ttbox} |
|
2562 To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is |
|
2563 essentially the converse of \tdx{apply_equality}: |
|
2564 \begin{ttbox} |
|
2565 by (resolve_tac [apply_Pair] 1); |
|
2566 {\out Level 3} |
|
2567 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2568 {\out 1. [| \ldots |] ==> f : (PROD x:?A2. ?B2(x))} |
|
2569 {\out 2. [| \ldots |] ==> a : ?A2} |
|
2570 {\out 3. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} |
|
2571 \end{ttbox} |
|
2572 Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals |
|
2573 from \tdx{apply_Pair}. Recall that a $\Pi$-set is merely a generalized |
|
2574 function space, and observe that~{\tt?A2} is instantiated to~\texttt{A}. |
|
2575 \begin{ttbox} |
|
2576 by (assume_tac 1); |
|
2577 {\out Level 4} |
|
2578 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2579 {\out 1. [| \ldots |] ==> a : A} |
|
2580 {\out 2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} |
|
2581 by (assume_tac 1); |
|
2582 {\out Level 5} |
|
2583 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2584 {\out 1. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))} |
|
2585 \end{ttbox} |
|
2586 To construct functions of the form $f\un g$, we apply |
|
2587 \tdx{fun_disjoint_Un}: |
|
2588 \begin{ttbox} |
|
2589 by (resolve_tac [fun_disjoint_Un] 1); |
|
2590 {\out Level 6} |
|
2591 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2592 {\out 1. [| \ldots |] ==> f : ?A3 -> ?B3} |
|
2593 {\out 2. [| \ldots |] ==> g : ?C3 -> ?D3} |
|
2594 {\out 3. [| \ldots |] ==> ?A3 Int ?C3 = 0} |
|
2595 \end{ttbox} |
|
2596 The remaining subgoals are instances of the assumptions. Again, observe how |
|
2597 unknowns are instantiated: |
|
2598 \begin{ttbox} |
|
2599 by (assume_tac 1); |
|
2600 {\out Level 7} |
|
2601 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2602 {\out 1. [| \ldots |] ==> g : ?C3 -> ?D3} |
|
2603 {\out 2. [| \ldots |] ==> A Int ?C3 = 0} |
|
2604 by (assume_tac 1); |
|
2605 {\out Level 8} |
|
2606 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2607 {\out 1. [| \ldots |] ==> A Int C = 0} |
|
2608 by (assume_tac 1); |
|
2609 {\out Level 9} |
|
2610 {\out [| \ldots |] ==> (f Un g) ` a = f ` a} |
|
2611 {\out No subgoals!} |
|
2612 \end{ttbox} |
|
2613 See the files \texttt{ZF/func.ML} and \texttt{ZF/WF.ML} for more |
|
2614 examples of reasoning about functions. |
|
2615 |
|
2616 \index{set theory|)} |