28 reasoning about the relations $<$ and $\le$). |
28 reasoning about the relations $<$ and $\le$). |
29 |
29 |
30 {\tt ZF} has a flexible package for handling inductive definitions, |
30 {\tt ZF} has a flexible package for handling inductive definitions, |
31 such as inference systems, and datatype definitions, such as lists and |
31 such as inference systems, and datatype definitions, such as lists and |
32 trees. Moreover it handles coinductive definitions, such as |
32 trees. Moreover it handles coinductive definitions, such as |
33 bisimulation relations, and codatatype definitions, such as streams. A |
33 bisimulation relations, and codatatype definitions, such as streams. |
34 recent paper describes the package~\cite{paulson-CADE}, but its examples |
34 There is a paper \cite{paulson-CADE} describing the package, but its |
35 use an obsolete declaration syntax. Please consult the version of the |
35 examples use an obsolete declaration syntax. Please consult the |
36 paper distributed with Isabelle. |
36 version of the paper distributed with Isabelle. |
37 |
37 |
38 Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less |
38 Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less |
39 formally than this chapter. Isabelle employs a novel treatment of |
39 formally than this chapter. Isabelle employs a novel treatment of |
40 non-well-founded data structures within the standard {\sc zf} axioms including |
40 non-well-founded data structures within the standard {\sc zf} axioms including |
41 the Axiom of Foundation~\cite{paulson-final}. |
41 the Axiom of Foundation~\cite{paulson-final}. |
187 \index{*"* symbol} |
187 \index{*"* symbol} |
188 \begin{center} \footnotesize\tt\frenchspacing |
188 \begin{center} \footnotesize\tt\frenchspacing |
189 \begin{tabular}{rrr} |
189 \begin{tabular}{rrr} |
190 \it external & \it internal & \it description \\ |
190 \it external & \it internal & \it description \\ |
191 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ |
191 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ |
192 \{$a@1$, $\ldots$, $a@n$\} & cons($a@1$,$\cdots$,cons($a@n$,0)) & |
192 \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace & cons($a@1$,$\cdots$,cons($a@n$,0)) & |
193 \rm finite set \\ |
193 \rm finite set \\ |
194 <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & |
194 <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & |
195 Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & |
195 Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & |
196 \rm ordered $n$-tuple \\ |
196 \rm ordered $n$-tuple \\ |
197 \{$x$:$A . P[x]$\} & Collect($A$,$\lambda x.P[x]$) & |
197 \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x.P[x]$) & |
198 \rm separation \\ |
198 \rm separation \\ |
199 \{$y . x$:$A$, $Q[x,y]$\} & Replace($A$,$\lambda x\,y.Q[x,y]$) & |
199 \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y.Q[x,y]$) & |
200 \rm replacement \\ |
200 \rm replacement \\ |
201 \{$b[x] . x$:$A$\} & RepFun($A$,$\lambda x.b[x]$) & |
201 \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x.b[x]$) & |
202 \rm functional replacement \\ |
202 \rm functional replacement \\ |
203 \sdx{INT} $x$:$A . B[x]$ & Inter(\{$B[x] . x$:$A$\}) & |
203 \sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) & |
204 \rm general intersection \\ |
204 \rm general intersection \\ |
205 \sdx{UN} $x$:$A . B[x]$ & Union(\{$B[x] . x$:$A$\}) & |
205 \sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) & |
206 \rm general union \\ |
206 \rm general union \\ |
207 \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & |
207 \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & |
208 \rm general product \\ |
208 \rm general product \\ |
209 \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & |
209 \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & |
210 \rm general sum \\ |
210 \rm general sum \\ |
231 \index{*in symbol} |
231 \index{*in symbol} |
232 \dquotes |
232 \dquotes |
233 \[\begin{array}{rcl} |
233 \[\begin{array}{rcl} |
234 term & = & \hbox{expression of type~$i$} \\ |
234 term & = & \hbox{expression of type~$i$} \\ |
235 & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ |
235 & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ |
236 & | & "\{ " term\; ("," term)^* " \}" \\ |
236 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ |
237 & | & "< " term\; ("," term)^* " >" \\ |
237 & | & "< " term\; ("," term)^* " >" \\ |
238 & | & "\{ " id ":" term " . " formula " \}" \\ |
238 & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\ |
239 & | & "\{ " id " . " id ":" term ", " formula " \}" \\ |
239 & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\ |
240 & | & "\{ " term " . " id ":" term " \}" \\ |
240 & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\ |
241 & | & term " `` " term \\ |
241 & | & term " `` " term \\ |
242 & | & term " -`` " term \\ |
242 & | & term " -`` " term \\ |
243 & | & term " ` " term \\ |
243 & | & term " ` " term \\ |
244 & | & term " * " term \\ |
244 & | & term " * " term \\ |
245 & | & term " Int " term \\ |
245 & | & term " Int " term \\ |
274 \end{figure} |
274 \end{figure} |
275 |
275 |
276 |
276 |
277 \section{Binding operators} |
277 \section{Binding operators} |
278 The constant \cdx{Collect} constructs sets by the principle of {\bf |
278 The constant \cdx{Collect} constructs sets by the principle of {\bf |
279 separation}. The syntax for separation is \hbox{\tt\{$x$:$A$.$P[x]$\}}, |
279 separation}. The syntax for separation is |
280 where $P[x]$ is a formula that may contain free occurrences of~$x$. It |
280 \hbox{\tt\ttlbrace$x$:$A$.$P[x]$\ttrbrace}, where $P[x]$ is a formula |
281 abbreviates the set {\tt Collect($A$,$\lambda x.P[x]$)}, which consists of |
281 that may contain free occurrences of~$x$. It abbreviates the set {\tt |
282 all $x\in A$ that satisfy~$P[x]$. Note that {\tt Collect} is an |
282 Collect($A$,$\lambda x.P[x]$)}, which consists of all $x\in A$ that |
283 unfortunate choice of name: some set theories adopt a set-formation |
283 satisfy~$P[x]$. Note that {\tt Collect} is an unfortunate choice of |
284 principle, related to replacement, called collection. |
284 name: some set theories adopt a set-formation principle, related to |
|
285 replacement, called collection. |
285 |
286 |
286 The constant \cdx{Replace} constructs sets by the principle of {\bf |
287 The constant \cdx{Replace} constructs sets by the principle of {\bf |
287 replacement}. The syntax \hbox{\tt\{$y$.$x$:$A$,$Q[x,y]$\}} denotes the |
288 replacement}. The syntax |
288 set {\tt Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such |
289 \hbox{\tt\ttlbrace$y$.$x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt |
289 that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom has |
290 Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such |
290 the condition that $Q$ must be single-valued over~$A$: for all~$x\in A$ |
291 that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom |
291 there exists at most one $y$ satisfying~$Q[x,y]$. A single-valued binary |
292 has the condition that $Q$ must be single-valued over~$A$: for |
292 predicate is also called a {\bf class function}. |
293 all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A |
|
294 single-valued binary predicate is also called a {\bf class function}. |
293 |
295 |
294 The constant \cdx{RepFun} expresses a special case of replacement, |
296 The constant \cdx{RepFun} expresses a special case of replacement, |
295 where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially |
297 where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially |
296 single-valued, since it is just the graph of the meta-level |
298 single-valued, since it is just the graph of the meta-level |
297 function~$\lambda x.b[x]$. The resulting set consists of all $b[x]$ |
299 function~$\lambda x.b[x]$. The resulting set consists of all $b[x]$ |
298 for~$x\in A$. This is analogous to the \ML{} functional {\tt map}, since |
300 for~$x\in A$. This is analogous to the \ML{} functional {\tt map}, |
299 it applies a function to every element of a set. The syntax is |
301 since it applies a function to every element of a set. The syntax is |
300 \hbox{\tt\{$b[x]$.$x$:$A$\}}, which expands to {\tt RepFun($A$,$\lambda |
302 \hbox{\tt\ttlbrace$b[x]$.$x$:$A$\ttrbrace}, which expands to {\tt |
301 x.b[x]$)}. |
303 RepFun($A$,$\lambda x.b[x]$)}. |
302 |
304 |
303 \index{*INT symbol}\index{*UN symbol} |
305 \index{*INT symbol}\index{*UN symbol} |
304 General unions and intersections of indexed |
306 General unions and intersections of indexed |
305 families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, |
307 families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, |
306 are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}. |
308 are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}. |
307 Their meaning is expressed using {\tt RepFun} as |
309 Their meaning is expressed using {\tt RepFun} as |
308 \[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad |
310 \[ |
309 \bigcap(\{B[x]. x\in A\}). |
311 \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad |
|
312 \bigcap(\{B[x]. x\in A\}). |
310 \] |
313 \] |
311 General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be |
314 General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be |
312 constructed in set theory, where $B[x]$ is a family of sets over~$A$. They |
315 constructed in set theory, where $B[x]$ is a family of sets over~$A$. They |
313 have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set. |
316 have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set. |
314 This is similar to the situation in Constructive Type Theory (set theory |
317 This is similar to the situation in Constructive Type Theory (set theory |
371 b : PrimReplace(A,P) <-> (EX x:A. P(x,b)) |
374 b : PrimReplace(A,P) <-> (EX x:A. P(x,b)) |
372 \subcaption{The Zermelo-Fraenkel Axioms} |
375 \subcaption{The Zermelo-Fraenkel Axioms} |
373 |
376 |
374 \tdx{Replace_def} Replace(A,P) == |
377 \tdx{Replace_def} Replace(A,P) == |
375 PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y)) |
378 PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y)) |
376 \tdx{RepFun_def} RepFun(A,f) == \{y . x:A, y=f(x)\} |
379 \tdx{RepFun_def} RepFun(A,f) == {\ttlbrace}y . x:A, y=f(x)\ttrbrace |
377 \tdx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\}) |
380 \tdx{the_def} The(P) == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace}) |
378 \tdx{if_def} if(P,a,b) == THE z. P & z=a | ~P & z=b |
381 \tdx{if_def} if(P,a,b) == THE z. P & z=a | ~P & z=b |
379 \tdx{Collect_def} Collect(A,P) == \{y . x:A, x=y & P(x)\} |
382 \tdx{Collect_def} Collect(A,P) == {\ttlbrace}y . x:A, x=y & P(x){\ttrbrace} |
380 \tdx{Upair_def} Upair(a,b) == |
383 \tdx{Upair_def} Upair(a,b) == |
381 \{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\} |
384 {\ttlbrace}y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b){\ttrbrace} |
382 \subcaption{Consequences of replacement} |
385 \subcaption{Consequences of replacement} |
383 |
386 |
384 \tdx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\} |
387 \tdx{Inter_def} Inter(A) == {\ttlbrace}x:Union(A) . ALL y:A. x:y{\ttrbrace} |
385 \tdx{Un_def} A Un B == Union(Upair(A,B)) |
388 \tdx{Un_def} A Un B == Union(Upair(A,B)) |
386 \tdx{Int_def} A Int B == Inter(Upair(A,B)) |
389 \tdx{Int_def} A Int B == Inter(Upair(A,B)) |
387 \tdx{Diff_def} A - B == \{ x:A . ~(x:B) \} |
390 \tdx{Diff_def} A - B == {\ttlbrace}x:A . x~:B{\ttrbrace} |
388 \subcaption{Union, intersection, difference} |
391 \subcaption{Union, intersection, difference} |
389 \end{ttbox} |
392 \end{ttbox} |
390 \caption{Rules and axioms of {\ZF}} \label{zf-rules} |
393 \caption{Rules and axioms of {\ZF}} \label{zf-rules} |
391 \end{figure} |
394 \end{figure} |
392 |
395 |
396 \tdx{cons_def} cons(a,A) == Upair(a,a) Un A |
399 \tdx{cons_def} cons(a,A) == Upair(a,a) Un A |
397 \tdx{succ_def} succ(i) == cons(i,i) |
400 \tdx{succ_def} succ(i) == cons(i,i) |
398 \tdx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) |
401 \tdx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) |
399 \subcaption{Finite and infinite sets} |
402 \subcaption{Finite and infinite sets} |
400 |
403 |
401 \tdx{Pair_def} <a,b> == \{\{a,a\}, \{a,b\}\} |
404 \tdx{Pair_def} <a,b> == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace} |
402 \tdx{split_def} split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b) |
405 \tdx{split_def} split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b) |
403 \tdx{fst_def} fst(A) == split(\%x y.x, p) |
406 \tdx{fst_def} fst(A) == split(\%x y.x, p) |
404 \tdx{snd_def} snd(A) == split(\%x y.y, p) |
407 \tdx{snd_def} snd(A) == split(\%x y.y, p) |
405 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\} |
408 \tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x,y>{\ttrbrace} |
406 \subcaption{Ordered pairs and Cartesian products} |
409 \subcaption{Ordered pairs and Cartesian products} |
407 |
410 |
408 \tdx{converse_def} converse(r) == \{z. w:r, EX x y. w=<x,y> & z=<y,x>\} |
411 \tdx{converse_def} converse(r) == {\ttlbrace}z. w:r, EX x y. w=<x,y> & z=<y,x>{\ttrbrace} |
409 \tdx{domain_def} domain(r) == \{x. w:r, EX y. w=<x,y>\} |
412 \tdx{domain_def} domain(r) == {\ttlbrace}x. w:r, EX y. w=<x,y>{\ttrbrace} |
410 \tdx{range_def} range(r) == domain(converse(r)) |
413 \tdx{range_def} range(r) == domain(converse(r)) |
411 \tdx{field_def} field(r) == domain(r) Un range(r) |
414 \tdx{field_def} field(r) == domain(r) Un range(r) |
412 \tdx{image_def} r `` A == \{y : range(r) . EX x:A. <x,y> : r\} |
415 \tdx{image_def} r `` A == {\ttlbrace}y : range(r) . EX x:A. <x,y> : r{\ttrbrace} |
413 \tdx{vimage_def} r -`` A == converse(r)``A |
416 \tdx{vimage_def} r -`` A == converse(r)``A |
414 \subcaption{Operations on relations} |
417 \subcaption{Operations on relations} |
415 |
418 |
416 \tdx{lam_def} Lambda(A,b) == \{<x,b(x)> . x:A\} |
419 \tdx{lam_def} Lambda(A,b) == {\ttlbrace}<x,b(x)> . x:A{\ttrbrace} |
417 \tdx{apply_def} f`a == THE y. <a,y> : f |
420 \tdx{apply_def} f`a == THE y. <a,y> : f |
418 \tdx{Pi_def} Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\} |
421 \tdx{Pi_def} Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f{\ttrbrace} |
419 \tdx{restrict_def} restrict(f,A) == lam x:A.f`x |
422 \tdx{restrict_def} restrict(f,A) == lam x:A.f`x |
420 \subcaption{Functions and general product} |
423 \subcaption{Functions and general product} |
421 \end{ttbox} |
424 \end{ttbox} |
422 \caption{Further definitions of {\ZF}} \label{zf-defs} |
425 \caption{Further definitions of {\ZF}} \label{zf-defs} |
423 \end{figure} |
426 \end{figure} |
566 |
569 |
567 %the [p] gives better page breaking for the book |
570 %the [p] gives better page breaking for the book |
568 \begin{figure}[p] |
571 \begin{figure}[p] |
569 \begin{ttbox} |
572 \begin{ttbox} |
570 \tdx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> |
573 \tdx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> |
571 b : \{y. x:A, P(x,y)\} |
574 b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace} |
572 |
575 |
573 \tdx{ReplaceE} [| b : \{y. x:A, P(x,y)\}; |
576 \tdx{ReplaceE} [| b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace}; |
574 !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R |
577 !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R |
575 |] ==> R |
578 |] ==> R |
576 |
579 |
577 \tdx{RepFunI} [| a : A |] ==> f(a) : \{f(x). x:A\} |
580 \tdx{RepFunI} [| a : A |] ==> f(a) : {\ttlbrace}f(x). x:A{\ttrbrace} |
578 \tdx{RepFunE} [| b : \{f(x). x:A\}; |
581 \tdx{RepFunE} [| b : {\ttlbrace}f(x). x:A{\ttrbrace}; |
579 !!x.[| x:A; b=f(x) |] ==> P |] ==> P |
582 !!x.[| x:A; b=f(x) |] ==> P |] ==> P |
580 |
583 |
581 \tdx{separation} a : \{x:A. P(x)\} <-> a:A & P(a) |
584 \tdx{separation} a : {\ttlbrace}x:A. P(x){\ttrbrace} <-> a:A & P(a) |
582 \tdx{CollectI} [| a:A; P(a) |] ==> a : \{x:A. P(x)\} |
585 \tdx{CollectI} [| a:A; P(a) |] ==> a : {\ttlbrace}x:A. P(x){\ttrbrace} |
583 \tdx{CollectE} [| a : \{x:A. P(x)\}; [| a:A; P(a) |] ==> R |] ==> R |
586 \tdx{CollectE} [| a : {\ttlbrace}x:A. P(x){\ttrbrace}; [| a:A; P(a) |] ==> R |] ==> R |
584 \tdx{CollectD1} a : \{x:A. P(x)\} ==> a:A |
587 \tdx{CollectD1} a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> a:A |
585 \tdx{CollectD2} a : \{x:A. P(x)\} ==> P(a) |
588 \tdx{CollectD2} a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> P(a) |
586 \end{ttbox} |
589 \end{ttbox} |
587 \caption{Replacement and separation} \label{zf-lemmas2} |
590 \caption{Replacement and separation} \label{zf-lemmas2} |
588 \end{figure} |
591 \end{figure} |
589 |
592 |
590 |
593 |
1023 % \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for {\tt bool} \\ |
1026 % \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for {\tt bool} \\ |
1024 % \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusive-or for {\tt bool} |
1027 % \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusive-or for {\tt bool} |
1025 %\end{constants} |
1028 %\end{constants} |
1026 % |
1029 % |
1027 \begin{ttbox} |
1030 \begin{ttbox} |
1028 \tdx{bool_def} bool == \{0,1\} |
1031 \tdx{bool_def} bool == {\ttlbrace}0,1{\ttrbrace} |
1029 \tdx{cond_def} cond(b,c,d) == if(b=1,c,d) |
1032 \tdx{cond_def} cond(b,c,d) == if(b=1,c,d) |
1030 \tdx{not_def} not(b) == cond(b,0,1) |
1033 \tdx{not_def} not(b) == cond(b,0,1) |
1031 \tdx{and_def} a and b == cond(a,b,0) |
1034 \tdx{and_def} a and b == cond(a,b,0) |
1032 \tdx{or_def} a or b == cond(a,1,b) |
1035 \tdx{or_def} a or b == cond(a,1,b) |
1033 \tdx{xor_def} a xor b == cond(a,not(b),b) |
1036 \tdx{xor_def} a xor b == cond(a,not(b),b) |
1064 \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ |
1067 \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ |
1065 \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ |
1068 \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ |
1066 \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ |
1069 \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ |
1067 \end{constants} |
1070 \end{constants} |
1068 \begin{ttbox} |
1071 \begin{ttbox} |
1069 \tdx{sum_def} A+B == \{0\}*A Un \{1\}*B |
1072 \tdx{sum_def} A+B == {\ttlbrace}0{\ttrbrace}*A Un {\ttlbrace}1{\ttrbrace}*B |
1070 \tdx{Inl_def} Inl(a) == <0,a> |
1073 \tdx{Inl_def} Inl(a) == <0,a> |
1071 \tdx{Inr_def} Inr(b) == <1,b> |
1074 \tdx{Inr_def} Inr(b) == <1,b> |
1072 \tdx{case_def} case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) |
1075 \tdx{case_def} case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) |
1073 |
1076 |
1074 \tdx{sum_InlI} a : A ==> Inl(a) : A+B |
1077 \tdx{sum_InlI} a : A ==> Inl(a) : A+B |
1095 \begin{figure} |
1098 \begin{figure} |
1096 \begin{ttbox} |
1099 \begin{ttbox} |
1097 \tdx{QPair_def} <a;b> == a+b |
1100 \tdx{QPair_def} <a;b> == a+b |
1098 \tdx{qsplit_def} qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b) |
1101 \tdx{qsplit_def} qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b) |
1099 \tdx{qfsplit_def} qfsplit(R,z) == EX x y. z=<x;y> & R(x,y) |
1102 \tdx{qfsplit_def} qfsplit(R,z) == EX x y. z=<x;y> & R(x,y) |
1100 \tdx{qconverse_def} qconverse(r) == \{z. w:r, EX x y. w=<x;y> & z=<y;x>\} |
1103 \tdx{qconverse_def} qconverse(r) == {\ttlbrace}z. w:r, EX x y. w=<x;y> & z=<y;x>{\ttrbrace} |
1101 \tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). \{<x;y>\} |
1104 \tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x;y>{\ttrbrace} |
1102 |
1105 |
1103 \tdx{qsum_def} A <+> B == (\{0\} <*> A) Un (\{1\} <*> B) |
1106 \tdx{qsum_def} A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) Un ({\ttlbrace}1{\ttrbrace} <*> B) |
1104 \tdx{QInl_def} QInl(a) == <0;a> |
1107 \tdx{QInl_def} QInl(a) == <0;a> |
1105 \tdx{QInr_def} QInr(b) == <1;b> |
1108 \tdx{QInr_def} QInr(b) == <1;b> |
1106 \tdx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) |
1109 \tdx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) |
1107 \end{ttbox} |
1110 \end{ttbox} |
1108 \caption{Non-standard pairs, products and sums} \label{zf-qpair} |
1111 \caption{Non-standard pairs, products and sums} \label{zf-qpair} |
1194 \cdx{surj} & $[i,i]\To i$ & & surjective function space\\ |
1197 \cdx{surj} & $[i,i]\To i$ & & surjective function space\\ |
1195 \cdx{bij} & $[i,i]\To i$ & & bijective function space |
1198 \cdx{bij} & $[i,i]\To i$ & & bijective function space |
1196 \end{constants} |
1199 \end{constants} |
1197 |
1200 |
1198 \begin{ttbox} |
1201 \begin{ttbox} |
1199 \tdx{comp_def} r O s == \{xz : domain(s)*range(r) . |
1202 \tdx{comp_def} r O s == {\ttlbrace}xz : domain(s)*range(r) . |
1200 EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\} |
1203 EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r{\ttrbrace} |
1201 \tdx{id_def} id(A) == (lam x:A. x) |
1204 \tdx{id_def} id(A) == (lam x:A. x) |
1202 \tdx{inj_def} inj(A,B) == \{ f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x\} |
1205 \tdx{inj_def} inj(A,B) == {\ttlbrace} f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x {\ttrbrace} |
1203 \tdx{surj_def} surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\} |
1206 \tdx{surj_def} surj(A,B) == {\ttlbrace} f: A->B . ALL y:B. EX x:A. f`x=y {\ttrbrace} |
1204 \tdx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B) |
1207 \tdx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B) |
1205 |
1208 |
1206 |
1209 |
1207 \tdx{left_inverse} [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a |
1210 \tdx{left_inverse} [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a |
1208 \tdx{right_inverse} [| f: inj(A,B); b: range(f) |] ==> |
1211 \tdx{right_inverse} [| f: inj(A,B); b: range(f) |] ==> |
1431 \item Theory {\tt Ord} defines the notions of transitive set and ordinal |
1434 \item Theory {\tt Ord} defines the notions of transitive set and ordinal |
1432 number. It derives transfinite induction. A key definition is {\bf |
1435 number. It derives transfinite induction. A key definition is {\bf |
1433 less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and |
1436 less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and |
1434 $i\in j$. As a special case, it includes less than on the natural |
1437 $i\in j$. As a special case, it includes less than on the natural |
1435 numbers. |
1438 numbers. |
1436 |
1439 |
1437 \item Theory {\tt Epsilon} derives $\epsilon$-induction and |
1440 \item Theory {\tt Epsilon} derives $\varepsilon$-induction and |
1438 $\epsilon$-recursion, which are generalisations of transfinite |
1441 $\varepsilon$-recursion, which are generalisations of transfinite |
1439 induction and recursion. It also defines \cdx{rank}$(x)$, which is the |
1442 induction and recursion. It also defines \cdx{rank}$(x)$, which |
1440 least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ |
1443 is the least ordinal $\alpha$ such that $x$ is constructed at |
1441 of the cumulative hierarchy (thus $x\in V@{\alpha+1}$). |
1444 stage $\alpha$ of the cumulative hierarchy (thus $x\in |
|
1445 V@{\alpha+1}$). |
1442 \end{itemize} |
1446 \end{itemize} |
1443 |
1447 |
1444 Other important theories lead to a theory of cardinal numbers. They have |
1448 Other important theories lead to a theory of cardinal numbers. They have |
1445 not yet been written up anywhere. Here is a summary: |
1449 not yet been written up anywhere. Here is a summary: |
1446 \begin{itemize} |
1450 \begin{itemize} |