*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Question about classes*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Sun, 07 Mar 2010 22:06:22 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <cc2478ab1003070725t4953c6a4x463eaa94faeec212@mail.gmail.com>*References*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com> <83424616-031E-4D84-AC94-E2A74D416BC2@cam.ac.uk> <4B92EB83.2040704@abo.fi> <cc2478ab1003070725t4953c6a4x463eaa94faeec212@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.1.8) Gecko/20100227 Thunderbird/3.0.3

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 typeThe 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:*Florian Haftmann

**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

**Re: [isabelle] Question about classes***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Question about classes
- Next by Date: Re: [isabelle] Question about classes
- Previous by Thread: Re: [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