# HG changeset patch # User lcp # Date 767264758 -7200 # Node ID 8d77f767bd26fd791a38c9c68922c9fd4f0af590 # Parent 82104a03565ad2ab3ed7fa80c70da99bede620de final Springer copy diff -r 82104a03565a -r 8d77f767bd26 doc-src/Logics/ZF.tex --- a/doc-src/Logics/ZF.tex Sun Apr 24 11:30:00 1994 +0200 +++ b/doc-src/Logics/ZF.tex Mon Apr 25 11:05:58 1994 +0200 @@ -32,7 +32,7 @@ Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less formally than this chapter. Isabelle employs a novel treatment of -non-well-founded data structures within the standard ZF axioms including +non-well-founded data structures within the standard {\sc zf} axioms including the Axiom of Foundation~\cite{paulson-final}. @@ -337,7 +337,7 @@ \hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}. -%%%% zf.thy +%%%% ZF.thy \begin{figure} \begin{ttbox} @@ -414,7 +414,7 @@ definitions. In particular, bounded quantifiers and the subset relation appear in other axioms. Object-level quantifiers and implications have been replaced by meta-level ones wherever possible, to simplify use of the -axioms. See the file {\tt ZF/zf.thy} for details. +axioms. See the file {\tt ZF/ZF.thy} for details. The traditional replacement axiom asserts \[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \] @@ -517,9 +517,9 @@ \subsection{Fundamental lemmas} Figure~\ref{zf-lemmas1} presents the derived rules for the most basic operators. The rules for the bounded quantifiers resemble those for the -ordinary quantifiers, but note that \tdx{ballE} uses a negated -assumption in the style of Isabelle's classical reasoner. The congruence rules -\tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's +ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption +in the style of Isabelle's classical reasoner. The \rmindex{congruence + rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's simplifier, but have few other uses. Congruence rules must be specially derived for all binding operators, and henceforth will not be shown. @@ -536,7 +536,7 @@ \tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to particular circumstances. Although too many rules can be confusing, there is no reason to aim for a minimal set of rules. See the file -{\tt ZF/zf.ML} for a complete listing. +{\tt ZF/ZF.ML} for a complete listing. Figure~\ref{zf-lemmas3} presents rules for general union and intersection. The empty intersection should be undefined. We cannot have @@ -772,7 +772,7 @@ The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other -encoding of ordered pairs. The non-standard ordered pairs mentioned below +encodings of ordered pairs. The non-standard ordered pairs mentioned below satisfy $\pair{\emptyset;\emptyset}=\emptyset$. The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} @@ -825,13 +825,13 @@ of ordered pairs. The converse of a relation~$r$ is the set of all pairs $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then {\cdx{converse}$(r)$} is its inverse. The rules for the domain -operation, \tdx{domainI} and~\tdx{domainE}, assert that -\cdx{domain}$(r)$ consists of every element~$a$ such that $r$ contains +operation, namely \tdx{domainI} and~\tdx{domainE}, assert that +\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains some pair of the form~$\pair{x,y}$. The range operation is similar, and the field of a relation is merely the union of its domain and range. Figure~\ref{zf-domrange2} presents rules for images and inverse images. -Note that these operations are generalizations of range and domain, +Note that these operations are generalisations of range and domain, respectively. See the file {\tt ZF/domrange.ML} for derivations of the rules. @@ -1019,6 +1019,7 @@ \begin{figure} \index{*"+ symbol} \begin{constants} + \it symbol & \it meta-type & \it priority & \it description \\ \tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ \cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ \cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ @@ -1293,7 +1294,7 @@ set of all finite sets over~$A$. The definition employs Isabelle's inductive definition package~\cite{paulson-fixedpt}, which proves various rules automatically. The induction rule shown is stronger than the one -proved by the package. See file {\tt ZF/fin.ML}. +proved by the package. See file {\tt ZF/Fin.ML}. \begin{figure} \begin{ttbox} @@ -1370,8 +1371,8 @@ Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$. The definition employs Isabelle's datatype package, which defines the introduction and induction rules automatically, as well as the constructors -and case operator (\verb|list_case|). See file {\tt ZF/list.ML}. -The file {\tt ZF/listfn.thy} proceeds to define structural +and case operator (\verb|list_case|). See file {\tt ZF/List.ML}. +The file {\tt ZF/ListFn.thy} proceeds to define structural recursion and the usual list functions. The constructions of the natural numbers and lists make use of a suite of @@ -1393,10 +1394,10 @@ numbers. \item Theory {\tt Epsilon} derives $\epsilon$-induction and - $\epsilon$-recursion, which are generalizations of transfinite - induction. It also defines \cdx{rank}$(x)$, which is the least - ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ of the - cumulative hierarchy (thus $x\in V@{\alpha+1}$). + $\epsilon$-recursion, which are generalisations of transfinite + induction and recursion. It also defines \cdx{rank}$(x)$, which is the + least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ + of the cumulative hierarchy (thus $x\in V@{\alpha+1}$). \end{itemize} @@ -1422,11 +1423,10 @@ a \in A \union B & \bimp & a\in A \disj a\in B\\ a \in A \inter B & \bimp & a\in A \conj a\in B\\ a \in A-B & \bimp & a\in A \conj \neg (a\in B)\\ - a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\ - i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\ \pair{a,b}\in {\tt Sigma}(A,B) & \bimp & a\in A \conj b\in B(a)\\ a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\ + (\forall x \in \emptyset. P(x)) & \bimp & \top\\ (\forall x \in A. \top) & \bimp & \top \end{eqnarray*} \caption{Rewrite rules for set theory} \label{zf-simpdata} @@ -1443,57 +1443,57 @@ Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition of homomorphisms' challenge~\cite{boyer86}. -\item[ZF/ex/ramsey.ML] +\item[ZF/ex/Ramsey.ML] proves the finite exponent 2 version of Ramsey's Theorem, following Basin and Kaufmann's presentation~\cite{basin91}. -\item[ZF/ex/equiv.ML] -develops a ZF theory of equivalence classes, not using the Axiom of Choice. +\item[ZF/ex/Equiv.ML] +develops a theory of equivalence classes, not using the Axiom of Choice. -\item[ZF/ex/integ.ML] +\item[ZF/ex/Integ.ML] develops a theory of the integers as equivalence classes of pairs of natural numbers. -\item[ZF/ex/bin.ML] +\item[ZF/ex/Bin.ML] defines a datatype for two's complement binary integers. File -{\tt binfn.ML} then develops rewrite rules for binary +{\tt BinFn.ML} then develops rewrite rules for binary arithmetic. For instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds. -\item[ZF/ex/bt.ML] +\item[ZF/ex/BT.ML] defines the recursive data structure ${\tt bt}(A)$, labelled binary trees. -\item[ZF/ex/term.ML] - and {\tt termfn.ML} define a recursive data structure for +\item[ZF/ex/Term.ML] + and {\tt TermFn.ML} define a recursive data structure for terms and term lists. These are simply finite branching trees. -\item[ZF/ex/tf.ML] - and {\tt tf_fn.ML} define primitives for solving mutually +\item[ZF/ex/TF.ML] + and {\tt TF_Fn.ML} define primitives for solving mutually recursive equations over sets. It constructs sets of trees and forests as an example, including induction and recursion rules that handle the mutual recursion. -\item[ZF/ex/prop.ML] - and {\tt proplog.ML} proves soundness and completeness of - propositional logic. This illustrates datatype definitions, inductive - definitions, structural induction and rule induction. +\item[ZF/ex/Prop.ML] + and {\tt PropLog.ML} proves soundness and completeness of + propositional logic~\cite{paulson-set-II}. This illustrates datatype + definitions, inductive definitions, structural induction and rule induction. -\item[ZF/ex/listn.ML] +\item[ZF/ex/ListN.ML] presents the inductive definition of the lists of $n$ elements~\cite{paulin92}. -\item[ZF/ex/acc.ML] +\item[ZF/ex/Acc.ML] presents the inductive definition of the accessible part of a relation~\cite{paulin92}. -\item[ZF/ex/comb.ML] +\item[ZF/ex/Comb.ML] presents the datatype definition of combinators. The file - {\tt contract0.ML} defines contraction, while file - {\tt parcontract.ML} defines parallel contraction and + {\tt Contract0.ML} defines contraction, while file + {\tt ParContract.ML} defines parallel contraction and proves the Church-Rosser Theorem. This case study follows Camilleri and Melham~\cite{camilleri92}. -\item[ZF/ex/llist.ML] - and {\tt llist_eq.ML} develop lazy lists in ZF and a notion +\item[ZF/ex/LList.ML] + and {\tt LList_Eq.ML} develop lazy lists and a notion of coinduction for proving equations between them. \end{ttdescription} @@ -1683,7 +1683,7 @@ \hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule. The file {\tt ZF/equalities.ML} has many similar proofs. Reasoning about -general intersection can be difficult because of its anomalous behavior on +general intersection can be difficult because of its anomalous behaviour on the empty set. However, \ttindex{fast_tac} copes well with these. Here is a typical example, borrowed from Devlin~\cite[page 12]{devlin79}: \begin{ttbox} @@ -1788,7 +1788,7 @@ {\out (f Un g) ` a = f ` a} {\out No subgoals!} \end{ttbox} -See the files {\tt ZF/func.ML} and {\tt ZF/wf.ML} for more +See the files {\tt ZF/func.ML} and {\tt ZF/WF.ML} for more examples of reasoning about functions. \index{set theory|)} diff -r 82104a03565a -r 8d77f767bd26 doc-src/Logics/intro.tex --- a/doc-src/Logics/intro.tex Sun Apr 24 11:30:00 1994 +0200 +++ b/doc-src/Logics/intro.tex Mon Apr 25 11:05:58 1994 +0200 @@ -21,8 +21,8 @@ system~\cite{paulson87}. It is built upon classical~\FOL{}. \item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40}, -which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon88a}. This -object-logic should not be confused with Isabelle's meta-logic, which is +which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}. +This object-logic should not be confused with Isabelle's meta-logic, which is also a form of higher-order logic. \item[\thydx{HOLCF}] is an alternative version of {\sc lcf}, defined @@ -99,7 +99,7 @@ actual syntax definitions in the {\tt.thy} files. Each nonterminal symbol is associated with some Isabelle type. For -example, the {\bf formulae} of first-order logic have type~$o$. Every +example, the formulae of first-order logic have type~$o$. Every Isabelle expression of type~$o$ is therefore a formula. These include atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have @@ -134,7 +134,7 @@ Many of the proof procedures use backtracking. Typically they attempt to solve subgoal~$i$ by repeatedly applying a certain tactic to it. This -tactic, which is known as a {\it step tactic}, resolves a selection of +tactic, which is known as a {\bf step tactic}, resolves a selection of rules with subgoal~$i$. This may replace one subgoal by many; the search persists until there are fewer subgoals in total than at the start. Backtracking happens when the search reaches a dead end: when the step