Re: [isabelle] Uses of type quantification

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 MHonArc.