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>).

5798

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

5790

20 
from several <a href="dist/">mirror sites</a>.


21 


22 
<p>


23 


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


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

5791

26 
systems. On the other hand, major object logics like


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

5790

28 
ready to use for sizable applications.


29 


30 


31 
<h2>Object logics</h2>


32 

5791

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

5801

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

5791

35 
library</a>).

5790

36 


37 
<dl>


38 

5801

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


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


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

5790

42 

5801

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


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

5790

45 

5801

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


47 
provides basic classical and intuitionistic firstorder logic.


48 
It is polymorphic.

5790

49 

5801

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

5790

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


52 


53 
</dl>


54 


55 
<p>


56 


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


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


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


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


61 
some large applications, for example correctness proofs of


62 
cryptographic protocols (<a

5801

63 
href="library/HOL/Auth/">HOL/Auth</a>).

5790

64 


65 
<p>


66 


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

5801

68 
slightly less developed library. Its definitional packages

5790

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

5798

70 
advanced constructions for sets than simplytyped HOL.

5790

71 


72 
<p>


73 

5798

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

5790

75 
examples: <a

5801

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

5790

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

5801

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

5790

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


80 
examples under <a

5801

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

5798

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

5801

83 
href="library/">Isabelle theory

5792

84 
library</a> for other examples.

5790

85 


86 


87 
<h2>Defining Logics</h2>


88 


89 
Logics are not hardwired into Isabelle, but formulated within


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

5791

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


92 
Isabelle. Thus defining new logics or extending existing ones


93 
basically works as follows:

5790

94 


95 
<ol>


96 


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


98 


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


100 


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


102 

5800

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


104 
tableau prover etc.),

5790

105 

5792

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


107 
handwritten ML).

5790

108 


109 
</ol>


110 

5798

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

5791

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


113 
environment based on primitive inferences (by employing the builtin


114 
mechanisms of Isabelle/Pure, in particular higherorder unification


115 
and resolution).

5790

116 


117 
For sizable applications some degree of automated reasoning is


118 
essential. Instantiating existing tools like the classical tableau

5791

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

5790

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


121 
without breaching system soundness (Isabelle follows the wellknown

5792

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

5790

123 


124 

5801

125 
<H2>Mailing list</H2>


126 


127 
<P>Use the mailing list


128 
<A HREF="mailto: isabelleusers@cl.cam.ac.uk">isabelleusers@cl.cam.ac.uk</A>


129 
to discuss problems and results.


130 

5790

131 
<h2>Further information</h2>


132 

5801

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

5799

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

5796

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

5792

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

5799

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

5801

138 
cambridge Isabelle pages at <a


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

5792

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


141 
provide further information on Isabelle and related projects.

5790

142 

5795

143 
</body>


144 

5790

145 
</html>
