Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The type class for integer division

Email Gateway (Aug 22 2022 at 09:57):

From: Larry Paulson <lp15@cam.ac.uk>
We currently define the type class semiring_numeral_div in the theory Divides, see attached snippet below. This type class is already general enough to allow some facts involving linearly ordered arithmetic types to be proved just once and be valid over the range from nat to real. The only problem is that type real is not an instance of semiring_numeral_div, for obvious reasons. Would it not be appropriate to attach the axiom le_add_diff_inverse2 to a more general type class, such as linordered_semidom?

Larry

subsection {* Generic numeral division with a pragmatic type class *}

text {*
The following type class contains everything necessary to formulate
a division algorithm in ring structures with numerals, restricted
to its positive segments. This is its primary motiviation, and it
could surely be formulated using a more fine-grained, more algebraic
and less technical class hierarchy.
*}

class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
assumes le_add_diff_inverse2: "b ≤ a ⟹ a - b + b = a"

Email Gateway (Aug 22 2022 at 09:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Larry,

We currently define the type class semiring_numeral_div in the theory
Divides, see attached snippet below. This type class is already general
enough to allow some facts involving linearly ordered arithmetic types
to be proved just once and be valid over the range from nat to real. The
only problem is that type real is not an instance of
semiring_numeral_div, for obvious reasons. Would it not be appropriate
to attach the axiom le_add_diff_inverse2 to a more general type class,
such as linordered_semidom?

this is surely something with can be taken into account. I have
recently refined the type class hierarchy to reflect the concept of
»partial inverse additive operation« up to a certain degree, and this
could be the next step.

Sorry that I won't elaborate further for now, but I am on leave for holiday.

All the best,
Florian

Larry

subsection {* Generic numeral division with a pragmatic type class *}

text {*
The following type class contains everything necessary to formulate
a division algorithm in ring structures with numerals, restricted
to its positive segments. This is its primary motiviation, and it
could surely be formulated using a more fine-grained, more algebraic
and less technical class hierarchy.
*}

class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
assumes le_add_diff_inverse2: "b ≤ a ⟹ a - b + b = a"

signature.asc

Email Gateway (Aug 22 2022 at 10:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

Shall we do this, then? Must something else be done or checked first?

I don't see any obstacle except striving to be consistent, i.e.

Step 1: Re-Join comm_semiring_1_diff_distrib into comm_semiring_1
Step 2: Attach le_add_diff_inverse2 to linordered_semidom

and doing consecutive changes in the sources.

Hence we just state that our distribution's type classes demand a
partial inverse operation for addition with certain properties, beyond
what can be justified from the current specifications -- which is not
critical since these specifications are pragmatically developed and not
an exact counterpart of any development from literature. If at some
time in the future this will expose problems, our system is flexible
enough to insert more intermediate points into the class hierarchy, even
within a particular application.

Cheers,
Florian

On 2 Jun 2015, at 20:49, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:

We currently define the type class semiring_numeral_div in the theory
Divides, see attached snippet below. This type class is already general
enough to allow some facts involving linearly ordered arithmetic types
to be proved just once and be valid over the range from nat to real. The
only problem is that type real is not an instance of
semiring_numeral_div, for obvious reasons. Would it not be appropriate
to attach the axiom le_add_diff_inverse2 to a more general type class,
such as linordered_semidom?

this is surely something with can be taken into account. I have
recently refined the type class hierarchy to reflect the concept of
»partial inverse additive operation« up to a certain degree, and this
could be the next step.

After a closer look at the whole matter, moving le_add_diff_inverse2 to
linordered_semidom seems reasonable (cf. class_deps "{linorder,
semiring, minus}")

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

signature.asc

Email Gateway (Aug 22 2022 at 10:28):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
After a closer look at the whole matter, moving le_add_diff_inverse2 to
linordered_semidom seems reasonable (cf. class_deps "{linorder,
semiring, minus}")

Florian
signature.asc

Email Gateway (Aug 22 2022 at 10:32):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
After a third look, one caveat is whether there are instances of
linordered_semidom which do not satisfy le_add_diff_inverse2 (maybe
polynomials)?

This should be figured out first. In the past I introduced e.g.
comm_semiring_1_diff_distrib since I saw no striking argument why a
partial subtraction in any case should follow a distributive law. Maybe
this has been a little bit overcritical.

If we move on to attach le_add_diff_inverse2 to linordered_semidom, we
should also remerge comm_semiring_1_diff_distrib into comm_semiring_1

Florian
signature.asc

Last updated: Apr 18 2024 at 20:16 UTC