[isabelle] Specifying subtype in a locale


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!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.