--- a/Admin/website/faq.html Wed Jul 12 17:00:33 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,245 +0,0 @@
-<?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>