*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] Question about classes*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sun, 7 Mar 2010 07:25:32 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4B92EB83.2040704@abo.fi>*References*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com> <83424616-031E-4D84-AC94-E2A74D416BC2@cam.ac.uk> <4B92EB83.2040704@abo.fi>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Question about classes***From:*Viorel Preoteasa

**References**:**[isabelle] argument order of List.foldr***From:*Brian Huffman

**Re: [isabelle] argument order of List.foldr***From:*Lawrence Paulson

**[isabelle] Question about classes***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] argument order of List.foldr
- Next by Date: Re: [isabelle] Question about classes
- Previous by Thread: [isabelle] Question about classes
- Next by Thread: Re: [isabelle] Question about classes
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list