Re: [isabelle] "partial order" type?



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.