Re: [isabelle] unification question in Isabelle 2005



I'm impressed that you worked all of this out for yourself! Yes, this is standard behaviour. It goes back many years in Isabelle, and I believe in HOL too. In the LCF system (1970s), "anonymous" type variables in goals were simply forbidden in order to prevent this sort of confusion.

I'm not sure if there's a better way to handle polymorphism or not. However, this case illustrates that when stuck, it's good to enable Isabelle > Settings > Show Types.

Larry Paulson


On 8 Feb 2006, at 22:12, Dimitrios Vytiniotis wrote:

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?






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