*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Specifying subtype in a locale*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 30 Apr 2012 13:06:59 +1000*Cc*: munddr at gmail.com*In-reply-to*: <CAP0k5J5cMAK84odqZ7iLjmuT+W1THPFuYF2Y9dzc_q6hgFhmtQ@mail.gmail.com>*References*: <CAP0k5J5cMAK84odqZ7iLjmuT+W1THPFuYF2Y9dzc_q6hgFhmtQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1

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**:**[isabelle] Specifying subtype in a locale***From:*John Munroe

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