Re: [isabelle] "partial order" type?



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





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