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--
     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 \ttlbracea@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 \ttlbracex:A . P[x]\ttrbrace & Collect(A,\lambda x. P[x]) &   186 \rm separation \\   187 \ttlbracey . x:A, Q[x,y]\ttrbrace & Replace(A,\lambda x\,y. Q[x,y]) &   188 \rm replacement \\   189 \ttlbraceb[x] . x:A\ttrbrace & RepFun(A,\lambda x. b[x]) &   190 \rm functional replacement \\   191 \sdx{INT} x:A . B[x] & Inter(\ttlbraceB[x] . x:A\ttrbrace) &   192 \rm general intersection \\   193 \sdx{UN} x:A . B[x] & Union(\ttlbraceB[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}: fa         == 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. fx

   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{}rA

   841 \tdx{imageE}:      [| b\isasymin{}rA; !!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) |] ==> fa = 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 |] ==> fa\isasymin{}B(a)

   875 \tdx{apply_Pair}:     [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> <a,fa>\isasymin{}f

   876 \tdx{apply_iff}:      f\isasymin{}Pi(A,B) ==> <a,b>\isasymin{}f <-> a\isasymin{}A & fa = b

   877

   878 \tdx{fun_extension}:  [| f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D);

   879                    !!x. x\isasymin{}A ==> fx = gx     |] ==> 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 ==> fx\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 = fa

   889 \tdx{restrict_type}:  [| !!x. x\isasymin{}A ==> fx\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. fx) = 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 = fa

   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 = gc

   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 $fa=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. fw=fx --> w=x {\ttrbrace}

  1270 \tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. fx=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)(fa) = 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(ga)

  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, fC)

  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)   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 = fa$:   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\ =\ fa"   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,fa}\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|)}
`