Error Messages
Irritating and misleading error messages
This page collects error messages and other gotchas which are not helpful (to a beginner) for locating the error.
also or finally fails with empty result sequence
(or creates a strange result) Noschinl 13:27, 8 October 2010 (UTC)
Both commands try to apply a transitivity rule to the facts
calculation and this; the error message indicates that this failed.
The most obvious reason is that there is no transitivity rule declared for your case (such rules can be declared with the "trans" attribute).
But there is also a more subtle reason, which is unfortunately a lot
more confusing: For calculational reasoning, Isabelle tries to find
rules which "make progress". So if you accidentally proved
a <= b and ... <= b, Isabelle rules out the obvious transitivity rule
which would yield a <= b. If there is no other applicable rule, this
results in the aforementioned error message, otherwise a more complicated rule
is applied which results in a strange, unexpected result (which may very
well lead to an "empty result sequence" for the next "also".
Note that this filtering also takes place if you explicitly give a set of transitivity rules to also or finally.
exception TYPE raised in a lemma statement
Noschinl 13:27, 8 October 2010 (UTC)
exception TYPE raised (line 360 of "envir.ML"): expand_atom: ill-typed replacement
(line number may vary over version of Isabelle). This error can occur of you bind and use a pattern in a lemma statement, e.g.
lemma assumes "P foo" (is "P ?bar") shows "Q ?bar"
This is due to the fact that parsing and type inference for the whole lemma statement is done at once. Sufficiently verbose type annotations might help.
Illegal variable name: "a :: 'a" at command "definition"
When typing a definition and using the quotes at the wrong position, as in:
definition "a :: 'a" where "a = False"
Isabelle returns
Illegal variable name: "a :: 'a" At command "definition"
To the user, it is totally unclear why "a" is interpreted as a variable.
Quickcheck returns error but no error message
When using Quickcheck before it is set up properly, as in:
theory Scratch imports Datatype begin
theorem "False" quickcheck
there is an error, but no error message. Suggestion: No quickcheck generator is set up. To have a quickcheck generator set up, you should import Main.
Misleading variable naming in list comprehension
In
[ (a,y) . (a,y) <- xs, y <- ys]
the two y after the . are distinct ie not shared. For shared variable it should be written as
[ (a,y). (a,y) <- xs, y' <- ys, y = y' ]
Suggestion: Add this information to the list theory.
Misleading variable naming in set comprehension
The expression
{(v, v). v ∈ {''a'', ''b''}}
is actually interpreted as
{(va∷'a, v∷char list). v ∈ {''a'', ''b''}}