*To*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Subject*: Re: [isabelle] Specifying subtype in a locale*From*: John Munroe <munddr at gmail.com>*Date*: Mon, 30 Apr 2012 22:08:04 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F9E01D3.4060907@nicta.com.au>*References*: <CAP0k5J5cMAK84odqZ7iLjmuT+W1THPFuYF2Y9dzc_q6hgFhmtQ@mail.gmail.com> <4F9E01D3.4060907@nicta.com.au>

Hi, So does your locale expression seems to instantiate 'a in T and 'b in S to the same type? I was indeed hoping to only say 'b in S is a subtype of 'a in T rather than they the same type. Can I do that outside of locales? Thanks John On Mon, Apr 30, 2012 at 4:06 AM, Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote: > There isn't really a subtype notion for you to work with here, unless I've > dramatically misunderstood. Types are equal or they aren't. > > To make matters clearer, what T really does is fix 'a and f, and S fixes > both 'b and g. R inherits two type parameters, 'a and 'b, and there is no > reason for them to be related. > > Perhaps what you wanted to do was identify 'a from T with 'b from S in R? > This can be done with the locale expression: > > locale R = > T "f :: 'a" + > S "g :: 'a" h > for f g h > begin > > lemma "g = h" > by (rule ax[rule_format]) > > end > > Is that what you want? > > Yours, > Thomas. > > > On 28/04/12 13:03, John Munroe wrote: >> >> Hi, >> >> I have a rather urgent question about asserting relationships between >> types in a locale. Suppose I have the following 3 locales: >> >> locale T = >> fixes f :: 'a >> assumes ax: "\<forall> (a :: 'a) b. a = b" >> >> locale S = >> fixes g :: 'b >> and h :: 'b >> >> locale R = >> T f + >> S g h >> for f g h >> ... >> >> I want to prove the following >> >> lemma (in R) "g = h" >> >> using 'ax'. I want to assert in R that 'b in S is a subtype of 'a in >> T. With that asserted, the above lemma can be resolved, right? If I >> understand correctly, types are not first class citizens in >> Isabelle/HOL, but is there a work around? >> >> Thanks in advance for the help! >> >> John >> >

**References**:**[isabelle] Specifying subtype in a locale***From:*John Munroe

**Re: [isabelle] Specifying subtype in a locale***From:*Thomas Sewell

- Previous by Date: [isabelle] Multi-dimensional arrays
- Previous by Thread: Re: [isabelle] Specifying subtype in a locale
- Next by Thread: [isabelle] Documant typesetting in Isabelle
- Cl-isabelle-users April 2012 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