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