lcp@105

1 
\documentstyle[a4,12pt,proof,iman,alltt]{article}

lcp@105

2 
%% $Id$

lcp@105

3 
%% run bibtex intro to prepare bibliography

lcp@105

4 
%% run ../sedindex intro to prepare index file

lcp@105

5 
%prth *(\(.*\)); \1;

lcp@105

6 
%{\\out \(.*\)} {\\out val it = "\1" : thm}

lcp@105

7 

lcp@105

8 
\title{Introduction to Isabelle}

lcp@105

9 
\author{{\em Lawrence C. Paulson}\\

lcp@105

10 
Computer Laboratory \\ University of Cambridge \\[2ex]

lcp@105

11 
{\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}

lcp@105

12 
}

lcp@105

13 
\date{}

lcp@105

14 
\makeindex

lcp@105

15 

lcp@105

16 
\underscoreoff

lcp@105

17 

lcp@105

18 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

lcp@105

19 

lcp@105

20 
\sloppy

lcp@105

21 
\binperiod %%%treat . like a binary operator

lcp@105

22 

lcp@105

23 
\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification

lcp@105

24 
\newcommand{\nand}{\mathbin{\lnot\&}}

lcp@105

25 
\newcommand{\xor}{\mathbin{\#}}

lcp@105

26 

lcp@105

27 
\pagenumbering{roman}

lcp@105

28 
\begin{document}

lcp@105

29 
\pagestyle{empty}

lcp@105

30 
\begin{titlepage}

lcp@105

31 
\maketitle

lcp@105

32 
\thispagestyle{empty}

lcp@105

33 
\vfill

lcp@105

34 
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}

lcp@105

35 
\end{titlepage}

lcp@105

36 

lcp@105

37 
\pagestyle{headings}

lcp@105

38 
\part*{Preface}

lcp@105

39 
\index{Isabelle!overview}

lcp@105

40 
\index{Isabelle!objectlogics supported}

lcp@105

41 
Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.

lcp@105

42 
It has been instantiated to support reasoning in several objectlogics:

lcp@105

43 
\begin{itemize}

lcp@105

44 
\item firstorder logic, constructive and classical versions

lcp@105

45 
\item higherorder logic, similar to that of Gordon's {\sc

lcp@105

46 
hol}~\cite{gordon88a}

lcp@105

47 
\item ZermeloFraenkel set theory~\cite{suppes72}

lcp@105

48 
\item an extensional version of MartinL\"of's Type Theory~\cite{nordstrom90}

lcp@105

49 
\item the classical firstorder sequent calculus, {\sc lk}

lcp@105

50 
\item the modal logics $T$, $S4$, and $S43$

lcp@105

51 
\item the Logic for Computable Functions~\cite{paulson87}

lcp@105

52 
\end{itemize}

lcp@105

53 
A logic's syntax and inference rules are specified declaratively; this

lcp@105

54 
allows singlestep proof construction. Isabelle provides control

lcp@105

55 
structures for expressing search procedures. Isabelle also provides

lcp@105

56 
several generic tools, such as simplifiers and classical theorem provers,

lcp@105

57 
which can be applied to objectlogics.

lcp@105

58 

lcp@105

59 
\index{ML}

lcp@105

60 
Isabelle is a large system, but beginners can get by with a small

lcp@105

61 
repertoire of commands and a basic knowledge of how Isabelle works. Some

lcp@105

62 
knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user

lcp@105

63 
interface. Advanced Isabelle theorem proving can involve writing \ML{}

lcp@105

64 
code, possibly with Isabelle's sources at hand. My book

lcp@105

65 
on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,

lcp@105

66 
including a simple theorem prover. Users must be familiar with logic as

lcp@105

67 
used in computer science; there are many good

lcp@105

68 
texts~\cite{galton90,reeves90}.

lcp@105

69 

lcp@105

70 
\index{LCF}

lcp@105

