# [isabelle] question on type classes and subclasses

Dear all,

`When trying to prove that a class C is a subclass of a class B, say, I
``am having trouble using lemmas that I have proved in C. The following
``stupid example illustrates it well:
`
class A = fixes f g::"'a â 'a" assumes HA: "f x = g x"
class B = A + assumes HB: "f x = x"
class C = A + assumes HC: "g x = x"
lemma lemmaC: "g x = (x::'a::C)" using HC by auto
subclass (in C) B
proof
(*fix x::'a show "f x = x" using HA[of x] HC[of x] by auto*)
fix x::'a show "f x = x" using HA[of x] lemmaC[of x] by auto
qed

`The proof fails, complaining that lemmaC[of x] makes no sense as the
``type 'a of x is not of class C (while it is...). On the other hand, the
``commented line succeeds. I do not understand what is going on here, as
``to me HC and lemmaC are the same statement.
`

`In my real use case, I want to use serious lemmas that I have proved in
``C, should I use another syntax for this?
`
Esseger

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