author | paulson |
Wed, 08 Jan 1997 15:17:25 +0100 | |
changeset 2495 | 82ec47e0a8d3 |
parent 1449 | 25a7ddf9c080 |
child 3133 | 8c55b0f16da2 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
287 | 2 |
\chapter{Zermelo-Fraenkel Set Theory} |
317 | 3 |
\index{set theory|(} |
4 |
||
5 |
The theory~\thydx{ZF} implements Zermelo-Fraenkel set |
|
6 |
theory~\cite{halmos60,suppes72} as an extension of~{\tt FOL}, classical |
|
104 | 7 |
first-order logic. The theory includes a collection of derived natural |
317 | 8 |
deduction rules, for use with Isabelle's classical reasoner. Much |
9 |
of it is based on the work of No\"el~\cite{noel}. |
|
104 | 10 |
|
11 |
A tremendous amount of set theory has been formally developed, including |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
12 |
the basic properties of relations, functions, ordinals and cardinals. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
13 |
Significant results have been proved, such as the Schr\"oder-Bernstein |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
14 |
Theorem, the Wellordering Theorem and a version of Ramsey's Theorem. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
15 |
General methods have been developed for solving recursion equations over |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
16 |
monotonic functors; these have been applied to yield constructions of |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
17 |
lists, trees, infinite lists, etc. The Recursion Theorem has been proved, |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
18 |
admitting recursive definitions of functions over well-founded relations. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
19 |
Thus, we may even regard set theory as a computational logic, loosely |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
20 |
inspired by Martin-L\"of's Type Theory. |
104 | 21 |
|
2495 | 22 |
Because {\ZF} is an extension of {\FOL}, it provides the same packages, namely |
23 |
{\tt hyp_subst_tac}, the simplifier, and the classical reasoner. The default |
|
24 |
simpset and claset are usually satisfactory. Named simpsets include |
|
25 |
\ttindexbold{ZF_ss} (basic set theory rules) and \ttindexbold{rank_ss} (for |
|
26 |
proving termination of well-founded recursion). Named clasets sets include |
|
27 |
\ttindexbold{ZF_cs} (basic set theory) and \ttindexbold{le_cs} (useful for |
|
28 |
reasoning about the relations $<$ and $\le$). |
|
104 | 29 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
30 |
{\tt ZF} has a flexible package for handling inductive definitions, |
111 | 31 |
such as inference systems, and datatype definitions, such as lists and |
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
32 |
trees. Moreover it handles coinductive definitions, such as |
317 | 33 |
bisimulation relations, and codatatype definitions, such as streams. A |
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
34 |
recent paper describes the package~\cite{paulson-CADE}, but its examples |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
35 |
use an obsolete declaration syntax. Please consult the version of the |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
36 |
paper distributed with Isabelle. |
111 | 37 |
|
317 | 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 |
|
343 | 40 |
non-well-founded data structures within the standard {\sc zf} axioms including |
317 | 41 |
the Axiom of Foundation~\cite{paulson-final}. |
111 | 42 |
|
104 | 43 |
|
44 |
\section{Which version of axiomatic set theory?} |
|
317 | 45 |
The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg}) |
46 |
and Zermelo-Fraenkel~({\sc zf}). Resolution theorem provers can use {\sc |
|
47 |
bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not |
|
48 |
have a finite axiom system because of its Axiom Scheme of Replacement. |
|
49 |
This makes it awkward to use with many theorem provers, since instances |
|
50 |
of the axiom scheme have to be invoked explicitly. Since Isabelle has no |
|
51 |
difficulty with axiom schemes, we may adopt either axiom system. |
|
104 | 52 |
|
53 |
These two theories differ in their treatment of {\bf classes}, which are |
|
317 | 54 |
collections that are `too big' to be sets. The class of all sets,~$V$, |
55 |
cannot be a set without admitting Russell's Paradox. In {\sc bg}, both |
|
56 |
classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In |
|
57 |
{\sc zf}, all variables denote sets; classes are identified with unary |
|
58 |
predicates. The two systems define essentially the same sets and classes, |
|
59 |
with similar properties. In particular, a class cannot belong to another |
|
60 |
class (let alone a set). |
|
104 | 61 |
|
317 | 62 |
Modern set theorists tend to prefer {\sc zf} because they are mainly concerned |
63 |
with sets, rather than classes. {\sc bg} requires tiresome proofs that various |
|
104 | 64 |
collections are sets; for instance, showing $x\in\{x\}$ requires showing that |
317 | 65 |
$x$ is a set. |
104 | 66 |
|
67 |
||
68 |
\begin{figure} |
|
69 |
\begin{center} |
|
70 |
\begin{tabular}{rrr} |
|
111 | 71 |
\it name &\it meta-type & \it description \\ |
1449 | 72 |
\cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\ |
317 | 73 |
\cdx{0} & $i$ & empty set\\ |
74 |
\cdx{cons} & $[i,i]\To i$ & finite set constructor\\ |
|
75 |
\cdx{Upair} & $[i,i]\To i$ & unordered pairing\\ |
|
76 |
\cdx{Pair} & $[i,i]\To i$ & ordered pairing\\ |
|
77 |
\cdx{Inf} & $i$ & infinite set\\ |
|
78 |
\cdx{Pow} & $i\To i$ & powerset\\ |
|
79 |
\cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\ |
|
80 |
\cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ |
|
81 |
\cdx{fst} \cdx{snd} & $i\To i$ & projections\\ |
|
82 |
\cdx{converse}& $i\To i$ & converse of a relation\\ |
|
83 |
\cdx{succ} & $i\To i$ & successor\\ |
|
84 |
\cdx{Collect} & $[i,i\To o]\To i$ & separation\\ |
|
85 |
\cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ |
|
86 |
\cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ |
|
87 |
\cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ |
|
88 |
\cdx{Pi} \cdx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ |
|
89 |
\cdx{domain} & $i\To i$ & domain of a relation\\ |
|
90 |
\cdx{range} & $i\To i$ & range of a relation\\ |
|
91 |
\cdx{field} & $i\To i$ & field of a relation\\ |
|
92 |
\cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\ |
|
93 |
\cdx{restrict}& $[i, i] \To i$ & restriction of a function\\ |
|
94 |
\cdx{The} & $[i\To o]\To i$ & definite description\\ |
|
95 |
\cdx{if} & $[o,i,i]\To i$ & conditional\\ |
|
96 |
\cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers |
|
104 | 97 |
\end{tabular} |
98 |
\end{center} |
|
99 |
\subcaption{Constants} |
|
100 |
||
101 |
\begin{center} |
|
317 | 102 |
\index{*"`"` symbol} |
103 |
\index{*"-"`"` symbol} |
|
104 |
\index{*"` symbol}\index{function applications!in \ZF} |
|
105 |
\index{*"- symbol} |
|
106 |
\index{*": symbol} |
|
107 |
\index{*"<"= symbol} |
|
104 | 108 |
\begin{tabular}{rrrr} |
317 | 109 |
\it symbol & \it meta-type & \it priority & \it description \\ |
111 | 110 |
\tt `` & $[i,i]\To i$ & Left 90 & image \\ |
111 |
\tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\ |
|
112 |
\tt ` & $[i,i]\To i$ & Left 90 & application \\ |
|
317 | 113 |
\sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\inter$) \\ |
114 |
\sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\union$) \\ |
|
111 | 115 |
\tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex] |
116 |
\tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ |
|
117 |
\tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) |
|
104 | 118 |
\end{tabular} |
119 |
\end{center} |
|
120 |
\subcaption{Infixes} |
|
317 | 121 |
\caption{Constants of {\ZF}} \label{zf-constants} |
104 | 122 |
\end{figure} |
123 |
||
124 |
||
125 |
\section{The syntax of set theory} |
|
126 |
The language of set theory, as studied by logicians, has no constants. The |
|
127 |
traditional axioms merely assert the existence of empty sets, unions, |
|
128 |
powersets, etc.; this would be intolerable for practical reasoning. The |
|
129 |
Isabelle theory declares constants for primitive sets. It also extends |
|
130 |
{\tt FOL} with additional syntax for finite sets, ordered pairs, |
|
131 |
comprehension, general union/intersection, general sums/products, and |
|
132 |
bounded quantifiers. In most other respects, Isabelle implements precisely |
|
133 |
Zermelo-Fraenkel set theory. |
|
134 |
||
498 | 135 |
Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while |
317 | 136 |
Figure~\ref{zf-trans} presents the syntax translations. Finally, |
137 |
Figure~\ref{zf-syntax} presents the full grammar for set theory, including |
|
104 | 138 |
the constructs of \FOL. |
139 |
||
1449 | 140 |
Local abbreviations can be introduced by a {\tt let} construct whose |
141 |
syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into |
|
142 |
the constant~\cdx{Let}. It can be expanded by rewriting with its |
|
143 |
definition, \tdx{Let_def}. |
|
144 |
||
145 |
Apart from {\tt let}, set theory does not use polymorphism. All terms in |
|
146 |
{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt |
|
713 | 147 |
term}. The type of first-order formulae, remember, is~{\tt o}. |
104 | 148 |
|
317 | 149 |
Infix operators include binary union and intersection ($A\union B$ and |
150 |
$A\inter B$), set difference ($A-B$), and the subset and membership |
|
151 |
relations. Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$. The |
|
152 |
union and intersection operators ($\bigcup A$ and $\bigcap A$) form the |
|
153 |
union or intersection of a set of sets; $\bigcup A$ means the same as |
|
154 |
$\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive. |
|
104 | 155 |
|
317 | 156 |
The constant \cdx{Upair} constructs unordered pairs; thus {\tt |
157 |
Upair($A$,$B$)} denotes the set~$\{A,B\}$ and {\tt Upair($A$,$A$)} |
|
158 |
denotes the singleton~$\{A\}$. General union is used to define binary |
|
159 |
union. The Isabelle version goes on to define the constant |
|
160 |
\cdx{cons}: |
|
104 | 161 |
\begin{eqnarray*} |
111 | 162 |
A\cup B & \equiv & \bigcup({\tt Upair}(A,B)) \\ |
163 |
{\tt cons}(a,B) & \equiv & {\tt Upair}(a,a) \union B |
|
104 | 164 |
\end{eqnarray*} |
165 |
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the |
|
166 |
obvious manner using~{\tt cons} and~$\emptyset$ (the empty set): |
|
167 |
\begin{eqnarray*} |
|
168 |
\{a,b,c\} & \equiv & {\tt cons}(a,{\tt cons}(b,{\tt cons}(c,\emptyset))) |
|
169 |
\end{eqnarray*} |
|
170 |
||
317 | 171 |
The constant \cdx{Pair} constructs ordered pairs, as in {\tt |
104 | 172 |
Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets, |
111 | 173 |
as {\tt<$a$,$b$>}. The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>} |
317 | 174 |
abbreviates the nest of pairs\par\nobreak |
175 |
\centerline{\tt Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).} |
|
104 | 176 |
|
177 |
In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an |
|
178 |
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not |
|
179 |
say $i\To i$. The infix operator~{\tt`} denotes the application of a |
|
180 |
function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The |
|
181 |
syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$. |
|
182 |
||
183 |
||
184 |
\begin{figure} |
|
317 | 185 |
\index{lambda abs@$\lambda$-abstractions!in \ZF} |
186 |
\index{*"-"> symbol} |
|
187 |
\index{*"* symbol} |
|
287 | 188 |
\begin{center} \footnotesize\tt\frenchspacing |
104 | 189 |
\begin{tabular}{rrr} |
111 | 190 |
\it external & \it internal & \it description \\ |
104 | 191 |
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ |
192 |
\{$a@1$, $\ldots$, $a@n$\} & cons($a@1$,$\cdots$,cons($a@n$,0)) & |
|
193 |
\rm finite set \\ |
|
111 | 194 |
<$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & |
195 |
Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) & |
|
196 |
\rm ordered $n$-tuple \\ |
|
197 |
\{$x$:$A . P[x]$\} & Collect($A$,$\lambda x.P[x]$) & |
|
104 | 198 |
\rm separation \\ |
199 |
\{$y . x$:$A$, $Q[x,y]$\} & Replace($A$,$\lambda x\,y.Q[x,y]$) & |
|
200 |
\rm replacement \\ |
|
201 |
\{$b[x] . x$:$A$\} & RepFun($A$,$\lambda x.b[x]$) & |
|
202 |
\rm functional replacement \\ |
|
317 | 203 |
\sdx{INT} $x$:$A . B[x]$ & Inter(\{$B[x] . x$:$A$\}) & |
111 | 204 |
\rm general intersection \\ |
317 | 205 |
\sdx{UN} $x$:$A . B[x]$ & Union(\{$B[x] . x$:$A$\}) & |
111 | 206 |
\rm general union \\ |
317 | 207 |
\sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & |
111 | 208 |
\rm general product \\ |
317 | 209 |
\sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & |
111 | 210 |
\rm general sum \\ |
211 |
$A$ -> $B$ & Pi($A$,$\lambda x.B$) & |
|
212 |
\rm function space \\ |
|
213 |
$A$ * $B$ & Sigma($A$,$\lambda x.B$) & |
|
214 |
\rm binary product \\ |
|
317 | 215 |
\sdx{THE} $x . P[x]$ & The($\lambda x.P[x]$) & |
111 | 216 |
\rm definite description \\ |
317 | 217 |
\sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x.b[x]$) & |
111 | 218 |
\rm $\lambda$-abstraction\\[1ex] |
317 | 219 |
\sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x.P[x]$) & |
111 | 220 |
\rm bounded $\forall$ \\ |
317 | 221 |
\sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x.P[x]$) & |
111 | 222 |
\rm bounded $\exists$ |
104 | 223 |
\end{tabular} |
224 |
\end{center} |
|
317 | 225 |
\caption{Translations for {\ZF}} \label{zf-trans} |
104 | 226 |
\end{figure} |
227 |
||
228 |
||
229 |
\begin{figure} |
|
1449 | 230 |
\index{*let symbol} |
231 |
\index{*in symbol} |
|
104 | 232 |
\dquotes |
233 |
\[\begin{array}{rcl} |
|
234 |
term & = & \hbox{expression of type~$i$} \\ |
|
1449 | 235 |
& | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ |
111 | 236 |
& | & "\{ " term\; ("," term)^* " \}" \\ |
317 | 237 |
& | & "< " term\; ("," term)^* " >" \\ |
111 | 238 |
& | & "\{ " id ":" term " . " formula " \}" \\ |
317 | 239 |
& | & "\{ " id " . " id ":" term ", " formula " \}" \\ |
111 | 240 |
& | & "\{ " term " . " id ":" term " \}" \\ |
241 |
& | & term " `` " term \\ |
|
242 |
& | & term " -`` " term \\ |
|
243 |
& | & term " ` " term \\ |
|
244 |
& | & term " * " term \\ |
|
245 |
& | & term " Int " term \\ |
|
246 |
& | & term " Un " term \\ |
|
247 |
& | & term " - " term \\ |
|
248 |
& | & term " -> " term \\ |
|
249 |
& | & "THE~~" id " . " formula\\ |
|
250 |
& | & "lam~~" id ":" term " . " term \\ |
|
251 |
& | & "INT~~" id ":" term " . " term \\ |
|
252 |
& | & "UN~~~" id ":" term " . " term \\ |
|
253 |
& | & "PROD~" id ":" term " . " term \\ |
|
254 |
& | & "SUM~~" id ":" term " . " term \\[2ex] |
|
104 | 255 |
formula & = & \hbox{expression of type~$o$} \\ |
111 | 256 |
& | & term " : " term \\ |
317 | 257 |
& | & term " \ttilde: " term \\ |
111 | 258 |
& | & term " <= " term \\ |
259 |
& | & term " = " term \\ |
|
317 | 260 |
& | & term " \ttilde= " term \\ |
111 | 261 |
& | & "\ttilde\ " formula \\ |
262 |
& | & formula " \& " formula \\ |
|
263 |
& | & formula " | " formula \\ |
|
264 |
& | & formula " --> " formula \\ |
|
265 |
& | & formula " <-> " formula \\ |
|
266 |
& | & "ALL " id ":" term " . " formula \\ |
|
267 |
& | & "EX~~" id ":" term " . " formula \\ |
|
268 |
& | & "ALL~" id~id^* " . " formula \\ |
|
269 |
& | & "EX~~" id~id^* " . " formula \\ |
|
270 |
& | & "EX!~" id~id^* " . " formula |
|
104 | 271 |
\end{array} |
272 |
\] |
|
317 | 273 |
\caption{Full grammar for {\ZF}} \label{zf-syntax} |
104 | 274 |
\end{figure} |
275 |
||
276 |
||
277 |
\section{Binding operators} |
|
317 | 278 |
The constant \cdx{Collect} constructs sets by the principle of {\bf |
104 | 279 |
separation}. The syntax for separation is \hbox{\tt\{$x$:$A$.$P[x]$\}}, |
280 |
where $P[x]$ is a formula that may contain free occurrences of~$x$. It |
|
317 | 281 |
abbreviates the set {\tt Collect($A$,$\lambda x.P[x]$)}, which consists of |
104 | 282 |
all $x\in A$ that satisfy~$P[x]$. Note that {\tt Collect} is an |
283 |
unfortunate choice of name: some set theories adopt a set-formation |
|
284 |
principle, related to replacement, called collection. |
|
285 |
||
317 | 286 |
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 |
set {\tt Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such |
|
289 |
that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom has |
|
290 |
the condition that $Q$ must be single-valued over~$A$: for all~$x\in A$ |
|
291 |
there exists at most one $y$ satisfying~$Q[x,y]$. A single-valued binary |
|
104 | 292 |
predicate is also called a {\bf class function}. |
293 |
||
317 | 294 |
The constant \cdx{RepFun} expresses a special case of replacement, |
104 | 295 |
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 |
|
287 | 297 |
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 |
|
299 |
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 |
|
301 |
x.b[x]$)}. |
|
104 | 302 |
|
317 | 303 |
\index{*INT symbol}\index{*UN symbol} |
287 | 304 |
General unions and intersections of indexed |
305 |
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]$}. |
|
307 |
Their meaning is expressed using {\tt RepFun} as |
|
104 | 308 |
\[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad |
309 |
\bigcap(\{B[x]. x\in A\}). |
|
310 |
\] |
|
311 |
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 |
|
313 |
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 | 315 |
has `dependent sets') and calls for similar syntactic conventions. The |
316 |
constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and |
|
104 | 317 |
products. Instead of {\tt Sigma($A$,$B$)} and {\tt Pi($A$,$B$)} we may write |
318 |
\hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt PROD $x$:$A$.$B[x]$}. |
|
317 | 319 |
\index{*SUM symbol}\index{*PROD symbol}% |
104 | 320 |
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate |
321 |
general sums and products over a constant family.\footnote{Unlike normal |
|
322 |
infix operators, {\tt*} and {\tt->} merely define abbreviations; there are |
|
323 |
no constants~{\tt op~*} and~\hbox{\tt op~->}.} Isabelle accepts these |
|
324 |
abbreviations in parsing and uses them whenever possible for printing. |
|
325 |
||
317 | 326 |
\index{*THE symbol} |
104 | 327 |
As mentioned above, whenever the axioms assert the existence and uniqueness |
328 |
of a set, Isabelle's set theory declares a constant for that set. These |
|
329 |
constants can express the {\bf definite description} operator~$\iota |
|
330 |
x.P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists. |
|
331 |
Since all terms in {\ZF} denote something, a description is always |
|
332 |
meaningful, but we do not know its value unless $P[x]$ defines it uniquely. |
|
317 | 333 |
Using the constant~\cdx{The}, we may write descriptions as {\tt |
104 | 334 |
The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}. |
335 |
||
317 | 336 |
\index{*lam symbol} |
104 | 337 |
Function sets may be written in $\lambda$-notation; $\lambda x\in A.b[x]$ |
338 |
stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for |
|
339 |
this to be a set, the function's domain~$A$ must be given. Using the |
|
317 | 340 |
constant~\cdx{Lambda}, we may express function sets as {\tt |
104 | 341 |
Lambda($A$,$\lambda x.b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.$b[x]$}. |
342 |
||
343 |
Isabelle's set theory defines two {\bf bounded quantifiers}: |
|
344 |
\begin{eqnarray*} |
|
317 | 345 |
\forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ |
346 |
\exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] |
|
104 | 347 |
\end{eqnarray*} |
317 | 348 |
The constants~\cdx{Ball} and~\cdx{Bex} are defined |
104 | 349 |
accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may |
350 |
write |
|
351 |
\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}. |
|
352 |
||
353 |
||
343 | 354 |
%%%% ZF.thy |
104 | 355 |
|
356 |
\begin{figure} |
|
357 |
\begin{ttbox} |
|
1449 | 358 |
\tdx{Let_def} Let(s, f) == f(s) |
359 |
||
317 | 360 |
\tdx{Ball_def} Ball(A,P) == ALL x. x:A --> P(x) |
361 |
\tdx{Bex_def} Bex(A,P) == EX x. x:A & P(x) |
|
104 | 362 |
|
317 | 363 |
\tdx{subset_def} A <= B == ALL x:A. x:B |
364 |
\tdx{extension} A = B <-> A <= B & B <= A |
|
104 | 365 |
|
498 | 366 |
\tdx{Union_iff} A : Union(C) <-> (EX B:C. A:B) |
367 |
\tdx{Pow_iff} A : Pow(B) <-> A <= B |
|
317 | 368 |
\tdx{foundation} A=0 | (EX x:A. ALL y:x. ~ y:A) |
104 | 369 |
|
317 | 370 |
\tdx{replacement} (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> |
104 | 371 |
b : PrimReplace(A,P) <-> (EX x:A. P(x,b)) |
372 |
\subcaption{The Zermelo-Fraenkel Axioms} |
|
373 |
||
317 | 374 |
\tdx{Replace_def} Replace(A,P) == |
287 | 375 |
PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y)) |
317 | 376 |
\tdx{RepFun_def} RepFun(A,f) == \{y . x:A, y=f(x)\} |
377 |
\tdx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\}) |
|
378 |
\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)\} |
|
380 |
\tdx{Upair_def} Upair(a,b) == |
|
104 | 381 |
\{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\} |
382 |
\subcaption{Consequences of replacement} |
|
383 |
||
317 | 384 |
\tdx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\} |
385 |
\tdx{Un_def} A Un B == Union(Upair(A,B)) |
|
386 |
\tdx{Int_def} A Int B == Inter(Upair(A,B)) |
|
387 |
\tdx{Diff_def} A - B == \{ x:A . ~(x:B) \} |
|
104 | 388 |
\subcaption{Union, intersection, difference} |
389 |
\end{ttbox} |
|
317 | 390 |
\caption{Rules and axioms of {\ZF}} \label{zf-rules} |
104 | 391 |
\end{figure} |
392 |
||
393 |
||
394 |
\begin{figure} |
|
395 |
\begin{ttbox} |
|
317 | 396 |
\tdx{cons_def} cons(a,A) == Upair(a,a) Un A |
397 |
\tdx{succ_def} succ(i) == cons(i,i) |
|
398 |
\tdx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf) |
|
111 | 399 |
\subcaption{Finite and infinite sets} |
400 |
||
317 | 401 |
\tdx{Pair_def} <a,b> == \{\{a,a\}, \{a,b\}\} |
402 |
\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) |
|
404 |
\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>\} |
|
104 | 406 |
\subcaption{Ordered pairs and Cartesian products} |
407 |
||
317 | 408 |
\tdx{converse_def} converse(r) == \{z. w:r, EX x y. w=<x,y> & z=<y,x>\} |
409 |
\tdx{domain_def} domain(r) == \{x. w:r, EX y. w=<x,y>\} |
|
410 |
\tdx{range_def} range(r) == domain(converse(r)) |
|
411 |
\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\} |
|
413 |
\tdx{vimage_def} r -`` A == converse(r)``A |
|
104 | 414 |
\subcaption{Operations on relations} |
415 |
||
317 | 416 |
\tdx{lam_def} Lambda(A,b) == \{<x,b(x)> . x:A\} |
417 |
\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\} |
|
419 |
\tdx{restrict_def} restrict(f,A) == lam x:A.f`x |
|
104 | 420 |
\subcaption{Functions and general product} |
421 |
\end{ttbox} |
|
317 | 422 |
\caption{Further definitions of {\ZF}} \label{zf-defs} |
104 | 423 |
\end{figure} |
424 |
||
425 |
||
426 |
||
427 |
\section{The Zermelo-Fraenkel axioms} |
|
317 | 428 |
The axioms appear in Fig.\ts \ref{zf-rules}. They resemble those |
104 | 429 |
presented by Suppes~\cite{suppes72}. Most of the theory consists of |
430 |
definitions. In particular, bounded quantifiers and the subset relation |
|
431 |
appear in other axioms. Object-level quantifiers and implications have |
|
432 |
been replaced by meta-level ones wherever possible, to simplify use of the |
|
343 | 433 |
axioms. See the file {\tt ZF/ZF.thy} for details. |
104 | 434 |
|
435 |
The traditional replacement axiom asserts |
|
436 |
\[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \] |
|
437 |
subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$. |
|
317 | 438 |
The Isabelle theory defines \cdx{Replace} to apply |
439 |
\cdx{PrimReplace} to the single-valued part of~$P$, namely |
|
104 | 440 |
\[ (\exists!z.P(x,z)) \conj P(x,y). \] |
441 |
Thus $y\in {\tt Replace}(A,P)$ if and only if there is some~$x$ such that |
|
442 |
$P(x,-)$ holds uniquely for~$y$. Because the equivalence is unconditional, |
|
443 |
{\tt Replace} is much easier to use than {\tt PrimReplace}; it defines the |
|
444 |
same set, if $P(x,y)$ is single-valued. The nice syntax for replacement |
|
445 |
expands to {\tt Replace}. |
|
446 |
||
447 |
Other consequences of replacement include functional replacement |
|
317 | 448 |
(\cdx{RepFun}) and definite descriptions (\cdx{The}). |
449 |
Axioms for separation (\cdx{Collect}) and unordered pairs |
|
450 |
(\cdx{Upair}) are traditionally assumed, but they actually follow |
|
104 | 451 |
from replacement~\cite[pages 237--8]{suppes72}. |
452 |
||
453 |
The definitions of general intersection, etc., are straightforward. Note |
|
317 | 454 |
the definition of {\tt cons}, which underlies the finite set notation. |
104 | 455 |
The axiom of infinity gives us a set that contains~0 and is closed under |
317 | 456 |
successor (\cdx{succ}). Although this set is not uniquely defined, |
457 |
the theory names it (\cdx{Inf}) in order to simplify the |
|
104 | 458 |
construction of the natural numbers. |
111 | 459 |
|
317 | 460 |
Further definitions appear in Fig.\ts\ref{zf-defs}. Ordered pairs are |
104 | 461 |
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall |
317 | 462 |
that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two |
104 | 463 |
sets. It is defined to be the union of all singleton sets |
464 |
$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of |
|
465 |
general union. |
|
466 |
||
317 | 467 |
The projections \cdx{fst} and~\cdx{snd} are defined in terms of the |
468 |
generalized projection \cdx{split}. The latter has been borrowed from |
|
469 |
Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst} |
|
470 |
and~\cdx{snd}. |
|
471 |
||
104 | 472 |
Operations on relations include converse, domain, range, and image. The |
473 |
set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets. |
|
474 |
Note the simple definitions of $\lambda$-abstraction (using |
|
317 | 475 |
\cdx{RepFun}) and application (using a definite description). The |
476 |
function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only |
|
104 | 477 |
over the domain~$A$. |
478 |
||
317 | 479 |
|
480 |
%%%% zf.ML |
|
481 |
||
482 |
\begin{figure} |
|
483 |
\begin{ttbox} |
|
484 |
\tdx{ballI} [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x) |
|
485 |
\tdx{bspec} [| ALL x:A. P(x); x: A |] ==> P(x) |
|
486 |
\tdx{ballE} [| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q |
|
487 |
||
488 |
\tdx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
489 |
(ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) |
|
490 |
||
491 |
\tdx{bexI} [| P(x); x: A |] ==> EX x:A. P(x) |
|
492 |
\tdx{bexCI} [| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A.P(x) |
|
493 |
\tdx{bexE} [| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q |
|
494 |
||
495 |
\tdx{bex_cong} [| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
496 |
(EX x:A. P(x)) <-> (EX x:A'. P'(x)) |
|
497 |
\subcaption{Bounded quantifiers} |
|
498 |
||
499 |
\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B |
|
500 |
\tdx{subsetD} [| A <= B; c:A |] ==> c:B |
|
501 |
\tdx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P |
|
502 |
\tdx{subset_refl} A <= A |
|
503 |
\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C |
|
504 |
||
505 |
\tdx{equalityI} [| A <= B; B <= A |] ==> A = B |
|
506 |
\tdx{equalityD1} A = B ==> A<=B |
|
507 |
\tdx{equalityD2} A = B ==> B<=A |
|
508 |
\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P |
|
509 |
\subcaption{Subsets and extensionality} |
|
510 |
||
511 |
\tdx{emptyE} a:0 ==> P |
|
512 |
\tdx{empty_subsetI} 0 <= A |
|
513 |
\tdx{equals0I} [| !!y. y:A ==> False |] ==> A=0 |
|
514 |
\tdx{equals0D} [| A=0; a:A |] ==> P |
|
515 |
||
516 |
\tdx{PowI} A <= B ==> A : Pow(B) |
|
517 |
\tdx{PowD} A : Pow(B) ==> A<=B |
|
518 |
\subcaption{The empty set; power sets} |
|
519 |
\end{ttbox} |
|
520 |
\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1} |
|
521 |
\end{figure} |
|
104 | 522 |
|
523 |
||
524 |
\section{From basic lemmas to function spaces} |
|
525 |
Faced with so many definitions, it is essential to prove lemmas. Even |
|
526 |
trivial theorems like $A\inter B=B\inter A$ would be difficult to prove |
|
527 |
from the definitions alone. Isabelle's set theory derives many rules using |
|
528 |
a natural deduction style. Ideally, a natural deduction rule should |
|
529 |
introduce or eliminate just one operator, but this is not always practical. |
|
530 |
For most operators, we may forget its definition and use its derived rules |
|
531 |
instead. |
|
532 |
||
533 |
\subsection{Fundamental lemmas} |
|
317 | 534 |
Figure~\ref{zf-lemmas1} presents the derived rules for the most basic |
104 | 535 |
operators. The rules for the bounded quantifiers resemble those for the |
343 | 536 |
ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption |
537 |
in the style of Isabelle's classical reasoner. The \rmindex{congruence |
|
538 |
rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's |
|
104 | 539 |
simplifier, but have few other uses. Congruence rules must be specially |
540 |
derived for all binding operators, and henceforth will not be shown. |
|
541 |
||
317 | 542 |
Figure~\ref{zf-lemmas1} also shows rules for the subset and equality |
104 | 543 |
relations (proof by extensionality), and rules about the empty set and the |
544 |
power set operator. |
|
545 |
||
317 | 546 |
Figure~\ref{zf-lemmas2} presents rules for replacement and separation. |
547 |
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than |
|
104 | 548 |
comparable rules for {\tt PrimReplace} would be. The principle of |
549 |
separation is proved explicitly, although most proofs should use the |
|
317 | 550 |
natural deduction rules for {\tt Collect}. The elimination rule |
551 |
\tdx{CollectE} is equivalent to the two destruction rules |
|
552 |
\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to |
|
104 | 553 |
particular circumstances. Although too many rules can be confusing, there |
554 |
is no reason to aim for a minimal set of rules. See the file |
|
343 | 555 |
{\tt ZF/ZF.ML} for a complete listing. |
104 | 556 |
|
317 | 557 |
Figure~\ref{zf-lemmas3} presents rules for general union and intersection. |
104 | 558 |
The empty intersection should be undefined. We cannot have |
559 |
$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All |
|
560 |
expressions denote something in {\ZF} set theory; the definition of |
|
561 |
intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is |
|
317 | 562 |
arbitrary. The rule \tdx{InterI} must have a premise to exclude |
104 | 563 |
the empty intersection. Some of the laws governing intersections require |
564 |
similar premises. |
|
565 |
||
566 |
||
317 | 567 |
%the [p] gives better page breaking for the book |
568 |
\begin{figure}[p] |
|
569 |
\begin{ttbox} |
|
570 |
\tdx{ReplaceI} [| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> |
|
571 |
b : \{y. x:A, P(x,y)\} |
|
572 |
||
573 |
\tdx{ReplaceE} [| b : \{y. x:A, P(x,y)\}; |
|
574 |
!!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R |
|
575 |
|] ==> R |
|
576 |
||
577 |
\tdx{RepFunI} [| a : A |] ==> f(a) : \{f(x). x:A\} |
|
578 |
\tdx{RepFunE} [| b : \{f(x). x:A\}; |
|
579 |
!!x.[| x:A; b=f(x) |] ==> P |] ==> P |
|
580 |
||
581 |
\tdx{separation} a : \{x:A. P(x)\} <-> a:A & P(a) |
|
582 |
\tdx{CollectI} [| a:A; P(a) |] ==> a : \{x:A. P(x)\} |
|
583 |
\tdx{CollectE} [| a : \{x:A. P(x)\}; [| a:A; P(a) |] ==> R |] ==> R |
|
584 |
\tdx{CollectD1} a : \{x:A. P(x)\} ==> a:A |
|
585 |
\tdx{CollectD2} a : \{x:A. P(x)\} ==> P(a) |
|
586 |
\end{ttbox} |
|
587 |
\caption{Replacement and separation} \label{zf-lemmas2} |
|
588 |
\end{figure} |
|
589 |
||
590 |
||
591 |
\begin{figure} |
|
592 |
\begin{ttbox} |
|
593 |
\tdx{UnionI} [| B: C; A: B |] ==> A: Union(C) |
|
594 |
\tdx{UnionE} [| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R |
|
595 |
||
596 |
\tdx{InterI} [| !!x. x: C ==> A: x; c:C |] ==> A : Inter(C) |
|
597 |
\tdx{InterD} [| A : Inter(C); B : C |] ==> A : B |
|
598 |
\tdx{InterE} [| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R |
|
599 |
||
600 |
\tdx{UN_I} [| a: A; b: B(a) |] ==> b: (UN x:A. B(x)) |
|
601 |
\tdx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |
|
602 |
|] ==> R |
|
603 |
||
604 |
\tdx{INT_I} [| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x)) |
|
605 |
\tdx{INT_E} [| b : (INT x:A. B(x)); a: A |] ==> b : B(a) |
|
606 |
\end{ttbox} |
|
607 |
\caption{General union and intersection} \label{zf-lemmas3} |
|
608 |
\end{figure} |
|
609 |
||
610 |
||
104 | 611 |
%%% upair.ML |
612 |
||
613 |
\begin{figure} |
|
614 |
\begin{ttbox} |
|
317 | 615 |
\tdx{pairing} a:Upair(b,c) <-> (a=b | a=c) |
616 |
\tdx{UpairI1} a : Upair(a,b) |
|
617 |
\tdx{UpairI2} b : Upair(a,b) |
|
618 |
\tdx{UpairE} [| a : Upair(b,c); a = b ==> P; a = c ==> P |] ==> P |
|
619 |
\end{ttbox} |
|
620 |
\caption{Unordered pairs} \label{zf-upair1} |
|
621 |
\end{figure} |
|
622 |
||
104 | 623 |
|
317 | 624 |
\begin{figure} |
625 |
\begin{ttbox} |
|
626 |
\tdx{UnI1} c : A ==> c : A Un B |
|
627 |
\tdx{UnI2} c : B ==> c : A Un B |
|
628 |
\tdx{UnCI} (~c : B ==> c : A) ==> c : A Un B |
|
629 |
\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P |
|
630 |
||
631 |
\tdx{IntI} [| c : A; c : B |] ==> c : A Int B |
|
632 |
\tdx{IntD1} c : A Int B ==> c : A |
|
633 |
\tdx{IntD2} c : A Int B ==> c : B |
|
634 |
\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P |
|
104 | 635 |
|
317 | 636 |
\tdx{DiffI} [| c : A; ~ c : B |] ==> c : A - B |
637 |
\tdx{DiffD1} c : A - B ==> c : A |
|
498 | 638 |
\tdx{DiffD2} c : A - B ==> c ~: B |
317 | 639 |
\tdx{DiffE} [| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P |
640 |
\end{ttbox} |
|
641 |
\caption{Union, intersection, difference} \label{zf-Un} |
|
642 |
\end{figure} |
|
643 |
||
104 | 644 |
|
317 | 645 |
\begin{figure} |
646 |
\begin{ttbox} |
|
647 |
\tdx{consI1} a : cons(a,B) |
|
648 |
\tdx{consI2} a : B ==> a : cons(b,B) |
|
649 |
\tdx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B) |
|
650 |
\tdx{consE} [| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P |
|
651 |
||
652 |
\tdx{singletonI} a : \{a\} |
|
653 |
\tdx{singletonE} [| a : \{b\}; a=b ==> P |] ==> P |
|
104 | 654 |
\end{ttbox} |
317 | 655 |
\caption{Finite and singleton sets} \label{zf-upair2} |
104 | 656 |
\end{figure} |
657 |
||
658 |
||
659 |
\begin{figure} |
|
660 |
\begin{ttbox} |
|
317 | 661 |
\tdx{succI1} i : succ(i) |
662 |
\tdx{succI2} i : j ==> i : succ(j) |
|
663 |
\tdx{succCI} (~ i:j ==> i=j) ==> i: succ(j) |
|
664 |
\tdx{succE} [| i : succ(j); i=j ==> P; i:j ==> P |] ==> P |
|
665 |
\tdx{succ_neq_0} [| succ(n)=0 |] ==> P |
|
666 |
\tdx{succ_inject} succ(m) = succ(n) ==> m=n |
|
667 |
\end{ttbox} |
|
668 |
\caption{The successor function} \label{zf-succ} |
|
669 |
\end{figure} |
|
104 | 670 |
|
671 |
||
317 | 672 |
\begin{figure} |
673 |
\begin{ttbox} |
|
674 |
\tdx{the_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a |
|
675 |
\tdx{theI} EX! x. P(x) ==> P(THE x. P(x)) |
|
104 | 676 |
|
461 | 677 |
\tdx{if_P} P ==> if(P,a,b) = a |
678 |
\tdx{if_not_P} ~P ==> if(P,a,b) = b |
|
104 | 679 |
|
461 | 680 |
\tdx{mem_asym} [| a:b; b:a |] ==> P |
681 |
\tdx{mem_irrefl} a:a ==> P |
|
104 | 682 |
\end{ttbox} |
317 | 683 |
\caption{Descriptions; non-circularity} \label{zf-the} |
104 | 684 |
\end{figure} |
685 |
||
686 |
||
687 |
\subsection{Unordered pairs and finite sets} |
|
317 | 688 |
Figure~\ref{zf-upair1} presents the principle of unordered pairing, along |
104 | 689 |
with its derived rules. Binary union and intersection are defined in terms |
317 | 690 |
of ordered pairs (Fig.\ts\ref{zf-Un}). Set difference is also included. The |
691 |
rule \tdx{UnCI} is useful for classical reasoning about unions, |
|
692 |
like {\tt disjCI}\@; it supersedes \tdx{UnI1} and |
|
693 |
\tdx{UnI2}, but these rules are often easier to work with. For |
|
104 | 694 |
intersection and difference we have both elimination and destruction rules. |
695 |
Again, there is no reason to provide a minimal rule set. |
|
696 |
||
317 | 697 |
Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules |
698 |
for~{\tt cons}, the finite set constructor, and rules for singleton |
|
699 |
sets. Figure~\ref{zf-succ} presents derived rules for the successor |
|
700 |
function, which is defined in terms of~{\tt cons}. The proof that {\tt |
|
701 |
succ} is injective appears to require the Axiom of Foundation. |
|
104 | 702 |
|
317 | 703 |
Definite descriptions (\sdx{THE}) are defined in terms of the singleton |
704 |
set~$\{0\}$, but their derived rules fortunately hide this |
|
705 |
(Fig.\ts\ref{zf-the}). The rule~\tdx{theI} is difficult to apply |
|
706 |
because of the two occurrences of~$\Var{P}$. However, |
|
707 |
\tdx{the_equality} does not have this problem and the files contain |
|
708 |
many examples of its use. |
|
104 | 709 |
|
710 |
Finally, the impossibility of having both $a\in b$ and $b\in a$ |
|
461 | 711 |
(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to |
104 | 712 |
the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence. |
713 |
||
317 | 714 |
See the file {\tt ZF/upair.ML} for full proofs of the rules discussed in |
715 |
this section. |
|
104 | 716 |
|
717 |
||
718 |
%%% subset.ML |
|
719 |
||
720 |
\begin{figure} |
|
721 |
\begin{ttbox} |
|
317 | 722 |
\tdx{Union_upper} B:A ==> B <= Union(A) |
723 |
\tdx{Union_least} [| !!x. x:A ==> x<=C |] ==> Union(A) <= C |
|
104 | 724 |
|
317 | 725 |
\tdx{Inter_lower} B:A ==> Inter(A) <= B |
726 |
\tdx{Inter_greatest} [| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A) |
|
104 | 727 |
|
317 | 728 |
\tdx{Un_upper1} A <= A Un B |
729 |
\tdx{Un_upper2} B <= A Un B |
|
730 |
\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C |
|
104 | 731 |
|
317 | 732 |
\tdx{Int_lower1} A Int B <= A |
733 |
\tdx{Int_lower2} A Int B <= B |
|
734 |
\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B |
|
104 | 735 |
|
317 | 736 |
\tdx{Diff_subset} A-B <= A |
737 |
\tdx{Diff_contains} [| C<=A; C Int B = 0 |] ==> C <= A-B |
|
104 | 738 |
|
317 | 739 |
\tdx{Collect_subset} Collect(A,P) <= A |
104 | 740 |
\end{ttbox} |
317 | 741 |
\caption{Subset and lattice properties} \label{zf-subset} |
104 | 742 |
\end{figure} |
743 |
||
744 |
||
745 |
\subsection{Subset and lattice properties} |
|
317 | 746 |
The subset relation is a complete lattice. Unions form least upper bounds; |
747 |
non-empty intersections form greatest lower bounds. Figure~\ref{zf-subset} |
|
748 |
shows the corresponding rules. A few other laws involving subsets are |
|
749 |
included. Proofs are in the file {\tt ZF/subset.ML}. |
|
750 |
||
751 |
Reasoning directly about subsets often yields clearer proofs than |
|
752 |
reasoning about the membership relation. Section~\ref{sec:ZF-pow-example} |
|
753 |
below presents an example of this, proving the equation ${{\tt Pow}(A)\cap |
|
754 |
{\tt Pow}(B)}= {\tt Pow}(A\cap B)$. |
|
104 | 755 |
|
756 |
%%% pair.ML |
|
757 |
||
758 |
\begin{figure} |
|
759 |
\begin{ttbox} |
|
317 | 760 |
\tdx{Pair_inject1} <a,b> = <c,d> ==> a=c |
761 |
\tdx{Pair_inject2} <a,b> = <c,d> ==> b=d |
|
762 |
\tdx{Pair_inject} [| <a,b> = <c,d>; [| a=c; b=d |] ==> P |] ==> P |
|
763 |
\tdx{Pair_neq_0} <a,b>=0 ==> P |
|
104 | 764 |
|
349 | 765 |
\tdx{fst_conv} fst(<a,b>) = a |
766 |
\tdx{snd_conv} snd(<a,b>) = b |
|
317 | 767 |
\tdx{split} split(\%x y.c(x,y), <a,b>) = c(a,b) |
104 | 768 |
|
317 | 769 |
\tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B) |
104 | 770 |
|
317 | 771 |
\tdx{SigmaE} [| c: Sigma(A,B); |
772 |
!!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P |
|
104 | 773 |
|
317 | 774 |
\tdx{SigmaE2} [| <a,b> : Sigma(A,B); |
775 |
[| a:A; b:B(a) |] ==> P |] ==> P |
|
104 | 776 |
\end{ttbox} |
317 | 777 |
\caption{Ordered pairs; projections; general sums} \label{zf-pair} |
104 | 778 |
\end{figure} |
779 |
||
780 |
||
781 |
\subsection{Ordered pairs} |
|
317 | 782 |
Figure~\ref{zf-pair} presents the rules governing ordered pairs, |
287 | 783 |
projections and general sums. File {\tt ZF/pair.ML} contains the |
104 | 784 |
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered |
785 |
pair. This property is expressed as two destruction rules, |
|
317 | 786 |
\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently |
787 |
as the elimination rule \tdx{Pair_inject}. |
|
104 | 788 |
|
317 | 789 |
The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This |
114 | 790 |
is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other |
343 | 791 |
encodings of ordered pairs. The non-standard ordered pairs mentioned below |
114 | 792 |
satisfy $\pair{\emptyset;\emptyset}=\emptyset$. |
104 | 793 |
|
317 | 794 |
The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} |
795 |
assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form |
|
796 |
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \tdx{SigmaE2} |
|
104 | 797 |
merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and |
798 |
$b\in B(a)$. |
|
799 |
||
1449 | 800 |
In addition, it is possible to use tuples as patterns in abstractions: |
801 |
\begin{center} |
|
802 |
{\tt\%<$x$,$y$>.$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)} |
|
803 |
\end{center} |
|
804 |
Nested patterns are translated recursively: |
|
805 |
{\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$ |
|
806 |
{\tt split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$ |
|
807 |
$z$.$t$))}. The reverse translation is performed upon printing. |
|
808 |
\begin{warn} |
|
809 |
The translation between patterns and {\tt split} is performed automatically |
|
810 |
by the parser and printer. Thus the internal and external form of a term |
|
811 |
may differ, whichs affects proofs. For example the term {\tt |
|
812 |
(\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to |
|
813 |
{\tt<b,a>}. |
|
814 |
\end{warn} |
|
815 |
In addition to explicit $\lambda$-abstractions, patterns can be used in any |
|
816 |
variable binding construct which is internally described by a |
|
817 |
$\lambda$-abstraction. Some important examples are |
|
818 |
\begin{description} |
|
819 |
\item[Let:] {\tt let {\it pattern} = $t$ in $u$} |
|
820 |
\item[Choice:] {\tt THE~{\it pattern}~.~$P$} |
|
821 |
\item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$} |
|
822 |
\item[Comprehension:] {\tt \{~{\it pattern}:$A$~.~$P$~\}} |
|
823 |
\end{description} |
|
824 |
||
104 | 825 |
|
826 |
%%% domrange.ML |
|
827 |
||
828 |
\begin{figure} |
|
829 |
\begin{ttbox} |
|
317 | 830 |
\tdx{domainI} <a,b>: r ==> a : domain(r) |
831 |
\tdx{domainE} [| a : domain(r); !!y. <a,y>: r ==> P |] ==> P |
|
832 |
\tdx{domain_subset} domain(Sigma(A,B)) <= A |
|
104 | 833 |
|
317 | 834 |
\tdx{rangeI} <a,b>: r ==> b : range(r) |
835 |
\tdx{rangeE} [| b : range(r); !!x. <x,b>: r ==> P |] ==> P |
|
836 |
\tdx{range_subset} range(A*B) <= B |
|
104 | 837 |
|
317 | 838 |
\tdx{fieldI1} <a,b>: r ==> a : field(r) |
839 |
\tdx{fieldI2} <a,b>: r ==> b : field(r) |
|
840 |
\tdx{fieldCI} (~ <c,a>:r ==> <a,b>: r) ==> a : field(r) |
|
104 | 841 |
|
317 | 842 |
\tdx{fieldE} [| a : field(r); |
104 | 843 |
!!x. <a,x>: r ==> P; |
844 |
!!x. <x,a>: r ==> P |
|
845 |
|] ==> P |
|
846 |
||
317 | 847 |
\tdx{field_subset} field(A*A) <= A |
848 |
\end{ttbox} |
|
849 |
\caption{Domain, range and field of a relation} \label{zf-domrange} |
|
850 |
\end{figure} |
|
104 | 851 |
|
317 | 852 |
\begin{figure} |
853 |
\begin{ttbox} |
|
854 |
\tdx{imageI} [| <a,b>: r; a:A |] ==> b : r``A |
|
855 |
\tdx{imageE} [| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P |
|
856 |
||
857 |
\tdx{vimageI} [| <a,b>: r; b:B |] ==> a : r-``B |
|
858 |
\tdx{vimageE} [| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P |
|
104 | 859 |
\end{ttbox} |
317 | 860 |
\caption{Image and inverse image} \label{zf-domrange2} |
104 | 861 |
\end{figure} |
862 |
||
863 |
||
864 |
\subsection{Relations} |
|
317 | 865 |
Figure~\ref{zf-domrange} presents rules involving relations, which are sets |
104 | 866 |
of ordered pairs. The converse of a relation~$r$ is the set of all pairs |
867 |
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then |
|
317 | 868 |
{\cdx{converse}$(r)$} is its inverse. The rules for the domain |
343 | 869 |
operation, namely \tdx{domainI} and~\tdx{domainE}, assert that |
870 |
\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains |
|
104 | 871 |
some pair of the form~$\pair{x,y}$. The range operation is similar, and |
317 | 872 |
the field of a relation is merely the union of its domain and range. |
873 |
||
874 |
Figure~\ref{zf-domrange2} presents rules for images and inverse images. |
|
343 | 875 |
Note that these operations are generalisations of range and domain, |
317 | 876 |
respectively. See the file {\tt ZF/domrange.ML} for derivations of the |
877 |
rules. |
|
104 | 878 |
|
879 |
||
880 |
%%% func.ML |
|
881 |
||
882 |
\begin{figure} |
|
883 |
\begin{ttbox} |
|
317 | 884 |
\tdx{fun_is_rel} f: Pi(A,B) ==> f <= Sigma(A,B) |
104 | 885 |
|
317 | 886 |
\tdx{apply_equality} [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b |
887 |
\tdx{apply_equality2} [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c |
|
104 | 888 |
|
317 | 889 |
\tdx{apply_type} [| f: Pi(A,B); a:A |] ==> f`a : B(a) |
890 |
\tdx{apply_Pair} [| f: Pi(A,B); a:A |] ==> <a,f`a>: f |
|
891 |
\tdx{apply_iff} f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b |
|
104 | 892 |
|
317 | 893 |
\tdx{fun_extension} [| f : Pi(A,B); g: Pi(A,D); |
104 | 894 |
!!x. x:A ==> f`x = g`x |] ==> f=g |
895 |
||
317 | 896 |
\tdx{domain_type} [| <a,b> : f; f: Pi(A,B) |] ==> a : A |
897 |
\tdx{range_type} [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a) |
|
104 | 898 |
|
317 | 899 |
\tdx{Pi_type} [| f: A->C; !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B) |
900 |
\tdx{domain_of_fun} f: Pi(A,B) ==> domain(f)=A |
|
901 |
\tdx{range_of_fun} f: Pi(A,B) ==> f: A->range(f) |
|
104 | 902 |
|
317 | 903 |
\tdx{restrict} a : A ==> restrict(f,A) ` a = f`a |
904 |
\tdx{restrict_type} [| !!x. x:A ==> f`x: B(x) |] ==> |
|
905 |
restrict(f,A) : Pi(A,B) |
|
104 | 906 |
\end{ttbox} |
317 | 907 |
\caption{Functions} \label{zf-func1} |
104 | 908 |
\end{figure} |
909 |
||
910 |
||
911 |
\begin{figure} |
|
912 |
\begin{ttbox} |
|
317 | 913 |
\tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x)) |
914 |
\tdx{lamE} [| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P |
|
915 |
|] ==> P |
|
916 |
||
917 |
\tdx{lam_type} [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B) |
|
104 | 918 |
|
317 | 919 |
\tdx{beta} a : A ==> (lam x:A.b(x)) ` a = b(a) |
920 |
\tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f |
|
921 |
\end{ttbox} |
|
922 |
\caption{$\lambda$-abstraction} \label{zf-lam} |
|
923 |
\end{figure} |
|
924 |
||
925 |
||
926 |
\begin{figure} |
|
927 |
\begin{ttbox} |
|
928 |
\tdx{fun_empty} 0: 0->0 |
|
929 |
\tdx{fun_single} \{<a,b>\} : \{a\} -> \{b\} |
|
930 |
||
931 |
\tdx{fun_disjoint_Un} [| f: A->B; g: C->D; A Int C = 0 |] ==> |
|
104 | 932 |
(f Un g) : (A Un C) -> (B Un D) |
933 |
||
317 | 934 |
\tdx{fun_disjoint_apply1} [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> |
104 | 935 |
(f Un g)`a = f`a |
936 |
||
317 | 937 |
\tdx{fun_disjoint_apply2} [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> |
104 | 938 |
(f Un g)`c = g`c |
939 |
\end{ttbox} |
|
317 | 940 |
\caption{Constructing functions from smaller sets} \label{zf-func2} |
104 | 941 |
\end{figure} |
942 |
||
943 |
||
944 |
\subsection{Functions} |
|
945 |
Functions, represented by graphs, are notoriously difficult to reason |
|
317 | 946 |
about. The file {\tt ZF/func.ML} derives many rules, which overlap more |
947 |
than they ought. This section presents the more important rules. |
|
104 | 948 |
|
317 | 949 |
Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$, |
104 | 950 |
the generalized function space. For example, if $f$ is a function and |
317 | 951 |
$\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}). Two functions |
104 | 952 |
are equal provided they have equal domains and deliver equals results |
317 | 953 |
(\tdx{fun_extension}). |
104 | 954 |
|
317 | 955 |
By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be |
104 | 956 |
refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable |
317 | 957 |
family of sets $\{B(x)\}@{x\in A}$. Conversely, by \tdx{range_of_fun}, |
104 | 958 |
any dependent typing can be flattened to yield a function type of the form |
959 |
$A\to C$; here, $C={\tt range}(f)$. |
|
960 |
||
317 | 961 |
Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE} |
962 |
describe the graph of the generated function, while \tdx{beta} and |
|
963 |
\tdx{eta} are the standard conversions. We essentially have a |
|
964 |
dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}). |
|
104 | 965 |
|
317 | 966 |
Figure~\ref{zf-func2} presents some rules that can be used to construct |
104 | 967 |
functions explicitly. We start with functions consisting of at most one |
968 |
pair, and may form the union of two functions provided their domains are |
|
969 |
disjoint. |
|
970 |
||
971 |
||
972 |
\begin{figure} |
|
973 |
\begin{ttbox} |
|
317 | 974 |
\tdx{Int_absorb} A Int A = A |
975 |
\tdx{Int_commute} A Int B = B Int A |
|
976 |
\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) |
|
977 |
\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) |
|
104 | 978 |
|
317 | 979 |
\tdx{Un_absorb} A Un A = A |
980 |
\tdx{Un_commute} A Un B = B Un A |
|
981 |
\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) |
|
982 |
\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) |
|
104 | 983 |
|
317 | 984 |
\tdx{Diff_cancel} A-A = 0 |
985 |
\tdx{Diff_disjoint} A Int (B-A) = 0 |
|
986 |
\tdx{Diff_partition} A<=B ==> A Un (B-A) = B |
|
987 |
\tdx{double_complement} [| A<=B; B<= C |] ==> (B - (C-A)) = A |
|
988 |
\tdx{Diff_Un} A - (B Un C) = (A-B) Int (A-C) |
|
989 |
\tdx{Diff_Int} A - (B Int C) = (A-B) Un (A-C) |
|
104 | 990 |
|
317 | 991 |
\tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) |
992 |
\tdx{Inter_Un_distrib} [| a:A; b:B |] ==> |
|
104 | 993 |
Inter(A Un B) = Inter(A) Int Inter(B) |
994 |
||
317 | 995 |
\tdx{Int_Union_RepFun} A Int Union(B) = (UN C:B. A Int C) |
104 | 996 |
|
317 | 997 |
\tdx{Un_Inter_RepFun} b:B ==> |
104 | 998 |
A Un Inter(B) = (INT C:B. A Un C) |
999 |
||
317 | 1000 |
\tdx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) = |
104 | 1001 |
(SUM x:A. C(x)) Un (SUM x:B. C(x)) |
1002 |
||
317 | 1003 |
\tdx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) = |
104 | 1004 |
(SUM x:C. A(x)) Un (SUM x:C. B(x)) |
1005 |
||
317 | 1006 |
\tdx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) = |
104 | 1007 |
(SUM x:A. C(x)) Int (SUM x:B. C(x)) |
1008 |
||
317 | 1009 |
\tdx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) = |
104 | 1010 |
(SUM x:C. A(x)) Int (SUM x:C. B(x)) |
1011 |
\end{ttbox} |
|
1012 |
\caption{Equalities} \label{zf-equalities} |
|
1013 |
\end{figure} |
|
1014 |
||
111 | 1015 |
|
1016 |
\begin{figure} |
|
317 | 1017 |
%\begin{constants} |
1018 |
% \cdx{1} & $i$ & & $\{\emptyset\}$ \\ |
|
1019 |
% \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ |
|
1020 |
% \cdx{cond} & $[i,i,i]\To i$ & & conditional for {\tt bool} \\ |
|
1021 |
% \cdx{not} & $i\To i$ & & negation for {\tt bool} \\ |
|
1022 |
% \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for {\tt bool} \\ |
|
1023 |
% \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} |
|
1025 |
%\end{constants} |
|
1026 |
% |
|
111 | 1027 |
\begin{ttbox} |
317 | 1028 |
\tdx{bool_def} bool == \{0,1\} |
1029 |
\tdx{cond_def} cond(b,c,d) == if(b=1,c,d) |
|
1030 |
\tdx{not_def} not(b) == cond(b,0,1) |
|
1031 |
\tdx{and_def} a and b == cond(a,b,0) |
|
1032 |
\tdx{or_def} a or b == cond(a,1,b) |
|
1033 |
\tdx{xor_def} a xor b == cond(a,not(b),b) |
|
1034 |
||
1035 |
\tdx{bool_1I} 1 : bool |
|
1036 |
\tdx{bool_0I} 0 : bool |
|
1037 |
\tdx{boolE} [| c: bool; c=1 ==> P; c=0 ==> P |] ==> P |
|
1038 |
\tdx{cond_1} cond(1,c,d) = c |
|
1039 |
\tdx{cond_0} cond(0,c,d) = d |
|
1040 |
\end{ttbox} |
|
1041 |
\caption{The booleans} \label{zf-bool} |
|
1042 |
\end{figure} |
|
1043 |
||
1044 |
||
1045 |
\section{Further developments} |
|
1046 |
The next group of developments is complex and extensive, and only |
|
1047 |
highlights can be covered here. It involves many theories and ML files of |
|
1048 |
proofs. |
|
1049 |
||
1050 |
Figure~\ref{zf-equalities} presents commutative, associative, distributive, |
|
1051 |
and idempotency laws of union and intersection, along with other equations. |
|
1052 |
See file {\tt ZF/equalities.ML}. |
|
1053 |
||
1054 |
Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the |
|
1055 |
usual operators including a conditional (Fig.\ts\ref{zf-bool}). Although |
|
1056 |
{\ZF} is a first-order theory, you can obtain the effect of higher-order |
|
1057 |
logic using {\tt bool}-valued functions, for example. The constant~{\tt1} |
|
1058 |
is translated to {\tt succ(0)}. |
|
1059 |
||
1060 |
\begin{figure} |
|
1061 |
\index{*"+ symbol} |
|
1062 |
\begin{constants} |
|
343 | 1063 |
\it symbol & \it meta-type & \it priority & \it description \\ |
317 | 1064 |
\tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ |
1065 |
\cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ |
|
1066 |
\cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ |
|
1067 |
\end{constants} |
|
1068 |
\begin{ttbox} |
|
1069 |
\tdx{sum_def} A+B == \{0\}*A Un \{1\}*B |
|
1070 |
\tdx{Inl_def} Inl(a) == <0,a> |
|
1071 |
\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) |
|
1073 |
||
1074 |
\tdx{sum_InlI} a : A ==> Inl(a) : A+B |
|
1075 |
\tdx{sum_InrI} b : B ==> Inr(b) : A+B |
|
1076 |
||
1077 |
\tdx{Inl_inject} Inl(a)=Inl(b) ==> a=b |
|
1078 |
\tdx{Inr_inject} Inr(a)=Inr(b) ==> a=b |
|
1079 |
\tdx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P |
|
1080 |
||
1081 |
\tdx{sumE2} u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y)) |
|
1082 |
||
1083 |
\tdx{case_Inl} case(c,d,Inl(a)) = c(a) |
|
1084 |
\tdx{case_Inr} case(c,d,Inr(b)) = d(b) |
|
1085 |
\end{ttbox} |
|
1086 |
\caption{Disjoint unions} \label{zf-sum} |
|
1087 |
\end{figure} |
|
1088 |
||
1089 |
||
1090 |
Theory \thydx{Sum} defines the disjoint union of two sets, with |
|
1091 |
injections and a case analysis operator (Fig.\ts\ref{zf-sum}). Disjoint |
|
1092 |
unions play a role in datatype definitions, particularly when there is |
|
1093 |
mutual recursion~\cite{paulson-set-II}. |
|
1094 |
||
1095 |
\begin{figure} |
|
1096 |
\begin{ttbox} |
|
1097 |
\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) |
|
1099 |
\tdx{qfsplit_def} qfsplit(R,z) == EX x y. z=<x;y> & R(x,y) |
|
461 | 1100 |
\tdx{qconverse_def} qconverse(r) == \{z. w:r, EX x y. w=<x;y> & z=<y;x>\} |
1101 |
\tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). \{<x;y>\} |
|
317 | 1102 |
|
1103 |
\tdx{qsum_def} A <+> B == (\{0\} <*> A) Un (\{1\} <*> B) |
|
1104 |
\tdx{QInl_def} QInl(a) == <0;a> |
|
1105 |
\tdx{QInr_def} QInr(b) == <1;b> |
|
1106 |
\tdx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) |
|
1107 |
\end{ttbox} |
|
1108 |
\caption{Non-standard pairs, products and sums} \label{zf-qpair} |
|
1109 |
\end{figure} |
|
1110 |
||
1111 |
Theory \thydx{QPair} defines a notion of ordered pair that admits |
|
1112 |
non-well-founded tupling (Fig.\ts\ref{zf-qpair}). Such pairs are written |
|
1113 |
{\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the |
|
1114 |
converse operator \cdx{qconverse}, and the summation operator |
|
1115 |
\cdx{QSigma}. These are completely analogous to the corresponding |
|
1116 |
versions for standard ordered pairs. The theory goes on to define a |
|
1117 |
non-standard notion of disjoint sum using non-standard pairs. All of these |
|
1118 |
concepts satisfy the same properties as their standard counterparts; in |
|
1119 |
addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive |
|
1120 |
definitions, for example of infinite lists~\cite{paulson-final}. |
|
1121 |
||
1122 |
\begin{figure} |
|
1123 |
\begin{ttbox} |
|
1124 |
\tdx{bnd_mono_def} bnd_mono(D,h) == |
|
111 | 1125 |
h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X)) |
1126 |
||
461 | 1127 |
\tdx{lfp_def} lfp(D,h) == Inter(\{X: Pow(D). h(X) <= X\}) |
1128 |
\tdx{gfp_def} gfp(D,h) == Union(\{X: Pow(D). X <= h(X)\}) |
|
317 | 1129 |
|
111 | 1130 |
|
317 | 1131 |
\tdx{lfp_lowerbound} [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A |
111 | 1132 |
|
317 | 1133 |
\tdx{lfp_subset} lfp(D,h) <= D |
111 | 1134 |
|
317 | 1135 |
\tdx{lfp_greatest} [| bnd_mono(D,h); |
111 | 1136 |
!!X. [| h(X) <= X; X<=D |] ==> A<=X |
1137 |
|] ==> A <= lfp(D,h) |
|
1138 |
||
317 | 1139 |
\tdx{lfp_Tarski} bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) |
111 | 1140 |
|
317 | 1141 |
\tdx{induct} [| a : lfp(D,h); bnd_mono(D,h); |
111 | 1142 |
!!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |
1143 |
|] ==> P(a) |
|
1144 |
||
317 | 1145 |
\tdx{lfp_mono} [| bnd_mono(D,h); bnd_mono(E,i); |
111 | 1146 |
!!X. X<=D ==> h(X) <= i(X) |
1147 |
|] ==> lfp(D,h) <= lfp(E,i) |
|
1148 |
||
317 | 1149 |
\tdx{gfp_upperbound} [| A <= h(A); A<=D |] ==> A <= gfp(D,h) |
111 | 1150 |
|
317 | 1151 |
\tdx{gfp_subset} gfp(D,h) <= D |
111 | 1152 |
|
317 | 1153 |
\tdx{gfp_least} [| bnd_mono(D,h); |
111 | 1154 |
!!X. [| X <= h(X); X<=D |] ==> X<=A |
1155 |
|] ==> gfp(D,h) <= A |
|
1156 |
||
317 | 1157 |
\tdx{gfp_Tarski} bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) |
111 | 1158 |
|
317 | 1159 |
\tdx{coinduct} [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |
111 | 1160 |
|] ==> a : gfp(D,h) |
1161 |
||
317 | 1162 |
\tdx{gfp_mono} [| bnd_mono(D,h); D <= E; |
111 | 1163 |
!!X. X<=D ==> h(X) <= i(X) |
1164 |
|] ==> gfp(D,h) <= gfp(E,i) |
|
1165 |
\end{ttbox} |
|
1166 |
\caption{Least and greatest fixedpoints} \label{zf-fixedpt} |
|
1167 |
\end{figure} |
|
1168 |
||
317 | 1169 |
The Knaster-Tarski Theorem states that every monotone function over a |
1170 |
complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the |
|
1171 |
Theorem only for a particular lattice, namely the lattice of subsets of a |
|
1172 |
set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest |
|
1173 |
fixedpoint operators with corresponding induction and coinduction rules. |
|
1174 |
These are essential to many definitions that follow, including the natural |
|
1175 |
numbers and the transitive closure operator. The (co)inductive definition |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1176 |
package also uses the fixedpoint operators~\cite{paulson-CADE}. See |
317 | 1177 |
Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski |
1178 |
Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle |
|
1179 |
proofs. |
|
1180 |
||
1181 |
Monotonicity properties are proved for most of the set-forming operations: |
|
1182 |
union, intersection, Cartesian product, image, domain, range, etc. These |
|
1183 |
are useful for applying the Knaster-Tarski Fixedpoint Theorem. The proofs |
|
1184 |
themselves are trivial applications of Isabelle's classical reasoner. See |
|
1185 |
file {\tt ZF/mono.ML}. |
|
1186 |
||
111 | 1187 |
|
104 | 1188 |
\begin{figure} |
317 | 1189 |
\begin{constants} |
1190 |
\it symbol & \it meta-type & \it priority & \it description \\ |
|
1191 |
\sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ |
|
349 | 1192 |
\cdx{id} & $i\To i$ & & identity function \\ |
317 | 1193 |
\cdx{inj} & $[i,i]\To i$ & & injective function space\\ |
1194 |
\cdx{surj} & $[i,i]\To i$ & & surjective function space\\ |
|
1195 |
\cdx{bij} & $[i,i]\To i$ & & bijective function space |
|
1196 |
\end{constants} |
|
1197 |
||
104 | 1198 |
\begin{ttbox} |
317 | 1199 |
\tdx{comp_def} r O s == \{xz : domain(s)*range(r) . |
104 | 1200 |
EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\} |
317 | 1201 |
\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\} |
|
1203 |
\tdx{surj_def} surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\} |
|
1204 |
\tdx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B) |
|
104 | 1205 |
|
317 | 1206 |
|
1207 |
\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) |] ==> |
|
104 | 1209 |
f`(converse(f)`b) = b |
1210 |
||
317 | 1211 |
\tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A) |
1212 |
\tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A) |
|
104 | 1213 |
|
317 | 1214 |
\tdx{comp_type} [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C |
1215 |
\tdx{comp_assoc} (r O s) O t = r O (s O t) |
|
104 | 1216 |
|
317 | 1217 |
\tdx{left_comp_id} r<=A*B ==> id(B) O r = r |
1218 |
\tdx{right_comp_id} r<=A*B ==> r O id(A) = r |
|
104 | 1219 |
|
317 | 1220 |
\tdx{comp_func} [| g:A->B; f:B->C |] ==> (f O g):A->C |
1221 |
\tdx{comp_func_apply} [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a) |
|
104 | 1222 |
|
317 | 1223 |
\tdx{comp_inj} [| g:inj(A,B); f:inj(B,C) |] ==> (f O g):inj(A,C) |
1224 |
\tdx{comp_surj} [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C) |
|
1225 |
\tdx{comp_bij} [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C) |
|
104 | 1226 |
|
317 | 1227 |
\tdx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A) |
1228 |
\tdx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B) |
|
104 | 1229 |
|
317 | 1230 |
\tdx{bij_disjoint_Un} |
104 | 1231 |
[| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> |
1232 |
(f Un g) : bij(A Un C, B Un D) |
|
1233 |
||
317 | 1234 |
\tdx{restrict_bij} [| f:inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C) |
104 | 1235 |
\end{ttbox} |
1236 |
\caption{Permutations} \label{zf-perm} |
|
1237 |
\end{figure} |
|
1238 |
||
317 | 1239 |
The theory \thydx{Perm} is concerned with permutations (bijections) and |
1240 |
related concepts. These include composition of relations, the identity |
|
1241 |
relation, and three specialized function spaces: injective, surjective and |
|
1242 |
bijective. Figure~\ref{zf-perm} displays many of their properties that |
|
1243 |
have been proved. These results are fundamental to a treatment of |
|
1244 |
equipollence and cardinality. |
|
104 | 1245 |
|
1246 |
\begin{figure} |
|
317 | 1247 |
\index{#*@{\tt\#*} symbol} |
1248 |
\index{*div symbol} |
|
1249 |
\index{*mod symbol} |
|
1250 |
\index{#+@{\tt\#+} symbol} |
|
1251 |
\index{#-@{\tt\#-} symbol} |
|
1252 |
\begin{constants} |
|
1253 |
\it symbol & \it meta-type & \it priority & \it description \\ |
|
1254 |
\cdx{nat} & $i$ & & set of natural numbers \\ |
|
1255 |
\cdx{nat_case}& $[i,i\To i,i]\To i$ & & conditional for $nat$\\ |
|
1256 |
\cdx{rec} & $[i,i,[i,i]\To i]\To i$ & & recursor for $nat$\\ |
|
1257 |
\tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\ |
|
1258 |
\tt div & $[i,i]\To i$ & Left 70 & division\\ |
|
1259 |
\tt mod & $[i,i]\To i$ & Left 70 & modulus\\ |
|
1260 |
\tt \#+ & $[i,i]\To i$ & Left 65 & addition\\ |
|
1261 |
\tt \#- & $[i,i]\To i$ & Left 65 & subtraction |
|
1262 |
\end{constants} |
|
111 | 1263 |
|
317 | 1264 |
\begin{ttbox} |
1265 |
\tdx{nat_def} nat == lfp(lam r: Pow(Inf). \{0\} Un \{succ(x). x:r\} |
|
1266 |
||
1267 |
\tdx{nat_case_def} nat_case(a,b,k) == |
|
1268 |
THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x)) |
|
1269 |
||
1270 |
\tdx{rec_def} rec(k,a,b) == |
|
1271 |
transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n)) |
|
1272 |
||
1273 |
\tdx{add_def} m#+n == rec(m, n, \%u v.succ(v)) |
|
1274 |
\tdx{diff_def} m#-n == rec(n, m, \%u v. rec(v, 0, \%x y.x)) |
|
1275 |
\tdx{mult_def} m#*n == rec(m, 0, \%u v. n #+ v) |
|
1276 |
\tdx{mod_def} m mod n == transrec(m, \%j f. if(j:n, j, f`(j#-n))) |
|
1277 |
\tdx{div_def} m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#-n)))) |
|
111 | 1278 |
|
1279 |
||
317 | 1280 |
\tdx{nat_0I} 0 : nat |
1281 |
\tdx{nat_succI} n : nat ==> succ(n) : nat |
|
104 | 1282 |
|
317 | 1283 |
\tdx{nat_induct} |
104 | 1284 |
[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |
1285 |
|] ==> P(n) |
|
1286 |
||
317 | 1287 |
\tdx{nat_case_0} nat_case(a,b,0) = a |
1288 |
\tdx{nat_case_succ} nat_case(a,b,succ(m)) = b(m) |
|
104 | 1289 |
|
317 | 1290 |
\tdx{rec_0} rec(0,a,b) = a |
1291 |
\tdx{rec_succ} rec(succ(m),a,b) = b(m, rec(m,a,b)) |
|
104 | 1292 |
|
317 | 1293 |
\tdx{mult_type} [| m:nat; n:nat |] ==> m #* n : nat |
1294 |
\tdx{mult_0} 0 #* n = 0 |
|
1295 |
\tdx{mult_succ} succ(m) #* n = n #+ (m #* n) |
|
1296 |
\tdx{mult_commute} [| m:nat; n:nat |] ==> m #* n = n #* m |
|
1297 |
\tdx{add_mult_dist} |
|
104 | 1298 |
[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k) |
317 | 1299 |
\tdx{mult_assoc} |
104 | 1300 |
[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k) |
317 | 1301 |
\tdx{mod_quo_equality} |
104 | 1302 |
[| 0:n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m |
1303 |
\end{ttbox} |
|
1304 |
\caption{The natural numbers} \label{zf-nat} |
|
1305 |
\end{figure} |
|
1306 |
||
317 | 1307 |
Theory \thydx{Nat} defines the natural numbers and mathematical |
1308 |
induction, along with a case analysis operator. The set of natural |
|
1309 |
numbers, here called {\tt nat}, is known in set theory as the ordinal~$\omega$. |
|
1310 |
||
1311 |
Theory \thydx{Arith} defines primitive recursion and goes on to develop |
|
1312 |
arithmetic on the natural numbers (Fig.\ts\ref{zf-nat}). It defines |
|
1313 |
addition, multiplication, subtraction, division, and remainder. Many of |
|
1314 |
their properties are proved: commutative, associative and distributive |
|
1315 |
laws, identity and cancellation laws, etc. The most interesting result is |
|
1316 |
perhaps the theorem $a \bmod b + (a/b)\times b = a$. Division and |
|
1317 |
remainder are defined by repeated subtraction, which requires well-founded |
|
1318 |
rather than primitive recursion; the termination argument relies on the |
|
1319 |
divisor's being non-zero. |
|
1320 |
||
1321 |
Theory \thydx{Univ} defines a `universe' ${\tt univ}(A)$, for |
|
1322 |
constructing datatypes such as trees. This set contains $A$ and the |
|
1323 |
natural numbers. Vitally, it is closed under finite products: ${\tt |
|
1324 |
univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$. This theory also |
|
1325 |
defines the cumulative hierarchy of axiomatic set theory, which |
|
1326 |
traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The |
|
1327 |
`universe' is a simple generalization of~$V@\omega$. |
|
1328 |
||
1329 |
Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, for |
|
1330 |
constructing codatatypes such as streams. It is analogous to ${\tt |
|
1331 |
univ}(A)$ (and is defined in terms of it) but is closed under the |
|
1332 |
non-standard product and sum. |
|
1333 |
||
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1334 |
Theory {\tt Finite} (Figure~\ref{zf-fin}) defines the finite set operator; |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1335 |
${\tt Fin}(A)$ is the set of all finite sets over~$A$. The theory employs |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1336 |
Isabelle's inductive definition package, which proves various rules |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1337 |
automatically. The induction rule shown is stronger than the one proved by |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1338 |
the package. The theory also defines the set of all finite functions |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1339 |
between two given sets. |
317 | 1340 |
|
111 | 1341 |
\begin{figure} |
1342 |
\begin{ttbox} |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1343 |
\tdx{Fin.emptyI} 0 : Fin(A) |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1344 |
\tdx{Fin.consI} [| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A) |
111 | 1345 |
|
317 | 1346 |
\tdx{Fin_induct} |
111 | 1347 |
[| b: Fin(A); |
1348 |
P(0); |
|
1349 |
!!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) |
|
1350 |
|] ==> P(b) |
|
1351 |
||
317 | 1352 |
\tdx{Fin_mono} A<=B ==> Fin(A) <= Fin(B) |
1353 |
\tdx{Fin_UnI} [| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A) |
|
1354 |
\tdx{Fin_UnionI} C : Fin(Fin(A)) ==> Union(C) : Fin(A) |
|
1355 |
\tdx{Fin_subset} [| c<=b; b: Fin(A) |] ==> c: Fin(A) |
|
111 | 1356 |
\end{ttbox} |
1357 |
\caption{The finite set operator} \label{zf-fin} |
|
1358 |
\end{figure} |
|
1359 |
||
317 | 1360 |
\begin{figure} |
1361 |
\begin{constants} |
|
1362 |
\cdx{list} & $i\To i$ && lists over some set\\ |
|
1363 |
\cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\ |
|
1364 |
\cdx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ && recursor for $list(A)$ \\ |
|
1365 |
\cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\ |
|
1366 |
\cdx{length} & $i\To i$ & & length of a list\\ |
|
1367 |
\cdx{rev} & $i\To i$ & & reverse of a list\\ |
|
1368 |
\tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ |
|
1369 |
\cdx{flat} & $i\To i$ & & append of list of lists |
|
1370 |
\end{constants} |
|
1371 |
||
1372 |
\underscoreon %%because @ is used here |
|
104 | 1373 |
\begin{ttbox} |
317 | 1374 |
\tdx{list_rec_def} list_rec(l,c,h) == |
287 | 1375 |
Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l)) |
104 | 1376 |
|
317 | 1377 |
\tdx{map_def} map(f,l) == list_rec(l, 0, \%x xs r. <f(x), r>) |
1378 |
\tdx{length_def} length(l) == list_rec(l, 0, \%x xs r. succ(r)) |
|
1379 |
\tdx{app_def} xs@ys == list_rec(xs, ys, \%x xs r. <x,r>) |
|
1380 |
\tdx{rev_def} rev(l) == list_rec(l, 0, \%x xs r. r @ <x,0>) |
|
1381 |
\tdx{flat_def} flat(ls) == list_rec(ls, 0, \%l ls r. l @ r) |
|
104 | 1382 |
|
1383 |
||
317 | 1384 |
\tdx{NilI} Nil : list(A) |
1385 |
\tdx{ConsI} [| a: A; l: list(A) |] ==> Cons(a,l) : list(A) |
|
1386 |
||
1387 |
\tdx{List.induct} |
|
104 | 1388 |
[| l: list(A); |
111 | 1389 |
P(Nil); |
1390 |
!!x y. [| x: A; y: list(A); P(y) |] ==> P(Cons(x,y)) |
|
104 | 1391 |
|] ==> P(l) |
1392 |
||
317 | 1393 |
\tdx{Cons_iff} Cons(a,l)=Cons(a',l') <-> a=a' & l=l' |
1394 |
\tdx{Nil_Cons_iff} ~ Nil=Cons(a,l) |
|
104 | 1395 |
|
317 | 1396 |
\tdx{list_mono} A<=B ==> list(A) <= list(B) |
111 | 1397 |
|
317 | 1398 |
\tdx{list_rec_Nil} list_rec(Nil,c,h) = c |
1399 |
\tdx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h)) |
|
104 | 1400 |
|
317 | 1401 |
\tdx{map_ident} l: list(A) ==> map(\%u.u, l) = l |
1402 |
\tdx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l) |
|
1403 |
\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys) |
|
1404 |
\tdx{map_type} |
|
104 | 1405 |
[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B) |
317 | 1406 |
\tdx{map_flat} |
104 | 1407 |
ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) |
1408 |
\end{ttbox} |
|
1409 |
\caption{Lists} \label{zf-list} |
|
1410 |
\end{figure} |
|
1411 |
||
111 | 1412 |
|
1413 |
Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$. |
|
1414 |
The definition employs Isabelle's datatype package, which defines the |
|
1415 |
introduction and induction rules automatically, as well as the constructors |
|
343 | 1416 |
and case operator (\verb|list_case|). See file {\tt ZF/List.ML}. |
1417 |
The file {\tt ZF/ListFn.thy} proceeds to define structural |
|
111 | 1418 |
recursion and the usual list functions. |
104 | 1419 |
|
1420 |
The constructions of the natural numbers and lists make use of a suite of |
|
317 | 1421 |
operators for handling recursive function definitions. I have described |
1422 |
the developments in detail elsewhere~\cite{paulson-set-II}. Here is a brief |
|
1423 |
summary: |
|
1424 |
\begin{itemize} |
|
1425 |
\item Theory {\tt Trancl} defines the transitive closure of a relation |
|
1426 |
(as a least fixedpoint). |
|
104 | 1427 |
|
317 | 1428 |
\item Theory {\tt WF} proves the Well-Founded Recursion Theorem, using an |
1429 |
elegant approach of Tobias Nipkow. This theorem permits general |
|
1430 |
recursive definitions within set theory. |
|
1431 |
||
1432 |
\item Theory {\tt Ord} defines the notions of transitive set and ordinal |
|
1433 |
number. It derives transfinite induction. A key definition is {\bf |
|
1434 |
less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and |
|
1435 |
$i\in j$. As a special case, it includes less than on the natural |
|
1436 |
numbers. |
|
104 | 1437 |
|
317 | 1438 |
\item Theory {\tt Epsilon} derives $\epsilon$-induction and |
343 | 1439 |
$\epsilon$-recursion, which are generalisations of transfinite |
1440 |
induction and recursion. It also defines \cdx{rank}$(x)$, which is the |
|
1441 |
least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ |
|
1442 |
of the cumulative hierarchy (thus $x\in V@{\alpha+1}$). |
|
317 | 1443 |
\end{itemize} |
1444 |
||
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1445 |
Other important theories lead to a theory of cardinal numbers. They have |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1446 |
not yet been written up anywhere. Here is a summary: |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1447 |
\begin{itemize} |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1448 |
\item Theory {\tt Rel} defines the basic properties of relations, such as |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1449 |
(ir)reflexivity, (a)symmetry, and transitivity. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1450 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1451 |
\item Theory {\tt EquivClass} develops a theory of equivalence |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1452 |
classes, not using the Axiom of Choice. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1453 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1454 |
\item Theory {\tt Order} defines partial orderings, total orderings and |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1455 |
wellorderings. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1456 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1457 |
\item Theory {\tt OrderArith} defines orderings on sum and product sets. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1458 |
These can be used to define ordinal arithmetic and have applications to |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1459 |
cardinal arithmetic. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1460 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1461 |
\item Theory {\tt OrderType} defines order types. Every wellordering is |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1462 |
equivalent to a unique ordinal, which is its order type. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1463 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1464 |
\item Theory {\tt Cardinal} defines equipollence and cardinal numbers. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1465 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1466 |
\item Theory {\tt CardinalArith} defines cardinal addition and |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1467 |
multiplication, and proves their elementary laws. It proves that there |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1468 |
is no greatest cardinal. It also proves a deep result, namely |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1469 |
$\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1470 |
Kunen~\cite[page 29]{kunen80}. None of these results assume the Axiom of |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1471 |
Choice, which complicates their proofs considerably. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1472 |
\end{itemize} |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1473 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1474 |
The following developments involve the Axiom of Choice (AC): |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1475 |
\begin{itemize} |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1476 |
\item Theory {\tt AC} asserts the Axiom of Choice and proves some simple |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1477 |
equivalent forms. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1478 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1479 |
\item Theory {\tt Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1480 |
and the Wellordering Theorem, following Abrial and |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1481 |
Laffitte~\cite{abrial93}. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1482 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1483 |
\item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1484 |
the cardinals. It also proves a theorem needed to justify |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1485 |
infinitely branching datatype declarations: if $\kappa$ is an infinite |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1486 |
cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1487 |
$|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1488 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1489 |
\item Theory {\tt InfDatatype} proves theorems to justify infinitely |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1490 |
branching datatypes. Arbitrary index sets are allowed, provided their |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1491 |
cardinalities have an upper bound. The theory also justifies some |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1492 |
unusual cases of finite branching, involving the finite powerset operator |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1493 |
and the finite function space operator. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1494 |
\end{itemize} |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1495 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1496 |
|
104 | 1497 |
|
317 | 1498 |
\section{Simplification rules} |
1499 |
{\ZF} does not merely inherit simplification from \FOL, but modifies it |
|
1500 |
extensively. File {\tt ZF/simpdata.ML} contains the details. |
|
1501 |
||
1502 |
The extraction of rewrite rules takes set theory primitives into account. |
|
1503 |
It can strip bounded universal quantifiers from a formula; for example, |
|
1504 |
${\forall x\in A.f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp |
|
1505 |
f(x)=g(x)$. Given $a\in\{x\in A.P(x)\}$ it extracts rewrite rules from |
|
1506 |
$a\in A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in A-B$. |
|
1507 |
||
2495 | 1508 |
The default simplification set contains congruence rules for |
317 | 1509 |
all the binding operators of {\ZF}\@. It contains all the conversion |
1510 |
rules, such as {\tt fst} and {\tt snd}, as well as the rewrites |
|
2495 | 1511 |
shown in Fig.\ts\ref{zf-simpdata}. See the file |
1512 |
{\tt ZF/simpdata.ML} for a fuller list. |
|
104 | 1513 |
|
1514 |
\begin{figure} |
|
1515 |
\begin{eqnarray*} |
|
111 | 1516 |
a\in \emptyset & \bimp & \bot\\ |
1517 |
a \in A \union B & \bimp & a\in A \disj a\in B\\ |
|
1518 |
a \in A \inter B & \bimp & a\in A \conj a\in B\\ |
|
1519 |
a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\ |
|
104 | 1520 |
\pair{a,b}\in {\tt Sigma}(A,B) |
111 | 1521 |
& \bimp & a\in A \conj b\in B(a)\\ |
1522 |
a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\ |
|
343 | 1523 |
(\forall x \in \emptyset. P(x)) & \bimp & \top\\ |
111 | 1524 |
(\forall x \in A. \top) & \bimp & \top |
104 | 1525 |
\end{eqnarray*} |
2495 | 1526 |
\caption{Some rewrite rules for set theory} \label{zf-simpdata} |
104 | 1527 |
\end{figure} |
1528 |
||
1529 |
||
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1530 |
\section{The examples directories} |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1531 |
Directory {\tt HOL/IMP} contains a mechanised version of a semantic |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1532 |
equivalence proof taken from Winskel~\cite{winskel93}. It formalises the |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1533 |
denotational and operational semantics of a simple while-language, then |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1534 |
proves the two equivalent. It contains several datatype and inductive |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1535 |
definitions, and demonstrates their use. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1536 |
|
317 | 1537 |
The directory {\tt ZF/ex} contains further developments in {\ZF} set |
1538 |
theory. Here is an overview; see the files themselves for more details. I |
|
1539 |
describe much of this material in other |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1540 |
publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1541 |
\begin{itemize} |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1542 |
\item File {\tt misc.ML} contains miscellaneous examples such as |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1543 |
Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1544 |
of homomorphisms' challenge~\cite{boyer86}. |
104 | 1545 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1546 |
\item Theory {\tt Ramsey} proves the finite exponent 2 version of |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1547 |
Ramsey's Theorem, following Basin and Kaufmann's |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1548 |
presentation~\cite{basin91}. |
114 | 1549 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1550 |
\item Theory {\tt Integ} develops a theory of the integers as |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1551 |
equivalence classes of pairs of natural numbers. |
114 | 1552 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1553 |
\item Theory {\tt Bin} defines a datatype for two's complement binary |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1554 |
integers, then proves rewrite rules to perform binary arithmetic. For |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1555 |
instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds. |
104 | 1556 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1557 |
\item Theory {\tt BT} defines the recursive data structure ${\tt |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1558 |
bt}(A)$, labelled binary trees. |
104 | 1559 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1560 |
\item Theory {\tt Term} defines a recursive data structure for terms |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1561 |
and term lists. These are simply finite branching trees. |
104 | 1562 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1563 |
\item Theory {\tt TF} defines primitives for solving mutually |
114 | 1564 |
recursive equations over sets. It constructs sets of trees and forests |
1565 |
as an example, including induction and recursion rules that handle the |
|
1566 |
mutual recursion. |
|
1567 |
||
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1568 |
\item Theory {\tt Prop} proves soundness and completeness of |
343 | 1569 |
propositional logic~\cite{paulson-set-II}. This illustrates datatype |
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1570 |
definitions, inductive definitions, structural induction and rule |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1571 |
induction. |
114 | 1572 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1573 |
\item Theory {\tt ListN} inductively defines the lists of $n$ |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1574 |
elements~\cite{paulin92}. |
104 | 1575 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1576 |
\item Theory {\tt Acc} inductively defines the accessible part of a |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1577 |
relation~\cite{paulin92}. |
114 | 1578 |
|
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1579 |
\item Theory {\tt Comb} defines the datatype of combinators and |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1580 |
inductively defines contraction and parallel contraction. It goes on to |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1581 |
prove the Church-Rosser Theorem. This case study follows Camilleri and |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1582 |
Melham~\cite{camilleri92}. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1583 |
|
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1584 |
\item Theory {\tt LList} defines lazy lists and a coinduction |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1585 |
principle for proving equations between them. |
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset
|
1586 |
\end{itemize} |
104 | 1587 |
|
1588 |
||
317 | 1589 |
\section{A proof about powersets}\label{sec:ZF-pow-example} |
114 | 1590 |
To demonstrate high-level reasoning about subsets, let us prove the |
1591 |
equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$. Compared |
|
1592 |
with first-order logic, set theory involves a maze of rules, and theorems |
|
1593 |
have many different proofs. Attempting other proofs of the theorem might |
|
1594 |
be instructive. This proof exploits the lattice properties of |
|
1595 |
intersection. It also uses the monotonicity of the powerset operation, |
|
1596 |
from {\tt ZF/mono.ML}: |
|
104 | 1597 |
\begin{ttbox} |
317 | 1598 |
\tdx{Pow_mono} A<=B ==> Pow(A) <= Pow(B) |
104 | 1599 |
\end{ttbox} |
1600 |
We enter the goal and make the first step, which breaks the equation into |
|
317 | 1601 |
two inclusions by extensionality:\index{*equalityI theorem} |
104 | 1602 |
\begin{ttbox} |
2495 | 1603 |
goal thy "Pow(A Int B) = Pow(A) Int Pow(B)"; |
104 | 1604 |
{\out Level 0} |
1605 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1606 |
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} |
|
287 | 1607 |
\ttbreak |
104 | 1608 |
by (resolve_tac [equalityI] 1); |
1609 |
{\out Level 1} |
|
1610 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1611 |
{\out 1. Pow(A Int B) <= Pow(A) Int Pow(B)} |
|
1612 |
{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
1613 |
\end{ttbox} |
|
1614 |
Both inclusions could be tackled straightforwardly using {\tt subsetI}. |
|
1615 |
A shorter proof results from noting that intersection forms the greatest |
|
317 | 1616 |
lower bound:\index{*Int_greatest theorem} |
104 | 1617 |
\begin{ttbox} |
1618 |
by (resolve_tac [Int_greatest] 1); |
|
1619 |
{\out Level 2} |
|
1620 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1621 |
{\out 1. Pow(A Int B) <= Pow(A)} |
|
1622 |
{\out 2. Pow(A Int B) <= Pow(B)} |
|
1623 |
{\out 3. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
1624 |
\end{ttbox} |
|
1625 |
Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\inter |
|
1626 |
B\subseteq A$; subgoal~2 follows similarly: |
|
317 | 1627 |
\index{*Int_lower1 theorem}\index{*Int_lower2 theorem} |
104 | 1628 |
\begin{ttbox} |
1629 |
by (resolve_tac [Int_lower1 RS Pow_mono] 1); |
|
1630 |
{\out Level 3} |
|
1631 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1632 |
{\out 1. Pow(A Int B) <= Pow(B)} |
|
1633 |
{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
287 | 1634 |
\ttbreak |
104 | 1635 |
by (resolve_tac [Int_lower2 RS Pow_mono] 1); |
1636 |
{\out Level 4} |
|
1637 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1638 |
{\out 1. Pow(A) Int Pow(B) <= Pow(A Int B)} |
|
1639 |
\end{ttbox} |
|
1640 |
We are left with the opposite inclusion, which we tackle in the |
|
317 | 1641 |
straightforward way:\index{*subsetI theorem} |
104 | 1642 |
\begin{ttbox} |
1643 |
by (resolve_tac [subsetI] 1); |
|
1644 |
{\out Level 5} |
|
1645 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1646 |
{\out 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)} |
|
1647 |
\end{ttbox} |
|
1648 |
The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt |
|
287 | 1649 |
Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two |
317 | 1650 |
subgoals. The rule \tdx{IntE} treats the intersection like a conjunction |
287 | 1651 |
instead of unfolding its definition. |
104 | 1652 |
\begin{ttbox} |
1653 |
by (eresolve_tac [IntE] 1); |
|
1654 |
{\out Level 6} |
|
1655 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1656 |
{\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)} |
|
1657 |
\end{ttbox} |
|
1658 |
The next step replaces the {\tt Pow} by the subset |
|
317 | 1659 |
relation~($\subseteq$).\index{*PowI theorem} |
104 | 1660 |
\begin{ttbox} |
1661 |
by (resolve_tac [PowI] 1); |
|
1662 |
{\out Level 7} |
|
1663 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1664 |
{\out 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B} |
|
1665 |
\end{ttbox} |
|
287 | 1666 |
We perform the same replacement in the assumptions. This is a good |
317 | 1667 |
demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem} |
104 | 1668 |
\begin{ttbox} |
1669 |
by (REPEAT (dresolve_tac [PowD] 1)); |
|
1670 |
{\out Level 8} |
|
1671 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1672 |
{\out 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B} |
|
1673 |
\end{ttbox} |
|
287 | 1674 |
The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but |
317 | 1675 |
$A\inter B$ is the greatest lower bound:\index{*Int_greatest theorem} |
104 | 1676 |
\begin{ttbox} |
1677 |
by (resolve_tac [Int_greatest] 1); |
|
1678 |
{\out Level 9} |
|
1679 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1680 |
{\out 1. !!x. [| x <= A; x <= B |] ==> x <= A} |
|
1681 |
{\out 2. !!x. [| x <= A; x <= B |] ==> x <= B} |
|
287 | 1682 |
\end{ttbox} |
1683 |
To conclude the proof, we clear up the trivial subgoals: |
|
1684 |
\begin{ttbox} |
|
104 | 1685 |
by (REPEAT (assume_tac 1)); |
1686 |
{\out Level 10} |
|
1687 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1688 |
{\out No subgoals!} |
|
1689 |
\end{ttbox} |
|
287 | 1690 |
\medskip |
104 | 1691 |
We could have performed this proof in one step by applying |
2495 | 1692 |
\ttindex{Fast_tac}. Let us |
287 | 1693 |
go back to the start: |
104 | 1694 |
\begin{ttbox} |
1695 |
choplev 0; |
|
1696 |
{\out Level 0} |
|
1697 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1698 |
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)} |
|
287 | 1699 |
\end{ttbox} |
2495 | 1700 |
We must add \tdx{equalityI} as an introduction rule. |
1701 |
Extensionality is not used by default: many equalities can be proved |
|
287 | 1702 |
by rewriting. |
1703 |
\begin{ttbox} |
|
2495 | 1704 |
by (fast_tac (!claset addIs [equalityI]) 1); |
104 | 1705 |
{\out Level 1} |
1706 |
{\out Pow(A Int B) = Pow(A) Int Pow(B)} |
|
1707 |
{\out No subgoals!} |
|
1708 |
\end{ttbox} |
|
287 | 1709 |
In the past this was regarded as a difficult proof, as indeed it is if all |
1710 |
the symbols are replaced by their definitions. |
|
1711 |
\goodbreak |
|
104 | 1712 |
|
1713 |
\section{Monotonicity of the union operator} |
|
1714 |
For another example, we prove that general union is monotonic: |
|
1715 |
${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we |
|
317 | 1716 |
tackle the inclusion using \tdx{subsetI}: |
104 | 1717 |
\begin{ttbox} |
2495 | 1718 |
val [prem] = goal thy "C<=D ==> Union(C) <= Union(D)"; |
104 | 1719 |
{\out Level 0} |
1720 |
{\out Union(C) <= Union(D)} |
|
1721 |
{\out 1. Union(C) <= Union(D)} |
|
114 | 1722 |
{\out val prem = "C <= D [C <= D]" : thm} |
1723 |
\ttbreak |
|
104 | 1724 |
by (resolve_tac [subsetI] 1); |
1725 |
{\out Level 1} |
|
1726 |
{\out Union(C) <= Union(D)} |
|
1727 |
{\out 1. !!x. x : Union(C) ==> x : Union(D)} |
|
1728 |
\end{ttbox} |
|
1729 |
Big union is like an existential quantifier --- the occurrence in the |
|
1730 |
assumptions must be eliminated early, since it creates parameters. |
|
317 | 1731 |
\index{*UnionE theorem} |
104 | 1732 |
\begin{ttbox} |
1733 |
by (eresolve_tac [UnionE] 1); |
|
1734 |
{\out Level 2} |
|
1735 |
{\out Union(C) <= Union(D)} |
|
1736 |
{\out 1. !!x B. [| x : B; B : C |] ==> x : Union(D)} |
|
1737 |
\end{ttbox} |
|
317 | 1738 |
Now we may apply \tdx{UnionI}, which creates an unknown involving the |
104 | 1739 |
parameters. To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs |
1740 |
to some element, say~$\Var{B2}(x,B)$, of~$D$. |
|
1741 |
\begin{ttbox} |
|
1742 |
by (resolve_tac [UnionI] 1); |
|
1743 |
{\out Level 3} |
|
1744 |
{\out Union(C) <= Union(D)} |
|
1745 |
{\out 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D} |
|
1746 |
{\out 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)} |
|
1747 |
\end{ttbox} |
|
317 | 1748 |
Combining \tdx{subsetD} with the premise $C\subseteq D$ yields |
104 | 1749 |
$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1: |
1750 |
\begin{ttbox} |
|
1751 |
by (resolve_tac [prem RS subsetD] 1); |
|
1752 |
{\out Level 4} |
|
1753 |
{\out Union(C) <= Union(D)} |
|
1754 |
{\out 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C} |
|
1755 |
{\out 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)} |
|
1756 |
\end{ttbox} |
|
1757 |
The rest is routine. Note how~$\Var{B2}(x,B)$ is instantiated. |
|
1758 |
\begin{ttbox} |
|
1759 |
by (assume_tac 1); |
|
1760 |
{\out Level 5} |
|
1761 |
{\out Union(C) <= Union(D)} |
|
1762 |
{\out 1. !!x B. [| x : B; B : C |] ==> x : B} |
|
1763 |
by (assume_tac 1); |
|
1764 |
{\out Level 6} |
|
1765 |
{\out Union(C) <= Union(D)} |
|
1766 |
{\out No subgoals!} |
|
1767 |
\end{ttbox} |
|
2495 | 1768 |
Again, \ttindex{fast_tac} can prove the theorem in one |
104 | 1769 |
step, provided we somehow supply it with~{\tt prem}. We can either add |
1770 |
this premise to the assumptions using \ttindex{cut_facts_tac}, or add |
|
2495 | 1771 |
\hbox{\tt prem RS subsetD} to the claset as an introduction rule. |
104 | 1772 |
|
317 | 1773 |
The file {\tt ZF/equalities.ML} has many similar proofs. Reasoning about |
343 | 1774 |
general intersection can be difficult because of its anomalous behaviour on |
317 | 1775 |
the empty set. However, \ttindex{fast_tac} copes well with these. Here is |
1776 |
a typical example, borrowed from Devlin~\cite[page 12]{devlin79}: |
|
104 | 1777 |
\begin{ttbox} |
1778 |
a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x)) |
|
1779 |
\end{ttbox} |
|
1780 |
In traditional notation this is |
|
317 | 1781 |
\[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) = |
1782 |
\Bigl(\inter@{x\in C} A(x)\Bigr) \int |
|
1783 |
\Bigl(\inter@{x\in C} B(x)\Bigr) \] |
|
104 | 1784 |
|
1785 |
\section{Low-level reasoning about functions} |
|
1786 |
The derived rules {\tt lamI}, {\tt lamE}, {\tt lam_type}, {\tt beta} |
|
1787 |
and {\tt eta} support reasoning about functions in a |
|
1788 |
$\lambda$-calculus style. This is generally easier than regarding |
|
1789 |
functions as sets of ordered pairs. But sometimes we must look at the |
|
1790 |
underlying representation, as in the following proof |
|
317 | 1791 |
of~\tdx{fun_disjoint_apply1}. This states that if $f$ and~$g$ are |
104 | 1792 |
functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then |
287 | 1793 |
$(f\un g)`a = f`a$: |
104 | 1794 |
\begin{ttbox} |
2495 | 1795 |
val prems = goal thy |
104 | 1796 |
"[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback |
1797 |
\ttback (f Un g)`a = f`a"; |
|
1798 |
{\out Level 0} |
|
1799 |
{\out (f Un g) ` a = f ` a} |
|
1800 |
{\out 1. (f Un g) ` a = f ` a} |
|
287 | 1801 |
\end{ttbox} |
1802 |
Isabelle has produced the output above; the \ML{} top-level now echoes the |
|
1803 |
binding of {\tt prems}. |
|
1804 |
\begin{ttbox} |
|
114 | 1805 |
{\out val prems = ["a : A [a : A]",} |
1806 |
{\out "f : A -> B [f : A -> B]",} |
|
1807 |
{\out "g : C -> D [g : C -> D]",} |
|
1808 |
{\out "A Int C = 0 [A Int C = 0]"] : thm list} |
|
104 | 1809 |
\end{ttbox} |
317 | 1810 |
Using \tdx{apply_equality}, we reduce the equality to reasoning about |
287 | 1811 |
ordered pairs. The second subgoal is to verify that $f\un g$ is a function. |
104 | 1812 |
\begin{ttbox} |
1813 |
by (resolve_tac [apply_equality] 1); |
|
1814 |
{\out Level 1} |
|
1815 |
{\out (f Un g) ` a = f ` a} |
|
1816 |
{\out 1. <a,f ` a> : f Un g} |
|
1817 |
{\out 2. f Un g : (PROD x:?A. ?B(x))} |
|
1818 |
\end{ttbox} |
|
317 | 1819 |
We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we |
104 | 1820 |
choose~$f$: |
1821 |
\begin{ttbox} |
|
1822 |
by (resolve_tac [UnI1] 1); |
|
1823 |
{\out Level 2} |
|
1824 |
{\out (f Un g) ` a = f ` a} |
|
1825 |
{\out 1. <a,f ` a> : f} |
|
1826 |
{\out 2. f Un g : (PROD x:?A. ?B(x))} |
|
1827 |
\end{ttbox} |
|
317 | 1828 |
To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is |
1829 |
essentially the converse of \tdx{apply_equality}: |
|
104 | 1830 |
\begin{ttbox} |
1831 |
by (resolve_tac [apply_Pair] 1); |
|
1832 |
{\out Level 3} |
|
1833 |
{\out (f Un g) ` a = f ` a} |
|
1834 |
{\out 1. f : (PROD x:?A2. ?B2(x))} |
|
1835 |
{\out 2. a : ?A2} |
|
1836 |
{\out 3. f Un g : (PROD x:?A. ?B(x))} |
|
1837 |
\end{ttbox} |
|
1838 |
Using the premises $f\in A\to B$ and $a\in A$, we solve the two subgoals |
|
317 | 1839 |
from \tdx{apply_Pair}. Recall that a $\Pi$-set is merely a generalized |
104 | 1840 |
function space, and observe that~{\tt?A2} is instantiated to~{\tt A}. |
1841 |
\begin{ttbox} |
|
1842 |
by (resolve_tac prems 1); |
|
1843 |
{\out Level 4} |
|
1844 |
{\out (f Un g) ` a = f ` a} |
|
1845 |
{\out 1. a : A} |
|
1846 |
{\out 2. f Un g : (PROD x:?A. ?B(x))} |
|
1847 |
by (resolve_tac prems 1); |
|
1848 |
{\out Level 5} |
|
1849 |
{\out (f Un g) ` a = f ` a} |
|
1850 |
{\out 1. f Un g : (PROD x:?A. ?B(x))} |
|
1851 |
\end{ttbox} |
|
1852 |
To construct functions of the form $f\union g$, we apply |
|
317 | 1853 |
\tdx{fun_disjoint_Un}: |
104 | 1854 |
\begin{ttbox} |
1855 |
by (resolve_tac [fun_disjoint_Un] 1); |
|
1856 |
{\out Level 6} |
|
1857 |
{\out (f Un g) ` a = f ` a} |
|
1858 |
{\out 1. f : ?A3 -> ?B3} |
|
1859 |
{\out 2. g : ?C3 -> ?D3} |
|
1860 |
{\out 3. ?A3 Int ?C3 = 0} |
|
1861 |
\end{ttbox} |
|
1862 |
The remaining subgoals are instances of the premises. Again, observe how |
|
1863 |
unknowns are instantiated: |
|
1864 |
\begin{ttbox} |
|
1865 |
by (resolve_tac prems 1); |
|
1866 |
{\out Level 7} |
|
1867 |
{\out (f Un g) ` a = f ` a} |
|
1868 |
{\out 1. g : ?C3 -> ?D3} |
|
1869 |
{\out 2. A Int ?C3 = 0} |
|
1870 |
by (resolve_tac prems 1); |
|
1871 |
{\out Level 8} |
|
1872 |
{\out (f Un g) ` a = f ` a} |
|
1873 |
{\out 1. A Int C = 0} |
|
1874 |
by (resolve_tac prems 1); |
|
1875 |
{\out Level 9} |
|
1876 |
{\out (f Un g) ` a = f ` a} |
|
1877 |
{\out No subgoals!} |
|
1878 |
\end{ttbox} |
|
343 | 1879 |
See the files {\tt ZF/func.ML} and {\tt ZF/WF.ML} for more |
104 | 1880 |
examples of reasoning about functions. |
317 | 1881 |
|
1882 |
\index{set theory|)} |