71 
{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an

lcp@105

72 
ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows

lcp@105

73 
ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an

lcp@105

74 
abstract type; tactics and tacticals support backward proof. But {\sc lcf}

lcp@105

75 
represents objectlevel rules by functions, while Isabelle represents them

lcp@105

76 
by terms. You may find my other writings~\cite{paulson87,paulsonhandbook}

lcp@105

77 
helpful in understanding the relationship between {\sc lcf} and Isabelle.

lcp@105

78 

lcp@105

79 
Isabelle does not keep a record of inference steps. Each step is checked

lcp@105

80 
at run time to ensure that theorems can only be constructed by applying

lcp@105

81 
inference rules. An Isabelle proof typically involves hundreds of

lcp@105

82 
primitive inferences, and would be unintelligible if displayed.

lcp@105

83 
Discarding proofs saves vast amounts of storage. But can Isabelle be

lcp@105

84 
trusted? If desired, objectlogics can be formalized such that each

lcp@105

85 
theorem carries a proof term, which could be checked by another program.

lcp@105

86 
Proofs can also be traced.

lcp@105

87 

lcp@105

88 
\index{Isabelle!release history} Isabelle was first distributed in 1986.

lcp@105

89 
The 1987 version introduced a higherorder metalogic with an improved

lcp@105

90 
treatment of quantifiers. The 1988 version added limited polymorphism and

lcp@105

91 
support for natural deduction. The 1989 version included a parser and

lcp@105

92 
pretty printer generator. The 1992 version introduced type classes, to

lcp@105

93 
support manysorted and higherorder logics. The current version provides

lcp@105

94 
greater support for theories and is much faster. Isabelle is still under

lcp@105

95 
development and will continue to change.

lcp@105

96 

lcp@105

97 
\subsubsection*{Overview}

lcp@105

98 
This manual consists of three parts.

lcp@105

99 
Part~I discusses the Isabelle's foundations.

lcp@105

100 
Part~II, presents simple online sessions, starting with forward proof.

lcp@105

101 
It also covers basic tactics and tacticals, and some commands for invoking

lcp@105

102 
Part~III contains further examples for users with a bit of experience.

lcp@105

103 
It explains how to derive rules define theories, and concludes with an

lcp@105

104 
extended example: a Prolog interpreter.

lcp@105

105 

lcp@105

106 
Isabelle's Reference Manual and ObjectLogics manual contain more details.

lcp@105

107 
They assume familiarity with the concepts presented here.

lcp@105

108 

lcp@105

109 

lcp@105

110 
\subsubsection*{Acknowledgements}

lcp@105

111 
Tobias Nipkow contributed most of the section on ``Defining Theories''.

lcp@105

112 
Sara Kalvala and Markus Wenzel suggested improvements.

lcp@105

113 

lcp@105

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

lcp@105

115 
parser generator, type classes, and the simplifier. Carsten Clasohm, Sonia

lcp@105

116 
Mahjoub, Karin Nimmermann and Markus Wenzel also made improvements.

lcp@105

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

lcp@105

118 
Poly/{\sc ml}. Many people have contributed to Isabelle's standard

lcp@105

119 
objectlogics, including Martin Coen, Philippe de Groote, Philippe No\"el.

lcp@105

120 
The research has been funded by the SERC (grants GR/G53279, GR/H40570) and

lcp@105

121 
by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).

lcp@105

122 

lcp@105

123 
\newpage

lcp@105

124 
\pagestyle{plain} \tableofcontents

lcp@105

125 
\newpage

lcp@105

126 

lcp@105

127 
\newfont{\sanssi}{cmssi12}

lcp@105

128 
\vspace*{2.5cm}

lcp@105

129 
\begin{quote}

lcp@105

130 
\raggedleft

lcp@105

131 
{\sanssi

lcp@105

132 
You can only find truth with logic\\

lcp@105

133 
if you have already found truth without it.}\\

lcp@105

134 
\bigskip

lcp@105

135 

lcp@105

136 
G.K. Chesterton, {\em The Man who was Orthodox}

lcp@105

137 
\end{quote}

lcp@105

138 

lcp@105

139 
\clearfirst \pagestyle{headings}

lcp@105

140 
\include{foundations}

lcp@105

141 
\include{getting}

lcp@105

142 
\include{advanced}

lcp@105

143 

lcp@105

144 

lcp@105

145 
\bibliographystyle{plain} \small\raggedright\frenchspacing

lcp@105

146 
\bibliography{atp,funprog,general,logicprog,theory}

lcp@105

147 

lcp@105

148 
\input{intro.ind}

lcp@105

149 
\end{document}
