Re: [isabelle] Specifying subtype in a locale



With a subtype, you have a "is_a" relation. If t1 is a subtype of t2, an x is of type t1 (x "is a" t1), then x is of type t2 (x "is a" t2), and x can be used anywhere a t2 is required. With sorts, you can group types together having some common features, such as having an associative, commutative binary operator. You may then prove facts for all the types in this class, based on the additional information that they have these features. However, no "is a" relationship exists between different types of a type class. Naturals with + are have sort associative-commutative, and lists with append have sort associative-commutative, but you can't use a list when you want a nat, and you can't use a nat when you want a list. Neither is a subtype of the other. We do have a subsort relation among type classes, however. So associative-commutative-with-identity is a subsort of associative-commutative. This may be, at least in part, the source of your confusion, and also why you can sometimes use type classes instead of subtyping.
---Elsa


On 5/1/12 11:49 AM, John Munroe wrote:
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.