*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Comparing polymorphic functions*From*: Eg Gloor <egglue at gmail.com>*Date*: Thu, 3 Feb 2011 18:49:26 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1102011612220.14100@atbroy100.informatik.tu-muenchen.de>*References*: <AANLkTik_QPi0HNJ9WShk7s_nc9jsbwH7_X9H6a-UDja-@mail.gmail.com> <4D415A30.7000104@dfki.de> <AANLkTi=2yDP7JNzG-tJHJE7JOXybL5YWiQEnCKkrWLU=@mail.gmail.com> <alpine.LNX.1.10.1102011612220.14100@atbroy100.informatik.tu-muenchen.de>

On Tue, Feb 1, 2011 at 3:18 PM, Makarius <makarius at sketis.net> wrote: > > For the logical framework, schematic variables are arbitrary (can be > instantiated), while free variables are fixed (local constant that might > become arbitrary after leaving the scope). > > Type inference has a third category of "parameters" that can get unified in > the type checking process. There is no user notation for that, apart from > nameless dummies "_". Otherwise type-inference insists that schematic and > free variables work out as they are written, no instantiation of schematic > variables here. > The above 'schematic_lemma' would give you a chance to instantiate > schematic variables in the course of reasoning, after type-checking has > already succeeded. Further confusion might be causes by proof tools that > choke on schematic type variables in a goal. > > If I understand this correctly, schematic variables can be instantiated but schematic *type* variables cannot due to a restriction of type-inference. Thus, there's no polymorphism of any kind at the meta-level. Likewise, with type variables because they are free variables. So it's expected that this wouldn't work: lemma "(x::'a) = (y::'b)" Because both 'a and 'b are free variables. But this works fine: const x :: 'a lemma "x = (y::'b)" Isn't 'a regarded as a free variable? How come it can be instantiated? Thanks again Eg > Makarius >

**Follow-Ups**:**Re: [isabelle] Comparing polymorphic functions***From:*Brian Huffman

**Re: [isabelle] Comparing polymorphic functions***From:*Makarius

**References**:**Re: [isabelle] Comparing polymorphic functions***From:*Makarius

- Previous by Date: [isabelle] Question about drule_tac
- Next by Date: Re: [isabelle] Question about drule_tac
- Previous by Thread: Re: [isabelle] Comparing polymorphic functions
- Next by Thread: Re: [isabelle] Comparing polymorphic functions
- Cl-isabelle-users February 2011 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