berghofe@3096

1 
\documentclass[12pt]{article}

paulson@4239

2 
\usepackage{a4,../iman,../extra,../proof}

wenzelm@2656

3 

lcp@105

4 
%% $Id$

lcp@105

5 
%% run bibtex intro to prepare bibliography

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

9 

lcp@105

10 
\title{Introduction to Isabelle}

lcp@105

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

paulson@3127

12 
Computer Laboratory \\ University of Cambridge \\

paulson@3127

13 
\texttt{lcp@cl.cam.ac.uk}\\[3ex]

paulson@3127

14 
With Contributions by Tobias Nipkow and Markus Wenzel

lcp@105

15 
}

lcp@105

16 
\makeindex

lcp@105

17 

lcp@105

18 
\underscoreoff

lcp@105

19 

lcp@105

20 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

lcp@105

21 

lcp@105

22 
\sloppy

lcp@105

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

lcp@105

24 

lcp@105

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

lcp@105

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

lcp@105

27 
\newcommand{\xor}{\mathbin{\#}}

lcp@105

28 

lcp@105

29 
\pagenumbering{roman}

lcp@105

30 
\begin{document}

lcp@105

31 
\pagestyle{empty}

lcp@105

32 
\begin{titlepage}

lcp@105

33 
\maketitle

lcp@105

34 
\thispagestyle{empty}

lcp@105

35 
\vfill

lcp@105

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

lcp@105

37 
\end{titlepage}

lcp@105

38 

lcp@105

39 
\pagestyle{headings}

lcp@105

40 
\part*{Preface}

paulson@1878

41 
\index{Isabelle!overview} \index{Isabelle!objectlogics supported}

paulson@1878

42 
Isabelle~\cite{paulsonnatural,paulsonfound,paulson700} is a generic theorem

paulson@1878

43 
prover. It has been instantiated to support reasoning in several

paulson@1878

44 
objectlogics:

lcp@105

45 
\begin{itemize}

lcp@105

46 
\item firstorder logic, constructive and classical versions

lcp@105

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

lcp@348

48 
hol}~\cite{mgordonhol}

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

54 
\end{itemize}

lcp@105

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

lcp@105

56 
allows singlestep proof construction. Isabelle provides control

lcp@105

57 
structures for expressing search procedures. Isabelle also provides

lcp@105

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

lcp@105

59 
which can be applied to objectlogics.

lcp@105

60 

lcp@105

61 
\index{ML}

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

69 
used in computer science; there are many good

lcp@105

70 
texts~\cite{galton90,reeves90}.

lcp@105

71 

lcp@105

72 
\index{LCF}

lcp@348

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

77 
represents objectlevel rules by functions, while Isabelle represents them

lcp@105

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

lcp@105

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

lcp@105

80 

lcp@105

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

lcp@105

82 
The 1987 version introduced a higherorder metalogic with an improved

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

86 
support manysorted and higherorder logics. The current version provides

lcp@105

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

lcp@105

88 
development and will continue to change.

lcp@105

89 

lcp@105

90 
\subsubsection*{Overview}

lcp@296

91 
This manual consists of three parts. Part~I discusses the Isabelle's

lcp@296

92 
foundations. Part~II, presents simple online sessions, starting with

lcp@296

93 
forward proof. It also covers basic tactics and tacticals, and some

lcp@296

94 
commands for invoking them. Part~III contains further examples for users

lcp@296

95 
with a bit of experience. It explains how to derive rules define theories,

lcp@296

96 
and concludes with an extended example: a Prolog interpreter.

lcp@105

97 

lcp@105

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

lcp@105

99 
They assume familiarity with the concepts presented here.

lcp@105

100 

lcp@105

101 

lcp@105

102 
\subsubsection*{Acknowledgements}

lcp@311

103 
Tobias Nipkow contributed most of the section on defining theories.

paulson@3127

104 
Stefan Berghofer and Sara Kalvala suggested improvements.

lcp@105

105 

lcp@105

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

lcp@184

107 
parser generator, type classes, and the simplifier. Carsten Clasohm and

lcp@184

108 
Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann

lcp@184

109 
also helped. Isabelle was developed using Dave Matthews's Standard~{\sc

lcp@184

110 
ml} compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's

lcp@184

111 
standard objectlogics, including Martin Coen, Philippe de Groote, Philippe

paulson@3127

112 
No\"el. The research has been funded by the EPSRC (grants

paulson@3127

113 
GR/G53279, GR/H40570, GR/K57381, GR/K77051)

paulson@3127

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

lcp@105

115 

lcp@105

116 
\newpage

lcp@105

117 
\pagestyle{plain} \tableofcontents

lcp@105

118 
\newpage

lcp@105

119 

lcp@105

120 
\newfont{\sanssi}{cmssi12}

lcp@105

121 
\vspace*{2.5cm}

lcp@105

122 
\begin{quote}

lcp@105

123 
\raggedleft

lcp@105

124 
{\sanssi

lcp@105

125 
You can only find truth with logic\\

lcp@105

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

lcp@105

127 
\bigskip

lcp@105

128 

lcp@105

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

lcp@105

130 
\end{quote}

lcp@105

131 

lcp@105

132 
\clearfirst \pagestyle{headings}

lcp@105

133 
\include{foundations}

lcp@105

134 
\include{getting}

lcp@105

135 
\include{advanced}

lcp@105

136 

lcp@105

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

lcp@873

138 
\bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}

lcp@105

139 

lcp@105

140 
\input{intro.ind}

lcp@105

141 
\end{document}
