Re: [isabelle] Specifying subtype in a locale



Thanks.

That's one thing I don't quite understand: isn't a sort a collection
of types? What does it actually mean to have a value assigned to a
'type' declared in a typeclass?

Thanks

John

On Tue, May 1, 2012 at 3:04 PM, Elsa L Gunter <egunter at illinois.edu> wrote:
> Isabelle's type classes allow for sub-sorts, not subclasses.  While you can
> often achieve essentially that same effects with subsorts, they are not the
> same thing as subclassses.
> ---Elsa
>
>
> On 5/1/12 6:04 AM, John Munroe wrote:
>
> 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.