*To*: Tom Ridge <Thomas.Ridge at cl.cam.ac.uk>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Uses of type quantification*From*: Tom Ridge <Thomas.Ridge at cl.cam.ac.uk>*Date*: Sat, 10 Sep 2005 14:20:02 +0100*Cc*: Randy Pollack <rap at inf.ed.ac.uk>*In-reply-to*: <4321CA0E.5010809@cl.cam.ac.uk>*References*: <817439747567edb58bbd67d41ed34f6c@galois.com> <17185.22277.728926.231796@slim.inf.ed.ac.uk> <4c8f87bc8e3057d6a723fa6861863627@galois.com> <4321CA0E.5010809@cl.cam.ac.uk>*User-agent*: Mozilla Thunderbird 0.8 (X11/20040913)

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

I x = x by straightforward application of the axiom. So (I I) x = x by an application of transitivity of =. T Tom Ridge wrote:

Randy first convinced me that type quantification was worth adding. Oneof my motivations is that I want to produce a better Locales package.The Locales package works by internalising what were previously axiomsas additional assumptions (i.e. instead of proving C in context of axiomA, I prove A ==> C). If an axiom contains type variables, theinternalisation 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", andvia type instantiation, I can get "forall x:'b. I x = x" for any 'b. Thecorresponding assumption is "forall 'a. forall x:'a. I x = x", but ofcourse, this can't be expressed currently.The point is that forall x:'a. I x = xmay have to be used at several types, e.g. when proving "I I = I". If Iassertforall 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 etc. T John Matthews wrote:Thanks Randy, that's an good point. Many of the things we are tryingto do with HOLCF using the axclass package would also be useful whenusing locales. This ties in with Tom Ridge's work on making theoriesand 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

**References**:**[isabelle] Uses of type quantification***From:*John Matthews

**Re: [isabelle] Uses of type quantification***From:*Randy Pollack

**Re: [isabelle] Uses of type quantification***From:*John Matthews

**Re: [isabelle] Uses of type quantification***From:*Tom Ridge

- Previous by Date: [isabelle] Quickcheck for HOLCF domains?
- Next by Date: [isabelle] Proof for graph/tree theorems
- Previous by Thread: Re: [isabelle] Uses of type quantification
- Next by Thread: [isabelle] DATE 2006 paper submission deadline very soon
- Cl-isabelle-users September 2005 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