[isabelle-dev] type class ordered_semiring_1

[Lawrence Paulson]

I wonder if we will be able to act on this question before the next release. The key question is precisely how this type class should be defined.

Larry

> On 14 Aug 2024, at 08:58, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
>> This type class is defined in a number of AFP entries. Unfortunately, the definitions used are not the same and it's not clear whether they are equivalent either. We ought to fill this gap, though I am not sure of the best way to do it. In LLL_Basis_Reduction/Missing_Lemmas it is used to generalise a number of simple results currently proved for a smaller type class, ordered_idom.
> 
> Looks interesting.
> 
> A few insights I gained from studying the occurrences:
> 
> a) Abstract-Rewriting/SN_Orders.thy
> 
> This seems somehow special and I would be inclined to put that aside in the first iteration.
> 
> b) (A) Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy and (B) LLL_Basis_Reduction/Missing_Lemmas.thy
> 
> Btw. (A) is an excellent example for separating generic and application-specific material in an AFP entry.
> 
> The two specifications are almost equivalent, since
> 
> subclass (in ordered_semiring_1) ordered_semiring_0 ..
> 
> holds in (A) and thus ordered_semiring_0 could also be removed as initial parent class in (B).
> 
> The remaining difference is zero_less_one. I would be inclined to add that as parent class to (A) to check whether all required instances are still valid.
> 
> After consolidation, the re-integration into HOL-Main could proceed.
> 
> Any thoughts?
> Florian
> <OpenPGP_0xA707172232CFA4E9.asc>