Added mention of directory IMP; tidied the section on examples.
authorlcp
Fri Sep 09 11:52:38 1994 +0200 (1994-09-09)
changeset 59596c87d5bb015
parent 594 33a6bdb62a18
child 596 cffb278ec83e
Added mention of directory IMP; tidied the section on examples.
doc-src/Logics/ZF.tex
     1.1 --- a/doc-src/Logics/ZF.tex	Fri Sep 09 11:45:44 1994 +0200
     1.2 +++ b/doc-src/Logics/ZF.tex	Fri Sep 09 11:52:38 1994 +0200
     1.3 @@ -9,14 +9,15 @@
     1.4  of it is based on the work of No\"el~\cite{noel}.
     1.5  
     1.6  A tremendous amount of set theory has been formally developed, including
     1.7 -the basic properties of relations, functions and ordinals.  Significant
     1.8 -results have been proved, such as the Schr\"oder-Bernstein Theorem and a
     1.9 -version of Ramsey's Theorem.  General methods have been developed for
    1.10 -solving recursion equations over monotonic functors; these have been
    1.11 -applied to yield constructions of lists, trees, infinite lists, etc.  The
    1.12 -Recursion Theorem has been proved, admitting recursive definitions of
    1.13 -functions over well-founded relations.  Thus, we may even regard set theory
    1.14 -as a computational logic, loosely inspired by Martin-L\"of's Type Theory.
    1.15 +the basic properties of relations, functions, ordinals and cardinals.
    1.16 +Significant results have been proved, such as the Schr\"oder-Bernstein
    1.17 +Theorem, the Wellordering Theorem and a version of Ramsey's Theorem.
    1.18 +General methods have been developed for solving recursion equations over
    1.19 +monotonic functors; these have been applied to yield constructions of
    1.20 +lists, trees, infinite lists, etc.  The Recursion Theorem has been proved,
    1.21 +admitting recursive definitions of functions over well-founded relations.
    1.22 +Thus, we may even regard set theory as a computational logic, loosely
    1.23 +inspired by Martin-L\"of's Type Theory.
    1.24  
    1.25  Because {\ZF} is an extension of {\FOL}, it provides the same packages,
    1.26  namely {\tt hyp_subst_tac}, the simplifier, and the classical reasoner.
    1.27 @@ -24,11 +25,13 @@
    1.28  classical rule sets are defined, including {\tt lemmas_cs},
    1.29  {\tt upair_cs} and~{\tt ZF_cs}.  
    1.30  
    1.31 -{\tt ZF} now has a flexible package for handling inductive definitions,
    1.32 +{\tt ZF} has a flexible package for handling inductive definitions,
    1.33  such as inference systems, and datatype definitions, such as lists and
    1.34 -trees.  Moreover it also handles coinductive definitions, such as
    1.35 +trees.  Moreover it handles coinductive definitions, such as
    1.36  bisimulation relations, and codatatype definitions, such as streams.  A
    1.37 -recent paper describes the package~\cite{paulson-fixedpt}.  
    1.38 +recent paper describes the package~\cite{paulson-CADE}, but its examples
    1.39 +use an obsolete declaration syntax.  Please consult the version of the
    1.40 +paper distributed with Isabelle.
    1.41  
    1.42  Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less
    1.43  formally than this chapter.  Isabelle employs a novel treatment of
    1.44 @@ -1132,7 +1135,7 @@
    1.45  fixedpoint operators with corresponding induction and coinduction rules.
    1.46  These are essential to many definitions that follow, including the natural
    1.47  numbers and the transitive closure operator.  The (co)inductive definition
    1.48 -package also uses the fixedpoint operators~\cite{paulson-fixedpt}.  See
    1.49 +package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
    1.50  Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
    1.51  Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
    1.52  proofs.
    1.53 @@ -1290,16 +1293,17 @@
    1.54    univ}(A)$ (and is defined in terms of it) but is closed under the
    1.55  non-standard product and sum.
    1.56  
    1.57 -Figure~\ref{zf-fin} presents the finite set operator; ${\tt Fin}(A)$ is the
    1.58 -set of all finite sets over~$A$.  The definition employs Isabelle's
    1.59 -inductive definition package~\cite{paulson-fixedpt}, which proves various
    1.60 -rules automatically.  The induction rule shown is stronger than the one
    1.61 -proved by the package.  See file {\tt ZF/Fin.ML}.
    1.62 +Theory {\tt Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
    1.63 +${\tt Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs
    1.64 +Isabelle's inductive definition package, which proves various rules
    1.65 +automatically.  The induction rule shown is stronger than the one proved by
    1.66 +the package.  The theory also defines the set of all finite functions
    1.67 +between two given sets.
    1.68  
    1.69  \begin{figure}
    1.70  \begin{ttbox}
    1.71 -\tdx{Fin_0I}          0 : Fin(A)
    1.72 -\tdx{Fin_consI}       [| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)
    1.73 +\tdx{Fin.emptyI}      0 : Fin(A)
    1.74 +\tdx{Fin.consI}       [| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)
    1.75  
    1.76  \tdx{Fin_induct}
    1.77      [| b: Fin(A);
    1.78 @@ -1400,6 +1404,58 @@
    1.79      of the cumulative hierarchy (thus $x\in V@{\alpha+1}$).
    1.80  \end{itemize}
    1.81  
    1.82 +Other important theories lead to a theory of cardinal numbers.  They have
    1.83 +not yet been written up anywhere.  Here is a summary:
    1.84 +\begin{itemize}
    1.85 +\item Theory {\tt Rel} defines the basic properties of relations, such as
    1.86 +  (ir)reflexivity, (a)symmetry, and transitivity.
    1.87 +
    1.88 +\item Theory {\tt EquivClass} develops a theory of equivalence
    1.89 +  classes, not using the Axiom of Choice.
    1.90 +
    1.91 +\item Theory {\tt Order} defines partial orderings, total orderings and
    1.92 +  wellorderings.
    1.93 +
    1.94 +\item Theory {\tt OrderArith} defines orderings on sum and product sets.
    1.95 +  These can be used to define ordinal arithmetic and have applications to
    1.96 +  cardinal arithmetic.
    1.97 +
    1.98 +\item Theory {\tt OrderType} defines order types.  Every wellordering is
    1.99 +  equivalent to a unique ordinal, which is its order type.
   1.100 +
   1.101 +\item Theory {\tt Cardinal} defines equipollence and cardinal numbers.
   1.102 + 
   1.103 +\item Theory {\tt CardinalArith} defines cardinal addition and
   1.104 +  multiplication, and proves their elementary laws.  It proves that there
   1.105 +  is no greatest cardinal.  It also proves a deep result, namely
   1.106 +  $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see
   1.107 +  Kunen~\cite[page 29]{kunen80}.  None of these results assume the Axiom of
   1.108 +  Choice, which complicates their proofs considerably.  
   1.109 +\end{itemize}
   1.110 +
   1.111 +The following developments involve the Axiom of Choice (AC):
   1.112 +\begin{itemize}
   1.113 +\item Theory {\tt AC} asserts the Axiom of Choice and proves some simple
   1.114 +  equivalent forms.
   1.115 +
   1.116 +\item Theory {\tt Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma
   1.117 +  and the Wellordering Theorem, following Abrial and
   1.118 +  Laffitte~\cite{abrial93}.
   1.119 +
   1.120 +\item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about
   1.121 +  the cardinals.  It also proves a theorem needed to justify
   1.122 +  infinitely branching datatype declarations: if $\kappa$ is an infinite
   1.123 +  cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then
   1.124 +  $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
   1.125 +
   1.126 +\item Theory {\tt InfDatatype} proves theorems to justify infinitely
   1.127 +  branching datatypes.  Arbitrary index sets are allowed, provided their
   1.128 +  cardinalities have an upper bound.  The theory also justifies some
   1.129 +  unusual cases of finite branching, involving the finite powerset operator
   1.130 +  and the finite function space operator.
   1.131 +\end{itemize}
   1.132 +
   1.133 +
   1.134  
   1.135  \section{Simplification rules}
   1.136  {\ZF} does not merely inherit simplification from \FOL, but modifies it
   1.137 @@ -1433,69 +1489,63 @@
   1.138  \end{figure}
   1.139  
   1.140  
   1.141 -\section{The examples directory}
   1.142 +\section{The examples directories}
   1.143 +Directory {\tt HOL/IMP} contains a mechanised version of a semantic
   1.144 +equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the
   1.145 +denotational and operational semantics of a simple while-language, then
   1.146 +proves the two equivalent.  It contains several datatype and inductive
   1.147 +definitions, and demonstrates their use.
   1.148 +
   1.149  The directory {\tt ZF/ex} contains further developments in {\ZF} set
   1.150  theory.  Here is an overview; see the files themselves for more details.  I
   1.151  describe much of this material in other
   1.152 -publications~\cite{paulson-fixedpt,paulson-set-I,paulson-set-II}. 
   1.153 -\begin{ttdescription}
   1.154 -\item[ZF/ex/misc.ML] contains miscellaneous examples such as
   1.155 -  Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the
   1.156 -  `Composition of homomorphisms' challenge~\cite{boyer86}.
   1.157 +publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 
   1.158 +\begin{itemize}
   1.159 +\item File {\tt misc.ML} contains miscellaneous examples such as
   1.160 +  Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
   1.161 +  of homomorphisms' challenge~\cite{boyer86}.
   1.162  
   1.163 -\item[ZF/ex/Ramsey.ML]
   1.164 -proves the finite exponent 2 version of Ramsey's Theorem, following Basin
   1.165 -and Kaufmann's presentation~\cite{basin91}.
   1.166 -
   1.167 -\item[ZF/ex/Equiv.ML]
   1.168 -develops a theory of equivalence classes, not using the Axiom of Choice.
   1.169 +\item Theory {\tt Ramsey} proves the finite exponent 2 version of
   1.170 +  Ramsey's Theorem, following Basin and Kaufmann's
   1.171 +  presentation~\cite{basin91}.
   1.172  
   1.173 -\item[ZF/ex/Integ.ML]
   1.174 -develops a theory of the integers as equivalence classes of pairs of
   1.175 -natural numbers.
   1.176 +\item Theory {\tt Integ} develops a theory of the integers as
   1.177 +  equivalence classes of pairs of natural numbers.
   1.178  
   1.179 -\item[ZF/ex/Bin.ML]
   1.180 -defines a datatype for two's complement binary integers.  File
   1.181 -{\tt BinFn.ML} then develops rewrite rules for binary
   1.182 -arithmetic.  For instance, $1359\times {-}2468 = {-}3354012$ takes under
   1.183 -14 seconds.
   1.184 +\item Theory {\tt Bin} defines a datatype for two's complement binary
   1.185 +  integers, then proves rewrite rules to perform binary arithmetic.  For
   1.186 +  instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds.
   1.187  
   1.188 -\item[ZF/ex/BT.ML]
   1.189 -defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.
   1.190 +\item Theory {\tt BT} defines the recursive data structure ${\tt
   1.191 +    bt}(A)$, labelled binary trees.
   1.192  
   1.193 -\item[ZF/ex/Term.ML] 
   1.194 -  and {\tt TermFn.ML} define a recursive data structure for
   1.195 -  terms and term lists.  These are simply finite branching trees.
   1.196 +\item Theory {\tt Term} defines a recursive data structure for terms
   1.197 +  and term lists.  These are simply finite branching trees.
   1.198  
   1.199 -\item[ZF/ex/TF.ML]
   1.200 -  and {\tt TF_Fn.ML} define primitives for solving mutually
   1.201 +\item Theory {\tt TF} defines primitives for solving mutually
   1.202    recursive equations over sets.  It constructs sets of trees and forests
   1.203    as an example, including induction and recursion rules that handle the
   1.204    mutual recursion.
   1.205  
   1.206 -\item[ZF/ex/Prop.ML]
   1.207 -  and {\tt PropLog.ML} proves soundness and completeness of
   1.208 +\item Theory {\tt Prop} proves soundness and completeness of
   1.209    propositional logic~\cite{paulson-set-II}.  This illustrates datatype
   1.210 -  definitions, inductive definitions, structural induction and rule induction.
   1.211 +  definitions, inductive definitions, structural induction and rule
   1.212 +  induction.
   1.213  
   1.214 -\item[ZF/ex/ListN.ML]
   1.215 -presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.
   1.216 -
   1.217 -\item[ZF/ex/Acc.ML]
   1.218 -presents the inductive definition of the accessible part of a
   1.219 -relation~\cite{paulin92}. 
   1.220 +\item Theory {\tt ListN} inductively defines the lists of $n$
   1.221 +  elements~\cite{paulin92}.
   1.222  
   1.223 -\item[ZF/ex/Comb.ML]
   1.224 -  presents the datatype definition of combinators.  The file
   1.225 -  {\tt Contract0.ML} defines contraction, while file
   1.226 -  {\tt ParContract.ML} defines parallel contraction and
   1.227 -  proves the Church-Rosser Theorem.  This case study follows Camilleri and
   1.228 -  Melham~\cite{camilleri92}. 
   1.229 +\item Theory {\tt Acc} inductively defines the accessible part of a
   1.230 +  relation~\cite{paulin92}.
   1.231  
   1.232 -\item[ZF/ex/LList.ML]
   1.233 -  and {\tt LList_Eq.ML} develop lazy lists and a notion
   1.234 -  of coinduction for proving equations between them.
   1.235 -\end{ttdescription}
   1.236 +\item Theory {\tt Comb} defines the datatype of combinators and
   1.237 +  inductively defines contraction and parallel contraction.  It goes on to
   1.238 +  prove the Church-Rosser Theorem.  This case study follows Camilleri and
   1.239 +  Melham~\cite{camilleri92}.
   1.240 +
   1.241 +\item Theory {\tt LList} defines lazy lists and a coinduction
   1.242 +  principle for proving equations between them.
   1.243 +\end{itemize}
   1.244  
   1.245  
   1.246  \section{A proof about powersets}\label{sec:ZF-pow-example}