*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Specifying subtype in a locale*From*: Elsa L Gunter <egunter at illinois.edu>*Date*: Tue, 1 May 2012 09:04:01 -0500*Cc*: Thomas Sewell <Thomas.Sewell at nicta.com.au>, Brian Huffman <huffman at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAP0k5J4+DrqsvFqNuv1M9SQ4i80PgmgKJTHBN75uu3j9Oq4XXw@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> <CAP0k5J4+DrqsvFqNuv1M9SQ4i80PgmgKJTHBN75uu3j9Oq4XXw@mail.gmail.com>*Reply-to*: egunter at illinois.edu*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2

---Elsa On 5/1/12 6:04 AM, John Munroe wrote:

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, - BrianOn 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:*John Munroe

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

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

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] Specifying subtype in a locale
- 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