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.
On 8 Feb 2006, at 22:12, Dimitrios Vytiniotis wrote:
In Isabelle 2005, take the following lemma:
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)"
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'
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