[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.