Email Gateway (Nov 26 2024 at 10:59): Email Gateway (Nov 26 2024 at 10:59):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
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@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>
Email Gateway (Apr 23 2025 at 17:24):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Reving this old thread after
https://isabelle.sketis.net/repos/afp-devel/rev/a194ec58339d the
situation is now:
In Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy, type class
ordered_semiring_1 is now also based on zero_neq_one
Hence it should now be equivalent to its counterpart
LLL_Basis_Reduction/Missing_Lemmas.thy
And note that there is also Jordan_Normal_Form/Missing_Ring.thy with
similar type classes.
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.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Apr 25 2025 at 12:12):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
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@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.
Email Gateway (May 02 2025 at 08:44):From: Florian Haftmann <florian.haftmann@cit.tum.de>
But I have big doubts about this:
class partial_abs_if = minus + uminus + ord + zero + abs +
Thoughts?
Looks slightly special indeed.
I would recommend to proceed iteratively and to leave doubtful classes
where they currently are.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (May 02 2025 at 08:44):From: Florian Haftmann <florian.haftmann@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.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (May 05 2025 at 10:06):From: "Thiemann, René via isabelle-dev" <isabelle-dev@mailman.proof.cit.tum.de>
Am 02.05.2025 um 10:44 schrieb Florian Haftmann <florian.haftmann@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é
Last updated: Sep 30 2025 at 16:26 UTC