*To*: Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>*Subject*: Re: [isabelle] unification question in Isabelle 2005*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 9 Feb 2006 09:59:15 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43EA6CB5.4050307@cis.upenn.edu>*References*: <17294.9451.576789.151325@raceme.rsise.anu.edu.au> <20051201031702.6082D2FFE@sunbroy2.informatik.tu-muenchen.de> <17294.27694.454478.142724@raceme.rsise.anu.edu.au> <1133442319.438ef50fb8a39@mailbroy.informatik.tu-muenchen.de> <43B9F0B5.8090705@rsise.anu.edu.au> <Pine.LNX.4.63.0601031206410.19491@atbroy10.informatik.tu-muenchen.de> <43EA68F7.70009@rsise.anu.edu.au> <43EA6CB5.4050307@cis.upenn.edu>

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?

**References**:**[isabelle] installation of Isabelle2004***From:*Jeremy Dawson

**[isabelle] unification question in Isabelle 2005***From:*Dimitrios Vytiniotis

- Previous by Date: Re: [isabelle] Finding a rule
- Next by Date: Re: [isabelle] nested \<^bsub> .. \<^esub>
- Previous by Thread: [isabelle] unification question in Isabelle 2005
- Next by Thread: Re: [isabelle] installation of Isabelle2004
- Cl-isabelle-users February 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list