*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] "partial order" type?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 14 Nov 2011 06:29:38 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4B31628E-B5BB-485F-A5C6-68813E5C04E2@cam.ac.uk>*References*: <F1C12596-4773-47CF-9D5E-67B727B39F93@cam.ac.uk> <CAAMXsiasT2rDZoFeJ3BtrsnMOVbhjFqe4uYojXPQ0BNAZ=JLcA@mail.gmail.com> <4B31628E-B5BB-485F-A5C6-68813E5C04E2@cam.ac.uk>*Sender*: huffman.brian.c at gmail.com

On Sun, Nov 13, 2011 at 9:45 PM, John Wickerson <jpw48 at cam.ac.uk> wrote: > Thanks very much Brian, that all makes sense to me. I was expecting you to tell me to tap into the type class "order" in some way (which is defined in http://isabelle.in.tum.de/dist/library/HOL/Orderings.html). Which is to say: do I really have to define my own "is_partialorder" predicate from scratch? [I forgot to reply also to the list with my first response; now we're back on the list again.] Now to answer your follow-up question: If you want to avoid defining an is_partialorder predicate from scratch, you can use the locale predicates that come from the existing type classes. The only complication here is that the locale predicate for class order takes *two* arguments, one for "op <=" and one for "op <": "class.order" :: "('a => 'a => bool) => ('a => 'a => bool) => bool" (Also note that the relations are modeled as binary predicates, rather than as sets of pairs.) So you could define your type in terms of pairs of relations, like this: typedef 'a partialorder = "{(le :: 'a => 'a => bool, lt :: 'a => 'a => bool). class.order le lt}" The definition of a partial order is still simple enough that I'm not sure if using the class predicate like this is worth the trouble. For other, more complicated type classes it would probably be worth it, though. If your main concern is getting copies of all the theorems that exist in class "order", then you could achieve this with a locale instantiation. Specifically, you could define parameterized versions of "op <=" and "op <" with these types: my_le :: 'a partialorder => 'a => 'a => bool my_lt :: 'a partialorder => 'a => 'a => bool And then do a locale instantiation like this: instantiation my_partialorder: order "my_le r" "my_lt r" <proof> after which you would have copies of all the theorems from the order class. - Brian > > On 13 Nov 2011, at 18:58, Brian Huffman wrote: > >> On Sun, Nov 13, 2011 at 7:26 PM, John Wickerson <jpw48 at cam.ac.uk> wrote: >>> Hello, >>> >>> I want to write a function that takes a partial-order as a parameter. Specifically, I want the following function... >>> >>> fun interleave :: "'a list => 'a list => 'a partialorder => 'a list set" >>> >>> ... which takes two lists and a partialorder, and returns the set of all interleavings of the elements of those lists which respect the partial order. >>> >>> I know that I could replace "'a partialorder" above with "('a \<times> 'a) set", and then prove a lemma saying "if that parameter is a partial-order then interleave has such-and-such a property". But it would be rather nice just to put the partial-order-ness of that parameter straight into its type. Can I do that, and if so how? >> >> Hi John, >> >> Yes, you certainly can do this. You just need to define the type 'a >> partialorder with a typedef, something like this: >> >> typedef 'a partialorder = "{r::('a * 'a) set. is_partialorder r}" >> >> where "is_partialorder" should be defined ahead of time as a predicate >> asserting that the given relation is a partial order. The typedef will >> require a nonemptiness proof, but that should be easy since the >> equality relation on any type is always a partial order. >> >> For an example of this kind of definition, have a look at >> src/HOL/Multivariate_Analysis/Topology_Euclidean_Space, which defines >> a type called 'a topology consisting of all the possible topologies on >> type 'a. >> >> Hope this helps, >> - Brian > >

**References**:**[isabelle] "partial order" type?***From:*John Wickerson

- Previous by Date: Re: [isabelle] "partial order" type?
- Next by Date: Re: [isabelle] natural number arithmetic normalisation
- Previous by Thread: Re: [isabelle] "partial order" type?
- Next by Thread: Re: [isabelle] "partial order" type?
- Cl-isabelle-users November 2011 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