# [isabelle] Problems using subclasses

```Dear all,

I stumbled upon the following problem: it seems, that it is not possible
to access generic lemmas with sort-constraints for proving a subclass
relation:

theory Test
imports Main
begin

consts P :: "'a => 'a => bool"
consts Q :: "'a => 'a => bool"

class A =
fixes foo :: "'a => 'a"

class B = A +
fixes bar :: "'a => 'a"
assumes P: "P (x :: 'a) (foo x)"
begin
lemma PQ: "P (x :: 'a) y ==> Q x y" sorry
end

lemma Q: "Q (x :: 'a :: B) (foo x)"
using P[of x] PQ by auto

class C = A +
assumes QQ: "? y. Q (x :: 'a) y"

subclass (in B) C
proof
fix x :: 'a
have "bar x = bar x" by simp
(* since the term "bar x" is accepted, definitely, x
has sort B *)

note P[of x] PQ[of x]
(* one can access lemmas from B like P and PQ which have been
defined within the context *)

show "? y. Q x y" using Q[of x] ..
(* delivers "Type unification failed: Variable 'a::type not of sort B" *)
(* but not lemmas like Q, which are defined outside the class via
sort constraints *)
qed
end

Is this is known limitation, or did I make some mistake?
In my concrete application, I would have liked to use
ex_le_of_nat in src/HOL/Archimedean_Field to prove a subclass
relation, but could not. Instead I currently use ex_le_of_int
and copied the proof for ex_le_of_nat to finish the subclass proof,
which works, but is a bit unsatisfactory.

Best regards,
René

PS: I used Isabelle2013-1-RC3

```

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