| What is Isabelle? | +
| Isabelle is a popular generic theorem proving + environment developed at Cambridge University (Larry Paulson) + and TU Munich (Tobias + Nipkow). See the Isabelle homepage for + more information. |
| Where can I find documentation? | +
| This + way, please. Also have a look at the theory + library. |
| Is it available for download? | +
| Yes, it is + available from several mirror + sites. It should run on most recent Unix systems (Solaris, + Linux, MacOS X, etc.). |
| There are lots of arrows in Isabelle. What's the + difference between ->, =>, -->, + and ==> ? | +
| Isabelle uses the => arrow for the function + type (contrary to most functional languages which use + ->). So a => b is the type of a function + that takes an element of a as input and gives you an + element of b as output. The long arrow --> + and ==> are object and meta level + implication. Roughly speaking, the meta level implication is + used to write down theorems (P ==> Q is a theorem + with P as premise and Q as conclusion), and + the object level implication is used in usual HOL formulas + (e.g. in definitions). |
| Where do I have to put those double quotes? |
| Isabelle distinguishes between inner + and outer 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 lemma, + consts, primrec, constdefs, + apply, done are without quotation marks, as are + the names of constants in constant definitions (consts + and constdefs) + |
| What is No such + constant: "_case_syntax" supposed to tell + me? |
| 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). + |
| Why doesn't Isabelle understand my + equation? |
| Isabelle's equality = binds + relatively strongly, so an equation like a = b & c might + not be what you intend. Isabelle parses it as (a = b) & + c. If you want it the other way around, you must set + explicit parentheses as in a = (b & c). This also applies + to e.g. primrec definitions (see below). |
| What does it mean "not a proper + equation"? |
| Most commonly this is an instance of the + question above. The primrec command (and others) expect + equations as input, and since equality binds strongly in Isabelle, + something like f x = b & c is not what you might expect + it to be: Isabelle parses it as (f x = b) & c (which is + indeed not a proper equation). To turn it into an equation you + must set explicit parentheses: f x = (b & c). |
| What does it mean + "Not a meta-equality (==)"? |
| This usually occurs if + you use = for constdefs. The constdefs + and defs commands expect not equations, but meta + equivalences. Just use the \<equiv> or == + signs instead of =. |
| What does "empty result sequence" + mean? |
| 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) |
| The Simplifier doesn't want to apply my + rule, what's wrong? |
| + 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 + Isabelle/Isar -> Settings -> Show Types and the + thm 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). Show Sorts, Show Constants, + and Trace Simplifier in the same menu may also be + helpful. + |
| If I do auto, it leaves me a goal + False. Is my theorem wrong? |
| Not necessarily. It just means that + auto transformed the goal into something that is not + provable any more. That could be due to auto 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. |
| Why does lemma + "1+1=2" fail? |
| Because it is not + necessarily true. Isabelle does not assume that 1 and 2 are + natural numbers. Try "(1::nat)+1=2" + instead. |
| How do I show + counter examples? |
+ There are a number of commands that try to find counter examples
+ automatically. Try quickcheck for small executable
+ examples and arith 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,
+ True & False ~= True | False is a counterexample of A
+ & B = A | B, and A = ~B ==> A & B ~= A | B is
+ another one. Sometimes Isabelle can help you to find the
+ counter example: just negate the proposition and do auto
+ or simp. If lucky, you are left with the assumptions you
+ need for the counter example to work. |
| X-Symbol doesn't seem to work. What can I + do? |
| 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 + Proof-General -> Options -> X-Symbol and (if you want to + save the setting for future sessions) select Options -> Save + Options in XEmacs. |
| How do I input those X-Symbols anyway? |
+ 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 \<and>). 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: --> is converted into the long
+ single arrow, /\ is converted into the 'and' symbol, the
+ sequence =_ into the equivalence sign, <_ into
+ less-or-equal, [| into opening semantic brackets, and so
+ on. For greek characters, the rotate command works well:
+ to input α type a and then C-.
+ (control and .). 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).
+ |
| I want to generate one of those flashy LaTeX + documents. How? |
| You will need to work with the + isatool command for this (in a Unix shell). The easiest + way to get to a document is the following: use isatool + mkdir to set up a new directory. The command will also create + a file called IsaMakefile in the current directory. Put + your theory file(s) into the new directory and edit the file + ROOT.ML 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 IsaMakefile is) + and type isatool make. 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. + |
| I have a large formalization with many + theories. Must I process all of them all of the time? |
| 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 ROOT.ML + file (as for generating a document) and use the command + isatool usedir -b HOL MyImage in that directory to create + an image MyImage using the parent logic HOL. + You should then be able to invoke Isabelle with Isabelle -l + MyImage and have everything that is loaded in ROOT.ML + instantly available. |
| Does Isabelle run on Windows? |
| 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 his + website. Be warned, though: emphasis is on minimal, + 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). + |