Re: [isabelle] Uses of type quantification

The "example" I gave below is hopelessly incorrect :(

Try proving

(I I) x = x

under the same axiom, i.e.

forall x:'a. I x = x

Hopefully this actually does require two uses of the axiom. For my own benefit:

(I I) (x:'a) = I x

since I I = I, using the axiom type-instantiated as forall x:'a->'a. I x = x, instantiated at x = I. Then

I x = x

by straightforward application of the axiom. So

(I I) x = x

by an application of transitivity of =.


Tom Ridge wrote:
Randy first convinced me that type quantification was worth adding. One of my motivations is that I want to produce a better Locales package. The Locales package works by internalising what were previously axioms as additional assumptions (i.e. instead of proving C in context of axiom A, I prove A ==> C). If an axiom contains type variables, the internalisation cannot currently be carried out smoothly.

This is the point of my previous example, which I reproduce:

HOL is open, because I can assert an axiom "forall x:'a. I x = x", and via type instantiation, I can get "forall x:'b. I x = x" for any 'b. The corresponding assumption is "forall 'a. forall x:'a. I x = x", but of course, this can't be expressed currently.

The point is that

forall x:'a. I x = x

may have to be used at several types, e.g. when proving "I I = I". If I assert

forall x:'a. I x = x

as an axiom, I can prove

I I = I

because the axiom can be used at any type 'a. If I have an assumption

forall x:'a. I x = x

Then 'a is fixed and cannot be instantiated. To prove

I I = I

I need two assumptions

forall x:'a. I x = x and forall x:'a->'a. I x = x



John Matthews wrote:

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