[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