# HG changeset patch
# User paulson
# Date 1091096153 -7200
# Node ID a471fd1d99614691a1be4cb0883760db64e777da
# Parent  6c3276a2735b2aa2be759e1ae738bf60d156a293
documents for ZF-AC and ZF-Constructible

diff -r 6c3276a2735b -r a471fd1d9961 src/ZF/AC/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/document/root.bib	Thu Jul 29 12:15:53 2004 +0200
@@ -0,0 +1,15 @@
+@ARTICLE{paulson-gr,
+  author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
+  title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice},
+  journal = {Journal of Automated Reasoning},
+  year = {1996},
+  volume = {17},
+  number = {3},
+  pages = {291-323},
+  month = dec}
+
+@Book{rubin&rubin,
+  author	= {Herman Rubin and Jean E. Rubin},
+  title		= {Equivalents of the Axiom of Choice, {II}},
+  publisher	= "North-Holland",
+  year		= 1985}
diff -r 6c3276a2735b -r a471fd1d9961 src/ZF/AC/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/document/root.tex	Thu Jul 29 12:15:53 2004 +0200
@@ -0,0 +1,41 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx}
+\usepackage{isabelle,amssymb,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+%table of contents is too crowded!
+\usepackage{tocloft}
+\addtolength\cftsubsecnumwidth {0.5em}
+\addtolength\cftsubsubsecnumwidth {1.0em}
+
+\begin{document}
+
+\title{Equivalents of the Axiom of Choice}
+\author{Krzysztof Gr\c{a}bczewski}
+\maketitle
+
+\begin{abstract}
+  This development~\cite{paulson-gr} proves the equivalence of seven
+  formulations of the well-ordering theorem and twenty formulations of the
+  axiom of choice. It formalizes the first two chapters of the monograph
+  \emph{Equivalents of the Axiom of Choice} by Rubin and
+  Rubin~\cite{rubin&rubin}. Some of this mmaterial involves extremely complex
+  techniques.
+\end{abstract}
+
+\tableofcontents
+
+\begin{center}
+  \includegraphics[scale=0.7]{session_graph}
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
diff -r 6c3276a2735b -r a471fd1d9961 src/ZF/Constructible/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/document/root.bib	Thu Jul 29 12:15:53 2004 +0200
@@ -0,0 +1,40 @@
+@incollection{goedel40,
+  author	= {Kurt G\"odel},
+  title		= {The Consistency of the Axiom of Choice and of the
+		   Generalized Continuum Hypothesis with the Axioms of Set
+		   Theory},
+  booktitle	= {{Kurt G\"odel}: Collected Works},
+  volume	= {II},
+  editor	= {S. Feferman and others},
+  publisher	= {Oxford University Press},
+  year		= 1990},
+  pages		= {33-101},
+  note		= {First published in 1940 by Princeton University Press}}
+
+@Book{kunen80,
+  author	= {Kenneth Kunen},
+  title		= {Set Theory: An Introduction to Independence Proofs},
+  publisher	= "North-Holland",
+  year		= 1980}
+
+@ARTICLE{paulson-consistency,
+  author = {Lawrence C. Paulson},
+  title = {The Relative Consistency of the Axiom of Choice --- Mechanized Using {Isabelle/ZF}},
+  journal = {LMS Journal of Computation and Mathematics},
+  year = {2003},
+  volume = {6},
+  pages = {198-248},
+  note = {\url{http://www.lms.ac.uk/jcm/6/lms2003-001/}},
+}
+
+@INPROCEEDINGS{paulson-reflection,
+  author = {Lawrence C. Paulson},
+  title = {The Reflection Theorem: A Study in Meta-Theoretic Reasoning},
+  pages = {377-391},
+  editor	= {Andrei Voronkov},
+  booktitle	= {Automated Deduction --- {CADE}-18 
+		  International Conference},
+  year		= 2002,
+  series	= {LNAI 2392},
+  publisher	= {Springer}}
+}
diff -r 6c3276a2735b -r a471fd1d9961 src/ZF/Constructible/document/root.tex
--- a/src/ZF/Constructible/document/root.tex	Wed Jul 28 16:26:27 2004 +0200
+++ b/src/ZF/Constructible/document/root.tex	Thu Jul 29 12:15:53 2004 +0200
@@ -3,17 +3,41 @@
 \usepackage{isabelle,amssymb,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}
 
-%table of contents too crowded!
+%table of contents is too crowded!
 \usepackage{tocloft}
 \addtolength\cftsubsecnumwidth {0.5em}
 \addtolength\cftsubsubsecnumwidth {1.0em}
 
 \begin{document}
 
-\title{Constructible}
+\title{The Constructible Universe\\ and the\\
+       Relative Consistency of the Axiom of Choice}
 \author{Lawrence C Paulson}
 \maketitle
 
+\begin{abstract}
+  G\"odel's proof of the relative consistency of the axiom of
+  choice~\cite{goedel40} is one of the most important results in the
+  foundations of mathematics. It bears on Hilbert's first problem, namely the
+  continuum hypothesis, and indeed G\"odel also proved the relative
+  consistency of the continuum hypothesis. Just as important, G\"odel's proof
+  introduced the \emph{inner model} method of proving relative consistency,
+  and it introduced the concept of \emph{constructible
+    set}. Kunen~\cite{kunen80} gives an excellent description of this body of
+  work.
+  
+  This Isabelle/ZF formalization demonstrates G\"odel's claim that his proof
+  can be undertaken without using metamathematical arguments, for example
+  arguments based on the general syntactic structure of a formula. Isabelle's
+  automation replaces the metamathematics, although it does not eliminate the
+  requirement at least to state many tedious results that would otherwise be
+  unnecessary.
+  
+  This formalization~\cite{paulson-consistency} is by far the deepest result
+  in set theory proved in any automated theorem prover. It rests on a previous
+  formal development of the reflection theorem~\cite{paulson-reflection}.
+\end{abstract}
+
 \tableofcontents
 
 \begin{center}
@@ -26,7 +50,7 @@
 
 \input{session}
 
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\bibliographystyle{plain}
+\bibliography{root}
 
 \end{document}
diff -r 6c3276a2735b -r a471fd1d9961 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed Jul 28 16:26:27 2004 +0200
+++ b/src/ZF/IsaMakefile	Thu Jul 29 12:15:53 2004 +0200
@@ -59,8 +59,8 @@
   AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \
   AC/AC_Equiv.thy AC/Cardinal_aux.thy \
   AC/DC.thy AC/HH.thy AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy \
-  AC/WO2_AC16.thy AC/WO6_WO1.thy 
-	@$(ISATOOL) usedir $(OUT)/ZF AC
+  AC/WO2_AC16.thy AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
+	@$(ISATOOL) usedir -g true $(OUT)/ZF AC
 
 
 ## ZF-Coind
@@ -87,7 +87,7 @@
   Constructible/Rec_Separation.thy Constructible/Separation.thy \
   Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \
   Constructible/Reflection.thy  Constructible/WFrec.thy \
-  Constructible/document/root.tex
+  Constructible/document/root.bib Constructible/document/root.tex
 	@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible