1 \documentclass[11pt,a4paper]{report} |
|
2 \usepackage{isabelle,isabellesym,railsetup} |
|
3 \usepackage{graphicx,logics,ttbox,proof,latexsym} |
|
4 \usepackage{isar} |
|
5 |
|
6 \usepackage{pdfsetup} |
|
7 %last package! |
|
8 |
|
9 \remarkstrue |
|
10 |
|
11 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
|
12 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
13 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
14 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
|
15 |
|
16 \title{\includegraphics[scale=0.5]{isabelle_zf} \\[4ex] |
|
17 Isabelle's Logics: FOL and ZF} |
|
18 |
|
19 \author{{\em Lawrence C. Paulson}\\ |
|
20 Computer Laboratory \\ University of Cambridge \\ |
|
21 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
|
22 With Contributions by Tobias Nipkow and Markus Wenzel} |
|
23 |
|
24 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
25 \hrule\bigskip} |
|
26 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
|
27 |
|
28 \let\ts=\thinspace |
|
29 |
|
30 \makeindex |
|
31 |
|
32 \underscoreoff |
|
33 |
|
34 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
|
35 |
|
36 \pagestyle{headings} |
|
37 \sloppy |
|
38 \binperiod %%%treat . like a binary operator |
|
39 |
|
40 |
|
41 \isadroptag{theory} |
|
42 |
|
43 \railtermfont{\isabellestyle{tt}} |
|
44 \railnontermfont{\isabellestyle{literal}} |
|
45 \railnamefont{\isabellestyle{literal}} |
|
46 |
|
47 |
|
48 \begin{document} |
|
49 \maketitle |
|
50 |
|
51 \begin{abstract} |
|
52 This manual describes Isabelle's formalizations of many-sorted first-order |
|
53 logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}). See the |
|
54 \emph{Reference Manual} for general Isabelle commands, and \emph{Introduction |
|
55 to Isabelle} for an overall tutorial. |
|
56 |
|
57 This manual is part of the earlier Isabelle documentation, |
|
58 which is somewhat superseded by the Isabelle/HOL |
|
59 \emph{Tutorial}~\cite{isa-tutorial}. However, the present document is the |
|
60 only available documentation for Isabelle's versions of first-order logic |
|
61 and set theory. Much of it is concerned with |
|
62 the primitives for conducting proofs |
|
63 using the ML top level. It has been rewritten to use the Isar proof |
|
64 language, but evidence of the old \ML{} orientation remains. |
|
65 \end{abstract} |
|
66 |
|
67 |
|
68 \subsubsection*{Acknowledgements} |
|
69 Markus Wenzel made numerous improvements. |
|
70 Philippe de Groote contributed to~ZF. Philippe No\"el and |
|
71 Martin Coen made many contributions to~ZF. The research has |
|
72 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
|
73 GR/K77051, GR/M75440) and by ESPRIT (projects 3245: |
|
74 Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm |
|
75 \emph{Deduktion}. |
|
76 |
|
77 \pagenumbering{roman} \tableofcontents \cleardoublepage |
|
78 \pagenumbering{arabic} |
|
79 \setcounter{page}{1} |
|
80 \input{syntax} |
|
81 \input{FOL} |
|
82 \input{ZF} |
|
83 |
|
84 \isabellestyle{literal} |
|
85 \input{ZF_Isar} |
|
86 \isabellestyle{tt} |
|
87 |
|
88 \bibliographystyle{plain} |
|
89 \bibliography{manual} |
|
90 \printindex |
|
91 \end{document} |
|