[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.