[isabelle] unification question in Isabelle 2005




Hello,

In Isabelle 2005, take the following lemma:

lemma foo
  assumes asm:"EX i. ALL Bs. (map_upds empty xs Bs) x = Some (Bs ! i)"
  shows       "EX i. ALL Bs. (map_upds empty xs Bs) x = Some (Bs ! i)"
apply(assumption)

Although the two lines are identical, we get back a fail message.
Apparently because Bs gets the type 'a list in the conclusion and
'b list in the premises. (And we don't seem able to 'obtain i' either).
We can fix the whole thing by putting type annotations.

Is this the expected behaviour? Why are 'a and 'b treated as
constants instead of as being able to unify with other types?

Thanks! Apologies if this issue has been brought up before.

-d

ps: Did Isabelle 2004 have the same behaviour?





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.