Admin/website/faq.html
author haftmann
Tue, 28 Jun 2005 16:12:03 +0200
changeset 16592 e7df213a1918
parent 16241 bf058cdf6841
child 17563 abb280dd3431
permissions -rw-r--r--
added project information in overview

<?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/docs.html">This way, please</a>.
          Also have a look at the <a href=
          "http://isabelle.in.tum.de/library/">theory library</a>.</dd>
    
      <dt>Is it available for download?</dt>
    
      <dd>Yes, it is available from <a href=
          "http://isabelle.in.tum.de/dist/">several mirror sites</a>. It should run
          on most recent Unix systems (Solaris, Linux, MacOS X, etc.).</dd>
    
</dl>
      <h2>Syntax</h2>

    <dl class="faq">
    
      <dt>There are lots of arrows in Isabelle. What's the difference between
          <tt>-&gt;</tt>, <tt>=&gt;</tt>, <tt>--&gt;</tt>, and <tt>==&gt;</tt>
          ?</dt>
    
      <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
          <code>--&gt;</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 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
          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, 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>
      <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
          -&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 does not assume that 1
          and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
    
      <dt>Can Isabelle 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 &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>
          </dd>
    
</dl>
      <h2>Interface</h2>

    <dl class="faq">
    
      <dt>ProofGeneral appears to hang when Isabelle is started.</dt>
      <dd><p>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse
      9.0/9.1</p>
      <p>RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be turned on
      in default locale. Unfortunately Proof General relies on 8-bit characters
      which are UTF8 prefixes in the output of proof assistants (inc Coq,
      Isabelle). These prefix characters are not flushed to stdout individually. As
      a workaround we must find a way to disable interpretation of UTF8 in the C
      libraries that Coq and friends use.</p>
    
      <p>Doing this inside PG/Emacs seems tricky; locale settings are set/inherited
      in strange ways. One solution is to run the Emacs process itself with an
      altered locale setting, for example, starting XEmacs by typing:</p>
    
      <ul class="shellcmd">
        <li>LC_CTYPE=en_GB Isabelle &amp;</li>
      </ul>
    
      <p>The supplied proofgeneral script makes this setting if it sees the string
      UTF in the current value of <tt class="shellcmd">LC_CTYPE</tt>.
      Depending on your distribution, this
      variable might also be called <tt class="shellcmd">LANG</tt>.</p>
    
      <p>Alternatively you can set <tt class="shellcmd">LC_CTYPE</tt> or
      <tt class="shellcmd">LANG</tt> inside a file <tt class="shellcmd">~/.i18n</tt>, which
      will be read by the shell. This will affect all applications, though.</p>
      
      <p>Suggestions for a better workaround inside Emacs would be welcomed;</p>
    
      <p>A related issue is warnings from x-symbol: "Emacs language environment
      and system locale specify different encoding, I'll assume `iso-8859-1'". This
      warning appears to be mainly harmless. Notice that the variable
      `buffer-file-coding-system' may determine the format that files are saved
      in.</p></dd>
    
      <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>
      <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>
    
    </dl>

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

</html>