
1 \chapter*{Preface} 

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

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

4 

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

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

7 the conjectured formula. The resolution prover Otter~\cite{wosbledsoe} is 

8 an impressive example. 

9 

10 {\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each 

11 support a fixed logic too. These are higherorder type theories, 

12 explicitly concerned with computation and capable of expressing 

13 developments in constructive mathematics. They are far removed from 

14 classical firstorder logic. 

15 

16 A diverse collection of logics  type theories, process calculi, 

17 $\lambda$calculi  may be found in the Computer Science literature. 

18 Such logics require proof support. Few proof procedures are known for 

19 them, but the theorem prover can at least automate routine steps. 

20 

21 A {\bf generic} theorem prover is one that supports a variety of logics. 

22 Some generic provers are noteworthy for their user interfaces 

23 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a 

24 syntactic framework that can express typical inference rules. Isabelle's 

25 distinctive feature is its representation of logics within a fragment of 

26 higherorder logic, called the metalogic. The proof theory of 

27 higherorder logic may be used to demonstrate that the representation is 

28 correct~\cite{paulson89}. The approach has much in common with the 

29 Edinburgh Logical Framework~\cite{harperjacm} and with 

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

31 

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

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

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

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

36 language and a fully automatic search would be impractical. Isabelle does 

37 not resolve clauses automatically, but under user direction. You can 

38 conduct singlestep proofs, use Isabelle's builtin proof procedures, or 

39 develop new proof procedures using tactics and tacticals. 

40 

41 Isabelle's metalogic is higherorder, based on the simply typed 

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

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

44 Isabelle strong support for many logical formalisms involving variable 

45 binding. 

46 

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

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

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

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

51 logics, and a Logic for Computable Functions~\cite{paulson87}. Several 

52 experimental logics are being developed, such as linear logic. 

53 

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

55 

56 

57 \section*{How to read this book} 

58 Isabelle is a complex 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\/} provides detailed information 

77 about Isabelle's facilities, excluding the objectlogics. This part 

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

79 should use it to locate facts quickly. 

80 

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

82 distributed with Isabelle. The chapters are intended for reference only; 

83 they overlap somewhat so that each chapter can be read in isolation. 

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} 

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 can be downloaded from . 

108 \begin{quote} 

109 {\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/} 

110 \end{quote} 

111 The electronic distribution list {\tt isabelleusers\at cl.cam.ac.uk} 

112 provides a forum for discussing problems and applications involving 

113 Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}. 

114 Please notify me of any errors you find in this book. 

115 

116 \section*{Acknowledgements} 

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

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

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

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

121 Mahjoub and Karin Nimmermann also contributed. 

122 

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

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

125 \S\ref{sec:refdefiningtheories}, Chap.\ts\ref{DefiningLogics}, 

126 Chap.\ts\ref{simpchap} and App.\ts\ref{app:TheorySyntax}\@. Carsten 

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

128 to Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation at 

129 the front. 

130 

131 David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert 

132 V{\"o}lker and Markus Wenzel suggested changes and corrections to the 

133 documentation. 

134 

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

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

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

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

139 Poly/{\sc ml}. 

140 

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

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

143 3245: Logical Frameworks and 6453: Types). 