[isabelle-dev] type class ordered_semiring_1

[Thiemann, René]

> Am 02.05.2025 um 10:44 schrieb Florian Haftmann <florian.haftmann at cit.tum.de>:
> 
>> But why zero_neq_one rather than zero_less_one? Are there really ordered semirings where 0<1 does not hold? Other AFP entries use that version.

> Surely, for an ordering 0 < 1 is a reasonable assumption if 0 =/= 1. 

Although it is a frequently used assumption, 0 < 1 is not satisfied for all ordered semirings.

For instance, for termination proving one sometimes uses semirings where x < y is defined as

x + delta <= y

where delta is some user-specified positive rational number, i.e., for delta = 2, 0 < 1 is not satisfied.

However, since these semirings are not modelled as a type-class, as there are infinitely many possible choices of delta, this should not be a problem for a type-based definition of ordered semiring.

Best,
René