296

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

105

2 
%% $Id$


3 
%% run bibtex intro to prepare bibliography


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


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


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


7 


8 
\title{Introduction to Isabelle}


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


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


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


12 
}


13 
\date{}


14 
\makeindex


15 


16 
\underscoreoff


17 


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


19 


20 
\sloppy


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


22 


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


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


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


26 


27 
\pagenumbering{roman}


28 
\begin{document}


29 
\pagestyle{empty}


30 
\begin{titlepage}


31 
\maketitle


32 
\thispagestyle{empty}


33 
\vfill


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


35 
\end{titlepage}


36 


37 
\pagestyle{headings}


38 
\part*{Preface}


39 
\index{Isabelle!overview}


40 
\index{Isabelle!objectlogics supported}


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


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


43 
\begin{itemize}


44 
\item firstorder logic, constructive and classical versions


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

348

46 
hol}~\cite{mgordonhol}

105

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


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


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


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


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


52 
\end{itemize}


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


54 
allows singlestep proof construction. Isabelle provides control


55 
structures for expressing search procedures. Isabelle also provides


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


57 
which can be applied to objectlogics.


58 


59 
\index{ML}


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


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


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


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


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


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


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


67 
used in computer science; there are many good


68 
texts~\cite{galton90,reeves90}.


69 


70 
\index{LCF}

348

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

105

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


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


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


75 
represents objectlevel rules by functions, while Isabelle represents them


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


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


78 


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


80 
The 1987 version introduced a higherorder metalogic with an improved


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


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


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


84 
support manysorted and higherorder logics. The current version provides


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


86 
development and will continue to change.


87 


88 
\subsubsection*{Overview}

296

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


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


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


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


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


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

105

95 


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


97 
They assume familiarity with the concepts presented here.


98 


99 


100 
\subsubsection*{Acknowledgements}

311

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

105

102 
Sara Kalvala and Markus Wenzel suggested improvements.


103 


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

184

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


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


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


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


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


110 
No\"el. The research has been funded by the SERC (grants GR/G53279,


111 
GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:


112 
Types).

105

113 


114 
\newpage


115 
\pagestyle{plain} \tableofcontents


116 
\newpage


117 


118 
\newfont{\sanssi}{cmssi12}


119 
\vspace*{2.5cm}


120 
\begin{quote}


121 
\raggedleft


122 
{\sanssi


123 
You can only find truth with logic\\


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


125 
\bigskip


126 


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


128 
\end{quote}


129 


130 
\clearfirst \pagestyle{headings}


131 
\include{foundations}


132 
\include{getting}


133 
\include{advanced}


134 


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

873

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

105

137 


138 
\input{intro.ind}


139 
\end{document}
