Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Specifying subtype in a locale

Email Gateway (Aug 18 2022 at 19:24):

From: John Munroe <munddr@gmail.com>
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

Email Gateway (Aug 18 2022 at 19:26):

From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.

Email Gateway (Aug 18 2022 at 19:28):

From: John Munroe <munddr@gmail.com>
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

Email Gateway (Aug 18 2022 at 19:38):

From: John Munroe <munddr@gmail.com>
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

Email Gateway (Aug 18 2022 at 19:39):

From: Elsa L Gunter <egunter@illinois.edu>
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

Email Gateway (Aug 18 2022 at 20:03):

From: Brian Huffman <huffman@in.tum.de>
On Mon, Apr 30, 2012 at 11:08 PM, John Munroe <munddr@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@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

Email Gateway (Aug 18 2022 at 20:05):

From: John Munroe <munddr@gmail.com>
Thanks.

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

Thanks

John

Email Gateway (Aug 18 2022 at 20:07):

From: Elsa L Gunter <egunter@illinois.edu>
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

Last updated: Apr 26 2024 at 08:19 UTC