|
1 \documentclass[12pt,a4paper]{article} |
|
2 \usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup} |
|
3 |
|
4 %% run bibtex intro to prepare bibliography |
|
5 %% run ../sedindex intro to prepare index file |
|
6 %prth *(\(.*\)); \1; |
|
7 %{\\out \(.*\)} {\\out val it = "\1" : thm} |
|
8 |
|
9 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle} |
|
10 \author{{\em Lawrence C. Paulson}\\ |
|
11 Computer Laboratory \\ University of Cambridge \\ |
|
12 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
|
13 With Contributions by Tobias Nipkow and Markus Wenzel |
|
14 } |
|
15 \makeindex |
|
16 |
|
17 \underscoreoff |
|
18 |
|
19 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
|
20 |
|
21 \sloppy |
|
22 \binperiod %%%treat . like a binary operator |
|
23 |
|
24 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification |
|
25 \newcommand{\nand}{\mathbin{\lnot\&}} |
|
26 \newcommand{\xor}{\mathbin{\#}} |
|
27 |
|
28 \pagenumbering{roman} |
|
29 \begin{document} |
|
30 \pagestyle{empty} |
|
31 \begin{titlepage} |
|
32 \maketitle |
|
33 \emph{Note}: this document is part of the earlier Isabelle documentation, |
|
34 which is largely superseded by the Isabelle/HOL |
|
35 \emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory |
|
36 syntax and shows how to conduct proofs using the |
|
37 ML top level. This style of interaction is largely obsolete: |
|
38 most Isabelle proofs are now written using the Isar |
|
39 language and the Proof General interface. However, this paper contains valuable |
|
40 information that is not available elsewhere. Its examples are based |
|
41 on first-order logic rather than higher-order logic. |
|
42 |
|
43 \thispagestyle{empty} |
|
44 \vfill |
|
45 {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} |
|
46 \end{titlepage} |
|
47 |
|
48 \pagestyle{headings} |
|
49 \part*{Preface} |
|
50 \index{Isabelle!overview} \index{Isabelle!object-logics supported} |
|
51 Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem |
|
52 prover. It has been instantiated to support reasoning in several |
|
53 object-logics: |
|
54 \begin{itemize} |
|
55 \item first-order logic, constructive and classical versions |
|
56 \item higher-order logic, similar to that of Gordon's {\sc |
|
57 hol}~\cite{mgordon-hol} |
|
58 \item Zermelo-Fraenkel set theory~\cite{suppes72} |
|
59 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90} |
|
60 \item the classical first-order sequent calculus, {\sc lk} |
|
61 \item the modal logics $T$, $S4$, and $S43$ |
|
62 \item the Logic for Computable Functions~\cite{paulson87} |
|
63 \end{itemize} |
|
64 A logic's syntax and inference rules are specified declaratively; this |
|
65 allows single-step proof construction. Isabelle provides control |
|
66 structures for expressing search procedures. Isabelle also provides |
|
67 several generic tools, such as simplifiers and classical theorem provers, |
|
68 which can be applied to object-logics. |
|
69 |
|
70 Isabelle is a large system, but beginners can get by with a small |
|
71 repertoire of commands and a basic knowledge of how Isabelle works. |
|
72 The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some |
|
73 knowledge of Standard~\ML{}, because Isabelle is written in \ML{}; |
|
74 \index{ML} |
|
75 if you are prepared to writing \ML{} |
|
76 code, you can get Isabelle to do almost anything. My book |
|
77 on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle, |
|
78 including a simple theorem prover. Users must be familiar with logic as |
|
79 used in computer science; there are many good |
|
80 texts~\cite{galton90,reeves90}. |
|
81 |
|
82 \index{LCF} |
|
83 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an |
|
84 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows |
|
85 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an |
|
86 abstract type; tactics and tacticals support backward proof. But {\sc lcf} |
|
87 represents object-level rules by functions, while Isabelle represents them |
|
88 by terms. You may find my other writings~\cite{paulson87,paulson-handbook} |
|
89 helpful in understanding the relationship between {\sc lcf} and Isabelle. |
|
90 |
|
91 \index{Isabelle!release history} Isabelle was first distributed in 1986. |
|
92 The 1987 version introduced a higher-order meta-logic with an improved |
|
93 treatment of quantifiers. The 1988 version added limited polymorphism and |
|
94 support for natural deduction. The 1989 version included a parser and |
|
95 pretty printer generator. The 1992 version introduced type classes, to |
|
96 support many-sorted and higher-order logics. The 1994 version introduced |
|
97 greater support for theories. The most important recent change is the |
|
98 introduction of the Isar proof language, thanks to Markus Wenzel. |
|
99 Isabelle is still under |
|
100 development and will continue to change. |
|
101 |
|
102 \subsubsection*{Overview} |
|
103 This manual consists of three parts. Part~I discusses the Isabelle's |
|
104 foundations. Part~II, presents simple on-line sessions, starting with |
|
105 forward proof. It also covers basic tactics and tacticals, and some |
|
106 commands for invoking them. Part~III contains further examples for users |
|
107 with a bit of experience. It explains how to derive rules define theories, |
|
108 and concludes with an extended example: a Prolog interpreter. |
|
109 |
|
110 Isabelle's Reference Manual and Object-Logics manual contain more details. |
|
111 They assume familiarity with the concepts presented here. |
|
112 |
|
113 |
|
114 \subsubsection*{Acknowledgements} |
|
115 Tobias Nipkow contributed most of the section on defining theories. |
|
116 Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements. |
|
117 |
|
118 Tobias Nipkow has made immense contributions to Isabelle, including the parser |
|
119 generator, type classes, and the simplifier. Carsten Clasohm and Markus |
|
120 Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also |
|
121 helped. Isabelle was developed using Dave Matthews's Standard~{\sc ml} |
|
122 compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's standard |
|
123 object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el. |
|
124 The research has been funded by the EPSRC (grants GR/G53279, GR/H40570, |
|
125 GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical |
|
126 Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm |
|
127 \emph{Deduktion}. |
|
128 |
|
129 \newpage |
|
130 \pagestyle{plain} \tableofcontents |
|
131 \newpage |
|
132 |
|
133 \newfont{\sanssi}{cmssi12} |
|
134 \vspace*{2.5cm} |
|
135 \begin{quote} |
|
136 \raggedleft |
|
137 {\sanssi |
|
138 You can only find truth with logic\\ |
|
139 if you have already found truth without it.}\\ |
|
140 \bigskip |
|
141 |
|
142 G.K. Chesterton, {\em The Man who was Orthodox} |
|
143 \end{quote} |
|
144 |
|
145 \clearfirst \pagestyle{headings} |
|
146 \input{foundations} |
|
147 \input{getting} |
|
148 \input{advanced} |
|
149 |
|
150 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
151 \bibliography{manual} |
|
152 |
|
153 \printindex |
|
154 \end{document} |