*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Uses of type quantification*From*: Tom Ridge <Thomas.Ridge at cl.cam.ac.uk>*Date*: Fri, 09 Sep 2005 18:44:46 +0100*Cc*: isabelle-users at cl.cam.ac.uk, Randy Pollack <rap at inf.ed.ac.uk>*In-reply-to*: <4c8f87bc8e3057d6a723fa6861863627@galois.com>*References*: <817439747567edb58bbd67d41ed34f6c@galois.com> <17185.22277.728926.231796@slim.inf.ed.ac.uk> <4c8f87bc8e3057d6a723fa6861863627@galois.com>*User-agent*: Mozilla Thunderbird 0.8 (X11/20040913)

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

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 etc. T John Matthews wrote:

Thanks Randy, that's an good point. Many of the things we are trying todo with HOLCF using the axclass package would also be useful when usinglocales. This ties in with Tom Ridge's work on making theories andtheorems 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

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

**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

- Previous by Date: Re: [isabelle] Uses of type quantification
- Next by Date: [isabelle] Quickcheck for HOLCF domains?
- Previous by Thread: Re: [isabelle] Uses of type quantification
- Next by Thread: Re: [isabelle] Uses of type quantification
- 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