7827

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

9695

2 
\usepackage{graphicx,../iman,../extra,../ttbox,../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

14148

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


35 
which is largely superseded by the Isabelle/HOL


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


37 
syntax and shows how to conduct proofs using the


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


39 
most Isabelle proofs are now written using the Isar


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


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


42 
on firstorder logic rather than higherorder logic.


43 

105

44 
\thispagestyle{empty}


45 
\vfill


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


47 
\end{titlepage}


48 


49 
\pagestyle{headings}


50 
\part*{Preface}

1878

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


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


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


54 
objectlogics:

105

55 
\begin{itemize}


56 
\item firstorder logic, constructive and classical versions


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

348

58 
hol}~\cite{mgordonhol}

105

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


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


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


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


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


64 
\end{itemize}


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


66 
allows singlestep proof construction. Isabelle provides control


67 
structures for expressing search procedures. Isabelle also provides


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


69 
which can be applied to objectlogics.


70 

14148

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


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


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


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

105

75 
\index{ML}

14148

76 
if you are prepared to writing \ML{}


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

6592

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

105

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


80 
used in computer science; there are many good


81 
texts~\cite{galton90,reeves90}.


82 


83 
\index{LCF}

348

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

105

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


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


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


88 
represents objectlevel rules by functions, while Isabelle represents them


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


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


91 


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


93 
The 1987 version introduced a higherorder metalogic with an improved


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


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


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

14148

97 
support manysorted and higherorder logics. The 1994 version introduced


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


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


100 
Isabelle is still under

105

101 
development and will continue to change.


102 


103 
\subsubsection*{Overview}

296

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


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


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


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


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


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

105

110 


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


112 
They assume familiarity with the concepts presented here.


113 


114 


115 
\subsubsection*{Acknowledgements}

311

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

14148

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

105

118 

8979

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


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


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


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


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


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


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


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


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


128 
\emph{Deduktion}.

105

129 


130 
\newpage


131 
\pagestyle{plain} \tableofcontents


132 
\newpage


133 


134 
\newfont{\sanssi}{cmssi12}


135 
\vspace*{2.5cm}


136 
\begin{quote}


137 
\raggedleft


138 
{\sanssi


139 
You can only find truth with logic\\


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


141 
\bigskip


142 


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


144 
\end{quote}


145 


146 
\clearfirst \pagestyle{headings}


147 
\include{foundations}


148 
\include{getting}


149 
\include{advanced}


150 


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

6592

152 
\bibliography{../manual}

105

153 

8828

154 
\printindex

105

155 
\end{document}
