Re: [isabelle] Question about classes



Hello Brian,

Thank you for your answer. Unfortunately both of the approaches
you suggested require defining the order in terms of possible orders on
the components, and this is something I don't want. I need to
have an un-interpreted order on pairs, and later I need to
instantiate it differently for different examples. The first definition
I used

Sup_less2 pair X u i = SUPR {v . pair v i < u} (% v . X v i)

could give me what I need. In examples I can instantiate both
the order and the function pair. However this approach,
using classes, does not bring any advantage because
everything becomes simpler if I use directly the order as a
parameter:

Sup_less2 lesspairs X u i = SUPR {v . lesspairs (v, i) u} (% v . X v i)

I have also tried to have the function pair defined by the class,
but then it was not possible to be of the type:
pair:: 'b * 'c => 'a.

Best regards,

Viorel

On 3/7/2010 5:25 PM, Brian Huffman wrote:
On Sat, Mar 6, 2010 at 3:55 PM, Viorel Preoteasa
<viorel.preoteasa at abo.fi>  wrote:
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
The problem is that Isabelle doesn't know what you mean by "(v, i)<
u", since the comparison operators have not been defined for pairs.
(That's what "No type arity * :: ord" is supposed to tell you.)

There are two ways to solve this problem:

1. Define the less-than operator for pairs, by giving an instance of
the ord class:

instantiation "*" :: (ord, ord) ord
begin
definition "a<  b = fst a<  fst b | (fst a = fst b&  snd a<  snd b)"
instance ..
end

The above definition is the lexicographic ordering, but other
definitions are certainly possible. You could also define less-than
pointwise:

instantiation "*" :: (ord, ord) ord
begin
definition "a<  b = fst a<  fst b&  snd a<  snd b"
instance ..
end

The drawback is that once you give a type class instance, you are
stuck with it: You must use the same definition of less-than for pairs
throughout the remainder of your theory.


2. Instead of writing "(v, i)<  u" in your definition, unfold whatever
definition of less-than on pairs that you mean. For example, if you
want the lexicographic ordering, you could define Sup_less2 like this:

definition
  "Sup_less2 X u i = SUPR {v . v<  fst u | (v = fst u&  i<  snd u)} (%
v . X v i)";

On the other hand, if you want a point-wise less-than ordering, you
would use this definition:

definition
  "Sup_less2 X u i = SUPR {v . v<  fst u&  i<  snd u} (% v . X v i)";


Hope this helps,
- Brian







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