# [isabelle] Question about classes

Hello,
I have the following class definition:
class well_founded_transitive = ord +
assumes order_trans1: "x < y ==> y < z ==> y < z"
and less_eq_def: "x <= y =( x = y \/ x < y)"

` and less_induct1 [case_names less]: "(!!x . (!!y . y < x ==> y) ==>
``x) ==> a"
`begin
definition
"Sup_less P w = SUPR {v . v < w} P";
end
and I have the following definition
definition

` "Sup_less2 pair X (u::'a::well_founded_transitive) i = SUPR {v . pair
``v i < u} (% v . X v i)";
`
However, what I am interested in is something like:
definition
"Sup_less2 X u i = SUPR {v . (v, i) < u} (% v . X v i)";
However, with the second definition I get the error message:
*** Type unification failed: No type arity * :: ord
*** Type error in application: Incompatible operand type
***
*** Operator: op < :: ??'a × ??'b => ??'a × ??'b => bool
*** Operand: (v, i) :: ??'a × ??'b
***
*** At command "definition".
Is there a way to achieve the second kind of definition for Sup_less2?
I need the order to be over pairs, however, I must have an un-instantiated
order relation.
Best regards,
Viorel Preoteasa

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