exception TYPE raised (line XXX of "envir.ML"): expand_atom: ill-typed replacement
This error can occur if 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.
Fix: Sufficiently verbose type annotations might help, e.g.
lemma assumes "P (foo ::'a)" (is "P ?bar") shows "Q (?bar :: 'a)"
Bad Name: "t :: T"
When typing a definition and using type annotations at the wrong position, as in:
definition "a :: bool" where "a ≡ False"
Isabelle returns Bad name: "a :: bool"
.
Fix: use type annotations in the where
clause instead:
definition "a" where "a :: bool ≡ False"
Not an equation | Not a meta-equality (≡)
Most commonly, these errors occur because Isabelle's equality =
binds relatively strongly.
For example
definition d where "d b = b ∧ False"
fun f where "f b = b ∧ False"
lead both to above error.
Isabelle parses the term t b = b ∧ False
as (t b = b) ∧ False
and not t b = (b ∧ False)
.
Fix:
Explicitly set the parentheses, e.g. t b = (b ∧ False)
(in an instantiation proof) Failed to refine any pending goal. Local statement fails to refine any pending goal.
When attempting to prove the necessary assumptions for the instantiation of a class, Isabelle may not infer the correct type.
Assume there is a class C
:
class C =
fixes f :: "'a option ⇒ 'a option"
assumes "f None = None"
When instantiating the class for an arbitrary type, e.g. int
, one goal is: f None = None
.
instantiation int :: C
begin
definition "f_int (x :: int option) ≡ (None :: int option)" (*arbitrary definition*)
instance proof
show "f None = None" sorry
qed
end
Isabelle does not infer the right type for f
(since f
may refer to another instantiation of C
).
Fix: Add a type annotation. For example:
show "f None = (None :: int option)" sorry