Re: [isabelle] Specifying subtype in a locale
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?
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
> lemma "g = h"
> by (rule ax[rule_format])
> Is that what you want?
> On 28/04/12 13:03, John Munroe wrote:
>> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and