Re: [isabelle] Specifying subtype in a locale



Thanks.

Doesn't Isabelle's type system have type classes? Are they not like subtypes?

Thanks

John

On Tue, May 1, 2012 at 10:00 AM, Brian Huffman <huffman at in.tum.de> wrote:
> 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.