
1 \chapter*{Preface} 

2 \markboth{Preface}{Preface} %or Preface ? 

3 \addcontentsline{toc}{chapter}{Preface} 

4 

5 \index{Isabelle!objectlogics supported} 

6 

7 Most theorem provers support a fixed logic, such as firstorder or 

8 equational logic. They bring sophisticated proof procedures to bear upon 

9 the conjectured formula. An impressive example is the resolution prover 

10 Otter, which Quaife~\cite{quaifebook} has used to formalize a body of 

11 mathematics. 

12 

13 ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a 

14 fixed logic too, but one far removed from firstorder logic. They are 

15 explicitly concerned with computation. A diverse collection of logics  

16 type theories, process calculi, $\lambda$calculi  may be found in the 

17 Computer Science literature. Such logics require proof support. Few proof 

18 procedures exist, but the theorem prover can at least check that each 

19 inference is valid. 

20 

21 A {\bf generic} theorem prover is one that can support many different 

22 logics. Most of these \cite{dawson90,mural,sawamura92} work by 

23 implementing a syntactic framework that can express the features of typical 

24 inference rules. Isabelle's distinctive feature is its representation of 

25 logics using a metalogic. This metalogic is just a fragment of 

26 higherorder logic; known proof theory may be used to demonstrate that the 

27 representation is correct~\cite{paulson89}. The representation has much in 

28 common with the Edinburgh Logical Framework~\cite{harperjacm} and with 

29 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. 

30 

31 An inference rule in Isabelle is a generalized Horn clause. Rules are 

32 joined to make proofs by resolving such clauses. Logical variables in 

33 goals can be instantiated incrementally. But Isabelle is not a resolution 

34 theorem prover like Otter. Isabelle's clauses are drawn from a richer, 

35 higherorder language and a fully automatic search would be impractical. 

36 Isabelle does not join clauses automatically, but under strict user 

37 control. You can conduct singlestep proofs, use Isabelle's builtin proof 

38 procedures, or develop new proof procedures using tactics and tacticals. 

39 

40 Isabelle's metalogic is higherorder, based on the typed 

41 $\lambda$calculus. So resolution cannot use ordinary unification, but 

42 higherorder unification~\cite{huet75}. This complicated procedure gives 

43 Isabelle strong support for many logical formalisms involving variable 

44 binding. 

45 

46 The diagram below illustrates some of the logics distributed with Isabelle. 

47 These include firstorder logic (intuitionistic and classical), the sequent 

48 calculus, higherorder logic, ZermeloFraenkel set theory~\cite{suppes72}, 

49 a version of Constructive Type Theory~\cite{nordstrom90}, several modal 

50 logics, and a Logic for Computable Functions. Several experimental 

51 logics are also available, such a term assignment calculus for linear 

52 logic. 

53 

54 \centerline{\epsfbox{Isalogics.eps}} 

55 

56 

57 \section*{How to read this book} 

58 Isabelle is a large system, but beginners can get by with a few commands 

59 and a basic knowledge of how Isabelle works. Some knowledge of 

60 Standard~\ML{} is essential because \ML{} is Isabelle's user interface. 

61 Advanced Isabelle theorem proving can involve writing \ML{} code, possibly 

62 with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers 

63 much material connected with Isabelle, including a simple theorem prover. 

64 

65 The Isabelle documentation is divided into three parts, which serve 

66 distinct purposes: 

67 \begin{itemize} 

68 \item {\em Introduction to Isabelle\/} describes the basic features of 

69 Isabelle. This part is intended to be read through. If you are 

70 impatient to get started, you might skip the first chapter, which 

71 describes Isabelle's metalogic in some detail. The other chapters 

72 present online sessions of increasing difficulty. It also explains how 

73 to derive rules define theories, and concludes with an extended example: 

74 a Prolog interpreter. 

75 

76 \item {\em The Isabelle Reference Manual\/} contains information about most 

77 of the facilities of Isabelle, apart from particular objectlogics. This 

78 part would make boring reading, though browsing might be useful. Mostly 

79 you should use it to locate facts quickly. 

80 

81 \item {\em Isabelle's ObjectLogics\/} describes the various logics 

82 distributed with Isabelle. Its final chapter explains how to define new 

83 logics. The other chapters are intended for reference only. 

84 \end{itemize} 

85 This book should not be read from start to finish. Instead you might read 

86 a couple of chapters from {\em Introduction to Isabelle}, then try some 

87 examples referring to the other parts, return to the {\em Introduction}, 

88 and so forth. Starred sections discuss obscure matters and may be skipped 

89 on a first reading. 

90 

91 

92 

93 \section*{Releases of Isabelle}\index{Isabelle!release history} 

94 Isabelle was first distributed in 1986. The 1987 version introduced a 

95 higherorder metalogic with an improved treatment of quantifiers. The 

96 1988 version added limited polymorphism and support for natural deduction. 

97 The 1989 version included a parser and pretty printer generator. The 1992 

98 version introduced type classes, to support manysorted and higherorder 

99 logics. The 1993 version provides greater support for theories and is 

100 much faster. 

101 

102 Isabelle is still under development. Projects under consideration include 

103 better support for inductive definitions, some means of recording proofs, a 

104 graphical user interface, and developments in the standard objectlogics. 

105 I hope but cannot promise to maintain upwards compatibility. 

106 

107 Isabelle is available by anonymous ftp: 

108 \begin{itemize} 

109 \item University of Cambridge\\ 

110 host {\tt ftp.cl.cam.ac.uk}\\ 

111 directory {\tt ml} 

112 

113 \item Technical University of Munich\\ 

114 host {\tt ftp.informatik.tumuenchen.de}\\ 

115 directory {\tt local/lehrstuhl/nipkow} 

116 \end{itemize} 

117 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any 

118 errors you find in this book and your problems or successes with Isabelle. 

119 

120 

121 \subsection*{Acknowledgements} 

122 Tobias Nipkow has made immense contributions to Isabelle, including the 

123 parser generator, type classes, the simplifier, and several objectlogics. 

124 He also arranged for several of his students to help. Carsten Clasohm 

125 implemented the theory database; Markus Wenzel implemented macros; Sonia 

126 Mahjoub and Karin Nimmermann also contributed. 

127 

128 Nipkow and his students wrote much of the documentation underlying this 

129 book. Nipkow wrote the first versions of \S\ref{sec:definingtheories}, 

130 Chap.\ts\ref{simpchap}, Chap.\ts\ref{DefiningLogics} and part of 

131 Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm 

132 contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to 

133 Chap.\ts\ref{DefiningLogics}. 

134 

135 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and 

136 Markus Wenzel suggested changes and corrections to the documentation. 

137 

138 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped 

139 to develop Isabelle's standard objectlogics. David Aspinall performed 

140 some useful research into theories and implemented an Isabelle Emacs mode. 

141 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, 

142 Poly/{\sc ml}. 

143 

144 The research has been funded by numerous SERC grants dating from the Alvey 

145 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects 

146 3245: Logical Frameworks and 6453: Types). 

147 

148 

149 \index{ML} 