[isabelle-dev] Order Relations

[Christian Sternagel]

On 02/19/2013 03:49 PM, Tobias Nipkow wrote:
> Am 19/02/2013 03:50, schrieb Christian Sternagel:
>> I'm not sure how much work it would be to use this new definition of
>> reflexivity. But if people think that what I say makes sense (or is more natural
>> as reflexivity), I would give it a try and report afterwards.
>
> It sounds plausible to me, and I would be in favour of such a change assuming
> that your application profits from it and the distribution does not suffer.

Well, currently my applications are all just based on different 
definitions than those of Main, so there would be no direct gain.

Moreover, relations are represented by "('a * 'a) set" in some places, 
whereas "'a => 'a => bool" (which I prefer, for some reason I'm not 
quite able to put my finger on) is used in others.

In an ideal Isabelle/world I would expect a single definition of 
reflexivity that is applicable everywhere and a clear convention for the 
type of relations (including orderings) that is used uniformly (or at 
least primarily). See. e.g., Ordering.thy vs. Relation.thy for the 
current status.

I know that this might not be feasible right now, but who knows, with a 
lot of small changes in the long run, it might be doable eventually?

cheers

chris