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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and