<?xml version="1.0" encoding="utf-8"?>
<?DOCTYPE html PUBLIC
"-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Overview</title>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type" />
<link media="all" href="http://isabelle.in.tum.de/css/aelfwine.css" type="text/css" rel="stylesheet" />
<link media="all" href="http://isabelle.in.tum.de/css/isabelle_base.css" type="text/css" rel="stylesheet" />
<style media="screen" type="text/css">
/*<![CDATA[*/
@import url(http://isabelle.in.tum.de/css/isabelle_screen.css);
/*]]>*/
</style>
<link media="print" href="http://isabelle.in.tum.de/css/isabelle_print.css" type="text/css" rel="stylesheet" />
<link href="http://isabelle.in.tum.de/img/favicon.ico" type="image/icon" rel="icon" />
<meta content="en" name="language" />
<meta content="index follow" name="robots" />
<meta content="Tobias Nipkow, Lawrence Paulson, Makarius Wenzel, Gerwin Klein, Florian Haftmann, Tjark Weber, Johannes Hölzl" name="author" />
<script src="http://isabelle.in.tum.de/js/deobfuscate.js" type="text/javascript"></script>
<style>
.bnd { color: #65AD5A }
.cmd { color: #006699 }
.free { color: #0000FF }
.kwd { color: #009966 }
.box, .err, .wrn { font-size: 18; }
.box { background-color: white; padding: 2pt; }
.err, .wrn {
font: courier;
font-family: monospace;
line-height: 1.5;
padding: 1pt;
}
.err { background-color: #FFC1C1; }
.wrn { background-color: #EEE8AA; }
.key { font-variant: small-caps; }
</style>
</head>
<body class="main">
<div id="header">
<h1>Overview</h1>
<a href="http://isabelle.in.tum.de/index.html" id="isabelle_logo" name="isabelle_logo">
<img src="http://isabelle.in.tum.de/img/isabelle_logo.gif" alt="Isabelle home" width="114" height="100" />
</a>
<span class="headersep">·</span>
<a href="http://www21.in.tum.de/" id="univ_tum" target="_blank" name="univ_tum">
<img src="http://isabelle.in.tum.de/img/univ_tum.gif" alt="Isabelle in Munich" width="45" height="55" />
</a>
<span class="headersep">·</span>
<a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/Cambridge/" id="univ_cambridge" target="_blank" name="univ_cambridge">
<img src="http://isabelle.in.tum.de/img/univ_cambridge.gif" alt="Isabelle in Cambridge" width="169" height="55" />
</a>
</div>
<div class="hr"><hr /></div>
<div id="navigation">
<h2>Navigation</h2>
<ul>
<li><span><a href="http://isabelle.in.tum.de/index.html">Home</a></span></li>
<li><strong><a href="http://isabelle.in.tum.de/overview.html">Overview</a></strong></li>
<li><span><a href="http://isabelle.in.tum.de/installation.html">Installation</a></span></li>
<li><span><a href="http://isabelle.in.tum.de/documentation.html">Documentation</a></span></li>
<li><span><a href="https://isabelle.in.tum.de/community">Community</a></span></li>
</ul>
<div class="hr"><hr /></div>
<ul>
<li>
<div class="mirrorlist">
<h3>Site Mirrors:</h3>
<ul>
<li><a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html">Cambridge (.uk)</a></li>
<li><a href="http://isabelle.in.tum.de/overview.html">Munich (.de)</a></li>
<li><a href="http://mirror.cse.unsw.edu.au/pub/isabelle/overview.html">Sydney (.au)</a></li>
</ul>
</div>
</li>
</ul>
</div>
<div class="hr"><hr /></div>
<div id="content">
<h2>What is Isabelle?</h2>
<p>Isabelle is a generic proof assistant. It allows mathematical formulas to
be expressed in a formal language and provides tools for proving those
formulas in a logical calculus. The main application is the formalization of
mathematical proofs and in particular <em>formal verification</em>, which
includes proving the correctness of computer hardware or software and
proving properties of computer languages and protocols.</p>
<h2>A bluffer's glance at Isabelle</h2>
<p>The most widespread instance of Isabelle nowadays is
<em>Isabelle/HOL</em>, providing a higher-order logic theorem proving
environment ready to use for sizable applications. Anyway, most capabilities
mentioned here are not restricted to <em>Isabelle/HOL</em> in particular but
may be instantiated for arbitrary calculi.</p>
<p><em>Isabelle/HOL</em> includes powerful specification tools,
e.g. for datatypes, inductive definitions and functions with complex
pattern matching.</p>
<p>Proofs are conducted in the structured proof language <em>Isar</em>,
allowing for proof text naturally understandable for both humans
<em>and</em> computers.</p>
<p>For proofs, Isabelle incorporates some tools to improve the user's
productivity. In particular, Isabelle's <em>classical reasoner</em> can
perform long chains of reasoning steps to prove formulas. The
<em>simplifier</em> can reason with and about equations. Linear
<em>arithmetic</em> facts are proved automatically, various
<em>algebraic</em> decision procedures are provided. External
<em>first-order</em> provers can be invoked through
<em>sledgehammer</em>.</p>
<p>Abstract specifications are supported by a module system (aka locales),
of which type classes are a special case.</p>
<p>Isabelle provides excellent notational support: new notations can be
introduced, using normal mathematical symbols. Definitions and proofs may
include LaTeX source, from which Isabelle can automatically generate typeset
documents.</p>
<p><em>Isabelle/HOL</em> allows to turn executable specifications directly
into code in SML, OCaml, Haskell, and Scala.</p>
<p>Ample <a
href="http://isabelle.in.tum.de/documentation.html">documentation</a> is
available, including a <a
href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
Springer-Verlag.</p>
<p>Isabelle comes with a large theory library of formally verified
mathematics, including elementary number theory (for example, Gauss's law of
quadratic reciprocity), analysis (basic properties of limits, derivatives
and integrals), algebra (up to Sylow's theorem) and set theory (the relative
consistency of the Axiom of Choice). Also provided are numerous examples
arising from research into formal verification. A vast collection of
applications is accessible via the <a href="http://afp.sf.net">Archive of
Formal Proofs</a>, stemming both from mathematics and software
engineering.</p>
<p>Isabelle may serve as a generic framework for rapid prototyping of
deductive systems. These are formulated within Isabelle's logical framework
<em>Isabelle/Pure</em>, which is suitable for a variety of formal calculi
(e.g. axiomatic set theory). Instantiating the generic infrastructure
to a particular calculus usually requires only minimal setup in the Isabelle
implementation language ML. One may also write arbitrary proof procedures or
even theory extension packages in ML, without breaking system soundness
(Isabelle follows the well-known <em>LCF system approach</em> to achieve a
secure system).</p>
<h2>The Isabelle/jEdit user interface</h2>
<p>Isabelle/jEdit is a Prover IDE based on Isabelle/Scala and jEdit, and
provides an interaction model where the user sees and <em>freely</em> edits
a document. All the heavy machinery of Isabelle, like proof checking and
proof search, asynchronously runs in the background and supplies the
document with semantic information that is presented in standard ways
(highlighting, hyperlinks, tooltips, etc.).</p>
<p>This model of interaction offers plenty of space for parallelization.
Thus, Isabelle/jEdit does not only provide a more modern user interface but
additionally facilitates to transparently (for the user) make use of
multi-core architectures.</p>
<h3>Getting started</h3>
<p>Isabelle/jEdit is part of the official Isabelle release. To use it, just
follow the <a
href="http://isabelle.in.tum.de/installation.html">installation
instructions</a>.</p>
<p>To start Isabelle/jEdit from a command line use something similar to
<pre>$ISABELLE_HOME/bin/isabelle jedit</pre>
(On MacOSX click on the <em>Isabelle2013.app</em> icon and select
<em>Isabelle/jEdit</em>; on windows click <em>Isabelle2013.exe</em>.)</p>
<p><img src="jedit.png" alt="Isabelle/jEdit when first started." /></p>
<p>On the top half is the <em>main buffer</em>, this is where source text is
shown and editing takes place.</p>
<p>At the bottom of the lower half there are (among others) the buttons
<em>Output</em> and <em>README</em>. By default <em>README</em> is
selected, which gives some useful information. When selecting
<em>Output</em>, the panel shows the <em>output buffer</em>. This is where
messages from the command on which the cursor is positioned can be
found.</p>
<p>Part of the right margin is the button <em>Theories</em>, whose
corresponding panel can be consulted to check whether Isabelle/jEdit agrees
with you on what files are loaded and how much of them (problems are
indicated in red).</p>
<h3>An example session</h3>
<p>Let's formalize a simple fact about lists. Before doing so, you need to
start a <em>theory</em> (Isabelle parlance for: source file that bundles
definitions, facts and proofs under a common name). This is done by typing
<pre class=box>
<span class=cmd>theory</span> Test <span class=kwd>imports</span> Main <span class=kwd>begin</span>
<span class=kwd>end</span></pre>
into the main buffer, telling the system to start a theory <em>Test</em> on
top of the theory <em>Main</em> (the default starting point for Isabelle/HOL
theories). Afterwards continue typing between <span class=kwd>begin</span>
and <span class=kwd>end</span>.</p>
<p>At this point you may notice an error message in the output buffer
<pre class=err>Bad file name "Scratch.thy" for theory "Test"</pre>
This occurs because the default file name for theories is
<code>Scratch.thy</code> and can easily be resolved by saving the current
file under the name <code>Test.thy</code>.</p>
<p>Let's come back to the announced fact about lists: when combining the
head and the tail of a non-empty list, the result is the same list. Define
two functions for computing the head and tail of a list as follows:
<pre class=box>
<span class=cmd>fun</span> head :: "<span style="color:#9E2BE6">'a</span> list => <span style="color:#9E2BE6">'a</span>" <span class=kwd>where</span> "<span class=free>head</span> (<span class=free>x</span> # <span class=free>xs</span>) = <span class=free>x</span>"
<span class=cmd>fun</span> tail :: "<span style="color:#9E2BE6">'a</span> list => <span style="color:#9E2BE6">'a</span> list" <span class=kwd>where</span> "<span class=free>tail</span> (<span class=free>x</span> # <span class=free>xs</span>) = <span class=free>xs</span>"</pre>
There are a few things to note here. When defining <code>head</code>, a
warning occurs
<pre class=wrn>
Missing patterns in function definition:
<span class=free>head</span> [] = undefined</pre>
which tells you that the function is not defined on <code>[]</code>. This is
not an error but just a warning, since it might be intentional that the
function is undefined on empty lists. A similar warning is issued for
<code>tail</code>. Further note that the status of an identifier is
indicated by its color: free variables are rendered <span
class=free>blue</span>, bound variables <span class=bnd>green</span>,
defined constants black, etc. Moreover, many entities allow to jump to their
declaration by holding <span class=key>C</span> down while left-clicking on
them with the mouse. For <code>head</code> and <code>tail</code> this means
that you end up in the line containing the corresponding <code>fun</code>
keyword (even if that line is part of a different file). Test this behavior
by <span class=key>C</span>-left-clicking <code>#</code> in the definition
of <code>head</code>, which brings you to the theory <em>List</em> of
Isabelle/HOL's standard library. More specifically, to the line where the
list datatype is defined (since <code>#</code> refers to one of the
constructors of this datatype). The fastest way of going back is <span
class=key>C-`</span> (control together with backtick, not to be confused
with a single quote).</p>
<p>Now prove our little lemma (note that at this point <code>head</code> and
<code>tail</code> are printed black, since they are defined constants now):
<pre class=box>
<span class=cmd>lemma</span> "~(<span class=free>xs</span> = []) ==> head <span class=free>xs</span> # tail <span class=free>xs</span> = <span class=free>xs</span>"
<span class=cmd>by</span> (cases <span class=free>xs</span>) simp_all</pre>
</p>
<h3>Fancy mathematical symbols</h3>
<p>Using fancy mathematical symbols is really easy thanks to the code
completion facility of the SideKick plugin. Code completion works as
follows: you just enter a plain ASCII approximation of a symbol and, if
available, a popup offers you alternative choices. If you want to close the
popup just keep on typing or press <span class=key>Esc</span>. Otherwise,
navigate through the popup using the arror keys or the mouse, and press
<span class=key>Tab</span> when you are satisfied. For example, after typing
<code>==></code> a popup shows up containing ⟹. Many symbols also
have names that are close to their LaTeX names, e.g., <code>forall</code> to
obtain ∀, <code>exists</code> to obtain ∃, etc.</p>
</div>
<div class="hr"><hr /></div>
<div id="footer"><p>Last updated:</p></div>
</body>
</html>