Re: [isabelle] Specifying subtype in a locale



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.