Re: [isabelle] Uses of type quantification



Thanks Randy, that's an good point. Many of the things we are trying to do with HOLCF using the axclass package would also be useful when using locales. This ties in with Tom Ridge's work on making theories and theorems inter-convertible in HOL light.

-john

On Sep 9, 2005, at 2:33 AM, Randy Pollack wrote:

Last autumn I came across examples that would have been improved by
some kind of type quantification in HOL.

Problems arise in relating two polymorphic properties:

(1)   (all 'a. !!(x::'a). P x)   ==>   all 'a. !!(x::'a). Q x

cannot be stated in HOL.  Perhaps the reason this isn't seen as a
common problem is that (1) can often be restated as

(2)   all 'a. (!!(x::'a). P x)   ==>   !!(x::'a). Q x

However, in a locale with assumption (!!(x::'a). P x) one might expect
to use the assumption at more than one type.

Randy






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