<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Isabelle FAQ</title>
<?include file="//include/htmlheader.include.html"?>
</head>
<body class="main">
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
<h2>General Questions</h2>
<dl class="faq">
<dt>What is Isabelle?</dt>
<dd>Isabelle is a popular generic theorem proving environment developed
at Cambridge University (<a href=
"http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU Munich
(<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). See the
<a href="http://isabelle.in.tum.de/">Isabelle homepage</a> for more
information.</dd>
<dt>Where can I find documentation?</dt>
<dd><a href="http://isabelle.in.tum.de/documentation.html">This way, please</a>.
Also have a look at the <a href=
"http://isabelle.in.tum.de/dist/library/">theory library</a>.</dd>
<dt>Is it available for download?</dt>
<dd>Yes, it is available from several mirror sites, e. g. from
<a href="http://isabelle.in.tum.de">Munich</a>. It runs on common
Unix systems (Linux, MacOS X, Solaris, etc.).</dd>
</dl>
<h2>Syntax</h2>
<dl class="faq">
<dt>There are lots of arrows in Isabelle/HOL. What's the difference between
<tt>-></tt>, <tt>=></tt>, <tt>--></tt>, and <tt>==></tt>
?</dt>
<dd>Isabelle uses the <tt>=></tt> arrow for the function type
(contrary to most functional languages which use <tt>-></tt>). So
<tt>a => b</tt> is the type of a function that takes an element of
<tt>a</tt> as input and gives you an element of <tt>b</tt> as output. The
long arrow <tt>--></tt> and <tt>==></tt> are object and meta level
implication. Roughly speaking, the meta level implication should only be
used when stating theorems where it separates the assumptions from the
conclusion. Whenever you need an implication inside a HOL formula, use
<code>--></code>.</dd>
<dt>Where do I have to put those double quotes?</dt>
<dd>Isabelle distinguishes between <em>inner</em> and <em>outer</em>
syntax. The outer syntax comes from the Isabelle framework, the inner
syntax is the one in between quotation marks and comes from the object
logic (in this case HOL). With time the distinction between the two
becomes obvious, but in the beginning the following rules of thumb may
work: types should be inside quotation marks, formulas and lemmas should
be inside quotation marks, rules and equations (e.g. for definitions)
should be inside quotation marks, commands like <tt>lemma</tt>,
<tt>consts</tt>, <tt>primrec</tt>, <tt>constdefs</tt>, <tt>apply</tt>,
<tt>done</tt> are without quotation marks, as are the names of constants
in constant definitions (<tt>consts</tt> and <tt>constdefs</tt>)</dd>
<dt>What is <tt>"No such constant: _case_syntax"</tt> supposed to tell
me?</dt>
<dd>You get this message if you use a case construct on a datatype and
have a typo in the names of the constructor patterns or if the order of
the constructors in the case pattern is different from the order in which
they where defined (in the datatype definition).</dd>
<dt>Why doesn't Isabelle/HOL understand my equation?</dt>
<dd>Isabelle's equality <tt>=</tt> binds relatively strongly, so an
equation like <tt>a = b & c</tt> might not be what you intend.
Isabelle parses it as <tt>(a = b) & c</tt>. If you want it the other
way around, you must set explicit parentheses as in <tt>a = (b &
c)</tt>. This also applies to e.g. <tt>primrec</tt> definitions (see
below).</dd>
<dt>What does it mean "not a proper equation"?</dt>
<dd>Most commonly this is an instance of the question above. The
<tt>primrec</tt> command (and others) expect equations as input, and
since equality binds strongly in Isabelle/HOL, something like <tt>f x = b
& c</tt> is not what you might expect it to be: Isabelle parses it as
<tt>(f x = b) & c</tt> (which is indeed not a proper equation). To
turn it into an equation you must set explicit parentheses: <tt>f x = (b
& c)</tt>.</dd>
<dt>What does it mean "<tt>Not a meta-equality (==)</tt>"?</dt>
<dd>This usually occurs if you use <tt>=</tt> for <tt>constdefs</tt>. The
<tt>constdefs</tt> and <tt>defs</tt> commands expect not equations, but
meta equivalences. Just use the <tt>\<equiv></tt> or <tt>==</tt>
signs instead of <tt>=</tt>.</dd>
</dl>
<h2>Proving</h2>
<dl class="faq">
<dt>What does "empty result sequence" mean?</dt>
<dd>It means that the applied proof method (or tactic) was unsuccessful.
It did not transform the goal in any way, or simply just failed to do
anything. You must try another tactic (or give the one you used more
hints or lemmas to work with)</dd>
<dt>The Simplifier doesn't want to apply my rule, what's wrong?</dt>
<dd>Most commonly this is a typing problem. The rule you want to apply
may require a more special (or just plain different) type from what you
have in the current goal. Use the ProofGeneral menu <tt>Isabelle/Isar
-> Settings -> Show Types</tt> and the <tt>thm</tt> command on the
rule you want to apply to find out if the types are what you expect them
to be (also take a look at the types in your goal). <tt>Show Sorts</tt>,
<tt>Show Constants</tt>, and <tt>Trace Simplifier</tt> in the same menu
may also be helpful.</dd>
<dt>If I do <tt>auto</tt>, it leaves me a goal <tt>False</tt>. Is my
theorem wrong?</dt>
<dd>Not necessarily. It just means that <tt>auto</tt> transformed the
goal into something that is not provable any more. That could be due to
<tt>auto</tt> doing something stupid, or e.g. due to some earlier step in
the proof that lost important information. It is of course also possible
that the goal was never provable in the first place.</dd>
<dt>Why does <tt>lemma "1+1=2"</tt> fail?</dt>
<dd>Because it is not necessarily true. Isabelle/HOL does not assume that 1
and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
<dt>Can Isabelle/HOL find counterexamples?</dt>
<dd>
<p>For arithmetic goals, <code>arith</code> finds counterexamples. For
executable goals, <code>quickcheck</code> tries to find a
counterexample. For goals of a more logical nature (including
quantifiers, sets and inductive definitions) <code>refute</code>
searches for a countermodel.</p>
<p>Otherwise, negate the proposition and instantiate (some) variables
with concrete values. You may also need additional assumptions about
these values. For example, <tt>True & False ~= True | False</tt> is
a counterexample of <tt>A & B = A | B</tt>, and <tt>A = ~B ==> A
& B ~= A | B</tt> is another one. Sometimes Isabelle can help you
to find the counterexample: just negate the proposition and do
<tt>auto</tt> or <tt>simp</tt>. If lucky, you are left with the
assumptions you need for the counterexample to work.</p>
</dd>
</dl>
<h2>Interface</h2>
<dl class="faq">
<dt>X-Symbol doesn't seem to work. What can I do?</dt>
<dd>The most common reason why X-Symbol doesn't work is: it's not
switched on yet. Assuming you are using ProofGeneral and have installed
the X-Symbol package, you still need to turn X-Symbol on in ProofGeneral:
select the menu items <tt>Proof-General -> Options -> X-Symbol</tt>
and (if you want to save the setting for future sessions) select
<tt>Options -> Save Options</tt> in XEmacs.</dd>
<dt>How do I input those X-Symbols anyway?</dt>
<dd>There are lots of ways to input x-symbols. The one that always works
is writing it out in plain text (e.g. for the 'and' symbol type
<tt>\<and></tt>). For common symbols you can try to "paint them in
ASCII" and if the xsymbol package recognizes them it will automatically
convert them into their graphical representation. Examples:
<tt>--></tt> is converted into the long single arrow, <tt>/\</tt> is
converted into the 'and' symbol, the sequence <tt>=_</tt> into the
equivalence sign, <tt><_</tt> into less-or-equal, <tt>[|</tt> into
opening semantic brackets, and so on. For greek characters, the
<code>rotate</code> command works well: to input α type
<code>a</code> and then <code>C-.</code> (control and <code>.</code>).
You can also display the grid-of-characters in the x-symbol menu to get
an overview of the available graphical representations (not all of them
already have a meaning in Isabelle, though).</dd>
</dl>
<h2>System</h2>
<dl class="faq">
<dt>I want to generate one of those flashy LaTeX documents. How?</dt>
<dd>You will need to work with the <tt class="shellcmd">isatool</tt> command for this (in
a Unix shell). The easiest way to get to a document is the following: use
<tt class="shellcmd">isatool mkdir</tt> to set up a new directory. The command will also
create a file called <tt class="shellcmd">IsaMakefile</tt> in the current directory. Put
your theory file(s) into the new directory and edit the file
<tt class="shellcmd">ROOT.ML</tt> in there (following the comments) to tell Isabelle which
of the theories to load (and in which order). Go back to the parent
directory (where the <tt class="shellcmd">IsaMakefile</tt> is) and type <tt class="shellcmd">isatool
make</tt>. Isabelle should then process your theories and tell you where
to find the finished document. For more information on generating
documents see the Isabelle Tutorial, Chapter 4.</dd>
<dt>I have a large formalization with many theories. Must I process all
of them all of the time?</dt>
<dd>No, you can tell Isabelle to build a so-called heap image. This heap
image can contain your preloaded theories. To get one, set up a directory
with a <tt class="shellcmd">ROOT.ML</tt> file (as for generating a document) and use the
command <tt class="shellcmd">isatool usedir -b HOL MyImage</tt> in that directory to
create an image <tt class="shellcmd">MyImage</tt> using the parent logic <tt class="shellcmd">HOL</tt>. You
should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt>
and have everything that is loaded in ROOT.ML instantly available.</dd>
<dt>Can I run Isabelle on Windows?</dt>
<dd>Not really. The Cygwin environment provides a Unixoid
look-and-feel that is sufficient for very basic Isabelle
functionality. See also <a
href="installation_notes_cygwin.html">Installation notes for
Cygwin/Windows.</a>
To try out Isabelle it might be much easier to use a Linux boot
CD, such as <a href="http://www.knoppix.org/">Knoppix</a>.</dd>
</dl>
</div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>
</body>
</html>