summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/ZF/ZF.tex

changeset 9695 | ec7d7f877712 |

parent 9584 | af21f4364c05 |

child 9836 | 56b632fd1dcd |

1.1 --- a/doc-src/ZF/ZF.tex Mon Aug 28 13:50:24 2000 +0200 1.2 +++ b/doc-src/ZF/ZF.tex Mon Aug 28 13:52:38 2000 +0200 1.3 @@ -23,10 +23,9 @@ 1.4 provides a streamlined syntax for defining primitive recursive functions over 1.5 datatypes. 1.6 1.7 -Because {\ZF} is an extension of {\FOL}, it provides the same 1.8 -packages, namely \texttt{hyp_subst_tac}, the simplifier, and the 1.9 -classical reasoner. The default simpset and claset are usually 1.10 -satisfactory. 1.11 +Because ZF is an extension of FOL, it provides the same packages, namely 1.12 +\texttt{hyp_subst_tac}, the simplifier, and the classical reasoner. The 1.13 +default simpset and claset are usually satisfactory. 1.14 1.15 Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF} 1.16 less formally than this chapter. Isabelle employs a novel treatment of 1.17 @@ -94,7 +93,7 @@ 1.18 \begin{center} 1.19 \index{*"`"` symbol} 1.20 \index{*"-"`"` symbol} 1.21 -\index{*"` symbol}\index{function applications!in \ZF} 1.22 +\index{*"` symbol}\index{function applications!in ZF} 1.23 \index{*"- symbol} 1.24 \index{*": symbol} 1.25 \index{*"<"= symbol} 1.26 @@ -111,7 +110,7 @@ 1.27 \end{tabular} 1.28 \end{center} 1.29 \subcaption{Infixes} 1.30 -\caption{Constants of {\ZF}} \label{zf-constants} 1.31 +\caption{Constants of ZF} \label{zf-constants} 1.32 \end{figure} 1.33 1.34 1.35 @@ -125,10 +124,10 @@ 1.36 bounded quantifiers. In most other respects, Isabelle implements precisely 1.37 Zermelo-Fraenkel set theory. 1.38 1.39 -Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while 1.40 +Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while 1.41 Figure~\ref{zf-trans} presents the syntax translations. Finally, 1.42 -Figure~\ref{zf-syntax} presents the full grammar for set theory, including 1.43 -the constructs of \FOL. 1.44 +Figure~\ref{zf-syntax} presents the full grammar for set theory, including the 1.45 +constructs of FOL. 1.46 1.47 Local abbreviations can be introduced by a \texttt{let} construct whose 1.48 syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into 1.49 @@ -136,7 +135,7 @@ 1.50 definition, \tdx{Let_def}. 1.51 1.52 Apart from \texttt{let}, set theory does not use polymorphism. All terms in 1.53 -{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt 1.54 +ZF have type~\tydx{i}, which is the type of individuals and has class~{\tt 1.55 term}. The type of first-order formulae, remember, is~\textit{o}. 1.56 1.57 Infix operators include binary union and intersection ($A\un B$ and 1.58 @@ -167,15 +166,15 @@ 1.59 abbreviates the nest of pairs\par\nobreak 1.60 \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}} 1.61 1.62 -In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an 1.63 -individual as far as Isabelle is concerned: its Isabelle type is~$i$, not 1.64 -say $i\To i$. The infix operator~{\tt`} denotes the application of a 1.65 -function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The 1.66 -syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$. 1.67 +In ZF, a function is a set of pairs. A ZF function~$f$ is simply an 1.68 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say 1.69 +$i\To i$. The infix operator~{\tt`} denotes the application of a function set 1.70 +to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The syntax for image 1.71 +is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$. 1.72 1.73 1.74 \begin{figure} 1.75 -\index{lambda abs@$\lambda$-abstractions!in \ZF} 1.76 +\index{lambda abs@$\lambda$-abstractions!in ZF} 1.77 \index{*"-"> symbol} 1.78 \index{*"* symbol} 1.79 \begin{center} \footnotesize\tt\frenchspacing 1.80 @@ -215,7 +214,7 @@ 1.81 \rm bounded $\exists$ 1.82 \end{tabular} 1.83 \end{center} 1.84 -\caption{Translations for {\ZF}} \label{zf-trans} 1.85 +\caption{Translations for ZF} \label{zf-trans} 1.86 \end{figure} 1.87 1.88 1.89 @@ -264,7 +263,7 @@ 1.90 & | & "EX!~" id~id^* " . " formula 1.91 \end{array} 1.92 \] 1.93 -\caption{Full grammar for {\ZF}} \label{zf-syntax} 1.94 +\caption{Full grammar for ZF} \label{zf-syntax} 1.95 \end{figure} 1.96 1.97 1.98 @@ -321,14 +320,13 @@ 1.99 no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these 1.100 abbreviations in parsing and uses them whenever possible for printing. 1.101 1.102 -\index{*THE symbol} 1.103 -As mentioned above, whenever the axioms assert the existence and uniqueness 1.104 -of a set, Isabelle's set theory declares a constant for that set. These 1.105 -constants can express the {\bf definite description} operator~$\iota 1.106 -x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists. 1.107 -Since all terms in {\ZF} denote something, a description is always 1.108 -meaningful, but we do not know its value unless $P[x]$ defines it uniquely. 1.109 -Using the constant~\cdx{The}, we may write descriptions as {\tt 1.110 +\index{*THE symbol} As mentioned above, whenever the axioms assert the 1.111 +existence and uniqueness of a set, Isabelle's set theory declares a constant 1.112 +for that set. These constants can express the {\bf definite description} 1.113 +operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, 1.114 +if such exists. Since all terms in ZF denote something, a description is 1.115 +always meaningful, but we do not know its value unless $P[x]$ defines it 1.116 +uniquely. Using the constant~\cdx{The}, we may write descriptions as {\tt 1.117 The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}. 1.118 1.119 \index{*lam symbol} 1.120 @@ -385,7 +383,7 @@ 1.121 \tdx{Diff_def} A - B == {\ttlbrace}x:A . x~:B{\ttrbrace} 1.122 \subcaption{Union, intersection, difference} 1.123 \end{ttbox} 1.124 -\caption{Rules and axioms of {\ZF}} \label{zf-rules} 1.125 +\caption{Rules and axioms of ZF} \label{zf-rules} 1.126 \end{figure} 1.127 1.128 1.129 @@ -417,7 +415,7 @@ 1.130 \tdx{restrict_def} restrict(f,A) == lam x:A. f`x 1.131 \subcaption{Functions and general product} 1.132 \end{ttbox} 1.133 -\caption{Further definitions of {\ZF}} \label{zf-defs} 1.134 +\caption{Further definitions of ZF} \label{zf-defs} 1.135 \end{figure} 1.136 1.137 1.138 @@ -515,7 +513,7 @@ 1.139 \tdx{PowD} A : Pow(B) ==> A<=B 1.140 \subcaption{The empty set; power sets} 1.141 \end{ttbox} 1.142 -\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1} 1.143 +\caption{Basic derived rules for ZF} \label{zf-lemmas1} 1.144 \end{figure} 1.145 1.146 1.147 @@ -555,7 +553,7 @@ 1.148 Figure~\ref{zf-lemmas3} presents rules for general union and intersection. 1.149 The empty intersection should be undefined. We cannot have 1.150 $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All 1.151 -expressions denote something in {\ZF} set theory; the definition of 1.152 +expressions denote something in ZF set theory; the definition of 1.153 intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is 1.154 arbitrary. The rule \tdx{InterI} must have a premise to exclude 1.155 the empty intersection. Some of the laws governing intersections require 1.156 @@ -1051,7 +1049,7 @@ 1.157 See file \texttt{ZF/equalities.ML}. 1.158 1.159 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual 1.160 -operators including a conditional (Fig.\ts\ref{zf-bool}). Although {\ZF} is a 1.161 +operators including a conditional (Fig.\ts\ref{zf-bool}). Although ZF is a 1.162 first-order theory, you can obtain the effect of higher-order logic using 1.163 \texttt{bool}-valued functions, for example. The constant~\texttt{1} is 1.164 translated to \texttt{succ(0)}. 1.165 @@ -1343,13 +1341,13 @@ 1.166 1.167 \section{Automatic Tools} 1.168 1.169 -{\ZF} provides the simplifier and the classical reasoner. Moreover it 1.170 -supplies a specialized tool to infer `types' of terms. 1.171 +ZF provides the simplifier and the classical reasoner. Moreover it supplies a 1.172 +specialized tool to infer `types' of terms. 1.173 1.174 \subsection{Simplification} 1.175 1.176 -{\ZF} inherits simplification from {\FOL} but adopts it for set theory. The 1.177 -extraction of rewrite rules takes the {\ZF} primitives into account. It can 1.178 +ZF inherits simplification from FOL but adopts it for set theory. The 1.179 +extraction of rewrite rules takes the ZF primitives into account. It can 1.180 strip bounded universal quantifiers from a formula; for example, ${\forall 1.181 x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp 1.182 f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in 1.183 @@ -1360,10 +1358,9 @@ 1.184 works for most purposes. A small simplification set for set theory is 1.185 called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal 1.186 starting point. \texttt{ZF_ss} contains congruence rules for all the binding 1.187 -operators of {\ZF}\@. It contains all the conversion rules, such as 1.188 -\texttt{fst} and \texttt{snd}, as well as the rewrites shown in 1.189 -Fig.\ts\ref{zf-simpdata}. See the file \texttt{ZF/simpdata.ML} for a fuller 1.190 -list. 1.191 +operators of ZF. It contains all the conversion rules, such as \texttt{fst} 1.192 +and \texttt{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}. 1.193 +See the file \texttt{ZF/simpdata.ML} for a fuller list. 1.194 1.195 1.196 \subsection{Classical Reasoning} 1.197 @@ -1396,7 +1393,7 @@ 1.198 \subsection{Type-Checking Tactics} 1.199 \index{type-checking tactics} 1.200 1.201 -Isabelle/{\ZF} provides simple tactics to help automate those proofs that are 1.202 +Isabelle/ZF provides simple tactics to help automate those proofs that are 1.203 essentially type-checking. Such proofs are built by applying rules such as 1.204 these: 1.205 \begin{ttbox} 1.206 @@ -1614,13 +1611,13 @@ 1.207 \label{sec:ZF:datatype} 1.208 \index{*datatype|(} 1.209 1.210 -The \ttindex{datatype} definition package of \ZF\ constructs inductive 1.211 -datatypes similar to those of \ML. It can also construct coinductive 1.212 -datatypes (codatatypes), which are non-well-founded structures such as 1.213 -streams. It defines the set using a fixed-point construction and proves 1.214 -induction rules, as well as theorems for recursion and case combinators. It 1.215 -supplies mechanisms for reasoning about freeness. The datatype package can 1.216 -handle both mutual and indirect recursion. 1.217 +The \ttindex{datatype} definition package of ZF constructs inductive datatypes 1.218 +similar to those of \ML. It can also construct coinductive datatypes 1.219 +(codatatypes), which are non-well-founded structures such as streams. It 1.220 +defines the set using a fixed-point construction and proves induction rules, 1.221 +as well as theorems for recursion and case combinators. It supplies 1.222 +mechanisms for reasoning about freeness. The datatype package can handle both 1.223 +mutual and indirect recursion. 1.224 1.225 1.226 \subsection{Basics} 1.227 @@ -2440,10 +2437,10 @@ 1.228 proves the two equivalent. It contains several datatype and inductive 1.229 definitions, and demonstrates their use. 1.230 1.231 -The directory \texttt{ZF/ex} contains further developments in {\ZF} set 1.232 -theory. Here is an overview; see the files themselves for more details. I 1.233 -describe much of this material in other 1.234 -publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 1.235 +The directory \texttt{ZF/ex} contains further developments in ZF set theory. 1.236 +Here is an overview; see the files themselves for more details. I describe 1.237 +much of this material in other 1.238 +publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 1.239 \begin{itemize} 1.240 \item File \texttt{misc.ML} contains miscellaneous examples such as 1.241 Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition