Re: [isabelle] Specifying subtype in a locale



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.