105

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


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


46 
hol}~\cite{gordon88a}


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}


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


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 
Isabelle does not keep a record of inference steps. Each step is checked


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


81 
inference rules. An Isabelle proof typically involves hundreds of


82 
primitive inferences, and would be unintelligible if displayed.


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


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


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


86 
Proofs can also be traced.


87 


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


89 
The 1987 version introduced a higherorder metalogic with an improved


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


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


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


93 
support manysorted and higherorder logics. The current version provides


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


95 
development and will continue to change.


96 


97 
\subsubsection*{Overview}


98 
This manual consists of three parts.


99 
Part~I discusses the Isabelle's foundations.


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


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


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


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


104 
extended example: a Prolog interpreter.


105 


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


107 
They assume familiarity with the concepts presented here.


108 


109 


110 
\subsubsection*{Acknowledgements}


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


112 
Sara Kalvala and Markus Wenzel suggested improvements.


113 


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

184

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


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


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


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


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


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


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


122 
Types).

105

123 


124 
\newpage


125 
\pagestyle{plain} \tableofcontents


126 
\newpage


127 


128 
\newfont{\sanssi}{cmssi12}


129 
\vspace*{2.5cm}


130 
\begin{quote}


131 
\raggedleft


132 
{\sanssi


133 
You can only find truth with logic\\


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


135 
\bigskip


136 


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


138 
\end{quote}


139 


140 
\clearfirst \pagestyle{headings}


141 
\include{foundations}


142 
\include{getting}


143 
\include{advanced}


144 


145 


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


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


148 


149 
\input{intro.ind}


150 
\end{document}
