Logics_ZF/document/ZF.tex

322 always meaningful, but we do not know its value unless $P[x]$ defines it
332 Isabelle's set theory defines two {\bf bounded quantifiers}:
427 The Isabelle theory defines \cdx{Replace} to apply
432 \isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the
1036 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
1074 Theory \thydx{Sum} defines the disjoint union of two sets, with
1098 Theory \thydx{QPair} defines a notion of ordered pair that admits
1100 {\tt<$a$;$b$>}.  It also defines the eliminator \cdx{qsplit}, the
1162 set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
1179 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
1183 the package.  The theory also defines the set of all finite functions
1246 definition employs Isabelle's datatype package, which defines the introduction
1248 (\isa{list\_case}) and recursion operator.  The theory then defines the usual
1312 Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by
1316 defines the cumulative hierarchy of axiomatic set theory, which
1320 Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by
1495 Theory \thydx{Nat} defines the natural numbers and mathematical
1561 Theory \thydx{Int} defines the integers, as equivalence classes of natural
1597 defines the set using a fixed-point construction and proves induction rules,
1744 The package defines an operator for performing case analysis over the
2176 Below, we shall see how Isabelle/ZF defines the finite powerset
2325 elsewhere~\cite{paulson-generic}.  The theory first defines the
2335 inductively.  Then the theory \isa{Induct/Comb.thy} defines special
2359   \item Theory \isa{Trancl} defines the transitive closure of a relation
2366   \item Theory \isa{Ord} defines the notions of transitive set and ordinal
2374     induction and recursion.  It also defines \cdx{rank}$(x)$, which is the
2382 \item Theory \isa{Rel} defines the basic properties of relations, such as
2388 \item Theory \isa{Order} defines partial orderings, total orderings and
2391 \item Theory \isa{OrderArith} defines orderings on sum and product sets.
2395 \item Theory \isa{OrderType} defines order types.  Every wellordering is
2398 \item Theory \isa{Cardinal} defines equipollence and cardinal numbers.
2400 \item Theory \isa{CardinalArith} defines cardinal addition and
2456   inductively defines the set of primitive recursive functions and presents a
2459 \item Theory \isa{Primes} defines the Greatest Common Divisor of two
2462 \item Theory \isa{Bin} defines a datatype for two's complement binary
2466 \item Theory \isa{BT} defines the recursive data structure $\isa{bt}(A)$, labelled binary trees.
2468 \item Theory \isa{Term} defines a recursive data structure for terms
2471 \item Theory \isa{TF} defines primitives for solving mutually
2481 \item Theory \isa{ListN} inductively defines the lists of $n$
2484 \item Theory \isa{Acc} inductively defines the accessible part of a
2487 \item Theory \isa{Comb} defines the datatype of combinators and
2488   inductively defines contraction and parallel contraction.  It goes on to
2492 \item Theory \isa{LList} defines lazy lists and a coinduction