Re: [isabelle] Specifying subtype in a locale



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





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