|
1 \documentstyle[a4,12pt,proof,iman,alltt]{article} |
|
2 %% $Id$ |
|
3 %% run bibtex intro to prepare bibliography |
|
4 %% run ../sedindex intro to prepare index file |
|
5 %prth *(\(.*\)); \1; |
|
6 %{\\out \(.*\)} {\\out val it = "\1" : thm} |
|
7 |
|
8 \title{Introduction to Isabelle} |
|
9 \author{{\em Lawrence C. Paulson}\\ |
|
10 Computer Laboratory \\ University of Cambridge \\[2ex] |
|
11 {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} |
|
12 } |
|
13 \date{} |
|
14 \makeindex |
|
15 |
|
16 \underscoreoff |
|
17 |
|
18 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
|
19 |
|
20 \sloppy |
|
21 \binperiod %%%treat . like a binary operator |
|
22 |
|
23 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification |
|
24 \newcommand{\nand}{\mathbin{\lnot\&}} |
|
25 \newcommand{\xor}{\mathbin{\#}} |
|
26 |
|
27 \pagenumbering{roman} |
|
28 \begin{document} |
|
29 \pagestyle{empty} |
|
30 \begin{titlepage} |
|
31 \maketitle |
|
32 \thispagestyle{empty} |
|
33 \vfill |
|
34 {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} |
|
35 \end{titlepage} |
|
36 |
|
37 \pagestyle{headings} |
|
38 \part*{Preface} |
|
39 \index{Isabelle!overview} |
|
40 \index{Isabelle!object-logics supported} |
|
41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover. |
|
42 It has been instantiated to support reasoning in several object-logics: |
|
43 \begin{itemize} |
|
44 \item first-order logic, constructive and classical versions |
|
45 \item higher-order logic, similar to that of Gordon's {\sc |
|
46 hol}~\cite{gordon88a} |
|
47 \item Zermelo-Fraenkel set theory~\cite{suppes72} |
|
48 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90} |
|
49 \item the classical first-order sequent calculus, {\sc lk} |
|
50 \item the modal logics $T$, $S4$, and $S43$ |
|
51 \item the Logic for Computable Functions~\cite{paulson87} |
|
52 \end{itemize} |
|
53 A logic's syntax and inference rules are specified declaratively; this |
|
54 allows single-step proof construction. Isabelle provides control |
|
55 structures for expressing search procedures. Isabelle also provides |
|
56 several generic tools, such as simplifiers and classical theorem provers, |
|
57 which can be applied to object-logics. |
|
58 |
|
59 \index{ML} |
|
60 Isabelle is a large system, but beginners can get by with a small |
|
61 repertoire of commands and a basic knowledge of how Isabelle works. Some |
|
62 knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user |
|
63 interface. Advanced Isabelle theorem proving can involve writing \ML{} |
|
64 code, possibly with Isabelle's sources at hand. My book |
|
65 on~\ML{}~\cite{paulson91} covers much material connected with Isabelle, |
|
66 including a simple theorem prover. Users must be familiar with logic as |
|
67 used in computer science; there are many good |
|
68 texts~\cite{galton90,reeves90}. |
|
69 |
|
70 \index{LCF} |
|
71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an |
|
72 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows |
|
73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an |
|
74 abstract type; tactics and tacticals support backward proof. But {\sc lcf} |
|
75 represents object-level rules by functions, while Isabelle represents them |
|
76 by terms. You may find my other writings~\cite{paulson87,paulson-handbook} |
|
77 helpful in understanding the relationship between {\sc lcf} and Isabelle. |
|
78 |
|
79 Isabelle does not keep a record of inference steps. Each step is checked |
|
80 at run time to ensure that theorems can only be constructed by applying |
|
81 inference rules. An Isabelle proof typically involves hundreds of |
|
82 primitive inferences, and would be unintelligible if displayed. |
|
83 Discarding proofs saves vast amounts of storage. But can Isabelle be |
|
84 trusted? If desired, object-logics can be formalized such that each |
|
85 theorem carries a proof term, which could be checked by another program. |
|
86 Proofs can also be traced. |
|
87 |
|
88 \index{Isabelle!release history} Isabelle was first distributed in 1986. |
|
89 The 1987 version introduced a higher-order meta-logic with an improved |
|
90 treatment of quantifiers. The 1988 version added limited polymorphism and |
|
91 support for natural deduction. The 1989 version included a parser and |
|
92 pretty printer generator. The 1992 version introduced type classes, to |
|
93 support many-sorted and higher-order logics. The current version provides |
|
94 greater support for theories and is much faster. Isabelle is still under |
|
95 development and will continue to change. |
|
96 |
|
97 \subsubsection*{Overview} |
|
98 This manual consists of three parts. |
|
99 Part~I discusses the Isabelle's foundations. |
|
100 Part~II, presents simple on-line sessions, starting with forward proof. |
|
101 It also covers basic tactics and tacticals, and some commands for invoking |
|
102 Part~III contains further examples for users with a bit of experience. |
|
103 It explains how to derive rules define theories, and concludes with an |
|
104 extended example: a Prolog interpreter. |
|
105 |
|
106 Isabelle's Reference Manual and Object-Logics manual contain more details. |
|
107 They assume familiarity with the concepts presented here. |
|
108 |
|
109 |
|
110 \subsubsection*{Acknowledgements} |
|
111 Tobias Nipkow contributed most of the section on ``Defining Theories''. |
|
112 Sara Kalvala and Markus Wenzel suggested improvements. |
|
113 |
|
114 Tobias Nipkow has made immense contributions to Isabelle, including the |
|
115 parser generator, type classes, and the simplifier. Carsten Clasohm, Sonia |
|
116 Mahjoub, Karin Nimmermann and Markus Wenzel also made improvements. |
|
117 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, |
|
118 Poly/{\sc ml}. Many people have contributed to Isabelle's standard |
|
119 object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el. |
|
120 The research has been funded by the SERC (grants GR/G53279, GR/H40570) and |
|
121 by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types). |
|
122 |
|
123 \newpage |
|
124 \pagestyle{plain} \tableofcontents |
|
125 \newpage |
|
126 |
|
127 \newfont{\sanssi}{cmssi12} |
|
128 \vspace*{2.5cm} |
|
129 \begin{quote} |
|
130 \raggedleft |
|
131 {\sanssi |
|
132 You can only find truth with logic\\ |
|
133 if you have already found truth without it.}\\ |
|
134 \bigskip |
|
135 |
|
136 G.K. Chesterton, {\em The Man who was Orthodox} |
|
137 \end{quote} |
|
138 |
|
139 \clearfirst \pagestyle{headings} |
|
140 \include{foundations} |
|
141 \include{getting} |
|
142 \include{advanced} |
|
143 |
|
144 |
|
145 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
146 \bibliography{atp,funprog,general,logicprog,theory} |
|
147 |
|
148 \input{intro.ind} |
|
149 \end{document} |