Logics_ZF/document/ZF.tex

4 The theory~\thydx{ZF} implements Zermelo-Fraenkel set
6 first-order logic.  The theory includes a collection of derived natural
32 The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})
41 collections that are `too big' to be sets.  The class of all sets,~$V$,
45 predicates.  The two systems define essentially the same sets and classes,
81   \cdx{The}     & $[i\To o]\To i$       & definite description\\
112 \section{The syntax of set theory}
113 The language of set theory, as studied by logicians, has no constants.  The
115 powersets, etc.; this would be intolerable for practical reasoning.  The
134 class~\cldx{term}.  The type of first-order formulae, remember,
140 which is equivalent to  $a\notin b$.  The
145 The constant \cdx{Upair} constructs unordered pairs; thus \isa{Upair($A$,$B$)} denotes the set~$\{A,B\}$ and
147 used to define binary union.  The Isabelle version goes on to define
154 The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
159 The constant \cdx{Pair} constructs ordered pairs, as in \isa{Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
160 as {\tt<$a$,$b$>}.  The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
166 $i\To i$.  The infix operator~{\tt`} denotes the application of a function set
167 to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The syntax for image
202   \sdx{THE}  $x . P[x]$ & The($\lambda x. P[x]$) &
266 The constant \cdx{Collect} constructs sets by the principle of {\bf
267   separation}.  The syntax for separation is
274 The constant \cdx{Replace} constructs sets by the principle of {\bf
275   replacement}.  The syntax
278 that there exists $x\in A$ satisfying~$Q[x,y]$.  The Replacement Axiom
283 The constant \cdx{RepFun} expresses a special case of replacement,
286 function~$\lambda x. b[x]$.  The resulting set consists of all $b[x]$
288 since it applies a function to every element of a set.  The syntax is
305 has `dependent sets') and calls for similar syntactic conventions.  The
311 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
323 uniquely.  Using the constant~\cdx{The}, we may write descriptions as
324 \isa{The($\lambda x. P[x]$)} or use the syntax \isa{THE $x$.\ $P[x]$}.
337 The constants~\cdx{Ball} and~\cdx{Bex} are defined
361 \subcaption{The Zermelo-Fraenkel Axioms}
366 \tdx{the_def}:     The(P)       == Union({\ttlbrace}y . x \isasymin {\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace})
416 \section{The Zermelo-Fraenkel axioms}
417 The axioms appear in Fig.\ts \ref{zf-rules}.  They resemble those
424 The traditional replacement axiom asserts
427 The Isabelle theory defines \cdx{Replace} to apply
433 same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
438 (\cdx{RepFun}) and definite descriptions (\cdx{The}).
443 The definitions of general intersection, etc., are straightforward.  Note
445 The axiom of infinity gives us a set that contains~0 and is closed under
457 The projections \cdx{fst} and~\cdx{snd} are defined in terms of the
458 generalized projection \cdx{split}.  The latter has been borrowed from
462 Operations on relations include converse, domain, range, and image.  The
465 \cdx{RepFun}) and application (using a definite description).  The
508 \subcaption{The empty set; power sets}
525 operators.  The rules for the bounded quantifiers resemble those for the
527 in the style of Isabelle's classical reasoner.  The \rmindex{congruence
537 The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
538 comparable rules for \isa{PrimReplace} would be.  The principle of
540 natural deduction rules for \isa{Collect}.  The elimination rule
547 The empty intersection should be undefined.  We cannot have
551 arbitrary.  The rule \tdx{InterI} must have a premise to exclude
657 \caption{The successor function} \label{zf-succ}
679 of ordered pairs (Fig.\ts\ref{zf-Un}).  Set difference is also included.  The
689 function, which is defined in terms of~\isa{cons}.  The proof that
694 (Fig.\ts\ref{zf-the}).  The rule~\tdx{theI} is difficult to apply
701 the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
732 The subset relation is a complete lattice.  Unions form least upper bounds;
775 The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$.  This
777 encodings of ordered pairs.  The non-standard ordered pairs mentioned below
780 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
782 $\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
793   $z$.\ $t$))}.  The reverse translation is performed upon printing.
795   The translation between patterns and \isa{split} is performed automatically
851 of ordered pairs.  The converse of a relation~$r$ is the set of all pairs
853 {\cdx{converse}$(r)$} is its inverse.  The rules for the domain
856 some pair of the form~$\pair{x,y}$.  The range operation is similar, and
930 about.  The ZF theory provides many derived rules, which overlap more
1025 \caption{The booleans} \label{zf-bool}
1030 The next group of developments is complex and extensive, and only
1039 \isa{bool}-valued functions, for example.  The constant~\isa{1} is
1103 versions for standard ordered pairs.  The theory goes on to define a
1106 addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
1159 The Knaster-Tarski Theorem states that every monotone function over a
1162 set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
1165 numbers and the transitive closure operator.  The (co)inductive definition
1173 are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
1180 $\isa{Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs
1182 automatically.  The induction rule shown is stronger than the one proved by
1183 the package.  The theory also defines the set of all finite functions
1202 \caption{The finite set operator} \label{zf-fin}
1245 Figure~\ref{zf-list} presents the set of lists over~$A$, $\isa{list}(A)$.  The
1248 (\isa{list\_case}) and recursion operator.  The theory then defines the usual
1305 The theory \thydx{Perm} is concerned with permutations (bijections) and
1317 traditionally is written $V@\alpha$ for an ordinal~$\alpha$.  The
1333 ZF inherits simplification from FOL but adopts it for set theory.  The
1340 The default simpset used by \isa{simp} contains congruence rules for all of ZF's
1383 does this job well.  The if-then-else rule, and many similar ones, can make
1384 the classical reasoner loop.  The simplifier refuses (on principle) to
1388 The simplifier calls the type-checker to solve rewritten subgoals: this stage
1490 \caption{The natural numbers} \label{zf-nat}
1496 induction, along with a case analysis operator.  The set of natural
1505 laws, etc.  The most interesting result is perhaps the theorem $a \bmod b +
1509 operators coerce their arguments to be natural numbers.  The function
1513 $\isa{natify}(x)=0$ in all other cases.  The benefit is that the addition,
1521 The simplifier automatically cancels common terms on the opposite sides of
1555 \caption{The integers} \label{zf-int}
1575 by simplification.  The simplifier also collects similar terms, multiplying
1594 The \ttindex{datatype} definition package of ZF constructs inductive datatypes
1599 mechanisms for reasoning about freeness.  The datatype package can handle both
1662 The datatype \isa{term}, which is defined by
1669 is an example of nested recursion.  (The theorem \isa{list_mono} is proved
1695 The datatype package also provides structural induction rules.  For datatypes
1699 \isa{TF}.  The rule \isa{tree_forest.induct} performs induction over a
1710 The rule \isa{tree_forest.mutual_induct} performs induction over two
1723 above, things are a bit more complicated.  The rule \isa{term.induct}
1730 The theory \isa{Induct/Term.thy} derives two higher-level induction rules,
1742 \subsubsection{The \isa{case} operator}
1744 The package defines an operator for performing case analysis over the
1753 argument has the form $\isa{Cons}(a,l)$.  The function can be expressed as
1763 The theory syntax for datatype definitions is shown in the
1786   datatype.  The induction variable should not occur among other assumptions
1799 some assumption, for example the assumption \isa{x \isasymin \ list(A)}.  The tactics
1812 \subsubsection{The theorems proved by a datatype declaration}
1847 \subsubsection{The datatype of binary trees}
1849 Let us define the set $\isa{bt}(A)$ of binary trees over~$A$.  The theory
1918 The theorem just created is
1929 Mixfix syntax is sometimes convenient.  The theory \isa{Induct/PropLog} makes a
1937 The second constructor has a special $\#n$ syntax, while the third constructor
1955 The datatype package scales well.  Even though all properties are proved
1957 (on a 1.8GHz machine).  The constructors have a balanced representation,
1963 You need not derive such inequalities explicitly.  The simplifier will
1991 The \ttindex{primrec} declaration is a safe means of defining primitive
2006 The general form of a primitive recursive definition is
2016 There must be at most one reduction rule for each constructor.  The order is
2024 The reduction rules become part of the default simpset, which
2042 accumulating argument for the counter.  The second argument, $k$, varies in
2110 \subsection{The syntax of a (co)inductive definition}
2124 The \isa{monos}, \isa{con\_defs}, \isa{type\_intros} and \isa{type\_elims}
2131   its domain.  (The domain is some existing set that is large enough to
2144   appearing in the introduction rules.  The (co)datatype package supplies
2151   (The proof uses depth-first search.)
2158 The package has a few restrictions:
2160 \item The theory must separately declare the recursive sets as
2163 \item The names of the recursive sets must be identifiers, not infix
2177 operator.  The first step is to declare the constant~\isa{Fin}.  Then we
2188 The resulting theory contains a name space, called~\isa{Fin}.
2189 The \isa{Fin}$~A$ introduction rules can be referred to collectively as
2191 \isa{Fin.consI}.  The induction rule is \isa{Fin.induct}.
2193 The chief problem with making (co)inductive definitions involves type-checking
2215 The type-checking subgoal:
2219 The subgoal after monos, type_elims:
2228 The type-checking subgoal:
2232 The subgoal after monos, type_elims:
2236 The type-checking subgoal:
2240 The subgoal after monos, type_elims:
2245 The first rule has been type-checked, but the second one has failed.  The
2247 and to supply it under \isa{type_intros}.  The solution actually used is
2281 The notion of equality on such lists is modelled as a bisimulation:
2296 The Isabelle distribution contains many other inductive definitions.  Simple
2297 examples are collected on subdirectory \isa{ZF/Induct}.  The directory
2325 elsewhere~\cite{paulson-generic}.  The theory first defines the
2334 The theory goes on to define contraction and parallel contraction
2340 The theorem just created is \isa{K -1-> r \ \isasymLongrightarrow \ Q},
2344 generated. The attribute \isa{elim!}\ shown above supplies the generated
2352 \section{The outer reaches of set theory}
2354 The constructions of the natural numbers and lists use a suite of
2408 The following developments involve the Axiom of Choice (AC):
2425   cardinalities have an upper bound.  The theory also justifies some
2432 \section{The examples directories}
2439 The directory \isa{ZF/ex} contains further developments in ZF set theory.
2543 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
2544 subgoals.  The rule \tdx{IntE} treats the intersection like a conjunction
2550 The next step replaces the \isa{Pow} by the subset
2562 The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
2618 The rest is routine.  Observe how the first call to \isa{assumption}
2630 The theory \isa{ZF/equalities.thy} has many similar proofs.  Reasoning about
2639 The derived rules \isa{lamI}, \isa{lamE}, \isa{lam_type}, \isa{beta}
2653 ordered pairs.  The second subgoal is to verify that \isa{f\ \isasymunion \ g} is a function, since
2700 The remaining subgoals are instances of the assumptions.  Again, observe how