Common Errors

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
```