--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/faq.html Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,271 @@
+<?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">
+<?cvs id="$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>-></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 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, 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 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 & 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>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>
+
+ <p><tt>$ LC_CTYPE=en_GB Isabelle &</tt></p>
+
+ <p>The supplied proofgeneral script makes this setting if it sees the string
+ UTF in the current value of LC_CTYPE. Depending on your distribution, this
+ variable might also be called <tt>LANG</tt>.</p>
+
+ <p>Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which
+ will be read by the shell. This will affect all applications, though. [
+ suggestions for a better workaround inside Emacs would be welcome ]</p>
+
+ <p>NB: 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 -> 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>isatool</tt> command for this (in
+ a Unix shell). The easiest way to get to a document is the following: use
+ <tt>isatool mkdir</tt> to set up a new directory. The command will also
+ create a file called <tt>IsaMakefile</tt> in the current directory. Put
+ your theory file(s) into the new directory and edit the file
+ <tt>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>IsaMakefile</tt> is) and type <tt>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>ROOT.ML</tt> file (as for generating a document) and use the
+ command <tt>isatool usedir -b HOL MyImage</tt> in that directory to
+ create an image <tt>MyImage</tt> using the parent logic <tt>HOL</tt>. You
+ should then be able to invoke Isabelle with <tt>Isabelle -l MyImage</tt>
+ and have everything that is loaded in ROOT.ML instantly available.</dd>
+
+ <dt>Does Isabelle run on Windows?</dt>
+
+ <dd>After a fashion, yes, but Isabelle is not being developed for
+ Windows. See the <a href="dist/installation_notes_cygwin.html">installation notes</a> for windows.
+ If the approach presented there is not sufficient for your purpose, consider a
+ dualboot Windows/Linux system.</dd>
+
+ </dl>
+
+ </div>
+ <div class="hr"><hr/></div>
+ <?include file="//include/footer.include.html"?>
+</body>
+
+</html>