Re: [isabelle] Specifying subtype in a locale



Hi,

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?

Thanks

John

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
>>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.