[isabelle] question on type classes and subclasses
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
(*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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and