# Re: [isabelle] question on type classes and subclasses

The problem is that lemmaC is /not/ proved in the class C; it is proved without any surrounding context, but with a sort constraint C on the type 'a. This is, unfortunately, something different insofar as you cannot use such facts from within the context of the class.
```
```
It is therefore advisable to prove facts like this within the class context whenever possible, e.g.:
```
class C = A + assumes HC: "g x = x"
begin

lemma lemmaC: "g x = x"
â

end

or

context C
begin

lemma lemmaC: "g x = x"
â

end

or

lemma (in C) lemmaC: "g x = x"
â

Cheers,

Manuel

On 2017-02-06 16:55, Esseger wrote:
```
```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.