Re: [isabelle] Question about classes



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.