*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] "Coercion inference failed"*From*: Eg Gloor <egglue at gmail.com>*Date*: Thu, 31 Mar 2011 15:21:36 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1103302154110.28155@atbroy100.informatik.tu-muenchen.de>*References*: <00504502cc7d7b2c40049fb6a7ce@google.com> <alpine.LNX.1.10.1103302154110.28155@atbroy100.informatik.tu-muenchen.de>

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 >

**Follow-Ups**:**Re: [isabelle] "Coercion inference failed"***From:*Makarius

**References**:**Re: [isabelle] "Coercion inference failed"***From:*egglue

**Re: [isabelle] "Coercion inference failed"***From:*Makarius

- Previous by Date: Re: [isabelle] Converting apply-style induction to Structured Isar
- Next by Date: [isabelle] Pairs/tuples
- Previous by Thread: Re: [isabelle] "Coercion inference failed"
- Next by Thread: Re: [isabelle] "Coercion inference failed"
- Cl-isabelle-users March 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