5790

1 
<html>


2 


3 
<head>

5794

4 
<! $Id$ >

5790

5 
<title>Isabelle</title>

5795

6 
</head>

5790

7 


8 
<body>


9 


10 
<h1>Isabelle </h1> <a href="http://www.in.tum.de/~isabelle/logo/"><img


11 
src="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a>


12 


13 
<p>


14 


15 
<strong>Isabelle</strong> is a popular generic theorem proving


16 
environment developed at Cambridge University (<a


17 
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU


18 
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).


19 


20 
<p>

5803

21 
<a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img


22 
src="cambridge.gif" width=145 border=0 align=right


23 
alt="[Cambridge]"></a> <a


24 
href="http://www.in.tum.de/~isabelle/munich.html"><img


25 
src="munich.gif" width=48 border=0 align=right alt="[Munich]"></a>

5790

26 

5803

27 
This page provides general information on Isabelle, more details are


28 
available on the local Isabelle pages at


29 
<a


30 
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">Cambridge</a>


31 
and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>.


32 
See there for informations on projects done with Isabelle, mailing list archives,


33 
research papers, the Isabelle bibliography, and Isabelle workshops and courses.


34 


35 


36 


37 
<h2>Obtaining Isabelle</h2>


38 
The latest version is <strong>Isabelle981</strong>, it is available


39 
from several mirror sites (given in alphabetical order):


40 


41 
<ul>


42 


43 
<li> <a


44 
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/">Cambridge


45 
(UK)</a>


46 


47 
<li> <a


48 
href="ftp://ftp.ci.uminho.pt/pub/mirrors/isabelle/index.html">Minho


49 
(Portugal)</a>


50 


51 
<li> <a


52 
href="http://www4.informatik.tumuenchen.de/~isabelle/dist/">Munich


53 
(Germany)</a>


54 


55 
<li> <a


56 
href="ftp://ftp.research.belllabs.com/dist/smlnj/isabelle/index.html">New


57 
Jersey (USA)</a>


58 


59 
</ul>


60 
<p>


61 


62 


63 
<h2>What is Isabelle?</h2>

5790

64 
Isabelle can be viewed from two main perspectives. On the one hand it


65 
may serve as a generic framework for rapid prototyping of deductive

5803

66 
systems. On the other hand, major existing logics like

5791

67 
<strong>Isabelle/HOL</strong> provide a theorem proving environment

5790

68 
ready to use for sizable applications.


69 


70 

5803

71 
<h3>Isabelle's Logics</h3>

5790

72 

5791

73 
The Isabelle distribution includes a large body of object logics and

5801

74 
other examples (see the <a href="library/">Isabelle theory

5791

75 
library</a>).

5790

76 


77 
<dl>


78 

5801

79 
<dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd>


80 
is a version of classical higherorder logic resembling that of the


81 
<A HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL System</A>.

5790

82 

5801

83 
<dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>


84 
adds Scott's Logic for Computable Functions (domain theory) to HOL.

5790

85 

5801

86 
<dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>


87 
provides basic classical and intuitionistic firstorder logic.


88 
It is polymorphic.

5790

89 

5801

90 
<dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd>

5790

91 
offers a formulation of ZermeloFraenkel set theory on top of FOL.


92 


93 
</dl>


94 


95 
<p>


96 


97 
Isabelle/HOL is currently the best developed object logic, including


98 
an extensive library of (concrete) mathematics, and various packages


99 
for advanced definitional concepts (like (co)inductive sets and


100 
types, wellfounded recursion etc.). The distribution also includes


101 
some large applications, for example correctness proofs of


102 
cryptographic protocols (<a

5803

103 
href="library/HOL/Auth/">HOL/Auth</a>) or communication protocols (<a


104 
href="library/HOLCF/IOA/">HOLCF/IOA</a>).

5790

105 


106 
<p>


107 


108 
Isabelle/ZF provides another starting point for applications, with a

5801

109 
slightly less developed library. Its definitional packages

5790

110 
are similar to those of Isabelle/HOL. Untyped ZF provides more

5798

111 
advanced constructions for sets than simplytyped HOL.

5790

112 


113 
<p>


114 

5798

115 
There are a few minor object logics that may serve as further

5790

116 
examples: <a

5801

117 
href="library/CTT/">CTT</a> is an

5790

118 
extensional version of MartinLöf's Type Theory, <a

5801

119 
href="library/Cube/">Cube</a> is

5790

120 
Barendregt's Lambda Cube. There are also some sequent calculus


121 
examples under <a

5801

122 
href="library/Sequents/">Sequents</a>,

5798

123 
including modal and linear logics. Again see the <a

5801

124 
href="library/">Isabelle theory

5792

125 
library</a> for other examples.

5790

126 


127 

5803

128 
<h3>Defining Logics</h3>

5790

129 


130 
Logics are not hardwired into Isabelle, but formulated within


131 
Isabelle's meta logic: <strong>Isabelle/Pure</strong>. There are

5791

132 
quite a lot of syntactic and deductive tools available in generic


133 
Isabelle. Thus defining new logics or extending existing ones


134 
basically works as follows:

5790

135 


136 
<ol>


137 


138 
<li> declare concrete syntax (via mixfix grammar and syntax macros),


139 


140 
<li> declare abstract syntax (as higherorder constants),


141 


142 
<li> declare inference rules (as metalogical propositions),


143 

5800

144 
<li> instantiate generic automatic proof tools (simplifier, classical


145 
tableau prover etc.),

5790

146 

5792

147 
<li> manually code special proof procedures (via tacticals or


148 
handwritten ML).

5790

149 


150 
</ol>


151 

5798

152 
The first three steps above are fully declarative and involve no ML

5791

153 
programming at all. Thus one already gets a decent deductive


154 
environment based on primitive inferences (by employing the builtin


155 
mechanisms of Isabelle/Pure, in particular higherorder unification


156 
and resolution).

5790

157 


158 
For sizable applications some degree of automated reasoning is


159 
essential. Instantiating existing tools like the classical tableau

5791

160 
prover involves only minimal MLbased setup. One may also write

5790

161 
arbitrary proof procedures or even theory extension packages in ML,


162 
without breaching system soundness (Isabelle follows the wellknown

5792

163 
<em>LCF system approach</em> to achieve a secure system).

5790

164 


165 

5801

166 

5790

167 
<h2>Further information</h2>

5803

168 
See the local Isabelle pages at


169 
<a

5801

170 
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">Cambridge</a>

5803

171 
and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>.

5795

172 
</body>


173 

5790

174 
</html>
