7827

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


2 
\usepackage{graphicx,../iman,../extra,../proof,../pdfsetup}

2656

3 

105

4 
%% $Id$


5 
%% run bibtex intro to prepare bibliography


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


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


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


9 

6611

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

105

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

3127

12 
Computer Laboratory \\ University of Cambridge \\


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


14 
With Contributions by Tobias Nipkow and Markus Wenzel

105

15 
}


16 
\makeindex


17 


18 
\underscoreoff


19 


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


21 


22 
\sloppy


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


24 


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


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


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


28 


29 
\pagenumbering{roman}


30 
\begin{document}


31 
\pagestyle{empty}


32 
\begin{titlepage}


33 
\maketitle


34 
\thispagestyle{empty}


35 
\vfill


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


37 
\end{titlepage}


38 


39 
\pagestyle{headings}


40 
\part*{Preface}

1878

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


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


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


44 
objectlogics:

105

45 
\begin{itemize}


46 
\item firstorder logic, constructive and classical versions


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

348

48 
hol}~\cite{mgordonhol}

105

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


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


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


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


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


54 
\end{itemize}


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


56 
allows singlestep proof construction. Isabelle provides control


57 
structures for expressing search procedures. Isabelle also provides


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


59 
which can be applied to objectlogics.


60 


61 
\index{ML}


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


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


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


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


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

6592

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

105

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


69 
used in computer science; there are many good


70 
texts~\cite{galton90,reeves90}.


71 


72 
\index{LCF}

348

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

105

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


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


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


77 
represents objectlevel rules by functions, while Isabelle represents them


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


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


80 


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


82 
The 1987 version introduced a higherorder metalogic with an improved


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


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


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


86 
support manysorted and higherorder logics. The current version provides


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


88 
development and will continue to change.


89 


90 
\subsubsection*{Overview}

296

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


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


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


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


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


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

105

97 


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


99 
They assume familiarity with the concepts presented here.


100 


101 


102 
\subsubsection*{Acknowledgements}

311

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

3127

104 
Stefan Berghofer and Sara Kalvala suggested improvements.

105

105 


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

184

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


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


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


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


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

3127

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


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


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

105

115 


116 
\newpage


117 
\pagestyle{plain} \tableofcontents


118 
\newpage


119 


120 
\newfont{\sanssi}{cmssi12}


121 
\vspace*{2.5cm}


122 
\begin{quote}


123 
\raggedleft


124 
{\sanssi


125 
You can only find truth with logic\\


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


127 
\bigskip


128 


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


130 
\end{quote}


131 


132 
\clearfirst \pagestyle{headings}


133 
\include{foundations}


134 
\include{getting}


135 
\include{advanced}


136 


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

6592

138 
\bibliography{../manual}

105

139 


140 
\input{intro.ind}


141 
\end{document}
