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