Re: [isabelle] "partial order" type?



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.