author wenzelm
Wed, 15 Feb 2006 21:34:55 +0100
changeset 19046 bc5c6c9b114e
parent 17661 994d010c0abd
permissions -rw-r--r--
removed distinct, renamed gen_distinct to distinct;

<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "">
<!-- $Id$ -->
<html xmlns="">

    <title>Isabelle FAQ</title>
    <?include file="//include/htmlheader.include.html"?>

<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=
          "">Larry Paulson</a>) and TU Munich
          (<a href="">Tobias Nipkow</a>). See the
          <a href="">Isabelle homepage</a> for more
      <dt>Where can I find documentation?</dt>
      <dd><a href="">This way, please</a>.
          Also have a look at the <a href=
          "">theory library</a>.</dd>
      <dt>Is it available for download?</dt>
      <dd>Yes, it is available from several mirror sites, e.&nbsp;g. from
          <a href="">Munich</a>. It runs on common
          Unix systems (Linux, MacOS&nbsp;X, Solaris, etc.).</dd>

    <dl class="faq">
      <dt>There are lots of arrows in Isabelle/HOL. What's the difference between
          <tt>-&gt;</tt>, <tt>=&gt;</tt>, <tt>--&gt;</tt>, and <tt>==&gt;</tt>
      <dd>Isabelle uses the <tt>=&gt;</tt> arrow for the function type
          (contrary to most functional languages which use <tt>-&gt;</tt>). So
          <tt>a =&gt; 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>--&gt;</tt> and <tt>==&gt;</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
      <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
      <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 &amp; c</tt> might not be what you intend.
          Isabelle parses it as <tt>(a = b) &amp; c</tt>. If you want it the other
          way around, you must set explicit parentheses as in <tt>a = (b &amp;
          c)</tt>. This also applies to e.g. <tt>primrec</tt> definitions (see
      <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
          &amp; c</tt> is not what you might expect it to be: Isabelle parses it as
          <tt>(f x = b) &amp; c</tt> (which is indeed not a proper equation). To
          turn it into an equation you must set explicit parentheses: <tt>f x = (b
          &amp; 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>\&lt;equiv&gt;</tt> or <tt>==</tt>
          signs instead of <tt>=</tt>.</dd>

    <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
          -&gt; Settings -&gt; 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>
            <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 &amp; False ~= True | False</tt> is
            a counterexample of <tt>A &amp; B = A | B</tt>, and <tt>A = ~B ==&gt; A
            &amp; 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>

    <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 -&gt; Options -&gt; X-Symbol</tt>
          and (if you want to save the setting for future sessions) select
          <tt>Options -&gt; 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>\&lt;and&gt;</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>--&gt;</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>&lt;_</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 &alpha; 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 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

      To try out Isabelle it might be much easier to use a Linux boot
      CD, such as <a href="">Knoppix</a>.</dd>

    <div class="hr"><hr/></div>
    <?include file="//include/footer.include.html"?>