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

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

- Previous by Date: Re: [isabelle] Multi-dimensional arrays
- Next by Date: [isabelle] New AFP entry: Ordinary Differential Equations
- Previous by Thread: Re: [isabelle] Multi-dimensional arrays
- 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