1.1 --- a/doc-src/Logics/ZF.tex Sun Apr 24 11:30:00 1994 +0200
1.2 +++ b/doc-src/Logics/ZF.tex Mon Apr 25 11:05:58 1994 +0200
1.3 @@ -32,7 +32,7 @@
1.4
1.5 Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less
1.6 formally than this chapter. Isabelle employs a novel treatment of
1.7 -non-well-founded data structures within the standard ZF axioms including
1.8 +non-well-founded data structures within the standard {\sc zf} axioms including
1.9 the Axiom of Foundation~\cite{paulson-final}.
1.10
1.11
1.12 @@ -337,7 +337,7 @@
1.13 \hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}.
1.14
1.15
1.16 -%%%% zf.thy
1.17 +%%%% ZF.thy
1.18
1.19 \begin{figure}
1.20 \begin{ttbox}
1.21 @@ -414,7 +414,7 @@
1.22 definitions. In particular, bounded quantifiers and the subset relation
1.23 appear in other axioms. Object-level quantifiers and implications have
1.24 been replaced by meta-level ones wherever possible, to simplify use of the
1.25 -axioms. See the file {\tt ZF/zf.thy} for details.
1.26 +axioms. See the file {\tt ZF/ZF.thy} for details.
1.27
1.28 The traditional replacement axiom asserts
1.29 \[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
1.30 @@ -517,9 +517,9 @@
1.31 \subsection{Fundamental lemmas}
1.32 Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
1.33 operators. The rules for the bounded quantifiers resemble those for the
1.34 -ordinary quantifiers, but note that \tdx{ballE} uses a negated
1.35 -assumption in the style of Isabelle's classical reasoner. The congruence rules
1.36 -\tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
1.37 +ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption
1.38 +in the style of Isabelle's classical reasoner. The \rmindex{congruence
1.39 + rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
1.40 simplifier, but have few other uses. Congruence rules must be specially
1.41 derived for all binding operators, and henceforth will not be shown.
1.42
1.43 @@ -536,7 +536,7 @@
1.44 \tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to
1.45 particular circumstances. Although too many rules can be confusing, there
1.46 is no reason to aim for a minimal set of rules. See the file
1.47 -{\tt ZF/zf.ML} for a complete listing.
1.48 +{\tt ZF/ZF.ML} for a complete listing.
1.49
1.50 Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
1.51 The empty intersection should be undefined. We cannot have
1.52 @@ -772,7 +772,7 @@
1.53
1.54 The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This
1.55 is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other
1.56 -encoding of ordered pairs. The non-standard ordered pairs mentioned below
1.57 +encodings of ordered pairs. The non-standard ordered pairs mentioned below
1.58 satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
1.59
1.60 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
1.61 @@ -825,13 +825,13 @@
1.62 of ordered pairs. The converse of a relation~$r$ is the set of all pairs
1.63 $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
1.64 {\cdx{converse}$(r)$} is its inverse. The rules for the domain
1.65 -operation, \tdx{domainI} and~\tdx{domainE}, assert that
1.66 -\cdx{domain}$(r)$ consists of every element~$a$ such that $r$ contains
1.67 +operation, namely \tdx{domainI} and~\tdx{domainE}, assert that
1.68 +\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains
1.69 some pair of the form~$\pair{x,y}$. The range operation is similar, and
1.70 the field of a relation is merely the union of its domain and range.
1.71
1.72 Figure~\ref{zf-domrange2} presents rules for images and inverse images.
1.73 -Note that these operations are generalizations of range and domain,
1.74 +Note that these operations are generalisations of range and domain,
1.75 respectively. See the file {\tt ZF/domrange.ML} for derivations of the
1.76 rules.
1.77
1.78 @@ -1019,6 +1019,7 @@
1.79 \begin{figure}
1.80 \index{*"+ symbol}
1.81 \begin{constants}
1.82 + \it symbol & \it meta-type & \it priority & \it description \\
1.83 \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\
1.84 \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\
1.85 \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$
1.86 @@ -1293,7 +1294,7 @@
1.87 set of all finite sets over~$A$. The definition employs Isabelle's
1.88 inductive definition package~\cite{paulson-fixedpt}, which proves various
1.89 rules automatically. The induction rule shown is stronger than the one
1.90 -proved by the package. See file {\tt ZF/fin.ML}.
1.91 +proved by the package. See file {\tt ZF/Fin.ML}.
1.92
1.93 \begin{figure}
1.94 \begin{ttbox}
1.95 @@ -1370,8 +1371,8 @@
1.96 Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$.
1.97 The definition employs Isabelle's datatype package, which defines the
1.98 introduction and induction rules automatically, as well as the constructors
1.99 -and case operator (\verb|list_case|). See file {\tt ZF/list.ML}.
1.100 -The file {\tt ZF/listfn.thy} proceeds to define structural
1.101 +and case operator (\verb|list_case|). See file {\tt ZF/List.ML}.
1.102 +The file {\tt ZF/ListFn.thy} proceeds to define structural
1.103 recursion and the usual list functions.
1.104
1.105 The constructions of the natural numbers and lists make use of a suite of
1.106 @@ -1393,10 +1394,10 @@
1.107 numbers.
1.108
1.109 \item Theory {\tt Epsilon} derives $\epsilon$-induction and
1.110 - $\epsilon$-recursion, which are generalizations of transfinite
1.111 - induction. It also defines \cdx{rank}$(x)$, which is the least
1.112 - ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ of the
1.113 - cumulative hierarchy (thus $x\in V@{\alpha+1}$).
1.114 + $\epsilon$-recursion, which are generalisations of transfinite
1.115 + induction and recursion. It also defines \cdx{rank}$(x)$, which is the
1.116 + least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$
1.117 + of the cumulative hierarchy (thus $x\in V@{\alpha+1}$).
1.118 \end{itemize}
1.119
1.120
1.121 @@ -1422,11 +1423,10 @@
1.122 a \in A \union B & \bimp & a\in A \disj a\in B\\
1.123 a \in A \inter B & \bimp & a\in A \conj a\in B\\
1.124 a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\
1.125 - a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\
1.126 - i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\
1.127 \pair{a,b}\in {\tt Sigma}(A,B)
1.128 & \bimp & a\in A \conj b\in B(a)\\
1.129 a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\
1.130 + (\forall x \in \emptyset. P(x)) & \bimp & \top\\
1.131 (\forall x \in A. \top) & \bimp & \top
1.132 \end{eqnarray*}
1.133 \caption{Rewrite rules for set theory} \label{zf-simpdata}
1.134 @@ -1443,57 +1443,57 @@
1.135 Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the
1.136 `Composition of homomorphisms' challenge~\cite{boyer86}.
1.137
1.138 -\item[ZF/ex/ramsey.ML]
1.139 +\item[ZF/ex/Ramsey.ML]
1.140 proves the finite exponent 2 version of Ramsey's Theorem, following Basin
1.141 and Kaufmann's presentation~\cite{basin91}.
1.142
1.143 -\item[ZF/ex/equiv.ML]
1.144 -develops a ZF theory of equivalence classes, not using the Axiom of Choice.
1.145 +\item[ZF/ex/Equiv.ML]
1.146 +develops a theory of equivalence classes, not using the Axiom of Choice.
1.147
1.148 -\item[ZF/ex/integ.ML]
1.149 +\item[ZF/ex/Integ.ML]
1.150 develops a theory of the integers as equivalence classes of pairs of
1.151 natural numbers.
1.152
1.153 -\item[ZF/ex/bin.ML]
1.154 +\item[ZF/ex/Bin.ML]
1.155 defines a datatype for two's complement binary integers. File
1.156 -{\tt binfn.ML} then develops rewrite rules for binary
1.157 +{\tt BinFn.ML} then develops rewrite rules for binary
1.158 arithmetic. For instance, $1359\times {-}2468 = {-}3354012$ takes under
1.159 14 seconds.
1.160
1.161 -\item[ZF/ex/bt.ML]
1.162 +\item[ZF/ex/BT.ML]
1.163 defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.
1.164
1.165 -\item[ZF/ex/term.ML]
1.166 - and {\tt termfn.ML} define a recursive data structure for
1.167 +\item[ZF/ex/Term.ML]
1.168 + and {\tt TermFn.ML} define a recursive data structure for
1.169 terms and term lists. These are simply finite branching trees.
1.170
1.171 -\item[ZF/ex/tf.ML]
1.172 - and {\tt tf_fn.ML} define primitives for solving mutually
1.173 +\item[ZF/ex/TF.ML]
1.174 + and {\tt TF_Fn.ML} define primitives for solving mutually
1.175 recursive equations over sets. It constructs sets of trees and forests
1.176 as an example, including induction and recursion rules that handle the
1.177 mutual recursion.
1.178
1.179 -\item[ZF/ex/prop.ML]
1.180 - and {\tt proplog.ML} proves soundness and completeness of
1.181 - propositional logic. This illustrates datatype definitions, inductive
1.182 - definitions, structural induction and rule induction.
1.183 +\item[ZF/ex/Prop.ML]
1.184 + and {\tt PropLog.ML} proves soundness and completeness of
1.185 + propositional logic~\cite{paulson-set-II}. This illustrates datatype
1.186 + definitions, inductive definitions, structural induction and rule induction.
1.187
1.188 -\item[ZF/ex/listn.ML]
1.189 +\item[ZF/ex/ListN.ML]
1.190 presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.
1.191
1.192 -\item[ZF/ex/acc.ML]
1.193 +\item[ZF/ex/Acc.ML]
1.194 presents the inductive definition of the accessible part of a
1.195 relation~\cite{paulin92}.
1.196
1.197 -\item[ZF/ex/comb.ML]
1.198 +\item[ZF/ex/Comb.ML]
1.199 presents the datatype definition of combinators. The file
1.200 - {\tt contract0.ML} defines contraction, while file
1.201 - {\tt parcontract.ML} defines parallel contraction and
1.202 + {\tt Contract0.ML} defines contraction, while file
1.203 + {\tt ParContract.ML} defines parallel contraction and
1.204 proves the Church-Rosser Theorem. This case study follows Camilleri and
1.205 Melham~\cite{camilleri92}.
1.206
1.207 -\item[ZF/ex/llist.ML]
1.208 - and {\tt llist_eq.ML} develop lazy lists in ZF and a notion
1.209 +\item[ZF/ex/LList.ML]
1.210 + and {\tt LList_Eq.ML} develop lazy lists and a notion
1.211 of coinduction for proving equations between them.
1.212 \end{ttdescription}
1.213
1.214 @@ -1683,7 +1683,7 @@
1.215 \hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule.
1.216
1.217 The file {\tt ZF/equalities.ML} has many similar proofs. Reasoning about
1.218 -general intersection can be difficult because of its anomalous behavior on
1.219 +general intersection can be difficult because of its anomalous behaviour on
1.220 the empty set. However, \ttindex{fast_tac} copes well with these. Here is
1.221 a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
1.222 \begin{ttbox}
1.223 @@ -1788,7 +1788,7 @@
1.224 {\out (f Un g) ` a = f ` a}
1.225 {\out No subgoals!}
1.226 \end{ttbox}
1.227 -See the files {\tt ZF/func.ML} and {\tt ZF/wf.ML} for more
1.228 +See the files {\tt ZF/func.ML} and {\tt ZF/WF.ML} for more
1.229 examples of reasoning about functions.
1.230
1.231 \index{set theory|)}
2.1 --- a/doc-src/Logics/intro.tex Sun Apr 24 11:30:00 1994 +0200
2.2 +++ b/doc-src/Logics/intro.tex Mon Apr 25 11:05:58 1994 +0200
2.3 @@ -21,8 +21,8 @@
2.4 system~\cite{paulson87}. It is built upon classical~\FOL{}.
2.5
2.6 \item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
2.7 -which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon88a}. This
2.8 -object-logic should not be confused with Isabelle's meta-logic, which is
2.9 +which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
2.10 +This object-logic should not be confused with Isabelle's meta-logic, which is
2.11 also a form of higher-order logic.
2.12
2.13 \item[\thydx{HOLCF}] is an alternative version of {\sc lcf}, defined
2.14 @@ -99,7 +99,7 @@
2.15 actual syntax definitions in the {\tt.thy} files.
2.16
2.17 Each nonterminal symbol is associated with some Isabelle type. For
2.18 -example, the {\bf formulae} of first-order logic have type~$o$. Every
2.19 +example, the formulae of first-order logic have type~$o$. Every
2.20 Isabelle expression of type~$o$ is therefore a formula. These include
2.21 atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more
2.22 generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have
2.23 @@ -134,7 +134,7 @@
2.24
2.25 Many of the proof procedures use backtracking. Typically they attempt to
2.26 solve subgoal~$i$ by repeatedly applying a certain tactic to it. This
2.27 -tactic, which is known as a {\it step tactic}, resolves a selection of
2.28 +tactic, which is known as a {\bf step tactic}, resolves a selection of
2.29 rules with subgoal~$i$. This may replace one subgoal by many; the
2.30 search persists until there are fewer subgoals in total than at the start.
2.31 Backtracking happens when the search reaches a dead end: when the step