Re: [isabelle] "Coercion inference failed"



On Wed, Mar 30, 2011 at 9:01 PM, Makarius <makarius at sketis.net> wrote:

> On Wed, 30 Mar 2011, egglue at gmail.com wrote:
>
>  axiomatization
>>> f :: "'a => 'b" and
>>> g :: "nat => nat" where
>>> ax : "f = g"
>>>
>>
>  Why are 'a and 'b fixed under "axiomatization"?
>>
>
> The specification is considered as one logical unit, where f and g are
> always the same local entity, with fixed types.  The context is essentially
> this:
>
>  fix_type 'a and 'b  -- "implicit"
>  fix g :: "'a => 'b" and g :: "nat => nat"
>  assume ax : "f = g"
>
> Later the types become arbitrary in the result, so the consts f and g in
> the target context can be used at different type.
>
> It is always the same game.  This is how naive polymorphism works.  There
> is no type quantification.  (It would make the logic very complicated, or
> break down).
>
>
I see. So Isabelle/HOL isn't truly polymorphic since there isn't type
quantification. Could you provide some pointers to material explaining the
naive polymorphism?

Thanks
Eg

>
>
>  It seems that I can produce very much the same declaration with:
>>
>> axiomatization
>> f:: "'a => 'b" and
>> g :: "nat => nat"
>>
>> axioms
>> ax : "f = g"
>>
>> Why is f polymorphic in "axioms" but not in "axiomatization"?
>>
>
> 'axioms' is an obsolete form, better do it like this:
>
>
> axiomatization
>  f :: "'a => 'b" and
>  g :: "nat => nat"
>
> axiomatization where
>  ax : "f = g"
>
> Separate specifications have separate scopes wrt. polymorphism.  The consts
> axiomatized in the first one can be used at different types at the second
> one.
>
>
>        Makarius
>




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