[isabelle] unification question in Isabelle 2005
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] unification question in Isabelle 2005
- From: Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>
- Date: Wed, 08 Feb 2006 17:12:05 -0500
- In-reply-to: <43EA68F7.firstname.lastname@example.org>
- References: <email@example.com> <20051201031702.6082D2FFE@sunbroy2.informatik.tu-muenchen.de> <firstname.lastname@example.org> <email@example.com> <43B9F0B5.firstname.lastname@example.org> <Pine.LNX.email@example.com> <43EA68F7.firstname.lastname@example.org>
- User-agent: Mozilla Thunderbird 1.0.6 (X11/20050715)
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' 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.
ps: Did Isabelle 2004 have the same behaviour?
This archive was generated by a fusion of
Pipermail (Mailman edition) and