Re: [isabelle] Comparing polymorphic functions



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
>




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