1 \documentclass[12pt]{article}
11 %% run bibtex intro to prepare bibliography
12 %% run ../sedindex intro to prepare index file
14 %{\\out \(.*\)} {\\out val it = "\1" : thm}
16 \title{Introduction to Isabelle}
17 \author{{\em Lawrence C. Paulson}\\
18 Computer Laboratory \\ University of Cambridge \\[2ex]
19 {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
25 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
28 \binperiod %%%treat . like a binary operator
30 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
31 \newcommand{\nand}{\mathbin{\lnot\&}}
32 \newcommand{\xor}{\mathbin{\#}}
41 {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
46 \index{Isabelle!overview} \index{Isabelle!object-logics supported}
47 Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
48 prover. It has been instantiated to support reasoning in several
51 \item first-order logic, constructive and classical versions
52 \item higher-order logic, similar to that of Gordon's {\sc
53 hol}~\cite{mgordon-hol}
54 \item Zermelo-Fraenkel set theory~\cite{suppes72}
55 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
56 \item the classical first-order sequent calculus, {\sc lk}
57 \item the modal logics $T$, $S4$, and $S43$
58 \item the Logic for Computable Functions~\cite{paulson87}
60 A logic's syntax and inference rules are specified declaratively; this
61 allows single-step proof construction. Isabelle provides control
62 structures for expressing search procedures. Isabelle also provides
63 several generic tools, such as simplifiers and classical theorem provers,
64 which can be applied to object-logics.
67 Isabelle is a large system, but beginners can get by with a small
68 repertoire of commands and a basic knowledge of how Isabelle works. Some
69 knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
70 interface. Advanced Isabelle theorem proving can involve writing \ML{}
71 code, possibly with Isabelle's sources at hand. My book
72 on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,
73 including a simple theorem prover. Users must be familiar with logic as
74 used in computer science; there are many good
75 texts~\cite{galton90,reeves90}.
78 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
79 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows
80 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
81 abstract type; tactics and tacticals support backward proof. But {\sc lcf}
82 represents object-level rules by functions, while Isabelle represents them
83 by terms. You may find my other writings~\cite{paulson87,paulson-handbook}
84 helpful in understanding the relationship between {\sc lcf} and Isabelle.
86 \index{Isabelle!release history} Isabelle was first distributed in 1986.
87 The 1987 version introduced a higher-order meta-logic with an improved
88 treatment of quantifiers. The 1988 version added limited polymorphism and
89 support for natural deduction. The 1989 version included a parser and
90 pretty printer generator. The 1992 version introduced type classes, to
91 support many-sorted and higher-order logics. The current version provides
92 greater support for theories and is much faster. Isabelle is still under
93 development and will continue to change.
95 \subsubsection*{Overview}
96 This manual consists of three parts. Part~I discusses the Isabelle's
97 foundations. Part~II, presents simple on-line sessions, starting with
98 forward proof. It also covers basic tactics and tacticals, and some
99 commands for invoking them. Part~III contains further examples for users
100 with a bit of experience. It explains how to derive rules define theories,
101 and concludes with an extended example: a Prolog interpreter.
103 Isabelle's Reference Manual and Object-Logics manual contain more details.
104 They assume familiarity with the concepts presented here.
107 \subsubsection*{Acknowledgements}
108 Tobias Nipkow contributed most of the section on defining theories.
109 Stefan Berghofer, Sara Kalvala and Markus Wenzel suggested improvements.
111 Tobias Nipkow has made immense contributions to Isabelle, including the
112 parser generator, type classes, and the simplifier. Carsten Clasohm and
113 Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann
114 also helped. Isabelle was developed using Dave Matthews's Standard~{\sc
115 ml} compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's
116 standard object-logics, including Martin Coen, Philippe de Groote, Philippe
117 No\"el. The research has been funded by the SERC (grants GR/G53279,
118 GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:
122 \pagestyle{plain} \tableofcontents
125 \newfont{\sanssi}{cmssi12}
130 You can only find truth with logic\\
131 if you have already found truth without it.}\\
134 G.K. Chesterton, {\em The Man who was Orthodox}
137 \clearfirst \pagestyle{headings}
138 \include{foundations}
142 \bibliographystyle{plain} \small\raggedright\frenchspacing
143 \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}