2 \chapter{Zermelo-Fraenkel Set Theory}
5 The theory~\thydx{ZF} implements Zermelo-Fraenkel set
6 theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical
7 first-order logic. The theory includes a collection of derived natural
8 deduction rules, for use with Isabelle's classical reasoner. Some
9 of it is based on the work of No\"el~\cite{noel}.
11 A tremendous amount of set theory has been formally developed, including the
12 basic properties of relations, functions, ordinals and cardinals. Significant
13 results have been proved, such as the Schr\"oder-Bernstein Theorem, the
14 Wellordering Theorem and a version of Ramsey's Theorem. \texttt{ZF} provides
15 both the integers and the natural numbers. General methods have been
16 developed for solving recursion equations over monotonic functors; these have
17 been applied to yield constructions of lists, trees, infinite lists, etc.
19 \texttt{ZF} has a flexible package for handling inductive definitions,
20 such as inference systems, and datatype definitions, such as lists and
21 trees. Moreover it handles coinductive definitions, such as
22 bisimulation relations, and codatatype definitions, such as streams. It
23 provides a streamlined syntax for defining primitive recursive functions over
26 Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
27 less formally than this chapter. Isabelle employs a novel treatment of
28 non-well-founded data structures within the standard {\sc zf} axioms including
29 the Axiom of Foundation~\cite{paulson-mscs}.
32 \section{Which version of axiomatic set theory?}
33 The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})
34 and Zermelo-Fraenkel~({\sc zf}). Resolution theorem provers can use {\sc
35 bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not
36 have a finite axiom system because of its Axiom Scheme of Replacement.
37 This makes it awkward to use with many theorem provers, since instances
38 of the axiom scheme have to be invoked explicitly. Since Isabelle has no
39 difficulty with axiom schemes, we may adopt either axiom system.
41 These two theories differ in their treatment of {\bf classes}, which are
42 collections that are `too big' to be sets. The class of all sets,~$V$,
43 cannot be a set without admitting Russell's Paradox. In {\sc bg}, both
44 classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In
45 {\sc zf}, all variables denote sets; classes are identified with unary
46 predicates. The two systems define essentially the same sets and classes,
47 with similar properties. In particular, a class cannot belong to another
48 class (let alone a set).
50 Modern set theorists tend to prefer {\sc zf} because they are mainly concerned
51 with sets, rather than classes. {\sc bg} requires tiresome proofs that various
52 collections are sets; for instance, showing $x\in\{x\}$ requires showing that
59 \it name &\it meta-type & \it description \\
60 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
61 \cdx{0} & $i$ & empty set\\
62 \cdx{cons} & $[i,i]\To i$ & finite set constructor\\
63 \cdx{Upair} & $[i,i]\To i$ & unordered pairing\\
64 \cdx{Pair} & $[i,i]\To i$ & ordered pairing\\
65 \cdx{Inf} & $i$ & infinite set\\
66 \cdx{Pow} & $i\To i$ & powerset\\
67 \cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\
68 \cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\
69 \cdx{fst} \cdx{snd} & $i\To i$ & projections\\
70 \cdx{converse}& $i\To i$ & converse of a relation\\
71 \cdx{succ} & $i\To i$ & successor\\
72 \cdx{Collect} & $[i,i\To o]\To i$ & separation\\
73 \cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\
74 \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\
75 \cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\
76 \cdx{Pi} \cdx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\
77 \cdx{domain} & $i\To i$ & domain of a relation\\
78 \cdx{range} & $i\To i$ & range of a relation\\
79 \cdx{field} & $i\To i$ & field of a relation\\
80 \cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$-abstraction\\
81 \cdx{restrict}& $[i, i] \To i$ & restriction of a function\\
82 \cdx{The} & $[i\To o]\To i$ & definite description\\
83 \cdx{if} & $[o,i,i]\To i$ & conditional\\
84 \cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers
87 \subcaption{Constants}
91 \index{*"-"`"` symbol}
92 \index{*"` symbol}\index{function applications}
97 \it symbol & \it meta-type & \it priority & \it description \\
98 \tt `` & $[i,i]\To i$ & Left 90 & image \\
99 \tt -`` & $[i,i]\To i$ & Left 90 & inverse image \\
100 \tt ` & $[i,i]\To i$ & Left 90 & application \\
101 \sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\int$) \\
102 \sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\un$) \\
103 \tt - & $[i,i]\To i$ & Left 65 & set difference ($-$) \\[1ex]
104 \tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\
105 \tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$)
109 \caption{Constants of ZF} \label{zf-constants}
113 \section{The syntax of set theory}
114 The language of set theory, as studied by logicians, has no constants. The
115 traditional axioms merely assert the existence of empty sets, unions,
116 powersets, etc.; this would be intolerable for practical reasoning. The
117 Isabelle theory declares constants for primitive sets. It also extends
118 \texttt{FOL} with additional syntax for finite sets, ordered pairs,
119 comprehension, general union/intersection, general sums/products, and
120 bounded quantifiers. In most other respects, Isabelle implements precisely
121 Zermelo-Fraenkel set theory.
123 Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while
124 Figure~\ref{zf-trans} presents the syntax translations. Finally,
125 Figure~\ref{zf-syntax} presents the full grammar for set theory, including the
128 Local abbreviations can be introduced by a \isa{let} construct whose
129 syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into
130 the constant~\cdx{Let}. It can be expanded by rewriting with its
131 definition, \tdx{Let_def}.
133 Apart from \isa{let}, set theory does not use polymorphism. All terms in
134 ZF have type~\tydx{i}, which is the type of individuals and has
135 class~\cldx{term}. The type of first-order formulae, remember,
138 Infix operators include binary union and intersection ($A\un B$ and
139 $A\int B$), set difference ($A-B$), and the subset and membership
140 relations. Note that $a$\verb|~:|$b$ is translated to $\lnot(a\in b)$,
141 which is equivalent to $a\notin b$. The
142 union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
143 union or intersection of a set of sets; $\bigcup A$ means the same as
144 $\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive.
146 The constant \cdx{Upair} constructs unordered pairs; thus \isa{Upair($A$,$B$)} denotes the set~$\{A,B\}$ and
147 \isa{Upair($A$,$A$)} denotes the singleton~$\{A\}$. General union is
148 used to define binary union. The Isabelle version goes on to define
152 A\cup B & \equiv & \bigcup(\isa{Upair}(A,B)) \\
153 \isa{cons}(a,B) & \equiv & \isa{Upair}(a,a) \un B
155 The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
156 obvious manner using~\isa{cons} and~$\emptyset$ (the empty set) \isasymin \begin{eqnarray*}
157 \{a,b,c\} & \equiv & \isa{cons}(a,\isa{cons}(b,\isa{cons}(c,\emptyset)))
160 The constant \cdx{Pair} constructs ordered pairs, as in \isa{Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets,
161 as {\tt<$a$,$b$>}. The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
162 abbreviates the nest of pairs\par\nobreak
163 \centerline{\isa{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
165 In ZF, a function is a set of pairs. A ZF function~$f$ is simply an
166 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
167 $i\To i$. The infix operator~{\tt`} denotes the application of a function set
168 to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The syntax for image
169 is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
173 \index{lambda abs@$\lambda$-abstractions}
176 \begin{center} \footnotesize\tt\frenchspacing
178 \it external & \it internal & \it description \\
179 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
180 \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace & cons($a@1$,$\ldots$,cons($a@n$,0)) &
182 <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> &
183 Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) &
184 \rm ordered $n$-tuple \\
185 \ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x. P[x]$) &
187 \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y. Q[x,y]$) &
189 \ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x. b[x]$) &
190 \rm functional replacement \\
191 \sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
192 \rm general intersection \\
193 \sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
195 \sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x. B[x]$) &
196 \rm general product \\
197 \sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x. B[x]$) &
199 $A$ -> $B$ & Pi($A$,$\lambda x. B$) &
200 \rm function space \\
201 $A$ * $B$ & Sigma($A$,$\lambda x. B$) &
202 \rm binary product \\
203 \sdx{THE} $x . P[x]$ & The($\lambda x. P[x]$) &
204 \rm definite description \\
205 \sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x. b[x]$) &
206 \rm $\lambda$-abstraction\\[1ex]
207 \sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x. P[x]$) &
208 \rm bounded $\forall$ \\
209 \sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x. P[x]$) &
210 \rm bounded $\exists$
213 \caption{Translations for ZF} \label{zf-trans}
222 term & = & \hbox{expression of type~$i$} \\
223 & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
224 & | & "if"~term~"then"~term~"else"~term \\
225 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
226 & | & "< " term\; ("," term)^* " >" \\
227 & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\
228 & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\
229 & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\
230 & | & term " `` " term \\
231 & | & term " -`` " term \\
232 & | & term " ` " term \\
233 & | & term " * " term \\
234 & | & term " \isasyminter " term \\
235 & | & term " \isasymunion " term \\
236 & | & term " - " term \\
237 & | & term " -> " term \\
238 & | & "THE~~" id " . " formula\\
239 & | & "lam~~" id ":" term " . " term \\
240 & | & "INT~~" id ":" term " . " term \\
241 & | & "UN~~~" id ":" term " . " term \\
242 & | & "PROD~" id ":" term " . " term \\
243 & | & "SUM~~" id ":" term " . " term \\[2ex]
244 formula & = & \hbox{expression of type~$o$} \\
245 & | & term " : " term \\
246 & | & term " \ttilde: " term \\
247 & | & term " <= " term \\
248 & | & term " = " term \\
249 & | & term " \ttilde= " term \\
250 & | & "\ttilde\ " formula \\
251 & | & formula " \& " formula \\
252 & | & formula " | " formula \\
253 & | & formula " --> " formula \\
254 & | & formula " <-> " formula \\
255 & | & "ALL " id ":" term " . " formula \\
256 & | & "EX~~" id ":" term " . " formula \\
257 & | & "ALL~" id~id^* " . " formula \\
258 & | & "EX~~" id~id^* " . " formula \\
259 & | & "EX!~" id~id^* " . " formula
262 \caption{Full grammar for ZF} \label{zf-syntax}
266 \section{Binding operators}
267 The constant \cdx{Collect} constructs sets by the principle of {\bf
268 separation}. The syntax for separation is
269 \hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula
270 that may contain free occurrences of~$x$. It abbreviates the set \isa{Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that
271 satisfy~$P[x]$. Note that \isa{Collect} is an unfortunate choice of
272 name: some set theories adopt a set-formation principle, related to
273 replacement, called collection.
275 The constant \cdx{Replace} constructs sets by the principle of {\bf
276 replacement}. The syntax
277 \hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set
278 \isa{Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such
279 that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom
280 has the condition that $Q$ must be single-valued over~$A$: for
281 all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A
282 single-valued binary predicate is also called a {\bf class function}.
284 The constant \cdx{RepFun} expresses a special case of replacement,
285 where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially
286 single-valued, since it is just the graph of the meta-level
287 function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$
288 for~$x\in A$. This is analogous to the \ML{} functional \isa{map},
289 since it applies a function to every element of a set. The syntax is
290 \isa{\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to
291 \isa{RepFun($A$,$\lambda x. b[x]$)}.
293 \index{*INT symbol}\index{*UN symbol}
294 General unions and intersections of indexed
295 families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
296 are written \isa{UN $x$:$A$.\ $B[x]$} and \isa{INT $x$:$A$.\ $B[x]$}.
297 Their meaning is expressed using \isa{RepFun} as
299 \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad
300 \bigcap(\{B[x]. x\in A\}).
302 General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be
303 constructed in set theory, where $B[x]$ is a family of sets over~$A$. They
304 have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.
305 This is similar to the situation in Constructive Type Theory (set theory
306 has `dependent sets') and calls for similar syntactic conventions. The
307 constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and
308 products. Instead of \isa{Sigma($A$,$B$)} and \isa{Pi($A$,$B$)} we may
310 \isa{SUM $x$:$A$.\ $B[x]$} and \isa{PROD $x$:$A$.\ $B[x]$}.
311 \index{*SUM symbol}\index{*PROD symbol}%
312 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
313 general sums and products over a constant family.\footnote{Unlike normal
314 infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
315 no constants~\isa{op~*} and~\isa{op~->}.} Isabelle accepts these
316 abbreviations in parsing and uses them whenever possible for printing.
318 \index{*THE symbol} As mentioned above, whenever the axioms assert the
319 existence and uniqueness of a set, Isabelle's set theory declares a constant
320 for that set. These constants can express the {\bf definite description}
321 operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$,
322 if such exists. Since all terms in ZF denote something, a description is
323 always meaningful, but we do not know its value unless $P[x]$ defines it
324 uniquely. Using the constant~\cdx{The}, we may write descriptions as
325 \isa{The($\lambda x. P[x]$)} or use the syntax \isa{THE $x$.\ $P[x]$}.
328 Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$
329 stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for
330 this to be a set, the function's domain~$A$ must be given. Using the
331 constant~\cdx{Lambda}, we may express function sets as \isa{Lambda($A$,$\lambda x. b[x]$)} or use the syntax \isa{lam $x$:$A$.\ $b[x]$}.
333 Isabelle's set theory defines two {\bf bounded quantifiers}:
335 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
336 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
338 The constants~\cdx{Ball} and~\cdx{Bex} are defined
339 accordingly. Instead of \isa{Ball($A$,$P$)} and \isa{Bex($A$,$P$)} we may
341 \isa{ALL $x$:$A$.\ $P[x]$} and \isa{EX $x$:$A$.\ $P[x]$}.
347 \begin{alltt*}\isastyleminor
348 \tdx{Let_def}: Let(s, f) == f(s)
350 \tdx{Ball_def}: Ball(A,P) == {\isasymforall}x. x \isasymin A --> P(x)
351 \tdx{Bex_def}: Bex(A,P) == {\isasymexists}x. x \isasymin A & P(x)
353 \tdx{subset_def}: A \isasymsubseteq B == {\isasymforall}x \isasymin A. x \isasymin B
354 \tdx{extension}: A = B <-> A \isasymsubseteq B & B \isasymsubseteq A
356 \tdx{Union_iff}: A \isasymin Union(C) <-> ({\isasymexists}B \isasymin C. A \isasymin B)
357 \tdx{Pow_iff}: A \isasymin Pow(B) <-> A \isasymsubseteq B
358 \tdx{foundation}: A=0 | ({\isasymexists}x \isasymin A. {\isasymforall}y \isasymin x. y \isasymnotin A)
360 \tdx{replacement}: ({\isasymforall}x \isasymin A. {\isasymforall}y z. P(x,y) & P(x,z) --> y=z) ==>
361 b \isasymin PrimReplace(A,P) <-> ({\isasymexists}x{\isasymin}A. P(x,b))
362 \subcaption{The Zermelo-Fraenkel Axioms}
364 \tdx{Replace_def}: Replace(A,P) ==
365 PrimReplace(A, \%x y. (\isasymexists!z. P(x,z)) & P(x,y))
366 \tdx{RepFun_def}: RepFun(A,f) == {\ttlbrace}y . x \isasymin A, y=f(x)\ttrbrace
367 \tdx{the_def}: The(P) == Union({\ttlbrace}y . x \isasymin {\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace})
368 \tdx{if_def}: if(P,a,b) == THE z. P & z=a | ~P & z=b
369 \tdx{Collect_def}: Collect(A,P) == {\ttlbrace}y . x \isasymin A, x=y & P(x){\ttrbrace}
370 \tdx{Upair_def}: Upair(a,b) ==
371 {\ttlbrace}y. x\isasymin{}Pow(Pow(0)), x=0 & y=a | x=Pow(0) & y=b{\ttrbrace}
372 \subcaption{Consequences of replacement}
374 \tdx{Inter_def}: Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace}
375 \tdx{Un_def}: A \isasymunion B == Union(Upair(A,B))
376 \tdx{Int_def}: A \isasyminter B == Inter(Upair(A,B))
377 \tdx{Diff_def}: A - B == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace}
378 \subcaption{Union, intersection, difference}
380 \caption{Rules and axioms of ZF} \label{zf-rules}
385 \begin{alltt*}\isastyleminor
386 \tdx{cons_def}: cons(a,A) == Upair(a,a) \isasymunion A
387 \tdx{succ_def}: succ(i) == cons(i,i)
388 \tdx{infinity}: 0 \isasymin Inf & ({\isasymforall}y \isasymin Inf. succ(y) \isasymin Inf)
389 \subcaption{Finite and infinite sets}
391 \tdx{Pair_def}: <a,b> == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace}
392 \tdx{split_def}: split(c,p) == THE y. {\isasymexists}a b. p=<a,b> & y=c(a,b)
393 \tdx{fst_def}: fst(A) == split(\%x y. x, p)
394 \tdx{snd_def}: snd(A) == split(\%x y. y, p)
395 \tdx{Sigma_def}: Sigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x,y>{\ttrbrace}
396 \subcaption{Ordered pairs and Cartesian products}
398 \tdx{converse_def}: converse(r) == {\ttlbrace}z. w\isasymin{}r, {\isasymexists}x y. w=<x,y> & z=<y,x>{\ttrbrace}
399 \tdx{domain_def}: domain(r) == {\ttlbrace}x. w \isasymin r, {\isasymexists}y. w=<x,y>{\ttrbrace}
400 \tdx{range_def}: range(r) == domain(converse(r))
401 \tdx{field_def}: field(r) == domain(r) \isasymunion range(r)
402 \tdx{image_def}: r `` A == {\ttlbrace}y\isasymin{}range(r) . {\isasymexists}x \isasymin A. <x,y> \isasymin r{\ttrbrace}
403 \tdx{vimage_def}: r -`` A == converse(r)``A
404 \subcaption{Operations on relations}
406 \tdx{lam_def}: Lambda(A,b) == {\ttlbrace}<x,b(x)> . x \isasymin A{\ttrbrace}
407 \tdx{apply_def}: f`a == THE y. <a,y> \isasymin f
408 \tdx{Pi_def}: Pi(A,B) == {\ttlbrace}f\isasymin{}Pow(Sigma(A,B)). {\isasymforall}x\isasymin{}A. \isasymexists!y. <x,y>\isasymin{}f{\ttrbrace}
409 \tdx{restrict_def}: restrict(f,A) == lam x \isasymin A. f`x
410 \subcaption{Functions and general product}
412 \caption{Further definitions of ZF} \label{zf-defs}
417 \section{The Zermelo-Fraenkel axioms}
418 The axioms appear in Fig.\ts \ref{zf-rules}. They resemble those
419 presented by Suppes~\cite{suppes72}. Most of the theory consists of
420 definitions. In particular, bounded quantifiers and the subset relation
421 appear in other axioms. Object-level quantifiers and implications have
422 been replaced by meta-level ones wherever possible, to simplify use of the
425 The traditional replacement axiom asserts
426 \[ y \in \isa{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
427 subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.
428 The Isabelle theory defines \cdx{Replace} to apply
429 \cdx{PrimReplace} to the single-valued part of~$P$, namely
430 \[ (\exists!z. P(x,z)) \conj P(x,y). \]
431 Thus $y\in \isa{Replace}(A,P)$ if and only if there is some~$x$ such that
432 $P(x,-)$ holds uniquely for~$y$. Because the equivalence is unconditional,
433 \isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the
434 same set, if $P(x,y)$ is single-valued. The nice syntax for replacement
435 expands to \isa{Replace}.
437 Other consequences of replacement include replacement for
439 (\cdx{RepFun}) and definite descriptions (\cdx{The}).
440 Axioms for separation (\cdx{Collect}) and unordered pairs
441 (\cdx{Upair}) are traditionally assumed, but they actually follow
442 from replacement~\cite[pages 237--8]{suppes72}.
444 The definitions of general intersection, etc., are straightforward. Note
445 the definition of \isa{cons}, which underlies the finite set notation.
446 The axiom of infinity gives us a set that contains~0 and is closed under
447 successor (\cdx{succ}). Although this set is not uniquely defined,
448 the theory names it (\cdx{Inf}) in order to simplify the
449 construction of the natural numbers.
451 Further definitions appear in Fig.\ts\ref{zf-defs}. Ordered pairs are
452 defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall
453 that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two
454 sets. It is defined to be the union of all singleton sets
455 $\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of
458 The projections \cdx{fst} and~\cdx{snd} are defined in terms of the
459 generalized projection \cdx{split}. The latter has been borrowed from
460 Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}
463 Operations on relations include converse, domain, range, and image. The
464 set $\isa{Pi}(A,B)$ generalizes the space of functions between two sets.
465 Note the simple definitions of $\lambda$-abstraction (using
466 \cdx{RepFun}) and application (using a definite description). The
467 function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only
474 \begin{alltt*}\isastyleminor
475 \tdx{ballI}: [| !!x. x\isasymin{}A ==> P(x) |] ==> {\isasymforall}x\isasymin{}A. P(x)
476 \tdx{bspec}: [| {\isasymforall}x\isasymin{}A. P(x); x\isasymin{}A |] ==> P(x)
477 \tdx{ballE}: [| {\isasymforall}x\isasymin{}A. P(x); P(x) ==> Q; x \isasymnotin A ==> Q |] ==> Q
479 \tdx{ball_cong}: [| A=A'; !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==>
480 ({\isasymforall}x\isasymin{}A. P(x)) <-> ({\isasymforall}x\isasymin{}A'. P'(x))
482 \tdx{bexI}: [| P(x); x\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)
483 \tdx{bexCI}: [| {\isasymforall}x\isasymin{}A. ~P(x) ==> P(a); a\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)
484 \tdx{bexE}: [| {\isasymexists}x\isasymin{}A. P(x); !!x. [| x\isasymin{}A; P(x) |] ==> Q |] ==> Q
486 \tdx{bex_cong}: [| A=A'; !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==>
487 ({\isasymexists}x\isasymin{}A. P(x)) <-> ({\isasymexists}x\isasymin{}A'. P'(x))
488 \subcaption{Bounded quantifiers}
490 \tdx{subsetI}: (!!x. x \isasymin A ==> x \isasymin B) ==> A \isasymsubseteq B
491 \tdx{subsetD}: [| A \isasymsubseteq B; c \isasymin A |] ==> c \isasymin B
492 \tdx{subsetCE}: [| A \isasymsubseteq B; c \isasymnotin A ==> P; c \isasymin B ==> P |] ==> P
493 \tdx{subset_refl}: A \isasymsubseteq A
494 \tdx{subset_trans}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> A \isasymsubseteq C
496 \tdx{equalityI}: [| A \isasymsubseteq B; B \isasymsubseteq A |] ==> A = B
497 \tdx{equalityD1}: A = B ==> A \isasymsubseteq B
498 \tdx{equalityD2}: A = B ==> B \isasymsubseteq A
499 \tdx{equalityE}: [| A = B; [| A \isasymsubseteq B; B \isasymsubseteq A |] ==> P |] ==> P
500 \subcaption{Subsets and extensionality}
502 \tdx{emptyE}: a \isasymin 0 ==> P
503 \tdx{empty_subsetI}: 0 \isasymsubseteq A
504 \tdx{equals0I}: [| !!y. y \isasymin A ==> False |] ==> A=0
505 \tdx{equals0D}: [| A=0; a \isasymin A |] ==> P
507 \tdx{PowI}: A \isasymsubseteq B ==> A \isasymin Pow(B)
508 \tdx{PowD}: A \isasymin Pow(B) ==> A \isasymsubseteq B
509 \subcaption{The empty set; power sets}
511 \caption{Basic derived rules for ZF} \label{zf-lemmas1}
515 \section{From basic lemmas to function spaces}
516 Faced with so many definitions, it is essential to prove lemmas. Even
517 trivial theorems like $A \int B = B \int A$ would be difficult to
518 prove from the definitions alone. Isabelle's set theory derives many
519 rules using a natural deduction style. Ideally, a natural deduction
520 rule should introduce or eliminate just one operator, but this is not
521 always practical. For most operators, we may forget its definition
522 and use its derived rules instead.
524 \subsection{Fundamental lemmas}
525 Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
526 operators. The rules for the bounded quantifiers resemble those for the
527 ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption
528 in the style of Isabelle's classical reasoner. The \rmindex{congruence
529 rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
530 simplifier, but have few other uses. Congruence rules must be specially
531 derived for all binding operators, and henceforth will not be shown.
533 Figure~\ref{zf-lemmas1} also shows rules for the subset and equality
534 relations (proof by extensionality), and rules about the empty set and the
537 Figure~\ref{zf-lemmas2} presents rules for replacement and separation.
538 The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
539 comparable rules for \isa{PrimReplace} would be. The principle of
540 separation is proved explicitly, although most proofs should use the
541 natural deduction rules for \isa{Collect}. The elimination rule
542 \tdx{CollectE} is equivalent to the two destruction rules
543 \tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to
544 particular circumstances. Although too many rules can be confusing, there
545 is no reason to aim for a minimal set of rules.
547 Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
548 The empty intersection should be undefined. We cannot have
549 $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All
550 expressions denote something in ZF set theory; the definition of
551 intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
552 arbitrary. The rule \tdx{InterI} must have a premise to exclude
553 the empty intersection. Some of the laws governing intersections require
557 %the [p] gives better page breaking for the book
559 \begin{alltt*}\isastyleminor
560 \tdx{ReplaceI}: [| x\isasymin{}A; P(x,b); !!y. P(x,y) ==> y=b |] ==>
561 b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace}
563 \tdx{ReplaceE}: [| b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace};
564 !!x. [| x\isasymin{}A; P(x,b); {\isasymforall}y. P(x,y)-->y=b |] ==> R
567 \tdx{RepFunI}: [| a\isasymin{}A |] ==> f(a)\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace}
568 \tdx{RepFunE}: [| b\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace};
569 !!x.[| x\isasymin{}A; b=f(x) |] ==> P |] ==> P
571 \tdx{separation}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} <-> a\isasymin{}A & P(a)
572 \tdx{CollectI}: [| a\isasymin{}A; P(a) |] ==> a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace}
573 \tdx{CollectE}: [| a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace}; [| a\isasymin{}A; P(a) |] ==> R |] ==> R
574 \tdx{CollectD1}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> a\isasymin{}A
575 \tdx{CollectD2}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> P(a)
577 \caption{Replacement and separation} \label{zf-lemmas2}
582 \begin{alltt*}\isastyleminor
583 \tdx{UnionI}: [| B\isasymin{}C; A\isasymin{}B |] ==> A\isasymin{}Union(C)
584 \tdx{UnionE}: [| A\isasymin{}Union(C); !!B.[| A\isasymin{}B; B\isasymin{}C |] ==> R |] ==> R
586 \tdx{InterI}: [| !!x. x\isasymin{}C ==> A\isasymin{}x; c\isasymin{}C |] ==> A\isasymin{}Inter(C)
587 \tdx{InterD}: [| A\isasymin{}Inter(C); B\isasymin{}C |] ==> A\isasymin{}B
588 \tdx{InterE}: [| A\isasymin{}Inter(C); A\isasymin{}B ==> R; B \isasymnotin C ==> R |] ==> R
590 \tdx{UN_I}: [| a\isasymin{}A; b\isasymin{}B(a) |] ==> b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x))
591 \tdx{UN_E}: [| b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x)); !!x.[| x\isasymin{}A; b\isasymin{}B(x) |] ==> R
594 \tdx{INT_I}: [| !!x. x\isasymin{}A ==> b\isasymin{}B(x); a\isasymin{}A |] ==> b\isasymin{}({\isasymInter}x\isasymin{}A. B(x))
595 \tdx{INT_E}: [| b\isasymin{}({\isasymInter}x\isasymin{}A. B(x)); a\isasymin{}A |] ==> b\isasymin{}B(a)
597 \caption{General union and intersection} \label{zf-lemmas3}
604 \begin{alltt*}\isastyleminor
605 \tdx{pairing}: a\isasymin{}Upair(b,c) <-> (a=b | a=c)
606 \tdx{UpairI1}: a\isasymin{}Upair(a,b)
607 \tdx{UpairI2}: b\isasymin{}Upair(a,b)
608 \tdx{UpairE}: [| a\isasymin{}Upair(b,c); a=b ==> P; a=c ==> P |] ==> P
610 \caption{Unordered pairs} \label{zf-upair1}
615 \begin{alltt*}\isastyleminor
616 \tdx{UnI1}: c\isasymin{}A ==> c\isasymin{}A \isasymunion B
617 \tdx{UnI2}: c\isasymin{}B ==> c\isasymin{}A \isasymunion B
618 \tdx{UnCI}: (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B
619 \tdx{UnE}: [| c\isasymin{}A \isasymunion B; c\isasymin{}A ==> P; c\isasymin{}B ==> P |] ==> P
621 \tdx{IntI}: [| c\isasymin{}A; c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B
622 \tdx{IntD1}: c\isasymin{}A \isasyminter B ==> c\isasymin{}A
623 \tdx{IntD2}: c\isasymin{}A \isasyminter B ==> c\isasymin{}B
624 \tdx{IntE}: [| c\isasymin{}A \isasyminter B; [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
626 \tdx{DiffI}: [| c\isasymin{}A; c \isasymnotin B |] ==> c\isasymin{}A - B
627 \tdx{DiffD1}: c\isasymin{}A - B ==> c\isasymin{}A
628 \tdx{DiffD2}: c\isasymin{}A - B ==> c \isasymnotin B
629 \tdx{DiffE}: [| c\isasymin{}A - B; [| c\isasymin{}A; c \isasymnotin B |] ==> P |] ==> P
631 \caption{Union, intersection, difference} \label{zf-Un}
636 \begin{alltt*}\isastyleminor
637 \tdx{consI1}: a\isasymin{}cons(a,B)
638 \tdx{consI2}: a\isasymin{}B ==> a\isasymin{}cons(b,B)
639 \tdx{consCI}: (a \isasymnotin B ==> a=b) ==> a\isasymin{}cons(b,B)
640 \tdx{consE}: [| a\isasymin{}cons(b,A); a=b ==> P; a\isasymin{}A ==> P |] ==> P
642 \tdx{singletonI}: a\isasymin{}{\ttlbrace}a{\ttrbrace}
643 \tdx{singletonE}: [| a\isasymin{}{\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P
645 \caption{Finite and singleton sets} \label{zf-upair2}
650 \begin{alltt*}\isastyleminor
651 \tdx{succI1}: i\isasymin{}succ(i)
652 \tdx{succI2}: i\isasymin{}j ==> i\isasymin{}succ(j)
653 \tdx{succCI}: (i \isasymnotin j ==> i=j) ==> i\isasymin{}succ(j)
654 \tdx{succE}: [| i\isasymin{}succ(j); i=j ==> P; i\isasymin{}j ==> P |] ==> P
655 \tdx{succ_neq_0}: [| succ(n)=0 |] ==> P
656 \tdx{succ_inject}: succ(m) = succ(n) ==> m=n
658 \caption{The successor function} \label{zf-succ}
663 \begin{alltt*}\isastyleminor
664 \tdx{the_equality}: [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x))=a
665 \tdx{theI}: \isasymexists! x. P(x) ==> P(THE x. P(x))
667 \tdx{if_P}: P ==> (if P then a else b) = a
668 \tdx{if_not_P}: ~P ==> (if P then a else b) = b
670 \tdx{mem_asym}: [| a\isasymin{}b; b\isasymin{}a |] ==> P
671 \tdx{mem_irrefl}: a\isasymin{}a ==> P
673 \caption{Descriptions; non-circularity} \label{zf-the}
677 \subsection{Unordered pairs and finite sets}
678 Figure~\ref{zf-upair1} presents the principle of unordered pairing, along
679 with its derived rules. Binary union and intersection are defined in terms
680 of ordered pairs (Fig.\ts\ref{zf-Un}). Set difference is also included. The
681 rule \tdx{UnCI} is useful for classical reasoning about unions,
682 like \isa{disjCI}\@; it supersedes \tdx{UnI1} and
683 \tdx{UnI2}, but these rules are often easier to work with. For
684 intersection and difference we have both elimination and destruction rules.
685 Again, there is no reason to provide a minimal rule set.
687 Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
688 for~\isa{cons}, the finite set constructor, and rules for singleton
689 sets. Figure~\ref{zf-succ} presents derived rules for the successor
690 function, which is defined in terms of~\isa{cons}. The proof that
691 \isa{succ} is injective appears to require the Axiom of Foundation.
693 Definite descriptions (\sdx{THE}) are defined in terms of the singleton
694 set~$\{0\}$, but their derived rules fortunately hide this
695 (Fig.\ts\ref{zf-the}). The rule~\tdx{theI} is difficult to apply
696 because of the two occurrences of~$\Var{P}$. However,
697 \tdx{the_equality} does not have this problem and the files contain
698 many examples of its use.
700 Finally, the impossibility of having both $a\in b$ and $b\in a$
701 (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
702 the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence.
708 \begin{alltt*}\isastyleminor
709 \tdx{Union_upper}: B\isasymin{}A ==> B \isasymsubseteq Union(A)
710 \tdx{Union_least}: [| !!x. x\isasymin{}A ==> x \isasymsubseteq C |] ==> Union(A) \isasymsubseteq C
712 \tdx{Inter_lower}: B\isasymin{}A ==> Inter(A) \isasymsubseteq B
713 \tdx{Inter_greatest}: [| a\isasymin{}A; !!x. x\isasymin{}A ==> C \isasymsubseteq x |] ==> C\isasymsubseteq{}Inter(A)
715 \tdx{Un_upper1}: A \isasymsubseteq A \isasymunion B
716 \tdx{Un_upper2}: B \isasymsubseteq A \isasymunion B
717 \tdx{Un_least}: [| A \isasymsubseteq C; B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C
719 \tdx{Int_lower1}: A \isasyminter B \isasymsubseteq A
720 \tdx{Int_lower2}: A \isasyminter B \isasymsubseteq B
721 \tdx{Int_greatest}: [| C \isasymsubseteq A; C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B
723 \tdx{Diff_subset}: A-B \isasymsubseteq A
724 \tdx{Diff_contains}: [| C \isasymsubseteq A; C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B
726 \tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A
728 \caption{Subset and lattice properties} \label{zf-subset}
732 \subsection{Subset and lattice properties}
733 The subset relation is a complete lattice. Unions form least upper bounds;
734 non-empty intersections form greatest lower bounds. Figure~\ref{zf-subset}
735 shows the corresponding rules. A few other laws involving subsets are
737 Reasoning directly about subsets often yields clearer proofs than
738 reasoning about the membership relation. Section~\ref{sec:ZF-pow-example}
739 below presents an example of this, proving the equation
740 ${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$.
745 \begin{alltt*}\isastyleminor
746 \tdx{Pair_inject1}: <a,b> = <c,d> ==> a=c
747 \tdx{Pair_inject2}: <a,b> = <c,d> ==> b=d
748 \tdx{Pair_inject}: [| <a,b> = <c,d>; [| a=c; b=d |] ==> P |] ==> P
749 \tdx{Pair_neq_0}: <a,b>=0 ==> P
751 \tdx{fst_conv}: fst(<a,b>) = a
752 \tdx{snd_conv}: snd(<a,b>) = b
753 \tdx{split}: split(\%x y. c(x,y), <a,b>) = c(a,b)
755 \tdx{SigmaI}: [| a\isasymin{}A; b\isasymin{}B(a) |] ==> <a,b>\isasymin{}Sigma(A,B)
757 \tdx{SigmaE}: [| c\isasymin{}Sigma(A,B);
758 !!x y.[| x\isasymin{}A; y\isasymin{}B(x); c=<x,y> |] ==> P |] ==> P
760 \tdx{SigmaE2}: [| <a,b>\isasymin{}Sigma(A,B);
761 [| a\isasymin{}A; b\isasymin{}B(a) |] ==> P |] ==> P
763 \caption{Ordered pairs; projections; general sums} \label{zf-pair}
767 \subsection{Ordered pairs} \label{sec:pairs}
769 Figure~\ref{zf-pair} presents the rules governing ordered pairs,
770 projections and general sums --- in particular, that
771 $\{\{a\},\{a,b\}\}$ functions as an ordered pair. This property is
772 expressed as two destruction rules,
773 \tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently
774 as the elimination rule \tdx{Pair_inject}.
776 The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This
777 is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other
778 encodings of ordered pairs. The non-standard ordered pairs mentioned below
779 satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
781 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
782 assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
783 $\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \tdx{SigmaE2}
784 merely states that $\pair{a,b}\in \isa{Sigma}(A,B)$ implies $a\in A$ and
787 In addition, it is possible to use tuples as patterns in abstractions:
789 {\tt\%<$x$,$y$>. $t$} \quad stands for\quad \isa{split(\%$x$ $y$.\ $t$)}
791 Nested patterns are translated recursively:
792 {\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$
793 \isa{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \isa{split(\%$x$. split(\%$y$
794 $z$.\ $t$))}. The reverse translation is performed upon printing.
796 The translation between patterns and \isa{split} is performed automatically
797 by the parser and printer. Thus the internal and external form of a term
798 may differ, which affects proofs. For example the term \isa{(\%<x,y>.<y,x>)<a,b>} requires the theorem \isa{split} to rewrite to
801 In addition to explicit $\lambda$-abstractions, patterns can be used in any
802 variable binding construct which is internally described by a
803 $\lambda$-abstraction. Here are some important examples:
805 \item[Let:] \isa{let {\it pattern} = $t$ in $u$}
806 \item[Choice:] \isa{THE~{\it pattern}~.~$P$}
807 \item[Set operations:] \isa{\isasymUnion~{\it pattern}:$A$.~$B$}
808 \item[Comprehension:] \isa{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}}
815 \begin{alltt*}\isastyleminor
816 \tdx{domainI}: <a,b>\isasymin{}r ==> a\isasymin{}domain(r)
817 \tdx{domainE}: [| a\isasymin{}domain(r); !!y. <a,y>\isasymin{}r ==> P |] ==> P
818 \tdx{domain_subset}: domain(Sigma(A,B)) \isasymsubseteq A
820 \tdx{rangeI}: <a,b>\isasymin{}r ==> b\isasymin{}range(r)
821 \tdx{rangeE}: [| b\isasymin{}range(r); !!x. <x,b>\isasymin{}r ==> P |] ==> P
822 \tdx{range_subset}: range(A*B) \isasymsubseteq B
824 \tdx{fieldI1}: <a,b>\isasymin{}r ==> a\isasymin{}field(r)
825 \tdx{fieldI2}: <a,b>\isasymin{}r ==> b\isasymin{}field(r)
826 \tdx{fieldCI}: (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r)
828 \tdx{fieldE}: [| a\isasymin{}field(r);
829 !!x. <a,x>\isasymin{}r ==> P;
830 !!x. <x,a>\isasymin{}r ==> P
833 \tdx{field_subset}: field(A*A) \isasymsubseteq A
835 \caption{Domain, range and field of a relation} \label{zf-domrange}
839 \begin{alltt*}\isastyleminor
840 \tdx{imageI}: [| <a,b>\isasymin{}r; a\isasymin{}A |] ==> b\isasymin{}r``A
841 \tdx{imageE}: [| b\isasymin{}r``A; !!x.[| <x,b>\isasymin{}r; x\isasymin{}A |] ==> P |] ==> P
843 \tdx{vimageI}: [| <a,b>\isasymin{}r; b\isasymin{}B |] ==> a\isasymin{}r-``B
844 \tdx{vimageE}: [| a\isasymin{}r-``B; !!x.[| <a,x>\isasymin{}r; x\isasymin{}B |] ==> P |] ==> P
846 \caption{Image and inverse image} \label{zf-domrange2}
850 \subsection{Relations}
851 Figure~\ref{zf-domrange} presents rules involving relations, which are sets
852 of ordered pairs. The converse of a relation~$r$ is the set of all pairs
853 $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
854 {\cdx{converse}$(r)$} is its inverse. The rules for the domain
855 operation, namely \tdx{domainI} and~\tdx{domainE}, assert that
856 \cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains
857 some pair of the form~$\pair{x,y}$. The range operation is similar, and
858 the field of a relation is merely the union of its domain and range.
860 Figure~\ref{zf-domrange2} presents rules for images and inverse images.
861 Note that these operations are generalisations of range and domain,
868 \begin{alltt*}\isastyleminor
869 \tdx{fun_is_rel}: f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B)
871 \tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
872 \tdx{apply_equality2}: [| <a,b>\isasymin{}f; <a,c>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b=c
874 \tdx{apply_type}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a)
875 \tdx{apply_Pair}: [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> <a,f`a>\isasymin{}f
876 \tdx{apply_iff}: f\isasymin{}Pi(A,B) ==> <a,b>\isasymin{}f <-> a\isasymin{}A & f`a = b
878 \tdx{fun_extension}: [| f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D);
879 !!x. x\isasymin{}A ==> f`x = g`x |] ==> f=g
881 \tdx{domain_type}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> a\isasymin{}A
882 \tdx{range_type}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b\isasymin{}B(a)
884 \tdx{Pi_type}: [| f\isasymin{}A->C; !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> f\isasymin{}Pi(A,B)
885 \tdx{domain_of_fun}: f\isasymin{}Pi(A,B) ==> domain(f)=A
886 \tdx{range_of_fun}: f\isasymin{}Pi(A,B) ==> f\isasymin{}A->range(f)
888 \tdx{restrict}: a\isasymin{}A ==> restrict(f,A) ` a = f`a
889 \tdx{restrict_type}: [| !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==>
890 restrict(f,A)\isasymin{}Pi(A,B)
892 \caption{Functions} \label{zf-func1}
897 \begin{alltt*}\isastyleminor
898 \tdx{lamI}: a\isasymin{}A ==> <a,b(a)>\isasymin{}(lam x\isasymin{}A. b(x))
899 \tdx{lamE}: [| p\isasymin{}(lam x\isasymin{}A. b(x)); !!x.[| x\isasymin{}A; p=<x,b(x)> |] ==> P
902 \tdx{lam_type}: [| !!x. x\isasymin{}A ==> b(x)\isasymin{}B(x) |] ==> (lam x\isasymin{}A. b(x))\isasymin{}Pi(A,B)
904 \tdx{beta}: a\isasymin{}A ==> (lam x\isasymin{}A. b(x)) ` a = b(a)
905 \tdx{eta}: f\isasymin{}Pi(A,B) ==> (lam x\isasymin{}A. f`x) = f
907 \caption{$\lambda$-abstraction} \label{zf-lam}
912 \begin{alltt*}\isastyleminor
913 \tdx{fun_empty}: 0\isasymin{}0->0
914 \tdx{fun_single}: {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
916 \tdx{fun_disjoint_Un}: [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0 |] ==>
917 (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)
919 \tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==>
920 (f \isasymunion g)`a = f`a
922 \tdx{fun_disjoint_apply2}: [| c\isasymin{}C; f\isasymin{}A->B; g\isasymin{}C->D; A\isasyminter{}C = 0 |] ==>
923 (f \isasymunion g)`c = g`c
925 \caption{Constructing functions from smaller sets} \label{zf-func2}
929 \subsection{Functions}
930 Functions, represented by graphs, are notoriously difficult to reason
931 about. The ZF theory provides many derived rules, which overlap more
932 than they ought. This section presents the more important rules.
934 Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$,
935 the generalized function space. For example, if $f$ is a function and
936 $\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}). Two functions
937 are equal provided they have equal domains and deliver equals results
938 (\tdx{fun_extension}).
940 By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be
941 refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable
942 family of sets $\{B(x)\}@{x\in A}$. Conversely, by \tdx{range_of_fun},
943 any dependent typing can be flattened to yield a function type of the form
944 $A\to C$; here, $C=\isa{range}(f)$.
946 Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE}
947 describe the graph of the generated function, while \tdx{beta} and
948 \tdx{eta} are the standard conversions. We essentially have a
949 dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}).
951 Figure~\ref{zf-func2} presents some rules that can be used to construct
952 functions explicitly. We start with functions consisting of at most one
953 pair, and may form the union of two functions provided their domains are
958 \begin{alltt*}\isastyleminor
959 \tdx{Int_absorb}: A \isasyminter A = A
960 \tdx{Int_commute}: A \isasyminter B = B \isasyminter A
961 \tdx{Int_assoc}: (A \isasyminter B) \isasyminter C = A \isasyminter (B \isasyminter C)
962 \tdx{Int_Un_distrib}: (A \isasymunion B) \isasyminter C = (A \isasyminter C) \isasymunion (B \isasyminter C)
964 \tdx{Un_absorb}: A \isasymunion A = A
965 \tdx{Un_commute}: A \isasymunion B = B \isasymunion A
966 \tdx{Un_assoc}: (A \isasymunion B) \isasymunion C = A \isasymunion (B \isasymunion C)
967 \tdx{Un_Int_distrib}: (A \isasyminter B) \isasymunion C = (A \isasymunion C) \isasyminter (B \isasymunion C)
969 \tdx{Diff_cancel}: A-A = 0
970 \tdx{Diff_disjoint}: A \isasyminter (B-A) = 0
971 \tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (B-A) = B
972 \tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A
973 \tdx{Diff_Un}: A - (B \isasymunion C) = (A-B) \isasyminter (A-C)
974 \tdx{Diff_Int}: A - (B \isasyminter C) = (A-B) \isasymunion (A-C)
976 \tdx{Union_Un_distrib}: Union(A \isasymunion B) = Union(A) \isasymunion Union(B)
977 \tdx{Inter_Un_distrib}: [| a \isasymin A; b \isasymin B |] ==>
978 Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B)
980 \tdx{Int_Union_RepFun}: A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C)
982 \tdx{Un_Inter_RepFun}: b \isasymin B ==>
983 A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)
985 \tdx{SUM_Un_distrib1}: (SUM x \isasymin A \isasymunion B. C(x)) =
986 (SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x))
988 \tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) =
989 (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))
991 \tdx{SUM_Int_distrib1}: (SUM x \isasymin A \isasyminter B. C(x)) =
992 (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x))
994 \tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) \isasyminter B(x)) =
995 (SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x))
997 \caption{Equalities} \label{zf-equalities}
1003 % \cdx{1} & $i$ & & $\{\emptyset\}$ \\
1004 % \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\
1005 % \cdx{cond} & $[i,i,i]\To i$ & & conditional for \isa{bool} \\
1006 % \cdx{not} & $i\To i$ & & negation for \isa{bool} \\
1007 % \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for \isa{bool} \\
1008 % \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for \isa{bool} \\
1009 % \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusive-or for \isa{bool}
1012 \begin{alltt*}\isastyleminor
1013 \tdx{bool_def}: bool == {\ttlbrace}0,1{\ttrbrace}
1014 \tdx{cond_def}: cond(b,c,d) == if b=1 then c else d
1015 \tdx{not_def}: not(b) == cond(b,0,1)
1016 \tdx{and_def}: a and b == cond(a,b,0)
1017 \tdx{or_def}: a or b == cond(a,1,b)
1018 \tdx{xor_def}: a xor b == cond(a,not(b),b)
1020 \tdx{bool_1I}: 1 \isasymin bool
1021 \tdx{bool_0I}: 0 \isasymin bool
1022 \tdx{boolE}: [| c \isasymin bool; c=1 ==> P; c=0 ==> P |] ==> P
1023 \tdx{cond_1}: cond(1,c,d) = c
1024 \tdx{cond_0}: cond(0,c,d) = d
1026 \caption{The booleans} \label{zf-bool}
1030 \section{Further developments}
1031 The next group of developments is complex and extensive, and only
1032 highlights can be covered here. It involves many theories and proofs.
1034 Figure~\ref{zf-equalities} presents commutative, associative, distributive,
1035 and idempotency laws of union and intersection, along with other equations.
1037 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
1038 operators including a conditional (Fig.\ts\ref{zf-bool}). Although ZF is a
1039 first-order theory, you can obtain the effect of higher-order logic using
1040 \isa{bool}-valued functions, for example. The constant~\isa{1} is
1041 translated to \isa{succ(0)}.
1046 \it symbol & \it meta-type & \it priority & \it description \\
1047 \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\
1048 \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\
1049 \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$
1051 \begin{alltt*}\isastyleminor
1052 \tdx{sum_def}: A+B == {\ttlbrace}0{\ttrbrace}*A \isasymunion {\ttlbrace}1{\ttrbrace}*B
1053 \tdx{Inl_def}: Inl(a) == <0,a>
1054 \tdx{Inr_def}: Inr(b) == <1,b>
1055 \tdx{case_def}: case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)
1057 \tdx{InlI}: a \isasymin A ==> Inl(a) \isasymin A+B
1058 \tdx{InrI}: b \isasymin B ==> Inr(b) \isasymin A+B
1060 \tdx{Inl_inject}: Inl(a)=Inl(b) ==> a=b
1061 \tdx{Inr_inject}: Inr(a)=Inr(b) ==> a=b
1062 \tdx{Inl_neq_Inr}: Inl(a)=Inr(b) ==> P
1064 \tdx{sum_iff}: u \isasymin A+B <-> ({\isasymexists}x\isasymin{}A. u=Inl(x)) | ({\isasymexists}y\isasymin{}B. u=Inr(y))
1066 \tdx{case_Inl}: case(c,d,Inl(a)) = c(a)
1067 \tdx{case_Inr}: case(c,d,Inr(b)) = d(b)
1069 \caption{Disjoint unions} \label{zf-sum}
1073 \subsection{Disjoint unions}
1075 Theory \thydx{Sum} defines the disjoint union of two sets, with
1076 injections and a case analysis operator (Fig.\ts\ref{zf-sum}). Disjoint
1077 unions play a role in datatype definitions, particularly when there is
1078 mutual recursion~\cite{paulson-set-II}.
1081 \begin{alltt*}\isastyleminor
1082 \tdx{QPair_def}: <a;b> == a+b
1083 \tdx{qsplit_def}: qsplit(c,p) == THE y. {\isasymexists}a b. p=<a;b> & y=c(a,b)
1084 \tdx{qfsplit_def}: qfsplit(R,z) == {\isasymexists}x y. z=<x;y> & R(x,y)
1085 \tdx{qconverse_def}: qconverse(r) == {\ttlbrace}z. w \isasymin r, {\isasymexists}x y. w=<x;y> & z=<y;x>{\ttrbrace}
1086 \tdx{QSigma_def}: QSigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x;y>{\ttrbrace}
1088 \tdx{qsum_def}: A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) \isasymunion ({\ttlbrace}1{\ttrbrace} <*> B)
1089 \tdx{QInl_def}: QInl(a) == <0;a>
1090 \tdx{QInr_def}: QInr(b) == <1;b>
1091 \tdx{qcase_def}: qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z)))
1093 \caption{Non-standard pairs, products and sums} \label{zf-qpair}
1097 \subsection{Non-standard ordered pairs}
1099 Theory \thydx{QPair} defines a notion of ordered pair that admits
1100 non-well-founded tupling (Fig.\ts\ref{zf-qpair}). Such pairs are written
1101 {\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the
1102 converse operator \cdx{qconverse}, and the summation operator
1103 \cdx{QSigma}. These are completely analogous to the corresponding
1104 versions for standard ordered pairs. The theory goes on to define a
1105 non-standard notion of disjoint sum using non-standard pairs. All of these
1106 concepts satisfy the same properties as their standard counterparts; in
1107 addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive
1108 definitions, for example of infinite lists~\cite{paulson-mscs}.
1111 \begin{alltt*}\isastyleminor
1112 \tdx{bnd_mono_def}: bnd_mono(D,h) ==
1113 h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X --> X\isasymsubseteq{}D --> h(W)\isasymsubseteq{}h(X))
1115 \tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace})
1116 \tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace})
1119 \tdx{lfp_lowerbound}: [| h(A) \isasymsubseteq A; A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
1121 \tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D
1123 \tdx{lfp_greatest}: [| bnd_mono(D,h);
1124 !!X. [| h(X) \isasymsubseteq X; X \isasymsubseteq D |] ==> A \isasymsubseteq X
1125 |] ==> A \isasymsubseteq lfp(D,h)
1127 \tdx{lfp_Tarski}: bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))
1129 \tdx{induct}: [| a \isasymin lfp(D,h); bnd_mono(D,h);
1130 !!x. x \isasymin h(Collect(lfp(D,h),P)) ==> P(x)
1133 \tdx{lfp_mono}: [| bnd_mono(D,h); bnd_mono(E,i);
1134 !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)
1135 |] ==> lfp(D,h) \isasymsubseteq lfp(E,i)
1137 \tdx{gfp_upperbound}: [| A \isasymsubseteq h(A); A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
1139 \tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D
1141 \tdx{gfp_least}: [| bnd_mono(D,h);
1142 !!X. [| X \isasymsubseteq h(X); X \isasymsubseteq D |] ==> X \isasymsubseteq A
1143 |] ==> gfp(D,h) \isasymsubseteq A
1145 \tdx{gfp_Tarski}: bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))
1147 \tdx{coinduct}: [| bnd_mono(D,h); a \isasymin X; X \isasymsubseteq h(X \isasymunion gfp(D,h)); X \isasymsubseteq D
1148 |] ==> a \isasymin gfp(D,h)
1150 \tdx{gfp_mono}: [| bnd_mono(D,h); D \isasymsubseteq E;
1151 !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)
1152 |] ==> gfp(D,h) \isasymsubseteq gfp(E,i)
1154 \caption{Least and greatest fixedpoints} \label{zf-fixedpt}
1158 \subsection{Least and greatest fixedpoints}
1160 The Knaster-Tarski Theorem states that every monotone function over a
1161 complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the
1162 Theorem only for a particular lattice, namely the lattice of subsets of a
1163 set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest
1164 fixedpoint operators with corresponding induction and coinduction rules.
1165 These are essential to many definitions that follow, including the natural
1166 numbers and the transitive closure operator. The (co)inductive definition
1167 package also uses the fixedpoint operators~\cite{paulson-CADE}. See
1168 Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski
1169 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
1172 Monotonicity properties are proved for most of the set-forming operations:
1173 union, intersection, Cartesian product, image, domain, range, etc. These
1174 are useful for applying the Knaster-Tarski Fixedpoint Theorem. The proofs
1175 themselves are trivial applications of Isabelle's classical reasoner.
1178 \subsection{Finite sets and lists}
1180 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
1181 $\isa{Fin}(A)$ is the set of all finite sets over~$A$. The theory employs
1182 Isabelle's inductive definition package, which proves various rules
1183 automatically. The induction rule shown is stronger than the one proved by
1184 the package. The theory also defines the set of all finite functions
1185 between two given sets.
1188 \begin{alltt*}\isastyleminor
1189 \tdx{Fin.emptyI} 0 \isasymin Fin(A)
1190 \tdx{Fin.consI} [| a \isasymin A; b \isasymin Fin(A) |] ==> cons(a,b) \isasymin Fin(A)
1193 [| b \isasymin Fin(A);
1195 !!x y. [| x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) |] ==> P(cons(x,y))
1198 \tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B)
1199 \tdx{Fin_UnI}: [| b \isasymin Fin(A); c \isasymin Fin(A) |] ==> b \isasymunion c \isasymin Fin(A)
1200 \tdx{Fin_UnionI}: C \isasymin Fin(Fin(A)) ==> Union(C) \isasymin Fin(A)
1201 \tdx{Fin_subset}: [| c \isasymsubseteq b; b \isasymin Fin(A) |] ==> c \isasymin Fin(A)
1203 \caption{The finite set operator} \label{zf-fin}
1208 \it symbol & \it meta-type & \it priority & \it description \\
1209 \cdx{list} & $i\To i$ && lists over some set\\
1210 \cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\
1211 \cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\
1212 \cdx{length} & $i\To i$ & & length of a list\\
1213 \cdx{rev} & $i\To i$ & & reverse of a list\\
1214 \tt \at & $[i,i]\To i$ & Right 60 & append for lists\\
1215 \cdx{flat} & $i\To i$ & & append of list of lists
1218 \underscoreon %%because @ is used here
1219 \begin{alltt*}\isastyleminor
1220 \tdx{NilI}: Nil \isasymin list(A)
1221 \tdx{ConsI}: [| a \isasymin A; l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
1224 [| l \isasymin list(A);
1226 !!x y. [| x \isasymin A; y \isasymin list(A); P(y) |] ==> P(Cons(x,y))
1229 \tdx{Cons_iff}: Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
1230 \tdx{Nil_Cons_iff}: Nil \isasymnoteq Cons(a,l)
1232 \tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B)
1234 \tdx{map_ident}: l\isasymin{}list(A) ==> map(\%u. u, l) = l
1235 \tdx{map_compose}: l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
1236 \tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys)
1238 [| l\isasymin{}list(A); !!x. x\isasymin{}A ==> h(x)\isasymin{}B |] ==> map(h,l)\isasymin{}list(B)
1240 ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
1242 \caption{Lists} \label{zf-list}
1246 Figure~\ref{zf-list} presents the set of lists over~$A$, $\isa{list}(A)$. The
1247 definition employs Isabelle's datatype package, which defines the introduction
1248 and induction rules automatically, as well as the constructors, case operator
1249 (\isa{list\_case}) and recursion operator. The theory then defines the usual
1250 list functions by primitive recursion. See theory \texttt{List}.
1253 \subsection{Miscellaneous}
1257 \it symbol & \it meta-type & \it priority & \it description \\
1258 \sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\
1259 \cdx{id} & $i\To i$ & & identity function \\
1260 \cdx{inj} & $[i,i]\To i$ & & injective function space\\
1261 \cdx{surj} & $[i,i]\To i$ & & surjective function space\\
1262 \cdx{bij} & $[i,i]\To i$ & & bijective function space
1265 \begin{alltt*}\isastyleminor
1266 \tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) .
1267 {\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace}
1268 \tdx{id_def}: id(A) == (lam x \isasymin A. x)
1269 \tdx{inj_def}: inj(A,B) == {\ttlbrace} f\isasymin{}A->B. {\isasymforall}w\isasymin{}A. {\isasymforall}x\isasymin{}A. f`w=f`x --> w=x {\ttrbrace}
1270 \tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace}
1271 \tdx{bij_def}: bij(A,B) == inj(A,B) \isasyminter surj(A,B)
1274 \tdx{left_inverse}: [| f\isasymin{}inj(A,B); a\isasymin{}A |] ==> converse(f)`(f`a) = a
1275 \tdx{right_inverse}: [| f\isasymin{}inj(A,B); b\isasymin{}range(f) |] ==>
1276 f`(converse(f)`b) = b
1278 \tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A)
1279 \tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A)
1281 \tdx{comp_type}: [| s \isasymsubseteq A*B; r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
1282 \tdx{comp_assoc}: (r O s) O t = r O (s O t)
1284 \tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r
1285 \tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
1287 \tdx{comp_func}: [| g\isasymin{}A->B; f\isasymin{}B->C |] ==> (f O g) \isasymin A->C
1288 \tdx{comp_func_apply}: [| g\isasymin{}A->B; f\isasymin{}B->C; a\isasymin{}A |] ==> (f O g)`a = f`(g`a)
1290 \tdx{comp_inj}: [| g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) |] ==> (f O g)\isasymin{}inj(A,C)
1291 \tdx{comp_surj}: [| g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) |] ==> (f O g)\isasymin{}surj(A,C)
1292 \tdx{comp_bij}: [| g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) |] ==> (f O g)\isasymin{}bij(A,C)
1294 \tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A)
1295 \tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B)
1297 \tdx{bij_disjoint_Un}:
1298 [| f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 |] ==>
1299 (f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D)
1301 \tdx{restrict_bij}: [| f\isasymin{}inj(A,B); C\isasymsubseteq{}A |] ==> restrict(f,C)\isasymin{}bij(C, f``C)
1303 \caption{Permutations} \label{zf-perm}
1306 The theory \thydx{Perm} is concerned with permutations (bijections) and
1307 related concepts. These include composition of relations, the identity
1308 relation, and three specialized function spaces: injective, surjective and
1309 bijective. Figure~\ref{zf-perm} displays many of their properties that
1310 have been proved. These results are fundamental to a treatment of
1311 equipollence and cardinality.
1313 Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by
1314 the datatype package. This set contains $A$ and the
1315 natural numbers. Vitally, it is closed under finite products:
1316 $\isa{univ}(A)\times\isa{univ}(A)\subseteq\isa{univ}(A)$. This theory also
1317 defines the cumulative hierarchy of axiomatic set theory, which
1318 traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The
1319 `universe' is a simple generalization of~$V@\omega$.
1321 Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by
1322 the datatype package to construct codatatypes such as streams. It is
1323 analogous to $\isa{univ}(A)$ (and is defined in terms of it) but is closed
1324 under the non-standard product and sum.
1327 \section{Automatic Tools}
1329 ZF provides the simplifier and the classical reasoner. Moreover it supplies a
1330 specialized tool to infer `types' of terms.
1332 \subsection{Simplification and Classical Reasoning}
1334 ZF inherits simplification from FOL but adopts it for set theory. The
1335 extraction of rewrite rules takes the ZF primitives into account. It can
1336 strip bounded universal quantifiers from a formula; for example, ${\forall
1337 x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
1338 f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
1339 A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in A-B$.
1341 The default simpset used by \isa{simp} contains congruence rules for all of ZF's
1342 binding operators. It contains all the conversion rules, such as
1344 \isa{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
1346 Classical reasoner methods such as \isa{blast} and \isa{auto} refer to
1347 a rich collection of built-in axioms for all the set-theoretic
1353 a\in \emptyset & \bimp & \bot\\
1354 a \in A \un B & \bimp & a\in A \disj a\in B\\
1355 a \in A \int B & \bimp & a\in A \conj a\in B\\
1356 a \in A-B & \bimp & a\in A \conj \lnot (a\in B)\\
1357 \pair{a,b}\in \isa{Sigma}(A,B)
1358 & \bimp & a\in A \conj b\in B(a)\\
1359 a \in \isa{Collect}(A,P) & \bimp & a\in A \conj P(a)\\
1360 (\forall x \in \emptyset. P(x)) & \bimp & \top\\
1361 (\forall x \in A. \top) & \bimp & \top
1363 \caption{Some rewrite rules for set theory} \label{zf-simpdata}
1367 \subsection{Type-Checking Tactics}
1368 \index{type-checking tactics}
1370 Isabelle/ZF provides simple tactics to help automate those proofs that are
1371 essentially type-checking. Such proofs are built by applying rules such as
1373 \begin{ttbox}\isastyleminor
1374 [| ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A |]
1375 ==> (if ?P then ?a else ?b) \isasymin ?A
1377 [| ?m \isasymin nat; ?n \isasymin nat |] ==> ?m #+ ?n \isasymin nat
1379 ?a \isasymin ?A ==> Inl(?a) \isasymin ?A + ?B
1381 In typical applications, the goal has the form $t\in\Var{A}$: in other words,
1382 we have a specific term~$t$ and need to infer its `type' by instantiating the
1383 set variable~$\Var{A}$. Neither the simplifier nor the classical reasoner
1384 does this job well. The if-then-else rule, and many similar ones, can make
1385 the classical reasoner loop. The simplifier refuses (on principle) to
1386 instantiate variables during rewriting, so goals such as \isa{i\#+j \isasymin \ ?A}
1389 The simplifier calls the type-checker to solve rewritten subgoals: this stage
1390 can indeed instantiate variables. If you have defined new constants and
1391 proved type-checking rules for them, then declare the rules using
1392 the attribute \isa{TC} and the rest should be automatic. In
1393 particular, the simplifier will use type-checking to help satisfy
1394 conditional rewrite rules. Call the method \ttindex{typecheck} to
1395 break down all subgoals using type-checking rules. You can add new
1396 type-checking rules temporarily like this:
1398 \isacommand{apply}\ (typecheck add:\ inj_is_fun)
1402 %Though the easiest way to invoke the type-checker is via the simplifier,
1403 %specialized applications may require more detailed knowledge of
1404 %the type-checking primitives. They are modelled on the simplifier's:
1405 %\begin{ttdescription}
1406 %\item[\ttindexbold{tcset}] is the type of tcsets: sets of type-checking rules.
1408 %\item[\ttindexbold{addTCs}] is an infix operator to add type-checking rules to
1411 %\item[\ttindexbold{delTCs}] is an infix operator to remove type-checking rules
1414 %\item[\ttindexbold{typecheck_tac}] is a tactic for attempting to prove all
1415 % subgoals using the rules given in its argument, a tcset.
1416 %\end{ttdescription}
1418 %Tcsets, like simpsets, are associated with theories and are merged when
1419 %theories are merged. There are further primitives that use the default tcset.
1420 %\begin{ttdescription}
1421 %\item[\ttindexbold{tcset}] is a function to return the default tcset; use the
1422 % expression \isa{tcset()}.
1424 %\item[\ttindexbold{AddTCs}] adds type-checking rules to the default tcset.
1426 %\item[\ttindexbold{DelTCs}] removes type-checking rules from the default
1429 %\item[\ttindexbold{Typecheck_tac}] calls \isa{typecheck_tac} using the
1431 %\end{ttdescription}
1433 %To supply some type-checking rules temporarily, using \isa{Addrules} and
1434 %later \isa{Delrules} is the simplest way. There is also a high-tech
1435 %approach. Call the simplifier with a new solver expressed using
1436 %\ttindexbold{type_solver_tac} and your temporary type-checking rules.
1437 %\begin{ttbox}\isastyleminor
1439 % (simpset() setSolver type_solver_tac (tcset() addTCs prems)) 2);
1443 \section{Natural number and integer arithmetic}
1445 \index{arithmetic|(}
1447 \begin{figure}\small
1448 \index{#*@{\tt\#*} symbol}
1451 \index{#+@{\tt\#+} symbol}
1452 \index{#-@{\tt\#-} symbol}
1454 \it symbol & \it meta-type & \it priority & \it description \\
1455 \cdx{nat} & $i$ & & set of natural numbers \\
1456 \cdx{nat_case}& $[i,i\To i,i]\To i$ & & conditional for $nat$\\
1457 \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\
1458 \tt div & $[i,i]\To i$ & Left 70 & division\\
1459 \tt mod & $[i,i]\To i$ & Left 70 & modulus\\
1460 \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\
1461 \tt \#- & $[i,i]\To i$ & Left 65 & subtraction
1464 \begin{alltt*}\isastyleminor
1465 \tdx{nat_def}: nat == lfp(lam r \isasymin Pow(Inf). {\ttlbrace}0{\ttrbrace} \isasymunion {\ttlbrace}succ(x). x \isasymin r{\ttrbrace}
1467 \tdx{nat_case_def}: nat_case(a,b,k) ==
1468 THE y. k=0 & y=a | ({\isasymexists}x. k=succ(x) & y=b(x))
1470 \tdx{nat_0I}: 0 \isasymin nat
1471 \tdx{nat_succI}: n \isasymin nat ==> succ(n) \isasymin nat
1474 [| n \isasymin nat; P(0); !!x. [| x \isasymin nat; P(x) |] ==> P(succ(x))
1477 \tdx{nat_case_0}: nat_case(a,b,0) = a
1478 \tdx{nat_case_succ}: nat_case(a,b,succ(m)) = b(m)
1480 \tdx{add_0_natify}: 0 #+ n = natify(n)
1481 \tdx{add_succ}: succ(m) #+ n = succ(m #+ n)
1483 \tdx{mult_type}: m #* n \isasymin nat
1484 \tdx{mult_0}: 0 #* n = 0
1485 \tdx{mult_succ}: succ(m) #* n = n #+ (m #* n)
1486 \tdx{mult_commute}: m #* n = n #* m
1487 \tdx{add_mult_dist}: (m #+ n) #* k = (m #* k) #+ (n #* k)
1488 \tdx{mult_assoc}: (m #* n) #* k = m #* (n #* k)
1489 \tdx{mod_div_equality}: m \isasymin nat ==> (m div n)#*n #+ m mod n = m
1491 \caption{The natural numbers} \label{zf-nat}
1494 \index{natural numbers}
1496 Theory \thydx{Nat} defines the natural numbers and mathematical
1497 induction, along with a case analysis operator. The set of natural
1498 numbers, here called \isa{nat}, is known in set theory as the ordinal~$\omega$.
1500 Theory \thydx{Arith} develops arithmetic on the natural numbers
1501 (Fig.\ts\ref{zf-nat}). Addition, multiplication and subtraction are defined
1502 by primitive recursion. Division and remainder are defined by repeated
1503 subtraction, which requires well-founded recursion; the termination argument
1504 relies on the divisor's being non-zero. Many properties are proved:
1505 commutative, associative and distributive laws, identity and cancellation
1506 laws, etc. The most interesting result is perhaps the theorem $a \bmod b +
1509 To minimize the need for tedious proofs of $t\in\isa{nat}$, the arithmetic
1510 operators coerce their arguments to be natural numbers. The function
1511 \cdx{natify} is defined such that $\isa{natify}(n) = n$ if $n$ is a natural
1512 number, $\isa{natify}(\isa{succ}(x)) =
1513 \isa{succ}(\isa{natify}(x))$ for all $x$, and finally
1514 $\isa{natify}(x)=0$ in all other cases. The benefit is that the addition,
1515 subtraction, multiplication, division and remainder operators always return
1516 natural numbers, regardless of their arguments. Algebraic laws (commutative,
1517 associative, distributive) are unconditional. Occurrences of \isa{natify}
1518 as operands of those operators are simplified away. Any remaining occurrences
1519 can either be tolerated or else eliminated by proving that the argument is a
1522 The simplifier automatically cancels common terms on the opposite sides of
1523 subtraction and of relations ($=$, $<$ and $\le$). Here is an example:
1525 1. i \#+ j \#+ k \#- j < k \#+ l\isanewline
1526 \isacommand{apply}\ simp\isanewline
1527 1. natify(i) < natify(l)
1529 Given the assumptions \isa{i \isasymin nat} and \isa{l \isasymin nat}, both occurrences of
1530 \cdx{natify} would be simplified away.
1533 \begin{figure}\small
1534 \index{$*@{\tt\$*} symbol}
1535 \index{$+@{\tt\$+} symbol}
1536 \index{$-@{\tt\$-} symbol}
1538 \it symbol & \it meta-type & \it priority & \it description \\
1539 \cdx{int} & $i$ & & set of integers \\
1540 \tt \$* & $[i,i]\To i$ & Left 70 & multiplication \\
1541 \tt \$+ & $[i,i]\To i$ & Left 65 & addition\\
1542 \tt \$- & $[i,i]\To i$ & Left 65 & subtraction\\
1543 \tt \$< & $[i,i]\To o$ & Left 50 & $<$ on integers\\
1544 \tt \$<= & $[i,i]\To o$ & Left 50 & $\le$ on integers
1547 \begin{alltt*}\isastyleminor
1548 \tdx{zadd_0_intify}: 0 $+ n = intify(n)
1550 \tdx{zmult_type}: m $* n \isasymin int
1551 \tdx{zmult_0}: 0 $* n = 0
1552 \tdx{zmult_commute}: m $* n = n $* m
1553 \tdx{zadd_zmult_dist}: (m $+ n) $* k = (m $* k) $+ (n $* k)
1554 \tdx{zmult_assoc}: (m $* n) $* k = m $* (n $* k)
1556 \caption{The integers} \label{zf-int}
1562 Theory \thydx{Int} defines the integers, as equivalence classes of natural
1563 numbers. Figure~\ref{zf-int} presents a tidy collection of laws. In
1564 fact, a large library of facts is proved, including monotonicity laws for
1565 addition and multiplication, covering both positive and negative operands.
1567 As with the natural numbers, the need for typing proofs is minimized. All the
1568 operators defined in Fig.\ts\ref{zf-int} coerce their operands to integers by
1569 applying the function \cdx{intify}. This function is the identity on integers
1570 and maps other operands to zero.
1572 Decimal notation is provided for the integers. Numbers, written as
1573 \isa{\#$nnn$} or \isa{\#-$nnn$}, are represented internally in
1574 two's-complement binary. Expressions involving addition, subtraction and
1575 multiplication of numeral constants are evaluated (with acceptable efficiency)
1576 by simplification. The simplifier also collects similar terms, multiplying
1577 them by a numerical coefficient. It also cancels occurrences of the same
1578 terms on the other side of the relational operators. Example:
1580 1. y \$+ z \$+ \#-3 \$* x \$+ y \$<= x \$* \#2 \$+
1582 \isacommand{apply}\ simp\isanewline
1583 1. \#2 \$* y \$<= \#5 \$* x
1585 For more information on the integers, please see the theories on directory
1588 \index{arithmetic|)}
1591 \section{Datatype definitions}
1592 \label{sec:ZF:datatype}
1595 The \ttindex{datatype} definition package of ZF constructs inductive datatypes
1596 similar to \ML's. It can also construct coinductive datatypes
1597 (codatatypes), which are non-well-founded structures such as streams. It
1598 defines the set using a fixed-point construction and proves induction rules,
1599 as well as theorems for recursion and case combinators. It supplies
1600 mechanisms for reasoning about freeness. The datatype package can handle both
1601 mutual and indirect recursion.
1605 \label{subsec:datatype:basics}
1607 A \isa{datatype} definition has the following form:
1610 \mathtt{datatype} & t@1(A@1,\ldots,A@h) & = &
1611 constructor^1@1 ~\mid~ \ldots ~\mid~ constructor^1@{k@1} \\
1613 \mathtt{and} & t@n(A@1,\ldots,A@h) & = &
1614 constructor^n@1~ ~\mid~ \ldots ~\mid~ constructor^n@{k@n}
1617 Here $t@1$, \ldots,~$t@n$ are identifiers and $A@1$, \ldots,~$A@h$ are
1618 variables: the datatype's parameters. Each constructor specification has the
1620 \[ C \hbox{\tt~( } \hbox{\tt"} x@1 \hbox{\tt:} T@1 \hbox{\tt"},\;
1622 \hbox{\tt"} x@m \hbox{\tt:} T@m \hbox{\tt"}
1625 Here $C$ is the constructor name, and variables $x@1$, \ldots,~$x@m$ are the
1626 constructor arguments, belonging to the sets $T@1$, \ldots, $T@m$,
1627 respectively. Typically each $T@j$ is either a constant set, a datatype
1628 parameter (one of $A@1$, \ldots, $A@h$) or a recursive occurrence of one of
1629 the datatypes, say $t@i(A@1,\ldots,A@h)$. More complex possibilities exist,
1630 but they are much harder to realize. Often, additional information must be
1631 supplied in the form of theorems.
1633 A datatype can occur recursively as the argument of some function~$F$. This
1634 is called a {\em nested} (or \emph{indirect}) occurrence. It is only allowed
1635 if the datatype package is given a theorem asserting that $F$ is monotonic.
1636 If the datatype has indirect occurrences, then Isabelle/ZF does not support
1637 recursive function definitions.
1639 A simple example of a datatype is \isa{list}, which is built-in, and is
1641 \begin{alltt*}\isastyleminor
1642 consts list :: "i=>i"
1643 datatype "list(A)" = Nil | Cons ("a \isasymin A", "l \isasymin list(A)")
1645 Note that the datatype operator must be declared as a constant first.
1646 However, the package declares the constructors. Here, \isa{Nil} gets type
1647 $i$ and \isa{Cons} gets type $[i,i]\To i$.
1649 Trees and forests can be modelled by the mutually recursive datatype
1651 \begin{alltt*}\isastyleminor
1655 tree_forest :: "i=>i"
1656 datatype "tree(A)" = Tcons ("a{\isasymin}A", "f{\isasymin}forest(A)")
1657 and "forest(A)" = Fnil | Fcons ("t{\isasymin}tree(A)", "f{\isasymin}forest(A)")
1659 Here $\isa{tree}(A)$ is the set of trees over $A$, $\isa{forest}(A)$ is
1660 the set of forests over $A$, and $\isa{tree_forest}(A)$ is the union of
1661 the previous two sets. All three operators must be declared first.
1663 The datatype \isa{term}, which is defined by
1664 \begin{alltt*}\isastyleminor
1665 consts term :: "i=>i"
1666 datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))")
1668 type_elims list_univ [THEN subsetD, elim_format]
1670 is an example of nested recursion. (The theorem \isa{list_mono} is proved
1671 in theory \isa{List}, and the \isa{term} example is developed in
1673 \thydx{Induct/Term}.)
1675 \subsubsection{Freeness of the constructors}
1677 Constructors satisfy {\em freeness} properties. Constructions are distinct,
1678 for example $\isa{Nil}\not=\isa{Cons}(a,l)$, and they are injective, for
1679 example $\isa{Cons}(a,l)=\isa{Cons}(a',l') \bimp a=a' \conj l=l'$.
1680 Because the number of freeness is quadratic in the number of constructors, the
1681 datatype package does not prove them. Instead, it ensures that simplification
1682 will prove them dynamically: when the simplifier encounters a formula
1683 asserting the equality of two datatype constructors, it performs freeness
1686 Freeness reasoning can also be done using the classical reasoner, but it is
1687 more complicated. You have to add some safe elimination rules rules to the
1688 claset. For the \isa{list} datatype, they are called
1689 \isa{list.free_elims}. Occasionally this exposes the underlying
1690 representation of some constructor, which can be rectified using the command
1691 \isa{unfold list.con_defs [symmetric]}.
1694 \subsubsection{Structural induction}
1696 The datatype package also provides structural induction rules. For datatypes
1697 without mutual or nested recursion, the rule has the form exemplified by
1698 \isa{list.induct} in Fig.\ts\ref{zf-list}. For mutually recursive
1699 datatypes, the induction rule is supplied in two forms. Consider datatype
1700 \isa{TF}. The rule \isa{tree_forest.induct} performs induction over a
1701 single predicate~\isa{P}, which is presumed to be defined for both trees
1703 \begin{alltt*}\isastyleminor
1704 [| x \isasymin tree_forest(A);
1705 !!a f. [| a \isasymin A; f \isasymin forest(A); P(f) |] ==> P(Tcons(a, f));
1707 !!f t. [| t \isasymin tree(A); P(t); f \isasymin forest(A); P(f) |]
1711 The rule \isa{tree_forest.mutual_induct} performs induction over two
1712 distinct predicates, \isa{P_tree} and \isa{P_forest}.
1713 \begin{alltt*}\isastyleminor
1715 [| a{\isasymin}A; f{\isasymin}forest(A); P_forest(f) |] ==> P_tree(Tcons(a,f));
1717 !!f t. [| t{\isasymin}tree(A); P_tree(t); f{\isasymin}forest(A); P_forest(f) |]
1718 ==> P_forest(Fcons(t, f))
1719 |] ==> ({\isasymforall}za. za \isasymin tree(A) --> P_tree(za)) &
1720 ({\isasymforall}za. za \isasymin forest(A) --> P_forest(za))
1723 For datatypes with nested recursion, such as the \isa{term} example from
1724 above, things are a bit more complicated. The rule \isa{term.induct}
1725 refers to the monotonic operator, \isa{list}:
1726 \begin{alltt*}\isastyleminor
1727 [| x \isasymin term(A);
1728 !!a l. [| a\isasymin{}A; l\isasymin{}list(Collect(term(A), P)) |] ==> P(Apply(a,l))
1731 The theory \isa{Induct/Term.thy} derives two higher-level induction rules,
1732 one of which is particularly useful for proving equations:
1733 \begin{alltt*}\isastyleminor
1734 [| t \isasymin term(A);
1735 !!x zs. [| x \isasymin A; zs \isasymin list(term(A)); map(f, zs) = map(g, zs) |]
1736 ==> f(Apply(x, zs)) = g(Apply(x, zs))
1739 How this can be generalized to other nested datatypes is a matter for future
1743 \subsubsection{The \isa{case} operator}
1745 The package defines an operator for performing case analysis over the
1746 datatype. For \isa{list}, it is called \isa{list_case} and satisfies
1748 \begin{ttbox}\isastyleminor
1749 list_case(f_Nil, f_Cons, []) = f_Nil
1750 list_case(f_Nil, f_Cons, Cons(a, l)) = f_Cons(a, l)
1752 Here \isa{f_Nil} is the value to return if the argument is \isa{Nil} and
1753 \isa{f_Cons} is a function that computes the value to return if the
1754 argument has the form $\isa{Cons}(a,l)$. The function can be expressed as
1755 an abstraction, over patterns if desired (\S\ref{sec:pairs}).
1757 For mutually recursive datatypes, there is a single \isa{case} operator.
1758 In the tree/forest example, the constant \isa{tree_forest_case} handles all
1759 of the constructors of the two datatypes.
1762 \subsection{Defining datatypes}
1764 The theory syntax for datatype definitions is shown in
1765 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
1766 definition has to obey the rules stated in the previous section. As a result
1767 the theory is extended with the new types, the constructors, and the theorems
1768 listed in the previous section. The quotation marks are necessary because
1769 they enclose general Isabelle formul\ae.
1773 datatype : ( 'datatype' | 'codatatype' ) datadecls;
1775 datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and'
1777 constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) )
1779 consargs : '(' ('"' var ' : ' term '"' + ',') ')'
1782 \caption{Syntax of datatype declarations}
1783 \label{datatype-grammar}
1786 Codatatypes are declared like datatypes and are identical to them in every
1787 respect except that they have a coinduction rule instead of an induction rule.
1788 Note that while an induction rule has the effect of limiting the values
1789 contained in the set, a coinduction rule gives a way of constructing new
1792 Most of the theorems about datatypes become part of the default simpset. You
1793 never need to see them again because the simplifier applies them
1796 \subsubsection{Specialized methods for datatypes}
1798 Induction and case-analysis can be invoked using these special-purpose
1800 \begin{ttdescription}
1801 \item[\methdx{induct_tac} $x$] applies structural
1802 induction on variable $x$ to subgoal~1, provided the type of $x$ is a
1803 datatype. The induction variable should not occur among other assumptions
1807 % we also have the ind_cases method, but what does it do?
1808 In some situations, induction is overkill and a case distinction over all
1809 constructors of the datatype suffices.
1810 \begin{ttdescription}
1811 \item[\methdx{case_tac} $x$]
1812 performs a case analysis for the variable~$x$.
1815 Both tactics can only be applied to a variable, whose typing must be given in
1816 some assumption, for example the assumption \isa{x \isasymin \ list(A)}. The tactics
1817 also work for the natural numbers (\isa{nat}) and disjoint sums, although
1818 these sets were not defined using the datatype package. (Disjoint sums are
1819 not recursive, so only \isa{case_tac} is available.)
1821 Structured Isar methods are also available. Below, $t$
1822 stands for the name of the datatype.
1823 \begin{ttdescription}
1824 \item[\methdx{induct} \isa{set:}\ $t$] is the Isar induction tactic.
1825 \item[\methdx{cases} \isa{set:}\ $t$] is the Isar case-analysis tactic.
1829 \subsubsection{The theorems proved by a datatype declaration}
1831 Here are some more details for the technically minded. Processing the
1832 datatype declaration of a set~$t$ produces a name space~$t$ containing
1833 the following theorems:
1834 \begin{ttbox}\isastyleminor
1835 intros \textrm{the introduction rules}
1836 cases \textrm{the case analysis rule}
1837 induct \textrm{the standard induction rule}
1838 mutual_induct \textrm{the mutual induction rule, if needed}
1839 case_eqns \textrm{equations for the case operator}
1840 recursor_eqns \textrm{equations for the recursor}
1841 simps \textrm{the union of} case_eqns \textrm{and} recursor_eqns
1842 con_defs \textrm{definitions of the case operator and constructors}
1843 free_iffs \textrm{logical equivalences for proving freeness}
1844 free_elims \textrm{elimination rules for proving freeness}
1845 defs \textrm{datatype definition(s)}
1847 Furthermore there is the theorem $C$ for every constructor~$C$; for
1848 example, the \isa{list} datatype's introduction rules are bound to the
1849 identifiers \isa{Nil} and \isa{Cons}.
1851 For a codatatype, the component \isa{coinduct} is the coinduction rule,
1852 replacing the \isa{induct} component.
1854 See the theories \isa{Induct/Ntree} and \isa{Induct/Brouwer} for examples of
1855 infinitely branching datatypes. See theory \isa{Induct/LList} for an example
1856 of a codatatype. Some of these theories illustrate the use of additional,
1857 undocumented features of the datatype package. Datatype definitions are
1858 reduced to inductive definitions, and the advanced features should be
1859 understood in that light.
1862 \subsection{Examples}
1864 \subsubsection{The datatype of binary trees}
1866 Let us define the set $\isa{bt}(A)$ of binary trees over~$A$. The theory
1867 must contain these lines:
1868 \begin{alltt*}\isastyleminor
1870 datatype "bt(A)" = Lf | Br ("a\isasymin{}A", "t1\isasymin{}bt(A)", "t2\isasymin{}bt(A)")
1872 After loading the theory, we can prove some theorem.
1873 We begin by declaring the constructor's typechecking rules
1874 as simplification rules:
1876 \isacommand{declare}\ bt.intros\ [simp]%
1879 Our first example is the theorem that no tree equals its
1880 left branch. To make the inductive hypothesis strong enough,
1881 the proof requires a quantified induction formula, but
1882 the \isa{rule\_format} attribute will remove the quantifiers
1883 before the theorem is stored.
1885 \isacommand{lemma}\ Br\_neq\_left\ [rule\_format]:\ "l\isasymin bt(A)\ ==>\ \isasymforall x\ r.\ Br(x,l,r)\isasymnoteq{}l"\isanewline
1886 \ 1.\ l\ \isasymin \ bt(A)\ \isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l%
1888 This can be proved by the structural induction tactic:
1890 \ \ \isacommand{apply}\ (induct\_tac\ l)\isanewline
1891 \ 1.\ \isasymforall x\ r.\ Br(x,\ Lf,\ r)\ \isasymnoteq \ Lf\isanewline
1892 \ 2.\ \isasymAnd a\ t1\ t2.\isanewline
1893 \isaindent{\ 2.\ \ \ \ }\isasymlbrakk a\ \isasymin \ A;\ t1\ \isasymin \ bt(A);\ \isasymforall x\ r.\ Br(x,\ t1,\ r)\ \isasymnoteq \ t1;\ t2\ \isasymin \ bt(A);\isanewline
1894 \isaindent{\ 2.\ \ \ \ \ \ \ }\isasymforall x\ r.\ Br(x,\ t2,\ r)\ \isasymnoteq \ t2\isasymrbrakk \isanewline
1895 \isaindent{\ 2.\ \ \ \ }\isasymLongrightarrow \ \isasymforall x\ r.\ Br(x,\ Br(a,\ t1,\ t2),\ r)\ \isasymnoteq \ Br(a,\ t1,\ t2)
1897 Both subgoals are proved using \isa{auto}, which performs the necessary
1900 \ \ \isacommand{apply}\ auto\isanewline
1901 No\ subgoals!\isanewline
1905 An alternative proof uses Isar's fancy \isa{induct} method, which
1906 automatically quantifies over all free variables:
1909 \isacommand{lemma}\ Br\_neq\_left':\ "l\ \isasymin \ bt(A)\ ==>\ (!!x\ r.\ Br(x,\ l,\ r)\ \isasymnoteq \ l)"\isanewline
1910 \ \ \isacommand{apply}\ (induct\ set:\ bt)\isanewline
1911 \ 1.\ \isasymAnd x\ r.\ Br(x,\ Lf,\ r)\ \isasymnoteq \ Lf\isanewline
1912 \ 2.\ \isasymAnd a\ t1\ t2\ x\ r.\isanewline
1913 \isaindent{\ 2.\ \ \ \ }\isasymlbrakk a\ \isasymin \ A;\ t1\ \isasymin \ bt(A);\ \isasymAnd x\ r.\ Br(x,\ t1,\ r)\ \isasymnoteq \ t1;\ t2\ \isasymin \ bt(A);\isanewline
1914 \isaindent{\ 2.\ \ \ \ \ \ \ }\isasymAnd x\ r.\ Br(x,\ t2,\ r)\ \isasymnoteq \ t2\isasymrbrakk \isanewline
1915 \isaindent{\ 2.\ \ \ \ }\isasymLongrightarrow \ Br(x,\ Br(a,\ t1,\ t2),\ r)\ \isasymnoteq \ Br(a,\ t1,\ t2)
1917 Compare the form of the induction hypotheses with the corresponding ones in
1918 the previous proof. As before, to conclude requires only \isa{auto}.
1920 When there are only a few constructors, we might prefer to prove the freenness
1921 theorems for each constructor. This is simple:
1923 \isacommand{lemma}\ Br\_iff:\ "Br(a,l,r)\ =\ Br(a',l',r')\ <->\ a=a'\ \&\ l=l'\ \&\ r=r'"\isanewline
1924 \ \ \isacommand{by}\ (blast\ elim!:\ bt.free\_elims)
1926 Here we see a demonstration of freeness reasoning using
1927 \isa{bt.free\_elims}, but simpler still is just to apply \isa{auto}.
1929 An \ttindex{inductive\_cases} declaration generates instances of the
1930 case analysis rule that have been simplified using freeness
1933 \isacommand{inductive\_cases}\ Br\_in\_bt:\ "Br(a,\ l,\ r)\ \isasymin \ bt(A)"
1935 The theorem just created is
1937 \isasymlbrakk Br(a,\ l,\ r)\ \isasymin \ bt(A);\ \isasymlbrakk a\ \isasymin \ A;\ l\ \isasymin \ bt(A);\ r\ \isasymin \ bt(A)\isasymrbrakk \ \isasymLongrightarrow \ Q\isasymrbrakk \ \isasymLongrightarrow \ Q.
1939 It is an elimination rule that from $\isa{Br}(a,l,r)\in\isa{bt}(A)$
1940 lets us infer $a\in A$, $l\in\isa{bt}(A)$ and
1944 \subsubsection{Mixfix syntax in datatypes}
1946 Mixfix syntax is sometimes convenient. The theory \isa{Induct/PropLog} makes a
1947 deep embedding of propositional logic:
1948 \begin{alltt*}\isastyleminor
1950 datatype "prop" = Fls
1951 | Var ("n \isasymin nat") ("#_" [100] 100)
1952 | "=>" ("p \isasymin prop", "q \isasymin prop") (infixr 90)
1954 The second constructor has a special $\#n$ syntax, while the third constructor
1955 is an infixed arrow.
1958 \subsubsection{A giant enumeration type}
1960 This example shows a datatype that consists of 60 constructors:
1961 \begin{alltt*}\isastyleminor
1964 "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
1965 | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
1966 | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
1967 | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
1968 | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
1969 | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
1972 The datatype package scales well. Even though all properties are proved
1973 rather than assumed, full processing of this definition takes around two seconds
1974 (on a 1.8GHz machine). The constructors have a balanced representation,
1975 related to binary notation, so freeness properties can be proved fast.
1977 \isacommand{lemma}\ "C00 \isasymnoteq\ C01"\isanewline
1978 \ \ \isacommand{by}\ simp
1980 You need not derive such inequalities explicitly. The simplifier will
1981 dispose of them automatically.
1986 \subsection{Recursive function definitions}\label{sec:ZF:recursive}
1987 \index{recursive functions|see{recursion}}
1989 \index{recursion!primitive|(}
1991 Datatypes come with a uniform way of defining functions, {\bf primitive
1992 recursion}. Such definitions rely on the recursion operator defined by the
1993 datatype package. Isabelle proves the desired recursion equations as
1996 In principle, one could introduce primitive recursive functions by asserting
1997 their reduction rules as axioms. Here is a dangerous way of defining a
1998 recursive function over binary trees:
2000 \isacommand{consts}\ \ n\_nodes\ ::\ "i\ =>\ i"\isanewline
2001 \isacommand{axioms}\isanewline
2002 \ \ n\_nodes\_Lf:\ "n\_nodes(Lf)\ =\ 0"\isanewline
2003 \ \ n\_nodes\_Br:\ "n\_nodes(Br(a,l,r))\ =\ succ(n\_nodes(l)\ \#+\ n\_nodes(r))"
2005 Asserting axioms brings the danger of accidentally introducing
2006 contradictions. It should be avoided whenever possible.
2008 The \ttindex{primrec} declaration is a safe means of defining primitive
2009 recursive functions on datatypes:
2011 \isacommand{consts}\ \ n\_nodes\ ::\ "i\ =>\ i"\isanewline
2012 \isacommand{primrec}\isanewline
2013 \ \ "n\_nodes(Lf)\ =\ 0"\isanewline
2014 \ \ "n\_nodes(Br(a,\ l,\ r))\ =\ succ(n\_nodes(l)\ \#+\ n\_nodes(r))"
2016 Isabelle will now derive the two equations from a low-level definition
2017 based upon well-founded recursion. If they do not define a legitimate
2018 recursion, then Isabelle will reject the declaration.
2021 \subsubsection{Syntax of recursive definitions}
2023 The general form of a primitive recursive definition is
2024 \begin{ttbox}\isastyleminor
2026 {\it reduction rules}
2028 where \textit{reduction rules} specify one or more equations of the form
2029 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
2030 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
2031 contains only the free variables on the left-hand side, and all recursive
2032 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$.
2033 There must be at most one reduction rule for each constructor. The order is
2034 immaterial. For missing constructors, the function is defined to return zero.
2036 All reduction rules are added to the default simpset.
2037 If you would like to refer to some rule by name, then you must prefix
2038 the rule with an identifier. These identifiers, like those in the
2039 \isa{rules} section of a theory, will be visible in proof scripts.
2041 The reduction rules become part of the default simpset, which
2042 leads to short proof scripts:
2044 \isacommand{lemma}\ n\_nodes\_type\ [simp]:\ "t\ \isasymin \ bt(A)\ ==>\ n\_nodes(t)\ \isasymin \ nat"\isanewline
2045 \ \ \isacommand{by}\ (induct\_tac\ t,\ auto)
2048 You can even use the \isa{primrec} form with non-recursive datatypes and
2049 with codatatypes. Recursion is not allowed, but it provides a convenient
2050 syntax for defining functions by cases.
2053 \subsubsection{Example: varying arguments}
2055 All arguments, other than the recursive one, must be the same in each equation
2056 and in each recursive call. To get around this restriction, use explict
2057 $\lambda$-abstraction and function application. For example, let us
2058 define the tail-recursive version of \isa{n\_nodes}, using an
2059 accumulating argument for the counter. The second argument, $k$, varies in
2062 \isacommand{consts}\ \ n\_nodes\_aux\ ::\ "i\ =>\ i"\isanewline
2063 \isacommand{primrec}\isanewline
2064 \ \ "n\_nodes\_aux(Lf)\ =\ (\isasymlambda k\ \isasymin \ nat.\ k)"\isanewline
2065 \ \ "n\_nodes\_aux(Br(a,l,r))\ =\ \isanewline
2066 \ \ \ \ \ \ (\isasymlambda k\ \isasymin \ nat.\ n\_nodes\_aux(r)\ `\ \ (n\_nodes\_aux(l)\ `\ succ(k)))"
2068 Now \isa{n\_nodes\_aux(t)\ `\ k} is our function in two arguments. We
2069 can prove a theorem relating it to \isa{n\_nodes}. Note the quantification
2070 over \isa{k\ \isasymin \ nat}:
2072 \isacommand{lemma}\ n\_nodes\_aux\_eq\ [rule\_format]:\isanewline
2073 \ \ \ \ \ "t\ \isasymin \ bt(A)\ ==>\ \isasymforall k\ \isasymin \ nat.\ n\_nodes\_aux(t)`k\ =\ n\_nodes(t)\ \#+\ k"\isanewline
2074 \ \ \isacommand{by}\ (induct\_tac\ t,\ simp\_all)
2077 Now, we can use \isa{n\_nodes\_aux} to define a tail-recursive version
2080 \isacommand{constdefs}\isanewline
2081 \ \ n\_nodes\_tail\ ::\ "i\ =>\ i"\isanewline
2082 \ \ \ "n\_nodes\_tail(t)\ ==\ n\_nodes\_aux(t)\ `\ 0"
2085 prove that \isa{n\_nodes\_tail} is equivalent to \isa{n\_nodes}:
2087 \isacommand{lemma}\ "t\ \isasymin \ bt(A)\ ==>\ n\_nodes\_tail(t)\ =\ n\_nodes(t)"\isanewline
2088 \ \isacommand{by}\ (simp\ add:\ n\_nodes\_tail\_def\ n\_nodes\_aux\_eq)
2094 \index{recursion!primitive|)}
2098 \section{Inductive and coinductive definitions}
2099 \index{*inductive|(}
2100 \index{*coinductive|(}
2102 An {\bf inductive definition} specifies the least set~$R$ closed under given
2103 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
2104 example, a structural operational semantics is an inductive definition of an
2105 evaluation relation. Dually, a {\bf coinductive definition} specifies the
2106 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
2107 seen as arising by applying a rule to elements of~$R$.) An important example
2108 is using bisimulation relations to formalise equivalence of processes and
2109 infinite data structures.
2111 A theory file may contain any number of inductive and coinductive
2112 definitions. They may be intermixed with other declarations; in
2113 particular, the (co)inductive sets {\bf must} be declared separately as
2114 constants, and may have mixfix syntax or be subject to syntax translations.
2116 Each (co)inductive definition adds definitions to the theory and also
2117 proves some theorems. It behaves identially to the analogous
2118 inductive definition except that instead of an induction rule there is
2119 a coinduction rule. Its treatment of coinduction is described in
2120 detail in a separate paper,%
2121 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
2122 distributed with Isabelle as \emph{A Fixedpoint Approach to
2123 (Co)Inductive and (Co)Datatype Definitions}.} %
2124 which you might refer to for background information.
2127 \subsection{The syntax of a (co)inductive definition}
2128 An inductive definition has the form
2129 \begin{ttbox}\isastyleminor
2131 domains {\it domain declarations}
2132 intros {\it introduction rules}
2133 monos {\it monotonicity theorems}
2134 con_defs {\it constructor definitions}
2135 type_intros {\it introduction rules for type-checking}
2136 type_elims {\it elimination rules for type-checking}
2138 A coinductive definition is identical, but starts with the keyword
2139 \isa{co\-inductive}.
2141 The \isa{monos}, \isa{con\_defs}, \isa{type\_intros} and \isa{type\_elims}
2142 sections are optional. If present, each is specified as a list of
2143 theorems, which may contain Isar attributes as usual.
2146 \item[\it domain declarations] are items of the form
2147 {\it string\/}~\isa{\isasymsubseteq }~{\it string}, associating each recursive set with
2148 its domain. (The domain is some existing set that is large enough to
2149 hold the new set being defined.)
2151 \item[\it introduction rules] specify one or more introduction rules in
2152 the form {\it ident\/}~{\it string}, where the identifier gives the name of
2153 the rule in the result structure.
2155 \item[\it monotonicity theorems] are required for each operator applied to
2156 a recursive set in the introduction rules. There \textbf{must} be a theorem
2157 of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each premise $t\in M(R_i)$
2158 in an introduction rule!
2160 \item[\it constructor definitions] contain definitions of constants
2161 appearing in the introduction rules. The (co)datatype package supplies
2162 the constructors' definitions here. Most (co)inductive definitions omit
2163 this section; one exception is the primitive recursive functions example;
2164 see theory \isa{Induct/Primrec}.
2166 \item[\it type\_intros] consists of introduction rules for type-checking the
2167 definition: for demonstrating that the new set is included in its domain.
2168 (The proof uses depth-first search.)
2170 \item[\it type\_elims] consists of elimination rules for type-checking the
2171 definition. They are presumed to be safe and are applied as often as
2172 possible prior to the \isa{type\_intros} search.
2175 The package has a few restrictions:
2177 \item The theory must separately declare the recursive sets as
2180 \item The names of the recursive sets must be identifiers, not infix
2183 \item Side-conditions must not be conjunctions. However, an introduction rule
2184 may contain any number of side-conditions.
2186 \item Side-conditions of the form $x=t$, where the variable~$x$ does not
2187 occur in~$t$, will be substituted through the rule \isa{mutual\_induct}.
2191 \subsection{Example of an inductive definition}
2193 Below, we shall see how Isabelle/ZF defines the finite powerset
2194 operator. The first step is to declare the constant~\isa{Fin}. Then we
2195 must declare it inductively, with two introduction rules:
2197 \isacommand{consts}\ \ Fin\ ::\ "i=>i"\isanewline
2198 \isacommand{inductive}\isanewline
2199 \ \ \isakeyword{domains}\ \ \ "Fin(A)"\ \isasymsubseteq\ "Pow(A)"\isanewline
2200 \ \ \isakeyword{intros}\isanewline
2201 \ \ \ \ emptyI:\ \ "0\ \isasymin\ Fin(A)"\isanewline
2202 \ \ \ \ consI:\ \ \ "[|\ a\ \isasymin\ A;\ \ b\ \isasymin\ Fin(A)\ |]\ ==>\ cons(a,b)\ \isasymin\ Fin(A)"\isanewline
2203 \ \ \isakeyword{type\_intros}\ \ empty\_subsetI\ cons\_subsetI\ PowI\isanewline
2204 \ \ \isakeyword{type\_elims}\ \ \ PowD\ [THEN\ revcut\_rl]\end{isabelle}
2205 The resulting theory contains a name space, called~\isa{Fin}.
2206 The \isa{Fin}$~A$ introduction rules can be referred to collectively as
2207 \isa{Fin.intros}, and also individually as \isa{Fin.emptyI} and
2208 \isa{Fin.consI}. The induction rule is \isa{Fin.induct}.
2210 The chief problem with making (co)inductive definitions involves type-checking
2211 the rules. Sometimes, additional theorems need to be supplied under
2212 \isa{type_intros} or \isa{type_elims}. If the package fails when trying
2213 to prove your introduction rules, then set the flag \ttindexbold{trace_induct}
2214 to \isa{true} and try again. (See the manual \emph{A Fixedpoint Approach
2215 \ldots} for more discussion of type-checking.)
2217 In the example above, $\isa{Pow}(A)$ is given as the domain of
2218 $\isa{Fin}(A)$, for obviously every finite subset of~$A$ is a subset
2219 of~$A$. However, the inductive definition package can only prove that given a
2221 Here is the output that results (with the flag set) when the
2222 \isa{type_intros} and \isa{type_elims} are omitted from the inductive
2224 \begin{alltt*}\isastyleminor
2225 Inductive definition Finite.Fin
2228 \%X. {z\isasymin{}Pow(A) . z = 0 | ({\isasymexists}a b. z = cons(a,b) & a\isasymin{}A & b\isasymin{}X)})
2229 Proving monotonicity...
2231 Proving the introduction rules...
2232 The type-checking subgoal:
2234 1. 0 \isasymin Pow(A)
2236 The subgoal after monos, type_elims:
2238 1. 0 \isasymin Pow(A)
2239 *** prove_goal: tactic failed
2241 We see the need to supply theorems to let the package prove
2242 $\emptyset\in\isa{Pow}(A)$. Restoring the \isa{type_intros} but not the
2243 \isa{type_elims}, we again get an error message:
2244 \begin{alltt*}\isastyleminor
2245 The type-checking subgoal:
2247 1. 0 \isasymin Pow(A)
2249 The subgoal after monos, type_elims:
2251 1. 0 \isasymin Pow(A)
2253 The type-checking subgoal:
2254 cons(a, b) \isasymin Fin(A)
2255 1. [| a \isasymin A; b \isasymin Fin(A) |] ==> cons(a, b) \isasymin Pow(A)
2257 The subgoal after monos, type_elims:
2258 cons(a, b) \isasymin Fin(A)
2259 1. [| a \isasymin A; b \isasymin Pow(A) |] ==> cons(a, b) \isasymin Pow(A)
2260 *** prove_goal: tactic failed
2262 The first rule has been type-checked, but the second one has failed. The
2263 simplest solution to such problems is to prove the failed subgoal separately
2264 and to supply it under \isa{type_intros}. The solution actually used is
2265 to supply, under \isa{type_elims}, a rule that changes
2266 $b\in\isa{Pow}(A)$ to $b\subseteq A$; together with \isa{cons_subsetI}
2267 and \isa{PowI}, it is enough to complete the type-checking.
2271 \subsection{Further examples}
2273 An inductive definition may involve arbitrary monotonic operators. Here is a
2274 standard example: the accessible part of a relation. Note the use
2275 of~\isa{Pow} in the introduction rule and the corresponding mention of the
2276 rule \isa{Pow\_mono} in the \isa{monos} list. If the desired rule has a
2277 universally quantified premise, usually the effect can be obtained using
2280 \isacommand{consts}\ \ acc\ ::\ "i\ =>\ i"\isanewline
2281 \isacommand{inductive}\isanewline
2282 \ \ \isakeyword{domains}\ "acc(r)"\ \isasymsubseteq \ "field(r)"\isanewline
2283 \ \ \isakeyword{intros}\isanewline
2284 \ \ \ \ vimage:\ \ "[|\ r-``\isacharbraceleft a\isacharbraceright\ \isasymin\ Pow(acc(r));\ a\ \isasymin \ field(r)\ |]
2286 \ \ \ \ \ \ \ \ \ \ \ \ \ \ ==>\ a\ \isasymin \ acc(r)"\isanewline
2287 \ \ \isakeyword{monos}\ \ Pow\_mono
2290 Finally, here are some coinductive definitions. We begin by defining
2291 lazy (potentially infinite) lists as a codatatype:
2293 \isacommand{consts}\ \ llist\ \ ::\ "i=>i"\isanewline
2294 \isacommand{codatatype}\isanewline
2295 \ \ "llist(A)"\ =\ LNil\ |\ LCons\ ("a\ \isasymin \ A",\ "l\ \isasymin \ llist(A)")\isanewline
2298 The notion of equality on such lists is modelled as a bisimulation:
2300 \isacommand{consts}\ \ lleq\ ::\ "i=>i"\isanewline
2301 \isacommand{coinductive}\isanewline
2302 \ \ \isakeyword{domains}\ "lleq(A)"\ <=\ "llist(A)\ *\ llist(A)"\isanewline
2303 \ \ \isakeyword{intros}\isanewline
2304 \ \ \ \ LNil:\ \ "<LNil,\ LNil>\ \isasymin \ lleq(A)"\isanewline
2305 \ \ \ \ LCons:\ "[|\ a\ \isasymin \ A;\ <l,l'>\ \isasymin \ lleq(A)\ |]\ \isanewline
2306 \ \ \ \ \ \ \ \ \ \ \ \ ==>\ <LCons(a,l),\ LCons(a,l')>\ \isasymin \ lleq(A)"\isanewline
2307 \ \ \isakeyword{type\_intros}\ \ llist.intros
2309 This use of \isa{type_intros} is typical: the relation concerns the
2310 codatatype \isa{llist}, so naturally the introduction rules for that
2311 codatatype will be required for type-checking the rules.
2313 The Isabelle distribution contains many other inductive definitions. Simple
2314 examples are collected on subdirectory \isa{ZF/Induct}. The directory
2315 \isa{Coind} and the theory \isa{ZF/Induct/LList} contain coinductive
2316 definitions. Larger examples may be found on other subdirectories of
2317 \isa{ZF}, such as \isa{IMP}, and \isa{Resid}.
2320 \subsection{Theorems generated}
2322 Each (co)inductive set defined in a theory file generates a name space
2323 containing the following elements:
2324 \begin{ttbox}\isastyleminor
2325 intros \textrm{the introduction rules}
2326 elim \textrm{the elimination (case analysis) rule}
2327 induct \textrm{the standard induction rule}
2328 mutual_induct \textrm{the mutual induction rule, if needed}
2329 defs \textrm{definitions of inductive sets}
2330 bnd_mono \textrm{monotonicity property}
2331 dom_subset \textrm{inclusion in `bounding set'}
2333 Furthermore, each introduction rule is available under its declared
2334 name. For a codatatype, the component \isa{coinduct} is the coinduction rule,
2335 replacing the \isa{induct} component.
2337 Recall that the \ttindex{inductive\_cases} declaration generates
2338 simplified instances of the case analysis rule. It is as useful for
2339 inductive definitions as it is for datatypes. There are many examples
2341 \isa{Induct/Comb}, which is discussed at length
2342 elsewhere~\cite{paulson-generic}. The theory first defines the
2344 \isa{comb} of combinators:
2345 \begin{alltt*}\isastyleminor
2349 | "#" ("p \isasymin comb", "q \isasymin comb") (infixl 90)
2351 The theory goes on to define contraction and parallel contraction
2352 inductively. Then the theory \isa{Induct/Comb.thy} defines special
2353 cases of contraction, such as this one:
2355 \isacommand{inductive\_cases}\ K\_contractE [elim!]:\ "K -1-> r"
2357 The theorem just created is \isa{K -1-> r \ \isasymLongrightarrow \ Q},
2358 which expresses that the combinator \isa{K} cannot reduce to
2359 anything. (From the assumption \isa{K-1->r}, we can conclude any desired
2360 formula \isa{Q}\@.) Similar elimination rules for \isa{S} and application are also
2361 generated. The attribute \isa{elim!}\ shown above supplies the generated
2362 theorem to the classical reasoner. This mode of working allows
2363 effective reasoniung about operational semantics.
2365 \index{*coinductive|)} \index{*inductive|)}
2369 \section{The outer reaches of set theory}
2371 The constructions of the natural numbers and lists use a suite of
2372 operators for handling recursive function definitions. I have described
2373 the developments in detail elsewhere~\cite{paulson-set-II}. Here is a brief
2376 \item Theory \isa{Trancl} defines the transitive closure of a relation
2377 (as a least fixedpoint).
2379 \item Theory \isa{WF} proves the well-founded recursion theorem, using an
2380 elegant approach of Tobias Nipkow. This theorem permits general
2381 recursive definitions within set theory.
2383 \item Theory \isa{Ord} defines the notions of transitive set and ordinal
2384 number. It derives transfinite induction. A key definition is {\bf
2385 less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and
2386 $i\in j$. As a special case, it includes less than on the natural
2389 \item Theory \isa{Epsilon} derives $\varepsilon$-induction and
2390 $\varepsilon$-recursion, which are generalisations of transfinite
2391 induction and recursion. It also defines \cdx{rank}$(x)$, which is the
2392 least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ of
2393 the cumulative hierarchy (thus $x\in V@{\alpha+1}$).
2396 Other important theories lead to a theory of cardinal numbers. They have
2397 not yet been written up anywhere. Here is a summary:
2399 \item Theory \isa{Rel} defines the basic properties of relations, such as
2400 reflexivity, symmetry and transitivity.
2402 \item Theory \isa{EquivClass} develops a theory of equivalence
2403 classes, not using the Axiom of Choice.
2405 \item Theory \isa{Order} defines partial orderings, total orderings and
2408 \item Theory \isa{OrderArith} defines orderings on sum and product sets.
2409 These can be used to define ordinal arithmetic and have applications to
2410 cardinal arithmetic.
2412 \item Theory \isa{OrderType} defines order types. Every wellordering is
2413 equivalent to a unique ordinal, which is its order type.
2415 \item Theory \isa{Cardinal} defines equipollence and cardinal numbers.
2417 \item Theory \isa{CardinalArith} defines cardinal addition and
2418 multiplication, and proves their elementary laws. It proves that there
2419 is no greatest cardinal. It also proves a deep result, namely
2420 $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see
2421 Kunen~\cite[page 29]{kunen80}. None of these results assume the Axiom of
2422 Choice, which complicates their proofs considerably.
2425 The following developments involve the Axiom of Choice (AC):
2427 \item Theory \isa{AC} asserts the Axiom of Choice and proves some simple
2430 \item Theory \isa{Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma
2431 and the Wellordering Theorem, following Abrial and
2432 Laffitte~\cite{abrial93}.
2434 \item Theory \isa{Cardinal\_AC} uses AC to prove simplified theorems about
2435 the cardinals. It also proves a theorem needed to justify
2436 infinitely branching datatype declarations: if $\kappa$ is an infinite
2437 cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then
2438 $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
2440 \item Theory \isa{InfDatatype} proves theorems to justify infinitely
2441 branching datatypes. Arbitrary index sets are allowed, provided their
2442 cardinalities have an upper bound. The theory also justifies some
2443 unusual cases of finite branching, involving the finite powerset operator
2444 and the finite function space operator.
2449 \section{The examples directories}
2450 Directory \isa{HOL/IMP} contains a mechanised version of a semantic
2451 equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
2452 denotational and operational semantics of a simple while-language, then
2453 proves the two equivalent. It contains several datatype and inductive
2454 definitions, and demonstrates their use.
2456 The directory \isa{ZF/ex} contains further developments in ZF set theory.
2457 Here is an overview; see the files themselves for more details. I describe
2458 much of this material in other
2459 publications~\cite{paulson-set-I,paulson-set-II,paulson-fixedpt-milner}.
2461 \item File \isa{misc.ML} contains miscellaneous examples such as
2462 Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
2463 of homomorphisms' challenge~\cite{boyer86}.
2465 \item Theory \isa{Ramsey} proves the finite exponent 2 version of
2466 Ramsey's Theorem, following Basin and Kaufmann's
2467 presentation~\cite{basin91}.
2469 \item Theory \isa{Integ} develops a theory of the integers as
2470 equivalence classes of pairs of natural numbers.
2472 \item Theory \isa{Primrec} develops some computation theory. It
2473 inductively defines the set of primitive recursive functions and presents a
2474 proof that Ackermann's function is not primitive recursive.
2476 \item Theory \isa{Primes} defines the Greatest Common Divisor of two
2477 natural numbers and and the ``divides'' relation.
2479 \item Theory \isa{Bin} defines a datatype for two's complement binary
2480 integers, then proves rewrite rules to perform binary arithmetic. For
2481 instance, $1359\times {-}2468 = {-}3354012$ takes 0.3 seconds.
2483 \item Theory \isa{BT} defines the recursive data structure $\isa{bt}(A)$, labelled binary trees.
2485 \item Theory \isa{Term} defines a recursive data structure for terms
2486 and term lists. These are simply finite branching trees.
2488 \item Theory \isa{TF} defines primitives for solving mutually
2489 recursive equations over sets. It constructs sets of trees and forests
2490 as an example, including induction and recursion rules that handle the
2493 \item Theory \isa{Prop} proves soundness and completeness of
2494 propositional logic~\cite{paulson-set-II}. This illustrates datatype
2495 definitions, inductive definitions, structural induction and rule
2498 \item Theory \isa{ListN} inductively defines the lists of $n$
2499 elements~\cite{paulin-tlca}.
2501 \item Theory \isa{Acc} inductively defines the accessible part of a
2502 relation~\cite{paulin-tlca}.
2504 \item Theory \isa{Comb} defines the datatype of combinators and
2505 inductively defines contraction and parallel contraction. It goes on to
2506 prove the Church-Rosser Theorem. This case study follows Camilleri and
2507 Melham~\cite{camilleri92}.
2509 \item Theory \isa{LList} defines lazy lists and a coinduction
2510 principle for proving equations between them.
2514 \section{A proof about powersets}\label{sec:ZF-pow-example}
2515 To demonstrate high-level reasoning about subsets, let us prove the
2516 equation ${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$. Compared
2517 with first-order logic, set theory involves a maze of rules, and theorems
2518 have many different proofs. Attempting other proofs of the theorem might
2519 be instructive. This proof exploits the lattice properties of
2520 intersection. It also uses the monotonicity of the powerset operation,
2521 from \isa{ZF/mono.ML}:
2523 \tdx{Pow_mono}: A \isasymsubseteq B ==> Pow(A) \isasymsubseteq Pow(B)
2525 We enter the goal and make the first step, which breaks the equation into
2526 two inclusions by extensionality:\index{*equalityI theorem}
2528 \isacommand{lemma}\ "Pow(A\ Int\ B)\ =\ Pow(A)\ Int\ Pow(B)"\isanewline
2529 \ 1.\ Pow(A\ \isasyminter \ B)\ =\ Pow(A)\ \isasyminter \ Pow(B)\isanewline
2530 \isacommand{apply}\ (rule\ equalityI)\isanewline
2531 \ 1.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(A)\ \isasyminter \ Pow(B)\isanewline
2532 \ 2.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B)
2534 Both inclusions could be tackled straightforwardly using \isa{subsetI}.
2535 A shorter proof results from noting that intersection forms the greatest
2536 lower bound:\index{*Int_greatest theorem}
2538 \isacommand{apply}\ (rule\ Int\_greatest)\isanewline
2539 \ 1.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(A)\isanewline
2540 \ 2.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(B)\isanewline
2541 \ 3.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B)
2543 Subgoal~1 follows by applying the monotonicity of \isa{Pow} to $A\int
2544 B\subseteq A$; subgoal~2 follows similarly:
2545 \index{*Int_lower1 theorem}\index{*Int_lower2 theorem}
2547 \isacommand{apply}\ (rule\ Int\_lower1\ [THEN\ Pow\_mono])\isanewline
2548 \ 1.\ Pow(A\ \isasyminter \ B)\ \isasymsubseteq \ Pow(B)\isanewline
2549 \ 2.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B)
2551 \isacommand{apply}\ (rule\ Int\_lower2\ [THEN\ Pow\_mono])\isanewline
2552 \ 1.\ Pow(A)\ \isasyminter \ Pow(B)\ \isasymsubseteq \ Pow(A\ \isasyminter \ B)
2554 We are left with the opposite inclusion, which we tackle in the
2555 straightforward way:\index{*subsetI theorem}
2557 \isacommand{apply}\ (rule\ subsetI)\isanewline
2558 \ 1.\ \isasymAnd x.\ x\ \isasymin \ Pow(A)\ \isasyminter \ Pow(B)\ \isasymLongrightarrow \ x\ \isasymin \ Pow(A\ \isasyminter \ B)
2560 The subgoal is to show $x\in \isa{Pow}(A\cap B)$ assuming $x\in\isa{Pow}(A)\cap \isa{Pow}(B)$; eliminating this assumption produces two
2561 subgoals. The rule \tdx{IntE} treats the intersection like a conjunction
2562 instead of unfolding its definition.
2564 \isacommand{apply}\ (erule\ IntE)\isanewline
2565 \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymin \ Pow(A);\ x\ \isasymin \ Pow(B)\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ Pow(A\ \isasyminter \ B)
2567 The next step replaces the \isa{Pow} by the subset
2568 relation~($\subseteq$).\index{*PowI theorem}
2570 \isacommand{apply}\ (rule\ PowI)\isanewline
2571 \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymin \ Pow(A);\ x\ \isasymin \ Pow(B)\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ A\ \isasyminter \ B%
2573 We perform the same replacement in the assumptions. This is a good
2574 demonstration of the tactic \ttindex{drule}:\index{*PowD theorem}
2576 \isacommand{apply}\ (drule\ PowD)+\isanewline
2577 \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymsubseteq \ A;\ x\ \isasymsubseteq \ B\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ A\ \isasyminter \ B%
2579 The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
2580 $A\int B$ is the greatest lower bound:\index{*Int_greatest theorem}
2582 \isacommand{apply}\ (rule\ Int\_greatest)\isanewline
2583 \ 1.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymsubseteq \ A;\ x\ \isasymsubseteq \ B\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ A\isanewline
2584 \ 2.\ \isasymAnd x.\ \isasymlbrakk x\ \isasymsubseteq \ A;\ x\ \isasymsubseteq \ B\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymsubseteq \ B%
2586 To conclude the proof, we clear up the trivial subgoals:
2588 \isacommand{apply}\ (assumption+)\isanewline
2592 We could have performed this proof instantly by calling
2595 \isacommand{lemma}\ "Pow(A\ Int\ B)\ =\ Pow(A)\ Int\ Pow(B)"\isanewline
2598 Past researchers regarded this as a difficult proof, as indeed it is if all
2599 the symbols are replaced by their definitions.
2602 \section{Monotonicity of the union operator}
2603 For another example, we prove that general union is monotonic:
2604 ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we
2605 tackle the inclusion using \tdx{subsetI}:
2607 \isacommand{lemma}\ "C\isasymsubseteq D\ ==>\ Union(C)\
2608 \isasymsubseteq \ Union(D)"\isanewline
2609 \isacommand{apply}\ (rule\ subsetI)\isanewline
2610 \ 1.\ \isasymAnd x.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ \isasymUnion C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ \isasymUnion D%
2612 Big union is like an existential quantifier --- the occurrence in the
2613 assumptions must be eliminated early, since it creates parameters.
2614 \index{*UnionE theorem}
2616 \isacommand{apply}\ (erule\ UnionE)\isanewline
2617 \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ \isasymUnion D%
2619 Now we may apply \tdx{UnionI}, which creates an unknown involving the
2620 parameters. To show \isa{x\ \isasymin \ \isasymUnion D} it suffices to show that~\isa{x} belongs
2621 to some element, say~\isa{?B2(x,B)}, of~\isa{D}\@.
2623 \isacommand{apply}\ (rule\ UnionI)\isanewline
2624 \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ ?B2(x,\ B)\ \isasymin \ D\isanewline
2625 \ 2.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ ?B2(x,\ B)
2627 Combining the rule \tdx{subsetD} with the assumption \isa{C\ \isasymsubseteq \ D} yields
2628 $\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1. Note that
2629 \isa{erule} removes the subset assumption.
2631 \isacommand{apply}\ (erule\ subsetD)\isanewline
2632 \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ ?B2(x,\ B)\ \isasymin \ C\isanewline
2633 \ 2.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ ?B2(x,\ B)
2635 The rest is routine. Observe how the first call to \isa{assumption}
2636 instantiates \isa{?B2(x,B)} to~\isa{B}\@.
2638 \isacommand{apply}\ assumption\ \isanewline
2639 \ 1.\ \isasymAnd x\ B.\ \isasymlbrakk C\ \isasymsubseteq \ D;\ x\ \isasymin \ B;\ B\ \isasymin \ C\isasymrbrakk \ \isasymLongrightarrow \ x\ \isasymin \ B%
2641 \isacommand{apply}\ assumption\ \isanewline
2642 No\ subgoals!\isanewline
2645 Again, \isa{blast} can prove this theorem in one step.
2647 The theory \isa{ZF/equalities.thy} has many similar proofs. Reasoning about
2648 general intersection can be difficult because of its anomalous behaviour on
2649 the empty set. However, \isa{blast} copes well with these. Here is
2650 a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
2651 \[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) =
2652 \Bigl(\inter@{x\in C} A(x)\Bigr) \int
2653 \Bigl(\inter@{x\in C} B(x)\Bigr) \]
2655 \section{Low-level reasoning about functions}
2656 The derived rules \isa{lamI}, \isa{lamE}, \isa{lam_type}, \isa{beta}
2657 and \isa{eta} support reasoning about functions in a
2658 $\lambda$-calculus style. This is generally easier than regarding
2659 functions as sets of ordered pairs. But sometimes we must look at the
2660 underlying representation, as in the following proof
2661 of~\tdx{fun_disjoint_apply1}. This states that if $f$ and~$g$ are
2662 functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
2665 \isacommand{lemma}\ "[|\ a\ \isasymin \ A;\ \ f\ \isasymin \ A->B;\ \ g\ \isasymin \ C->D;\ \ A\ \isasyminter \ C\ =\ 0\ |]
2667 \ \ \ \ \ \ \ \ ==>\ (f\ \isasymunion \ g)`a\ =\ f`a"
2669 Using \tdx{apply_equality}, we reduce the equality to reasoning about
2670 ordered pairs. The second subgoal is to verify that \isa{f\ \isasymunion \ g} is a function, since
2671 \isa{Pi(?A,?B)} denotes a dependent function space.
2673 \isacommand{apply}\ (rule\ apply\_equality)\isanewline
2674 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline
2675 \isaindent{\ 1.\ }\isasymLongrightarrow \ \isasymlangle a,\ f\ `\ a\isasymrangle \ \isasymin \ f\ \isasymunion \ g\isanewline
2676 \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline
2677 \isaindent{\ 2.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B)
2679 We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we
2682 \isacommand{apply}\ (rule\ UnI1)\isanewline
2683 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ \isasymlangle a,\ f\ `\ a\isasymrangle \ \isasymin \ f\isanewline
2684 \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline
2685 \isaindent{\ 2.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B)
2687 To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is
2688 essentially the converse of \tdx{apply_equality}:
2690 \isacommand{apply}\ (rule\ apply\_Pair)\isanewline
2691 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ f\ \isasymin \ Pi(?A2,?B2)\isanewline
2692 \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ a\ \isasymin \ ?A2\isanewline
2693 \ 3.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline
2694 \isaindent{\ 3.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B)
2696 Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals
2697 from \tdx{apply_Pair}. Recall that a $\Pi$-set is merely a generalized
2698 function space, and observe that~{\tt?A2} gets instantiated to~\isa{A}.
2700 \isacommand{apply}\ assumption\ \isanewline
2701 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ a\ \isasymin \ A\isanewline
2702 \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline
2703 \isaindent{\ 2.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B)
2705 \isacommand{apply}\ assumption\ \isanewline
2706 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \isanewline
2707 \isaindent{\ 1.\ }\isasymLongrightarrow \ f\ \isasymunion \ g\ \isasymin \ Pi(?A,\ ?B)
2709 To construct functions of the form $f\un g$, we apply
2710 \tdx{fun_disjoint_Un}:
2712 \isacommand{apply}\ (rule\ fun\_disjoint\_Un)\isanewline
2713 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ f\ \isasymin \ ?A3\ \isasymrightarrow \ ?B3\isanewline
2714 \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ g\ \isasymin \ ?C3\ \isasymrightarrow \ ?D3\isanewline
2715 \ 3.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ ?A3\ \isasyminter \ ?C3\ =\ 0
2717 The remaining subgoals are instances of the assumptions. Again, observe how
2718 unknowns become instantiated:
2720 \isacommand{apply}\ assumption\ \isanewline
2721 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ g\ \isasymin \ ?C3\ \isasymrightarrow \ ?D3\isanewline
2722 \ 2.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ A\ \isasyminter \ ?C3\ =\ 0
2724 \isacommand{apply}\ assumption\ \isanewline
2725 \ 1.\ \isasymlbrakk a\ \isasymin \ A;\ f\ \isasymin \ A\ \isasymrightarrow \ B;\ g\ \isasymin \ C\ \isasymrightarrow \ D;\ A\ \isasyminter \ C\ =\ 0\isasymrbrakk \ \isasymLongrightarrow \ A\ \isasyminter \ C\ =\ 0
2727 \isacommand{apply}\ assumption\ \isanewline
2728 No\ subgoals!\isanewline
2731 See the theories \isa{ZF/func.thy} and \isa{ZF/WF.thy} for more
2732 examples of reasoning about functions.
2734 \index{set theory|)}