| 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
- 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 -->.
- |
| 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. |
| Can Isabelle find - counterexamples? |
|
-
- For arithmetic goals, - 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 - counterexample: just negate the proposition and do auto - or simp. If lucky, you are left with the assumptions you - need for the counterexample to work. - - |
| ProofGeneral appears to hang when Isabelle is started. |
| 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). - |