*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Question about classes*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Thu, 11 Mar 2010 14:40:53 +0200*Cc*: isabelle-users at cl.cam.ac.uk, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4B95F1E6.2010702@informatik.tu-muenchen.de>*References*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com> <83424616-031E-4D84-AC94-E2A74D416BC2@cam.ac.uk> <4B92EB83.2040704@abo.fi> <cc2478ab1003070725t4953c6a4x463eaa94faeec212@mail.gmail.com> <4B94073E.1030603@abo.fi> <4B95F1E6.2010702@informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.23 (Windows/20090812)

Hello Florian, Thank you for your answer. In my development I need the order on 'a types as well as on pairs 'a * 'b, and I have a general result using a order on 'a which is instantiated later to a order on pairs. I think that I have finally reached a conclusion which is flexible enough, and also sound. I will define the class of well founded and transitive relations class well_founded_transitive = ord + assumes order_trans1: "x < y /\ y < z ==> x < z" ... begin...end I will also declare an uninterpreted constant consts pair:: "'a => 'b => 'c::well_founded_transitive" and I will prove all results based on these facts Later for concrete examples I instantiate both the class for pairs, as well as I define the pair using an axiom:

begin ...end axioms pair_def: "pair a b = (a, b)"; I have tested this approach and it seems to work. I also think that I am not introducing inconsistencies, because I only introduce this axiom once after I instantiate the class for pairs. Viorel Florian Haftmann wrote:

Hi Viorel,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.something like class pair_ord = fixes pair_less_eq :: "'a * 'b => 'a * 'b => bool" assumes ... is indeed beyond the rather restricted Isabelle polymorphism. Perhaps a possible solution is to formulate this order as locale and develope your specfication relative to this: locale pair_ord = fixes pair_less_eq :: "'a * 'b => 'a * 'b => bool" assumes ... begin definition ... lemma ... primrec ... ... end This could then be interpreted on different pair order predicates: definition pair_less_eq_nat_int :: "nat * int => nat * int => bool" where ... definition pair_less_eq_list_unit :: 'a list * unit => 'a list * unit => bool" where ... interpretation pair_ord_nat_int: pair_ord pair_less_eq_nat_int ... interpretation pair_ord_list_unit: pair_ord pair_less_eq_list_unit ... Hope this helps, Florian

**Follow-Ups**:**[isabelle] case _ of***From:*Viorel Preoteasa

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

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

**Re: [isabelle] Question about classes***From:*Florian Haftmann

- Previous by Date: [isabelle] PLMMS 2010: Last Call for Papers
- Next by Date: [isabelle] CFP: SSV'10 @ USENIX OSDI 2010
- Previous by Thread: Re: [isabelle] Question about classes
- Next by Thread: [isabelle] case _ of
- 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