lcp@285

1 
\chapter*{Preface}

lcp@285

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

lcp@285

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

lcp@285

4 

lcp@285

5 
\index{Isabelle!objectlogics supported}

lcp@285

6 

lcp@285

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

lcp@285

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

lcp@304

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

lcp@304

10 
an impressive example. ALF~\cite{alf}, Coq~\cite{coq} and

lcp@304

11 
Nuprl~\cite{constable86} each support a fixed logic too, but one far

lcp@304

12 
removed from firstorder logic. They are explicitly concerned with

lcp@304

13 
computation. A diverse collection of logics  type theories, process

lcp@304

14 
calculi, $\lambda$calculi  may be found in the Computer Science

lcp@304

15 
literature. Such logics require proof support. Few proof procedures are

lcp@304

16 
known for them, but the theorem prover can at least automate routine steps.

lcp@285

17 

lcp@304

18 
A {\bf generic} theorem prover is one that can support a variety of logics.

lcp@304

19 
Some generic provers are noteworthy for their user interfaces

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@285

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

lcp@285

28 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

36 
develop new proof procedures using tactics and tacticals.

lcp@285

37 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

41 
Isabelle strong support for many logical formalisms involving variable

lcp@285

42 
binding.

lcp@285

43 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

50 
logic.

lcp@285

51 

lcp@285

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

lcp@285

53 

lcp@285

54 

lcp@285

55 
\section*{How to read this book}

lcp@304

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

62 

lcp@285

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

lcp@285

64 
distinct purposes:

lcp@285

65 
\begin{itemize}

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

72 
a Prolog interpreter.

lcp@285

73 

lcp@304

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

lcp@304

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

lcp@304

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

lcp@304

77 
should use it to locate facts quickly.

lcp@285

78 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

82 
\end{itemize}

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

87 
on a first reading.

lcp@285

88 

lcp@285

89 

lcp@285

90 

lcp@285

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

lcp@285

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

lcp@285

93 
higherorder metalogic with an improved treatment of quantifiers. The

lcp@285

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

lcp@285

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

lcp@285

96 
version introduced type classes, to support manysorted and higherorder

lcp@285

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

lcp@285

98 
much faster.

lcp@285

99 

lcp@285

100 
Isabelle is still under development. Projects under consideration include

lcp@285

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

lcp@285

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

lcp@285

103 
I hope but cannot promise to maintain upwards compatibility.

lcp@285

104 

lcp@285

105 
Isabelle is available by anonymous ftp:

lcp@285

106 
\begin{itemize}

lcp@285

107 
\item University of Cambridge\\

lcp@285

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

lcp@285

109 
directory {\tt ml}

lcp@285

110 

lcp@285

111 
\item Technical University of Munich\\

lcp@285

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

lcp@285

113 
directory {\tt local/lehrstuhl/nipkow}

lcp@285

114 
\end{itemize}

lcp@285

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

lcp@285

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

lcp@285

117 

lcp@285

118 

lcp@304

119 
\section*{Acknowledgements}

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

124 
Mahjoub and Karin Nimmermann also contributed.

lcp@285

125 

lcp@285

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

lcp@285

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

lcp@304

128 
\S\ref{sec:refdefiningtheories}, Chap.\ts\ref{simpchap},

lcp@304

129 
Chap.\ts\ref{DefiningLogics} and App.\ts\ref{app:TheorySyntax}\@. Carsten

lcp@304

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

lcp@304

131 
to Chap.\ts\ref{DefiningLogics}.

lcp@285

132 

lcp@304

133 
David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and

lcp@285

134 
Markus Wenzel suggested changes and corrections to the documentation.

lcp@285

135 

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

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

lcp@285

140 
Poly/{\sc ml}.

lcp@285

141 

lcp@285

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

lcp@285

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

lcp@285

144 
3245: Logical Frameworks and 6453: Types).

lcp@285

145 

lcp@285

146 

lcp@285

147 
\index{ML}
