- 1 General Questions
- 2 Syntax
- 3 Proving
- 3.1 What does empty result sequence mean?
- 3.2 The Simplifier doesn't want to apply my rule, what's wrong?
- 3.3 If I do auto, it leaves me a goal False. Is my theorem wrong?
- 3.4 Can Isabelle/HOL find counterexamples?
- 3.5 Sometimes when I enter a lemma proposition it takes a long time until proof mode is entered. What's the reason for this?
- 3.6 Is there any chance to model generic monads and such?
- 4 System
- 5 Isabelle/JEdit Interface
What is Isabelle?
Where can I find documentation?
On the main Isabelle page: Documentation.
Is it available for download?
Yes, on the main Isabelle page: Download and installation.
There are lots of arrows in Isabelle/HOL. 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 arrows --> and ==> are object and meta level implication, respectively. Roughly speaking, meta level implication should be used to separate the assumptions from the conclusion in rule statements. Whenever you need an implication inside a closed 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, definition, primrec, inductive, apply, done are without quotation marks, as are the names of constants in constant definitions (consts and constdefs)
Why doesn't Isabelle/HOL understand my equation?
Isabelle's equality = binds relatively strongly, so a formula 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). You may also consider to use the equivalence operator <-> which has lower precedence than =.
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/HOL, 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), or sue the equivalence operator <-> instead: f x <-> (b &c)
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 Proof General 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.
Can Isabelle/HOL find counterexamples?
For executable goals,
quickcheck tries to find a counterexample. For goals of a more logical nature (including quantifiers, sets and inductive definitions),
nitpick searches for a counter model. For arithmetic goals,
arith finds counterexamples.
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.
Sometimes when I enter a lemma proposition it takes a long time until proof mode is entered. What's the reason for this?
This is due to auto quickcheck: each toplevel goal entered in interactive mode is automatically checked for counterexamples. You can set a timeout for this feature or turn it off using the Proof General menu Isabelle/Isar -> Settings.
Is there any chance to model generic monads and such?
Perhaps the AWE toolkit provides a solution for your problem.
I want to generate one of those flashy LaTeX documents. How?
You will need to work with the isabelle command in a Unix shell. The easiest way to get to a document is the following: use isabelle 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 isabelle 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 pre-loaded theories. To get one, set up a directory with a ROOT.ML file (as for generating a document) and use the command isabelle usedir -b HOL My_Image in that directory to create an image My_Image using the parent logic HOL. You should then be able to invoke Isabelle with isabelle emacs -l My_Image and have everything that is loaded in ROOT.ML instantly available.
To give Isabelle/Isar theories a more mathematical appearance we map ASCII characters to more graphical Unicode characters, like ∀ instead of ALL.
How do I input those symbols anyway?
There are lots of ways to input symbols. The one that always works is to write it out in plain text (e.g. for the 'and' symbol type \<and>), wait for the symbol to appear, and then press the tab-key. For common symbols you can try to "paint them in ASCII" and if Isabelle/JEdit 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, <= into less-or-equal, [| into opening semantic brackets, and so on. You can also take a look in the symbols panel at the bottom of the Isabelle/JEdit window to get an overview of the available symbols.
Another method is to enter them in LaTeX style, e.g., \circ, \and and \forall, then wait for the symbol to appear, and then press the tab-key.