[isabelle-dev] type class ordered_semiring_1

[Florian Haftmann]

> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 19161 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240814/2484829a/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240814/2484829a/attachment.sig>