# Re: [isabelle] Problems using subclasses

Hi René,

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 *)

`No, 'a has sort type, not B, as can be seen by showing the sorts with [[show_sorts]].
``Inside a class context, occurrences of class parameters are mapped to the locally fixed
``class parameter whenever type inference says that this is possible.
`

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

`Fact names from class contexts are localised similarly. You can refer to the global
``version of these facts with Test.P and Test.PQ. Then, type unification will fail.
`

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.

`This is a known problem. And for this reason, as many theorems as possible should be
``proven inside the class context. However, many theories have yet not been "optimised" in
``this respect.
`
Alternatively, you can do an instance declaration instead of a subclass declaration:
instance B \<subseteq> C

`Then, the type variable 'a has sort B in the proof, and you can use all you need. The
``difference to subclass is that you do not get the sublocale declaration B < C, that
``subclass implicitly issues, i.e., inside the context of B, you cannot refer to theorems
``from C.
`
Best,
Andreas
PS: All this is explained in the Isar-Ref manual, section 5.7.

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