lcp@285

1 
\chapter*{Preface}

lcp@285

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

lcp@356

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

lcp@285

4 

lcp@285

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

lcp@285

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

lcp@304

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

lcp@329

8 
an impressive example.

lcp@285

9 

lcp@329

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

lcp@329

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

lcp@329

12 
explicitly concerned with computation and capable of expressing

lcp@329

13 
developments in constructive mathematics. They are far removed from

lcp@329

14 
classical firstorder logic.

lcp@329

15 

lcp@329

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

lcp@329

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

lcp@329

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

lcp@329

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

lcp@329

20 

lcp@329

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

lcp@304

22 
Some generic provers are noteworthy for their user interfaces

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@285

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

lcp@285

31 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

39 
develop new proof procedures using tactics and tacticals.

lcp@285

40 

lcp@329

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

lcp@285

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

lcp@285

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

lcp@285

44 
Isabelle strong support for many logical formalisms involving variable

lcp@285

45 
binding.

lcp@285

46 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@356

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

lcp@356

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

lcp@285

53 

wenzelm@5374

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

lcp@285

55 

lcp@285

56 

lcp@285

57 
\section*{How to read this book}

lcp@304

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

64 

lcp@285

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

lcp@285

66 
distinct purposes:

lcp@285

67 
\begin{itemize}

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

74 
a Prolog interpreter.

lcp@285

75 

lcp@304

76 
\item {\em The Isabelle Reference Manual\/} provides detailed information

lcp@304

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

lcp@304

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

lcp@304

79 
should use it to locate facts quickly.

lcp@285

80 

lcp@285

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

lcp@329

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

lcp@329

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

lcp@285

84 
\end{itemize}

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

89 
on a first reading.

lcp@285

90 

lcp@285

91 

lcp@285

92 

lcp@329

93 
\section*{Releases of Isabelle}

lcp@285

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

lcp@285

95 
higherorder metalogic with an improved treatment of quantifiers. The

lcp@285

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

lcp@285

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

lcp@285

98 
version introduced type classes, to support manysorted and higherorder

lcp@285

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

lcp@285

100 
much faster.

lcp@285

101 

lcp@285

102 
Isabelle is still under development. Projects under consideration include

lcp@285

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

lcp@285

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

lcp@285

105 
I hope but cannot promise to maintain upwards compatibility.

lcp@285

106 

lcp@285

107 
Isabelle is available by anonymous ftp:

lcp@285

108 
\begin{itemize}

lcp@285

109 
\item University of Cambridge\\

lcp@285

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

lcp@285

111 
directory {\tt ml}

lcp@285

112 

lcp@285

113 
\item Technical University of Munich\\

lcp@285

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

lcp@285

115 
directory {\tt local/lehrstuhl/nipkow}

lcp@285

116 
\end{itemize}

lcp@356

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

lcp@356

118 
provides a forum for discussing problems and applications involving

lcp@356

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

lcp@356

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

lcp@285

121 

lcp@304

122 
\section*{Acknowledgements}

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

127 
Mahjoub and Karin Nimmermann also contributed.

lcp@285

128 

lcp@285

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

lcp@285

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

lcp@329

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

lcp@329

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

lcp@304

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

lcp@329

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

lcp@329

135 
the front.

lcp@285

136 

lcp@329

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

lcp@329

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

lcp@329

139 
documentation.

lcp@285

140 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

145 
Poly/{\sc ml}.

lcp@285

146 

lcp@285

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

lcp@285

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

lcp@285

149 
3245: Logical Frameworks and 6453: Types).
