*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] Specifying subtype in a locale*From*: John Munroe <munddr at gmail.com>*Date*: Tue, 1 May 2012 12:04:08 +0100*Cc*: Thomas Sewell <Thomas.Sewell at nicta.com.au>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsia0FgkgUALn55PXu8nMEbdgDAuAUMmZKy1OULSvW385Kg@mail.gmail.com>*References*: <CAP0k5J5cMAK84odqZ7iLjmuT+W1THPFuYF2Y9dzc_q6hgFhmtQ@mail.gmail.com> <4F9E01D3.4060907@nicta.com.au> <CAP0k5J7euO+6oyBRVT-5k+Z6LZ8t8AH0vmGmw6CeSDDqQU_gFA@mail.gmail.com> <CAAMXsia0FgkgUALn55PXu8nMEbdgDAuAUMmZKy1OULSvW385Kg@mail.gmail.com>

Thanks. Doesn't Isabelle's type system have type classes? Are they not like subtypes? Thanks John On Tue, May 1, 2012 at 10:00 AM, Brian Huffman <huffman at in.tum.de> wrote: > On Mon, Apr 30, 2012 at 11:08 PM, John Munroe <munddr at gmail.com> wrote: >> 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? > > Isabelle's type system does not have a notion of "subtypes". It seems > like you really have two choices here: 1) Identify types 'b from S and > 'a from T, as Thomas suggested; or 2) fix an injective function from > type 'b into type 'a, as shown below. > > locale R = > T "f :: 'a" + > S "g :: 'b" h > for f g h + > fixes c :: "'b => 'a" > assumes inj_c: "inj c" > begin > > lemma "g = h" > apply (rule inj_c [THEN injD]) > apply (rule ax[rule_format]) > done > > end > > Hope this helps, > - Brian > >> 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 >>>> >>> >>

**Follow-Ups**:**Re: [isabelle] Specifying subtype in a locale***From:*Elsa L Gunter

**References**:**Re: [isabelle] Specifying subtype in a locale***From:*Brian Huffman

- Previous by Date: [isabelle] New AFP entry: Ordinary Differential Equations
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] Specifying subtype in a locale
- Next by Thread: Re: [isabelle] Specifying subtype in a locale
- Cl-isabelle-users May 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