--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-content/faq.content Fri Apr 16 04:06:25 2004 +0200
@@ -0,0 +1,282 @@
+%title%
+Isabelle FAQ
+
+%meta%
+<style type="text/css">
+ <!--
+ .question { background-color:#C0C0C0; color:#000001; padding:3px; margin-top:12px; font-weight: bold; }
+ .answer { background-color:#E0E0E0; padding:3px; margin-top:3px; }
+ -->
+</style>
+
+
+%body%
+ <h2>General Questions</h2>
+ <table class="question" width="100%">
+ <tr>
+ <td>What is Isabelle?</td>
+ </tr>
+ </table>
+
+ <table class="answer" width="100%">
+ <tr><td>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.</td></tr>
+ </table>
+
+
+ <table class="question" width="100%">
+ <tr>
+ <td>Where can I find documentation?</td>
+ </tr>
+ </table>
+ <table class="answer" width="100%">
+ <tr><td><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>.</td></tr>
+ </table>
+
+ <table class="question" width="100%">
+ <tr>
+ <td>Is it available for download?</td>
+ </tr>
+ </table> <table class="answer" width="100%"> <tr><td>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.).</td></tr>
+ </table>
+
+
+ <h2>Syntax</h2>
+ <table class="question" width="100%">
+ <tr>
+ <td>There are lots of arrows in Isabelle. What's the
+ difference between <tt>-></tt>, <tt>=></tt>, <tt>--></tt>,
+ and <tt>==></tt> ?</td>
+ </tr>
+ </table>
+ <table class="answer" width="100%">
+ <tr><td>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 is
+ used to write down theorems (<tt>P ==> Q</tt> is a theorem
+ with <tt>P</tt> as premise and <tt>Q</tt> as conclusion), and
+ the object level implication is used in usual HOL formulas
+ (e.g. in definitions).</td></tr>
+ </table>
+
+ <table class="question" width="100%"><tr><td>Where do I have to put those double quotes?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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>)
+ </td></tr></table>
+
+ <table class="question" width="100%"><tr><td>What is <tt>No such
+ constant: "_case_syntax"</tt> supposed to tell
+ me?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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).
+ </td></tr></table>
+
+ <table class="question" width="100%"><tr><td>Why doesn't Isabelle understand my
+ equation?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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).</td></tr></table>
+
+ <table class="question" width="100%"><tr><td>What does it mean "not a proper
+ equation"?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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>.</td></tr></table>
+
+ <table class="question" width="100%"><tr><td>What does it mean
+ "<tt>Not a meta-equality (==)</tt>"?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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>. </td></tr></table>
+
+
+ <h2>Proving</h2>
+
+ <table class="question" width="100%"><tr><td>What does "empty result sequence"
+ mean?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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)</td></tr></table>
+
+
+ <table class="question" width="100%"><tr><td>The Simplifier doesn't want to apply my
+ rule, what's wrong?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>
+ 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.
+ </td></tr></table>
+
+
+ <table class="question" width="100%"><tr><td>If I do <tt>auto</tt>, it leaves me a goal
+ <tt>False</tt>. Is my theorem wrong?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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.</td></tr></table>
+
+
+ <table class="question" width="100%"><tr><td>Why does <tt>lemma
+ "1+1=2"</tt> fail?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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.</td></tr></table>
+
+
+ <table class="question" width="100%"><tr><td>How do I show
+ counter examples?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>
+ There are a number of commands that try to find counter examples
+ automatically. Try <code>quickcheck</code> for small executable
+ examples and <code>arith</code> for Presburger arithmetic.
+ 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
+ counter example: 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 counter example to work.</td></tr></table>
+
+
+ <h2>Interface</h2>
+
+ <table class="question" width="100%"><tr><td>X-Symbol doesn't seem to work. What can I
+ do?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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.</td></tr></table>
+
+ <table class="question" width="100%"><tr><td>How do I input those X-Symbols anyway?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>
+ 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).
+ </td></tr></table>
+
+ <h2>System</h2>
+
+ <table class="question" width="100%"><tr><td>I want to generate one of those flashy LaTeX
+ documents. How?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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.
+ </td></tr></table>
+
+
+ <table class="question" width="100%"><tr><td>I have a large formalization with many
+ theories. Must I process all of them all of the time?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td>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.</td></tr></table>
+
+ <table class="question" width="100%"><tr><td>Does Isabelle run on Windows?</td></tr></table>
+
+ <table class="answer" width="100%"><tr><td> After a fashion, yes,
+ but Isabelle is not being developed for Windows. A friendly user
+ (Norbert Völker) has managed to get a minimal Isabelle environment
+ to work on it. See the description on <a
+ href="http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">his
+ website</a>. Be warned, though: emphasis is on <em>minimal</em>,
+ working with Windows is no fun at all. To enjoy Isabelle in its
+ full beauty it is recommended to get a Linux distribution (they
+ are inexpensive, any reasonably recent one should work, dualboot
+ Windows/Linux should pose no problems).
+ </td></tr></table>
+