wenzelm@7827

1 
\documentclass[12pt,a4paper]{article}

wenzelm@48941

2 
\usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}

wenzelm@2656

3 

lcp@105

4 
%% run bibtex intro to prepare bibliography

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

8 

wenzelm@30118

9 
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}

lcp@105

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

paulson@3127

11 
Computer Laboratory \\ University of Cambridge \\

paulson@3127

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

paulson@3127

13 
With Contributions by Tobias Nipkow and Markus Wenzel

lcp@105

14 
}

lcp@105

15 
\makeindex

lcp@105

16 

lcp@105

17 
\underscoreoff

lcp@105

18 

lcp@105

19 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

lcp@105

20 

lcp@105

21 
\sloppy

lcp@105

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

lcp@105

23 

lcp@105

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

lcp@105

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

lcp@105

26 
\newcommand{\xor}{\mathbin{\#}}

lcp@105

27 

lcp@105

28 
\pagenumbering{roman}

lcp@105

29 
\begin{document}

lcp@105

30 
\pagestyle{empty}

lcp@105

31 
\begin{titlepage}

lcp@105

32 
\maketitle

paulson@14148

33 
\emph{Note}: this document is part of the earlier Isabelle documentation,

paulson@14148

34 
which is largely superseded by the Isabelle/HOL

paulson@14148

35 
\emph{Tutorial}~\cite{isatutorial}. It describes the oldstyle theory

paulson@14148

36 
syntax and shows how to conduct proofs using the

paulson@14148

37 
ML top level. This style of interaction is largely obsolete:

paulson@14148

38 
most Isabelle proofs are now written using the Isar

paulson@14148

39 
language and the Proof General interface. However, this paper contains valuable

paulson@14148

40 
information that is not available elsewhere. Its examples are based

paulson@14148

41 
on firstorder logic rather than higherorder logic.

paulson@14148

42 

lcp@105

43 
\thispagestyle{empty}

lcp@105

44 
\vfill

lcp@105

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

lcp@105

46 
\end{titlepage}

lcp@105

47 

lcp@105

48 
\pagestyle{headings}

lcp@105

49 
\part*{Preface}

paulson@1878

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

paulson@1878

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

paulson@1878

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

paulson@1878

53 
objectlogics:

lcp@105

54 
\begin{itemize}

lcp@105

55 
\item firstorder logic, constructive and classical versions

lcp@105

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

lcp@348

57 
hol}~\cite{mgordonhol}

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

63 
\end{itemize}

lcp@105

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

lcp@105

65 
allows singlestep proof construction. Isabelle provides control

lcp@105

66 
structures for expressing search procedures. Isabelle also provides

lcp@105

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

lcp@105

68 
which can be applied to objectlogics.

lcp@105

69 

paulson@14148

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

paulson@14148

71 
repertoire of commands and a basic knowledge of how Isabelle works.

paulson@14148

72 
The Isabelle/HOL \emph{Tutorial}~\cite{isatutorial} describes how to get started. Advanced Isabelle users will benefit from some

paulson@14148

73 
knowledge of Standard~\ML{}, because Isabelle is written in \ML{};

lcp@105

74 
\index{ML}

paulson@14148

75 
if you are prepared to writing \ML{}

paulson@14148

76 
code, you can get Isabelle to do almost anything. My book

paulson@6592

77 
on~\ML{}~\cite{paulsonml2} covers much material connected with Isabelle,

lcp@105

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

lcp@105

79 
used in computer science; there are many good

lcp@105

80 
texts~\cite{galton90,reeves90}.

lcp@105

81 

lcp@105

82 
\index{LCF}

lcp@348

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

lcp@105

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

lcp@105

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

lcp@105

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

lcp@105

87 
represents objectlevel rules by functions, while Isabelle represents them

lcp@105

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

lcp@105

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

lcp@105

90 

lcp@105

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

lcp@105

92 
The 1987 version introduced a higherorder metalogic with an improved

lcp@105

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

lcp@105

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

lcp@105

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

paulson@14148

96 
support manysorted and higherorder logics. The 1994 version introduced

paulson@14148

97 
greater support for theories. The most important recent change is the

paulson@14148

98 
introduction of the Isar proof language, thanks to Markus Wenzel.

paulson@14148

99 
Isabelle is still under

lcp@105

100 
development and will continue to change.

lcp@105

101 

lcp@105

102 
\subsubsection*{Overview}

lcp@296

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

lcp@296

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

lcp@296

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

lcp@296

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

lcp@296

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

lcp@296

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

lcp@105

109 

lcp@105

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

lcp@105

111 
They assume familiarity with the concepts presented here.

lcp@105

112 

lcp@105

113 

lcp@105

114 
\subsubsection*{Acknowledgements}

lcp@311

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

paulson@14148

116 
Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.

lcp@105

117 

paulson@8979

118 
Tobias Nipkow has made immense contributions to Isabelle, including the parser

paulson@8979

119 
generator, type classes, and the simplifier. Carsten Clasohm and Markus

paulson@8979

120 
Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also

paulson@8979

121 
helped. Isabelle was developed using Dave Matthews's Standard~{\sc ml}

paulson@8979

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

paulson@8979

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

paulson@8979

124 
The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,

paulson@8979

125 
GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical

paulson@8979

126 
Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm

paulson@8979

127 
\emph{Deduktion}.

lcp@105

128 

lcp@105

129 
\newpage

lcp@105

130 
\pagestyle{plain} \tableofcontents

lcp@105

131 
\newpage

lcp@105

132 

lcp@105

133 
\newfont{\sanssi}{cmssi12}

lcp@105

134 
\vspace*{2.5cm}

lcp@105

135 
\begin{quote}

lcp@105

136 
\raggedleft

lcp@105

137 
{\sanssi

lcp@105

138 
You can only find truth with logic\\

lcp@105

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

lcp@105

140 
\bigskip

lcp@105

141 

lcp@105

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

lcp@105

143 
\end{quote}

lcp@105

144 

lcp@105

145 
\clearfirst \pagestyle{headings}

wenzelm@48970

146 
\input{foundations}

wenzelm@48970

147 
\input{getting}

wenzelm@48970

148 
\input{advanced}

lcp@105

149 

lcp@105

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

wenzelm@48941

151 
\bibliography{manual}

lcp@105

152 

wenzelm@8828

153 
\printindex

lcp@105

154 
\end{document}
