*To*: Peter Gammie <peteg42 at gmail.com>*Subject*: Re: [isabelle] "partial order" type?*From*: Steven Obua <steven.obua at googlemail.com>*Date*: Sun, 13 Nov 2011 23:38:02 +0000*Cc*: John Wickerson <jpw48 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <83E05DD0-7569-4011-B508-236523E7E650@gmail.com>*References*: <F1C12596-4773-47CF-9D5E-67B727B39F93@cam.ac.uk> <83E05DD0-7569-4011-B508-236523E7E650@gmail.com>

you can also define a new type ala typedef 'a partial_order = those "('a \<times> 'a) set" which correspond to partial orders I don't have the exact syntax at hand right now, but that should point you in the right direction, and it will work. Not sure if it is worth the effort though, you might be better off using an explicit assumption. Cheers, Steven On 13.11.2011, at 22:14, Peter Gammie wrote: > John, > > On 14/11/2011, at 5:26 AM, John Wickerson wrote: > >> 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? > > You can use a type class. See the lattice theories in the HOL distribution, i.e. HOL/Lattices.thy, or the partial order setup in HOLCF. > > The problem (in general) with this approach is that it only allows each type to be partially ordered in one way. If this is an issue then I suggest you use a locale instead, or your original approach. > > cheers > peter > > -- > http://peteg.org/ > >

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

**Re: [isabelle] "partial order" type?***From:*Peter Gammie

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