[isabelle-dev] type class ordered_semiring_1

[Lawrence Paulson]

Looking at that, I see the case for these:

class unbounded_dense_order = dense_order + no_top + no_bot
class ordered_semiring_1 = ordered_semiring + semiring_1 + zero_neq_one
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + … (mult_strict_left_mono, mult_strict_right_mono)

They look like they could go into Orderings, Rings, etc.

But I have big doubts about this:

class partial_abs_if = minus + uminus + ord + zero + abs +

Thoughts?

Larry

> On 23 Apr 2025, at 18:16, Florian Haftmann <florian.haftmann at cit.tum.de> wrote:
> 
> I do not know if anybody has an agenda to unify these; a suitable starting point could to be to integrate (parts of) Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy into HOL-Library.Ordered_Rings_and_Fields and then consolidate with the two other theories.