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