# [isabelle] classes and interpretations

Hello,
I am trying to use the class mechanism for a collection of algebraic
structures and I got into the following problem:
class A = ord + times + one +
assumes
.... (axioms which ensures the existence of an infimum operation)
begin
definition
"inf_l a b = ..."
end
interpretation semilattice_inf "op <=" "op <" "inf_l";
by ...
The problem is now when I state some lemmas:
lemma l1: "inf_l (a:'a::A) b <= a"
lemma (in A) l2: "inf_l a b <= a"

`The first problem is that although lemmas l1 and l2 seem similar, they
``cannot
`be applied in the same contexts. Lemma l2 seem more general than lemma l1.

`The second problem. The fact that inf_l is an infimum operation, given
``by the
``interpretation, is available when proving lemma l1, but not when
``proving lemma l2.
``How should I state the interpretation such that it becomes available
``when proving
`a lemma like l2?
Best regards,
Viorel Preoteasa

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